feat(AlgebraicGeometry/Modules): flat sheaves of modules#8
Open
chrisflav wants to merge 6 commits into
Open
Conversation
Port the definition of relative flatness of a sheaf of modules on a scheme over a base, from chrisflav/mathlib4#2. Adds `AlgebraicGeometry.Scheme.Modules.Flat f F`: for a morphism `f : X ⟶ S` and an `𝒪_X`-module `F`, every stalk `F_x` is flat over the local ring `𝒪_{S, f(x)}` acting through `f.stalkMap x`. Main results: the affine criteria (`flat_tilde_iff`, `flat_tilde_iff_of_algebra`), transitivity along a flat base (`Flat.comp`), locality on the base (`flat_comp_isOpenImmersion_iff`) and on the source (`flat_iff_forall_openCover`). Also mirrors the supporting flatness lemmas: `Module.compHom_smul`, `Module.Flat.tensor_tower`, `Module.flat_iff_forall_localizedModule_prime` and friends, and `Module.Flat.trans_compHom` / `Module.Flat.compHom_bijective_iff`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
added
the
awaiting-auto-review
- Generalize `Module.Flat.tensor_tower` to a flat `S`-module `A` (not a ring/algebra) - Derive `flat_iff_forall_localizedModule_prime` from the `_of_algebra` version and reorder - `stalkModule`: use `abbrev`; document why the explicit instance (not `inferInstance`) is pinned - Factor `stalkMap_comp_hom` helper and reuse it; drop semicolon-chained tactics - `haveI` -> `have` in tactic proofs; inline the trivial `e1` - Add module/instance docstrings; document `instModuleStalk` and the `backward.*` options Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav-agent
Bot
force-pushed
the
flat-sheaves-of-modules
branch
from
June 28, 2026 21:27
c5b5a88 to
29f56b5
Compare
chrisflav
commented
Jun 28, 2026
chrisflav
commented
Jun 28, 2026
chrisflav
removed
the
awaiting-auto-review
chrisflav
commented
Jun 28, 2026
chrisflav
added
the
awaiting-orchestra
- RingHom/Flat: state the bijective-scalar criterion for an Algebra + scalar tower (Module.Flat.iff_of_bijective_algebraMap) and derive the compHom version. - Flat/Localization: index the local-global criterion by maximal ideals and drop the unused prime-indexed special case. - AlgebraicGeometry/Modules/Flat: avoid the bare rfl in stalkMap_comp_hom. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
removed
the
awaiting-orchestra
Owner
Author
|
Fix the merge conflict and address the open review comments. |
chrisflav
added
awaiting-orchestra
Owner
Author
|
Fix the merge conflict. |
chrisflav
added
the
awaiting-orchestra
…odules # Conflicts: # MathlibStaging.lean
chrisflav
removed
the
awaiting-orchestra
Introduce ModuleCat.flat : ObjectProperty (ModuleCat R) with an API for restriction of scalars (preservation along flat ring homs, reflection along bijective ones, compatibility with composition), and redefine Scheme.Modules.FlatAt through it, replacing the letI-based definition and proofs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
chrisflav
commented
Jul 6, 2026
Comment on lines
+76
to
+81
| /-- The pointwise flatness condition at a single point `x ∈ X`: the stalk `F_x` is flat over the | ||
| local ring `𝒪_{S, f(x)}`, where the latter acts by restriction of scalars along the stalk map | ||
| `f.stalkMap x`. -/ | ||
| def FlatAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X) : Prop := | ||
| ModuleCat.flat (S.presheaf.stalk (f.base x)) | ||
| ((ModuleCat.restrictScalars (f.stalkMap x).hom).obj (F.stalk x)) |
Owner
Author
There was a problem hiding this comment.
Refactor this file by removing the morphism and S argument from FlatAt and Flat. Show that for a X-module M, the restriction of scalars of M to f^{-1} S is flat if and only if for every stalk, M_x is a flat O_{S, f(x)}-module.
chrisflav
added
the
awaiting-orchestra
Make FlatAt/Flat absolute (flatness of F_x over 𝒪_{X,x}, no morphism/base
arguments), per review. Relative flatness over a base S via f : X ⟶ S is kept
as FlatAtOver/FlatOver (restriction of scalars along the stalk map), with
flatOver_id_iff identifying the absolute notion as the f = 𝟙 X case.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
removed
the
awaiting-orchestra
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Port the definition of relative flatness of a sheaf of modules on a scheme over a base from chrisflav/mathlib4#2 (closes #7).
For a morphism
f : X ⟶ Sand an𝒪_X-moduleF, defineAlgebraicGeometry.Scheme.Modules.Flat f F: at every pointx, the stalkF_xis flat over the local ring𝒪_{S, f(x)}acting throughf.stalkMap x. Main results: the affine criteriaflat_tilde_iffandflat_tilde_iff_of_algebra, transitivity along a flat baseFlat.comp, locality on the baseflat_comp_isOpenImmersion_iff, and locality on the sourceflat_iff_forall_openCover.The supporting flatness lemmas are mirrored into the corresponding files:
Module.compHom_smul,Module.Flat.tensor_tower,Module.flat_iff_forall_localizedModule_primeand friends, andModule.Flat.trans_compHom/Module.Flat.compHom_bijective_iff.The two
changetactics used upstream are replaced to satisfy the stagingbannedTacticslinter: the semilinearity proof derives directly fromrestrictStalkNatIso_hom_smulviaModule.compHom_smul, andflatAt_restrict_iffphrases its module structures over(ι ≫ f).base uso the goal matchesModule.Flat.equiv_iffwithout achange.