38.2 Lemmas on étale… to 38.18 A criterion for purity

Section38.2 Lemmas on étale localization#

Section 38.2 of the Stacks Project, Tag 05FM. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 057R, a lemma

Tag 057R in the Stacks Project.

Stacks.Etale.exists_etale_lift_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/LiftAcrossClosedImmersion.lean, line 138.

Let Z → X be a closed immersion of affine schemes and let Z' → Z be an étale morphism with affine source. Then it is the pullback of an étale morphism X' → X with affine source.

theorem exists_etale_lift_of_isClosedImmersion
    {Z X Z' : AlgebraicGeometry.Scheme.{u}} (i : Z ⟶ X) (p : Z' ⟶ Z)
    [AlgebraicGeometry.IsAffine Z] [AlgebraicGeometry.IsAffine X]
    [AlgebraicGeometry.IsAffine Z'] [AlgebraicGeometry.IsClosedImmersion i]
    [AlgebraicGeometry.Etale p] :
    ∃ (X' : AlgebraicGeometry.Scheme.{u}) (f : X' ⟶ X),
      AlgebraicGeometry.IsAffine X' ∧ AlgebraicGeometry.Etale f ∧
        ∃ e : Z' ≅ pullback i f, e.hom ≫ pullback.fst i f = p
Tag 05H2, a lemma

Tag 05H2 in the Stacks Project.

AlgebraicGeometry.etale_stalkBaseChangeMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/EtaleBaseChange.lean, line 94.

Stacks Project, Tag 05H2. The morphism between the base changes to the spectrum of a local ring, induced by a commutative square with étale horizontal morphisms, is étale.

lemma etale_stalkBaseChangeMap (f' : X' ⟶ S') (g' : X' ⟶ X)
    (g : S' ⟶ S) (f : X ⟶ S) (h : g' ≫ f = f' ≫ g) (s' : S')
    [Etale g'] [Etale g] : Etale (stalkBaseChangeMap f' g' g f h s')
Tag 05B9, a lemma

Tag 05B9 in the Stacks Project.

AlgebraicGeometry.isFlatOverAt_comp_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/EtaleBase.lean, line 101. The attribute's comment: “pointwise statement”.

Flatness of a quasi-coherent module at a point is unchanged when the base is replaced by an étale intermediate scheme.

public theorem isFlatOverAt_comp_iff_of_etale [Etale g] (x : X) :
    AlgebraicGeometry.IsFlatOverAt (f ≫ g).toLRSHom.toShHom F x ↔
      AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F x

AlgebraicGeometry.isFlatOver_comp_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/EtaleBase.lean, line 149. The attribute's comment: “global statement”.

A quasi-coherent module is flat over the base if and only if it is flat over an étale intermediate scheme.

public theorem isFlatOver_comp_iff_of_etale [Etale g] :
    AlgebraicGeometry.IsFlatOver (f ≫ g).toLRSHom.toShHom F ↔
      AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F
Tag 05BA, a lemma

Tag 05BA in the Stacks Project.

AlgebraicGeometry.flat_stalk_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FlatMorphisms/EtaleStalk.lean, line 73.

Let f : T ⟶ S be étale, let t : T and let M be a module over 𝒪_{T,t}. Then M is flat over 𝒪_{S,f(t)}, acting through the map of local rings, if and only if it is flat over 𝒪_{T,t}.

theorem flat_stalk_iff_of_etale [Etale f] (t : T) (M : Type*) [AddCommGroup M]
    [Module (T.presheaf.stalk t) M] :
    letI : Module (S.presheaf.stalk (f t)) M := Module.compHom M (f.stalkMap t).hom
    Module.Flat (S.presheaf.stalk (f t)) M ↔ Module.Flat (T.presheaf.stalk t) M
Tag 05VL, a lemma

Tag 05VL in the Stacks Project.

flat_tfae_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/FlatHenselization.lean, line 133. The attribute's comment: “conditions (1)--(3)”. References: SGA 4 VIII (4.1), “more general”; SGA 4 VIII (4.4), “more general”; SGA 4 XVII (5.5.29), “Flatness clause”.

Stacks Project, Tag 05VL, conditions (1)--(3). A module over a henselization with extended residue field is flat over the original local ring if and only if it is flat over the henselization with unchanged residue field, if and only if it is flat over the extended-residue-field henselization. A strict henselization is the case where K is a separable closure of the residue field.

theorem flat_tfae_henselization {Msh : Type y} [AddCommGroup Msh] [Module Rsh Msh] :
    letI : Module Rh Msh := Module.compHom Msh (algebraMap Rh Rsh)
    letI : Module R Msh := Module.compHom Msh (algebraMap R Rsh)
    List.TFAE [Module.Flat R Msh, Module.Flat Rh Msh, Module.Flat Rsh Msh]

flat_tfae_baseChange_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/FlatHenselization.lean, line 152. The attribute's comment: “conditions (1)--(5)”.

Stacks Project, Tag 05VL, conditions (1)--(5). If the module over the extended-residue-field henselization is obtained from an Rh-module by extension of scalars, its three flatness conditions are also equivalent to flatness of the original module over R and over Rh.

theorem flat_tfae_baseChange_henselization {Mh : Type y} [AddCommGroup Mh] [Module Rh Mh] :
    letI : Module R Mh := Module.compHom Mh (algebraMap R Rh)
    letI : Module Rsh (Rsh ⊗[Rh] Mh) := TensorProduct.leftModule
    letI : Module Rh (Rsh ⊗[Rh] Mh) := Module.compHom (Rsh ⊗[Rh] Mh) (algebraMap Rh Rsh)
    letI : Module R (Rsh ⊗[Rh] Mh) := Module.compHom (Rsh ⊗[Rh] Mh) (algebraMap R Rsh)
    List.TFAE [Module.Flat R (Rsh ⊗[Rh] Mh), Module.Flat Rh (Rsh ⊗[Rh] Mh),
      Module.Flat Rsh (Rsh ⊗[Rh] Mh), Module.Flat R Mh, Module.Flat Rh Mh]

flat_tfae_iteratedBaseChange_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/FlatHenselization.lean, line 187. The attribute's comment: “conditions (1)--(6)”.

Stacks Project, Tag 05VL, conditions (1)--(6). If the Rh-module is in turn obtained from an R-module by extension of scalars, all five flatness conditions after base change are equivalent to flatness of the original module over R.

theorem flat_tfae_iteratedBaseChange_henselization {M : Type y} [AddCommGroup M] [Module R M] :
    letI : Module Rh (Rh ⊗[R] M) := TensorProduct.leftModule
    letI : Module R (Rh ⊗[R] M) := Module.compHom (Rh ⊗[R] M) (algebraMap R Rh)
    letI : Module Rsh (Rsh ⊗[Rh] (Rh ⊗[R] M)) := TensorProduct.leftModule
    letI : Module Rh (Rsh ⊗[Rh] (Rh ⊗[R] M)) :=
      Module.compHom (Rsh ⊗[Rh] (Rh ⊗[R] M)) (algebraMap Rh Rsh)
    letI : Module R (Rsh ⊗[Rh] (Rh ⊗[R] M)) :=
      Module.compHom (Rsh ⊗[Rh] (Rh ⊗[R] M)) (algebraMap R Rsh)
    List.TFAE [Module.Flat R (Rsh ⊗[Rh] (Rh ⊗[R] M)), Module.Flat Rh (Rsh ⊗[Rh] (Rh ⊗[R] M)),
      Module.Flat Rsh (Rsh ⊗[Rh] (Rh ⊗[R] M)), Module.Flat R (Rh ⊗[R] M),
      Module.Flat Rh (Rh ⊗[R] M), Module.Flat R M]
Tag 0DK0, a lemma

Tag 0DK0 in the Stacks Project.

torAmplitude_tfae_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/TorAmplitudeHenselization.lean, line 983. The attribute's comment: “conditions (1)--(3)”.

Stacks Project, Tag 0DK0, conditions (1)--(3). The tor amplitude of a complex over a henselization with extended residue field is the same whether it is measured over the original local ring, the henselization with unchanged residue field, or the extended-residue-field henselization.

public theorem torAmplitude_tfae_henselization
    (Msh : CochainComplex (ModuleCat.{max u uh ush w} Rsh) ℤ) (a b : ℤ) :
    List.TFAE
      [StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap R Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap Rh Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj Msh) a b]

torAmplitude_tfae_baseChange_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/TorAmplitudeHenselization.lean, line 1029. The attribute's comment: “conditions (1)--(5)”.

Stacks Project, Tag 0DK0, conditions (1)--(5). If the complex over the extended-residue-field henselization is obtained from a complex over Rh by base change, the preceding three conditions are also equivalent to tor amplitude of the original complex over R and over Rh.

public theorem torAmplitude_tfae_baseChange_henselization
    (Mh : CochainComplex (ModuleCat.{max u uh ush w} Rh) ℤ) (a b : ℤ) :
    let Msh := (CochainComplex.extendScalarsLarge.{max u w, uh, ush}
      (algebraMap Rh Rsh)).obj Mh
    List.TFAE
      [StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap R Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap Rh Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj Msh) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap R Rh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Mh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj Mh) a b]

torAmplitude_tfae_iteratedBaseChange_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/TorAmplitudeHenselization.lean, line 1095. The attribute's comment: “conditions (1)--(6)”.

Stacks Project, Tag 0DK0, conditions (1)--(6). If the complex over Rh is itself obtained by base change from R, all five conditions after base change are equivalent to tor amplitude of the original complex over R.

public theorem torAmplitude_tfae_iteratedBaseChange_henselization
    (M : CochainComplex (ModuleCat.{max u uh ush w} R) ℤ) (a b : ℤ) :
    let Mh := (CochainComplex.extendScalarsLarge.{max ush w, u, uh}
      (algebraMap R Rh)).obj M
    let Msh := (CochainComplex.extendScalarsLarge.{max u w, uh, ush}
      (algebraMap Rh Rsh)).obj Mh
    List.TFAE
      [StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap R Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap Rh Rsh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Msh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj Msh) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
        (DerivedCategory.Q.obj
          (((ModuleCat.restrictScalars (algebraMap R Rh)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj Mh)) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj Mh) a b,
       StacksDraft.TorAmplitude.HasTorAmplitudeCanonicalLift
         (DerivedCategory.Q.obj M) a b]
Tag 05FN, a lemma

Tag 05FN in the Stacks Project.

AlgebraicGeometry.isWeaklyAssociatedPoint_pullback_iff_of_finite_flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/FiniteFlatPullback.lean, line 276.

Stacks Project, Tag 05FN. A point is weakly associated to the pullback of a quasi-coherent module along a finite flat morphism if and only if its image is weakly associated to the original module.

lemma isWeaklyAssociatedPoint_pullback_iff_of_finite_flat
    {T S : Scheme.{u}} (g : T ⟶ S) [IsFinite g] [Flat g]
    (G : S.Modules) [G.IsQuasicoherent] (t : T) :
    Stacks.Divisors.IsWeaklyAssociatedPoint ((Scheme.Modules.pullback g).obj G) t ↔
      Stacks.Divisors.IsWeaklyAssociatedPoint G (g.base t)
Tag 05FP, a lemma

Tag 05FP in the Stacks Project.

AlgebraicGeometry.isWeaklyAssociatedPoint_pullback_iff_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/EtalePullback.lean, line 239.

Stacks Project, Tag 05FP. A point is weakly associated to the pullback of a quasi-coherent module along an étale morphism if and only if its image is weakly associated to the original module.

lemma isWeaklyAssociatedPoint_pullback_iff_of_etale
    {U S : Scheme.{u}} (h : U ⟶ S) [Etale h]
    (G : S.Modules) [G.IsQuasicoherent] (x : U) :
    Stacks.Divisors.IsWeaklyAssociatedPoint ((Scheme.Modules.pullback h).obj G) x ↔
      Stacks.Divisors.IsWeaklyAssociatedPoint G (h.base x)

AlgebraicGeometry.schemeWeaklyAssociatedPoints_eq_preimage_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedLocallyFiniteCharts.lean, line 77. The attribute's comment: “the weakly associated points of a scheme etale over another, at the structure sheaf”.

For an étale morphism of schemes f : X ⟶ Y, the weakly associated points of X are the preimage under f of the weakly associated points of Y.

theorem schemeWeaklyAssociatedPoints_eq_preimage_of_etale {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Etale f] :
    Stacks.Divisors.schemeWeaklyAssociatedPoints X =
      f.base ⁻¹' Stacks.Divisors.schemeWeaklyAssociatedPoints Y
Tag 0CTU, a lemma

Tag 0CTU in the Stacks Project.

AlgebraicGeometry.weaklyAssociated_tfae_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/EtaleLocalization/Henselization.lean, line 164.

Stacks Project, Tag 0CTU. A point is weakly associated to a quasi-coherent sheaf if and only if the maximal ideal of its stalk is weakly associated to the stalk module; equivalently, the corresponding maximal ideal remains weakly associated after extension to a henselization or a strict henselization.

theorem weaklyAssociated_tfae_henselization
    {X : Scheme.{u}} (F : X.Modules) [F.IsQuasicoherent] (x : X)
    {Rh Rsh : Type u}
    [CommRing Rh] [IsLocalRing Rh] [Algebra (X.presheaf.stalk x) Rh]
    [IsHenselization (X.presheaf.stalk x) (ResidueField (X.presheaf.stalk x)) Rh]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra (X.presheaf.stalk x) Rsh]
    [Algebra (ResidueField (X.presheaf.stalk x)) (ResidueField Rsh)]
    [IsSepClosure (ResidueField (X.presheaf.stalk x)) (ResidueField Rsh)]
    [IsHenselization (X.presheaf.stalk x) (ResidueField Rsh) Rsh] :
    let F' : PresheafOfModules (X.presheaf ⋙ forget₂ CommRingCat RingCat) := F.val
    let M := ↑(TopCat.Presheaf.stalk F'.presheaf x)
    letI : Module (X.presheaf.stalk x) M := inferInstance
    List.TFAE
      [Stacks.Divisors.IsWeaklyAssociatedPoint F x,
       IsWeaklyAssociatedPrime (X.presheaf.stalk x) M
         (maximalIdeal (X.presheaf.stalk x)),
       IsWeaklyAssociatedPrime Rh (TensorProduct (X.presheaf.stalk x) Rh M)
         (maximalIdeal Rh),
       IsWeaklyAssociatedPrime Rsh (TensorProduct (X.presheaf.stalk x) Rsh M)
         (maximalIdeal Rsh)]
Sources
LeanStacks.Etale.exists_etale_lift_of_isClosedImmersion · AlgebraicGeometry.etale_stalkBaseChangeMap · AlgebraicGeometry.isFlatOverAt_comp_iff_of_etale · AlgebraicGeometry.isFlatOver_comp_iff_of_etale · AlgebraicGeometry.flat_stalk_iff_of_etale · flat_tfae_henselization · flat_tfae_baseChange_henselization · flat_tfae_iteratedBaseChange_henselization

Section38.3 The local structure of a finite type module#

Section 38.3 of the Stacks Project, Tag 057P. 4 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 057Q, a lemma

Tag 057Q in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_closedSubscheme_fiber_eq_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FiniteTypeModuleLocalStructure.lean, line 264.

[Stacks, Tag 057Q]. Let f : X ⟶ S be a finite type morphism of affine schemes and let F be a quasi-coherent 𝒪_X-module of finite type. For every point s of S there is a closed immersion i : Z ⟶ X of finite presentation and a quasi-coherent finite type 𝒪_Z-module G with i_* G ≅ F whose fibre over s is the support of the restriction of F to the fibre of X over s.

The equality of the fibre with the support is an equality of subsets of X: the image of the fibre of Z is the image of the support of the pullback of F to the fibre of X.

theorem exists_finitePresentation_closedSubscheme_fiber_eq_supp {S : Scheme.{u}} (f : X ⟶ S)
    [IsAffine X] [IsAffine S] [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (s : S) :
    ∃ (Z : Scheme.{u}) (i : Z ⟶ X) (G : Z.Modules)
      (_ : (Scheme.Modules.pushforward i).obj G ≅ F),
      IsClosedImmersion i ∧ FinitePresentation i ∧ G.IsQuasicoherent ∧ G.IsFiniteType ∧
        Set.range (fun z : (i ≫ f).fiber s => i ((i ≫ f).fiberι s z)) =
          f.fiberι s '' SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)
Tag 057S, a lemma

Tag 057S in the Stacks Project.

AlgebraicGeometry.exists_elementaryDevissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/ElementaryDevissage.lean, line 811.

Stacks Project, Tag 057S. A finite-type quasi-coherent module admits an elementary dévissage at any point of the support of its fibre.

theorem exists_elementaryDevissage {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (x : X)
    (hx : f.asFiber x ∈
      SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι (f x))).obj F)) :
    Nonempty (ElementaryDevissage f F x hx)
Tag 057T, a lemma

Tag 057T in the Stacks Project.

AlgebraicGeometry.ElementaryDevissage.finitePresentation_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FinitePresentationTransfer.lean, line 338. The attribute's comment: “finite presentation of π”.

Stacks Project, Tag 057T. The finite morphism π of an elementary dévissage of a morphism locally of finite presentation is of finite presentation.

The composite Z ⟶ Y ⟶ V equals Z ⟶ U ⟶ X ⟶ S, which is locally of finite presentation because the closed immersion i is, U ⟶ X is étale and f is; the structure morphism V ⟶ S is locally of finite type, so Stacks 02FV strips it off twice and leaves π locally of finite presentation. A finite morphism is quasi-compact and quasi-separated, so π is of finite presentation.

theorem finitePresentation_π [LocallyOfFinitePresentation f] (D : ElementaryDevissage f F x hx) :
    FinitePresentation D.π

AlgebraicGeometry.ElementaryDevissage.isFinitePresentationNear_iff_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FinitePresentationTransfer.lean, line 361. The attribute's comment: “equivalence of (1), (2) and (3)”.

Stacks Project, Tag 057T, the equivalence of conditions (1) and (2). In an elementary dévissage, F is of finite presentation near x exactly when the module G on the closed subscheme is of finite presentation near z.

Finite presentation near x passes to the étale neighbourhood U and back by Stacks 01BQ and Stacks 05B0; on U the module is i_* G by the dévissage isomorphism, and the closed immersion i is finite with singleton fibre, so Stacks 05B4 and Stacks 05B8 exchange i_* G and G.

theorem isFinitePresentationNear_iff_closed [F.IsQuasicoherent]
    (D : ElementaryDevissage f F x hx) :
    IsFinitePresentationNear F x ↔ IsFinitePresentationNear D.G D.z

AlgebraicGeometry.ElementaryDevissage.isFinitePresentationNear_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FinitePresentationTransfer.lean, line 382. The attribute's comment: “equivalence of (1), (2) and (3)”.

Stacks Project, Tag 057T, the equivalence of conditions (2) and (3). In an elementary dévissage of a morphism locally of finite presentation, the module G is of finite presentation near z exactly when its direct image π_* G is of finite presentation near π z.

The morphism π is finite, of finite presentation by AlgebraicGeometry.ElementaryDevissage.finitePresentation_π, and its fibre over π z is {z}, so this is the transfer across a finite morphism with a singleton fibre.

theorem isFinitePresentationNear_iff_pushforward [LocallyOfFinitePresentation f]
    (D : ElementaryDevissage f F x hx) :
    IsFinitePresentationNear D.G D.z ↔
      IsFinitePresentationNear ((Scheme.Modules.pushforward D.π).obj D.G) (D.π D.z)

AlgebraicGeometry.ElementaryDevissage.finitePresentation_stalk_iff_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FinitePresentationTransfer.lean, line 400. The attribute's comment: “equivalence of (a), (b) and (c)”.

Stacks Project, Tag 057T, the equivalence of conditions (a) and (b). In an elementary dévissage the stalk F_x is a finitely presented 𝒪_{X,x}-module exactly when the stalk G_z is a finitely presented 𝒪_{Z,z}-module.

The étale morphism U ⟶ X is flat, so the stalk map 𝒪_{X,x} → 𝒪_{U,i z} is a flat local homomorphism and finite presentation of the stalk is unchanged by the pullback; the pullback of F to U is i_* G; and the closed immersion i is finite, of finite presentation and has singleton fibre, so Stacks 05B8 and Stacks 0564 exchange (i_* G)_{i z} and G_z.

theorem finitePresentation_stalk_iff_closed (D : ElementaryDevissage f F x hx) :
    Module.FinitePresentation (ToType (X.presheaf.stalk x))
        (ToType (TopCat.Presheaf.stalk F.val.presheaf x)) ↔
      Module.FinitePresentation (ToType (D.Z.presheaf.stalk D.z))
        (ToType (TopCat.Presheaf.stalk D.G.val.presheaf D.z))

AlgebraicGeometry.ElementaryDevissage.finitePresentation_stalk_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FinitePresentationTransfer.lean, line 425. The attribute's comment: “equivalence of (a), (b) and (c)”.

Stacks Project, Tag 057T, the equivalence of conditions (b) and (c). In an elementary dévissage of a morphism locally of finite presentation the stalk G_z is a finitely presented 𝒪_{Z,z}-module exactly when the stalk (π_* G)_{π z} is a finitely presented 𝒪_{Y,π z}-module.

The morphism π is finite, of finite presentation by AlgebraicGeometry.ElementaryDevissage.finitePresentation_π, and its fibre over π z is {z}, so this is the transfer of finite presentation of a stalk across a finite morphism with a singleton fibre.

theorem finitePresentation_stalk_iff_pushforward [LocallyOfFinitePresentation f]
    (D : ElementaryDevissage f F x hx) :
    Module.FinitePresentation (ToType (D.Z.presheaf.stalk D.z))
        (ToType (TopCat.Presheaf.stalk D.G.val.presheaf D.z)) ↔
      Module.FinitePresentation (ToType (D.Y.presheaf.stalk (D.π D.z)))
        (ToType (TopCat.Presheaf.stalk
          ((Scheme.Modules.pushforward D.π).obj D.G).val.presheaf (D.π D.z)))
Tag 057U, a lemma

Tag 057U in the Stacks Project.

AlgebraicGeometry.ElementaryDevissage.isFlatOverAt_iff_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FlatnessTransfer.lean, line 252. The attribute's comment: “equivalence of (a), (b) and (c)”.

Stacks Project, Tag 057U, the equivalence of conditions (a) and (b). In an elementary dévissage the stalk F_x is flat over 𝒪_{S,f x} exactly when the stalk G_z is flat over 𝒪_{V,h (π z)}.

The étale morphism U ⟶ X is flat, so Stacks 02JZ replaces F at x by its pullback to U at the distinguished point; Stacks 05B9 replaces flatness over S by flatness over V; the pullback of F to U is i_* G; and the closed immersion i is finite with singleton fibre, so Stacks 05B8 exchanges the stalk of i_* G for the stalk of G.

theorem isFlatOverAt_iff_closed [F.IsQuasicoherent] (D : ElementaryDevissage f F x hx) :
    IsFlatOverAt f.toLRSHom.toShHom F x ↔
      IsFlatOverAt (D.π ≫ D.h).toLRSHom.toShHom D.G D.z

AlgebraicGeometry.ElementaryDevissage.isFlatOverAt_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FlatnessTransfer.lean, line 286. The attribute's comment: “equivalence of (a), (b) and (c)”.

Stacks Project, Tag 057U, the equivalence of conditions (b) and (c). In an elementary dévissage the stalk G_z is flat over 𝒪_{V,h (π z)} exactly when the stalk (π_* G)_{π z} is.

The morphism π is finite and its fibre over π z is {z}, so this is the transfer of flatness over the base at a point across a finite morphism with a singleton fibre.

theorem isFlatOverAt_iff_pushforward (D : ElementaryDevissage f F x hx) :
    IsFlatOverAt (D.π ≫ D.h).toLRSHom.toShHom D.G D.z ↔
      IsFlatOverAt D.h.toLRSHom.toShHom
        ((Scheme.Modules.pushforward D.π).obj D.G) (D.π D.z)

AlgebraicGeometry.ElementaryDevissage.isFlatOverNear_iff_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FlatnessTransfer.lean, line 302. The attribute's comment: “equivalence of (1), (2) and (3)”.

Stacks Project, Tag 057U, the equivalence of conditions (1) and (2). In an elementary dévissage, F is flat over S near x exactly when G is flat over V near z.

The étale morphism U ⟶ X is flat and open, so Stacks 02JZ transfers flatness over the base near x to flatness of the pullback near the distinguished point of U; Stacks 05B9 interchanges flatness over S and over V; the pullback is i_* G; and the closed immersion i is finite with singleton fibre, so Stacks 0FLM and Stacks 05B8 exchange i_* G and G.

theorem isFlatOverNear_iff_closed [F.IsQuasicoherent] (D : ElementaryDevissage f F x hx) :
    IsFlatOverNear f F x ↔ IsFlatOverNear (D.π ≫ D.h) D.G D.z

AlgebraicGeometry.ElementaryDevissage.isFlatOverNear_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/FlatnessTransfer.lean, line 324. The attribute's comment: “equivalence of (1), (2) and (3)”.

Stacks Project, Tag 057U, the equivalence of conditions (2) and (3). In an elementary dévissage, G is flat over V near z exactly when π_* G is flat over V near π z.

The morphism π is finite and its fibre over π z is {z}, so this is the transfer of flatness over the base near a point across a finite morphism with a singleton fibre.

theorem isFlatOverNear_iff_pushforward (D : ElementaryDevissage f F x hx) :
    IsFlatOverNear (D.π ≫ D.h) D.G D.z ↔
      IsFlatOverNear D.h ((Scheme.Modules.pushforward D.π).obj D.G) (D.π D.z)
Sources
LeanAlgebraicGeometry.exists_finitePresentation_closedSubscheme_fiber_eq_supp · AlgebraicGeometry.exists_elementaryDevissage · AlgebraicGeometry.ElementaryDevissage.finitePresentation_π · AlgebraicGeometry.ElementaryDevissage.isFinitePresentationNear_iff_closed · AlgebraicGeometry.ElementaryDevissage.isFinitePresentationNear_iff_pushforward · AlgebraicGeometry.ElementaryDevissage.finitePresentation_stalk_iff_closed · AlgebraicGeometry.ElementaryDevissage.finitePresentation_stalk_iff_pushforward · AlgebraicGeometry.ElementaryDevissage.isFlatOverAt_iff_closed

Section38.4 One step dévissage#

Section 38.4 of the Stacks Project, Tag 05H3. 9 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05H4, a definition

Tag 05H4 in the Stacks Project.

AlgebraicGeometry.OneStepDevissage, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep.lean, line 77.

A one-step dévissage of F/X/S over s.

structure OneStepDevissage {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (s : S)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
Tag 05H5, a definition

Tag 05H5 in the Stacks Project.

AlgebraicGeometry.OneStepDevissageAt, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep.lean, line 110.

A one-step dévissage of F/X/S at x.

structure OneStepDevissageAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
Tag 05H6, a lemma

Tag 05H6 in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_oneStepDevissageAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/EtaleNeighborhoodOneStep.lean, line 260.

Stacks Project, Tag 05H6. A finite-type quasi-coherent module supported at a point of a fibre admits a one-step dévissage there after elementary étale neighbourhoods of the point and of its image.

theorem exists_etaleNeighborhood_oneStepDevissageAt {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (x : X)
    (hx : f.asFiber x ∈
      SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι (f x))).obj F)) :
    ∃ (U : EtaleNeighborhood X x) (V : EtaleNeighborhood S (f x)) (h : U.scheme ⟶ V.scheme),
      U.IsElementary ∧ V.IsElementary ∧ (U.toBase ≫ f = h ≫ V.toBase) ∧
        (h U.point = V.point) ∧
        ∃ (hft : LocallyOfFiniteType h)
          (hq : ((Scheme.Modules.pullback U.toBase).obj F).IsQuasicoherent)
          (hf : ((Scheme.Modules.pullback U.toBase).obj F).IsFiniteType),
          letI : LocallyOfFiniteType h := hft
          letI : ((Scheme.Modules.pullback U.toBase).obj F).IsQuasicoherent := hq
          letI : ((Scheme.Modules.pullback U.toBase).obj F).IsFiniteType := hf
          Nonempty (OneStepDevissageAt h
            ((Scheme.Modules.pullback U.toBase).obj F) U.point)

AlgebraicGeometry.exists_etaleNeighborhood_oneStepDevissageAt_iff_mem_fiber_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/EtaleNeighborhoodOneStep.lean, line 551.

Stacks Project, Tag 05H6, in sharp form. The elementary étale neighbourhoods of (X, x) and of (S, f x) over which the pullback of F acquires a one-step dévissage at the distinguished point exist exactly when x lies in the support of the restriction of F to the fibre of f through x.

The forward implication is the converse of the source's lemma; it holds because a one-step dévissage at a point records that the point lies in the support of the module on its fibre (AlgebraicGeometry.OneStepDevissageAt.mem_supp), and the support of the pullback of F to an étale neighbourhood is the inverse image of the support of F.

theorem exists_etaleNeighborhood_oneStepDevissageAt_iff_mem_fiber_supp {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (x : X) :
    (∃ (U : EtaleNeighborhood X x) (V : EtaleNeighborhood S (f x)) (h : U.scheme ⟶ V.scheme),
      U.IsElementary ∧ V.IsElementary ∧ (U.toBase ≫ f = h ≫ V.toBase) ∧
        (h U.point = V.point) ∧
        ∃ (hft : LocallyOfFiniteType h)
          (hq : ((Scheme.Modules.pullback U.toBase).obj F).IsQuasicoherent)
          (hf : ((Scheme.Modules.pullback U.toBase).obj F).IsFiniteType),
          letI : LocallyOfFiniteType h := hft
          letI : ((Scheme.Modules.pullback U.toBase).obj F).IsQuasicoherent := hq
          letI : ((Scheme.Modules.pullback U.toBase).obj F).IsFiniteType := hf
          Nonempty (OneStepDevissageAt h
            ((Scheme.Modules.pullback U.toBase).obj F) U.point)) ↔
      f.asFiber x ∈
        SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι (f x))).obj F)
Tag 05H7, a lemma

Tag 05H7 in the Stacks Project.

AlgebraicGeometry.OneStepDevissage.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/BaseChange.lean, line 245.

Stacks Project, Tag 05H7. A one-step dévissage and all its presenting data persist under base change to a pointed affine scheme.

def baseChange {X S S' : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
    (s : S) (s' : S') (h : S' ⟶ S) (hs : h s' = s)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType] [IsAffine S']
    (D : OneStepDevissage f F s) :
    BaseChangeData f F s s' h hs D
Tag 05H8, a lemma

Tag 05H8 in the Stacks Project.

AlgebraicGeometry.OneStepDevissageAt.exists_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/BaseChangeAt.lean, line 481.

Stacks Project, Tag 05H8. A one-step dévissage at a point survives an affine pointed base change which induces an isomorphism of residue fields: for the unique points x', z', y' of the base-changed schemes lying over the original distinguished points and over the new base point, the base-changed dévissage is a one-step dévissage at x' with distinguished points z' and y'.

theorem exists_baseChange {X S S' : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : OneStepDevissageAt f F x)
    (s' : S') (h : S' ⟶ S) (hs : h s' = f x) [IsAffine S']
    [IsIso ((S.residueFieldCongr hs).inv ≫ h.residueFieldMap s')]
    (B : OneStepDevissage.BaseChangeData f F (f x) s' h hs D.toOneStepDevissage) :
    letI := B.locallyOfFiniteType
    letI := B.quasicoherent
    letI := B.finiteType
    ∀ (x' : ↥(pullback f h)) (_ : pullback.fst f h x' = x)
      (_ : pullback.snd f h x' = s') (z' : B.devissage.Z) (_ : B.pZ z' = D.z)
      (_ : (B.devissage.π ≫ B.devissage.g) z' = s') (y' : B.devissage.Y)
      (_ : B.pY y' = D.y) (_ : B.devissage.g y' = s'),
      ∃ E : OneStepDevissageAt (pullback.snd f h)
          ((Scheme.Modules.pullback (pullback.fst f h)).obj F) x',
        HEq E.toOneStepDevissage B.devissage ∧ HEq E.z z' ∧ HEq E.y y'

AlgebraicGeometry.OneStepDevissageAt.exists_baseChange_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/BaseChangeAtPoints.lean, line 130.

Stacks Project, Tag 05H8. A one-step dévissage at a point survives an affine pointed base change which induces an isomorphism of residue fields: the base change of the dévissage constructed in AlgebraicGeometry.OneStepDevissage.baseChange is a one-step dévissage at the unique point x' of the base-changed source lying over x and over the new base point, with distinguished points the unique points z' and y' of the base-changed closed subscheme and smooth scheme lying over z and y and over the new base point.

theorem exists_baseChange_of_affine {X S S' : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : OneStepDevissageAt f F x)
    (s' : S') (h : S' ⟶ S) (hs : h s' = f x) [IsAffine S']
    [IsIso ((S.residueFieldCongr hs).inv ≫ h.residueFieldMap s')] :
    let B := OneStepDevissage.baseChange f F (f x) s' h hs D.toOneStepDevissage
    letI := B.locallyOfFiniteType
    letI := B.quasicoherent
    letI := B.finiteType
    ∃ (x' : ↥(pullback f h)) (z' : B.devissage.Z) (y' : B.devissage.Y)
      (E : OneStepDevissageAt (pullback.snd f h)
        ((Scheme.Modules.pullback (pullback.fst f h)).obj F) x'),
      ((pullback.fst f h x' = x ∧ pullback.snd f h x' = s') ∧
        ∀ w : ↥(pullback f h), pullback.fst f h w = x → pullback.snd f h w = s' → w = x') ∧
      ((B.pZ z' = D.z ∧ (B.devissage.π ≫ B.devissage.g) z' = s') ∧
        ∀ w : B.devissage.Z, B.pZ w = D.z →
          (B.devissage.π ≫ B.devissage.g) w = s' → w = z') ∧
      ((B.pY y' = D.y ∧ B.devissage.g y' = s') ∧
        ∀ w : B.devissage.Y, B.pY w = D.y → B.devissage.g w = s' → w = y') ∧
      HEq E.toOneStepDevissage B.devissage ∧ HEq E.z z' ∧ HEq E.y y'
Tag 05H9, a definition

Tag 05H9 in the Stacks Project.

AlgebraicGeometry.OneStepDevissageAt.StandardShrinking, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep.lean, line 145.

A standard shrinking of a one-step dévissage at x.

structure StandardShrinking {X S : Scheme.{u}} (f : X ⟶ S)
    (F : X.Modules) (x : X) [LocallyOfFiniteType f]
    [F.IsQuasicoherent] [F.IsFiniteType]
    (D : OneStepDevissageAt f F x)
Tag 05HA, a lemma

Tag 05HA in the Stacks Project.

AlgebraicGeometry.exists_standardShrinking_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/Shrinking.lean, line 470. The attribute's comment: “part (1)”.

Stacks Tag 05HA, part (1). Restricting a one-step dévissage at x to a principal open neighbourhood V of f x in the base is a standard shrinking, whose other three opens are the inverse images of V.

theorem exists_standardShrinking_base {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType] (D : OneStepDevissageAt f F x)
    (V : S.Opens) (a : Γ(S, ⊤)) (hV : V = S.basicOpen a) (hs : f x ∈ V) :
    ∃ E : D.StandardShrinking, E.S' = V ∧ E.X' = f ⁻¹ᵁ V ∧
      E.Z' = (D.toOneStepDevissage.i ≫ f) ⁻¹ᵁ V ∧ E.Y' = D.toOneStepDevissage.g ⁻¹ᵁ V

AlgebraicGeometry.exists_standardShrinking_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/Shrinking.lean, line 495. The attribute's comment: “part (2)”.

Stacks Tag 05HA, part (2). Given a principal open neighbourhood W of the distinguished point y of the smooth scheme, there is a standard shrinking whose smooth open is W cut down to the inverse image of the new base.

theorem exists_standardShrinking_smooth {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType] (D : OneStepDevissageAt f F x)
    (W : D.toOneStepDevissage.Y.Opens) (a : Γ(D.toOneStepDevissage.Y, ⊤))
    (hW : W = D.toOneStepDevissage.Y.basicOpen a) (hy : D.y ∈ W) :
    ∃ E : D.StandardShrinking, E.Y' = W ⊓ (D.toOneStepDevissage.g ⁻¹ᵁ E.S')

AlgebraicGeometry.exists_standardShrinking_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/Shrinking.lean, line 507. The attribute's comment: “part (3)”.

Stacks Tag 05HA, part (3). Given any open neighbourhood U of x, there is a standard shrinking whose source open lies inside U.

theorem exists_standardShrinking_source {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType] (D : OneStepDevissageAt f F x)
    (U : X.Opens) (hx : x ∈ U) : ∃ E : D.StandardShrinking, E.X' ≤ U
Tag 05HE, a lemma

Tag 05HE in the Stacks Project.

AlgebraicGeometry.exists_oneStepDevissageAt_of_etaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Glueing.lean, line 630.

Stacks Project, Tag 05HE. A one-step dévissage at a point can be pulled through a compatible pair of elementary étale neighbourhoods of the base and of the smooth scheme, after a further elementary étale localization of the base: the new smooth scheme is an open subscheme of the base change of the given neighbourhood, the new closed subscheme is the base change of the old one, and the new module is the pullback of the old one.

theorem exists_oneStepDevissageAt_of_etaleNeighborhood
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : OneStepDevissageAt f F x)
    (U : EtaleNeighborhood S (f x)) (hU : U.IsElementary)
    (V : EtaleNeighborhood D.toOneStepDevissage.Y D.y)
    (hV : V.IsElementary) (h : V.scheme ⟶ U.scheme)
    (hcomm : V.toBase ≫ D.toOneStepDevissage.g = h ≫ U.toBase)
    (hpoint : h V.point = U.point) :
    ∃ (W : EtaleNeighborhood U.scheme U.point)
      (_ : W.IsElementary)
      (A : EtaleNeighborhood X x) (_ : A.IsElementary)
      (b : A.scheme ⟶ W.scheme),
      b A.point = W.point ∧
      A.toBase ≫ f = b ≫ W.toBase ≫ U.toBase ∧
      ∃ (hl : LocallyOfFiniteType b)
        (hq : ((Scheme.Modules.pullback A.toBase).obj F).IsQuasicoherent)
        (ht : ((Scheme.Modules.pullback A.toBase).obj F).IsFiniteType),
        letI := hl
        letI := hq
        letI := ht
        ∃ (D' : OneStepDevissageAt b ((Scheme.Modules.pullback A.toBase).obj F) A.point)
          (j : D'.toOneStepDevissage.Y ⟶ pullback h W.toBase)
          (p : D'.toOneStepDevissage.Z ⟶ D.toOneStepDevissage.Z),
          IsOpenImmersion j ∧
          D'.toOneStepDevissage.g = j ≫ pullback.snd h W.toBase ∧
          (j ≫ pullback.fst h W.toBase) D'.y = V.point ∧
          p D'.z = D.z ∧
          D'.toOneStepDevissage.i ≫ A.toBase =
            p ≫ D.toOneStepDevissage.i ∧
          IsPullback p D'.toOneStepDevissage.i D.toOneStepDevissage.i
            A.toBase ∧
          IsPullback p D'.toOneStepDevissage.π D.toOneStepDevissage.π
            (j ≫ pullback.fst h W.toBase ≫ V.toBase) ∧
          Nonempty (D'.toOneStepDevissage.G ≅
            (Scheme.Modules.pullback p).obj D.toOneStepDevissage.G)
Tag 05HF, a lemma

Tag 05HF in the Stacks Project.

AlgebraicGeometry.exists_freeMap_isIso_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/FreeMap.lean, line 591. The attribute's comment: “existence of the generically invertible map”.

Stacks 05HF, first assertion. For a one-step dévissage, a free 𝒪_Y-module of positive finite rank maps to the direct image π_* G by a map that becomes an isomorphism over the residue field of the image in Y of a point of the fibre of g over s.

theorem exists_freeMap_isIso_genericFiber :
    ∃ (r : ℕ) (_ : 0 < r)
      (α : SheafOfModules.free (R := D.Y.ringCatSheaf) (ULift.{u} (Fin r)) ⟶
        (Scheme.Modules.pushforward D.π).obj D.G),
      IsIso ((Scheme.Modules.pullback
        (D.Y.fromSpecResidueField (D.g.fiberι s ξ))).map α)

AlgebraicGeometry.dim_support_cokernel_fiber_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/OneStep/FreeMap.lean, line 644. The attribute's comment: “dimension of the cokernel support”.

Stacks 05HF, second assertion. If a map into the direct image π_* G of a one-step dévissage becomes an isomorphism over the residue field of the image in Y of a point of the fibre of g over s, then the fibre over s of the support of its cokernel has strictly smaller dimension than the fibre over s of the support of F.

theorem dim_support_cokernel_fiber_lt {P : D.Y.Modules}
    (α : P ⟶ (Scheme.Modules.pushforward D.π).obj D.G)
    (hα : IsIso ((Scheme.Modules.pullback
      (D.Y.fromSpecResidueField (D.g.fiberι s ξ))).map α)) :
    topologicalKrullDim
        (SheafOfModules.supp ((Scheme.Modules.pullback (D.g.fiberι s)).obj (cokernel α))) <
      topologicalKrullDim
        (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F))
Sources
LeanAlgebraicGeometry.OneStepDevissage · AlgebraicGeometry.OneStepDevissageAt · AlgebraicGeometry.exists_etaleNeighborhood_oneStepDevissageAt · AlgebraicGeometry.exists_etaleNeighborhood_oneStepDevissageAt_iff_mem_fiber_supp · AlgebraicGeometry.OneStepDevissage.baseChange · AlgebraicGeometry.OneStepDevissageAt.exists_baseChange · AlgebraicGeometry.OneStepDevissageAt.exists_baseChange_of_affine · AlgebraicGeometry.OneStepDevissageAt.StandardShrinking

Section38.5 Complete dévissage#

Section 38.5 of the Stacks Project, Tag 05HG. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05HH, a definition

Tag 05HH in the Stacks Project.

AlgebraicGeometry.CompleteDevissage, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete.lean, line 151.

A complete dévissage of F/X/S over s: either the empty dévissage, which exists precisely for the zero module, or a finite nonempty chain of stages.

inductive CompleteDevissage {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (s : S)
    [hl : LocallyOfFiniteType f] [hq : F.IsQuasicoherent] [ht : F.IsFiniteType]
Tag 05HI, a definition

Tag 05HI in the Stacks Project.

AlgebraicGeometry.CompleteDevissageAt, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete.lean, line 212.

A complete dévissage of F/X/S at x: either the empty dévissage, which exists precisely for the zero module, or a nonempty chain of stages with compatible distinguished points.

inductive CompleteDevissageAt {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [hl : LocallyOfFiniteType f] [hq : F.IsQuasicoherent] [ht : F.IsFiniteType]
Tag 05HJ, a lemma

Tag 05HJ in the Stacks Project.

AlgebraicGeometry.exists_completeDevissage_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/BaseChange.lean, line 410.

Stacks 05HJ. A complete dévissage of F/X/S over s base-changes, stage by stage, to a complete dévissage of the base-changed module over s', for any cartesian square whose new base is affine.

theorem exists_completeDevissage_baseChange {X X' : Scheme.{u}} {f : X ⟶ S} {f' : X' ⟶ S'}
    {F : X.Modules} {F' : X'.Modules} (hs : h s' = s) [IsAffine S'] [LocallyOfFiniteType f]
    [F.IsQuasicoherent] [F.IsFiniteType] [LocallyOfFiniteType f'] [F'.IsQuasicoherent]
    [F'.IsFiniteType] (D : NonemptyCompleteDevissage f F s) (pX : X' ⟶ X)
    (hX : IsPullback pX f' f h) (eF : (Scheme.Modules.pullback pX).obj F ≅ F') :
    ∃ D' : NonemptyCompleteDevissage f' F' s', ChainIsBaseChange h pX D.chain D'.chain
Tag 05HK, a lemma

Tag 05HK in the Stacks Project.

AlgebraicGeometry.CompleteDevissageAt.exists_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/BaseChangeAt.lean, line 349.

Stacks 05HK. Let (S', s') → (S, s) be a morphism of pointed schemes inducing an isomorphism of residue fields, with S' affine, let X' be the base change of X and F' the pullback of F, and let x' ∈ X' lie over x ∈ X and s' (so s = f x, s' = f' x'). Then every complete dévissage of F/X/S at x base-changes, stage by stage as in Stacks 05HJ, to a complete dévissage of F'/X'/S' at x' whose distinguished points lie over the original ones. The finiteness properties of f' and F' are derived from the base change, not assumed.

theorem CompleteDevissageAt.exists_isBaseChange {h : S' ⟶ S} [IsAffine S']
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (hres : IsIso (h.residueFieldMap (f' x'))) (pX : X' ⟶ X) (hX : IsPullback pX f' f h)
    (eF : (Scheme.Modules.pullback pX).obj F ≅ F') (hx : pX x' = x)
    (D : CompleteDevissageAt f F x) :
    haveI := locallyOfFiniteType_of_isPullback hX
    haveI := isQuasicoherent_of_iso_pullback eF
    haveI := isFiniteType_of_iso_pullback eF
    ∃ D' : CompleteDevissageAt f' F' x', D.IsBaseChange h pX D'
Tag 05HL, a definition

Tag 05HL in the Stacks Project.

AlgebraicGeometry.NonemptyCompleteDevissageAt.StandardShrinking, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/StandardShrinking.lean, line 195.

A standard shrinking of a complete dévissage of F/X/S at x: standard opens of the base and of the source, and standard opens in every stage, containing the distinguished points, whose restricted system is again a complete dévissage at x.

structure StandardShrinking {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : NonemptyCompleteDevissageAt f F x)
Tag 05HM, a lemma

Tag 05HM in the Stacks Project.

AlgebraicGeometry.exists_standardShrinking_finalTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/ShrinkingFinalTarget.lean, line 339. The attribute's comment: “final_target_shrinking”.

Stacks 05HM, final target shrinking. Let W be a principal open neighbourhood of the distinguished point of the smooth scheme of the last stage of a complete dévissage of F/X/S at x. Then there is a standard shrinking of the dévissage whose last smooth open is W cut down to the inverse image of the new base.

theorem exists_standardShrinking_finalTarget {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
    (x : X) [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : NonemptyCompleteDevissageAt f F x) (W : (finalTargetScheme D.pointed).Opens)
    (a : Γ(finalTargetScheme D.pointed, ⊤))
    (hW : W = (finalTargetScheme D.pointed).basicOpen a)
    (hy : finalTargetPoint D.pointed ∈ W) :
    ∃ E : NonemptyCompleteDevissageAt.StandardShrinking f F x D,
      letI := E.locally_finite_type
      letI := E.quasi_coherent
      letI := E.finite_type
      FinalTargetIsBaseRestriction E.S'.ι E.S' D.pointed E.restricted_devissage.pointed
        E.restricted_stages W

AlgebraicGeometry.NonemptyCompleteDevissageAt.exists_standardShrinking_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/ShrinkingOverBase.lean, line 169. The attribute's comment: “base_shrinking”.

Stacks 05HM, base shrinking. Restricting a complete dévissage at x over a standard open neighbourhood of f x gives a standard shrinking whose base and source are that open and its inverse image, and all of whose stages are the corresponding base changes.

theorem exists_standardShrinking_base {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : NonemptyCompleteDevissageAt f F x)
    (V : S.Opens) (a : Γ(S, ⊤)) (hV : V = S.basicOpen a) (hs : f x ∈ V) :
    ∃ E : NonemptyCompleteDevissageAt.StandardShrinking f F x D,
      E.S' = V ∧ E.X' = f ⁻¹ᵁ V ∧
        (letI := E.locally_finite_type
         letI := E.quasi_coherent
         letI := E.finite_type
         PointedChainIsBaseChange E.S'.ι E.X'.ι D.pointed E.restricted_devissage.pointed)

AlgebraicGeometry.NonemptyCompleteDevissageAt.exists_standardShrinking_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/ShrinkingSource.lean, line 101. The attribute's comment: “source_shrinking”.

Stacks 05HM, source shrinking. A complete dévissage of F/X/S at x admits a standard shrinking whose source open lies inside any prescribed open neighbourhood of x.

theorem exists_standardShrinking_source {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFiniteType f] [F.IsQuasicoherent] [F.IsFiniteType]
    (D : NonemptyCompleteDevissageAt f F x) (U : X.Opens) (hx : x ∈ U) :
    ∃ E : NonemptyCompleteDevissageAt.StandardShrinking f F x D, E.X' ≤ U
Tag 05HR, a proposition

Tag 05HR in the Stacks Project.

AlgebraicGeometry.hasEtaleNeighborhoodCompleteDevissageAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/Existence.lean, line 619.

Stacks Project, Tag 05HR. A finite-type quasi-coherent module on a scheme locally of finite type over S acquires a complete dévissage at any chosen point after elementary étale neighbourhoods of that point and of its image.

The induction is a well-founded recursion on AlgebraicGeometry.fiberSupportDim, which takes values in the well-founded order WithBot ℕ∞.

theorem hasEtaleNeighborhoodCompleteDevissageAt {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (x : X) :
    HasEtaleNeighborhoodCompleteDevissageAt f F x
Tag 05HU, a lemma

Tag 05HU in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_completeDevissage_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/Existence.lean, line 1041.

Stacks Project, Tag 05HU. Let X ⟶ S be a finite-type morphism of schemes and F a finite-type quasi-coherent module on X. For every point s of S there is an elementary étale neighbourhood (S', s') ⟶ (S, s) and finitely many étale morphisms hᵢ : Yᵢ ⟶ X ×_S S' whose images cover the fibre (X ×_S S')_{s'} = X_s, such that the pullback of F to each Yᵢ has a complete dévissage along Yᵢ ⟶ S' over s'.

theorem exists_etaleNeighborhood_completeDevissage_cover {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules) [F.IsQuasicoherent]
    [F.IsFiniteType] (s : S) :
    ∃ (S' : EtaleNeighborhood S s) (_ : S'.IsElementary) (n : ℕ) (Y : Fin n → Scheme.{u})
      (h : ∀ i, Y i ⟶ pullback f S'.toBase) (_ : ∀ i, Etale (h i))
      (hl : ∀ i, LocallyOfFiniteType (h i ≫ pullback.snd f S'.toBase))
      (hq : ∀ i, ((Scheme.Modules.pullback
        (h i ≫ pullback.fst f S'.toBase)).obj F).IsQuasicoherent)
      (ht : ∀ i, ((Scheme.Modules.pullback
        (h i ≫ pullback.fst f S'.toBase)).obj F).IsFiniteType),
      (∀ i, Nonempty (@CompleteDevissage _ _ (h i ≫ pullback.snd f S'.toBase)
        ((Scheme.Modules.pullback (h i ≫ pullback.fst f S'.toBase)).obj F) S'.point
        (hl i) (hq i) (ht i))) ∧
        pullback.snd f S'.toBase ⁻¹' {S'.point} ⊆ ⋃ i, Set.range (h i)
Sources
LeanAlgebraicGeometry.CompleteDevissage · AlgebraicGeometry.CompleteDevissageAt · AlgebraicGeometry.exists_completeDevissage_baseChange · AlgebraicGeometry.CompleteDevissageAt.exists_isBaseChange · AlgebraicGeometry.NonemptyCompleteDevissageAt.StandardShrinking · AlgebraicGeometry.exists_standardShrinking_finalTarget · AlgebraicGeometry.NonemptyCompleteDevissageAt.exists_standardShrinking_base · AlgebraicGeometry.NonemptyCompleteDevissageAt.exists_standardShrinking_source

Section38.6 Translation into algebra#

Section 38.6 of the Stacks Project, Tag 05HV. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05HW, a definition

Tag 05HW in the Stacks Project.

Algebra.ElementaryEtaleLocalization, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ElementaryEtaleNeighborhood.lean, line 70.

An elementary étale localization of R → S at a prime q lying over p.

The rings R' and S', their structure maps, and commutes form the square of the definition. The primes p' and q' lie over the indicated primes, and the canonical residue-field maps are isomorphisms.

public structure Algebra.ElementaryEtaleLocalization (R : Type u) (S : Type v)
    [CommRing R] [CommRing S]
    [Algebra R S] (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
Tag 05HX, a definition

Tag 05HX in the Stacks Project.

Module.CompleteDevissage, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/CompleteDevissage.lean, line 89.

A complete dévissage of a finite S-module N over a prime ideal r of R.

There are stepCount + 1 stages. At stage i, A i and B i are R-algebras, M i is a finite A i-module, and alpha i maps a finite free B i-module to M i viewed as a B i-module through toLeft i. The maps toRight connect consecutive stages.

public structure CompleteDevissage (R : Type u) (S : Type v) (N : Type w) [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.FiniteType R S] [AddCommGroup N] [Module S N]
    [Module.Finite S N] (r : Ideal R) [r.IsPrime]

Ideal.isPrime_map_of_smooth_of_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/GeometricallyIrreducibleFibres.lean, line 66. The attribute's comment: “the prime of the lower algebra”.

Stacks Project, Tag 05HX. If R → B is smooth and the fibres of Spec B → Spec R are geometrically irreducible, then the ideal generated by a prime r of R in B is prime. It is the generic point of the fibre over r.

theorem Ideal.isPrime_map_of_smooth_of_geometricallyIrreducible
    (R B : Type u) [CommRing R] [CommRing B] [Algebra R B] [Algebra.Smooth R B]
    [GeometricallyIrreducible (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
    (r : Ideal R) [r.IsPrime] : (Ideal.map (algebraMap R B) r).IsPrime
Tag 05HY, a remark

Tag 05HY in the Stacks Project.

Module.CompleteDevissage.upperAlgebra_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 81. The attribute's comment: “finite presentation of the upper algebras after the first”.

Except for the first one, every upper algebra in a complete dévissage is finitely presented over the base.

public theorem upperAlgebra_finitePresentation (D : CompleteDevissage R S N r)
    (i : Fin D.stepCount) :
    Algebra.FinitePresentation R (D.A i.succ)

Module.CompleteDevissage.initialUpperAlgebra_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 92. The attribute's comment: “finite presentation of the first upper algebra”.

If the original algebra is finitely presented over the base, so is the first upper algebra in a complete dévissage.

public theorem initialUpperAlgebra_finitePresentation [Algebra.FinitePresentation R S]
    (D : CompleteDevissage R S N r) :
    Algebra.FinitePresentation R (D.A 0)

Module.CompleteDevissage.left_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 103. The attribute's comment: “finite presentation of the maps in the dévissage”.

When the original algebra is finitely presented over the base, every same-stage map B i → A i in a complete dévissage is finitely presented.

public theorem left_finitePresentation [Algebra.FinitePresentation R S]
    (D : CompleteDevissage R S N r) (i : Fin (D.stepCount + 1)) :
    (D.toLeft i).toRingHom.FinitePresentation

Module.CompleteDevissage.finitePresentation_iff_initial_over_upper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 120. The attribute's comment: “equivalence of conditions (1) and (2)”.

Condition (1) of Tag 05HY is equivalent to condition (2): finite presentation of the original module is equivalent to finite presentation of the first stage over its upper algebra.

public theorem finitePresentation_iff_initial_over_upper [Algebra.FinitePresentation R S]
    (D : CompleteDevissage R S N r) :
    Module.FinitePresentation S N ↔ Module.FinitePresentation (D.A 0) (D.M 0)

Module.CompleteDevissage.finitePresentation_iff_initial_over_lower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 142. The attribute's comment: “equivalence of conditions (2) and (3)”.

Conditions (2) and (3) of Tag 05HY are equivalent: at the first stage, finite presentation over the upper algebra is equivalent to finite presentation after restriction of scalars to the lower algebra.

public theorem finitePresentation_iff_initial_over_lower [Algebra.FinitePresentation R S]
    (D : CompleteDevissage R S N r) :
    letI : Module (D.B 0) (D.M 0) :=
      Module.compHom (D.M 0) (D.toLeft 0).toRingHom
    Module.FinitePresentation (D.A 0) (D.M 0) ↔
      Module.FinitePresentation (D.B 0) (D.M 0)

Module.CompleteDevissage.finitePresentation_iff_all_stages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageElementaryNeighborhood.lean, line 153. The attribute's comment: “equivalence of conditions (3) and (4)”.

Condition (3) of Tag 05HY is equivalent to condition (4): finite presentation at the first lower algebra propagates precisely to finite presentation over both algebras at every stage.

public theorem finitePresentation_iff_all_stages [Algebra.FinitePresentation R S]
    (D : CompleteDevissage R S N r) :
    letI : Module (D.B 0) (D.M 0) :=
      Module.compHom (D.M 0) (D.toLeft 0).toRingHom
    Module.FinitePresentation (D.B 0) (D.M 0) ↔
      ∀ i : Fin (D.stepCount + 1),
        Module.FinitePresentation (D.A i) (D.M i) ∧
          letI : Module (D.B i) (D.M i) :=
            Module.compHom (D.M i) (D.toLeft i).toRingHom
          Module.FinitePresentation (D.B i) (D.M i)

Declarations registered for the tag:

Tag 05HZ, a definition

Tag 05HZ in the Stacks Project.

Module.CompleteDevissageAt, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/CompleteDevissage.lean, line 328.

A complete dévissage at q is either the empty dévissage of the zero module, or a nonempty dévissage with the prime and dimension conditions of Stacks 05HZ.

public inductive CompleteDevissageAt (R : Type u) (S : Type v) (N : Type w)
    [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    [AddCommGroup N] [Module S N] [Module.Finite S N]
    (q : Ideal S) [q.IsPrime]
Tag 05I0, a remark

Tag 05I0 in the Stacks Project.

Module.nonempty_completeDevissage_of_completeDevissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/AlgebraTranslation.lean, line 178. The attribute's comment: “(1): a geometric complete dévissage over a point gives an algebraic one”.

Stacks Project, Tag 05I0, item (1).

Let f : X ⟶ S be locally of finite type between affine schemes, let ℱ be a quasi-coherent 𝒪_X-module of finite type and let s : S correspond to the prime r of Γ(S, ⊤). If there exists a complete dévissage of ℱ/X/S over s, then there exists a complete dévissage of Γ(ℱ, ⊤)/Γ(X, ⊤)/Γ(S, ⊤) over r.

Taking X = Spec B, S = Spec A and ℱ = Ñ recovers the statement of the source, whose N is Γ(ℱ, ⊤). Remark 05I0 states this item as an implication and nothing more, and says why: the definition of a complete dévissage of N/B/A over r, Stacks 05HX, omits the condition on the relative dimension that Stacks 05H4 (5) puts on the smooth scheme of a one-step dévissage, so the algebraic notion over r is the weaker of the two. The zero module separates them. It has the one-stage dévissage Module.CompleteDevissage.ofSubsingleton, while the zero sheaf has only the empty dévissage of Stacks 05HH: a smooth morphism with geometrically irreducible fibres has fibres of dimension at least 0, and dim (Supp(ℱ_s)) = -∞. Item (2) of the source, for the notions at a point, is an equivalence, because Stacks 05HZ (4) restores that condition.

Both cases of AlgebraicGeometry.CompleteDevissage are covered. A chain of stages is translated stage by stage by AlgebraicGeometry.DevissageChain.toCompleteDevissage. The empty dévissage, which AlgebraicGeometry.CompleteDevissage.empty allows for the zero sheaf, is sent to Module.CompleteDevissage.ofSubsingleton: the sections of a zero sheaf vanish, and the zero module has a one-stage algebraic dévissage — with the zero ring upstairs and Γ(S, ⊤) itself as the smooth algebra — because Stacks 05HX imposes no condition on the dimensions of the fibres, which is the same omission that makes this item one-directional.

public theorem nonempty_completeDevissage_of_completeDevissage {X S : Scheme.{u}}
    [IsAffine X] [IsAffine S] {f : X ⟶ S} {F : X.Modules} {s : S} [hl : LocallyOfFiniteType f]
    [hq : F.IsQuasicoherent] [ht : F.IsFiniteType] (r : Ideal Γ(S, ⊤)) [r.IsPrime]
    (hr : (S.isoSpec.hom s).asIdeal = r)
    (D : AlgebraicGeometry.CompleteDevissage f F s) :
    letI := f.appTop.hom.toAlgebra
    letI : Algebra.FiniteType Γ(S, ⊤) Γ(X, ⊤) :=
      HasRingHomProperty.appTop (P := @LocallyOfFiniteType) f hl
    letI : Module.Finite Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) :=
      Stacks.AlgebraicGeometry.CoherentFinite.finite_sections F (isAffineOpen_top X)
    Nonempty (Module.CompleteDevissage Γ(S, ⊤) Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) r)

Module.nonempty_completeDevissage_of_nonemptyCompleteDevissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/AlgebraTranslation.lean, line 217. The attribute's comment: “(1): a geometric complete dévissage over a point gives an algebraic one”.

Stacks Project, Tag 05I0, item (1).

Let f : X ⟶ S be locally of finite type between affine schemes, let ℱ be a quasi-coherent 𝒪_X-module of finite type and let s : S correspond to the prime r of Γ(S, ⊤). If there exists a nonempty complete dévissage of ℱ/X/S over s, then there exists a complete dévissage of Γ(ℱ, ⊤)/Γ(X, ⊤)/Γ(S, ⊤) over r.

Taking X = Spec B, S = Spec A and ℱ = Ñ recovers the statement of the source, whose N is Γ(ℱ, ⊤). The implication goes only in this direction: the source omits the condition on the relative dimension from the definition of a complete dévissage of N/B/A over r, so an algebraic dévissage carries strictly less information than a geometric one. The hypothesis is the nonempty notion because Module.CompleteDevissage, like the zigzag of Stacks 05HX, always has at least one stage, while AlgebraicGeometry.CompleteDevissage also allows the empty dévissage of the zero sheaf.

public theorem nonempty_completeDevissage_of_nonemptyCompleteDevissage {X S : Scheme.{u}}
    [IsAffine X] [IsAffine S] {f : X ⟶ S} {F : X.Modules} {s : S} [hl : LocallyOfFiniteType f]
    [hq : F.IsQuasicoherent] [ht : F.IsFiniteType] (r : Ideal Γ(S, ⊤)) [r.IsPrime]
    (hr : (S.isoSpec.hom s).asIdeal = r)
    (D : AlgebraicGeometry.NonemptyCompleteDevissage f F s) :
    letI := f.appTop.hom.toAlgebra
    letI : Algebra.FiniteType Γ(S, ⊤) Γ(X, ⊤) :=
      HasRingHomProperty.appTop (P := @LocallyOfFiniteType) f hl
    letI : Module.Finite Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) :=
      Stacks.AlgebraicGeometry.CoherentFinite.finite_sections F (isAffineOpen_top X)
    Nonempty (Module.CompleteDevissage Γ(S, ⊤) Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) r)

Module.nonempty_completeDevissageAt_of_completeDevissageAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/AlgebraTranslationAt.lean, line 328. The attribute's comment: “(2): a geometric complete dévissage at a point gives an algebraic one”.

Stacks Project, Tag 05I0, item (2).

Let f : X ⟶ S be locally of finite type between affine schemes, let ℱ be a quasi-coherent 𝒪_X-module of finite type and let x : X correspond to the prime q of Γ(X, ⊤). If ℱ/X/S has a complete dévissage at x then Γ(ℱ, ⊤)/Γ(X, ⊤)/Γ(S, ⊤) has a complete dévissage at q.

Taking X = Spec B, S = Spec A and ℱ = Ñ recovers the statement of the source, whose N is Γ(ℱ, ⊤), after composing Module.nonempty_completeDevissageAt_ofRingEquiv with the three comparison isomorphisms Γ(Spec A, ⊤) ≅ A, Γ(Spec B, ⊤) ≅ B and Γ(Ñ, ⊤) ≅ N.

The source states item (2) as an equivalence and uses only this direction; the equivalence is Module.nonempty_completeDevissageAt_iff in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/SpecCompleteDevissageAt.lean, whose converse half builds the scheme-theoretic dévissage out of the algebraic one on Spec.

public theorem nonempty_completeDevissageAt_of_completeDevissageAt {X S : Scheme.{u}}
    [IsAffine X] [IsAffine S] {f : X ⟶ S} {F : X.Modules} {x : X}
    [hl : LocallyOfFiniteType f] [hq : F.IsQuasicoherent] [ht : F.IsFiniteType]
    (q : Ideal Γ(X, ⊤)) (hqp : q.IsPrime) (hqx : (X.isoSpec.hom x).asIdeal = q)
    (D : AlgebraicGeometry.CompleteDevissageAt f F x) :
    letI := f.appTop.hom.toAlgebra
    letI : Algebra.FiniteType Γ(S, ⊤) Γ(X, ⊤) :=
      HasRingHomProperty.appTop (P := @LocallyOfFiniteType) f hl
    letI : Module.Finite Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) :=
      Stacks.AlgebraicGeometry.CoherentFinite.finite_sections F (isAffineOpen_top X)
    letI := hqp
    Nonempty (Module.CompleteDevissageAt Γ(S, ⊤) Γ(X, ⊤) Γ(F, (⊤ : X.Opens)) q)

Module.nonempty_completeDevissageAt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/SpecCompleteDevissageAt.lean, line 358. The attribute's comment: “(2): a complete dévissage at a point exists for the sheaf exactly when it exists for the module”.

Stacks Project, Tag 05I0 (2), as an equivalence. For a ring map A → B of finite type, a finite B-module N and a prime q of B, a complete dévissage of Ñ/Spec B/Spec A at the point of q exists if and only if a complete dévissage of N/B/A at q exists.

The relative dimension condition of Stacks 05HZ (4) is read fibre by fibre, as Stacks 05I0 describes it: every fibre of Spec Bᵢ → Spec A has the dimension dim_{qᵢ}(Supp(Mᵢ ⊗ κ(r))). That is the supremum condition Module.NonemptyCompleteDevissageAt.relativeDimension_eq_support of the dévissage together with Module.CompleteDevissageAt.FibresHaveRelativeDimension.

The direction from sheaves to modules is AlgebraicGeometry.exists_completeDevissageAt_fibresHaveRelativeDimension_of_spec; the converse is nonempty_completeDevissageAt_of_algebraic.

public theorem Module.nonempty_completeDevissageAt_iff (A B : Type u) [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.FiniteType A B] (N : Type u) [AddCommGroup N] [Module B N]
    [Module.Finite B N] (q : PrimeSpectrum B) :
    Nonempty (@AlgebraicGeometry.CompleteDevissageAt (Spec (.of B)) (Spec (.of A))
        (Spec.map (CommRingCat.ofHom (algebraMap A B)))
        (tilde (R := .of B) (ModuleCat.of B N)) q
        (AlgebraicGeometry.locallyOfFiniteType_specMap_algebraMap A B) inferInstance
        ((AlgebraicGeometry.tilde_isFiniteType_iff (R := .of B) (ModuleCat.of B N)).2
          inferInstance)) ↔
      ∃ D : @Module.CompleteDevissageAt A B N _ _ _ _ _ _ _ q.asIdeal q.isPrime,
        D.FibresHaveRelativeDimension
Tag 05I1, a lemma

Tag 05I1 in the Stacks Project.

Module.exists_elementaryEtaleLocalization_completeDevissageAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Devissage/Complete/AlgebraExistence.lean, line 348.

Stacks Project, Tag 05I1. Let R → S be a ring map of finite type, let M be a finite S-module and let q be a prime of S. There is an elementary étale localization of R → S at q — rings R' and S', primes p' and q' — such that (M ⊗_S S')/S'/R' has a complete dévissage at q'.

The localized ring map R' → S' is again of finite type, which the definition of a complete dévissage at a prime requires; it is returned with the dévissage because no consumer can state it in advance of the localization.

theorem exists_elementaryEtaleLocalization_completeDevissageAt (R S M : Type u) [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.FiniteType R S] [AddCommGroup M] [Module S M]
    [Module.Finite S M] (q : Ideal S) [q.IsPrime] :
    ∃ E : Algebra.ElementaryEtaleLocalization.{u, u, u, u} R S (q.under R) q,
      ∃ hFiniteType : Algebra.FiniteType E.R' E.S',
        letI := hFiniteType
        Nonempty (Module.CompleteDevissageAt E.R' E.S' (TensorProduct S E.S' M) E.q')
Sources
LeanAlgebra.ElementaryEtaleLocalization · Module.CompleteDevissage · Ideal.isPrime_map_of_smooth_of_geometricallyIrreducible · Module.CompleteDevissage.upperAlgebra_finitePresentation · Module.CompleteDevissage.initialUpperAlgebra_finitePresentation · Module.CompleteDevissage.left_finitePresentation · Module.CompleteDevissage.finitePresentation_iff_initial_over_upper · Module.CompleteDevissage.finitePresentation_iff_initial_over_lower

Section38.7 Localization and universally injective maps#

Section 38.7 of the Stacks Project, Tag 05DD. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05DE, a lemma

Tag 05DE in the Stacks Project.

Stacks.UniversalInjectivity.finite_maximalSpectrum_localization_nonZeroSMulDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 267. The attribute's comment: “semilocality; the multiplicative subset is nonZeroSMulDivisors”.

Localizing at the elements regular on a finite module over the Noetherian closed fibre of a local base produces a semilocal ring.

theorem finite_maximalSpectrum_localization_nonZeroSMulDivisors : Finite (MaximalSpectrum T)

Stacks.UniversalInjectivity.range_under_localization_nonZeroSMulDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 285. The attribute's comment: “the prime spectrum”.

The contractions of the primes of the localization are exactly the primes of S contained in an associated prime of the closed-fibre module.

theorem range_under_localization_nonZeroSMulDivisors :
    Set.range (fun q : PrimeSpectrum T ↦ q.asIdeal.under S) =
      {q : Ideal S | q.IsPrime ∧
        ∃ p ∈ assStacks S
          (N ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S N))), q ≤ p}

Stacks.UniversalInjectivity.exists_assStacks_closedFibre_of_isMaximal_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 302. The attribute's comment: “the maximal ideals”.

Every maximal ideal of the localization corresponds to an associated prime of the closed-fibre module over the closed-fibre ring, whose contraction to S is the maximal ideal's.

theorem exists_assStacks_closedFibre_of_isMaximal_localization (q : MaximalSpectrum T) :
    ∃ p ∈ assStacks (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
      (N ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S N))),
      p.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) =
        q.asIdeal.under S
Tag 05DF, a lemma

Tag 05DF in the Stacks Project.

Stacks.UniversalInjectivity.universallyInjectivePoly_lsmul_of_nonZeroSMulDivisors, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 363. The attribute's comment: “the homotheties”.

Every element acting injectively on the closed fibre defines a universally injective R-linear homothety of N.

lemma universallyInjectivePoly_lsmul_of_nonZeroSMulDivisors
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation)
    (s : nonZeroSMulDivisors S
      (N ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S N)))) :
    UniversallyInjectivePoly (((LinearMap.lsmul S N) s.1).restrictScalars R)

Stacks.UniversalInjectivity.universallyInjectivePoly_mkLinearMap_nonZeroSMulDivisors, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 376. The attribute's comment: “the localization map”.

The canonical map from N to its localization at the elements acting injectively on the closed fibre is universally injective over R.

lemma universallyInjectivePoly_mkLinearMap_nonZeroSMulDivisors
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation) :
    UniversallyInjectivePoly
      ((LocalizedModule.mkLinearMap
        (nonZeroSMulDivisors S
          (N ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) •
            (⊤ : Submodule S N)))) N).restrictScalars R)
Tag 05DG, a lemma

Tag 05DG in the Stacks Project.

Stacks.UniversalInjectivity.universallyInjectivePoly_tensorUnit_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChange.lean, line 494.

Let R → S be a local homomorphism of local rings, essentially of finite presentation, let N be a finitely presented S-module which is flat over R, and let S → S' be flat. If the image of Spec(S') → Spec(S) contains every prime of S lying over the maximal ideal of R which is an associated prime of the closed fibre N / 𝔪_R N, then the canonical map N → N ⊗[S] S' is universally injective over R.

theorem universallyInjectivePoly_tensorUnit_of_flat {R : Type u} {S : Type v} {S' : Type w}
    {N : Type x} [CommRing R] [CommRing S] [CommRing S'] [IsLocalRing R] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] [Algebra S S']
    [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.FinitePresentation S N] [Module.Flat R N] [Module.Flat S S']
    (hS : (algebraMap R S).EssentiallyOfFinitePresentation)
    (hspec : ∀ q : Ideal S, Ideal.comap (algebraMap R S) q = maximalIdeal R →
      IsAssociatedPrimeStacks S
        (N ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S N))) q →
      ∃ q' : Ideal S', q'.IsPrime ∧ Ideal.comap (algebraMap S S') q' = q) :
    UniversallyInjectivePoly (((TensorProduct.mk S N S').flip 1).restrictScalars R)
Tag 05DH, a lemma

Tag 05DH in the Stacks Project.

Stacks.UniversalInjectivity.universallyInjective_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/UniversallyInjectiveBaseChangeFlat.lean, line 589.

Stacks 05DH. Under the stated finite-presentation and flatness hypotheses, if every associated prime of each fibre of N lifts to S', then the canonical base-change map N → N ⊗[S] S' is universally injective over R.

theorem universallyInjective_baseChange_of_flat
    {R : Type u} {S : Type v} {S' N : Type w}
    [CommRing R] [CommRing S] [CommRing S']
    [AddCommGroup N] [Module S N] [Algebra R S] [Algebra S S']
    [Module R N] [IsScalarTower R S N] [Algebra R S'] [IsScalarTower R S S']
    [Algebra.FinitePresentation R S] [Module.FinitePresentation S N]
    [Module.Flat R N] [Module.Flat S S']
    (himage : ∀ (q : Ideal S) [q.IsPrime],
      IsAssociatedPrimeStacks S (N ⊗[R] (q.under R).ResidueField) q →
        ∃ q' : Ideal S', q'.IsPrime ∧ q'.under S = q) :
    UniversallyInjective
      (((TensorProduct.mk S N S').flip 1).restrictScalars R)
Tag 05FQ, a lemma

Tag 05FQ in the Stacks Project.

Module.Flat.rTensor_injective_of_projective_of_mem_maximalIdeal_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/MittagLeffler.lean, line 291. The attribute's comment: “the hypothesis spells out injectivity of M/𝔪M → N/𝔪N as u x ∈ 𝔪 • ⊤ → x ∈ 𝔪 • ⊤, the form Submodule.injective_mapQ_smul_top_iff shows it to be equivalent to; the conclusion spells out universal injectivity, which Mathlib has no name for, as in Stacks 0AS5, 05CJ and 05CM.”.

Stacks 05FQ. Let (R, 𝔪) be a local ring and let u : M →ₗ[R] N be a map of R-modules with M projective and N flat. If the reduction M/𝔪M → N/𝔪N is injective -- that is, if u x ∈ 𝔪 • ⊤ forces x ∈ 𝔪 • ⊤ -- then u is universally injective, i.e. u ⊗ id_Q is injective for every R-module Q.

public theorem Module.Flat.rTensor_injective_of_projective_of_mem_maximalIdeal_smul_top
    {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v} R] {M N : Type v} [AddCommGroup M]
    [Module R M] [Module.Projective R M] [AddCommGroup N] [Module R N] [Module.Flat R N]
    (u : M →ₗ[R] N)
    (hu : ∀ x : M, u x ∈ maximalIdeal R • (⊤ : Submodule R N) →
      x ∈ maximalIdeal R • (⊤ : Submodule R M)) :
    ∀ (Q : Type v) [AddCommGroup Q] [Module R Q], Function.Injective (u.rTensor Q)

Module.Flat.rTensor_injective_of_projective_of_injective_mapQ_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/MittagLeffler.lean, line 347. The attribute's comment: “M/𝔪M is M ⧸ 𝔪 • ⊤ and the reduction of u is Submodule.mapQ along u, as in Stacks 0AS5 and 046Y; the conclusion spells out universal injectivity, which Mathlib has no name for.”.

Stacks 05FQ. Let (R, 𝔪) be a local ring and let u : M →ₗ[R] N be a map of R-modules with M projective and N flat. If the induced map M/𝔪M → N/𝔪N is injective, then u is universally injective, i.e. u ⊗ id_Q is injective for every R-module Q.

public theorem Module.Flat.rTensor_injective_of_projective_of_injective_mapQ_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v} R] {M N : Type v} [AddCommGroup M]
    [Module R M] [Module.Projective R M] [AddCommGroup N] [Module R N] [Module.Flat R N]
    (u : M →ₗ[R] N)
    (hu : Function.Injective ((maximalIdeal R • (⊤ : Submodule R M)).mapQ
      (maximalIdeal R • (⊤ : Submodule R N)) u
      (Submodule.smul_top_le_comap_smul_top (maximalIdeal R) u))) :
    ∀ (Q : Type v) [AddCommGroup Q] [Module R Q], Function.Injective (u.rTensor Q)
Tag 05FR, a lemma

Tag 05FR in the Stacks Project.

Stacks.UniversalInjectivity.universallyInjective_lsmul_of_mem_nonZeroSMulDivisors_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/UniversalInjectivity.lean, line 54. The attribute's comment: “elementwise_universal_injectivity”.

Stacks Project, Tag 05FR. An element which acts injectively on the closed fibre of a projective module acts universally injectively on the module over the local base ring.

theorem universallyInjective_lsmul_of_mem_nonZeroSMulDivisors_quotient
    {R : Type u} {S : Type v} {N : Type w}
    [CommRing R] [CommRing S] [IsLocalRing R] [Algebra R S]
    [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [IsNoetherianRing
      (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))]
    [Module.Finite
      (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
      (N ⧸ (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) •
        (⊤ : Submodule S N)))]
    [Module.Projective R N]
    {s : S}
    (hs : s ∈ nonZeroSMulDivisors S
      (N ⧸ (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) •
        (⊤ : Submodule S N)))) :
    UniversallyInjective ((LinearMap.lsmul S N s).restrictScalars R)

Stacks.UniversalInjectivity.universallyInjective_localizedModule_mkLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/UniversalInjectivity.lean, line 103. The attribute's comment: “localization_universal_injectivity”.

Stacks Project, Tag 05FR. If a module is projective over a local base ring, its canonical map to the localization at the elements acting injectively on its closed fibre is universally injective over the base.

theorem universallyInjective_localizedModule_mkLinearMap
    {R : Type u} {S : Type v} {N : Type (max v w)} [CommRing R] [CommRing S] [IsLocalRing R]
    [Algebra R S] [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Projective R N]
    [IsNoetherianRing
      (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))]
    [Module.Finite
      (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
      (N ⧸ (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) •
        (⊤ : Submodule S N)))] :
    UniversallyInjective
      ((LocalizedModule.mkLinearMap
        (nonZeroSMulDivisors S
          (N ⧸ (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) •
            (⊤ : Submodule S N)))) N).restrictScalars R)
Sources
LeanStacks.UniversalInjectivity.finite_maximalSpectrum_localization_nonZeroSMulDivisors · Stacks.UniversalInjectivity.range_under_localization_nonZeroSMulDivisors · Stacks.UniversalInjectivity.exists_assStacks_closedFibre_of_isMaximal_localization · Stacks.UniversalInjectivity.universallyInjectivePoly_lsmul_of_nonZeroSMulDivisors · Stacks.UniversalInjectivity.universallyInjectivePoly_mkLinearMap_nonZeroSMulDivisors · Stacks.UniversalInjectivity.universallyInjectivePoly_tensorUnit_of_flat · Stacks.UniversalInjectivity.universallyInjective_baseChange_of_flat · Module.Flat.rTensor_injective_of_projective_of_mem_maximalIdeal_smul_top

Section38.8 Completion and Mittag-Leffler modules#

Section 38.8 of the Stacks Project, Tag 05DI. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05DJ, a lemma

Tag 05DJ in the Stacks Project.

AdicCompletion.isMittagLeffler_finsupp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveCompletedDirectSum.lean, line 186. The attribute's comment: “the Mittag-Leffler property; the direct sum ⊕_{α ∈ A} R is spelled A →₀ R. Mittag-Leffler is IsMittagLeffler, condition (1) of 059E, as in 059N and 059X.”.

Stacks Project, Tag 05DJ. If R is Noetherian and I-adically complete, then the I-adic completion of the direct sum of an A-indexed family of copies of R is a Mittag-Leffler R-module.

theorem isMittagLeffler_finsupp {R : Type uR} [CommRing R] (I : Ideal R) [IsNoetherianRing R]
    [IsAdicComplete I R] (A : Type uA) :
    IsMittagLeffler.{uR, uP, max uR uA, max uR uP, uN} R (AdicCompletion I (A →₀ R))

Declarations registered for the tag:

Tag 05DK, a lemma

Tag 05DK in the Stacks Project.

AdicCompletion.flat_of_projective_quotient_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveQuotientAdicCompletion.lean, line 112. The attribute's comment: “flatness; M/IM is M ⧸ I • ⊤. The source's hypothesis that R be I-adically complete is dropped: it is unused, neither Tag 05D3 nor Tag 06LE needing it, so this is strictly more general than the source's statement.”. References: SGA 1 IV (3.1).

Stacks Project, Tag 05DK. If R is Noetherian, M is flat and M/IM is projective over R/I, then the I-adic completion of M is flat over R. The source's hypothesis that R be I-adically complete is not needed for this half.

theorem flat_of_projective_quotient_smul_top [IsNoetherianRing R]
    [Module.Flat R M] (hM : Module.Projective (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))) :
    Module.Flat R (AdicCompletion I M)

AdicCompletion.isMittagLeffler_of_projective_quotient_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveQuotientAdicCompletion.lean, line 129. The attribute's comment: “the Mittag-Leffler property; M/IM is M ⧸ I • ⊤, and Mittag-Leffler is IsMittagLeffler, condition (1) of 059E, as in 059N and 05DJ.”.

Stacks Project, Tag 05DK. If R is Noetherian and I-adically complete, M is flat and M/IM is projective over R/I, then the I-adic completion of M is a Mittag-Leffler R-module.

theorem isMittagLeffler_of_projective_quotient_smul_top [IsNoetherianRing R] [IsAdicComplete I R]
    [Module.Flat R M] (hM : Module.Projective (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))) :
    IsMittagLeffler.{u, uP, v, max u uP, uN} R (AdicCompletion I M)
Tag 05DL, a lemma

Tag 05DL in the Stacks Project.

AdicCompletion.universallyInjective_of_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveAdicCompletionInjectivity.lean, line 227. The attribute's comment: “IS is I.map (algebraMap R S) and IS + 𝔮 is a supremum of ideals; associatedness is IsAssociatedPrimeStacks, the source's definition; the tensor product is written N ⊗[R] Q, with N on the left, so that it carries its standard S-module structure. The source's hypothesis that R be Noetherian is dropped: the argument runs entirely over S, using Tag 00IQ and Tag 0311 there, so this is strictly more general than the source's statement.”.

Stacks Project, Tag 05DL. Let R → S be a map of Noetherian rings, let I ⊆ R be an ideal and let N be a finite S-module. If for every finite R-module Q and every associated prime q of N ⊗[R] Q the ideal IS + q is proper, then the canonical map from N to its I-adic completion is universally injective as a map of R-modules.

theorem universallyInjective_of_associatedPrimes {R : Type u} [CommRing R] (I : Ideal R)
    {S : Type v} [CommRing S] [Algebra R S] {N : Type w} [AddCommGroup N] [Module R N]
    [Module S N] [IsScalarTower R S N] [IsNoetherianRing S] [Module.Finite S N]
    (h : ∀ (Q : Type w) [AddCommGroup Q] [Module R Q] [Module.Finite R Q] (q : Ideal S),
      IsAssociatedPrimeStacks S (N ⊗[R] Q) q → I.map (algebraMap R S) ⊔ q ≠ ⊤) :
    UniversallyInjective (AdicCompletion.of I N)
Tag 05DM, a lemma

Tag 05DM in the Stacks Project.

AdicCompletion.universallyInjective_of_flat_of_fibre_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveAdicCompletionInjectivity.lean, line 303. The attribute's comment: “IS is I.map (algebraMap R S) and IS + 𝔮 is a supremum of ideals; the contraction 𝔭 = R ∩ 𝔮 is PrimeSpectrum.comap (algebraMap R S) 𝔮, and κ(𝔭) is its ResidueField; the tensor product is written N ⊗[R] κ(𝔭), with N on the left, so that it carries its standard S-module structure.”.

Stacks Project, Tag 05DM. Let R → S be a map of Noetherian rings, let I ⊆ R be an ideal and let N be a finite S-module which is flat over R. If for every prime 𝔮 of S which is an associated prime of the fibre N ⊗[R] κ(𝔭), where 𝔭 = R ∩ 𝔮, the ideal IS + 𝔮 is proper, then the canonical map from N to its I-adic completion is universally injective as a map of R-modules.

theorem universallyInjective_of_flat_of_fibre_associatedPrimes {R : Type u} {S : Type v}
    [CommRing R] [CommRing S] [Algebra R S] (I : Ideal R) (N : Type w) [AddCommGroup N]
    [Module S N] [Module R N] [IsScalarTower R S N] [IsNoetherianRing R] [IsNoetherianRing S]
    [Module.Finite S N] [Module.Flat R N]
    (h : ∀ q : PrimeSpectrum S, q.asIdeal ∈ associatedPrimes S
        (N ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField) →
      I.map (algebraMap R S) ⊔ q.asIdeal ≠ ⊤) :
    UniversallyInjective (AdicCompletion.of I N)
Sources
LeanAdicCompletion.isMittagLeffler_finsupp · AdicCompletion.flat_directSum · AdicCompletion.flat_of_projective_quotient_smul_top · AdicCompletion.isMittagLeffler_of_projective_quotient_smul_top · AdicCompletion.universallyInjective_of_associatedPrimes · AdicCompletion.universallyInjective_of_flat_of_fibre_associatedPrimes

Section38.9 Projective modules#

Section 38.9 of the Stacks Project, Tag 05DN. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05DP, a lemma

Tag 05DP in the Stacks Project.

Module.projective_of_flat_of_projective_quotient_of_associatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveOfFlatOverComplete.lean, line 87. The attribute's comment: “N/IN is N ⧸ I • ⊤; the contraction 𝔭 = R ∩ 𝔮 is PrimeSpectrum.comap (algebraMap R S) 𝔮 and κ(𝔭) its ResidueField; the condition IS + 𝔮 ≠ S is the join of ideals being different from ⊤.”.

Stacks Project, Tag 05DP. Let R be a Noetherian ring, I-adically complete, let S be a finite type R-algebra and let N be a finite S-module which is flat over R. If N/IN is projective over R/I and IS + 𝔮 ≠ S for every prime 𝔮 of S which is an associated prime of the fibre N ⊗[R] κ(𝔭) with 𝔭 = R ∩ 𝔮, then N is projective as an R-module.

theorem projective_of_flat_of_projective_quotient_of_associatedPrimes (R : Type u) (S : Type v)
    [CommRing R] [CommRing S] [Algebra R S] (I : Ideal R) (N : Type w) [AddCommGroup N]
    [Module S N] [Module R N] [IsScalarTower R S N] [IsNoetherianRing R] [IsAdicComplete I R]
    [Algebra.FiniteType R S] [Module.Finite S N] [Module.Flat R N]
    (hprojective : Module.Projective (R ⧸ I) (N ⧸ I • (⊤ : Submodule R N)))
    (hassociated : ∀ q : PrimeSpectrum S, q.asIdeal ∈ associatedPrimes S
        (N ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField) →
      I.map (algebraMap R S) ⊔ q.asIdeal ≠ ⊤) :
    Module.Projective R N
Tag 05FS, a lemma

Tag 05FS in the Stacks Project.

Module.Flat.projective_of_finiteType_of_geometricallyIntegral_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ProjectiveOfIntegralFibres.lean, line 207.

Stacks Project, Tag 05FS. A flat finite type algebra over a Noetherian ring whose fibres are geometrically integral is projective as a module over its base ring.

theorem Module.Flat.projective_of_finiteType_of_geometricallyIntegral_fibres
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [Algebra.FiniteType R S] [Module.Flat R S]
    (h : ∀ (p : Ideal R) [p.IsPrime],
      letI : Algebra p.ResidueField (S ⊗[R] p.ResidueField) :=
        Algebra.TensorProduct.rightAlgebra
      Algebra.IsGeometricallyIntegral p.ResidueField (S ⊗[R] p.ResidueField)) :
    Module.Projective R S
Tag 05FT, a lemma

Tag 05FT in the Stacks Project.

Algebra.projective_of_geometricallyIntegral_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/ReducedFibreFromSmoothLocus.lean, line 188.

Stacks Project, Tag 05FT. Let R → S be flat and of finite presentation and suppose that every fibre ring S ⊗[R] κ(p) is geometrically integral over κ(p). Then S is a projective R-module.

This is Algebra.projective_of_geometricallyIntegral_fibres_of_isConstructible_reduced with its hypothesis — constructibility of the geometrically reduced fibre locus over a Noetherian base, the affine case of Stacks 0579 — discharged by Algebra.isConstructible_geometricallyReducedFibreLocus'. The irreducible half was discharged by Algebra.isConstructible_geometricallyIrreducibleFibreLocus_of_finiteType, the affine case of the level set n = 1 of Stacks 055B.

public theorem projective_of_geometricallyIntegral_fibres {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FinitePresentation R S] [Module.Flat R S]
    (h : ∀ (p : Ideal R) [p.IsPrime],
      letI : Algebra p.ResidueField (S ⊗[R] p.ResidueField) :=
        Algebra.TensorProduct.rightAlgebra
      Algebra.IsGeometricallyIntegral p.ResidueField (S ⊗[R] p.ResidueField)) :
    Module.Projective R S
Sources
LeanModule.projective_of_flat_of_projective_quotient_of_associatedPrimes · Module.Flat.projective_of_finiteType_of_geometricallyIntegral_fibres · Algebra.projective_of_geometricallyIntegral_fibres

Section38.10 Flat finite type modules, Part I#

Section 38.10 of the Stacks Project, Tag 05I2. 10 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05I3, a lemma

Tag 05I3 in the Stacks Project.

Algebra.closedFiberIdeal_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/CompleteDevissageStep.lean, line 92. The attribute's comment: “the generic point of the closed fibre”.

Stacks Project, Tag 05I3, the generic point of the closed fibre. If the fibres of Spec S ⟶ Spec R are geometrically integral, the ideal extending the maximal ideal of the local ring R is prime.

public theorem Algebra.closedFiberIdeal_isPrime
    (R : Type u) (S : Type u) [CommRing R] [CommRing S] [IsLocalRing R] [Algebra R S]
    [GeometricallyIntegral (Spec.map (CommRingCat.ofHom (algebraMap R S)))] :
    (Algebra.closedFiberIdeal R S).IsPrime

Module.freeMapAtResidueField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/CompleteDevissageStep.lean, line 112. The attribute's comment: “construction of the free map”.

Stacks Project, Tag 05I3, construction of the free map. For a finite module and a prime ideal p, some map from a finite free module becomes an isomorphism after tensoring with the residue field at p.

public noncomputable def Module.freeMapAtResidueField
    (S : Type u) [CommRing S] (p : Ideal S) [p.IsPrime]
    (N : Type v) [AddCommGroup N] [Module S N] [Module.Finite S N] :
    Σ r : ℕ, { alpha : (Fin r → S) →ₗ[S] N //
      Function.Bijective (alpha.rTensor p.ResidueField) }

Module.flat_localizedModule_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageFlatTfae.lean, line 193. The attribute's comment: “the five equivalent conditions”.

Stacks Project, Tag 05I3, the five equivalent conditions, with the universe of the module independent of that of the base ring and the algebra.

Every hypothesis of the source is present and no others: R is local, R → S is flat of finite presentation with geometrically integral fibres, q lies over the maximal ideal, N is a finite S-module and alpha becomes an isomorphism over the residue field of 𝔪S. Projectivity of S over R, which the source invokes to run the argument, is Stacks 05FT (Algebra.projective_of_geometricallyIntegral_fibres) applied to the geometrically integral fibres.

public theorem flat_localizedModule_tfae
    (R : Type u) (S : Type u) [CommRing R] [CommRing S] [IsLocalRing R] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    [AlgebraicGeometry.GeometricallyIntegral
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))]
    [(Algebra.closedFiberIdeal R S).IsPrime]
    (q : Ideal S) [q.IsPrime]
    (hq : q.comap (algebraMap R S) = IsLocalRing.maximalIdeal R)
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Finite S N]
    (r : ℕ) (alpha : (Fin r → S) →ₗ[S] N)
    (halpha : Function.Bijective (alpha.rTensor (Algebra.closedFiberIdeal R S).ResidueField)) :
    List.TFAE [
      Module.Flat R (LocalizedModule q.primeCompl N),
      Stacks.UniversalInjectivity.LocalizationCriteria.UniversallyInjective.{max u w}
        (alpha.restrictScalars R) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Injective alpha ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Bijective
          (LocalizedModule.map (Algebra.closedFiberIdeal R S).primeCompl alpha) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Injective (LocalizedModule.map q.primeCompl alpha) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha))]
Tag 05I4, a lemma

Tag 05I4 in the Stacks Project.

Module.CompleteDevissageAt.finitePresentation_free_linearEquiv_directSum_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageProjectiveStages.lean, line 441.

Stacks Project, Tag 05I4. Let (R, 𝔪) be a local ring, let R → S be a ring map of finite presentation, let N be a finite S-module and let q be a prime of S lying over 𝔪. Assume that N_q is flat over R and that D is a complete dévissage of N/S/R at q. Then N is a finitely presented S-module, free as an R-module, and there is an isomorphism of R-modules N ≅ B₁^{⊕ r₁} ⊕ … ⊕ Bₙ^{⊕ rₙ}, where B₁, …, Bₙ are the lower algebras of D and each Bᵢ is a smooth R-algebra with geometrically irreducible fibres.

public theorem finitePresentation_free_linearEquiv_directSum_of_flat [IsLocalRing R] [Module R N]
    [IsScalarTower R S N] [Algebra.FinitePresentation R S]
    (D : CompleteDevissageAt R S N q) (hq : q.under R = IsLocalRing.maximalIdeal R)
    (hflat : Module.Flat R (LocalizedModule q.primeCompl N)) :
    Module.FinitePresentation S N ∧ Module.Free R N ∧
      (∀ i : Fin D.length, Algebra.Smooth R (D.lowerAlgebra i) ∧
        GeometricallyIrreducible
          (Spec.map (CommRingCat.ofHom (algebraMap R (D.lowerAlgebra i))))) ∧
      Nonempty (N ≃ₗ[R] ⨁ i : Fin D.length, (Fin (D.multiplicity i) →₀ D.lowerAlgebra i))
Tag 05I5, a proposition

Tag 05I5 in the Stacks Project.

AlgebraicGeometry.existsElementaryEtaleNeighborhoodFinitePresentationFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhoodFlatness.lean, line 392.

Stacks Project, Tag 05I5. For f locally of finite presentation and F quasi-coherent of finite type and flat over S at x, there is an elementary étale neighbourhood (S', s') of (S, f x) and an open subscheme of X ×_S Spec 𝒪_{S', s'} containing the unique point over x on which the pullback of F is of finite presentation and flat over 𝒪_{S', s'}.

Here U is the elementary étale neighbourhood (S', s'), the base change is along the composite Spec 𝒪_{S', s'} ⟶ S' ⟶ S, V is the open subscheme and v the point of V over x; the first clause says that v is the only point of X ×_S Spec 𝒪_{S', s'} over x. Its type is the body of AlgebraicGeometry.ExistsElementaryEtaleNeighborhoodFinitePresentationFlatOver, written out.

The pointwise form above composed with AlgebraicGeometry.ExistsElementaryEtaleNeighborhoodFinitePresentationFlatOver.of_mem, which supplies the uniqueness of the point over x.

theorem existsElementaryEtaleNeighborhoodFinitePresentationFlatOver
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f] (F : X.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] (x : X)
    (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : EtaleNeighborhood S (f x)) (_ : U.IsElementary)
      (V : (pullback f (U.scheme.fromSpecStalk U.point ≫ U.toBase)).Opens) (v : V),
      (pullback.fst f (U.scheme.fromSpecStalk U.point ≫ U.toBase) ⁻¹' {x} = {V.ι v}) ∧
      ((Scheme.Modules.pullback
        (V.ι ≫ pullback.fst f (U.scheme.fromSpecStalk U.point ≫ U.toBase))).obj
          F).IsFinitePresentation ∧
      IsFlatOver
        (LocallyRingedSpace.forgetToSheafedSpace.map
          (V.ι ≫ pullback.snd f (U.scheme.fromSpecStalk U.point ≫ U.toBase)).toLRSHom)
        ((Scheme.Modules.pullback
          (V.ι ≫ pullback.fst f (U.scheme.fromSpecStalk U.point ≫ U.toBase))).obj F)
Tag 05M9, a lemma

Tag 05M9 in the Stacks Project.

AlgebraicGeometry.isOpen_isFlatOverAt_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FlatFiniteTypeModules.lean, line 340. The attribute's comment: “for f locally of finite presentation”.

Stacks Project, Tag 05M9 for a morphism locally of finite presentation: in every fibre of f, the locus where a finite type quasi-coherent 𝒪_X-module is flat over the base is open.

The source states this for f locally of finite type, and deduces it from Tag 05I5, which assumes locally of finite presentation. For f only locally of finite type the same argument needs Tag 05KT in place of Tag 05I5; that deduction is AlgebraicGeometry.isOpen_isFlatOverAt_fiber_of_exists.

theorem isOpen_isFlatOverAt_fiber {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFinitePresentation f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (s : S) :
    IsOpen {w : f.fiber s | IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s w)}

AlgebraicGeometry.isOpen_isFlatOverAt_fiber_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FlatFiniteTypeNeighborhood.lean, line 382.

In every fibre of a morphism locally of finite type, the locus where a quasi-coherent module of finite type is flat over the base is open.

theorem isOpen_isFlatOverAt_fiber_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (s : S) :
    IsOpen {w : f.fiber s | IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s w)}
Tag 05KT, a lemma

Tag 05KT in the Stacks Project.

AlgebraicGeometry.ElementaryEtaleFlatness.exists_elementaryEtaleNeighborhood_open_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FlatnessAtPoint.lean, line 71.

Stacks Project, Tag 05KT. Flatness at a point of a finite type quasi-coherent module spreads to an open neighbourhood after base change to the local scheme of a suitable elementary étale neighbourhood of the image point.

theorem exists_elementaryEtaleNeighborhood_open_flat
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (x : X)
    (hF : AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : AlgebraicGeometry.EtaleNeighborhood S (f x)) (_ : U.IsElementary),
      let g := U.scheme.fromSpecStalk U.point ≫ U.toBase
      let P : Scheme.{u} := pullback f g
      ∃ (z : P) (_ : pullback.fst f g z = x)
      (_ : ∀ z' : P, pullback.fst f g z' = x → z' = z) (V : P.Opens),
      z ∈ V ∧
        AlgebraicGeometry.IsFlatOver
          (((V.ι : V.toScheme ⟶ P) ≫ pullback.snd f g).toLRSHom.toShHom)
          ((Scheme.Modules.pullback
            ((V.ι : V.toScheme ⟶ P) ≫ pullback.fst f g)).obj F)

AlgebraicGeometry.existsElementaryEtaleNeighborhoodFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FlatFiniteTypeNeighborhood.lean, line 372.

For a morphism f : X ⟶ S locally of finite type and a quasi-coherent 𝒪_X-module F of finite type which is flat over S at x, there is an elementary étale neighbourhood (S', s') of (S, f x) and an open subscheme of X ×_S Spec 𝒪_{S', s'} containing the unique point over x on which the pullback of F is flat over 𝒪_{S', s'}.

theorem existsElementaryEtaleNeighborhoodFlatOver :
    ExistsElementaryEtaleNeighborhoodFlatOver.{u}
Tag 05KU, a lemma

Tag 05KU in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_isFinitePresentation_isFlatOver_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FlatOverFibre.lean, line 330.

Stacks Project, Tag 05KU. Let f : X ⟶ S be of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite type, and let s be a point of S such that F is flat over S at every point of the fibre X_s. Then there are an elementary étale neighbourhood (S', s') of (S, s) and an open V ⊆ X ×_S Spec 𝒪_{S', s'} containing the whole fibre X_s = X ×_S s' such that the pullback of F to V is of finite presentation as an 𝒪_V-module and flat over 𝒪_{S', s'}.

The fibre X ×_S s' is read as the set of points of X ×_S Spec 𝒪_{S', s'} whose image in X lies over s.

theorem exists_elementaryEtaleNeighborhood_isFinitePresentation_isFlatOver_fiber
    {X S : Scheme.{u}} (f : X ⟶ S) (hf : FinitePresentation f) (F : X.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] (s : S)
    (hflat : ∀ x : X, f x = s → IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
      (V : (pullback f (U.scheme.fromSpecStalk U.point ≫ U.toBase)).Opens),
      (∀ z : ↑(pullback f (U.scheme.fromSpecStalk U.point ≫ U.toBase)),
          f (pullback.fst f (U.scheme.fromSpecStalk U.point ≫ U.toBase) z) = s → z ∈ V) ∧
      ((Scheme.Modules.pullback (V.ι ≫ pullback.fst f
          (U.scheme.fromSpecStalk U.point ≫ U.toBase))).obj F).IsFinitePresentation ∧
      IsFlatOver
        (V.ι ≫ pullback.snd f
          (U.scheme.fromSpecStalk U.point ≫ U.toBase)).toLRSHom.toShHom
        ((Scheme.Modules.pullback (V.ι ≫ pullback.fst f
          (U.scheme.fromSpecStalk U.point ≫ U.toBase))).obj F)
Tag 05KV, a lemma

Tag 05KV in the Stacks Project.

AlgebraicGeometry.ElementaryEtaleFlatness.exists_elementaryEtaleNeighborhood_open_flat_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FlatnessAlongFibre.lean, line 528.

Stacks Project, Tag 05KV. Flatness of a finite type quasi-coherent module along a fibre spreads to an open neighbourhood of that fibre after passing to the local scheme of an elementary étale neighbourhood of the base point.

theorem exists_elementaryEtaleNeighborhood_open_flat_along_fibre
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (s : S)
    (hF : ∀ x : X, f x = s → AlgebraicGeometry.IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : AlgebraicGeometry.EtaleNeighborhood S s) (_ : U.IsElementary),
      let g := U.scheme.fromSpecStalk U.point ≫ U.toBase
      let P : Scheme.{u} := pullback f g
      ∃ (V : P.Opens),
        (∀ z : P, pullback.snd f g z = IsLocalRing.closedPoint _ → z ∈ V) ∧
          AlgebraicGeometry.IsFlatOver
            (((V.ι : V.toScheme ⟶ P) ≫ pullback.snd f g).toLRSHom.toShHom)
            ((Scheme.Modules.pullback
              ((V.ι : V.toScheme ⟶ P) ≫ pullback.fst f g)).obj F)
Tag 05I6, a lemma

Tag 05I6 in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_flat_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FlatFiniteTypeSchemeNeighborhood.lean, line 236.

Stacks Project, Tag 05I6. Let X be locally of finite type over S and let x ∈ X be a point at which X is flat over S. Then there is an elementary étale neighbourhood (S', s') of (S, f x) and an open subscheme of X ×_S Spec 𝒪_{S', s'} containing the unique point over x which is flat and of finite presentation over Spec 𝒪_{S', s'}.

theorem exists_elementaryEtaleNeighborhood_flat_finitePresentation {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] (x : X) (hflat : IsFlatAt f.toLRSHom.toShHom x) :
    ∃ (U : EtaleNeighborhood S (f x)) (_ : U.IsElementary),
      let b : Spec (U.scheme.presheaf.stalk U.point) ⟶ S :=
        U.scheme.fromSpecStalk U.point ≫ U.toBase
      ∃ (V : (pullback f b).Opens) (v : V),
        (pullback.fst f b ⁻¹' {x} = {V.ι v}) ∧
        Flat (V.ι ≫ pullback.snd f b) ∧
        FinitePresentation (V.ι ≫ pullback.snd f b)
Tag 05I7, a lemma

Tag 05I7 in the Stacks Project.

Stacks.Flatness.finitePresentation_stalk_of_isFlatOverAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/StalkFinitePresentation.lean, line 86.

Stacks Project, Tag 05I7, from Stacks Project, Tag 05I5. Let f : X ⟶ S be locally of finite presentation and let F be a finite type quasi-coherent 𝒪_X-module. If F is flat over S at x, then the stalk F_x is a finitely presented 𝒪_{X,x}-module.

Stacks 05I5 is AlgebraicGeometry.existsElementaryEtaleNeighborhoodFinitePresentationFlatOver. The neighbourhood it produces maps to X by a flat morphism, the pullback of F to it is finitely presented, so its stalk is finitely presented (Stacks.StalkFiniteType.finitePresentation_stalk), and finite presentation descends along the flat local homomorphism of local rings that the stalk map is (Stacks.StalkFiniteType.finitePresentation_stalk_of_flat).

theorem finitePresentation_stalk_of_isFlatOverAt
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f] (F : X.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] (x : X)
    (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    Module.FinitePresentation (ToType (X.presheaf.stalk x))
      (ToType (TopCat.Presheaf.stalk F.val.presheaf x))
Tag 05I8, a lemma

Tag 05I8 in the Stacks Project.

AlgebraicGeometry.isEssentiallyOfFinitePresentation_stalkMap_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/StalkEssentiallyFinitePresentation.lean, line 151.

Stacks Project, Tag 05I8. If f : X ⟶ S is locally of finite type and flat at x, then the local ring 𝒪_{X,x} is essentially of finite presentation over 𝒪_{S,f x}.

theorem isEssentiallyOfFinitePresentation_stalkMap_of_flatAt
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) (hflat : AlgebraicGeometry.IsFlatAt f.toLRSHom.toShHom x) :
    IsEssentiallyOfFinitePresentation
      (S.presheaf.stalk (f x)) (X.presheaf.stalk x) (f.stalkMap x).hom
Sources
LeanAlgebra.closedFiberIdeal_isPrime · Module.freeMapAtResidueField · Module.flat_localizedModule_tfae · Module.CompleteDevissageAt.finitePresentation_free_linearEquiv_directSum_of_flat · AlgebraicGeometry.existsElementaryEtaleNeighborhoodFinitePresentationFlatOver · AlgebraicGeometry.isOpen_isFlatOverAt_fiber · AlgebraicGeometry.isOpen_isFlatOverAt_fiber_of_locallyOfFiniteType · AlgebraicGeometry.ElementaryEtaleFlatness.exists_elementaryEtaleNeighborhood_open_flat

Section38.11 Extending properties from an open#

Section 38.11 of the Stacks Project, Tag 0B47. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 081N, a lemma

Tag 081N in the Stacks Project.

AlgebraicGeometry.FinitePresentationFromDenseOpen.isFinitePresentation_of_isFlatOver_of_retrocompact_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FinitePresentationFromDenseOpen.lean, line 710.

Stacks Project, Tag 081N. A quasi-coherent module of finite type, flat over the base, which is finitely presented over the inverse image of a retrocompact scheme-theoretically dense open of the base is finitely presented.

public theorem isFinitePresentation_of_isFlatOver_of_retrocompact_dense_open
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) [F.IsQuasicoherent]
    [LocallyOfFinitePresentation f] [F.IsFiniteType]
    (hflat : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F)
    (U : S.Opens) (hUretro : IsRetrocompact (U : Set S))
    (hUdense : AlgebraicGeometry.Scheme.Opens.IsSchemeTheoreticallyDense U)
    (hfp : ((Scheme.Modules.pullback (f ⁻¹ᵁ U).ι).obj F).IsFinitePresentation) :
    F.IsFinitePresentation
Tag 081P, a lemma

Tag 081P in the Stacks Project.

AlgebraicGeometry.FinitePresentationFromDenseOpen.locallyOfFinitePresentation_of_flat_of_retrocompact_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/FinitePresentationFromDenseOpen.lean, line 861.

Stacks Project, Tag 081P. A flat morphism of schemes which is locally of finite type, and which is locally of finite presentation over a retrocompact scheme-theoretically dense open of the target, is locally of finite presentation.

public theorem locallyOfFinitePresentation_of_flat_of_retrocompact_dense_open
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [Flat f]
    (U : S.Opens) (hUretro : IsRetrocompact (U : Set S))
    (hUdense : Scheme.Opens.IsSchemeTheoreticallyDense U)
    [LocallyOfFinitePresentation (f ∣_ U)] :
    LocallyOfFinitePresentation f
Tag 081L, a lemma

Tag 081L in the Stacks Project.

AlgebraicGeometry.relativeDimensionLE_of_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ExtendingFromOpen/RelativeDimension.lean, line 220.

Stacks Project, Tag 081L. A relative-dimension bound for a flat morphism locally of finite type extends from a dense open of the base when the morphism is locally of finite presentation or the open is retrocompact.

theorem relativeDimensionLE_of_dense_open {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFiniteType f] (U : S.Opens) (hU : Dense (U : Set S)) (e : ℕ)
    (hfe : RelativeDimensionLE (pullback.snd f U.ι) e)
    (hfin : LocallyOfFinitePresentation f ∨ IsRetrocompact (U : Set S)) :
    RelativeDimensionLE f e
Tag 0B48, a lemma

Tag 0B48 in the Stacks Project.

AlgebraicGeometry.isFinite_of_isFinite_over_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ExtendingFromOpen/Finite.lean, line 45.

A proper flat morphism which is finite over a dense open of the base is finite, provided it is locally of finite presentation or the open is retrocompact.

theorem isFinite_of_isFinite_over_dense_open {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] (U : S.Opens) (hU : Dense (U : Set S))
    [IsFinite (pullback.snd f U.ι)]
    (hfin : LocallyOfFinitePresentation f ∨ IsRetrocompact (U : Set S)) :
    IsFinite f
Tag 081M, a lemma

Tag 081M in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_of_isIso_morphismRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ExtendingFromOpen/OpenImmersion.lean, line 154.

Stacks Project, Tag 081M. A separated flat morphism locally of finite type which is an isomorphism over a retrocompact scheme-theoretically dense open subscheme of the target is an open immersion.

theorem isOpenImmersion_of_isIso_morphismRestrict {X S : Scheme.{u}} (f : X ⟶ S) [IsSeparated f]
    [LocallyOfFiniteType f] [Flat f] (U : S.Opens) (hUretro : IsRetrocompact (U : Set S))
    (hUdense : Scheme.Opens.IsSchemeTheoreticallyDense U)
    [IsIso (f ∣_ U)] : IsOpenImmersion f
Sources
LeanAlgebraicGeometry.FinitePresentationFromDenseOpen.isFinitePresentation_of_isFlatOver_of_retrocompact_dense_open · AlgebraicGeometry.FinitePresentationFromDenseOpen.locallyOfFinitePresentation_of_flat_of_retrocompact_dense_open · AlgebraicGeometry.relativeDimensionLE_of_dense_open · AlgebraicGeometry.isFinite_of_isFinite_over_dense_open · AlgebraicGeometry.isOpenImmersion_of_isIso_morphismRestrict

Section38.12 Flat finitely presented modules#

Section 38.12 of the Stacks Project, Tag 05I9. 10 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05IA, a lemma

Tag 05IA in the Stacks Project.

Module.exists_freeMap_bijective_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapAtGenericFibre.lean, line 136. The attribute's comment: “existence”.

Stacks Project, Tag 05IA, the existence assertion. Let R → S be flat with a geometrically integral fibre over the prime r, and let N be a finite S-module. Then the extension 𝔭 = rS is prime and some map from a finite free S-module to N becomes an isomorphism after base change to the residue field κ(𝔭).

public theorem Module.exists_freeMap_bijective_residueField {R S N : Type u} [CommRing R]
    [CommRing S] [Algebra R S] [Module.Flat R S] {r : Ideal R} [r.IsPrime] [AddCommGroup N]
    [Module S N] [Module.Finite S N]
    (hgeom : Algebra.IsGeometricallyIntegral r.ResidueField (r.Fiber S)) :
    ∃ (n : ℕ) (a : (Fin n → S) →ₗ[S] N),
      ∃ hp : (r.map (algebraMap R S)).IsPrime,
        Function.Bijective
          (a.rTensor (@Ideal.ResidueField S _ (r.map (algebraMap R S)) hp))

Module.universallyInjective_localizedMap_of_flat_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 656. The attribute's comment: “the implication (1) ⟹ (3), the universal injectivity of α_𝔯 over R_𝔯”.

Let R → S be a flat ring map of finite presentation with geometrically integral fibres, let q ⊆ S be a prime lying over r = q ∩ R, write p = rS for the generic point of the fibre over r, let N be a finite S-module and let alpha : S^{⊕ n} → N become injective over κ(p). If N_q is flat over R then alpha_r : S_r^{⊕ n} → N_r is universally injective as a map of R-modules.

public theorem Module.universallyInjective_localizedMap_of_flat_localizedModule
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))]
    (q : Ideal S) [q.IsPrime]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Finite S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S (q.under R)
      Function.Injective (alpha.rTensor
        (Ideal.map (algebraMap R S) (q.under R)).ResidueField))
    (hflat : Module.Flat R (LocalizedModule q.primeCompl N))
    (Q : Type (max u w)) [AddCommGroup Q] [Module R Q] :
    Function.Injective (((LocalizedModule.map (q.under R).primeCompl
      (alpha.restrictScalars R)).restrictScalars R).rTensor Q)

Module.exists_universallyInjective_localizedModule_away_of_flat_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 757. The attribute's comment: “the first half of the implication (1) ⟹ (2), the universal injectivity of α_f”.

In the situation of Module.universallyInjective_localizedMap_of_flat_localizedModule, with N finitely presented and alpha an isomorphism over κ(p), there is an f ∈ R, f ∉ r, such that alpha_f : S_f^{⊕ n} → N_f is universally injective as a map of R-modules.

public theorem Module.exists_universallyInjective_localizedModule_away_of_flat_localizedModule
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))]
    (r : Ideal R) [r.IsPrime] (q : Ideal S) [q.IsPrime] (hq : q.under R = r)
    (N : Type u) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.FinitePresentation S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
      Function.Bijective (alpha.rTensor (Ideal.map (algebraMap R S) r).ResidueField))
    (hflat : Module.Flat R (LocalizedModule q.primeCompl N)) :
    ∃ f ∈ r.primeCompl, ∀ (Q : Type u) [AddCommGroup Q] [Module R Q],
        Function.Injective (((LocalizedModule.map (Submonoid.powers f)
          (alpha.restrictScalars R)).restrictScalars R).rTensor Q)

Module.flat_localizedModule_coker_of_flat_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 869. The attribute's comment: “the flatness of Coker(α)_𝔮, the second half of conditions (3) to (6)”.

In the situation of Module.universallyInjective_localizedMap_of_flat_localizedModule the localization of Coker(alpha) at q is flat over R.

public theorem Module.flat_localizedModule_coker_of_flat_localizedModule
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))]
    (q : Ideal S) [q.IsPrime]
    (N : Type u) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Finite S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S (q.under R)
      Function.Injective (alpha.rTensor
        (Ideal.map (algebraMap R S) (q.under R)).ResidueField))
    (hflat : Module.Flat R (LocalizedModule q.primeCompl N)) :
    Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha))

Module.exists_universallyInjective_and_flat_coker_of_flat_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 931. The attribute's comment: “the implication (1) ⟹ (2)”.

Let R → S be a flat ring map of finite presentation with geometrically integral fibres, let q ⊆ S be a prime lying over r = q ∩ R, write p = rS, let N be a finitely presented S-module and let alpha : S^{⊕ n} → N be an isomorphism over κ(p). If N_q is flat over R then there are an f ∈ R, f ∉ r, such that alpha_f is universally injective as a map of R-modules, and a g ∈ S, g ∉ q, such that Coker(alpha)_g is flat over R.

public theorem Module.exists_universallyInjective_and_flat_coker_of_flat_localizedModule
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))]
    (q : Ideal S) [q.IsPrime]
    (N : Type u) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.FinitePresentation S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S (q.under R)
      Function.Bijective (alpha.rTensor
        (Ideal.map (algebraMap R S) (q.under R)).ResidueField))
    (hflat : Module.Flat R (LocalizedModule q.primeCompl N)) :
    (∃ f ∈ (q.under R).primeCompl, ∀ (Q : Type u) [AddCommGroup Q] [Module R Q],
        Function.Injective (((LocalizedModule.map (Submonoid.powers f)
          (alpha.restrictScalars R)).restrictScalars R).rTensor Q)) ∧
      ∃ g ∈ q.primeCompl, Module.Flat R (LocalizedModule.Away g (N ⧸ LinearMap.range alpha))

Module.universallyInjective_localizedMap_and_flat_coker_of_exists_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1139. The attribute's comment: “the implication (2) ⟹ (3)”.

If alpha_f is universally injective as a map of R-modules for some f ∈ R, f ∉ r, and Coker(alpha)_g is R-flat for some g ∈ S, g ∉ q, then alpha_r is universally injective as a map of R-modules and Coker(alpha)_q is R-flat. The prime q need not lie over r.

public theorem Module.universallyInjective_localizedMap_and_flat_coker_of_exists_away
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (r : Ideal R) [r.IsPrime]
    (q : Ideal S) [q.IsPrime]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N] (n : ℕ)
    (alpha : (Fin n → S) →ₗ[S] N)
    (h : (∃ f ∈ r.primeCompl, UniversallyInjective.{max u w} (A := R)
            ((LocalizedModule.map (Submonoid.powers f)
              (alpha.restrictScalars R)).restrictScalars R)) ∧
      ∃ g ∈ q.primeCompl,
        Module.Flat R (LocalizedModule.Away g (N ⧸ LinearMap.range alpha))) :
    UniversallyInjective.{max u w} (A := R)
        ((LocalizedModule.map r.primeCompl (alpha.restrictScalars R)).restrictScalars R) ∧
      Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha))

Module.injective_localizedMap_of_universallyInjective_localizedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1168. The attribute's comment: “the implication (3) ⟹ (4), the injectivity of α_𝔯”.

If alpha_r is universally injective as a map of R-modules then it is injective.

public theorem Module.injective_localizedMap_of_universallyInjective_localizedMap
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (r : Ideal R) [r.IsPrime]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N] (n : ℕ)
    (alpha : (Fin n → S) →ₗ[S] N)
    (h : UniversallyInjective.{max u w} (A := R)
      ((LocalizedModule.map r.primeCompl (alpha.restrictScalars R)).restrictScalars R)) :
    Function.Injective (LocalizedModule.map r.primeCompl (alpha.restrictScalars R))

Module.bijective_localizedMap_map_of_injective_localizedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1181. The attribute's comment: “the implication (4) ⟹ (5), the isomorphism α_𝔭”.

If alpha is surjective over κ(p) and alpha_r is injective, then alpha_p is an isomorphism at the generic point p = rS of the fibre over r.

public theorem Module.bijective_localizedMap_map_of_injective_localizedMap (R S : Type u)
    [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))] (r : Ideal R) [r.IsPrime]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Finite S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
      Function.Surjective (alpha.rTensor (Ideal.map (algebraMap R S) r).ResidueField))
    (hinj : Function.Injective (LocalizedModule.map r.primeCompl (alpha.restrictScalars R))) :
    letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
    Function.Bijective
      (LocalizedModule.map (Ideal.map (algebraMap R S) r).primeCompl alpha)

Module.injective_localizedMap_atPrime_of_bijective_localizedMap_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1201. The attribute's comment: “the implication (5) ⟹ (6), the injectivity of α_𝔮”.

If alpha_p is an isomorphism at the generic point p = rS of the fibre over r then alpha_q is injective at every prime q of S lying over r.

public theorem Module.injective_localizedMap_atPrime_of_bijective_localizedMap_map (R S : Type u)
    [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))] (r : Ideal R) [r.IsPrime]
    (q : Ideal S) [q.IsPrime] (hq : q.under R = r)
    (N : Type w) [AddCommGroup N] [Module S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (hbij : letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
      Function.Bijective (LocalizedModule.map (Ideal.map (algebraMap R S) r).primeCompl alpha)) :
    Function.Injective (LocalizedModule.map q.primeCompl alpha)

Module.flat_localizedModule_of_injective_localizedMap_of_flat_coker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1220. The attribute's comment: “the implication (6) ⟹ (1)”.

For S flat over R, if alpha_q is injective and Coker(alpha)_q is R-flat then N_q is R-flat.

public theorem Module.flat_localizedModule_of_injective_localizedMap_of_flat_coker (R S : Type u)
    [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] (q : Ideal S) [q.IsPrime]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N] (n : ℕ)
    (alpha : (Fin n → S) →ₗ[S] N)
    (hinj : Function.Injective (LocalizedModule.map q.primeCompl alpha))
    (hC : Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha))) :
    Module.Flat R (LocalizedModule q.primeCompl N)

Module.flat_localizedModule_freeMap_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FinitelyPresented/FreeMapSpreadingOut.lean, line 1249. The attribute's comment: “the equivalence of the six conditions”.

Let R → S be a finitely presented flat ring map with geometrically integral fibres, let q ⊆ S be a prime lying over r ⊆ R, write p = rS for the generic point of the fibre over r, let N be a finitely presented S-module and let alpha : S^{⊕ n} → N become an isomorphism over κ(p). Then the following six conditions are equivalent:

  1. N_q is R-flat;
  2. there are an f ∈ R, f ∉ r, with alpha_f universally injective over R, and a g ∈ S, g ∉ q, with Coker(alpha)_g R-flat;
  3. alpha_r is universally injective over R and Coker(alpha)_q is R-flat;
  4. alpha_r is injective and Coker(alpha)_q is R-flat;
  5. alpha_p is an isomorphism and Coker(alpha)_q is R-flat;
  6. alpha_q is injective and Coker(alpha)_q is R-flat.
public theorem Module.flat_localizedModule_freeMap_tfae (R S : Type u) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FinitePresentation R S] [Module.Flat R S]
    [GeometricallyIntegral (Spec.map (ofHom (algebraMap R S)))] (r : Ideal R) [r.IsPrime]
    (q : Ideal S) [q.IsPrime] (hq : q.under R = r)
    (N : Type u) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.FinitePresentation S N] (n : ℕ) (alpha : (Fin n → S) →ₗ[S] N)
    (halpha : letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
      Function.Bijective (alpha.rTensor (Ideal.map (algebraMap R S) r).ResidueField)) :
    letI := Ideal.isPrime_map_of_geometricallyIntegral R S r
    List.TFAE [
      Module.Flat R (LocalizedModule q.primeCompl N),
      (∃ f ∈ r.primeCompl, UniversallyInjective.{u} (A := R)
            ((LocalizedModule.map (Submonoid.powers f)
              (alpha.restrictScalars R)).restrictScalars R)) ∧
        ∃ g ∈ q.primeCompl,
          Module.Flat R (LocalizedModule.Away g (N ⧸ LinearMap.range alpha)),
      UniversallyInjective.{u} (A := R)
          ((LocalizedModule.map r.primeCompl (alpha.restrictScalars R)).restrictScalars R) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Injective (LocalizedModule.map r.primeCompl (alpha.restrictScalars R)) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Bijective (LocalizedModule.map (Ideal.map (algebraMap R S) r).primeCompl alpha) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha)),
      Function.Injective (LocalizedModule.map q.primeCompl alpha) ∧
        Module.Flat R (LocalizedModule q.primeCompl (N ⧸ LinearMap.range alpha))]
Tag 05IB, a lemma

Tag 05IB in the Stacks Project.

Module.CompleteDevissage.exists_away_decomposition_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/DevissageAwayGeneralBase.lean, line 239. The attribute's comment: “the decomposition and projectivity, over a general base”.

Stacks Project, Tag 05IB. Let N be a finitely presented module over a finitely presented R-algebra S which is flat over R, and let N/S/R admit a complete dévissage over a prime r of R. Then there is an a ∈ R outside r such that, over R_a, the stage algebras of the dévissage stay smooth with geometrically irreducible fibres, the module N_a is the direct sum of the finite free modules (Bᵢ)_a^{⊕ rᵢ} over them, and N_a is projective.

One and the same a does all of this: it is the element of Module.CompleteDevissage.exists_away_injective_alpha, after inverting which the away-localized dévissage (Module.CompleteDevissage.localizeAwayCanonical) has injective stage maps, so that Module.CompleteDevissage.nonempty_linearEquiv_directSum gives the decomposition and Module.CompleteDevissage.projective_of_injective_alpha the projectivity, the lower algebras being projective over the new base by Stacks 05FT (Module.CompleteDevissage.projective_lowerAlgebra). The smoothness and the fibres are the fields of the away-localized dévissage.

public theorem exists_away_decomposition_projective (D : CompleteDevissage R S N r) :
    ∃ a ∈ r.primeCompl,
      (∀ i, Algebra.Smooth (Localization.Away a) (D.locAwayB a i)) ∧
      (∀ i, GeometricallyIrreducible
        (Spec.map (ofHom (algebraMap (Localization.Away a) (D.locAwayB a i))))) ∧
      Nonempty (LocalizedModule (Submonoid.powers a) N ≃ₗ[Localization.Away a]
        ⨁ i : Fin (D.stepCount + 1), (Fin (D.multiplicity i) →₀ D.locAwayB a i)) ∧
      Module.Projective (Localization.Away a) (LocalizedModule (Submonoid.powers a) N)

Module.CompleteDevissage.nonempty_linearEquiv_directSum_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/EtaleNeighborhoodProjectiveSections.lean, line 223. The attribute's comment: “the decomposition, over a local base”.

The decomposition over a local base. Let R be a local ring, let N be a finite S-module flat over R and let N/S/R have a complete dévissage over the maximal ideal of R. Then N is, as an R-module, the direct sum of the finite free modules Bᵢ^{⊕ rᵢ} over the smooth stage algebras of the dévissage.

public theorem nonempty_linearEquiv_directSum_of_flat [IsLocalRing R] [Module.Flat R N]
    (D : CompleteDevissage R S N r) (hr : r = IsLocalRing.maximalIdeal R) :
    Nonempty (N ≃ₗ[R] ⨁ i : Fin (D.stepCount + 1), (Fin (D.multiplicity i) →₀ D.B i))

Module.CompleteDevissage.projective_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/EtaleNeighborhoodProjectiveSections.lean, line 233. The attribute's comment: “projectivity over a local base”.

Projectivity over a local base. In the situation of Module.CompleteDevissage.nonempty_linearEquiv_directSum_of_flat the module N is projective over R.

public theorem projective_of_flat [IsLocalRing R] [Module.Flat R N]
    (D : CompleteDevissage R S N r) (hr : r = IsLocalRing.maximalIdeal R) :
    Module.Projective R N
Tag 05ID, a proposition

Tag 05ID in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_of_isFlatOverAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/ProjectiveSectionsFlatAtPoint.lean, line 244.

Stacks Project, Tag 05ID. A finitely presented quasi-coherent module which is flat over the base at a point has projective global sections after compatible affine elementary étale localization of the source and of the base.

Openness of the flat locus (Tag 0399) replaces X by the open subscheme on which F is flat over S; Proposition 05HR and Remark 05I0 then produce an affine elementary étale square carrying a complete dévissage of the global sections at the prime of the distinguished point, and Lemma 05IB over a general base makes those sections projective after inverting a global function on the new base which does not vanish at the distinguished point. Shrinking the square to the basic opens of that function and of its pullback gives the square of the conclusion.

theorem exists_elementaryEtaleNeighborhood_projective_sections_of_isFlatOverAt
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (x : X)
    [LocallyOfFinitePresentation f] [F.IsQuasicoherent] [F.IsFinitePresentation]
    (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (V : EtaleNeighborhood S (f x))
      (U : EtaleNeighborhood X x) (h : U.scheme ⟶ V.scheme),
      V.IsElementary ∧ U.IsElementary ∧
        (h ≫ V.toBase = U.toBase ≫ f) ∧ (h U.point = V.point) ∧
        IsAffine U.scheme ∧ IsAffine V.scheme ∧
        (let M := (Scheme.Modules.pullback U.toBase).obj F
         letI : Module Γ(V.scheme, ⊤) Γ(M, ⊤) :=
           Module.compHom Γ(M, ⊤) h.appTop.hom
         Module.Projective Γ(V.scheme, ⊤) Γ(M, ⊤))
Tag 05KW, a lemma

Tag 05KW in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/ProjectiveSectionsAlongFibre.lean, line 619.

Stacks Project, Tag 05KW. Let f : X ⟶ S be of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation and let s ∈ S be such that F is flat over S at every point of the fibre X_s. Then there is an elementary étale neighbourhood (S', s') ⟶ (S, s) and a commutative square whose upper arrow g : X' ⟶ X is étale, with X' and S' affine, with X_s ⊆ g(X'), and with Γ(X', g^*F) a projective Γ(S', 𝒪_{S'})-module.

Tag 05ID enters as AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_of_isFlatOverAt.

theorem exists_elementaryEtaleNeighborhood_projective_sections_along_fibre
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (s : S)
    (hf : FinitePresentation f)
    [F.IsQuasicoherent] [F.IsFinitePresentation]
    (hflat : ∀ x : f.fiber s,
      IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x)) :
    ∃ (U : EtaleNeighborhood S s) (X' : Scheme.{u})
      (h : X' ⟶ U.scheme) (g : X' ⟶ X),
      U.IsElementary ∧ IsAffine U.scheme ∧ IsAffine X' ∧ Etale g ∧
      g ≫ f = h ≫ U.toBase ∧
      f ⁻¹' {s} ⊆ Set.range g ∧
      (let N := Γ((Scheme.Modules.pullback g).obj F, ⊤)
       letI : Module Γ(U.scheme, ⊤) N := Module.compHom N h.appTop.hom
       Module.Projective Γ(U.scheme, ⊤) N)
Tag 05IE, a lemma

Tag 05IE in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_structureSheafSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/StructureSheafProjectiveSections.lean, line 196. The attribute's comment: “the full conclusion; assumes only hdev of Tag 05ID at the structure sheaf”.

Stacks Project, Tag 05IE. Let f : X ⟶ S be locally of finite presentation and let x : X. If f is flat at x over S, then there is a commutative square of pointed schemes 

  (X, x) ←ᵍ (X', x')
    ↓          ↓
  (S, s) ← (S', s')
whose horizontal arrows are elementary étale neighbourhoods, with X' and S' affine, such that Γ(X', 𝒪_{X'}) is a projective Γ(S', 𝒪_{S'})-module.

This is the case ℱ = 𝒪_X of Tag 05ID, as in the source. The flatness hypothesis is converted from the morphism to the structure sheaf by AlgebraicGeometry.isFlatOverAt_unit_iff_isFlatAt, and the conclusion is converted back from Γ(X', g^*𝒪_X) to Γ(X', 𝒪_{X'}) by AlgebraicGeometry.Scheme.Modules.pullbackUnitSectionsLinearEquiv; the finite presentation of 𝒪_X as a module, which Tag 05ID requires of ℱ, is AlgebraicGeometry.Scheme.unitModule_isFinitePresentation.

The hypothesis hdev is the hypothesis of this library's Tag 05ID, AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections, instantiated at the structure sheaf: Proposition 05HR composed with Remark 05I0, carrying the injectivity of the maps α i of Lemma 05IA. Nothing is assumed beyond it — in particular no Noetherian hypothesis, which Tag 05IE does not have. The form without hdev is exists_elementaryEtaleNeighborhood_projective_structureSheafSections_of_isFlatAt.

theorem exists_elementaryEtaleNeighborhood_projective_structureSheafSections
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) [LocallyOfFinitePresentation f]
    (hflat : IsFlatAt (LocallyRingedSpace.forgetToSheafedSpace.map f.toLRSHom) x)
    (hdev : IsFlatOverAt (LocallyRingedSpace.forgetToSheafedSpace.map f.toLRSHom)
        (Scheme.unitModule X) x →
      ∃ (V : EtaleNeighborhood S (f x)) (U : EtaleNeighborhood X x) (h : U.scheme ⟶ V.scheme)
        (_ : V.IsElementary) (_ : U.IsElementary)
        (hover : h ≫ V.toBase = U.toBase ≫ f) (_ : h U.point = V.point)
        (_ : IsAffine U.scheme) (_ : IsAffine V.scheme)
        (r : Ideal Γ(V.scheme, ⊤)) (_ : r.IsPrime),
        letI : (Scheme.unitModule X).IsFiniteType :=
          SheafOfModules.instIsFiniteTypeOfIsFinitePresentation (Scheme.unitModule X)
        letI : Algebra Γ(V.scheme, ⊤) Γ(U.scheme, ⊤) := h.appTop.hom.toAlgebra
        letI : Algebra.FinitePresentation Γ(V.scheme, ⊤) Γ(U.scheme, ⊤) :=
          EtaleNeighborhood.algebraFinitePresentation_globalSections f V U h hover
        letI : Module Γ(V.scheme, ⊤)
            Γ((Scheme.Modules.pullback U.toBase).obj (Scheme.unitModule X), ⊤) :=
          Module.compHom _ h.appTop.hom
        letI : Module.Finite Γ(U.scheme, ⊤)
            Γ((Scheme.Modules.pullback U.toBase).obj (Scheme.unitModule X), ⊤) :=
          EtaleNeighborhood.moduleFinite_pullback_globalSections (Scheme.unitModule X) U
        letI : IsScalarTower Γ(V.scheme, ⊤) Γ(U.scheme, ⊤)
            Γ((Scheme.Modules.pullback U.toBase).obj (Scheme.unitModule X), ⊤) :=
          IsScalarTower.of_algebraMap_smul fun _ _ => rfl
        ∃ D : Module.CompleteDevissage Γ(V.scheme, ⊤) Γ(U.scheme, ⊤)
            Γ((Scheme.Modules.pullback U.toBase).obj (Scheme.unitModule X), ⊤) r,
          ∀ i, letI : Module (D.B i) (D.M i) :=
              Module.compHom (D.M i) (D.toLeft i).toRingHom
            Function.Injective (D.alpha i)) :
    ∃ (V : EtaleNeighborhood S (f x)) (U : EtaleNeighborhood X x) (h : U.scheme ⟶ V.scheme),
      V.IsElementary ∧ U.IsElementary ∧
        (h ≫ V.toBase = U.toBase ≫ f) ∧ (h U.point = V.point) ∧
        IsAffine U.scheme ∧ IsAffine V.scheme ∧
        (letI : Module Γ(V.scheme, ⊤) Γ(U.scheme, ⊤) :=
           Module.compHom Γ(U.scheme, ⊤) h.appTop.hom
         Module.Projective Γ(V.scheme, ⊤) Γ(U.scheme, ⊤))

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_structureSheafSections_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/StructureSheafProjectiveSections.lean, line 266.

Stacks Project, Tag 05IE. Let f : X ⟶ S be locally of finite presentation and let x : X. If f is flat at x over S, then there is a commutative square of pointed schemes 

  (X, x) ←ᵍ (X', x')
    ↓          ↓
  (S, s) ← (S', s')
whose horizontal arrows are elementary étale neighbourhoods, with X' and S' affine, such that Γ(X', 𝒪_{X'}) is a projective Γ(S', 𝒪_{S'})-module.

This is the case ℱ = 𝒪_X of Tag 05ID, as in the source, whose proof of Tag 05IE is the single sentence "This is a special case of Proposition 05ID". The specialisation needs the three identifications of the module docstring: AlgebraicGeometry.Scheme.unitModule X is quasi-coherent and, by AlgebraicGeometry.Scheme.unitModule_isFinitePresentation, of finite presentation, so Tag 05ID applies to it; AlgebraicGeometry.isFlatOverAt_unit_iff_isFlatAt turns flatness of the morphism at x into flatness of the structure sheaf over the base at x; and AlgebraicGeometry.Scheme.Modules.pullbackUnitSectionsLinearEquiv identifies Γ(X', g^*𝒪_X) with Γ(X', 𝒪_{X'}), compatibly with the restriction of scalars along Γ(S', 𝒪_{S'}) ⟶ Γ(X', 𝒪_{X'}) that both sides carry.

Unlike AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_structureSheafSections, this carries no hypothesis beyond the source's: the unconditional form of Tag 05ID, AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_of_isFlatOverAt, is used in place of the conditional AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections, so there is nothing left to assume.

theorem exists_elementaryEtaleNeighborhood_projective_structureSheafSections_of_isFlatAt
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) [LocallyOfFinitePresentation f]
    (hflat : IsFlatAt f.toLRSHom.toShHom x) :
    ∃ (V : EtaleNeighborhood S (f x)) (U : EtaleNeighborhood X x) (h : U.scheme ⟶ V.scheme),
      V.IsElementary ∧ U.IsElementary ∧
        (h ≫ V.toBase = U.toBase ≫ f) ∧ (h U.point = V.point) ∧
        IsAffine U.scheme ∧ IsAffine V.scheme ∧
        (letI : Module Γ(V.scheme, ⊤) Γ(U.scheme, ⊤) :=
           Module.compHom Γ(U.scheme, ⊤) h.appTop.hom
         Module.Projective Γ(V.scheme, ⊤) Γ(U.scheme, ⊤))
Tag 05KX, a lemma

Tag 05KX in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_structureSheafSections_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/StructureSheafProjectiveSectionsAlongFibre.lean, line 102.

Stacks Project, Tag 05KX. Let f : X ⟶ S be of finite presentation and let s : S be a point at which X is flat over S at every point of the fibre X_s. Then there are an elementary étale neighbourhood (S', s') ⟶ (S, s) and a commutative square 

  X  ←ᵍ  X'
  ↓      ↓
  S  ←   S'
with g étale, X_s ⊆ g(X'), with X' and S' affine, and with Γ(X', 𝒪_{X'}) a projective Γ(S', 𝒪_{S'})-module.

This is the case ℱ = 𝒪_X of Tag 05KW, as in the source. The flatness hypothesis is converted from the morphism to the structure sheaf by AlgebraicGeometry.isFlatOverAt_unit_iff_isFlatAt, and the conclusion is converted back from Γ(X', g^*𝒪_X) to Γ(X', 𝒪_{X'}) by AlgebraicGeometry.Scheme.Modules.pullbackUnitSectionsLinearEquiv; the finite presentation of 𝒪_X as a module, which Tag 05KW requires of ℱ, is AlgebraicGeometry.Scheme.unitModule_isFinitePresentation. Tag 05KW enters as AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_along_fibre, which is unconditional, so nothing is assumed here beyond the source's hypotheses.

theorem exists_elementaryEtaleNeighborhood_projective_structureSheafSections_along_fibre
    {X S : Scheme.{u}} (f : X ⟶ S) (s : S) (hf : FinitePresentation f)
    (hflat : ∀ x : f.fiber s, IsFlatAt f.toLRSHom.toShHom (f.fiberι s x)) :
    ∃ (U : EtaleNeighborhood S s) (X' : Scheme.{u})
      (h : X' ⟶ U.scheme) (g : X' ⟶ X),
      U.IsElementary ∧ IsAffine U.scheme ∧ IsAffine X' ∧ Etale g ∧
      g ≫ f = h ≫ U.toBase ∧
      f ⁻¹' {s} ⊆ Set.range g ∧
      (letI : Module Γ(U.scheme, ⊤) Γ(X', ⊤) := Module.compHom Γ(X', ⊤) h.appTop.hom
       Module.Projective Γ(U.scheme, ⊤) Γ(X', ⊤))
Tag 05KY, a lemma

Tag 05KY in the Stacks Project.

AlgebraicGeometry.exists_etale_neighborhood_with_free_globalSections_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSectionsFromFiniteTypeFlatness.lean, line 652.

Stacks Project, Tag 05KY. Let f : X ⟶ S be locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite type and let x ∈ X be a point at which F is flat over S. Then there is an elementary étale neighbourhood (S', s') ⟶ (S, s) of the image s of x and a commutative diagram of pointed schemes 

  (X, x) ← (X', x')
    ↓         ↓
  (S, s) ← Spec 𝒪_{S', s'}
such that X' ⟶ X ×_S Spec 𝒪_{S', s'} is étale, κ(x) = κ(x'), X' is affine and of finite presentation over 𝒪_{S', s'}, g^*F is of finite presentation, and Γ(X', g^*F) is a free 𝒪_{S', s'}-module.

The two inputs are Tag 05ID, AlgebraicGeometry.exists_elementaryEtaleNeighborhood_projective_sections_of_isFlatOverAt, and Tag 05I5, AlgebraicGeometry.existsElementaryEtaleNeighborhoodFinitePresentationFlatOver.

theorem exists_etale_neighborhood_with_free_globalSections_of_isFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (x : X) (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : EtaleNeighborhood S (f x)) (_ : U.IsElementary)
      (X' : Scheme.{u}) (x' : X')
      (g : X' ⟶ X)
      (q : X' ⟶ Spec (.of (U.scheme.presheaf.stalk U.point)))
      (_ : g x' = x)
      (_ : q x' = IsLocalRing.closedPoint (U.scheme.presheaf.stalk U.point))
      (hcomm : g ≫ f = q ≫ U.scheme.fromSpecStalk U.point ≫ U.toBase)
      (_ : Etale (pullback.lift g q hcomm))
      (_ : IsIso (g.residueFieldMap x'))
      (_ : IsAffine X')
      (_ : FinitePresentation q)
      (_ : ((Scheme.Modules.pullback g).obj F).IsFinitePresentation),
      letI : Module (U.scheme.presheaf.stalk U.point)
          Γ((Scheme.Modules.pullback g).obj F, ⊤) :=
        Module.compHom _
          ((Scheme.ΓSpecIso (.of (U.scheme.presheaf.stalk U.point))).inv ≫ q.appTop).hom
      Module.Free (U.scheme.presheaf.stalk U.point)
        Γ((Scheme.Modules.pullback g).obj F, ⊤)
Tag 05KZ, a lemma

Tag 05KZ in the Stacks Project.

AlgebraicGeometry.exists_etale_neighborhood_with_free_globalSections_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSectionsFiniteType.lean, line 217.

Stacks Project, Tag 05KZ. Let f : X ⟶ S be locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let x : X be a point at which F is flat over S. Then there is an elementary étale neighbourhood (S', s') ⟶ (S, s) of the image s of x and a commutative diagram of pointed schemes 

  (X, x) ← (X', x')
    ↓         ↓
  (S, s) ← Spec 𝒪_{S', s'}
such that X' ⟶ X ×_S Spec 𝒪_{S', s'} is étale, κ(x) = κ(x'), X' is affine, and Γ(X', g^*F) is a free 𝒪_{S', s'}-module.

This is Tag 05KY with the finite-presentation hypothesis on f weakened to finite type, by the source's embedding into affine space: an affine neighbourhood V of x is a closed subscheme i : V ⟶ A of an affine space A over an affine open of S, with A ⟶ S locally of finite presentation, and Tag 05KY applies to A ⟶ S, to the direct image i_*(F|_V) and to the point i x. The chart Y ⟶ A it returns is pulled back to X' = V ×_A Y. The embedding is AlgebraicGeometry.exists_closedImmersion_affineSpace_of_locallyOfFiniteType, the flatness transfer across i is AlgebraicGeometry.isFlatOverAt_pushforward_finite_iff, and the comparison of sections is AlgebraicGeometry.affinePushforwardBaseChangeIso.

theorem exists_etale_neighborhood_with_free_globalSections_of_locallyOfFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (x : X) (hflat : IsFlatOverAt f.toLRSHom.toShHom F x) :
    ∃ (U : EtaleNeighborhood S (f x)) (_ : U.IsElementary)
      (X' : Scheme.{u}) (x' : X')
      (g : X' ⟶ X)
      (q : X' ⟶ Spec (.of (U.scheme.presheaf.stalk U.point)))
      (_ : g x' = x)
      (_ : q x' = IsLocalRing.closedPoint (U.scheme.presheaf.stalk U.point))
      (hcomm : g ≫ f = q ≫ U.scheme.fromSpecStalk U.point ≫ U.toBase)
      (_ : Etale (pullback.lift g q hcomm))
      (_ : IsIso (g.residueFieldMap x'))
      (_ : IsAffine X'),
      letI : Module (U.scheme.presheaf.stalk U.point)
          Γ((Scheme.Modules.pullback g).obj F, ⊤) :=
        Module.compHom _
          ((Scheme.ΓSpecIso (.of (U.scheme.presheaf.stalk U.point))).inv ≫ q.appTop).hom
      Module.Free (U.scheme.presheaf.stalk U.point)
        Γ((Scheme.Modules.pullback g).obj F, ⊤)
Tag 05L0, a lemma

Tag 05L0 in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSectionsAlongFibre.lean, line 902.

Stacks Project, Tag 05L0. Let f : X ⟶ S be of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite type and let s : S be such that F is flat over S at every point of the fibre X_s. Then there are an elementary étale neighbourhood (S', s') ⟶ (S, s) and a commutative diagram 

  X  ←ᵍ  X'
  ↓      ↓
  S  ←  Spec 𝒪_{S', s'}
such that X' ⟶ X ×_S Spec 𝒪_{S', s'} is étale, X_s = g((X')_{s'}), X' is affine and of finite presentation over 𝒪_{S', s'}, g^*F is of finite presentation, and Γ(X', g^*F) is a free 𝒪_{S', s'}-module.

The inputs are Tag 05KY, AlgebraicGeometry.exists_etale_neighborhood_with_free_globalSections_of_isFiniteType, applied at every point of the fibre, and Tag 057B, which makes the elementary étale neighbourhoods of (S, s) cofiltered so that the finitely many neighbourhoods surviving the quasi-compactness of the fibre are dominated by one of them.

theorem exists_elementaryEtaleNeighborhood_free_sections_along_fibre
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (hfp : FinitePresentation f)
    [F.IsQuasicoherent] [F.IsFiniteType] (s : S)
    (hflat : ∀ x : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x)) :
    ∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
      (X' : Scheme.{u})
      (q : X' ⟶ Spec (.of (U.scheme.presheaf.stalk U.point)))
      (g : X' ⟶ X)
      (hcomm : g ≫ f = q ≫ U.scheme.fromSpecStalk U.point ≫ U.toBase)
      (_ : Etale (pullback.lift g q hcomm))
      (_ : f ⁻¹' {s} = g '' (q ⁻¹' {IsLocalRing.closedPoint _}))
      (_ : IsAffine X')
      (_ : FinitePresentation q)
      (_ : ((Scheme.Modules.pullback g).obj F).IsFinitePresentation),
      letI : Module (U.scheme.presheaf.stalk U.point)
          Γ((Scheme.Modules.pullback g).obj F, ⊤) :=
        Module.compHom _
          ((Scheme.ΓSpecIso (.of (U.scheme.presheaf.stalk U.point))).inv ≫ q.appTop).hom
      Module.Free (U.scheme.presheaf.stalk U.point)
        Γ((Scheme.Modules.pullback g).obj F, ⊤)
Tag 05L1, a lemma

Tag 05L1 in the Stacks Project.

AlgebraicGeometry.exists_elementaryEtaleNeighborhood_free_sections_along_fibre_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ElementaryNeighborhood/FreeSectionsAlongFibre.lean, line 1031.

Stacks Project, Tag 05L1. Let f : X ⟶ S be of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let s : S be such that F is flat over S at every point of the fibre X_s. Then there are an elementary étale neighbourhood (S', s') ⟶ (S, s) and a commutative diagram 

  X  ←ᵍ  X'
  ↓      ↓
  S  ←  Spec 𝒪_{S', s'}
such that X' ⟶ X ×_S Spec 𝒪_{S', s'} is étale, X_s = g((X')_{s'}), X' is affine, and Γ(X', g^*F) is a free 𝒪_{S', s'}-module.

This differs from Tag 05L0 only in assuming f of finite type rather than of finite presentation, the input at each point of the fibre being Tag 05KZ, AlgebraicGeometry.exists_etale_neighborhood_with_free_globalSections_of_locallyOfFiniteType, in place of Tag 05KY; correspondingly the two finite-presentation clauses are dropped from the conclusion.

theorem exists_elementaryEtaleNeighborhood_free_sections_along_fibre_of_finiteType
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules)
    [LocallyOfFiniteType f] [QuasiCompact f]
    [F.IsQuasicoherent] [F.IsFiniteType] (s : S)
    (hflat : ∀ x : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x)) :
    ∃ (U : EtaleNeighborhood S s) (_ : U.IsElementary)
      (X' : Scheme.{u})
      (q : X' ⟶ Spec (.of (U.scheme.presheaf.stalk U.point)))
      (g : X' ⟶ X)
      (hcomm : g ≫ f = q ≫ U.scheme.fromSpecStalk U.point ≫ U.toBase)
      (_ : Etale (pullback.lift g q hcomm))
      (_ : f ⁻¹' {s} = g '' (q ⁻¹' {IsLocalRing.closedPoint _}))
      (_ : IsAffine X'),
      letI : Module (U.scheme.presheaf.stalk U.point)
          Γ((Scheme.Modules.pullback g).obj F, ⊤) :=
        Module.compHom _
          ((Scheme.ΓSpecIso (.of (U.scheme.presheaf.stalk U.point))).inv ≫ q.appTop).hom
      Module.Free (U.scheme.presheaf.stalk U.point)
        Γ((Scheme.Modules.pullback g).obj F, ⊤)
Sources
LeanModule.exists_freeMap_bijective_residueField · Module.universallyInjective_localizedMap_of_flat_localizedModule · Module.exists_universallyInjective_localizedModule_away_of_flat_localizedModule · Module.flat_localizedModule_coker_of_flat_localizedModule · Module.exists_universallyInjective_and_flat_coker_of_flat_localizedModule · Module.universallyInjective_localizedMap_and_flat_coker_of_exists_away · Module.injective_localizedMap_of_universallyInjective_localizedMap · Module.bijective_localizedMap_map_of_injective_localizedMap

Section38.13 Flat finite type modules, Part II#

Section 38.13 of the Stacks Project, Tag 05IF. 13 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CU6, a lemma

Tag 0CU6 in the Stacks Project.

Stacks.PureModules.exists_not_mem_and_mem_associatedPrimes_not_le_fiberIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/FibreAssociatedPrimes.lean, line 64.

Stacks Project, Tag 0CU6. An element can be chosen outside q whose image in the fibre lies in every associated prime of the fibre module that is not contained in the extension of q.

theorem exists_not_mem_and_mem_associatedPrimes_not_le_fiberIdeal
    {R S N : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [AddCommGroup N] [Module S N]
    [Module.FinitePresentation S N]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] :
    letI : Algebra S (p.Fiber S) := Algebra.TensorProduct.rightAlgebra
    ∃ g : S, g ∉ q ∧
      ∀ r ∈ associatedPrimes (p.Fiber S) (TensorProduct S (p.Fiber S) N),
        ¬ r ≤ Ideal.map
          (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S).toRingHom q →
        (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S) g ∈ r
Tag 05IG, a lemma

Tag 05IG in the Stacks Project.

Stacks.WeaklyAssociatedPrimes.isWeaklyAssociatedPrime_and_isAssociatedPrimeStacks_fibre_of_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/FlatFibreAtPrime.lean, line 499. The attribute's comment: “RESTRICTED: the implication ⟹ only, and its base clause carries the extra hypothesis that 𝔭 is finitely generated, which the tag does not have. That hypothesis stands in for the étale-local structure theorem 05ID, proved only scheme-side here”.

[Stacks, Tag 05IG], the implication ⟹. Let R → S be a ring map of finite presentation, let N be an S-module of finite presentation which is flat as an R-module, let M be an R-module, and let 𝔮 be a prime of S lying over a prime 𝔭 of R which is finitely generated. If 𝔮 is weakly associated to N ⊗_R M over S, then 𝔭 is weakly associated to M over R and 𝔮-bar is an associated prime, in the strict sense of [Stacks, Tag 00LA], of N-bar over the fibre ring S-bar.

Finite generation of 𝔭 enters the base clause only. It stands in for the étale-local structure theorem [Stacks, Tag 05ID], which the source uses to make N projective over the base and which this library has only in scheme-theoretic form; see the module documentation for what the ring-theoretic form would need. With N projective over a local base the witness lands in a finite free summand and no prime avoidance is needed, whereas the finiteness-free content available here (exists_smul_pow_eq_zero_localizedModule_of_tensorProduct) only covers 𝔭 R_𝔭 by the primes weakly associated to M_𝔭, and finitely many generators of 𝔭 are what turn that covering into a single witness. The variant ..._of_tensorProduct_of_finite trades it for finiteness of WeakAss_R(M), and the fibre clause isAssociatedPrimeStacks_fibre_of_isWeaklyAssociatedPrime_tensorProduct is free of both.

The converse implication of the tag is not proved here; see the module documentation.

theorem isWeaklyAssociatedPrime_and_isAssociatedPrimeStacks_fibre_of_tensorProduct
    [Algebra.FinitePresentation R S] [Module.FinitePresentation S N] [Module.Flat R N]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] (hfg : p.FG)
    (hq : IsWeaklyAssociatedPrime S (N ⊗[R] M) q) :
    IsWeaklyAssociatedPrime R M p ∧
      IsAssociatedPrimeStacks (Localization (primeComplImage S p) ⧸ fibreIdeal S p)
        ((Localization (primeComplImage S p) ⧸ fibreIdeal S p) ⊗[S] N)
        (Ideal.map (algebraMap S (Localization (primeComplImage S p) ⧸ fibreIdeal S p)) q)

Stacks.WeaklyAssociatedPrimes.tensorFibreFormula05IG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/TensorFibreFormula.lean, line 60.

[Stacks, Tag 05IG]. Let R → S be a ring map of finite presentation, let N be a finitely presented S-module which is flat as an R-module, let M be an R-module and let 𝔮 be a prime of S lying over a prime 𝔭 of R. Then 𝔮 is weakly associated to N ⊗_R M if and only if 𝔭 is weakly associated to M and some prime of the fibre ring S ⊗_R κ(𝔭) associated — in the strict sense of [Stacks, Tag 00LA] — to the fibre module contracts to 𝔮.

Both directions are proved, and no hypothesis beyond the tag's own is used.

theorem tensorFibreFormula05IG : TensorFibreFormula05IG.{u}
Tag 0CU7, an equation

Tag 0CU7 in the Stacks Project.

Stacks.PureModules.comap_associatedPrime_le_fiberIdeal_of_isUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/FibreAssociatedPrimesAway.lean, line 73.

Stacks Project, Tag 0CU7. With g ∈ S chosen as in Tag 0CU6, let B be an étale algebra over the fibre ring p.Fiber S in which the image of g is a unit. Then every prime of B associated to the base change of the fibre module contracts to a prime of p.Fiber S contained in the extension of q.

Indeed, such a contraction is associated to the fibre module itself, because B is flat over the fibre ring and the fibre ring is Noetherian; were it not contained in the extension of q, the choice of g would put the image of g inside it, contradicting the fact that the image of g in B is a unit.

theorem comap_associatedPrime_le_fiberIdeal_of_isUnit
    {R S N B : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FinitePresentation R S] [AddCommGroup N] [Module S N]
    [Module.FinitePresentation S N]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    [CommRing B] [Algebra (p.Fiber S) B] [Algebra.Etale (p.Fiber S) B]
    (g : S)
    (hg : letI : Algebra S (p.Fiber S) := Algebra.TensorProduct.rightAlgebra
      g ∉ q ∧
        (∀ r ∈ associatedPrimes (p.Fiber S)
          (TensorProduct S (p.Fiber S) N),
          (¬ r ≤ Ideal.map
            (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S).toRingHom q →
            (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S) g ∈ r)))
    (hunit : IsUnit ((algebraMap (p.Fiber S) B)
      ((Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S) g))) :
    letI : Algebra S (p.Fiber S) := Algebra.TensorProduct.rightAlgebra
    ∀ r' ∈ associatedPrimes B
      (TensorProduct (p.Fiber S) B (TensorProduct S (p.Fiber S) N)),
      Ideal.comap (algebraMap (p.Fiber S) B) r' ≤
        Ideal.map
          (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S).toRingHom q
Tag 05IH, a lemma

Tag 05IH in the Stacks Project.

Stacks.Divisors.isWeaklyAssociatedPoint_tensorPullback_iff_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedTensorPullbackIff.lean, line 118.

Let S be a scheme, let f : X ⟶ S be locally of finite type, let x ∈ X, let F be a quasi-coherent 𝒪_X-module of finite type and let G be a quasi-coherent 𝒪_S-module. If F is flat at x over S, then x is weakly associated to F ⊗_{𝒪_X} f^*G if and only if f x is weakly associated to G and x is an associated point of the restriction of F to the fibre X_{f x}, that is, x lies in the relative assassin Ass_{X/S}(F).

theorem isWeaklyAssociatedPoint_tensorPullback_iff_of_finiteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) (G : S.Modules) [F.IsQuasicoherent] [F.IsFiniteType] [G.IsQuasicoherent]
    (x : X) (hF : IsFlatOverAt f.toLRSHom.toShHom F x) :
    IsWeaklyAssociatedPoint
        ((((Stacks.SheafOfModules.Tensor.sheafTensor
                  ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf,
                    ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj
              (((Scheme.Modules.pullback f).obj G)))) x ↔
      (IsWeaklyAssociatedPoint G (f x) ∧ x ∈ relativeAssassin f F)
Tag 05II, a lemma

Tag 05II in the Stacks Project.

Stacks.WeaklyAssociatedPrimes.weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/TensorFibreEssentiallyFiniteType.lean, line 449. The attribute's comment: “the full set equality; the two rings lie in one universe, as IsEssentiallyOfFiniteType requires, and the modules are in arbitrary universes”.

[Stacks, Tag 05II]. For R → S essentially of finite type, N a localization of a finite S-module flat over R and M any R-module, the weakly associated primes of N ⊗[R] M are the contractions of the primes of the fibre rings S ⊗[R] κ(p) associated to the fibre modules, over the weakly associated primes p of M.

theorem weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small
    (R S : Type u) (M : Type v) (N₀ : Type w) (N : Type x)
    [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M]
    [AddCommGroup N₀] [Module S N₀] [Module.Finite S N₀]
    [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Flat R N]
    (hfinite : IsEssentiallyOfFiniteType R S (algebraMap R S))
    (T : Submonoid S) (f : N₀ →ₗ[S] N) [IsLocalizedModule T f] :
    weaklyAssociatedPrimes S (N ⊗[R] M) =
      {q : Ideal S | ∃ p ∈ weaklyAssociatedPrimes R M, ∃ hp : p.IsPrime,
        letI : p.IsPrime := hp
        ∃ q' ∈ assStacks (S ⊗[R] p.ResidueField)
          ((S ⊗[R] p.ResidueField) ⊗[S] N),
          q = Ideal.comap (Algebra.TensorProduct.includeLeft (R := R)
            (S := S) (A := S) (B := p.ResidueField)).toRingHom q'}

Stacks.WeaklyAssociatedPrimes.weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/WeaklyAssociatedPrime/TensorFibreFormulaEssentiallyFiniteType.lean, line 143. The attribute's comment: “the full set equality, for a module in the universe of the two rings”.

For M in the universe of the two rings, the weakly associated primes of N ⊗[R] M are the contractions of the primes of the fibre rings associated to the fibre modules, over the weakly associated primes of M.

theorem weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small'
    (R S : Type u) (M : Type u) (N₀ : Type w) (N : Type x)
    [CommRing R] [CommRing S] [Algebra R S]
    [AddCommGroup M] [Module R M]
    [AddCommGroup N₀] [Module S N₀] [Module.Finite S N₀]
    [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Flat R N]
    (hfinite : IsEssentiallyOfFiniteType R S (algebraMap R S))
    (T : Submonoid S) (f : N₀ →ₗ[S] N) [IsLocalizedModule T f] :
    weaklyAssociatedPrimes S (N ⊗[R] M) =
      {q : Ideal S | ∃ p ∈ weaklyAssociatedPrimes R M, ∃ hp : p.IsPrime,
        letI : p.IsPrime := hp
        ∃ q' ∈ assStacks (S ⊗[R] p.ResidueField)
          ((S ⊗[R] p.ResidueField) ⊗[S] N),
          q = Ideal.comap (Algebra.TensorProduct.includeLeft (R := R)
            (S := S) (A := S) (B := p.ResidueField)).toRingHom q'}
Tag 05IJ, a lemma

Tag 05IJ in the Stacks Project.

Stacks.Divisors.weaklyAssociatedPoints_tensorPullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedTensorPullbackFormula.lean, line 88.

[Stacks, Tag 05IJ]. Let f : X ⟶ S be locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type which is flat over S, and let G be a quasi-coherent 𝒪_S-module. Then the weakly associated points of F ⊗_{𝒪_X} f^*G are exactly the points of the fibres X_s, over the weakly associated points s of G, that are associated to the restriction of F to X_s.

This is the global form of Tag 05IH, and the source's proof of it is the pointwise statement plus the passage to sets. Both are already in StacksFrontier.AlgebraicGeometry.Flatness.WeaklyAssociatedTensorPullbackGlobal, up to the same algebraic input that Tag 05IH needed; supplying it here removes the hypothesis.

theorem weaklyAssociatedPoints_tensorPullback_eq
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) (G : S.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] [G.IsQuasicoherent]
    (hF : IsFlatOver f.toLRSHom.toShHom F) :
    weaklyAssociatedPoints
        (((Stacks.SheafOfModules.Tensor.sheafTensor
              ⟨(X.toLocallyRingedSpace.toRingedSpace).presheaf,
                (X.toLocallyRingedSpace.toRingedSpace).IsSheaf⟩).obj F).obj
          ((Scheme.Modules.pullback f).obj G)) =
      ⋃ s ∈ weaklyAssociatedPoints G,
        f.fiberι s '' associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F)

Stacks.Divisors.weaklyAssociatedPoints_tensorPullback_eq_of_localFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedTensorPullbackGlobal.lean, line 119. The attribute's comment: “the set equality, conditional on the algebraic formula of Tag 05II, carried here by the hypothesis LocalWeaklyAssociatedTensorFormula, which this library does not prove”.

Stacks Project, Tag 05IJ, from the local form of the algebraic formula of tag 05II. Let f : X ⟶ S be locally of finite type, let F be a finite-type quasi-coherent 𝒪_X-module flat over S, and let G be a quasi-coherent 𝒪_S-module. The weakly associated points of F ⊗_{𝒪_X} f^*G are the points of the fibres X_s over weakly associated points s of G that are associated to the restriction of F to X_s.

This is the source's own proof: the pointwise statement is tag 05IH, available here as Stacks.Divisors.isWeaklyAssociatedPoint_tensorPullback_iff_of_localFormula, and the passage to the set equality is Stacks.Divisors.mem_iUnion_fiberι_associatedPoints_iff.

theorem weaklyAssociatedPoints_tensorPullback_eq_of_localFormula
    (hformula : LocalWeaklyAssociatedTensorFormula.{u})
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) (G : S.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] [G.IsQuasicoherent]
    (hF : IsFlatOver f.toLRSHom.toShHom F) :
    weaklyAssociatedPoints
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf, ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (((Scheme.Modules.pullback f).obj G)))) =
      ⋃ s ∈ weaklyAssociatedPoints G,
        f.fiberι s '' associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F)

Stacks.Divisors.weaklyAssociatedPoints_tensorPullback_eq_of_formula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedTensorPullbackGlobal.lean, line 137. The attribute's comment: “the set equality, conditional on the formula of Tag 05II, carried here by the hypothesis WeaklyAssociatedPrimesTensorFormula, which this library does not prove”.

Stacks Project, Tag 05IJ, from the algebraic formula of tag 05II itself.

theorem weaklyAssociatedPoints_tensorPullback_eq_of_formula
    (hformula : WeaklyAssociatedPrimesTensorFormula.{u})
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) (G : S.Modules)
    [F.IsQuasicoherent] [F.IsFiniteType] [G.IsQuasicoherent]
    (hF : IsFlatOver f.toLRSHom.toShHom F) :
    weaklyAssociatedPoints
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf, ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (((Scheme.Modules.pullback f).obj G)))) =
      ⋃ s ∈ weaklyAssociatedPoints G,
        f.fiberι s '' associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F)

Stacks.Divisors.weaklyAssociatedPoints_tensorPullback_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedTensorPullbackGlobal.lean, line 164. The attribute's comment: “the inclusion ⊆ only, and under one hypothesis the tag does not have: finitely generated maximal ideals on S, which the base clause of Tag 05IH needs”.

Stacks Project, Tag 05IJ, the inclusion ⊆. Let f : X ⟶ S be locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type which is flat over S, and let G be an 𝒪_S-module. If the maximal ideals of the local rings of S are finitely generated, then every weakly associated point of F ⊗_{𝒪_X} f^*G lies on the fibre over a weakly associated point of G and is associated to the restriction of F to that fibre.

No algebraic input is assumed: this is the forward implication of tag 05IH, Stacks.Divisors.isWeaklyAssociatedPoint_and_mem_relativeAssassin_of_tensorPullback_of_finiteType, read as a statement about sets. Its one restriction is inherited: finite generation of the maximal ideal at the image point, which replaces the prime avoidance the source runs after making the stalk of F projective over the base by the étale-local structure theorem of tag 05ID.

theorem weaklyAssociatedPoints_tensorPullback_subset
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) (G : S.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hF : IsFlatOver f.toLRSHom.toShHom F)
    (hfg : ∀ s : S, (IsLocalRing.maximalIdeal (S.presheaf.stalk s)).FG) :
    weaklyAssociatedPoints
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf, ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (((Scheme.Modules.pullback f).obj G)))) ⊆
      ⋃ s ∈ weaklyAssociatedPoints G,
        f.fiberι s '' associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F)
Tag 05IK, a theorem

Tag 05IK in the Stacks Project.

AlgebraicGeometry.isOpen_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocus.lean, line 231. The attribute's comment: “openness of the relative flat locus”. References: EGA IV (11.1.6), “case C = B”; EGA IV (11.3.3), “wk assoc pts loc finite”; SGA 3 VIB (13.1), “(i) U open”.

Stacks Project, Tag 05IK (openness). The locus where a quasi-coherent module of finite type is flat over the target of a morphism locally of finite presentation is open, provided the weakly associated points of the target are locally finite.

theorem isOpen_flatLocus
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    IsOpen (flatLocus f F)

AlgebraicGeometry.isFinitePresentation_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocus.lean, line 352. The attribute's comment: “finite presentation on the flat locus”.

Stacks Project, Tag 05IK (finite presentation on the flat locus). For a morphism locally of finite presentation whose target has locally finite weakly associated points, a quasi-coherent module of finite type restricts to a module of finite presentation on the open subscheme that is its relative flat locus.

theorem isFinitePresentation_flatLocus
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    letI U : X.Opens := ⟨flatLocus f F, isOpen_flatLocus f F hS⟩
    (F.restrict U.ι).IsFinitePresentation

AlgebraicGeometry.isFlatOver_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocus.lean, line 366. The attribute's comment: “flatness over the base on the flat locus”.

Stacks Project, Tag 05IK (flatness on the flat locus). For a morphism locally of finite presentation whose target has locally finite weakly associated points, a quasi-coherent module of finite type restricts to a module flat over the base on the open subscheme that is its relative flat locus.

theorem isFlatOver_flatLocus
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    letI U : X.Opens := ⟨flatLocus f F, isOpen_flatLocus f F hS⟩
    IsFlatOver (U.ι ≫ f).toLRSHom.toShHom (F.restrict U.ι)
Tag 05IL, a lemma

Tag 05IL in the Stacks Project.

Stacks.Flatness.isOpen_setOf_flat_localizedModule_atPrime_of_finite_weaklyAssociatedPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteModuleOpenness.lean, line 74. The attribute's comment: “openness of the relative flat locus”. References: EGA IV (11.1.6), “case C = B”; EGA IV (11.3.3), “WeakAss finite”.

Stacks Project, Tag 05IL (openness). For a ring map R → S of finite presentation and a finite S-module M, the locus of primes q of S at which M_q is flat over R is open in Spec S, provided R has only finitely many weakly associated primes.

theorem isOpen_setOf_flat_localizedModule_atPrime_of_finite_weaklyAssociatedPrimes
    (hR : (weaklyAssociatedPrimes R R).Finite) :
    IsOpen {q : PrimeSpectrum S | Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)}

Stacks.Flatness.finitePresentation_localizedModule_away_of_basicOpen_subset_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteModuleOpenness.lean, line 111. The attribute's comment: “finite presentation on a basic open inside the flat locus”.

Stacks Project, Tag 05IL (finite presentation on a basic open). For a ring map R → S of finite presentation and a finite S-module M, if the basic open D(g) is contained in the locus where M is flat over R, then M_g is a finitely presented S_g-module, provided R has only finitely many weakly associated primes.

theorem finitePresentation_localizedModule_away_of_basicOpen_subset_flatLocus
    (hR : (weaklyAssociatedPrimes R R).Finite) (g : S)
    (hg : (↑(PrimeSpectrum.basicOpen g) : Set (PrimeSpectrum S)) ⊆
      {q : PrimeSpectrum S | Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)}) :
    Module.FinitePresentation (Localization.Away g) (LocalizedModule.Away g M)

Stacks.Flatness.OpenFlatLocus.flat_localizedModule_away_of_forall_flat_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/OpenFlatLocusNoetherian.lean, line 877. The attribute's comment: “flatness over the base”.

Flatness over the base spreads from the points of a basic open to the basic open itself. If M_{𝔮} is flat over R for every prime 𝔮 of S with g ∉ 𝔮, then M_g is flat over R.

Flatness over R is local on Spec (S_g) (Module.flat_of_isLocalized_maximal), and the local ring of M_g at a prime P of S_g is the localization of M at the prime P ∩ S of S: (S_g)_P is the localization of S at P ∩ S (IsLocalization.isLocalization_atPrime_localization_atPrime), and a composite of two base changes is a base change (IsBaseChange.comp).

theorem flat_localizedModule_away_of_forall_flat_atPrime {R S M : Type*} [CommRing R]
    [CommRing S]
    [Algebra R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (g : S)
    (H : ∀ q : PrimeSpectrum S, q ∈ PrimeSpectrum.basicOpen g →
      Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)) :
    Module.Flat R (LocalizedModule.Away g M)
Tag 05IM, a lemma

Tag 05IM in the Stacks Project.

AlgebraicGeometry.isOpen_setOf_isFlatAt_of_locallyOfFiniteType_of_locally_finite_weakAss, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/FlatLocus.lean, line 44. The attribute's comment: “openness of the locus of flatness”.

Openness of the flat locus. For a morphism f : X ⟶ S locally of finite type whose base has locally finite weakly associated points, the set of points at which f is flat is open.

theorem isOpen_setOf_isFlatAt_of_locallyOfFiniteType_of_locally_finite_weakAss
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (hS : ∀ s : S, ∃ V : S.Opens, s ∈ V ∧
      (schemeWeaklyAssociatedPoints S ∩ (V : Set S)).Finite) :
    IsOpen {x : X | IsFlatAt f.toLRSHom.toShHom x}

AlgebraicGeometry.locallyOfFinitePresentation_restrict_of_subset_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/FlatLocus.lean, line 106. The attribute's comment: “the flat locus is locally of finite presentation over the base”.

Finite presentation on the flat locus. For a morphism f : X ⟶ S locally of finite type whose base has locally finite weakly associated points, the restriction of f to an open subscheme contained in the locus of points of flatness is locally of finite presentation.

theorem locallyOfFinitePresentation_restrict_of_subset_flatLocus
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (hS : ∀ s : S, ∃ V : S.Opens, s ∈ V ∧
      (schemeWeaklyAssociatedPoints S ∩ (V : Set S)).Finite)
    (U : X.Opens) (hU : (U : Set X) ⊆ {x : X | IsFlatAt f.toLRSHom.toShHom x}) :
    LocallyOfFinitePresentation (U.ι ≫ f)

AlgebraicGeometry.flat_of_subset_setOf_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Flat/PointwiseOpenLocus.lean, line 88. The attribute's comment: “the flat locus is flat over the base”.

A morphism which is flat at every point of an open subscheme of its source is flat after restriction to that open subscheme.

theorem flat_of_subset_setOf_isFlatAt {X S : Scheme.{u}} (f : X ⟶ S) (V : X.Opens)
    (hV : (V : Set X) ⊆ {x : X | IsFlatAt f.toLRSHom.toShHom x}) :
    Flat (V.ι ≫ f)
Tag 05IN, a lemma

Tag 05IN in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_flat_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/FlatLocus.lean, line 55.

A morphism locally of finite type and flat over an integral base is locally of finite presentation.

theorem locallyOfFinitePresentation_of_flat_of_isIntegral
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [Flat f] [IsIntegral S] :
    LocallyOfFinitePresentation f
Tag 053G, a proposition

Tag 053G in the Stacks Project.

Stacks.Flatness.finitePresentation_of_flat_of_finiteType_of_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteTypeAlgebra.lean, line 149. The attribute's comment: “(1): a flat algebra of finite type over a domain is of finite presentation”.

Stacks Project, Tag 053G, part (1). A flat algebra of finite type over a domain is of finite presentation.

theorem finitePresentation_of_flat_of_finiteType_of_isDomain
    {R : Type u} [CommRing R] [IsDomain R] {S : Type v} [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] [Module.Flat R S] :
    Algebra.FinitePresentation R S

Stacks.Flatness.finitePresentation_of_finite_of_flat_of_isDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteTypeAlgebra.lean, line 158. The attribute's comment: “(2): a finite module flat over a domain is finitely presented”.

Stacks Project, Tag 053G, part (2). A finite module over an algebra of finite type over a domain is finitely presented as soon as it is flat over the domain.

theorem finitePresentation_of_finite_of_flat_of_isDomain
    {R : Type u} [CommRing R] [IsDomain R] {S : Type v} [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] {M : Type w} [AddCommGroup M] [Module S M] [Module R M]
    [IsScalarTower R S M] [Module.Finite S M] [Module.Flat R M] :
    Module.FinitePresentation S M
Tag 05IQ, a lemma

Tag 05IQ in the Stacks Project.

AlgebraicGeometry.isOpen_flatLocus_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocusFiniteType.lean, line 169. The attribute's comment: “openness of the relative flat locus”. References: SGA 3 VIB (13.1), “(i) U open”.

Stacks Project, Tag 05IQ (openness). The locus where a quasi-coherent module of finite type is flat over the target of a morphism locally of finite type is open, provided the weakly associated points of the target are locally finite.

theorem isOpen_flatLocus_of_locallyOfFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    IsOpen (flatLocus f F)

AlgebraicGeometry.isFlatOver_flatLocus_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocusFiniteType.lean, line 293. The attribute's comment: “flatness over the base on the flat locus”.

Stacks Project, Tag 05IQ (flatness on the flat locus). The restriction of the module to its relative flat locus is flat over the base.

theorem isFlatOver_flatLocus_of_locallyOfFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    letI U : X.Opens := ⟨flatLocus f F, isOpen_flatLocus_of_locallyOfFiniteType f F hS⟩
    IsFlatOver (U.ι ≫ f).toLRSHom.toShHom (F.restrict U.ι)

AlgebraicGeometry.isFinitelyPresentedRelative_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteTypeII/ModuleFlatLocusFiniteType.lean, line 306. The attribute's comment: “relative finite presentation on the flat locus”.

Stacks Project, Tag 05IQ (relative finite presentation on the flat locus). The restriction of the module to its relative flat locus is finitely presented relative to the base.

theorem isFinitelyPresentedRelative_flatLocus
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hS : ∀ s : S, ∃ W : S.Opens, s ∈ W ∧
      (schemeWeaklyAssociatedPoints S ∩ (W : Set S)).Finite) :
    letI U : X.Opens := ⟨flatLocus f F, isOpen_flatLocus_of_locallyOfFiniteType f F hS⟩
    IsFinitelyPresentedRelative (U.ι ≫ f) (F.restrict U.ι)
Tag 05IR, a lemma

Tag 05IR in the Stacks Project.

Stacks.Flatness.isOpen_setOf_flat_localizedModule_atPrime_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteTypeAlgebra.lean, line 92. The attribute's comment: “openness of the relative flat locus”. References: EGA IV (11.1.6), “case C = B”; EGA IV (11.3.3), “WeakAss finite”.

Stacks Project, Tag 05IR (openness). For a ring map R → S of finite type and a finite S-module M, the locus of primes q of S at which M_q is flat over R is open in Spec S, provided R has only finitely many weakly associated primes.

theorem isOpen_setOf_flat_localizedModule_atPrime_of_finiteType
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    {M : Type w} [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M]
    [Module.Finite S M] (hR : (weaklyAssociatedPrimes R R).Finite) :
    IsOpen {q : PrimeSpectrum S | Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)}

Stacks.Flatness.finitePresentationRel_localizedModule_away_of_basicOpen_subset_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FlatLocusFiniteTypeAlgebra.lean, line 171. The attribute's comment: “relative finite presentation on a basic open inside the flat locus”.

Stacks Project, Tag 05IR (relative finite presentation on a basic open). For a ring map R → S of finite type and a finite S-module M, if the basic open D(g) is contained in the locus where M is flat over R, then M_g is an S_g-module finitely presented relative to R, provided R has only finitely many weakly associated primes.

theorem finitePresentationRel_localizedModule_away_of_basicOpen_subset_flatLocus
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    {M : Type w} [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M]
    [Module.Finite S M] (hR : (weaklyAssociatedPrimes R R).Finite) (g : S)
    (hg : (↑(PrimeSpectrum.basicOpen g) : Set (PrimeSpectrum S)) ⊆
      {q : PrimeSpectrum S | Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)}) :
    Module.FinitePresentationRel R (Localization.Away g) (LocalizedModule.Away g M)

Stacks.Flatness.OpenFlatLocus.flat_localizedModule_away_of_forall_flat_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/OpenFlatLocusNoetherian.lean, line 877. The attribute's comment: “flatness over the base”.

Flatness over the base spreads from the points of a basic open to the basic open itself. If M_{𝔮} is flat over R for every prime 𝔮 of S with g ∉ 𝔮, then M_g is flat over R.

Flatness over R is local on Spec (S_g) (Module.flat_of_isLocalized_maximal), and the local ring of M_g at a prime P of S_g is the localization of M at the prime P ∩ S of S: (S_g)_P is the localization of S at P ∩ S (IsLocalization.isLocalization_atPrime_localization_atPrime), and a composite of two base changes is a base change (IsBaseChange.comp).

theorem flat_localizedModule_away_of_forall_flat_atPrime {R S M : Type*} [CommRing R]
    [CommRing S]
    [Algebra R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (g : S)
    (H : ∀ q : PrimeSpectrum S, q ∈ PrimeSpectrum.basicOpen g →
      Module.Flat R (LocalizedModule.AtPrime q.asIdeal M)) :
    Module.Flat R (LocalizedModule.Away g M)
Sources
LeanStacks.PureModules.exists_not_mem_and_mem_associatedPrimes_not_le_fiberIdeal · Stacks.WeaklyAssociatedPrimes.isWeaklyAssociatedPrime_and_isAssociatedPrimeStacks_fibre_of_tensorProduct · Stacks.WeaklyAssociatedPrimes.tensorFibreFormula05IG · Stacks.PureModules.comap_associatedPrime_le_fiberIdeal_of_isUnit · Stacks.Divisors.isWeaklyAssociatedPoint_tensorPullback_iff_of_finiteType · Stacks.WeaklyAssociatedPrimes.weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small · Stacks.WeaklyAssociatedPrimes.weaklyAssociatedPrimes_tensorProduct_eq_fibrewise_assStacks_of_small' · Stacks.Divisors.weaklyAssociatedPoints_tensorPullback_eq

Section38.14 Examples of relatively pure modules#

Section 38.14 of the Stacks Project, Tag 05IS. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05FV, a lemma

Tag 05FV in the Stacks Project.

Stacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/ClosedFibreAssociatedPrimes.lean, line 77.

Stacks Project, Tag 05FV. Under the finite Noetherian closed-fibre hypotheses, an associated prime of any fibre of a projective module meets the closed fibre of a local base.

lemma associatedPrime_add_map_maximalIdeal_ne_top
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R]
    (N : Type w) [AddCommGroup N] [Module S N] [Module R N] [IsScalarTower R S N]
    [Module.Projective R N]
    [IsNoetherianRing (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))]
    [Module.Finite (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))
      (N ⧸ ((IsLocalRing.maximalIdeal R).map (algebraMap R S) • (⊤ : Submodule S N)))]
    (q : PrimeSpectrum S)
    (hq : IsAssociatedPrimeStacks S
      (N ⊗[R] (PrimeSpectrum.comap (algebraMap R S) q).asIdeal.ResidueField) q.asIdeal) :
    q.asIdeal + (IsLocalRing.maximalIdeal R).map (algebraMap R S) ≠ ⊤
Tag 05IT, a lemma

Tag 05IT in the Stacks Project.

Stacks.PureModules.associatedPrime_add_map_ne_top_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/AdicComplete.lean, line 49.

Stacks Project, Tag 05IT. An associated prime of the tensor product of an adically complete module with any base module is not comaximal with the ideal of completion.

theorem associatedPrime_add_map_ne_top_of_isAdicComplete
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    (I : Ideal R) (N : Type w) [AddCommGroup N] [Module R N] [Module S N]
    [IsScalarTower R S N] [IsAdicComplete I N]
    (M : Type x) [AddCommGroup M] [Module R M]
    (q : Ideal S) (hq : IsAssociatedPrimeStacks S (N ⊗[R] M) q) :
    q + I.map (algebraMap R S) ≠ ⊤
Tag 05IU, a lemma

Tag 05IU in the Stacks Project.

Stacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top_of_directSum_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/MittagLeffler.lean, line 328.

Stacks Project, Tag 05IU. An associated prime of a tensor product of a direct sum of finite modules cannot be comaximal with the closed fibre of a local base ring.

theorem associatedPrime_add_map_maximalIdeal_ne_top_of_directSum_finite
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsLocalRing R] [Algebra R S]
    (N : Type w) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    (ι : Type x) (F : ι → Type y)
    [∀ i, AddCommGroup (F i)] [∀ i, Module R (F i)]
    (hF : ∀ i, Module.Finite R (F i))
    (e : N ≃ₗ[R] ⨁ i, F i)
    (M : Type z) [AddCommGroup M] [Module R M]
    (q : Ideal S) (hq : IsAssociatedPrimeStacks S (N ⊗[R] M) q) :
    q + (IsLocalRing.maximalIdeal R).map (algebraMap R S) ≠ ⊤
Tag 05IV, a lemma

Tag 05IV in the Stacks Project.

Stacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top_of_countable_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/MittagLeffler.lean, line 391.

Stacks Project, Tag 05IV. An associated prime of a tensor product of a countably generated Mittag-Leffler module over a henselian local ring cannot be comaximal with the closed fibre.

theorem associatedPrime_add_map_maximalIdeal_ne_top_of_countable_mittagLeffler
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [HenselianLocalRing R]
    [Algebra R S]
    (N : Type w) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [Small.{w} R]
    (hcg : ∃ t : Set N, t.Countable ∧ Submodule.span R t = ⊤)
    (hML : IsMittagLeffler.{u, w, w, w, w} R N)
    (M : Type x) [AddCommGroup M] [Module R M]
    (q : Ideal S) (hq : IsAssociatedPrimeStacks S (N ⊗[R] M) q) :
    q + (IsLocalRing.maximalIdeal R).map (algebraMap R S) ≠ ⊤
Sources
LeanStacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top · Stacks.PureModules.associatedPrime_add_map_ne_top_of_isAdicComplete · Stacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top_of_directSum_finite · Stacks.PureModules.associatedPrime_add_map_maximalIdeal_ne_top_of_countable_mittagLeffler

Section38.15 Impurities#

Section 38.15 of the Stacks Project, Tag 05IW. 9 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05FW, a situation

Tag 05FW in the Stacks Project.

AlgebraicGeometry.PrePureSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Impurities.lean, line 60.

Stacks Project, Tag 05FW. The standing pre-pure situation: a finite type morphism X ⟶ S, a finite type quasi-coherent module on X, and a point of S.

structure PrePureSituation
Tag 05IX, an equation

Tag 05IX in the Stacks Project.

AlgebraicGeometry.ImpurityDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Impurities.lean, line 85.

Stacks Project, Tag 05IX. A base-change diagram together with a specialization over the chosen point of a pre-pure situation and a point above its generalization.

structure ImpurityDiagram (P : PrePureSituation.{u})
Tag 05IY, a definition

Tag 05IY in the Stacks Project.

AlgebraicGeometry.IsImpurity, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Impurities.lean, line 118.

Stacks Project, Tag 05IY. An impurity diagram defines an impurity when its chosen point belongs to the relative assassin of the pulled-back module and its closure is disjoint from the fibre over the specialized point.

abbrev IsImpurity (P : PrePureSituation.{u}) (D : ImpurityDiagram P) : Prop
Tag 05FX, a lemma

Tag 05FX in the Stacks Project.

AlgebraicGeometry.exists_impurity_locallyOfFinitePresentation_closedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/FinitePresentationBase.lean, line 300.

An impurity can be witnessed over a test family which is locally of finite presentation over the base, with its specialized point closed in the fibre over the distinguished point.

theorem exists_impurity_locallyOfFinitePresentation_closedPoint (P : PrePureSituation.{u})
    (h : ∃ D : ImpurityDiagram P, IsImpurity P D) :
    ∃ D : ImpurityDiagram P, IsImpurity P D ∧ LocallyOfFinitePresentation D.g ∧
      ∃ t_fib : D.g.fiber P.s,
        D.g.fiberι P.s t_fib = D.t ∧ t_fib ∈ closedPoints (D.g.fiber P.s)
Tag 05IZ, a lemma

Tag 05IZ in the Stacks Project.

AlgebraicGeometry.exists_isImpurity_mapBase_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/LimitDescent.lean, line 399.

An impurity on a cofiltered limit of affine schemes over the base is the pullback of an impurity at some stage.

public theorem exists_isImpurity_mapBase_of_isLimit
    {P : AlgebraicGeometry.PrePureSituation.{u}}
    {I : Type v} [Category.{w} I] [IsCofiltered I]
    (F : I ⥤ Over P.S) (c : Cone F) (hc : IsLimit c)
    (D : AlgebraicGeometry.ImpurityDiagram P) (e : Over.mk D.g ≅ c.pt)
    (hF : ∀ i, IsAffine (F.obj i).left) (hD : AlgebraicGeometry.IsImpurity P D) :
    ∃ i, AlgebraicGeometry.IsImpurity P
      (mapBase D (F.obj i).hom (e.hom ≫ c.π.app i).left (e.hom ≫ c.π.app i).w)
Tag 05J0, a lemma

Tag 05J0 in the Stacks Project.

AlgebraicGeometry.exists_isImpurity_elementaryEtaleNeighborhood_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/QuasiFiniteNeighborhood.lean, line 235.

Stacks Project, Tag 05J0. If a pre-pure situation admits an impurity whose test family is quasi-finite over the base at the distinguished point, then it admits one whose test family, pointed at the distinguished point, is an elementary étale neighbourhood of the chosen point of the base.

theorem exists_isImpurity_elementaryEtaleNeighborhood_of_quasiFiniteAt
    (P : PrePureSituation.{u})
    (h : ∃ D : ImpurityDiagram P, IsImpurity P D ∧ quasiFiniteAt D.g D.t) :
    ∃ (D : ImpurityDiagram P) (hD : Etale D.g), IsImpurity P D ∧
      EtaleNeighborhood.IsElementary
        ({ scheme := D.T
           point := D.t
           toBase := D.g
           etale_toBase := hD
           map_point := D.mapsToChosenPoint } : EtaleNeighborhood P.S P.s)
Tag 05J1, a lemma

Tag 05J1 in the Stacks Project.

AlgebraicGeometry.exists_isImpurity_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/QuasiFiniteTestFamily.lean, line 337.

Stacks Project, Tag 05J1. Over a locally Noetherian base, an impurity of the module of a pre-pure situation above the chosen point of the base can be witnessed by an impurity whose test family is quasi-finite over the base at its specialized point.

theorem exists_isImpurity_quasiFiniteAt (P : PrePureSituation.{u}) [IsLocallyNoetherian P.S]
    (h : ∃ D : ImpurityDiagram P, IsImpurity P D) :
    ∃ D : ImpurityDiagram P, IsImpurity P D ∧ quasiFiniteAt D.g D.t
Tag 05J2, a lemma

Tag 05J2 in the Stacks Project.

AlgebraicGeometry.exists_isImpurity_elementaryEtaleNeighborhood_of_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/HenselizationDescent.lean, line 173.

An impurity whose test family is the spectrum of a henselization of the local ring of the base at the distinguished point already occurs over an elementary étale neighbourhood of that point.

theorem exists_isImpurity_elementaryEtaleNeighborhood_of_henselization
    (P : PrePureSituation.{u}) (Rh : Type u) [CommRing Rh] [IsLocalRing Rh]
    [Algebra (P.S.presheaf.stalk P.s) Rh]
    [IsLocalRing.IsHenselization (P.S.presheaf.stalk P.s)
      (IsLocalRing.ResidueField (P.S.presheaf.stalk P.s)) Rh]
    (h : ∃ (D : ImpurityDiagram P) (e : D.T ≅ Spec (CommRingCat.of Rh)),
      D.g = e.hom ≫ specHenselizationToBase P.s Rh ∧ IsImpurity P D) :
    ∃ (D : ImpurityDiagram P) (hD : Etale D.g), IsImpurity P D ∧
      EtaleNeighborhood.IsElementary
        ({ scheme := D.T
           point := D.t
           toBase := D.g
           etale_toBase := hD
           map_point := D.mapsToChosenPoint } : EtaleNeighborhood P.S P.s)
Tag 05J3, a lemma

Tag 05J3 in the Stacks Project.

AlgebraicGeometry.exists_isImpurity_henselization_iff_elementaryEtaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Impurity/HenselizationAscent.lean, line 104. The attribute's comment: “parts (1) and (2)”.

In a pre-pure situation, an impurity over the henselization of the base at the distinguished point exists if and only if one exists over an elementary étale neighbourhood of that point.

theorem exists_isImpurity_henselization_iff_elementaryEtaleNeighborhood
    (P : PrePureSituation.{u}) :
    (∃ (D : ImpurityDiagram P) (e : D.T ≅ henselization P.S P.s),
      D.g = e.hom ≫ henselizationToBase P.S P.s ∧ IsImpurity P D) ↔
    (∃ (D : ImpurityDiagram P) (hD : Etale D.g), IsImpurity P D ∧
      EtaleNeighborhood.IsElementary
        ({ scheme := D.T
           point := D.t
           toBase := D.g
           etale_toBase := hD
           map_point := D.mapsToChosenPoint } : EtaleNeighborhood P.S P.s))

AlgebraicGeometry.exists_isImpurity_elementaryEtaleNeighborhood_iff_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/QuasiFiniteImpurityData.lean, line 248. The attribute's comment: “parts (2) and (3)”.

Stacks Project, Tag 05J3, parts (2) and (3). A pre-pure situation admits an impurity whose test family, pointed at the distinguished point, is an elementary étale neighbourhood of the chosen point of the base if and only if it admits one whose test family is quasi-finite over the base at the distinguished point.

theorem exists_isImpurity_elementaryEtaleNeighborhood_iff_quasiFiniteAt
    (P : PrePureSituation.{u}) :
    (∃ (D : ImpurityDiagram P) (hD : Etale D.g), IsImpurity P D ∧
      EtaleNeighborhood.IsElementary
        ({ scheme := D.T
           point := D.t
           toBase := D.g
           etale_toBase := hD
           map_point := D.mapsToChosenPoint } : EtaleNeighborhood P.S P.s)) ↔
    (∃ D : ImpurityDiagram P, IsImpurity P D ∧ quasiFiniteAt D.g D.t)
Sources
LeanAlgebraicGeometry.PrePureSituation · AlgebraicGeometry.ImpurityDiagram · AlgebraicGeometry.IsImpurity · AlgebraicGeometry.exists_impurity_locallyOfFinitePresentation_closedPoint · AlgebraicGeometry.exists_isImpurity_mapBase_of_isLimit · AlgebraicGeometry.exists_isImpurity_elementaryEtaleNeighborhood_of_quasiFiniteAt · AlgebraicGeometry.exists_isImpurity_quasiFiniteAt · AlgebraicGeometry.exists_isImpurity_elementaryEtaleNeighborhood_of_henselization

Section38.16 Relatively pure modules#

Section 38.16 of the Stacks Project, Tag 05BB. 7 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05J4, a definition

Tag 05J4 in the Stacks Project.

AlgebraicGeometry.IsPureAlong, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 111. The attribute's comment: “part (1)”.

A finite type quasi-coherent module is pure along the fibre over the chosen point if no impurity occurs over an elementary étale neighbourhood of that point.

abbrev IsPureAlong (P : PrePureSituation.{u}) : Prop

AlgebraicGeometry.IsUniversallyPureAlong, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 124. The attribute's comment: “part (2)”.

A finite type quasi-coherent module is universally pure along the fibre over the chosen point if no impurity occurs after any base change.

abbrev IsUniversallyPureAlong (P : PrePureSituation.{u}) : Prop

AlgebraicGeometry.IsSchemePureAlong, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 129. The attribute's comment: “part (3)”.

The scheme X is pure along the fibre over s when its structure sheaf is pure there.

abbrev IsSchemePureAlong {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (s : S) : Prop

AlgebraicGeometry.IsUniversallyPureRelative, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 143. The attribute's comment: “part (4)”.

A finite type quasi-coherent module is universally pure relative to the base if it is universally pure along every fibre.

abbrev IsUniversallyPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] : Prop

AlgebraicGeometry.IsPureRelative, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 156. The attribute's comment: “part (5)”.

A finite type quasi-coherent module is pure relative to the base if it is pure along every fibre.

abbrev IsPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] : Prop

AlgebraicGeometry.IsSchemePureRelative, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/Purity.lean, line 169. The attribute's comment: “part (6)”.

The scheme X is pure relative to S when its structure sheaf is pure relative to the base.

abbrev IsSchemePureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] : Prop
Tag 05J5, a remark

Tag 05J5 in the Stacks Project.

AlgebraicGeometry.noElementaryEtaleImpurity_of_noQuasiFiniteImpurity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/LocallyOfFiniteTypePurity.lean, line 218. The attribute's comment: “condition (2) implies condition (1)”.

Condition (2) implies condition (1): an elementary étale neighbourhood is étale, hence quasi-finite at its distinguished point.

This is one direction of the equivalence of conditions (1) and (2), and is unconditional. The converse is Tag 05J0, whose proof does not use quasi-compactness but which is not available in this library, so the equivalence itself is not claimed here.

theorem noElementaryEtaleImpurity_of_noQuasiFiniteImpurity {f : X ⟶ S} {F : X.Modules} {s : S}
    (h : NoQuasiFiniteImpurity f F s) : NoElementaryEtaleImpurity f F s

AlgebraicGeometry.noHenselianImpurity_iff_relativeAssassinSpecializesIntoClosedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/LocallyOfFiniteTypePurity.lean, line 268. The attribute's comment: “conditions (3) and (4) are equivalent”.

Stacks Project, Tag 05J5. For a morphism which is only locally of finite type, conditions (3) and (4) are still equivalent: the impurities above s whose test family is a model of S^h → S are exactly the points of Ass_{X^h/S^h}(ℱ^h) which fail to specialize into the fibre of X^h over the closed point of S^h.

What makes this work is that the auxiliary data of such an impurity carry no information: its distinguished point is forced to be the closed point of the model, because every point of S^h over s is the closed point, and the specialization to it is automatic, because every point of the spectrum of a local ring specializes to its closed point.

theorem noHenselianImpurity_iff_relativeAssassinSpecializesIntoClosedFibre
    [LocallyOfFiniteType f] [F.IsFiniteType] [F.IsQuasicoherent] :
    NoHenselianImpurity f F s Rh ↔ RelativeAssassinSpecializesIntoClosedFibre f F s Rh

AlgebraicGeometry.noElementaryEtaleImpurity_iff_noQuasiFiniteImpurity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/QuasiFiniteImpurityData.lean, line 285. The attribute's comment: “conditions (1) and (2) are equivalent”.

Stacks Project, Tag 05J5. For a morphism which is only locally of finite type, conditions (1) and (2) are still equivalent: an impurity above s whose test family is merely quasi-finite at its distinguished point can be replaced by one whose test family is an elementary étale neighbourhood of s.

This is the half of the remark which asserts that the proof of Tag 05J0 does not use quasi-compactness of the morphism: that proof is run here for impurity data, which carry no such hypothesis.

theorem noElementaryEtaleImpurity_iff_noQuasiFiniteImpurity {f : X ⟶ S} [LocallyOfFiniteType f]
    {F : X.Modules} [F.IsQuasicoherent] {s : S} :
    NoElementaryEtaleImpurity f F s ↔ NoQuasiFiniteImpurity f F s
Tag 05J6, a lemma

Tag 05J6 in the Stacks Project.

AlgebraicGeometry.isUniversallyPureAlong_iff_forall_baseChange_isPureAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/BaseChange.lean, line 70. The attribute's comment: “the pointed-fibre equivalence”.

Stacks Project, Tag 05J6. Universal purity along the chosen fibre can be tested by purity after every pointed base change.

public theorem isUniversallyPureAlong_iff_forall_baseChange_isPureAlong
    (P : PrePureSituation.{u}) :
    IsUniversallyPureAlong P ↔
      ∀ (Q : PrePureSituation.{u}) (g : Q.S ⟶ P.S)
        (_hg : g.base Q.s = P.s) (toX : Q.X ⟶ P.X)
        (_hpb : IsPullback toX Q.f P.f g)
        (_hF : Q.F ≅ (Scheme.Modules.pullback toX).obj P.F),
          IsPureAlong Q

AlgebraicGeometry.isUniversallyPureRelative_iff_forall_baseChange_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/BaseChange.lean, line 117. The attribute's comment: “the relative equivalence”.

Stacks Project, Tag 05J6, in particular. Universal purity over the base can be tested by purity relative to every base change.

public theorem isUniversallyPureRelative_iff_forall_baseChange_isPureRelative
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] :
    IsUniversallyPureRelative f F ↔
      ∀ {X' S' : Scheme.{u}} (f' : X' ⟶ S')
        [LocallyOfFiniteType f'] [QuasiCompact f']
        (F' : X'.Modules) [F'.IsFiniteType] [F'.IsQuasicoherent]
        (g : S' ⟶ S) (toX : X' ⟶ X)
        (_hpb : IsPullback toX f' f g)
        (_hF : F' ≅ (Scheme.Modules.pullback toX).obj F),
          IsPureRelative f' F'
Tag 05J7, a lemma

Tag 05J7 in the Stacks Project.

AlgebraicGeometry.isPureAlong_of_quasiFiniteAt_of_isPureAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/QuasiFinitePointedBaseChange.lean, line 54.

Stacks Project, Tag 05J7. If a morphism of pointed schemes (S', s') → (S, s) is quasi-finite at s' and a finite type quasi-coherent module is pure along the fibre over s, then its pullback to the base change is pure along the fibre over s'.

public theorem isPureAlong_of_quasiFiniteAt_of_isPureAlong {P Q : PrePureSituation.{u}}
    (g : Q.S ⟶ P.S) (hg : g.base Q.s = P.s) (toX : Q.X ⟶ P.X)
    (hpb : IsPullback toX Q.f P.f g)
    (hF : Q.F ≅ (Scheme.Modules.pullback toX).obj P.F)
    (hqf : quasiFiniteAt g Q.s) (hP : IsPureAlong P) :
    IsPureAlong Q
Tag 05J8, a lemma

Tag 05J8 in the Stacks Project.

AlgebraicGeometry.isPureAlong_iff_isUniversallyPureAlong_of_isNoetherianRing_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/NoetherianStalk.lean, line 218.

Stacks Project, Tag 05J8. Let f : X ⟶ S be of finite type, let ℱ be a finite type quasi-coherent 𝒪_X-module and let s be a point of S whose local ring 𝒪_{S, s} is Noetherian. Then ℱ is pure along the fibre X_s if and only if it is universally pure along X_s.

theorem isPureAlong_iff_isUniversallyPureAlong_of_isNoetherianRing_stalk
    (P : PrePureSituation.{u}) [IsNoetherianRing (P.S.presheaf.stalk P.s)] :
    IsPureAlong P ↔ IsUniversallyPureAlong P
Tag 05J9, a lemma

Tag 05J9 in the Stacks Project.

AlgebraicGeometry.isPureAlong_of_flatPointedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/PurityDescent.lean, line 102. The attribute's comment: “flat_descend_pure”.

Stacks Project, Tag 05J9. Purity along the original fibre follows from purity along the fibre of a pointed base change which is flat at its distinguished point.

public theorem isPureAlong_of_flatPointedBaseChange (H : FlatPointedBaseChangeSituation.{u})
    (P' : PrePureSituation.{u}) (eS : P'.S = H.S') (eX : P'.X = pullback H.f H.g)
    (hf : eqToHom eX.symm ≫ P'.f ≫ eqToHom eS = pullback.snd H.f H.g)
    (hF : HEq P'.F ((Scheme.Modules.pullback (pullback.fst H.f H.g)).obj H.F))
    (hs : eS ▸ P'.s = H.s') (hpure : IsPureAlong P') :
    IsPureAlong ({ S := H.S, X := H.X, f := H.f, F := H.F, s := H.s } :
      PrePureSituation.{u})

AlgebraicGeometry.universallyPureAlong_of_flatPointedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningStratification/PurityDescent.lean, line 180. The attribute's comment: “flat_descend_universally_pure”.

Stacks Project, Tag 05J9. Universal purity along a fibre descends through a pointed base change which is flat at the new distinguished point.

public theorem universallyPureAlong_of_flatPointedBaseChange
    (H : FlatPointedBaseChangeSituation.{u})
    (h : IsUniversallyPureAlong H.baseChangedSituation) :
    IsUniversallyPureAlong ({ S := H.S, X := H.X, f := H.f, F := H.F, s := H.s } :
      PrePureSituation.{u})
Tag 05K1, a lemma

Tag 05K1 in the Stacks Project.

AlgebraicGeometry.isPureAlong_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/FinitePushforward.lean, line 201. The attribute's comment: “purity along the fibre”.

Stacks Project, Tag 05K1. Purity along a fibre is unchanged by pushing a finite type quasi-coherent module forward along a closed immersion.

theorem isPureAlong_iff_pushforward :
    IsPureAlong (prePureSituationComp i f F s) ↔
      IsPureAlong (prePureSituationPushforward i f F s)

AlgebraicGeometry.isUniversallyPureAlong_iff_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/FinitePushforward.lean, line 225. The attribute's comment: “universal purity along the fibre”.

Stacks Project, Tag 05K1. Universal purity along a fibre is unchanged by pushing a finite type quasi-coherent module forward along a closed immersion.

theorem isUniversallyPureAlong_iff_pushforward :
    IsUniversallyPureAlong (prePureSituationComp i f F s) ↔
      IsUniversallyPureAlong (prePureSituationPushforward i f F s)
Sources
LeanAlgebraicGeometry.IsPureAlong · AlgebraicGeometry.IsUniversallyPureAlong · AlgebraicGeometry.IsSchemePureAlong · AlgebraicGeometry.IsUniversallyPureRelative · AlgebraicGeometry.IsPureRelative · AlgebraicGeometry.IsSchemePureRelative · AlgebraicGeometry.noElementaryEtaleImpurity_of_noQuasiFiniteImpurity · AlgebraicGeometry.noHenselianImpurity_iff_relativeAssassinSpecializesIntoClosedFibre

Section38.17 Examples of relatively pure sheaves#

Section 38.17 of the Stacks Project, Tag 05K2. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05K3, a lemma

Tag 05K3 in the Stacks Project.

AlgebraicGeometry.isUniversallyPureRelative_of_support_isProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/ProperSupport.lean, line 116. The attribute's comment: “part (1)”.

Stacks Project, Tag 05K3, part (1). A finite type quasi-coherent module whose support is proper over the base is universally pure relative to that base.

theorem isUniversallyPureRelative_of_support_isProperOver {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent]
    (hF : IsProperOver f (⟨SheafOfModules.supp F, SheafOfModules.isClosed_supp F⟩ : Closeds X)) :
    IsUniversallyPureRelative f F

AlgebraicGeometry.isUniversallyPureRelative_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/ProperSupport.lean, line 154. The attribute's comment: “part (2)”.

Stacks Project, Tag 05K3, part (2). A finite type quasi-coherent module on a scheme which is proper over the base is universally pure relative to that base.

theorem isUniversallyPureRelative_of_isProper {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] :
    IsUniversallyPureRelative f F

AlgebraicGeometry.isSchemeUniversallyPureRelative_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/ProperSupport.lean, line 164. The attribute's comment: “part (3)”.

Stacks Project, Tag 05K3, part (3). A proper scheme is universally pure over its base.

theorem isSchemeUniversallyPureRelative_of_isProper {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] :
    @IsUniversallyPureRelative.{u} X S f _ _ (SheafOfModules.unit.{u} X.ringCatSheaf)
      (structureSheaf_isFiniteType X)
      (Stacks.AlgebraicGeometry.AffineQcohPushforward.isQuasicoherent_unit X)
Tag 05K4, a lemma

Tag 05K4 in the Stacks Project.

AlgebraicGeometry.isPureRelative_iff_isFinite_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/FiniteSupport.lean, line 363. The attribute's comment: “conditions (1) and (2)”.

Stacks Project, Tag 05K4, conditions (1) and (2). Let f : X ⟶ S be separated of finite type and let ℱ be a finite type quasi-coherent 𝒪_X-module with finite support on every fibre of f. Then ℱ is pure relative to S if and only if its scheme-theoretic support is finite over S.

theorem isPureRelative_iff_isFinite_schemeTheoreticSupport {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent]
    (hfinite : ∀ s : S,
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)).Finite) :
    IsPureRelative f F ↔
      IsFinite ((Scheme.Modules.schemeTheoreticSupport F).subschemeι ≫ f)

AlgebraicGeometry.isUniversallyPureRelative_iff_isFinite_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/FiniteSupport.lean, line 400. The attribute's comment: “conditions (2) and (3)”.

Stacks Project, Tag 05K4, conditions (2) and (3). Let f : X ⟶ S be separated of finite type and let ℱ be a finite type quasi-coherent 𝒪_X-module with finite support on every fibre of f. Then ℱ is universally pure relative to S if and only if its scheme-theoretic support is finite over S.

theorem isUniversallyPureRelative_iff_isFinite_schemeTheoreticSupport {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent]
    (hfinite : ∀ s : S,
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)).Finite) :
    IsUniversallyPureRelative f F ↔
      IsFinite ((Scheme.Modules.schemeTheoreticSupport F).subschemeι ≫ f)

AlgebraicGeometry.isSchemePureRelative_iff_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/RelativelyPure/FiniteSupport.lean, line 414. The attribute's comment: “in particular: quasi-finite separated morphisms”.

Stacks Project, Tag 05K4, in particular. A separated quasi-finite scheme over S is pure relative to S if and only if its structure morphism is finite.

theorem isSchemePureRelative_iff_isFinite {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] [LocallyQuasiFinite f] [IsSeparated f] :
    IsSchemePureRelative f ↔ IsFinite f
Tag 05K5, a lemma

Tag 05K5 in the Stacks Project.

AlgebraicGeometry.universallyPure_of_flat_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/GeometricallyIntegralFibres.lean, line 67.

Stacks Project, Tag 05K5. A flat finite type morphism with geometrically integral fibres has universally pure structure sheaf over its base.

theorem universallyPure_of_flat_geometricallyIntegral {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] [Flat f] [GeometricallyIntegral f] :
    @IsUniversallyPureRelative.{u} X S f _ _
      (SheafOfModules.unit.{u} X.ringCatSheaf)
      (structureSheaf_isFiniteType X)
      (Stacks.AlgebraicGeometry.AffineQcohPushforward.isQuasicoherent_unit X)
Tag 05K6, a lemma

Tag 05K6 in the Stacks Project.

AlgebraicGeometry.isUniversallyPureRelative_of_pushforward_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FlatteningFunctor/LocallyProjectivePurity.lean, line 788.

Stacks Project, Tag 05K6. For an affine morphism of finite type, a finite type quasi-coherent module with locally projective direct image is universally pure over the base.

The affine base change used along the way is the third assertion of Stacks Tag 02KG, Stacks.AlgebraicGeometry.AffineBaseChangeLocality.baseChangeIso, bound to bc below and threaded through the private lemmas in the shape in which they take it.

public theorem isUniversallyPureRelative_of_pushforward_isLocallyProjective
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffineHom f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (hF : Scheme.Modules.IsLocallyProjective ((Scheme.Modules.pushforward f).obj F)) :
    IsUniversallyPureRelative f F
Sources
LeanAlgebraicGeometry.isUniversallyPureRelative_of_support_isProperOver · AlgebraicGeometry.isUniversallyPureRelative_of_isProper · AlgebraicGeometry.isSchemeUniversallyPureRelative_of_isProper · AlgebraicGeometry.isPureRelative_iff_isFinite_schemeTheoreticSupport · AlgebraicGeometry.isUniversallyPureRelative_iff_isFinite_schemeTheoreticSupport · AlgebraicGeometry.isSchemePureRelative_iff_isFinite · AlgebraicGeometry.universallyPure_of_flat_geometricallyIntegral · AlgebraicGeometry.isUniversallyPureRelative_of_pushforward_isLocallyProjective

Section38.18 A criterion for purity#

Section 38.18 of the Stacks Project, Tag 05L2. 6 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05L3, a lemma

Tag 05L3 in the Stacks Project.

Stacks.RelativeAssassin.exists_specializes_mem_associatedPoints_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeAssassin/FlatFibreSpecialization.lean, line 273.

Stacks Project, Tag 05L3: a criterion for purity. Let f : X ⟶ S be locally of finite type and F a quasi-coherent 𝒪_X-module of finite type which is flat over S at every point of the fibre X_s. A point of Ass_{X/S}(F) which specializes to some point of X_s specializes to a point of X_s associated to the restriction of F to X_s.

theorem exists_specializes_mem_associatedPoints_fibre
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (s : S)
    (hflat : ∀ t : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s t))
    {x' : X} (hx' : x' ∈ Stacks.Divisors.relativeAssassin f F)
    (hmeets : ∃ t : f.fiber s, x' ⤳ f.fiberι s t) :
    ∃ x : f.fiber s, x' ⤳ f.fiberι s x ∧
      x ∈ Stacks.Divisors.associatedPoints
        ((Scheme.Modules.pullback (f.fiberι s)).obj F)
Tag 05L4, a lemma

Tag 05L4 in the Stacks Project.

AlgebraicGeometry.isPureAlong_iff_relativeAssassin_specializing_mem_range_of_associatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityCriterion.lean, line 603.

Stacks Project, Tag 05L4. Let f : X ⟶ S be of finite type, let ℱ be a finite type quasi-coherent 𝒪_X-module and let s ∈ S. Let (S', s') ⟶ (S, s) be an elementary étale neighbourhood and let g : X' ⟶ X and p : X' ⟶ S' form a commutative square over S' ⟶ S. Assume

  1. ℱ is flat over S at all points of X_s,
  2. p : X' ⟶ S' is of finite type,
  3. g^*ℱ is pure along X'_{s'},
  4. g : X' ⟶ X is étale, and
  5. g(X'_{s'}) contains Ass_{X_s}(ℱ_s).

Then ℱ is pure along X_s if and only if the image of X' ⟶ X ×_S S' contains the points of Ass_{X ×_S S'/S'}(ℱ ×_S S') lying over points of S' which specialize to s'.

The source states (5) as g(X') ⊇ Ass_{X_s}(ℱ_s). With that reading the statement is false, by Stacks.Examples.not_forall_isPureAlong_iff_of_associatedPoints_subset_range: take X = S, ℱ = 𝒪_S, S' = S ⨿ S with s' in the first copy and X' = S mapping onto the second copy. The proof of the source, which first replaces S by S', uses (5) for the fibre over s', as stated here.

Hypothesis (5) is moved to the fibre of X ×_S S' over s' by Tag 05DC (AlgebraicGeometry.mem_relativeAssassin_pullback_iff), and a point of that fibre is pinned down by its image in X (AlgebraicGeometry.pullbackLift_eq_fiberι_of_fst_eq).

public theorem isPureAlong_iff_relativeAssassin_specializing_mem_range_of_associatedPoints
    {X S X' : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (s : S) (U : EtaleNeighborhood S s) (hU : U.IsElementary)
    (p : X' ⟶ U.scheme) [LocallyOfFiniteType p] [QuasiCompact p]
    (g : X' ⟶ X) [Etale g] (hcomm : g ≫ f = p ≫ U.toBase)
    (hflat : ∀ x : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x))
    (hpure' : IsPureAlong
      ({ S := U.scheme
         X := X'
         f := p
         F := (Scheme.Modules.pullback g).obj F
         isFiniteType := SheafOfModules.pullback_isFiniteType g.toLRSHom.toShHom F
         isQuasicoherent := by
           have hF : F.IsQuasicoherent := inferInstance
           exact @SheafOfModules.modulePullback_isQuasicoherent X'.toRingedSpace
             X.toRingedSpace g.toLRSHom.toShHom F hF
         s := U.point } : PrePureSituation.{u}))
    (hass : ∀ z : f.fiber s,
      z ∈ Stacks.Divisors.associatedPoints ((Scheme.Modules.pullback (f.fiberι s)).obj F) →
        f.fiberι s z ∈ g '' (p ⁻¹' {U.point})) :
    IsPureAlong ({ S := S, X := X, f := f, F := F, s := s } : PrePureSituation.{u}) ↔
      ∀ x : pullback (C := Scheme.{u}) f U.toBase,
        x ∈ Stacks.Divisors.relativeAssassin (pullback.snd f U.toBase)
            ((Scheme.Modules.pullback (pullback.fst f U.toBase)).obj F) →
          pullback.snd f U.toBase x ⤳ U.point →
            x ∈ Set.range (pullback.lift g p hcomm)
Tag 05L5, a lemma

Tag 05L5 in the Stacks Project.

AlgebraicGeometry.isUniversallyPureAlong_of_isPureAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/UniversalPurityCriterion.lean, line 403.

Stacks Project, Tag 05L5. Let f : X ⟶ S be of finite type, let ℱ be a finite type quasi-coherent 𝒪_X-module, and let s : S. If ℱ is flat over S at every point of the fibre X_s and pure along X_s, then ℱ is universally pure along X_s.

The inputs are Tag 05L1, which produces an affine étale chart of the whole fibre with free sections after an elementary étale localization of the base, Tag 05K6, which makes that chart universally pure over the local base, Tag 05L4, which converts the resulting containment of the relative assassin into purity after an arbitrary base change, the unconditional half of Tag 05KL, which propagates that containment along a base change, and Tags 05J7 and 05J9, which transport purity and universal purity along the elementary étale neighbourhood and the localization.

public theorem isUniversallyPureAlong_of_isPureAlong
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (s : S)
    (hflat : ∀ x : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x))
    (hpure : IsPureAlong ({ S := S, X := X, f := f, F := F, s := s } : PrePureSituation.{u})) :
    IsUniversallyPureAlong ({ S := S, X := X, f := f, F := F, s := s } :
      PrePureSituation.{u})
Tag 05L6, a lemma

Tag 05L6 in the Stacks Project.

AlgebraicGeometry.isPureRelative_of_isUniversallyPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityIffUniversalPurity.lean, line 58. The attribute's comment: “the implication universally pure relative to S implies pure relative to S, with no flatness and no Noetherian hypothesis”.

Stacks Project, Tag 05L6, the implication which needs no hypothesis on the base: a finite type quasi-coherent module which is universally pure relative to the base is pure relative to the base, there being fewer impurity diagrams to exclude.

theorem isPureRelative_of_isUniversallyPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (h : IsUniversallyPureRelative f F) :
    IsPureRelative f F

AlgebraicGeometry.isUniversallyPureRelative_of_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityIffUniversalPurity.lean, line 69. The attribute's comment: “the implication pure relative to S implies universally pure relative to S, for a module flat over S, with no hypothesis on S”.

Stacks Project, Tag 05L6, the harder implication. Let f : X ⟶ S be of finite type and let ℱ be a finite type quasi-coherent 𝒪_X-module which is flat over S. If ℱ is pure relative to S then it is universally pure relative to S.

theorem isUniversallyPureRelative_of_isPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (hflat : IsFlatOver f.toLRSHom.toShHom F)
    (h : IsPureRelative f F) :
    IsUniversallyPureRelative f F

AlgebraicGeometry.isPureRelative_iff_isUniversallyPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityIffUniversalPurity.lean, line 81.

Stacks Project, Tag 05L6. Let f : X ⟶ S be of finite type and let ℱ be a finite type quasi-coherent 𝒪_X-module which is flat over S. Then ℱ is pure relative to S if and only if it is universally pure relative to S.

theorem isPureRelative_iff_isUniversallyPureRelative {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    IsPureRelative f F ↔ IsUniversallyPureRelative f F

AlgebraicGeometry.isPureRelative_iff_isUniversallyPureRelative_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityIffUniversalPurity.lean, line 94. The attribute's comment: “a strengthening over a locally Noetherian base: Tag 05J8 replaces Tag 05L5 and needs no flatness, so the flatness hypothesis of the source is dropped here”.

Stacks Project, Tag 05L6 over a locally Noetherian base, where the flatness hypothesis is unnecessary. Let f : X ⟶ S be of finite type and let ℱ be a finite type quasi-coherent 𝒪_X-module. If S is locally Noetherian then ℱ is pure relative to S if and only if it is universally pure relative to S.

theorem isPureRelative_iff_isUniversallyPureRelative_of_isLocallyNoetherian
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    [IsLocallyNoetherian S] (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] :
    IsPureRelative f F ↔ IsUniversallyPureRelative f F
Tag 05MA, a lemma

Tag 05MA in the Stacks Project.

AlgebraicGeometry.exists_stage_isPureAlong_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityCriterionLimits.lean, line 340. The attribute's comment: “assuming the limit descent as hdescend and the purity step as hstage”.

Stacks Project, Tag 05MA. Let (S_i) be an inverse system of affine schemes over a directed index with limit S, let s ∈ S with images s_i, let f : X ⟶ S be of finite presentation and let ℱ be a quasi-coherent 𝒪_X-module of finite presentation which is pure along X_s and flat over S at every point of X_s. Then the whole situation descends to a finite stage: some i carries a finite-presentation morphism X_i ⟶ S_i and a finitely presented quasi-coherent module ℱ_i which is pure along (X_i)_{s_i} and flat over S_i at every point of that fibre, with X = X_i ×_{S_i} S and ℱ the pullback of ℱ_i.

The descent of the morphism, the module, the open flat locus and the flatness, which is Stacks Limits 01ZM, 01ZR, 01ZS and 05LY, is the hypothesis hdescend; the passage of purity to a finite stage, which is the second half of the proof of the source and uses Stacks 05KW, 05K6, 05L4, 05KR and Limits 05F4, is the hypothesis hstage.

public theorem exists_stage_isPureAlong_of_isLimit
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) [∀ i : I, IsAffine (D.obj i)] (c : Cone D) (_hc : IsLimit c)
    {X : Scheme.{u}} (f : X ⟶ c.pt)
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation] [F.IsFiniteType] (s : c.pt)
    (_hpure : IsPureAlong ({ S := c.pt, X := X, f := f, F := F,
                             s := s } : PrePureSituation.{u}))
    (_hflat : ∀ x : f.fiber s, IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x))
    (hdescend : ∃ (i : I) (Xi : Scheme.{u}) (fi : Xi ⟶ D.obj i)
      (_ : LocallyOfFinitePresentation fi) (_ : QuasiCompact fi) (_ : QuasiSeparated fi)
      (Fi : Xi.Modules) (_ : Fi.IsFiniteType) (_ : Fi.IsQuasicoherent)
      (_ : Fi.IsFinitePresentation) (a : X ⟶ Xi),
      IsPullback a f fi (c.π.app i) ∧ Nonempty (F ≅ (Scheme.Modules.pullback a).obj Fi) ∧
        ∀ x : fi.fiber (c.π.app i s),
          IsFlatOverAt fi.toLRSHom.toShHom Fi (fi.fiberι (c.π.app i s) x))
    (hstage : ∀ (i : I) (Xi : Scheme.{u}) (fi : Xi ⟶ D.obj i)
      (_ : LocallyOfFinitePresentation fi) (_ : QuasiCompact fi) (_ : QuasiSeparated fi)
      (Fi : Xi.Modules) (_ : Fi.IsFiniteType) (_ : Fi.IsQuasicoherent)
      (_ : Fi.IsFinitePresentation) (a : X ⟶ Xi), IsPullback a f fi (c.π.app i) →
      Nonempty (F ≅ (Scheme.Modules.pullback a).obj Fi) →
      (∀ x : fi.fiber (c.π.app i s),
        IsFlatOverAt fi.toLRSHom.toShHom Fi (fi.fiberι (c.π.app i s) x)) →
      ∃ (j : I) (e : j ⟶ i) (_ : LocallyOfFiniteType (pullback.snd fi (D.map e)))
        (_ : QuasiCompact (pullback.snd fi (D.map e)))
        (_ : ((Scheme.Modules.pullback (pullback.fst fi (D.map e))).obj Fi).IsFiniteType)
        (_ : ((Scheme.Modules.pullback (pullback.fst fi (D.map e))).obj Fi).IsQuasicoherent),
        IsPureAlong ({ S := D.obj j, X := pullback fi (D.map e),
                       f := pullback.snd fi (D.map e),
                       F := (Scheme.Modules.pullback (pullback.fst fi (D.map e))).obj Fi,
                       s := c.π.app j s } : PrePureSituation.{u})) :
    ∃ (i : I) (Xi : Scheme.{u}) (fi : Xi ⟶ D.obj i) (_ : LocallyOfFinitePresentation fi)
      (_ : QuasiCompact fi) (_ : QuasiSeparated fi) (Fi : Xi.Modules) (_ : Fi.IsFiniteType)
      (_ : Fi.IsQuasicoherent) (_ : Fi.IsFinitePresentation) (a : X ⟶ Xi),
      IsPullback a f fi (c.π.app i) ∧ Nonempty (F ≅ (Scheme.Modules.pullback a).obj Fi) ∧
        (∀ x : fi.fiber (c.π.app i s),
          IsFlatOverAt fi.toLRSHom.toShHom Fi (fi.fiberι (c.π.app i s) x)) ∧
        IsPureAlong ({ S := D.obj i, X := Xi, f := fi, F := Fi,
                       s := c.π.app i s } : PrePureSituation.{u})

AlgebraicGeometry.exists_stage_isPureAlong_of_isLimit_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityLimitStage.lean, line 612.

Stacks Project, Tag 05MA. Let I be a directed set, let (S_k) be an inverse system of affine schemes indexed by I with limit S, let s be a point of S with images s_k, let f : X ⟶ S be of finite presentation and let ℱ be a quasi-coherent 𝒪_X-module of finite presentation which is pure along X_s and flat over S at every point of X_s. Then the whole situation descends to a finite stage: some k carries a finite-presentation morphism X_k ⟶ S_k and a finitely presented quasi-coherent module ℱ_k which is pure along (X_k)_{s_k} and flat over S_k at every point of that fibre, with X = X_k ×_{S_k} S and ℱ the pullback of ℱ_k.

The descent of the morphism, of the module and of the flatness over the open locus where it holds — Stacks Limits 01ZM, 01ZR, 01Z4 and 05LY — is AlgebraicGeometry.exists_stage_isFlatOverAt_fiber_of_isLimit; the passage of purity to a finite stage, which is the rest of the proof of the source, is AlgebraicGeometry.exists_stage_isPureAlong.

public theorem exists_stage_isPureAlong_of_isLimit_directed {I : Type u} [Preorder I]
    [IsDirected I (· ≤ ·)] [Nonempty I] (D : Iᵒᵖ ⥤ Scheme.{u}) [∀ k : Iᵒᵖ, IsAffine (D.obj k)]
    (c : Cone D) (hc : IsLimit c) {X : Scheme.{u}} (f : X ⟶ c.pt)
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsFinitePresentation] [F.IsQuasicoherent] (s : c.pt)
    (hpure : IsPureAlong ({ S := c.pt, X := X, f := f, F := F, s := s } : PrePureSituation.{u}))
    (hflat : ∀ x : f.fiber s,
      IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s x)) :
    ∃ (k : I) (Xk : Scheme.{u}) (fk : Xk ⟶ D.obj (op k))
      (_ : LocallyOfFinitePresentation fk) (_ : QuasiCompact fk) (_ : QuasiSeparated fk)
      (Fk : Xk.Modules) (_ : Fk.IsQuasicoherent) (_ : Fk.IsFinitePresentation)
      (_ : Fk.IsFiniteType) (a : X ⟶ Xk),
      IsPullback a f fk (c.π.app (op k)) ∧ Nonempty (F ≅ (Scheme.Modules.pullback a).obj Fk) ∧
        (∀ x : fk.fiber (c.π.app (op k) s),
          IsFlatOverAt fk.toLRSHom.toShHom Fk (fk.fiberι (c.π.app (op k) s) x)) ∧
        IsPureAlong ({ S := D.obj (op k), X := Xk, f := fk, F := Fk,
                       s := c.π.app (op k) s } : PrePureSituation.{u})
Tag 05MC, a lemma

Tag 05MC in the Stacks Project.

AlgebraicGeometry.isOpen_setOf_isPureAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/PureModules/PurityCriterionLimits.lean, line 162. The attribute's comment: “using Stacks 05KR, proved outright in this library”.

Stacks Project, Tag 05MC. For a morphism f : X ⟶ S of finite presentation and a quasi-coherent 𝒪_X-module ℱ of finite presentation which is flat over S, the set of points s ∈ S at which ℱ is pure along the fibre X_s is open in S.

The local constructibility of the fibrewise containment locus, Tag 05KR, which the argument applies to the base change of f, is proved outright in this library.

public theorem isOpen_setOf_isPureAlong
    {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFinitePresentation f] [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFinitePresentation] [F.IsFiniteType]
    (hflat : ∀ x : X, IsFlatOverAt f.toLRSHom.toShHom F x) :
    IsOpen {s : S | IsPureAlong ({ S := S, X := X, f := f, F := F,
                                   s := s } : PrePureSituation.{u})}
Sources
LeanStacks.RelativeAssassin.exists_specializes_mem_associatedPoints_fibre · AlgebraicGeometry.isPureAlong_iff_relativeAssassin_specializing_mem_range_of_associatedPoints · AlgebraicGeometry.isUniversallyPureAlong_of_isPureAlong · AlgebraicGeometry.isPureRelative_of_isUniversallyPureRelative · AlgebraicGeometry.isUniversallyPureRelative_of_isPureRelative · AlgebraicGeometry.isPureRelative_iff_isUniversallyPureRelative · AlgebraicGeometry.isPureRelative_iff_isUniversallyPureRelative_of_isLocallyNoetherian · AlgebraicGeometry.exists_stage_isPureAlong_of_isLimit

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.