feat(AlgebraicGeometry/Modules): flat sheaves of modules#2
Open
chrisflav wants to merge 2 commits into
Open
Conversation
chrisflav-archon-agent
Bot
force-pushed
the
flat-sheaves-of-modules
branch
from
June 27, 2026 14:51
f9701ca to
7fc8b5b
Compare
Define flatness of a sheaf of modules `F` on a scheme `X` over a base `S`
via a morphism `f : X ⟶ S`: `Scheme.Modules.FlatAt f F x` is the pointwise
condition that the stalk `F_x` is flat over `𝒪_{S, f(x)}` (acting through
`f.stalkMap x`), and `Scheme.Modules.Flat f F` asserts `∀ x, FlatAt f F x`.
Main results:
* `Scheme.Modules.flat_tilde_iff` / `flat_tilde_iff_of_algebra`: affine
criteria identifying flatness of `M^~` with flatness of `M`.
* `Scheme.Modules.Flat.comp`: transitivity along a flat base.
* `Scheme.Modules.flat_comp_isOpenImmersion_iff`: locality on the base.
* `Scheme.Modules.flat_iff_forall_openCover`: locality on the source.
Supporting `RingTheory` lemmas:
* `Module.compHom_smul` (`Algebra/Module/RingHom`)
* `Module.Flat.tensor_tower` (`RingTheory/Flat/Stability`)
* `Module.flat_iff_forall_localizedModule_prime`,
`Module.Flat.localizedModule_base`,
`Module.flat_iff_forall_localizedModule_prime_of_algebra`
(`RingTheory/Flat/Localization`)
* `Module.Flat.trans_compHom`, `Module.Flat.compHom_bijective_iff`
(`RingTheory/RingHom/Flat`)
Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
chrisflav-archon-agent
Bot
force-pushed
the
flat-sheaves-of-modules
branch
from
June 27, 2026 15:55
7fc8b5b to
b6270ad
Compare
chrisflav
commented
Jun 27, 2026
chrisflav
added
the
awaiting-orchestra
…tilde_iff_of_algebra Address PR review: derive the affine-case `flat_tilde_iff` (identity morphism) as the special case `f = 𝟙 R` of the general `flat_tilde_iff_of_algebra`, removing the now-redundant identity-specific helpers `Tilde.compHom_stalkMap_id_eq` and `Tilde.stalk_flat_iff`. Note: could not be compiled locally; the branch requires the lean toolchain v4.32.0-rc1 which is not provisioned in this environment. 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.
Define relative flatness of a sheaf of modules
Fon a schemeXover a baseSvia a morphismf : X ⟶ S(AlgebraicGeometry.IsRelativeFlat): for every pointx, the stalkF_xis flat over the local ring𝒪_{S, f(x)}acting throughf.stalkMap x.Main results:
isRelativeFlat_tilde_iffandisRelativeFlat_tilde_iff_of_algebra: the affine criteria identifying relative flatness ofM^~with flatness ofM.IsRelativeFlat.comp: transitivity along a flat base.isRelativeFlat_comp_isOpenImmersion_iff: locality on the base.isRelativeFlat_iff_forall_openCover: locality on the source.Also adds supporting flatness lemmas to
RingTheory:Module.Flat.tensor_tower(RingTheory/Flat/Stability)Module.flat_iff_forall_localizedModule_prime,Module.Flat.localizedModule_base,Module.flat_iff_forall_localizedModule_prime_of_algebra(RingTheory/Flat/Localization)Module.Flat.trans_compHom,Module.Flat.compHom_bijective_iff(RingTheory/RingHom/Flat)