From 4ad28dc63da8d5ee2338ed8525f6273613728574 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Sun, 28 Jun 2026 20:23:53 +0000 Subject: [PATCH 1/5] Add flat sheaves of modules on a scheme MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- MathlibStaging.lean | 5 + MathlibStaging/Algebra/Module/RingHom.lean | 22 ++ .../AlgebraicGeometry/Modules/Flat.lean | 359 ++++++++++++++++++ .../RingTheory/Flat/Localization.lean | 56 +++ MathlibStaging/RingTheory/Flat/Stability.lean | 57 +++ MathlibStaging/RingTheory/RingHom/Flat.lean | 37 ++ 6 files changed, 536 insertions(+) create mode 100644 MathlibStaging/Algebra/Module/RingHom.lean create mode 100644 MathlibStaging/AlgebraicGeometry/Modules/Flat.lean create mode 100644 MathlibStaging/RingTheory/Flat/Localization.lean create mode 100644 MathlibStaging/RingTheory/Flat/Stability.lean create mode 100644 MathlibStaging/RingTheory/RingHom/Flat.lean diff --git a/MathlibStaging.lean b/MathlibStaging.lean index 5b7ab14..2124bdf 100644 --- a/MathlibStaging.lean +++ b/MathlibStaging.lean @@ -1,6 +1,11 @@ import MathlibStaging.Algebra.Category.ModuleCat.Presheaf import MathlibStaging.Algebra.Category.ModuleCat.Presheaf.Submodule +import MathlibStaging.Algebra.Module.RingHom import MathlibStaging.Algebra.Module.Submodule.Map +import MathlibStaging.AlgebraicGeometry.Modules.Flat import MathlibStaging.Init import MathlibStaging.Linter.Staging import MathlibStaging.Meta.Overrides +import MathlibStaging.RingTheory.Flat.Localization +import MathlibStaging.RingTheory.Flat.Stability +import MathlibStaging.RingTheory.RingHom.Flat diff --git a/MathlibStaging/Algebra/Module/RingHom.lean b/MathlibStaging/Algebra/Module/RingHom.lean new file mode 100644 index 0000000..ac657e8 --- /dev/null +++ b/MathlibStaging/Algebra/Module/RingHom.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Module.RingHom +public import MathlibStaging.Init + +/-! +-/ + +@[expose] public section + +variable {R S M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] + +/-- The scalar action of `Module.compHom M f` (restriction of scalars along a ring +homomorphism `f : S →+* R`) is given by `s • m = f s • m`. -/ +lemma Module.compHom_smul [Semiring S] (f : S →+* R) (s : S) (m : M) : + letI := Module.compHom M f; s • m = f s • m := + rfl diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean new file mode 100644 index 0000000..53e8df1 --- /dev/null +++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean @@ -0,0 +1,359 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.AlgebraicGeometry.Modules.Tilde +public import Mathlib.AlgebraicGeometry.Morphisms.Flat +public import MathlibStaging.Algebra.Module.RingHom +public import MathlibStaging.RingTheory.Flat.Localization +public import MathlibStaging.RingTheory.RingHom.Flat +public import MathlibStaging.Init + +/-! +# Flat sheaves of modules + +Given a morphism of schemes `f : X ⟶ S` and an `𝒪_X`-module `F`, we say that `F` is +*flat* over `S` (via `f`) if for every point `x ∈ X`, the stalk `F_x` is a flat module over the +local ring `𝒪_{S, f(x)}`, where `𝒪_{S, f(x)}` acts on `F_x` through the local ring homomorphism +`f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}` induced by `f`. + +## Main definitions + +* `AlgebraicGeometry.Scheme.Modules.stalkModule`: the canonical module structure of the local + ring `𝒪_{X, x}` on the stalk `F_x` of an `𝒪_X`-module `F`. +* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise flatness condition at a point. +* `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting flatness, defined as + `∀ x, FlatAt f F x`. + +## Main results + +* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff`: for a commutative ring `R` and an `R`-module + `M`, the sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if + `M` is a flat `R`-module. +* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff_of_algebra`: the same criterion for a ring map + `f : R ⟶ S` and an `S`-module `M`: the sheaf `M^~` on `Spec S` is flat over `Spec R` + (via `Spec.map f`) if and only if `M` is flat as an `R`-module. +* `AlgebraicGeometry.Scheme.Modules.Flat.comp`: flatness is preserved under composition with a + flat morphism of the base. +* `AlgebraicGeometry.Scheme.Modules.flat_comp_isOpenImmersion_iff`: flatness is local on the base. +* `AlgebraicGeometry.Scheme.Modules.flat_iff_forall_openCover`: flatness is local on the source. +-/ + +@[expose] public noncomputable section + +universe u + +open CategoryTheory TopologicalSpace Opposite + +namespace AlgebraicGeometry + +namespace Scheme.Modules + +/-! ### Flatness of a sheaf of modules -/ + +/-- The canonical module structure of the local ring `𝒪_{X, x}` (the stalk of the structure +sheaf at `x`) on the stalk `F_x` of an `𝒪_X`-module `F`. -/ +@[reducible] +def stalkModule {X : Scheme.{u}} (F : X.Modules) (x : X) : + Module (X.presheaf.stalk x) (F.presheaf.stalk x) := + PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier + (R := X.presheaf) F.val x + +/-- 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 := + letI := stalkModule F x + letI : Module (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x) := + Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom + Module.Flat (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x) + +/-- A sheaf of modules `F` on a scheme `X` is *flat* over `S` via a morphism `f : X ⟶ S` if for +every point `x ∈ X`, the stalk `F_x` is flat over the local ring `𝒪_{S, f(x)}` (acting by +restriction of scalars along the stalk map `f.stalkMap x`), i.e. if `FlatAt f F x` holds at every +point. -/ +class Flat {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : Prop where + flatAt : ∀ x : X, FlatAt f F x + +/-- `Flat f F` holds iff the pointwise condition `FlatAt f F x` holds for all `x`. -/ +theorem flat_iff_forall_flatAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : + Flat f F ↔ ∀ x : X, FlatAt f F x := + ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩ + +end Scheme.Modules + +namespace Tilde + +variable {R : CommRingCat.{u}} (M : ModuleCat.{u} R) + +/-- The local ring `𝒪_{Spec R, x}` is an `R`-algebra (it is the localization of `R` at the prime +corresponding to `x`). -/ +instance instAlgebraStalk (x : PrimeSpectrum.Top R) : + Algebra R ((Spec R).presheaf.stalk x) := + StructureSheaf.stalkAlgebra R x + +instance instIsLocalizationStalk (x : PrimeSpectrum.Top R) : + IsLocalization.AtPrime ((Spec R).presheaf.stalk x) x.asIdeal := + StructureSheaf.IsLocalization.to_stalk R x + +/-- The stalk `(M^~)_x` is a module over the local ring `𝒪_{Spec R, x}`. -/ +instance instModuleStalk (x : PrimeSpectrum.Top R) : + Module ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) := + Scheme.Modules.stalkModule (tilde M) x + +instance instScalarTowerStalk (x : PrimeSpectrum.Top R) : + IsScalarTower R ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) := + IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + +end Tilde + +namespace Scheme.Modules + +/-! ### Transitivity and base-locality of flatness + +We relate `Flat` to flat morphisms of schemes (`AlgebraicGeometry.Flat`), proving that flatness is +transitive along a flat base change and that flatness is local on the base. -/ + +/-- **Transitivity along a flat base.** If a sheaf of modules `F` on `X` is flat over `Y` via +`f : X ⟶ Y`, and `g : Y ⟶ Z` is a flat morphism of schemes, then `F` is flat over `Z` via the +composite `f ≫ g`. -/ +theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Modules) + [hf : Flat f F] [AlgebraicGeometry.Flat g] : Flat (f ≫ g) F := by + refine ⟨fun x ↦ ?_⟩ + simp only [FlatAt] + letI := stalkModule F x + letI : Module (Y.presheaf.stalk (f.base x)) (F.presheaf.stalk x) := + Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom + have hmap : ((f ≫ g).stalkMap x).hom + = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by + rw [Scheme.Hom.stalkMap_comp]; rfl + rw [congrArg (Module.compHom (F.presheaf.stalk x)) hmap] + exact Module.Flat.trans_compHom (g.stalkMap (f.base x)).hom + (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x) + +/-- **Flatness is local on the base.** If `j : V ⟶ S` is an open immersion and `g : X ⟶ V`, then +`F` is flat over `S` via `g ≫ j` if and only if it is flat over `V` via `g`. In other words, +flatness over the base only depends on the base through an open neighbourhood of the image. -/ +theorem flat_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S) + [IsOpenImmersion j] (F : X.Modules) : + Flat (g ≫ j) F ↔ Flat g F := by + have hbij : ∀ x : X, Function.Bijective (j.stalkMap (g.base x)).hom := fun x ↦ + (ConcreteCategory.isIso_iff_bijective (j.stalkMap (g.base x))).mp inferInstance + refine ⟨fun h ↦ ⟨fun x ↦ ?_⟩, fun h ↦ ⟨fun x ↦ ?_⟩⟩ + all_goals + simp only [FlatAt] + letI := stalkModule F x + letI : Module (V.presheaf.stalk (g.base x)) (F.presheaf.stalk x) := + Module.compHom (F.presheaf.stalk x) (g.stalkMap x).hom + have hmap : ((g ≫ j).stalkMap x).hom + = (g.stalkMap x).hom.comp (j.stalkMap (g.base x)).hom := by + rw [Scheme.Hom.stalkMap_comp]; rfl + have hcompHom := congrArg (Module.compHom (F.presheaf.stalk x)) hmap + · have hx := h.flatAt x + simp only [FlatAt] at hx + rw [hcompHom] at hx + exact (Module.Flat.compHom_bijective_iff (j.stalkMap (g.base x)).hom (hbij x)).1 hx + · rw [hcompHom] + exact Module.Flat.trans_compHom (j.stalkMap (g.base x)).hom + (RingHom.Flat.of_bijective (hbij x)) (h.flatAt x) + +/-! ### The affine criterion for an `R`-algebra `S` and an `S`-module `M` + +We generalise `flat_tilde_iff` from the identity morphism on `Spec R` to the morphism +`Spec S ⟶ Spec R` induced by an `R`-algebra `S`, applied to the sheaf `M^~` of an `S`-module `M` +(which is in particular an `R`-module). The result: `M^~` is flat over `Spec R` iff `M` is flat as +an `R`-module. -/ + +/-- The pointwise flatness condition for `M^~` (with `M` an `S`-module, for a ring map `f : R ⟶ S`) +over `Spec R` at a prime `x` of `S` is equivalent to the localization `M_x` being flat over `R` +(with `R` acting on `M` by restriction of scalars along `f`). -/ +theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) + (x : PrimeSpectrum S) : + letI := f.hom.toAlgebra + letI : Module R M := Module.compHom M f.hom + letI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + FlatAt (Spec.map f) (tilde M) x ↔ + Module.Flat R (LocalizedModule x.asIdeal.primeCompl M) := by + letI := f.hom.toAlgebra + letI : Module R M := Module.compHom M f.hom + haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + letI : Module ((Spec R).presheaf.stalk ((Spec.map f).base x)) ((tilde M).presheaf.stalk x) := + Module.compHom ((tilde M).presheaf.stalk x) ((Spec.map f).stalkMap x).hom + letI : Module R ((tilde M).presheaf.stalk x) := + Module.compHom ((tilde M).presheaf.stalk x) f.hom + have hsquare : ∀ r : R, ((Spec.map f).stalkMap x).hom + (algebraMap R ((Spec R).presheaf.stalk ((Spec.map f).base x)) r) + = algebraMap S ((Spec S).presheaf.stalk x) (f.hom r) := fun r ↦ + AlgebraicGeometry.stalkMap_toStalk_apply f x r + haveI : IsScalarTower R S ((tilde M).presheaf.stalk x) := + IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + haveI : IsScalarTower R ((Spec R).presheaf.stalk ((Spec.map f).base x)) + ((tilde M).presheaf.stalk x) := by + refine IsScalarTower.of_algebraMap_smul fun r n ↦ ?_ + rw [Module.compHom_smul, hsquare r, Module.compHom_smul, algebraMap_smul] + simp only [FlatAt] + rw [Module.flat_iff_of_isLocalization ((Spec R).presheaf.stalk ((Spec.map f).base x)) + ((Spec.map f).base x).asIdeal.primeCompl ((tilde M).presheaf.stalk x)] + exact Module.Flat.equiv_iff + ((IsLocalizedModule.linearEquiv x.asIdeal.primeCompl (tilde.toStalk M x).hom + (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)).restrictScalars R) + +/-- **The affine case for an `R`-algebra `S`.** For a ring map `f : R ⟶ S` (an `R`-algebra `S`) and +an `S`-module `M` (hence also an `R`-module, by restriction of scalars), the sheaf `M^~` on `Spec S` +is flat over `Spec R` (via `Spec.map f`) if and only if `M` is a flat `R`-module. -/ +theorem flat_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) : + letI := f.hom.toAlgebra + letI : Module R M := Module.compHom M f.hom + Flat (Spec.map f) (tilde M) ↔ Module.Flat R M := by + letI := f.hom.toAlgebra + letI : Module R M := Module.compHom M f.hom + haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + rw [flat_iff_forall_flatAt, + Module.flat_iff_forall_localizedModule_prime_of_algebra (R := R) (S := S) (M := M)] + refine ⟨fun h q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, ‹_›⟩).mp (h ⟨q, ‹_›⟩), + fun h x ↦ (flatAt_tilde_algebra_iff f M x).mpr (h x.asIdeal)⟩ + +/-- **The affine case.** For a commutative ring `R` and an `R`-module `M`, the quasi-coherent +sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if `M` is a +flat `R`-module. This is the special case of `flat_tilde_iff_of_algebra` for the identity ring +map `𝟙 R`. -/ +theorem flat_tilde_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) : + Flat (𝟙 (Spec R)) (tilde M) ↔ Module.Flat R M := by + rw [← Spec.map_id R] + exact flat_tilde_iff_of_algebra (𝟙 R) M + +/-! ### Flatness is local on the source (open covers) + +We show that flatness can be checked on the members of an open cover of the source: for an open +cover `{Uᵢ}` of `X`, the module `F` is flat over `S` (via `f : X ⟶ S`) iff each restriction +`F|_{Uᵢ}` is flat over `S` (via `Uᵢ ⟶ X ⟶ S`). -/ + +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +/-- The additive isomorphism `(F.restrict ι)_u ≅ F_{ι u}` coming from `restrictStalkNatIso` is +semilinear over the (iso) stalk map `ι.stalkMap u : 𝒪_{X,ι u} ⟶ 𝒪_{U,u}`: scaling by +`ι.stalkMap u c` on the restriction side corresponds to scaling by `c` on `F`. -/ +theorem restrictStalkNatIso_hom_smul {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] + (F : X.Modules) (u : U) (c : X.presheaf.stalk (ι.base u)) + (m : (F.restrict ι).presheaf.stalk u) : + letI := stalkModule (F.restrict ι) u + letI := stalkModule F (ι.base u) + let Φ : (F.restrict ι).presheaf.stalk u → F.presheaf.stalk (ι.base u) := + fun z ↦ (Scheme.Modules.restrictStalkNatIso ι u).hom.app F z + Φ ((ι.stalkMap u).hom c • m) = c • Φ m := by + letI := stalkModule (F.restrict ι) u + letI := stalkModule F (ι.base u) + intro Φ + obtain ⟨V, hV, t, rfl⟩ := X.presheaf.exists_germ_eq c + obtain ⟨W, hW, s, rfl⟩ := (F.restrict ι).presheaf.exists_germ_eq m + rw [Scheme.Hom.germ_stalkMap_apply ι V u hV t] + set W' : U.Opens := W ⊓ ι ⁻¹ᵁ V with hW'def + have huW' : u ∈ W' := ⟨hW, hV⟩ + rw [← TopCat.Presheaf.germ_res_apply U.presheaf (homOfLE inf_le_right : W' ⟶ ι ⁻¹ᵁ V) u huW' + (ι.app V t), + ← TopCat.Presheaf.germ_res_apply (F.restrict ι).presheaf (homOfLE inf_le_left : W' ⟶ W) u + huW' s] + -- combine the `𝒪_U`-side scalar action into a single germ of a section + have lemL : U.presheaf.germ W' u huW' (U.presheaf.map (homOfLE inf_le_right).op (ι.app V t)) + • (F.restrict ι).presheaf.germ W' u huW' + ((F.restrict ι).presheaf.map (homOfLE inf_le_left).op s) + = (F.restrict ι).presheaf.germ W' u huW' + (U.presheaf.map (homOfLE inf_le_right).op (ι.app V t) + • (F.restrict ι).presheaf.map (homOfLE inf_le_left).op s) := + (PresheafOfModules.germ_smul (R := U.presheaf) (F.restrict ι).val u W' huW' _ _).symm + rw [lemL] + -- push `Φ` through germs of the restricted module + have hΦ : ∀ (A : U.Opens) (h : u ∈ A) (z : Γ(F.restrict ι, A)), + Φ ((F.restrict ι).presheaf.germ A u h z) + = F.presheaf.germ (ι ''ᵁ A) (ι.base u) ⟨u, h, rfl⟩ z := by + intro A h z + have e1 : Φ ((F.restrict ι).presheaf.germ A u h z) + = ((F.restrict ι).presheaf.germ A u h + ≫ (Scheme.Modules.restrictStalkNatIso ι u).hom.app F) z := rfl + rw [e1] + exact DFunLike.congr_fun (congrArg ConcreteCategory.hom + (Scheme.Modules.germ_restrictStalkNatIso_hom_app ι u F h)) z + rw [hΦ, hΦ, Scheme.Modules.restrict_map] + -- align the `𝒪_X`-germ of `t` over `ι ''ᵁ W'` and combine the `F`-side action + have hsub : ι ''ᵁ W' ≤ V := by rintro _ ⟨p, hp, rfl⟩; exact hp.2 + rw [← TopCat.Presheaf.germ_res_apply X.presheaf (homOfLE hsub : ι ''ᵁ W' ⟶ V) (ι.base u) + ⟨u, huW', rfl⟩ t] + have lemR : X.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩ + (X.presheaf.map (homOfLE hsub).op t) + • F.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩ + (F.presheaf.map (ι.opensFunctor.map (homOfLE inf_le_left)).op s) + = F.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩ + (X.presheaf.map (homOfLE hsub).op t + • F.presheaf.map (ι.opensFunctor.map (homOfLE inf_le_left)).op s) := + (PresheafOfModules.germ_smul (R := X.presheaf) F.val (ι.base u) (ι ''ᵁ W') ⟨u, huW', rfl⟩ + _ _).symm + -- the structure-sheaf identity comparing the two scalars + have F2 : (ι.appIso W').inv + (U.presheaf.map (homOfLE (inf_le_right : W' ≤ ι ⁻¹ᵁ V)).op (ι.app V t)) + = X.presheaf.map (homOfLE hsub).op t := by + have F2mor : ι.app V ≫ U.presheaf.map (homOfLE (inf_le_right : W' ≤ ι ⁻¹ᵁ V)).op + ≫ (ι.appIso W').inv = X.presheaf.map (homOfLE hsub).op := by + rw [Scheme.Hom.appIso_inv_naturality, Scheme.Hom.app_appIso_inv_assoc, ← Functor.map_comp] + rfl + rw [← F2mor]; rfl + -- conclude: both germs are of the same section of `F`, using the scalar identity `F2` + refine Eq.trans (congrArg _ ?_) lemR.symm + exact congrArg + (· • F.presheaf.map (ι.opensFunctor.map (homOfLE (inf_le_left : W ⊓ ι ⁻¹ᵁ V ≤ W))).op s) F2 + +/-- **Pointwise comparison under restriction to an open subscheme.** For an open immersion +`ι : U ⟶ X`, the flatness of the restricted module `F|_U` at `u` (over `S`, via `ι ≫ f`) is +equivalent to the flatness of `F` at `ι(u)`. This holds because the stalk map of an open immersion +is an isomorphism, so restriction does not change the stalk data. -/ +theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] + (f : X ⟶ S) (F : X.Modules) (u : U) : + FlatAt (ι ≫ f) (F.restrict ι) u ↔ FlatAt f F (ι.base u) := by + letI := stalkModule (F.restrict ι) u + letI := stalkModule F (ι.base u) + let Φe : (F.restrict ι).presheaf.stalk u ≃+ F.presheaf.stalk (ι.base u) := + ((Scheme.Modules.restrictStalkNatIso ι u).app F).addCommGroupIsoToAddEquiv + -- The two stalk-map base points `(ι ≫ f) u` and `f (ι u)` only agree up to + -- `Scheme.Hom.comp_base`; we phrase the module structures over the former (matching the + -- left-hand `FlatAt` syntactically), letting `f.stalkMap (ι.base u)` act through the latter. + letI : Module (S.presheaf.stalk ((ι ≫ f).base u)) ((F.restrict ι).presheaf.stalk u) := + Module.compHom ((F.restrict ι).presheaf.stalk u) ((ι ≫ f).stalkMap u).hom + letI : Module (S.presheaf.stalk ((ι ≫ f).base u)) (F.presheaf.stalk (ι.base u)) := + Module.compHom (F.presheaf.stalk (ι.base u)) (f.stalkMap (ι.base u)).hom + let e : (F.restrict ι).presheaf.stalk u ≃ₗ[S.presheaf.stalk ((ι ≫ f).base u)] + F.presheaf.stalk (ι.base u) := + Φe.toLinearEquiv (by + intro b m + have hb : ((ι ≫ f).stalkMap u).hom b + = (ι.stalkMap u).hom ((f.stalkMap (ι.base u)).hom b) := by + rw [Scheme.Hom.stalkMap_comp]; rfl + have key := restrictStalkNatIso_hom_smul ι F u ((f.stalkMap (ι.base u)).hom b) m + rw [← hb] at key + exact key) + exact Module.Flat.equiv_iff e + +/-- Flatness of the restriction of `F` to an open subscheme `U` (via `ι ≫ f`) is equivalent to the +pointwise flatness of `F` at every point of `U`. -/ +theorem flat_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] + (f : X ⟶ S) (F : X.Modules) : + Flat (ι ≫ f) (F.restrict ι) ↔ ∀ u : U, FlatAt f F (ι.base u) := by + rw [flat_iff_forall_flatAt] + exact forall_congr' fun u ↦ flatAt_restrict_iff ι f F u + +/-- **Flatness is local on the source.** For an open cover `𝒰` of `X`, the module `F` is flat over +`S` (via `f`) if and only if for every member `Uᵢ` of the cover, the restriction `F|_{Uᵢ}` is flat +over `S` (via `𝒰.f i ≫ f`). -/ +theorem flat_iff_forall_openCover {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) + (𝒰 : X.OpenCover) : + Flat f F ↔ ∀ i, Flat (𝒰.f i ≫ f) (F.restrict (𝒰.f i)) := by + simp_rw [flat_restrict_iff, flat_iff_forall_flatAt] + refine ⟨fun h i u ↦ h _, fun h x ↦ ?_⟩ + obtain ⟨u, hu⟩ := 𝒰.covers x + rw [← hu] + exact h (𝒰.idx x) u + +end Scheme.Modules + +end AlgebraicGeometry diff --git a/MathlibStaging/RingTheory/Flat/Localization.lean b/MathlibStaging/RingTheory/Flat/Localization.lean new file mode 100644 index 0000000..3bd3986 --- /dev/null +++ b/MathlibStaging/RingTheory/Flat/Localization.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.RingTheory.Flat.Localization +public import MathlibStaging.RingTheory.Flat.Stability +public import MathlibStaging.Init + +/-! +-/ + +@[expose] public section + +open scoped TensorProduct + +/-- A module `N` over a commutative ring `R` is flat if and only if its localization at every +prime ideal is flat over `R`. -/ +theorem Module.flat_iff_forall_localizedModule_prime (R : Type*) [CommRing R] (N : Type*) + [AddCommGroup N] [Module R N] : + Module.Flat R N ↔ + ∀ (p : Ideal R) [p.IsPrime], Module.Flat R (LocalizedModule p.primeCompl N) := by + refine ⟨fun _ p _ ↦ ?_, fun h ↦ Module.flat_of_localized_maximal _ fun P hP ↦ ?_⟩ + · have : Module.Flat (Localization p.primeCompl) (LocalizedModule p.primeCompl N) := + Module.Flat.localizedModule _ + have : Module.Flat R (Localization p.primeCompl) := IsLocalization.flat _ p.primeCompl + exact Module.Flat.trans R (Localization p.primeCompl) _ + · haveI := hP.isPrime + exact h P + +/-- Localising an `R`-flat module (which is also a module over an `R`-algebra `S`) at a submonoid +of `S` yields again an `R`-flat module. -/ +theorem Module.Flat.localizedModule_base {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] + (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] + (q : Submonoid S) [Module.Flat R M] : + Module.Flat R (LocalizedModule q M) := by + have e : LocalizedModule q M ≃ₗ[R] (Localization q ⊗[S] M) := + (LocalizedModule.equivTensorProduct q M).restrictScalars R + haveI : Module.Flat S (Localization q) := IsLocalization.flat (Localization q) q + haveI : Module.Flat R (Localization q ⊗[S] M) := Module.Flat.tensor_tower (Localization q) M + exact Module.Flat.of_linearEquiv e + +/-- **Local–global flatness over a base, indexed by primes of `S`.** For an `R`-algebra `S` and an +`S`-module `M`, `M` is flat over `R` iff its localization at every prime of `S` is flat over `R`. -/ +theorem Module.flat_iff_forall_localizedModule_prime_of_algebra {R S : Type*} [CommRing R] + [CommRing S] [Algebra R S] (M : Type*) [AddCommGroup M] [Module R M] [Module S M] + [IsScalarTower R S M] : + Module.Flat R M ↔ + ∀ (q : Ideal S) [q.IsPrime], Module.Flat R (LocalizedModule q.primeCompl M) := by + refine ⟨fun _ q _ ↦ Module.Flat.localizedModule_base M q.primeCompl, fun h ↦ ?_⟩ + refine Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M) + (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P hP ↦ ?_ + haveI := hP.isPrime + exact h P diff --git a/MathlibStaging/RingTheory/Flat/Stability.lean b/MathlibStaging/RingTheory/Flat/Stability.lean new file mode 100644 index 0000000..d6acdcb --- /dev/null +++ b/MathlibStaging/RingTheory/Flat/Stability.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.RingTheory.Flat.Stability +public import MathlibStaging.Init + +/-! +-/ + +@[expose] public section + +open scoped TensorProduct + +namespace Module.Flat + +section TensorTower + +/-- **Flatness of a tensor product over a tower.** If `A` is a flat `S`-algebra and `M` is a flat +`R`-module (where `R → S → A` is a tower), then `A ⊗[S] M` is a flat `R`-module. -/ +theorem tensor_tower {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] + (A : Type*) [CommRing A] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [Flat S A] + (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Flat R M] : + Flat R (A ⊗[S] M) := by + rw [iff_lTensor_preserves_injective_linearMap] + intro N N' _ _ _ _ f hf + let g : M ⊗[R] N →ₗ[S] M ⊗[R] N' := TensorProduct.AlgebraTensorModule.lTensor S M f + have hg : Function.Injective g := by + have hcoe : (g : M ⊗[R] N → M ⊗[R] N') = LinearMap.lTensor M f := by ext x; rfl + rw [hcoe] + exact lTensor_preserves_injective_linearMap (M := M) f hf + have hbot : Function.Injective (LinearMap.lTensor A g) := + lTensor_preserves_injective_linearMap (M := A) g hg + let eN := TensorProduct.AlgebraTensorModule.assoc R S S A M N + let eN' := TensorProduct.AlgebraTensorModule.assoc R S S A M N' + have hsqL : eN'.toLinearMap.restrictScalars R ∘ₗ LinearMap.lTensor (A ⊗[S] M) f + = (LinearMap.lTensor A g).restrictScalars R ∘ₗ eN.toLinearMap.restrictScalars R := by + apply TensorProduct.ext' + intro w n + induction w using TensorProduct.induction_on with + | zero => simp + | tmul x y => simp [eN, eN', g, TensorProduct.AlgebraTensorModule.assoc_tmul, + TensorProduct.AlgebraTensorModule.lTensor_tmul] + | add a b ha hb => simp [TensorProduct.add_tmul, map_add, ha, hb] + have hsq : (eN' : _ → _) ∘ LinearMap.lTensor (A ⊗[S] M) f + = LinearMap.lTensor A g ∘ (eN : _ → _) := by + simpa using congrArg (fun L : _ →ₗ[R] _ ↦ (L : _ → _)) hsqL + have hcomp : Function.Injective ((eN' : _ → _) ∘ LinearMap.lTensor (A ⊗[S] M) f) := by + rw [hsq]; exact hbot.comp eN.injective + exact hcomp.of_comp + +end TensorTower + +end Module.Flat diff --git a/MathlibStaging/RingTheory/RingHom/Flat.lean b/MathlibStaging/RingTheory/RingHom/Flat.lean new file mode 100644 index 0000000..45e2b9e --- /dev/null +++ b/MathlibStaging/RingTheory/RingHom/Flat.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.RingTheory.RingHom.Flat +public import MathlibStaging.Init + +/-! +-/ + +@[expose] public section + +/-- If `M` is an `S`-module that is flat over `S`, and `φ : R →+* S` is a flat ring homomorphism, +then `M` is flat over `R` for the module structure obtained by restricting scalars along `φ`. -/ +theorem Module.Flat.trans_compHom {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) + {M : Type*} [AddCommGroup M] [Module S M] (hφ : RingHom.Flat φ) (hM : Module.Flat S M) : + letI := Module.compHom M φ; Module.Flat R M := by + letI := φ.toAlgebra + letI := Module.compHom M φ + haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + haveI : Module.Flat R S := hφ + exact Module.Flat.trans R S M + +/-- Restricting scalars along a bijective ring homomorphism preserves and reflects flatness. -/ +theorem Module.Flat.compHom_bijective_iff {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) + (hφ : Function.Bijective φ) {M : Type*} [AddCommGroup M] [Module S M] : + (letI := Module.compHom M φ; Module.Flat R M) ↔ Module.Flat S M := by + refine ⟨fun hM ↦ ?_, fun hM ↦ Module.Flat.trans_compHom φ (.of_bijective hφ) hM⟩ + letI := Module.compHom M φ + let e : R ≃+* S := RingEquiv.ofBijective φ hφ + have key := Module.Flat.trans_compHom e.symm.toRingHom (.of_bijective e.symm.bijective) hM + have h : (inferInstanceAs (Module S M)) = Module.compHom M e.symm.toRingHom := + Module.ext' _ _ fun s m ↦ (congrArg (· • m) (e.apply_symm_apply s)).symm + rwa [← h] at key From 29f56b5d07643a2a0b6f5fa40a2e71b24146f002 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Sun, 28 Jun 2026 21:26:08 +0000 Subject: [PATCH 2/5] Address review on flat sheaves of modules - 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 --- .../AlgebraicGeometry/Modules/Flat.lean | 58 +++++++++++-------- .../RingTheory/Flat/Localization.lean | 29 ++++------ MathlibStaging/RingTheory/Flat/Stability.lean | 14 +++-- MathlibStaging/RingTheory/RingHom/Flat.lean | 4 +- 4 files changed, 58 insertions(+), 47 deletions(-) diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean index 53e8df1..432ecb0 100644 --- a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean +++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean @@ -55,9 +55,12 @@ namespace Scheme.Modules /-! ### Flatness of a sheaf of modules -/ /-- The canonical module structure of the local ring `𝒪_{X, x}` (the stalk of the structure -sheaf at `x`) on the stalk `F_x` of an `𝒪_X`-module `F`. -/ -@[reducible] -def stalkModule {X : Scheme.{u}} (F : X.Modules) (x : X) : +sheaf at `x`) on the stalk `F_x` of an `𝒪_X`-module `F`. + +We pin the `PresheafOfModules`-instance explicitly rather than via `inferInstance`: `Stalk.lean` +registers two definitionally-equal `Module (X.presheaf.stalk x) _` instances, and the downstream +germ-level rewrites (e.g. via `PresheafOfModules.germ_smul`) only match against this one. -/ +abbrev stalkModule {X : Scheme.{u}} (F : X.Modules) (x : X) : Module (X.presheaf.stalk x) (F.presheaf.stalk x) := PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier (R := X.presheaf) F.val x @@ -95,15 +98,20 @@ instance instAlgebraStalk (x : PrimeSpectrum.Top R) : Algebra R ((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra R x +/-- The local ring `𝒪_{Spec R, x}` is the localization of `R` at the prime `x`. -/ instance instIsLocalizationStalk (x : PrimeSpectrum.Top R) : IsLocalization.AtPrime ((Spec R).presheaf.stalk x) x.asIdeal := StructureSheaf.IsLocalization.to_stalk R x -/-- The stalk `(M^~)_x` is a module over the local ring `𝒪_{Spec R, x}`. -/ +/-- The stalk `(M^~)_x` is a module over the local ring `𝒪_{Spec R, x}`. This re-exposes the +canonical `PresheafOfModules`-instance: typeclass search does not otherwise find it through the +`SheafOfModules.presheaf` projection, so the downstream `IsScalarTower`/flatness statements rely on +it being registered here. -/ instance instModuleStalk (x : PrimeSpectrum.Top R) : Module ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) := Scheme.Modules.stalkModule (tilde M) x +/-- The actions of `R` and the local ring `𝒪_{Spec R, x}` on the stalk `(M^~)_x` are compatible. -/ instance instScalarTowerStalk (x : PrimeSpectrum.Top R) : IsScalarTower R ((Spec R).presheaf.stalk x) ((tilde M).presheaf.stalk x) := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl @@ -117,6 +125,13 @@ namespace Scheme.Modules We relate `Flat` to flat morphisms of schemes (`AlgebraicGeometry.Flat`), proving that flatness is transitive along a flat base change and that flatness is local on the base. -/ +/-- The underlying ring homomorphism of the stalk map of a composition factors as the composition +of the underlying ring homomorphisms of the stalk maps. -/ +lemma stalkMap_comp_hom {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : + ((f ≫ g).stalkMap x).hom = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by + rw [Scheme.Hom.stalkMap_comp] + rfl + /-- **Transitivity along a flat base.** If a sheaf of modules `F` on `X` is flat over `Y` via `f : X ⟶ Y`, and `g : Y ⟶ Z` is a flat morphism of schemes, then `F` is flat over `Z` via the composite `f ≫ g`. -/ @@ -127,10 +142,7 @@ theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Module letI := stalkModule F x letI : Module (Y.presheaf.stalk (f.base x)) (F.presheaf.stalk x) := Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom - have hmap : ((f ≫ g).stalkMap x).hom - = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by - rw [Scheme.Hom.stalkMap_comp]; rfl - rw [congrArg (Module.compHom (F.presheaf.stalk x)) hmap] + rw [congrArg (Module.compHom (F.presheaf.stalk x)) (stalkMap_comp_hom f g x)] exact Module.Flat.trans_compHom (g.stalkMap (f.base x)).hom (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x) @@ -148,10 +160,7 @@ theorem flat_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V letI := stalkModule F x letI : Module (V.presheaf.stalk (g.base x)) (F.presheaf.stalk x) := Module.compHom (F.presheaf.stalk x) (g.stalkMap x).hom - have hmap : ((g ≫ j).stalkMap x).hom - = (g.stalkMap x).hom.comp (j.stalkMap (g.base x)).hom := by - rw [Scheme.Hom.stalkMap_comp]; rfl - have hcompHom := congrArg (Module.compHom (F.presheaf.stalk x)) hmap + have hcompHom := congrArg (Module.compHom (F.presheaf.stalk x)) (stalkMap_comp_hom g j x) · have hx := h.flatAt x simp only [FlatAt] at hx rw [hcompHom] at hx @@ -179,7 +188,7 @@ theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Modu Module.Flat R (LocalizedModule x.asIdeal.primeCompl M) := by letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom - haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl letI : Module ((Spec R).presheaf.stalk ((Spec.map f).base x)) ((tilde M).presheaf.stalk x) := Module.compHom ((tilde M).presheaf.stalk x) ((Spec.map f).stalkMap x).hom letI : Module R ((tilde M).presheaf.stalk x) := @@ -188,9 +197,9 @@ theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Modu (algebraMap R ((Spec R).presheaf.stalk ((Spec.map f).base x)) r) = algebraMap S ((Spec S).presheaf.stalk x) (f.hom r) := fun r ↦ AlgebraicGeometry.stalkMap_toStalk_apply f x r - haveI : IsScalarTower R S ((tilde M).presheaf.stalk x) := + have : IsScalarTower R S ((tilde M).presheaf.stalk x) := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl - haveI : IsScalarTower R ((Spec R).presheaf.stalk ((Spec.map f).base x)) + have : IsScalarTower R ((Spec R).presheaf.stalk ((Spec.map f).base x)) ((tilde M).presheaf.stalk x) := by refine IsScalarTower.of_algebraMap_smul fun r n ↦ ?_ rw [Module.compHom_smul, hsquare r, Module.compHom_smul, algebraMap_smul] @@ -210,7 +219,7 @@ theorem flat_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Mod Flat (Spec.map f) (tilde M) ↔ Module.Flat R M := by letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom - haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl rw [flat_iff_forall_flatAt, Module.flat_iff_forall_localizedModule_prime_of_algebra (R := R) (S := S) (M := M)] refine ⟨fun h q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, ‹_›⟩).mp (h ⟨q, ‹_›⟩), @@ -231,6 +240,9 @@ We show that flatness can be checked on the members of an open cover of the sour cover `{Uᵢ}` of `X`, the module `F` is flat over `S` (via `f : X ⟶ S`) iff each restriction `F|_{Uᵢ}` is flat over `S` (via `Uᵢ ⟶ X ⟶ S`). -/ +-- The `rw`s below rewrite scalar actions on stalks whose module instance enters the goal as a +-- `letI`-bound local instance, while `PresheafOfModules.germ_smul` phrases the action through the +-- canonical instance. These are defeq but not syntactically equal, so `rw` needs the relaxed defeq. set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The additive isomorphism `(F.restrict ι)_u ≅ F_{ι u}` coming from `restrictStalkNatIso` is @@ -270,15 +282,13 @@ theorem restrictStalkNatIso_hom_smul {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenIm Φ ((F.restrict ι).presheaf.germ A u h z) = F.presheaf.germ (ι ''ᵁ A) (ι.base u) ⟨u, h, rfl⟩ z := by intro A h z - have e1 : Φ ((F.restrict ι).presheaf.germ A u h z) - = ((F.restrict ι).presheaf.germ A u h - ≫ (Scheme.Modules.restrictStalkNatIso ι u).hom.app F) z := rfl - rw [e1] exact DFunLike.congr_fun (congrArg ConcreteCategory.hom (Scheme.Modules.germ_restrictStalkNatIso_hom_app ι u F h)) z rw [hΦ, hΦ, Scheme.Modules.restrict_map] -- align the `𝒪_X`-germ of `t` over `ι ''ᵁ W'` and combine the `F`-side action - have hsub : ι ''ᵁ W' ≤ V := by rintro _ ⟨p, hp, rfl⟩; exact hp.2 + have hsub : ι ''ᵁ W' ≤ V := by + rintro _ ⟨p, hp, rfl⟩ + exact hp.2 rw [← TopCat.Presheaf.germ_res_apply X.presheaf (homOfLE hsub : ι ''ᵁ W' ⟶ V) (ι.base u) ⟨u, huW', rfl⟩ t] have lemR : X.presheaf.germ (ι ''ᵁ W') (ι.base u) ⟨u, huW', rfl⟩ @@ -298,7 +308,8 @@ theorem restrictStalkNatIso_hom_smul {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenIm ≫ (ι.appIso W').inv = X.presheaf.map (homOfLE hsub).op := by rw [Scheme.Hom.appIso_inv_naturality, Scheme.Hom.app_appIso_inv_assoc, ← Functor.map_comp] rfl - rw [← F2mor]; rfl + rw [← F2mor] + rfl -- conclude: both germs are of the same section of `F`, using the scalar identity `F2` refine Eq.trans (congrArg _ ?_) lemR.symm exact congrArg @@ -328,7 +339,8 @@ theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion intro b m have hb : ((ι ≫ f).stalkMap u).hom b = (ι.stalkMap u).hom ((f.stalkMap (ι.base u)).hom b) := by - rw [Scheme.Hom.stalkMap_comp]; rfl + rw [stalkMap_comp_hom ι f u] + rfl have key := restrictStalkNatIso_hom_smul ι F u ((f.stalkMap (ι.base u)).hom b) m rw [← hb] at key exact key) diff --git a/MathlibStaging/RingTheory/Flat/Localization.lean b/MathlibStaging/RingTheory/Flat/Localization.lean index 3bd3986..2bc7af1 100644 --- a/MathlibStaging/RingTheory/Flat/Localization.lean +++ b/MathlibStaging/RingTheory/Flat/Localization.lean @@ -16,20 +16,6 @@ public import MathlibStaging.Init open scoped TensorProduct -/-- A module `N` over a commutative ring `R` is flat if and only if its localization at every -prime ideal is flat over `R`. -/ -theorem Module.flat_iff_forall_localizedModule_prime (R : Type*) [CommRing R] (N : Type*) - [AddCommGroup N] [Module R N] : - Module.Flat R N ↔ - ∀ (p : Ideal R) [p.IsPrime], Module.Flat R (LocalizedModule p.primeCompl N) := by - refine ⟨fun _ p _ ↦ ?_, fun h ↦ Module.flat_of_localized_maximal _ fun P hP ↦ ?_⟩ - · have : Module.Flat (Localization p.primeCompl) (LocalizedModule p.primeCompl N) := - Module.Flat.localizedModule _ - have : Module.Flat R (Localization p.primeCompl) := IsLocalization.flat _ p.primeCompl - exact Module.Flat.trans R (Localization p.primeCompl) _ - · haveI := hP.isPrime - exact h P - /-- Localising an `R`-flat module (which is also a module over an `R`-algebra `S`) at a submonoid of `S` yields again an `R`-flat module. -/ theorem Module.Flat.localizedModule_base {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] @@ -38,8 +24,8 @@ theorem Module.Flat.localizedModule_base {R S : Type*} [CommRing R] [CommRing S] Module.Flat R (LocalizedModule q M) := by have e : LocalizedModule q M ≃ₗ[R] (Localization q ⊗[S] M) := (LocalizedModule.equivTensorProduct q M).restrictScalars R - haveI : Module.Flat S (Localization q) := IsLocalization.flat (Localization q) q - haveI : Module.Flat R (Localization q ⊗[S] M) := Module.Flat.tensor_tower (Localization q) M + have : Module.Flat S (Localization q) := IsLocalization.flat (Localization q) q + have : Module.Flat R (Localization q ⊗[S] M) := Module.Flat.tensor_tower (Localization q) M exact Module.Flat.of_linearEquiv e /-- **Local–global flatness over a base, indexed by primes of `S`.** For an `R`-algebra `S` and an @@ -52,5 +38,14 @@ theorem Module.flat_iff_forall_localizedModule_prime_of_algebra {R S : Type*} [C refine ⟨fun _ q _ ↦ Module.Flat.localizedModule_base M q.primeCompl, fun h ↦ ?_⟩ refine Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M) (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P hP ↦ ?_ - haveI := hP.isPrime + have := hP.isPrime exact h P + +/-- A module `N` over a commutative ring `R` is flat if and only if its localization at every +prime ideal is flat over `R`. This is the special case of +`Module.flat_iff_forall_localizedModule_prime_of_algebra` for `S := R`. -/ +theorem Module.flat_iff_forall_localizedModule_prime (R : Type*) [CommRing R] (N : Type*) + [AddCommGroup N] [Module R N] : + Module.Flat R N ↔ + ∀ (p : Ideal R) [p.IsPrime], Module.Flat R (LocalizedModule p.primeCompl N) := + Module.flat_iff_forall_localizedModule_prime_of_algebra (S := R) N diff --git a/MathlibStaging/RingTheory/Flat/Stability.lean b/MathlibStaging/RingTheory/Flat/Stability.lean index d6acdcb..366c63e 100644 --- a/MathlibStaging/RingTheory/Flat/Stability.lean +++ b/MathlibStaging/RingTheory/Flat/Stability.lean @@ -19,17 +19,20 @@ namespace Module.Flat section TensorTower -/-- **Flatness of a tensor product over a tower.** If `A` is a flat `S`-algebra and `M` is a flat -`R`-module (where `R → S → A` is a tower), then `A ⊗[S] M` is a flat `R`-module. -/ +/-- **Flatness of a tensor product over a tower.** If `A` is a flat `S`-module and `M` is a flat +`R`-module (where `R → S` is an algebra and `A`, `M` carry compatible scalar towers), then +`A ⊗[S] M` is a flat `R`-module. -/ theorem tensor_tower {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] - (A : Type*) [CommRing A] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [Flat S A] + (A : Type*) [AddCommGroup A] [Module S A] [Module R A] [IsScalarTower R S A] [Flat S A] (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Flat R M] : Flat R (A ⊗[S] M) := by rw [iff_lTensor_preserves_injective_linearMap] intro N N' _ _ _ _ f hf let g : M ⊗[R] N →ₗ[S] M ⊗[R] N' := TensorProduct.AlgebraTensorModule.lTensor S M f have hg : Function.Injective g := by - have hcoe : (g : M ⊗[R] N → M ⊗[R] N') = LinearMap.lTensor M f := by ext x; rfl + have hcoe : (g : M ⊗[R] N → M ⊗[R] N') = LinearMap.lTensor M f := by + ext x + rfl rw [hcoe] exact lTensor_preserves_injective_linearMap (M := M) f hf have hbot : Function.Injective (LinearMap.lTensor A g) := @@ -49,7 +52,8 @@ theorem tensor_tower {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] = LinearMap.lTensor A g ∘ (eN : _ → _) := by simpa using congrArg (fun L : _ →ₗ[R] _ ↦ (L : _ → _)) hsqL have hcomp : Function.Injective ((eN' : _ → _) ∘ LinearMap.lTensor (A ⊗[S] M) f) := by - rw [hsq]; exact hbot.comp eN.injective + rw [hsq] + exact hbot.comp eN.injective exact hcomp.of_comp end TensorTower diff --git a/MathlibStaging/RingTheory/RingHom/Flat.lean b/MathlibStaging/RingTheory/RingHom/Flat.lean index 45e2b9e..a332e7a 100644 --- a/MathlibStaging/RingTheory/RingHom/Flat.lean +++ b/MathlibStaging/RingTheory/RingHom/Flat.lean @@ -20,8 +20,8 @@ theorem Module.Flat.trans_compHom {R S : Type*} [CommRing R] [CommRing S] (φ : letI := Module.compHom M φ; Module.Flat R M := by letI := φ.toAlgebra letI := Module.compHom M φ - haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl - haveI : Module.Flat R S := hφ + have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + have : Module.Flat R S := hφ exact Module.Flat.trans R S M /-- Restricting scalars along a bijective ring homomorphism preserves and reflects flatness. -/ From cbe3e8c3d80cec74ce1cb55d61cbc6c5ee427874 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Sun, 28 Jun 2026 22:24:41 +0000 Subject: [PATCH 3/5] Address review on flat sheaves of modules (round 2) - 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 --- .../AlgebraicGeometry/Modules/Flat.lean | 12 +++++---- .../RingTheory/Flat/Localization.lean | 24 +++++------------ MathlibStaging/RingTheory/RingHom/Flat.lean | 27 ++++++++++++++----- 3 files changed, 35 insertions(+), 28 deletions(-) diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean index 432ecb0..d9b90f1 100644 --- a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean +++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean @@ -130,7 +130,7 @@ of the underlying ring homomorphisms of the stalk maps. -/ lemma stalkMap_comp_hom {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : ((f ≫ g).stalkMap x).hom = (f.stalkMap x).hom.comp (g.stalkMap (f.base x)).hom := by rw [Scheme.Hom.stalkMap_comp] - rfl + exact CommRingCat.hom_comp _ _ /-- **Transitivity along a flat base.** If a sheaf of modules `F` on `X` is flat over `Y` via `f : X ⟶ Y`, and `g : Y ⟶ Z` is a flat morphism of schemes, then `F` is flat over `Z` via the @@ -220,10 +220,12 @@ theorem flat_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Mod letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl - rw [flat_iff_forall_flatAt, - Module.flat_iff_forall_localizedModule_prime_of_algebra (R := R) (S := S) (M := M)] - refine ⟨fun h q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, ‹_›⟩).mp (h ⟨q, ‹_›⟩), - fun h x ↦ (flatAt_tilde_algebra_iff f M x).mpr (h x.asIdeal)⟩ + rw [flat_iff_forall_flatAt] + refine ⟨fun h ↦ (Module.flat_iff_forall_localizedModule_maximal_of_algebra (R := R) (S := S) + (M := M)).mpr fun q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, inferInstance⟩).mp + (h ⟨q, inferInstance⟩), + fun hM x ↦ (flatAt_tilde_algebra_iff f M x).mpr + (Module.Flat.localizedModule_base M x.asIdeal.primeCompl)⟩ /-- **The affine case.** For a commutative ring `R` and an `R`-module `M`, the quasi-coherent sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if `M` is a diff --git a/MathlibStaging/RingTheory/Flat/Localization.lean b/MathlibStaging/RingTheory/Flat/Localization.lean index 2bc7af1..c31dec7 100644 --- a/MathlibStaging/RingTheory/Flat/Localization.lean +++ b/MathlibStaging/RingTheory/Flat/Localization.lean @@ -28,24 +28,14 @@ theorem Module.Flat.localizedModule_base {R S : Type*} [CommRing R] [CommRing S] have : Module.Flat R (Localization q ⊗[S] M) := Module.Flat.tensor_tower (Localization q) M exact Module.Flat.of_linearEquiv e -/-- **Local–global flatness over a base, indexed by primes of `S`.** For an `R`-algebra `S` and an -`S`-module `M`, `M` is flat over `R` iff its localization at every prime of `S` is flat over `R`. -/ -theorem Module.flat_iff_forall_localizedModule_prime_of_algebra {R S : Type*} [CommRing R] +/-- **Local–global flatness over a base, indexed by maximal ideals of `S`.** For an `R`-algebra `S` +and an `S`-module `M`, `M` is flat over `R` iff its localization at every maximal ideal of `S` is +flat over `R`. -/ +theorem Module.flat_iff_forall_localizedModule_maximal_of_algebra {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] (M : Type*) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Module.Flat R M ↔ - ∀ (q : Ideal S) [q.IsPrime], Module.Flat R (LocalizedModule q.primeCompl M) := by + ∀ (q : Ideal S) [q.IsMaximal], Module.Flat R (LocalizedModule q.primeCompl M) := by refine ⟨fun _ q _ ↦ Module.Flat.localizedModule_base M q.primeCompl, fun h ↦ ?_⟩ - refine Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M) - (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P hP ↦ ?_ - have := hP.isPrime - exact h P - -/-- A module `N` over a commutative ring `R` is flat if and only if its localization at every -prime ideal is flat over `R`. This is the special case of -`Module.flat_iff_forall_localizedModule_prime_of_algebra` for `S := R`. -/ -theorem Module.flat_iff_forall_localizedModule_prime (R : Type*) [CommRing R] (N : Type*) - [AddCommGroup N] [Module R N] : - Module.Flat R N ↔ - ∀ (p : Ideal R) [p.IsPrime], Module.Flat R (LocalizedModule p.primeCompl N) := - Module.flat_iff_forall_localizedModule_prime_of_algebra (S := R) N + exact Module.flat_of_isLocalized_maximal S M (fun P _ ↦ LocalizedModule P.primeCompl M) + (fun P _ ↦ LocalizedModule.mkLinearMap P.primeCompl M) fun P _ ↦ h P diff --git a/MathlibStaging/RingTheory/RingHom/Flat.lean b/MathlibStaging/RingTheory/RingHom/Flat.lean index a332e7a..92d3177 100644 --- a/MathlibStaging/RingTheory/RingHom/Flat.lean +++ b/MathlibStaging/RingTheory/RingHom/Flat.lean @@ -24,14 +24,29 @@ theorem Module.Flat.trans_compHom {R S : Type*} [CommRing R] [CommRing S] (φ : have : Module.Flat R S := hφ exact Module.Flat.trans R S M +/-- If the algebra map `R → S` is bijective, then an `S`-module `M` is flat over `R` (via the tower) +iff it is flat over `S`. -/ +theorem Module.Flat.iff_of_bijective_algebraMap {R S : Type*} [CommRing R] [CommRing S] + [Algebra R S] (hb : Function.Bijective (algebraMap R S)) (M : Type*) [AddCommGroup M] + [Module R M] [Module S M] [IsScalarTower R S M] : + Module.Flat R M ↔ Module.Flat S M := by + let e : R ≃+* S := RingEquiv.ofBijective (algebraMap R S) hb + refine ⟨fun hM ↦ ?_, fun hM ↦ ?_⟩ + · letI : Algebra S R := e.symm.toRingHom.toAlgebra + haveI : IsScalarTower S R M := IsScalarTower.of_algebraMap_smul fun s x ↦ by + have h : (algebraMap R S) (e.symm s) = s := e.apply_symm_apply s + rw [show algebraMap S R s = e.symm s from rfl, ← algebraMap_smul (A := S) (e.symm s) x, h] + haveI : Module.Flat S R := RingHom.Flat.of_bijective (f := e.symm.toRingHom) e.symm.bijective + exact Module.Flat.trans S R M + · haveI : Module.Flat R S := + Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hb).symm + exact Module.Flat.trans R S M + /-- Restricting scalars along a bijective ring homomorphism preserves and reflects flatness. -/ theorem Module.Flat.compHom_bijective_iff {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) (hφ : Function.Bijective φ) {M : Type*} [AddCommGroup M] [Module S M] : (letI := Module.compHom M φ; Module.Flat R M) ↔ Module.Flat S M := by - refine ⟨fun hM ↦ ?_, fun hM ↦ Module.Flat.trans_compHom φ (.of_bijective hφ) hM⟩ + letI := φ.toAlgebra letI := Module.compHom M φ - let e : R ≃+* S := RingEquiv.ofBijective φ hφ - have key := Module.Flat.trans_compHom e.symm.toRingHom (.of_bijective e.symm.bijective) hM - have h : (inferInstanceAs (Module S M)) = Module.compHom M e.symm.toRingHom := - Module.ext' _ _ fun s m ↦ (congrArg (· • m) (e.apply_symm_apply s)).symm - rwa [← h] at key + haveI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl + exact Module.Flat.iff_of_bijective_algebraMap hφ M From 6be73ce0271c813d82d540bb0c9db05f5779fe8d Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 6 Jul 2026 17:17:24 +0100 Subject: [PATCH 4/5] Define FlatAt via a ModuleCat.flat object property 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 --- MathlibStaging.lean | 1 + .../Algebra/Category/ModuleCat/Flat.lean | 77 +++++++++++++ .../AlgebraicGeometry/Modules/Flat.lean | 104 ++++++++---------- 3 files changed, 125 insertions(+), 57 deletions(-) create mode 100644 MathlibStaging/Algebra/Category/ModuleCat/Flat.lean diff --git a/MathlibStaging.lean b/MathlibStaging.lean index 9197a97..14d8432 100644 --- a/MathlibStaging.lean +++ b/MathlibStaging.lean @@ -1,3 +1,4 @@ +import MathlibStaging.Algebra.Category.ModuleCat.Flat import MathlibStaging.Algebra.Category.ModuleCat.Presheaf import MathlibStaging.Algebra.Category.ModuleCat.Presheaf.Submodule import MathlibStaging.Algebra.Module.RingHom diff --git a/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean b/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean new file mode 100644 index 0000000..c1d6056 --- /dev/null +++ b/MathlibStaging/Algebra/Category/ModuleCat/Flat.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms +public import Mathlib.RingTheory.RingHom.Flat +public import MathlibStaging.RingTheory.RingHom.Flat +public import MathlibStaging.Init + +/-! +# Flat modules, as a property of objects of `ModuleCat R` + +We define `ModuleCat.flat R : ObjectProperty (ModuleCat R)`, the property of objects of +`ModuleCat R` given by `Module.Flat`, show that it is closed under isomorphisms and record its +interaction with restriction of scalars (`ModuleCat.restrictScalars`): + +* `ModuleCat.flat_restrictScalars`: restriction of scalars along a flat ring homomorphism + preserves flatness. +* `ModuleCat.flat_restrictScalars_iff_of_bijective`: restriction of scalars along a bijective + ring homomorphism preserves and reflects flatness. +* `ModuleCat.flat_restrictScalars_comp_iff`: restricting scalars along a composition agrees with + successively restricting scalars. +-/ + +@[expose] public section + +open CategoryTheory + +universe v u + +namespace ModuleCat + +variable (R : Type u) [CommRing R] + +/-- Flat modules, as a property of objects of `ModuleCat R`. -/ +def flat : ObjectProperty (ModuleCat.{v} R) := + fun M ↦ Module.Flat R M + +variable {R} + +@[simp] +lemma flat_iff (M : ModuleCat.{v} R) : flat R M ↔ Module.Flat R M := + Iff.rfl + +instance : (flat R).IsClosedUnderIsomorphisms where + of_iso e hM := (Module.Flat.equiv_iff e.toLinearEquiv).mp hM + +section RestrictScalars + +variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] + +/-- Restriction of scalars along a flat ring homomorphism preserves flatness. -/ +lemma flat_restrictScalars {φ : R →+* S} (hφ : φ.Flat) {M : ModuleCat.{v} S} (hM : flat S M) : + flat R ((restrictScalars φ).obj M) := + Module.Flat.trans_compHom φ hφ hM + +/-- Restriction of scalars along a bijective ring homomorphism preserves and reflects +flatness. -/ +lemma flat_restrictScalars_iff_of_bijective {φ : R →+* S} (hφ : Function.Bijective φ) + (M : ModuleCat.{v} S) : + flat R ((restrictScalars φ).obj M) ↔ flat S M := + Module.Flat.compHom_bijective_iff φ hφ + +/-- Restricting scalars along a composition of ring homomorphisms is flat if and only if +successively restricting scalars is. -/ +lemma flat_restrictScalars_comp_iff (f : R →+* S) (g : S →+* T) (M : ModuleCat.{v} T) : + flat R ((restrictScalars (g.comp f)).obj M) ↔ + flat R ((restrictScalars f).obj ((restrictScalars g).obj M)) := + ObjectProperty.prop_iff_of_iso _ (restrictScalarsComp'App f g (g.comp f) rfl M) + +end RestrictScalars + +end ModuleCat diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean index d9b90f1..ccfda51 100644 --- a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean +++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean @@ -7,9 +7,9 @@ module public import Mathlib.AlgebraicGeometry.Modules.Tilde public import Mathlib.AlgebraicGeometry.Morphisms.Flat +public import MathlibStaging.Algebra.Category.ModuleCat.Flat public import MathlibStaging.Algebra.Module.RingHom public import MathlibStaging.RingTheory.Flat.Localization -public import MathlibStaging.RingTheory.RingHom.Flat public import MathlibStaging.Init /-! @@ -24,7 +24,10 @@ local ring `𝒪_{S, f(x)}`, where `𝒪_{S, f(x)}` acts on `F_x` through the lo * `AlgebraicGeometry.Scheme.Modules.stalkModule`: the canonical module structure of the local ring `𝒪_{X, x}` on the stalk `F_x` of an `𝒪_X`-module `F`. -* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise flatness condition at a point. +* `AlgebraicGeometry.Scheme.Modules.stalk`: the stalk `F_x`, bundled as an object of the category + of modules over the local ring `𝒪_{X, x}`. +* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise flatness condition at a point, + phrased via `ModuleCat.flat` and restriction of scalars along the stalk map. * `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting flatness, defined as `∀ x, FlatAt f F x`. @@ -65,14 +68,17 @@ abbrev stalkModule {X : Scheme.{u}} (F : X.Modules) (x : X) : PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier (R := X.presheaf) F.val x +/-- The stalk `F_x` of an `𝒪_X`-module `F` at a point `x ∈ X`, bundled as an object of the +category of modules over the local ring `𝒪_{X, x}`, with the module structure `stalkModule`. -/ +def stalk {X : Scheme.{u}} (F : X.Modules) (x : X) : ModuleCat (X.presheaf.stalk x) := + @ModuleCat.of _ _ (F.presheaf.stalk x) _ (stalkModule F x) + /-- 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 := - letI := stalkModule F x - letI : Module (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x) := - Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom - Module.Flat (S.presheaf.stalk (f.base x)) (F.presheaf.stalk x) + ModuleCat.flat (S.presheaf.stalk (f.base x)) + ((ModuleCat.restrictScalars (f.stalkMap x).hom).obj (F.stalk x)) /-- A sheaf of modules `F` on a scheme `X` is *flat* over `S` via a morphism `f : X ⟶ S` if for every point `x ∈ X`, the stalk `F_x` is flat over the local ring `𝒪_{S, f(x)}` (acting by @@ -139,12 +145,9 @@ theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Module [hf : Flat f F] [AlgebraicGeometry.Flat g] : Flat (f ≫ g) F := by refine ⟨fun x ↦ ?_⟩ simp only [FlatAt] - letI := stalkModule F x - letI : Module (Y.presheaf.stalk (f.base x)) (F.presheaf.stalk x) := - Module.compHom (F.presheaf.stalk x) (f.stalkMap x).hom - rw [congrArg (Module.compHom (F.presheaf.stalk x)) (stalkMap_comp_hom f g x)] - exact Module.Flat.trans_compHom (g.stalkMap (f.base x)).hom - (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x) + rw [stalkMap_comp_hom f g x] + exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).mpr + (ModuleCat.flat_restrictScalars (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x)) /-- **Flatness is local on the base.** If `j : V ⟶ S` is an open immersion and `g : X ⟶ V`, then `F` is flat over `S` via `g ≫ j` if and only if it is flat over `V` via `g`. In other words, @@ -152,22 +155,13 @@ flatness over the base only depends on the base through an open neighbourhood of theorem flat_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S) [IsOpenImmersion j] (F : X.Modules) : Flat (g ≫ j) F ↔ Flat g F := by - have hbij : ∀ x : X, Function.Bijective (j.stalkMap (g.base x)).hom := fun x ↦ - (ConcreteCategory.isIso_iff_bijective (j.stalkMap (g.base x))).mp inferInstance - refine ⟨fun h ↦ ⟨fun x ↦ ?_⟩, fun h ↦ ⟨fun x ↦ ?_⟩⟩ - all_goals - simp only [FlatAt] - letI := stalkModule F x - letI : Module (V.presheaf.stalk (g.base x)) (F.presheaf.stalk x) := - Module.compHom (F.presheaf.stalk x) (g.stalkMap x).hom - have hcompHom := congrArg (Module.compHom (F.presheaf.stalk x)) (stalkMap_comp_hom g j x) - · have hx := h.flatAt x - simp only [FlatAt] at hx - rw [hcompHom] at hx - exact (Module.Flat.compHom_bijective_iff (j.stalkMap (g.base x)).hom (hbij x)).1 hx - · rw [hcompHom] - exact Module.Flat.trans_compHom (j.stalkMap (g.base x)).hom - (RingHom.Flat.of_bijective (hbij x)) (h.flatAt x) + simp only [flat_iff_forall_flatAt] + refine forall_congr' fun x ↦ ?_ + simp only [FlatAt] + rw [stalkMap_comp_hom g j x] + exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans + (ModuleCat.flat_restrictScalars_iff_of_bijective + ((ConcreteCategory.isIso_iff_bijective (j.stalkMap (g.base x))).mp inferInstance) _) /-! ### The affine criterion for an `R`-algebra `S` and an `S`-module `M` @@ -203,12 +197,12 @@ theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Modu ((tilde M).presheaf.stalk x) := by refine IsScalarTower.of_algebraMap_smul fun r n ↦ ?_ rw [Module.compHom_smul, hsquare r, Module.compHom_smul, algebraMap_smul] - simp only [FlatAt] - rw [Module.flat_iff_of_isLocalization ((Spec R).presheaf.stalk ((Spec.map f).base x)) - ((Spec.map f).base x).asIdeal.primeCompl ((tilde M).presheaf.stalk x)] - exact Module.Flat.equiv_iff - ((IsLocalizedModule.linearEquiv x.asIdeal.primeCompl (tilde.toStalk M x).hom - (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)).restrictScalars R) + exact Iff.trans + (Module.flat_iff_of_isLocalization ((Spec R).presheaf.stalk ((Spec.map f).base x)) + ((Spec.map f).base x).asIdeal.primeCompl ((tilde M).presheaf.stalk x)) + (Module.Flat.equiv_iff + ((IsLocalizedModule.linearEquiv x.asIdeal.primeCompl (tilde.toStalk M x).hom + (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)).restrictScalars R)) /-- **The affine case for an `R`-algebra `S`.** For a ring map `f : R ⟶ S` (an `R`-algebra `S`) and an `S`-module `M` (hence also an `R`-module, by restriction of scalars), the sheaf `M^~` on `Spec S` @@ -317,6 +311,19 @@ theorem restrictStalkNatIso_hom_smul {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenIm exact congrArg (· • F.presheaf.map (ι.opensFunctor.map (homOfLE (inf_le_left : W ⊓ ι ⁻¹ᵁ V ≤ W))).op s) F2 +/-- For an open immersion `ι : U ⟶ X` and a point `u ∈ U`, the stalk of the restriction `F|_U` +at `u`, with scalars restricted along the (iso) stalk map `ι.stalkMap u`, is isomorphic in +`ModuleCat 𝒪_{X, ι u}` to the stalk of `F` at `ι u`. -/ +def restrictStalkModuleIso {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] + (F : X.Modules) (u : U) : + (ModuleCat.restrictScalars (ι.stalkMap u).hom).obj ((F.restrict ι).stalk u) ≅ + F.stalk (ι.base u) := + (AddEquiv.toLinearEquiv + (M := (ModuleCat.restrictScalars (ι.stalkMap u).hom).obj ((F.restrict ι).stalk u)) + (M₂ := F.stalk (ι.base u)) + ((Scheme.Modules.restrictStalkNatIso ι u).app F).addCommGroupIsoToAddEquiv + (fun c m ↦ restrictStalkNatIso_hom_smul ι F u c m)).toModuleIso + /-- **Pointwise comparison under restriction to an open subscheme.** For an open immersion `ι : U ⟶ X`, the flatness of the restricted module `F|_U` at `u` (over `S`, via `ι ≫ f`) is equivalent to the flatness of `F` at `ι(u)`. This holds because the stalk map of an open immersion @@ -324,29 +331,12 @@ is an isomorphism, so restriction does not change the stalk data. -/ theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] (f : X ⟶ S) (F : X.Modules) (u : U) : FlatAt (ι ≫ f) (F.restrict ι) u ↔ FlatAt f F (ι.base u) := by - letI := stalkModule (F.restrict ι) u - letI := stalkModule F (ι.base u) - let Φe : (F.restrict ι).presheaf.stalk u ≃+ F.presheaf.stalk (ι.base u) := - ((Scheme.Modules.restrictStalkNatIso ι u).app F).addCommGroupIsoToAddEquiv - -- The two stalk-map base points `(ι ≫ f) u` and `f (ι u)` only agree up to - -- `Scheme.Hom.comp_base`; we phrase the module structures over the former (matching the - -- left-hand `FlatAt` syntactically), letting `f.stalkMap (ι.base u)` act through the latter. - letI : Module (S.presheaf.stalk ((ι ≫ f).base u)) ((F.restrict ι).presheaf.stalk u) := - Module.compHom ((F.restrict ι).presheaf.stalk u) ((ι ≫ f).stalkMap u).hom - letI : Module (S.presheaf.stalk ((ι ≫ f).base u)) (F.presheaf.stalk (ι.base u)) := - Module.compHom (F.presheaf.stalk (ι.base u)) (f.stalkMap (ι.base u)).hom - let e : (F.restrict ι).presheaf.stalk u ≃ₗ[S.presheaf.stalk ((ι ≫ f).base u)] - F.presheaf.stalk (ι.base u) := - Φe.toLinearEquiv (by - intro b m - have hb : ((ι ≫ f).stalkMap u).hom b - = (ι.stalkMap u).hom ((f.stalkMap (ι.base u)).hom b) := by - rw [stalkMap_comp_hom ι f u] - rfl - have key := restrictStalkNatIso_hom_smul ι F u ((f.stalkMap (ι.base u)).hom b) m - rw [← hb] at key - exact key) - exact Module.Flat.equiv_iff e + simp only [FlatAt] + rw [stalkMap_comp_hom ι f u] + exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans + (ObjectProperty.prop_iff_of_iso _ + ((ModuleCat.restrictScalars (f.stalkMap (ι.base u)).hom).mapIso + (restrictStalkModuleIso ι F u))) /-- Flatness of the restriction of `F` to an open subscheme `U` (via `ι ≫ f`) is equivalent to the pointwise flatness of `F` at every point of `U`. -/ From 17070a4fe3676b8208dded19e705641215cc30a8 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 6 Jul 2026 19:05:09 +0000 Subject: [PATCH 5/5] refactor(AlgebraicGeometry/Modules): make sheaf flatness absolute MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../AlgebraicGeometry/Modules/Flat.lean | 165 ++++++++++++------ 1 file changed, 109 insertions(+), 56 deletions(-) diff --git a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean index ccfda51..f015419 100644 --- a/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean +++ b/MathlibStaging/AlgebraicGeometry/Modules/Flat.lean @@ -15,10 +15,16 @@ public import MathlibStaging.Init /-! # Flat sheaves of modules -Given a morphism of schemes `f : X ⟶ S` and an `𝒪_X`-module `F`, we say that `F` is -*flat* over `S` (via `f`) if for every point `x ∈ X`, the stalk `F_x` is a flat module over the -local ring `𝒪_{S, f(x)}`, where `𝒪_{S, f(x)}` acts on `F_x` through the local ring homomorphism -`f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}` induced by `f`. +We say that an `𝒪_X`-module `F` is *flat* if for every point `x ∈ X`, the stalk `F_x` is a flat +module over the local ring `𝒪_{X, x}`. This is the *absolute* notion, over the structure sheaf of +`X` itself. + +More generally, given a morphism of schemes `f : X ⟶ S`, we say that `F` is *flat over `S`* (via +`f`) if for every point `x ∈ X`, the stalk `F_x` is a flat module over the local ring `𝒪_{S, f(x)}`, +where `𝒪_{S, f(x)}` acts on `F_x` through the local ring homomorphism +`f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}` induced by `f`. Conceptually this is the absolute flatness +of the restriction of scalars of `F` to the inverse-image structure sheaf `f⁻¹𝒪_S`; the absolute +notion is the special case `f = 𝟙 X` (`flatOver_id_iff`). ## Main definitions @@ -26,23 +32,29 @@ local ring `𝒪_{S, f(x)}`, where `𝒪_{S, f(x)}` acts on `F_x` through the lo ring `𝒪_{X, x}` on the stalk `F_x` of an `𝒪_X`-module `F`. * `AlgebraicGeometry.Scheme.Modules.stalk`: the stalk `F_x`, bundled as an object of the category of modules over the local ring `𝒪_{X, x}`. -* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise flatness condition at a point, - phrased via `ModuleCat.flat` and restriction of scalars along the stalk map. -* `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting flatness, defined as - `∀ x, FlatAt f F x`. +* `AlgebraicGeometry.Scheme.Modules.FlatAt`: the pointwise (absolute) flatness condition at a point, + `F_x` is flat over `𝒪_{X, x}`. +* `AlgebraicGeometry.Scheme.Modules.Flat`: the class asserting (absolute) flatness, defined as + `∀ x, FlatAt F x`. +* `AlgebraicGeometry.Scheme.Modules.FlatAtOver`/`FlatOver`: the relative pointwise condition and + class, flatness of `F` over a base `S` via `f : X ⟶ S`, phrased via `ModuleCat.flat` and + restriction of scalars along the stalk map. ## Main results -* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff`: for a commutative ring `R` and an `R`-module - `M`, the sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if - `M` is a flat `R`-module. -* `AlgebraicGeometry.Scheme.Modules.flat_tilde_iff_of_algebra`: the same criterion for a ring map - `f : R ⟶ S` and an `S`-module `M`: the sheaf `M^~` on `Spec S` is flat over `Spec R` +* `AlgebraicGeometry.Scheme.Modules.flatOver_id_iff`: `F` is flat over the base via the identity + morphism `𝟙 X` iff it is (absolutely) flat. +* `AlgebraicGeometry.Scheme.Modules.flatOver_tilde_iff`: for a commutative ring `R` and an + `R`-module `M`, the sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if + and only if `M` is a flat `R`-module. +* `AlgebraicGeometry.Scheme.Modules.flatOver_tilde_iff_of_algebra`: the same criterion for a ring + map `f : R ⟶ S` and an `S`-module `M`: the sheaf `M^~` on `Spec S` is flat over `Spec R` (via `Spec.map f`) if and only if `M` is flat as an `R`-module. -* `AlgebraicGeometry.Scheme.Modules.Flat.comp`: flatness is preserved under composition with a +* `AlgebraicGeometry.Scheme.Modules.FlatOver.comp`: flatness is preserved under composition with a flat morphism of the base. -* `AlgebraicGeometry.Scheme.Modules.flat_comp_isOpenImmersion_iff`: flatness is local on the base. -* `AlgebraicGeometry.Scheme.Modules.flat_iff_forall_openCover`: flatness is local on the source. +* `AlgebraicGeometry.Scheme.Modules.flatOver_comp_isOpenImmersion_iff`: flatness is local on the + base. +* `AlgebraicGeometry.Scheme.Modules.flatOver_iff_forall_openCover`: flatness is local on the source. -/ @[expose] public noncomputable section @@ -74,24 +86,65 @@ def stalk {X : Scheme.{u}} (F : X.Modules) (x : X) : ModuleCat (X.presheaf.stalk @ModuleCat.of _ _ (F.presheaf.stalk x) _ (stalkModule F x) /-- 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 := +local ring `𝒪_{X, x}`. -/ +def FlatAt {X : Scheme.{u}} (F : X.Modules) (x : X) : Prop := + ModuleCat.flat (X.presheaf.stalk x) (F.stalk x) + +/-- A sheaf of modules `F` on a scheme `X` is *flat* if for every point `x ∈ X`, the stalk `F_x` +is flat over the local ring `𝒪_{X, x}`, i.e. if `FlatAt F x` holds at every point. -/ +class Flat {X : Scheme.{u}} (F : X.Modules) : Prop where + flatAt : ∀ x : X, FlatAt F x + +/-- `Flat F` holds iff the pointwise condition `FlatAt F x` holds for all `x`. -/ +theorem flat_iff_forall_flatAt {X : Scheme.{u}} (F : X.Modules) : + Flat F ↔ ∀ x : X, FlatAt F x := + ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩ + +/-! ### Relative flatness over a base + +`Flat` above is *absolute*: it is flatness of `F` over its own structure sheaf `𝒪_X`. To talk about +flatness of `F` over a base `S` via a morphism `f : X ⟶ S`, we restrict scalars of each stalk `F_x` +along the stalk map `f.stalkMap x : 𝒪_{S, f(x)} ⟶ 𝒪_{X, x}`. + +Conceptually this is the absolute flatness (`Flat`) of the restriction of scalars of `F` to the +inverse-image structure sheaf `f⁻¹𝒪_S` (whose stalk at `x` is `𝒪_{S, f(x)}`). We phrase it +stalk-wise directly, as Mathlib does not yet provide the inverse-image sheaf of rings and its stalk +identification. -/ + +/-- The pointwise flatness condition of `F` over a base `S` (via `f : X ⟶ S`) 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 FlatAtOver {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)) -/-- A sheaf of modules `F` on a scheme `X` is *flat* over `S` via a morphism `f : X ⟶ S` if for +/-- A sheaf of modules `F` on a scheme `X` is *flat over `S`* via a morphism `f : X ⟶ S` if for every point `x ∈ X`, the stalk `F_x` is flat over the local ring `𝒪_{S, f(x)}` (acting by -restriction of scalars along the stalk map `f.stalkMap x`), i.e. if `FlatAt f F x` holds at every -point. -/ -class Flat {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : Prop where - flatAt : ∀ x : X, FlatAt f F x - -/-- `Flat f F` holds iff the pointwise condition `FlatAt f F x` holds for all `x`. -/ -theorem flat_iff_forall_flatAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : - Flat f F ↔ ∀ x : X, FlatAt f F x := +restriction of scalars along the stalk map `f.stalkMap x`), i.e. if `FlatAtOver f F x` holds at +every point. -/ +class FlatOver {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : Prop where + flatAt : ∀ x : X, FlatAtOver f F x + +/-- `FlatOver f F` holds iff the pointwise condition `FlatAtOver f F x` holds for all `x`. -/ +theorem flatOver_iff_forall_flatAtOver {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) : + FlatOver f F ↔ ∀ x : X, FlatAtOver f F x := ⟨fun h ↦ h.flatAt, fun h ↦ ⟨h⟩⟩ +/-- Flatness of `F` over its own structure sheaf, `Flat F`, is the special case of relative +flatness `FlatOver f F` for the identity morphism `f = 𝟙 X`. Under the identity stalk map the +restriction of scalars is the identity, so the two pointwise conditions agree. -/ +theorem flatAtOver_id {X : Scheme.{u}} (F : X.Modules) (x : X) : + FlatAtOver (𝟙 X) F x ↔ FlatAt F x := by + have hf : ((𝟙 X : X ⟶ X).stalkMap x).hom = RingHom.id (X.presheaf.stalk x) := by + rw [Scheme.Hom.stalkMap_id]; exact CommRingCat.hom_id + exact ObjectProperty.prop_iff_of_iso _ (ModuleCat.restrictScalarsId'App _ hf (F.stalk x)) + +/-- `F` is flat over the base via the identity morphism `𝟙 X` iff it is (absolutely) flat. -/ +theorem flatOver_id_iff {X : Scheme.{u}} (F : X.Modules) : + FlatOver (𝟙 X) F ↔ Flat F := by + rw [flatOver_iff_forall_flatAtOver, flat_iff_forall_flatAt] + exact forall_congr' fun x ↦ flatAtOver_id F x + end Scheme.Modules namespace Tilde @@ -141,10 +194,10 @@ lemma stalkMap_comp_hom {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) /-- **Transitivity along a flat base.** If a sheaf of modules `F` on `X` is flat over `Y` via `f : X ⟶ Y`, and `g : Y ⟶ Z` is a flat morphism of schemes, then `F` is flat over `Z` via the composite `f ≫ g`. -/ -theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Modules) - [hf : Flat f F] [AlgebraicGeometry.Flat g] : Flat (f ≫ g) F := by +theorem FlatOver.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Modules) + [hf : FlatOver f F] [AlgebraicGeometry.Flat g] : FlatOver (f ≫ g) F := by refine ⟨fun x ↦ ?_⟩ - simp only [FlatAt] + simp only [FlatAtOver] rw [stalkMap_comp_hom f g x] exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).mpr (ModuleCat.flat_restrictScalars (AlgebraicGeometry.Flat.stalkMap g (f.base x)) (hf.flatAt x)) @@ -152,12 +205,12 @@ theorem Flat.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (F : X.Module /-- **Flatness is local on the base.** If `j : V ⟶ S` is an open immersion and `g : X ⟶ V`, then `F` is flat over `S` via `g ≫ j` if and only if it is flat over `V` via `g`. In other words, flatness over the base only depends on the base through an open neighbourhood of the image. -/ -theorem flat_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S) +theorem flatOver_comp_isOpenImmersion_iff {X V S : Scheme.{u}} (g : X ⟶ V) (j : V ⟶ S) [IsOpenImmersion j] (F : X.Modules) : - Flat (g ≫ j) F ↔ Flat g F := by - simp only [flat_iff_forall_flatAt] + FlatOver (g ≫ j) F ↔ FlatOver g F := by + simp only [flatOver_iff_forall_flatAtOver] refine forall_congr' fun x ↦ ?_ - simp only [FlatAt] + simp only [FlatAtOver] rw [stalkMap_comp_hom g j x] exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans (ModuleCat.flat_restrictScalars_iff_of_bijective @@ -173,12 +226,12 @@ an `R`-module. -/ /-- The pointwise flatness condition for `M^~` (with `M` an `S`-module, for a ring map `f : R ⟶ S`) over `Spec R` at a prime `x` of `S` is equivalent to the localization `M_x` being flat over `R` (with `R` acting on `M` by restriction of scalars along `f`). -/ -theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) +theorem flatAtOver_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) (x : PrimeSpectrum S) : letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom letI : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl - FlatAt (Spec.map f) (tilde M) x ↔ + FlatAtOver (Spec.map f) (tilde M) x ↔ Module.Flat R (LocalizedModule x.asIdeal.primeCompl M) := by letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom @@ -207,28 +260,28 @@ theorem flatAt_tilde_algebra_iff {R S : CommRingCat.{u}} (f : R ⟶ S) (M : Modu /-- **The affine case for an `R`-algebra `S`.** For a ring map `f : R ⟶ S` (an `R`-algebra `S`) and an `S`-module `M` (hence also an `R`-module, by restriction of scalars), the sheaf `M^~` on `Spec S` is flat over `Spec R` (via `Spec.map f`) if and only if `M` is a flat `R`-module. -/ -theorem flat_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) : +theorem flatOver_tilde_iff_of_algebra {R S : CommRingCat.{u}} (f : R ⟶ S) (M : ModuleCat.{u} S) : letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom - Flat (Spec.map f) (tilde M) ↔ Module.Flat R M := by + FlatOver (Spec.map f) (tilde M) ↔ Module.Flat R M := by letI := f.hom.toAlgebra letI : Module R M := Module.compHom M f.hom have : IsScalarTower R S M := IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl - rw [flat_iff_forall_flatAt] + rw [flatOver_iff_forall_flatAtOver] refine ⟨fun h ↦ (Module.flat_iff_forall_localizedModule_maximal_of_algebra (R := R) (S := S) - (M := M)).mpr fun q _ ↦ (flatAt_tilde_algebra_iff f M ⟨q, inferInstance⟩).mp + (M := M)).mpr fun q _ ↦ (flatAtOver_tilde_algebra_iff f M ⟨q, inferInstance⟩).mp (h ⟨q, inferInstance⟩), - fun hM x ↦ (flatAt_tilde_algebra_iff f M x).mpr + fun hM x ↦ (flatAtOver_tilde_algebra_iff f M x).mpr (Module.Flat.localizedModule_base M x.asIdeal.primeCompl)⟩ /-- **The affine case.** For a commutative ring `R` and an `R`-module `M`, the quasi-coherent sheaf `M^~` on `Spec R` is flat over `Spec R` (via the identity morphism) if and only if `M` is a -flat `R`-module. This is the special case of `flat_tilde_iff_of_algebra` for the identity ring +flat `R`-module. This is the special case of `flatOver_tilde_iff_of_algebra` for the identity ring map `𝟙 R`. -/ -theorem flat_tilde_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) : - Flat (𝟙 (Spec R)) (tilde M) ↔ Module.Flat R M := by +theorem flatOver_tilde_iff {R : CommRingCat.{u}} (M : ModuleCat.{u} R) : + FlatOver (𝟙 (Spec R)) (tilde M) ↔ Module.Flat R M := by rw [← Spec.map_id R] - exact flat_tilde_iff_of_algebra (𝟙 R) M + exact flatOver_tilde_iff_of_algebra (𝟙 R) M /-! ### Flatness is local on the source (open covers) @@ -328,10 +381,10 @@ def restrictStalkModuleIso {U X : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι `ι : U ⟶ X`, the flatness of the restricted module `F|_U` at `u` (over `S`, via `ι ≫ f`) is equivalent to the flatness of `F` at `ι(u)`. This holds because the stalk map of an open immersion is an isomorphism, so restriction does not change the stalk data. -/ -theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] +theorem flatAtOver_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] (f : X ⟶ S) (F : X.Modules) (u : U) : - FlatAt (ι ≫ f) (F.restrict ι) u ↔ FlatAt f F (ι.base u) := by - simp only [FlatAt] + FlatAtOver (ι ≫ f) (F.restrict ι) u ↔ FlatAtOver f F (ι.base u) := by + simp only [FlatAtOver] rw [stalkMap_comp_hom ι f u] exact (ModuleCat.flat_restrictScalars_comp_iff _ _ _).trans (ObjectProperty.prop_iff_of_iso _ @@ -340,19 +393,19 @@ theorem flatAt_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion /-- Flatness of the restriction of `F` to an open subscheme `U` (via `ι ≫ f`) is equivalent to the pointwise flatness of `F` at every point of `U`. -/ -theorem flat_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] +theorem flatOver_restrict_iff {U X S : Scheme.{u}} (ι : U ⟶ X) [IsOpenImmersion ι] (f : X ⟶ S) (F : X.Modules) : - Flat (ι ≫ f) (F.restrict ι) ↔ ∀ u : U, FlatAt f F (ι.base u) := by - rw [flat_iff_forall_flatAt] - exact forall_congr' fun u ↦ flatAt_restrict_iff ι f F u + FlatOver (ι ≫ f) (F.restrict ι) ↔ ∀ u : U, FlatAtOver f F (ι.base u) := by + rw [flatOver_iff_forall_flatAtOver] + exact forall_congr' fun u ↦ flatAtOver_restrict_iff ι f F u /-- **Flatness is local on the source.** For an open cover `𝒰` of `X`, the module `F` is flat over `S` (via `f`) if and only if for every member `Uᵢ` of the cover, the restriction `F|_{Uᵢ}` is flat over `S` (via `𝒰.f i ≫ f`). -/ -theorem flat_iff_forall_openCover {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) +theorem flatOver_iff_forall_openCover {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (𝒰 : X.OpenCover) : - Flat f F ↔ ∀ i, Flat (𝒰.f i ≫ f) (F.restrict (𝒰.f i)) := by - simp_rw [flat_restrict_iff, flat_iff_forall_flatAt] + FlatOver f F ↔ ∀ i, FlatOver (𝒰.f i ≫ f) (F.restrict (𝒰.f i)) := by + simp_rw [flatOver_restrict_iff, flatOver_iff_forall_flatAtOver] refine ⟨fun h i u ↦ h _, fun h x ↦ ?_⟩ obtain ⟨u, hu⟩ := 𝒰.covers x rw [← hu]