77 Flatness on Algebraic Spaces

Chapter 77 of the Stacks Project, Flatness on Algebraic Spaces, Tag 0CU3: the 12 sections of its 13 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 70 tags are carried by 165 declarations of the repository (all in StacksFrontier).

Section77.2 Impurities #

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

Tag 0CV6, a situation

Tag 0CV6 in the Stacks Project.

AlgebraicGeometry.Space.PrePureSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/Impurities.lean, line 112.

Stacks 0CV6. The standing situation for impurities: a finite type, decent morphism f : X ⟶ Y of algebraic spaces over S, a finite type quasi-coherent module F on the source, and a point y of the target.

structure PrePureSituation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)

Tag 0CV7, an equation

Tag 0CV7 in the Stacks Project.

AlgebraicGeometry.Space.ImpurityDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/Impurities.lean, line 145.

Stacks 0CV7. The diagram from which an impurity is defined: a scheme T with a morphism g : T ⟶ Y to the target, a specialization t' ⤳ t in T whose specialized point lies over the chosen point y, and a point ξ of the base change X_T = T ×_Y X lying over the generalization t'.

structure ImpurityDiagram (P : PrePureSituation.{u, m} B S hS)

Tag 0CV8, a definition

Tag 0CV8 in the Stacks Project.

AlgebraicGeometry.Space.ImpurityDiagram.IsImpurity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/Impurities.lean, line 250.

Stacks 0CV8. The diagram defines an impurity of F above y when the distinguished point ξ of the base change X_T lies in the relative assassin Ass_{X_T/T}(F_T) and the point t of T does not lie in the image under f_T of the closure of {ξ}.

noncomputable def IsImpurity : Prop

Tag 0CV9, a lemma

Tag 0CV9 in the Stacks Project.

AlgebraicGeometry.Space.AffineLimitPresentation.exists_isImpurity_stageDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ImpurityAffineLimitDescent.lean, line 1017.

Stacks 0CV9. In Situation 0CV6, let (g : T ⟶ Y, t' ⤳ t, ξ) be an impurity of ℱ above y and let T = lim_{i} Tᵢ be a directed limit of affine schemes over Y. Then for some stage i the triple (Tᵢ ⟶ Y, t'ᵢ ⤳ tᵢ, ξᵢ) is an impurity of ℱ above y, where the three points are the images of t', t and ξ under the canonical projections.

theorem exists_isImpurity_stageDiagram (hD : D.IsImpurity) :
    ∃ i : A.J, (A.stageDiagram i).IsImpurity

Tag 0CVA, a lemma

Tag 0CVA in the Stacks Project.

AlgebraicGeometry.Space.exists_isImpurity_baseChange_etale_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ImpurityFlatAscent.lean, line 178.

Stacks 0CVA. Let (Y', y') ⟶ (Y, y) be a morphism of pointed algebraic spaces over S with Y' ⟶ Y flat at y'. An impurity (T ⟶ Y, t' ⤳ t, ξ) of F above y gives an impurity (T₁ ⟶ Y', t₁' ⤳ t₁, ξ₁) of the pullback F' of F to X' = Y' ×_Y X above y' such that T₁ is étale over Y' ×_Y T: the structure morphism T₁ ⟶ Y' is an étale morphism T₁ ⟶ Y' ×_Y T followed by the projection.

theorem exists_isImpurity_baseChange_etale_of_isFlatAt (P : PrePureSituation.{u, u} B S hS)
    (c : PointedOver P) (hflat : IsFlatAt B S hS c.g c.y')
    (D : ImpurityDiagram P) (hD : D.IsImpurity) :
    ∃ (E : ImpurityDiagram c.baseChange) (e : yoneda.obj E.T ⟶ pullback c.g D.g),
      IsEtale B S hS e ∧ e ≫ pullback.fst c.g D.g = E.g ∧ E.IsImpurity

AlgebraicGeometry.Space.exists_isImpurity_pointedBaseChange_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ImpurityFlatAscent.lean, line 193. The attribute's comment: “granting hwitness, the choice of field-valued representative that Stacks 05DC supplies; the binder is unused, that representative always existing by ImpurityDiagram.hasFibreWitnessAboveGeneralization”.

Stacks 0CVA, with the field-valued representative of Stacks 05DC as a hypothesis. That hypothesis always holds, by AlgebraicGeometry.Space.ImpurityDiagram.hasFibreWitnessAboveGeneralization, and is not used: the statement is AlgebraicGeometry.Space.exists_isImpurity_baseChange_etale_of_isFlatAt.

theorem exists_isImpurity_pointedBaseChange_of_isFlatAt (P : PrePureSituation.{u, u} B S hS)
    (c : PointedOver P) (hflat : IsFlatAt B S hS c.g c.y')
    (D : ImpurityDiagram P) (hD : D.IsImpurity)
    (hwitness : D.HasFibreWitnessAboveGeneralization) :
    ∃ (E : ImpurityDiagram c.baseChange) (e : yoneda.obj E.T ⟶ pullback c.g D.g),
      IsEtale B S hS e ∧ e ≫ pullback.fst c.g D.g = E.g ∧ E.IsImpurity

Tag 0CVB, a lemma

Tag 0CVB in the Stacks Project.

AlgebraicGeometry.Space.exists_isImpurity_isQuasiFiniteAt_of_exists_isImpurity_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 259. The attribute's comment: “condition (3) implies condition (4)”.

Stacks 0CVB, condition (3) implies condition (4). An impurity of F above y whose structure morphism T ⟶ Y is étale, so that (T, t) ⟶ (Y, y) is an étale neighbourhood, is an impurity whose structure morphism is quasi-finite at t: an étale morphism of algebraic spaces is locally quasi-finite by Stacks 03XU.

The implications (1) ⟹ (3) and (1) ⟹ (4) are AlgebraicGeometry.Space.exists_isImpurity_isEtale_of_isImpurity_strictHenselization and AlgebraicGeometry.Space.exists_isImpurity_isQuasiFiniteAt_of_isImpurity_strictHenselization.

theorem exists_isImpurity_isQuasiFiniteAt_of_exists_isImpurity_isEtale
    (P : PrePureSituation.{u, u} B S hS)
    (h : ∃ D : ImpurityDiagram P, IsEtale B S hS D.g ∧ D.IsImpurity) :
    ∃ D : ImpurityDiagram P, IsQuasiFiniteAt B S hS D.g D.t ∧ D.IsImpurity

AlgebraicGeometry.Space.hasImpurityOverStrictHenselization_iff_hasRelativeAssociatedPointAvoidingClosedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/StrictHenselizationConditionsTwo.lean, line 207. The attribute's comment: “(1) ⟺ (2), with (2) corrected as in AlgebraicGeometry.Space.HasRelativeAssociatedPointAvoidingClosedFibre”.

Stacks 0CVB, (1) ⟺ (2). For a geometric point ȳ of Y lying over y, there is an impurity of ℱ above y over the strict henselization Y^{sh} exactly when some point of the relative assassin of ℱ^{sh} does not specialize to a point of the closed fibre.

theorem hasImpurityOverStrictHenselization_iff_hasRelativeAssociatedPointAvoidingClosedFibre
    (hybar : ybar.LiesOver P.y) :
    HasImpurityOverStrictHenselization P ybar ↔
      HasRelativeAssociatedPointAvoidingClosedFibre P ybar

AlgebraicGeometry.Space.tfae_hasImpurityOverStrictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/StrictHenselizationTFAE.lean, line 46. The attribute's comment: “condition (2) in the corrected reading recorded in the note of StrictHenselizationConditions: some associated point does not specialize into the closed fibre”.

Stacks 0CVB. In Situation 0CV6, for a geometric point ȳ of Y lying over y, the four conditions of the source are equivalent: an impurity of ℱ above y over Y^{sh} with specialized point ȳ; a point of Ass_{X^{sh}/Y^{sh}}(ℱ^{sh}) not specializing into the closed fibre; an impurity over an étale neighbourhood of y; an impurity whose structure morphism is quasi-finite at its specialized point.

theorem tfae_hasImpurityOverStrictHenselization (P : PrePureSituation.{u, u} B S hS)
    (ybar : GeometricPoint B S hS P.Y) (hybar : ybar.LiesOver P.y) :
    [HasImpurityOverStrictHenselization P ybar,
      HasRelativeAssociatedPointAvoidingClosedFibre P ybar,
      HasImpurityOverEtaleNeighborhood P,
      HasImpurityQuasiFiniteAtPoint P].TFAE

Sources

LeanAlgebraicGeometry.Space.PrePureSituation · AlgebraicGeometry.Space.ImpurityDiagram · AlgebraicGeometry.Space.ImpurityDiagram.IsImpurity · AlgebraicGeometry.Space.AffineLimitPresentation.exists_isImpurity_stageDiagram · AlgebraicGeometry.Space.exists_isImpurity_baseChange_etale_of_isFlatAt · AlgebraicGeometry.Space.exists_isImpurity_pointedBaseChange_of_isFlatAt · AlgebraicGeometry.Space.exists_isImpurity_isQuasiFiniteAt_of_exists_isImpurity_isEtale · AlgebraicGeometry.Space.hasImpurityOverStrictHenselization_iff_hasRelativeAssociatedPointAvoidingClosedFibre

Section77.3 Relatively pure modules #

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

Tag 0CVD, a definition

Tag 0CVD in the Stacks Project.

AlgebraicGeometry.Space.IsSpacePureAbove, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 289. The attribute's comment: “part (3)”.

Stacks 0CVD, part (3). The algebraic space X is pure above y when its structure sheaf 𝒪_X is pure above y.

The module of the situation plays no role: the condition is part (1) for the situation with the same morphism and the same chosen point whose module is 𝒪_X.

def IsSpacePureAbove (P : PrePureSituation.{u, u} B S hS) : Prop

AlgebraicGeometry.Space.IsSpacePureRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 299. The attribute's comment: “part (6)”.

Stacks 0CVD, part (6). The algebraic space X is Y-pure, or pure relative to Y, when its structure sheaf 𝒪_X is pure relative to Y.

This is part (5) for the situation whose module is 𝒪_X; neither the module nor the chosen point of the situation plays a role, the latter because purity relative to Y varies it over all of |Y|.

def IsSpacePureRelative (P : PrePureSituation.{u, u} B S hS) : Prop

AlgebraicGeometry.Space.IsPureAbove, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 216. The attribute's comment: “part (1), as the failure of condition (4) of Stacks 0CVB”.

Stacks 0CVD, part (1). The module is pure above y when no impurity of F above y has its structure morphism T ⟶ Y quasi-finite at t.

This is the failure of condition (4) of Stacks 0CVB, which is the condition the proof of Stacks 0CVF works with.

def IsPureAbove (P : PrePureSituation.{u, u} B S hS) : Prop

AlgebraicGeometry.Space.IsUniversallyPureAbove, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 222. The attribute's comment: “part (2)”.

Stacks 0CVD, part (2). The module is universally pure above y when there is no impurity of F above y at all.

def IsUniversallyPureAbove (P : PrePureSituation.{u, u} B S hS) : Prop

AlgebraicGeometry.Space.IsUniversallyPureRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 234. The attribute's comment: “part (4)”.

Stacks 0CVD, part (4). The module is universally pure relative to Y when it is universally pure above every point of Y.

The chosen point of the situation is irrelevant: the condition varies it over all of |Y|.

def IsUniversallyPureRelative (P : PrePureSituation.{u, u} B S hS) : Prop

AlgebraicGeometry.Space.IsPureRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 242. The attribute's comment: “part (5)”.

Stacks 0CVD, part (5). The module is pure relative to Y when it is pure above every point of Y.

The chosen point of the situation is irrelevant: the condition varies it over all of |Y|.

def IsPureRelative (P : PrePureSituation.{u, u} B S hS) : Prop

Tag 0CVE, a lemma

Tag 0CVE in the Stacks Project.

AlgebraicGeometry.Space.isUniversallyPureAbove_iff_forall_baseChange_isPureAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 576. The attribute's comment: “the equivalence left implicit by the source”.

Stacks 0CVE. A finite type quasi-coherent module is universally pure above y exactly when, for every morphism (Y', y') ⟶ (Y, y) of pointed algebraic spaces, its base change F_{Y'} is pure above y'.

The source lists the two conditions without the connective; they are equivalent, as the statement of the analogous Stacks 05J6 for schemes makes explicit. The consequence the source draws for purity relative to the whole base is isUniversallyPureRelative_iff_forall_baseChange_isPureRelative.

Both directions are formal, as the source says: an impurity of a base change is an impurity of F by isImpurity_alongBaseChange_iff, and conversely an impurity diagram (T, t' ⤳ t, ξ) of F is an impurity of the base change along (T, t) ⟶ (Y, y) itself, whose structure morphism is the identity and hence quasi-finite at t.

theorem isUniversallyPureAbove_iff_forall_baseChange_isPureAbove
    (P : PrePureSituation.{u, u} B S hS) :
    IsUniversallyPureAbove P ↔ ∀ c : PointedOver P, IsPureAbove c.baseChange

AlgebraicGeometry.Space.isUniversallyPureRelative_iff_forall_baseChange_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 677. The attribute's comment: “the 'in particular' clause: universally pure relative to Y iff every base change is pure relative to Y'”.

Stacks 0CVE, the closing clause. The module is universally pure relative to Y exactly when, for every morphism Y' ⟶ Y of algebraic spaces, its base change F_{Y'} is pure relative to Y'.

This is formal, as the source says, and is the pointwise equivalence AlgebraicGeometry.Space.isUniversallyPureAbove_iff_forall_baseChange_isPureAbove read at every point of the base at once: a pointed morphism (Y', y') ⟶ (Y, y) is a morphism Y' ⟶ Y together with a point y' of Y' whose image is y, and the two sides quantify over all y and all such y' in the two possible orders.

theorem isUniversallyPureRelative_iff_forall_baseChange_isPureRelative
    (P : PrePureSituation.{u, u} B S hS) :
    IsUniversallyPureRelative P ↔
      ∀ (Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hY' : IsAlgebraicSpace B S hS Y')
        (g : Y' ⟶ P.Y), P.IsPureRelativeAlong hY' g

Tag 0CVF, a lemma

Tag 0CVF in the Stacks Project.

AlgebraicGeometry.Space.isPureAbove_baseChange_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/RelativelyPureModules.lean, line 595.

Stacks 0CVF. If (Y', y') ⟶ (Y, y) is a morphism of pointed algebraic spaces with Y' ⟶ Y quasi-finite at y', and the module is pure above y, then its base change F_{Y'} is pure above y'.

An impurity of F_{Y'} above y' whose structure morphism is quasi-finite at t is an impurity of F above y whose structure morphism is quasi-finite at t, by isQuasiFiniteAt_comp, the pointwise form of Stacks 03XK that the source appeals to.

Purity above y is written out in the hypothesis rather than named: the condition stated there is AlgebraicGeometry.Space.IsPureAbove of Stacks 0CVD part (1), definitionally and on the nose, so a consumer holding that predicate may pass it directly.

theorem isPureAbove_baseChange_of_isQuasiFiniteAt (P : PrePureSituation.{u, u} B S hS)
    (c : PointedOver P)
    (hqf : IsQuasiFiniteAt B S hS c.g c.y')
    (hP : ∀ D : ImpurityDiagram P, IsQuasiFiniteAt B S hS D.g D.t → ¬ D.IsImpurity) :
    IsPureAbove c.baseChange

Tag 0CVG, a lemma

Tag 0CVG in the Stacks Project.

AlgebraicGeometry.Space.isPureAbove_of_isFlatAt, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ImpurityFlatAscent.lean, line 209. The attribute's comment: “part (1)”.

Stacks 0CVG, part (1). In the situation of Stacks 0CV6, let (Y₁, y₁) ⟶ (Y, y) be a morphism of pointed algebraic spaces with Y₁ ⟶ Y flat at y₁. If the base change F_{Y₁} is pure above y₁, then F is pure above y. This is AlgebraicGeometry.Space.isPureAbove_of_isPureAbove_baseChange_of_isFlatAt.

alias isPureAbove_of_isFlatAt

AlgebraicGeometry.Space.isUniversallyPureAbove_of_isFlatAt, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ImpurityFlatAscent.lean, line 217. The attribute's comment: “part (2)”.

Stacks 0CVG, part (2). In the situation of Stacks 0CV6, let (Y₁, y₁) ⟶ (Y, y) be a morphism of pointed algebraic spaces with Y₁ ⟶ Y flat at y₁. If the base change F_{Y₁} is universally pure above y₁, then F is universally pure above y. This is AlgebraicGeometry.Space.isUniversallyPureAbove_of_isUniversallyPureAbove_baseChange_of_isFlatAt.

alias isUniversallyPureAbove_of_isFlatAt

AlgebraicGeometry.Space.isPureAbove_of_isPureAbove_baseChange_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityFlatDescent.lean, line 547. The attribute's comment: “part (1)”.

Stacks 0CVG, part (1). If (Y₁, y₁) ⟶ (Y, y) is a morphism of pointed algebraic spaces with Y₁ ⟶ Y flat at y₁ and the base change F_{Y₁} is pure above y₁, then F is pure above y.

theorem isPureAbove_of_isPureAbove_baseChange_of_isFlatAt (P : PrePureSituation.{u, u} B S hS)
    (c : PointedOver P) (hflat : IsFlatAt B S hS c.g c.y')
    (hpure : IsPureAbove c.baseChange) :
    IsPureAbove P

Tag 0CVH, a lemma

Tag 0CVH in the Stacks Project.

AlgebraicGeometry.Space.ClosedSubspaceModule.isPureAbove_situation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityClosedImmersion.lean, line 540. The attribute's comment: “pure above y, granting as hin affine base change (Stacks 02KG) on the base changes of the situation”.

Stacks 0CVH, purity above y. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. Then 𝒢 is pure above y exactly when ℱ is.

An impurity of 𝒢 above y whose structure morphism is quasi-finite at t is such an impurity of ℱ above y, and conversely; this is Stacks 0CV4 on the base changes, together with the fact that Z_T ⟶ X_T is a closed embedding on points.

The inputs of AlgebraicGeometry.Space.ClosedSubspaceModule.BaseChangeInput — affine base change on the base changes — are hypotheses.

theorem isPureAbove_situation_iff
    (hin : c.BaseChangeInput) :
    IsPureAbove c.situation ↔ IsPureAbove P

AlgebraicGeometry.Space.ClosedSubspaceModule.isUniversallyPureAbove_situation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityClosedImmersion.lean, line 563. The attribute's comment: “universally pure above y, granting as hin affine base change (Stacks 02KG) on the base changes of the situation”.

Stacks 0CVH, universal purity above y. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. Then 𝒢 is universally pure above y exactly when ℱ is.

An impurity of 𝒢 above y is an impurity of ℱ above y, and conversely.

The inputs of AlgebraicGeometry.Space.ClosedSubspaceModule.BaseChangeInput — affine base change on the base changes — are hypotheses.

theorem isUniversallyPureAbove_situation_iff
    (hin : c.BaseChangeInput) :
    IsUniversallyPureAbove c.situation ↔ IsUniversallyPureAbove P

AlgebraicGeometry.Space.ClosedSubspaceModule.isPureAbove_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityClosedImmersionBaseChange.lean, line 70. The attribute's comment: “pure above y”.

Stacks 0CVH, purity above y. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. Then 𝒢 is pure above y if and only if ℱ is pure above y.

theorem isPureAbove_iff : IsPureAbove c.situation ↔ IsPureAbove P

AlgebraicGeometry.Space.ClosedSubspaceModule.isUniversallyPureAbove_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityClosedImmersionBaseChange.lean, line 78. The attribute's comment: “universally pure above y”.

Stacks 0CVH, universal purity above y. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. Then 𝒢 is universally pure above y if and only if ℱ is universally pure above y.

theorem isUniversallyPureAbove_iff :
    IsUniversallyPureAbove c.situation ↔ IsUniversallyPureAbove P

Tag 0CVI, a lemma

Tag 0CVI in the Stacks Project.

AlgebraicGeometry.Space.isUniversallyPureAbove_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 171. The attribute's comment: “part (2): a finite type quasi-coherent module on the source of a proper morphism is universally pure above every point of the target”.

Stacks 0CVI, part (2). In the situation of Stacks 0CV6, if f : X ⟶ Y is proper then the module ℱ is universally pure above y.

A proper morphism is universally closed, and a universally closed morphism admits no impurity diagram. Since the point y of the situation is arbitrary, this is purity of ℱ relative to Y.

theorem isUniversallyPureAbove_of_isProper (P : PrePureSituation.{u, u} B S hS)
    (hf : IsProper B S hS P.f) : IsUniversallyPureAbove P

AlgebraicGeometry.Space.ClosedSubspaceModule.isUniversallyPureAbove_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 190. The attribute's comment: “part (1) in general form, taking the closed-immersion presentation of the module as data”.

Stacks 0CVI, part (1), in general form. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. If the composite Z ⟶ Y is proper, then ℱ is universally pure above y.

This is part (2) applied to the situation on Z, transferred to ℱ by Stacks 0CVH. The source states the hypothesis as properness of the support of ℱ over Y and then reduces to part (2) exactly this way, at the scheme-theoretic support; see AlgebraicGeometry.Space.isUniversallyPureAbove_of_isProper_schemeTheoreticSupport.

The input of Stacks 0CVH, affine base change on the base changes of the situation, is AlgebraicGeometry.Space.ClosedSubspaceModule.baseChangeInput.

theorem ClosedSubspaceModule.isUniversallyPureAbove_of_isProper
    {P : PrePureSituation.{u, u} B S hS} (c : ClosedSubspaceModule P)
    (hZY : IsProper B S hS (c.i.hom ≫ P.f)) :
    IsUniversallyPureAbove P

AlgebraicGeometry.Space.isUniversallyPureAbove_of_isProper_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 237. The attribute's comment: “part (1) at the scheme-theoretic support, naming the support's closed-subspace data”.

Stacks 0CVI, part (1). In the situation of Stacks 0CV6, if the scheme-theoretic support of ℱ is proper over Y, then ℱ is universally pure above y.

This is the general form above at the closed-immersion presentation of ℱ furnished by its scheme-theoretic support, Stacks 07U1, and the module on it of Stacks 07U0.

The two arguments hZ and hid are not assumptions about the geometry but the closed-subspace data of the scheme-theoretic support, which AlgebraicGeometry.Space.exists_isClosedSubspace_schemeTheoreticSupport produces from quasi-coherence of the module together with its finite type in the sectionwise sense of Stacks 03DL(5); they are taken as arguments because every other hypothesis here, the properness assumption included, is stated about the closed subspace they exhibit.

theorem isUniversallyPureAbove_of_isProper_schemeTheoreticSupport
    (P : PrePureSituation.{u, u} B S hS)
    (hZ : IsClosedSubspace B S hS (schemeTheoreticSupport B S hS P.sourceSpace P.F))
    (hid : definingIdealSheaf B S hS P.sourceSpace
        ⟨schemeTheoreticSupport B S hS P.sourceSpace P.F, hZ⟩ =
      annihilatorIdealSheaf B S hS P.sourceSpace P.F)
    (hZY : IsProper B S hS ((closedSubspaceInclusion B S hS P.sourceSpace
      ⟨schemeTheoreticSupport B S hS P.sourceSpace P.F, hZ⟩).hom ≫ P.f)) :
    IsUniversallyPureAbove P

AlgebraicGeometry.Space.isUniversallyPureAbove_structure_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProper.lean, line 317. The attribute's comment: “part (3): the source of a proper decent morphism is universally pure above every point of the target”.

Stacks 0CVI, part (3). If f : X ⟶ Y is a proper decent morphism of algebraic spaces over S, then X is universally pure above every point of Y, that is, universally pure relative to Y.

This is part (2) for the situation whose module is the structure sheaf of X.

theorem isUniversallyPureAbove_structure_of_isProper
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hdec : IsDecent B S hS f) (hf : IsProper B S hS f) (y : points B S hS Y) :
    IsUniversallyPureAbove
      (structurePrePureSituation hX hY f (IsProper.isFiniteType B S hS hf) hdec y)

AlgebraicGeometry.Space.ClosedSubspaceModule.isUniversallyPureAbove_of_isProper_comp, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProperSupport.lean, line 72. The attribute's comment: “part (1), for any presentation of the module as the direct image along a closed immersion whose composite to the target is proper”.

Stacks 0CVI, part (1), for a closed-immersion presentation of the module. In the situation of Stacks 0CV6, let i : Z ⟶ X be a closed immersion and suppose ℱ = i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢. If the composite Z ⟶ Y is proper, then ℱ is universally pure above y.

This is part (2) applied to the situation on Z, transferred to ℱ by Stacks 0CVH; it is AlgebraicGeometry.Space.ClosedSubspaceModule.isUniversallyPureAbove_of_isProper.

alias ClosedSubspaceModule.isUniversallyPureAbove_of_isProper_comp

AlgebraicGeometry.Space.isUniversallyPureAbove_of_isProper_supportSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityProperSupport.lean, line 105. The attribute's comment: “part (1): a finite type quasi-coherent module whose scheme-theoretic support is proper over the target is universally pure above every point of the target”.

Stacks 0CVI, part (1). In the situation of Stacks 0CV6, if the support of ℱ is proper over Y, then ℱ is universally pure above y; the point y being arbitrary, ℱ is universally pure relative to Y.

The support is the scheme-theoretic support Z of Stacks 07U1, and properness over Y is properness of the composite Z ⟶ X ⟶ Y. The proof is the source's: by Stacks 07U0 the module is i_*𝒢 for a finite type quasi-coherent 𝒪_Z-module 𝒢, and the closed-immersion form above applies.

theorem isUniversallyPureAbove_of_isProper_supportSubspace
    (P : PrePureSituation.{u, u} B S hS)
    (hZY : IsProper B S hS
      ((closedSubspaceInclusion B S hS P.sourceSpace P.supportSubspace).hom ≫ P.f)) :
    IsUniversallyPureAbove P

Sources

LeanAlgebraicGeometry.Space.IsSpacePureAbove · AlgebraicGeometry.Space.IsSpacePureRelative · AlgebraicGeometry.Space.IsPureAbove · AlgebraicGeometry.Space.IsUniversallyPureAbove · AlgebraicGeometry.Space.IsUniversallyPureRelative · AlgebraicGeometry.Space.IsPureRelative · AlgebraicGeometry.Space.isUniversallyPureAbove_iff_forall_baseChange_isPureAbove · AlgebraicGeometry.Space.isUniversallyPureRelative_iff_forall_baseChange_isPureRelative

Section77.4 Flat finite type modules #

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

Tag 0CWJ, a lemma

Tag 0CWJ in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_etale_completeDevissage_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/CompleteDevissageEtaleCover.lean, line 318. The attribute's comment: “the full statement, proved from the source's hypotheses; nothing is assumed”.

Stacks Project, Tag 0CWJ. Let X ⟶ Y be a finite type morphism of algebraic spaces over S, let F be a finite type quasi-coherent 𝒪_X-module and let y be a point of Y. There are an étale morphism q : (Y', y') ⟶ (Y, y) with Y' an affine scheme, and étale morphisms hᵢ : Wᵢ ⟶ X_{Y'} = Y' ×_Y X, i = 1, …, n, from schemes Wᵢ, such that for each i the pullback Fᵢ of F to Wᵢ (its restriction to the étale chart Wᵢ ⟶ X_{Y'} ⟶ X) has a complete dévissage Fᵢ/Wᵢ/Y' over y', the morphism Wᵢ ⟶ Y' being the aᵢ with hᵢ ≫ pr₁ = aᵢ, and such that every point of X_{Y'} lying over y' is in the image of some hᵢ, that is, |(X_{Y'})_{y'}| ⊆ ⋃ hᵢ(Wᵢ).

theorem exists_affine_etale_completeDevissage_cover (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFiniteType B S hS f) (F : Modules.{u, u} B S hS X hX)
    (hFq : F.IsQuasicoherentOnSite) (hFt : SheafOfModules.IsFiniteTypeOnSite F)
    (y : points B S hS Y) :
    ∃ (Y' : BigFppfOver B S hS) (q : yoneda.obj Y' ⟶ Y) (y' : points B S hS (yoneda.obj Y')),
      IsAffine ((BigFppfOver.toScheme B S hS).obj Y') ∧ IsEtale B S hS q ∧
      pointsMap B S hS (yoneda.obj Y') q y' = y ∧
      ∃ (n : ℕ) (W : Fin n → BigFppfOver B S hS)
        (h : ∀ i, yoneda.obj (W i) ⟶ pullback q f) (_ : ∀ i, IsEtale B S hS (h i))
        (hW : ∀ i, IsEtaleChart B S hS X (CostructuredArrow.mk (h i ≫ pullback.snd q f)))
        (a : ∀ i, W i ⟶ Y') (_ : ∀ i, h i ≫ pullback.fst q f = yoneda.map (a i))
        (hl : ∀ i, LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map (a i)))
        (hq : ∀ i, (restrictToChart B S hS hX F ⟨_, hW i⟩).IsQuasicoherent)
        (ht : ∀ i, (restrictToChart B S hS hX F ⟨_, hW i⟩).IsFiniteType),
        (∀ i, Nonempty (@CompleteDevissage _ _ ((BigFppfOver.toScheme B S hS).map (a i))
          (restrictToChart B S hS hX F ⟨_, hW i⟩) (pointsToScheme B S hS Y' y')
          (hl i) (hq i) (ht i))) ∧
        ∀ x : points B S hS (pullback q f),
          pointsMap B S hS _ (pullback.fst q f) x = y' →
            ∃ (i : Fin n) (z : points B S hS (yoneda.obj (W i))),
              pointsMap B S hS _ (h i) z = x

AlgebraicGeometry.Space.exists_affineChart_hasCompleteDevissageCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ExistenceCompleteDevissage.lean, line 183. The attribute's comment: “the elementary étale neighbourhood of the point, the covering family and its dévissages are delivered for the affine étale chart of the base change rather than for the base change as an algebraic space: the sources of the covering étale morphisms carry no size bound, so they are not objects of the big fppf site”.

Stacks Project, Tag 0CWJ, delivered at an affine étale chart of the base change.

Let X ⟶ Y be a finite type morphism of algebraic spaces over S, let F be a finite type quasi-coherent 𝒪_X-module, and let y be a point of Y. Then there are

an object Y₁ of the site whose scheme is affine, an étale morphism q : Y₁ ⟶ Y, and a point w of Y₁ above y — the source's (Y', y') ⟶ (Y, y) before the passage to an elementary étale neighbourhood;

an étale chart U of X whose scheme is affine, and a morphism ĝ : U ⟶ Y₁ of the site making the square over q commute, such that the induced morphism from U to the base change X ×_Y Y₁ is surjective on points — the source's affine surjective étale cover X' of X, after the reduction to an affine base;

the morphism of schemes underlying ĝ is locally of finite type and quasi-compact, and the conclusion of Stacks 05HU holds for it, for the restriction of F to U, and for the point of the scheme of Y₁ determined by w.

The finitely many étale morphisms hᵢ : Wᵢ ⟶ X_{Y'} of the source's conclusion, their complete dévissages and the inclusion of the fibre in the union of their images are bound inside AlgebraicGeometry.HasCompleteDevissageCover. See the implementation notes of this file for why they are delivered at the chart U rather than at X_{Y'}.

theorem exists_affineChart_hasCompleteDevissageCover (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFiniteType B S hS f) (F : Modules.{u, u} B S hS X hX)
    (hFq : F.IsQuasicoherentOnSite) (hFt : SheafOfModules.IsFiniteTypeOnSite F)
    (y : points B S hS Y) :
    ∃ (Y₁ : BigFppfOver B S hS) (q : yoneda.obj Y₁ ⟶ Y) (U : SmallEtale B S hS X)
      (ĝ : U.obj.left ⟶ Y₁) (hsq : yoneda.map ĝ ≫ q = U.obj.hom ≫ f)
      (w : points B S hS (yoneda.obj Y₁)),
      IsAffine ((BigFppfOver.toScheme B S hS).obj Y₁) ∧
      IsAffine (etaleChartScheme B S hS U) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q ∧
      pointsMap B S hS (yoneda.obj Y₁) q w = y ∧
      IsSurjective B S hS (Limits.pullback.lift (yoneda.map ĝ) U.obj.hom hsq) ∧
      LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map ĝ) ∧
      QuasiCompact ((BigFppfOver.toScheme B S hS).map ĝ) ∧
      HasCompleteDevissageCover ((BigFppfOver.toScheme B S hS).map ĝ)
        (restrictToChart B S hS hX F U) (pointsToScheme B S hS Y₁ w)

Tag 0CWK, a lemma

Tag 0CWK in the Stacks Project.

AlgebraicGeometry.Space.isOpen_flatLocus_setFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFiniteTypeModuleFibre.lean, line 453. The attribute's comment: “the statement in full, at the Stacks erratum: the point y of the target has a quasi-compact field-valued representative, condition (5) of Stacks 03JV, which holds at every point of a decent algebraic space. The tag as published asks nothing of y and is false that way, refuted by the theorem Stacks.Examples.NonOpenFlatLocusSpace.not_isOpen_flatLocus_setFibre_of_free_shift of StacksFrontier/Examples/Flatness/NonOpenFlatLocusSpace.lean”.

Stacks 0CWK. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let y be a point of |Y| with a quasi-compact field-valued representative. In the set-theoretic fibre f^{-1}({y}) ⊆ |X|, with its subspace topology, the points at which F is flat over Y form an open subset.

The hypothesis on y is condition (5) of Stacks 03JV; by Stacks 0AC8 it provides an étale scheme chart of Y with exactly one point above y, which is what makes the fibre of a chart of X map openly onto the set-theoretic fibre. It holds at every point of a decent algebraic space, which is AlgebraicGeometry.Space.isOpen_flatLocus_setFibre_of_isDecentSpace.

The hypothesis on y corrects Stacks 0CWK, which as published asks nothing of y; the corrected statement adds condition (5) of Stacks 03JV at y. The published form is false: Stacks.Examples.NonOpenFlatLocusSpace.not_isOpen_flatLocus_setFibre_of_free_shift takes no hypotheses and produces a big fppf site, an algebraic space Y = Spec A/ℤ for A = ℚ[t, u_i]/((t - i)u_i), the étale quotient morphism f : Spec A ⟶ Y, the cyclic module A ⧸ (u_i : i ≥ 1) on its source and a point y of |Y|, satisfying every hypothesis of this theorem except the one on y, and for which the conclusion below is false. Its companion Stacks.Examples.NonOpenFlatLocusSpace.not_hasQuasiCompactFieldRepresentative_ybase deduces from that failure that the point it produces has no quasi-compact field-valued representative, so the hypothesis on y is exactly what the source is missing.

Flatness at a point is AlgebraicGeometry.Space.flatLocus, the some-chart form of Stacks 05VV part (1), which Stacks 05VU shows is independent of the chart.

theorem isOpen_flatLocus_setFibre (f : X ⟶ Y)
    (Fm : Modules.{u, u} B S hS X.1 X.2) [Fm.IsQuasicoherentOnSite]
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (hft : IsFiniteTypeOnCharts B S hS X.2 Fm)
    (y : points B S hS Y.1) (hy : HasQuasiCompactFieldRepresentative B S hS Y.1 y) :
    IsOpen {x : (pointsMap B S hS X.1 f.hom ⁻¹' {y} : Set (points B S hS X.1)) |
      (x : points B S hS X.1) ∈ flatLocus B S hS X.2 f.hom Fm}

Tag 0CVK, a lemma

Tag 0CVK in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_tensor_modulePullback_iff_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/BourbakiFiniteTypePointwise.lean, line 144.

Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let x be a point of |X|, let 𝓕 be a finite type quasi-coherent 𝒪_X-module and let 𝓖 be a quasi-coherent 𝒪_Y-module. If 𝓕 is flat at x over Y, then x is weakly associated to 𝓕 ⊗_{𝒪_X} f^*𝓖 if and only if the image of x is weakly associated to 𝓖 and x lies in the relative weak assassin WeakAss_{X/Y}(𝓕) of Stacks 0CV0 — which, the fibres of f being locally Noetherian by Stacks 0CUY, is the set the source writes Ass_{X/Y}(𝓕).

This is the source's proof. A commuting square of étale scheme charts over f through x exists by AlgebraicGeometry.Space.exists_chartDiagram_chartSchemeToPoints_eq; on it the two sides of the formula become the Zariski conditions of the scheme case by AlgebraicGeometry.Space.isWeaklyAssociatedPoint_tensor_modulePullback_iff_of_chartDiagram, whose comparison of (𝓕 ⊗_{𝒪_X} f^*𝓖)|_U with 𝓕|_U ⊗_{𝒪_U} q^*(𝓖|_V) is AlgebraicGeometry.Space.nonempty_restrictToChart_tensor_modulePullback_chartDiagram and whose identification of the relative assassins is the two chart-diagram comparisons of StacksFrontier.AlgebraicGeometry.Divisors.MorphismWeaklyAssociated.ChartDiagramRelativeAssassin joined by Stacks 05F2, available because the chart morphism inherits local finite type from f. The chart restrictions are quasi-coherent and, on the source, of finite type, the chart morphism is locally of finite type, and the chart restriction of 𝓕 is flat over the target chart at the chart point by Stacks 05VU; so the scheme case, Stacks.Divisors.isWeaklyAssociatedPoint_tensorPullback_iff_of_finiteType, applies with no further hypothesis.

theorem isWeaklyAssociatedPoint_tensor_modulePullback_iff_of_finiteType (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (G : Modules.{u, u} B S hS Y.1 Y.2)
    [F.IsQuasicoherentOnSite] [F.IsFiniteType] [G.IsQuasicoherentOnSite]
    (x : points B S hS X.1)
    (hflat : IsFlatOverAtPoint B S hS X.2 f.hom F x) :
    IsWeaklyAssociatedPoint B S hS X (F ⊗ (modulePullback B S hS f).obj G) x ↔
      (IsWeaklyAssociatedPoint B S hS Y G (pointsMap B S hS X.1 f.hom x) ∧
        x ∈ relativeWeaklyAssociatedPoints B S hS f F)

Tag 0CVL, a lemma

Tag 0CVL in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_tensor_modulePullback_eq_inter_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTensorPullbackFiniteType.lean, line 209. The attribute's comment: “the full set equality, in the intersection-with-a-preimage form the tag writes, under the tag's own assumptions and with the source's own proof: the statement is an immediate consequence of its pointwise form, Stacks 0CVK, proved in its own generality as Space.isWeaklyAssociatedPoint_tensor_modulePullback_iff_of_finiteType and is applied here through Space.isBourbakiFormulaAtFlatPoints_of_finiteType, the two differing by and_comm. The sets are Space.relativeWeaklyAssociatedPoints of Stacks 0CV0, the Ass_{X/Y}(F) of the tag once the fibres of f are locally Noetherian as they are here by Stacks 0CUY, and Space.weaklyAssociatedPoints of Stacks 0CTX. The tag's flatness assumption hF is used, through Space.isFlatOverAtPoint_forall_of_isFlatOver, to discharge the pointwise flatness side condition of Stacks 0CVK at every point. Nothing beyond the tag's own assumptions is used: every binder of this theorem is one of them, namely f locally of finite type, F quasi-coherent of finite type, G quasi-coherent, and F flat over Y”.

Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S which is locally of finite type, let F be a finite type quasi-coherent 𝒪_X-module which is flat over Y, and let G be a quasi-coherent 𝒪_Y-module. Then the weakly associated points of F ⊗_{𝒪_X} f^*G are exactly the points of Ass_{X/Y}(F) lying over weakly associated points of G.

This is the source's own proof, which is that the statement is an immediate consequence of its pointwise form, Stacks 0CVK, available here as AlgebraicGeometry.Space.isBourbakiFormulaAtFlatPoints_of_finiteType. The tag's flatness hypothesis is what makes the pointwise flatness side condition hold at every point, by AlgebraicGeometry.Space.isFlatOverAtPoint_forall_of_isFlatOver.

theorem weaklyAssociatedPoints_tensor_modulePullback_eq_inter_preimage (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (G : Modules.{u, u} B S hS Y.1 Y.2)
    [F.IsQuasicoherentOnSite] [F.IsFiniteType] [G.IsQuasicoherentOnSite]
    (hF : IsFlatOver B S hS X.2 f.hom F) :
    weaklyAssociatedPoints B S hS X (F ⊗ (modulePullback B S hS f).obj G) =
      relativeWeaklyAssociatedPoints B S hS f F ∩
        pointsMap B S hS X.1 f.hom ⁻¹' weaklyAssociatedPoints B S hS Y G

Tag 0DLR, a theorem

Tag 0DLR in the Stacks Project.

AlgebraicGeometry.Space.isOpen_flatLocus_of_isSurjectiveChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartRestrictionFromSite.lean, line 145. The attribute's comment: “openness of the locus U, with all three conditions of the statement in the source's own shape: the module quasi-coherent of finite type on the small etale site, and the weakly associated points of the target locally finite on one surjective etale scheme chart”.

For a morphism f : X ⟶ Y of algebraic spaces locally of finite presentation and a module which is quasi-coherent and of finite type on the small étale site of X, the relative flat locus is open in the point space of X as soon as the weakly associated points of the scheme of one surjective étale chart of Y are locally finite there.

theorem isOpen_flatLocus_of_isSurjectiveChart (f : X.1 ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (hf : IsLocallyOfFinitePresentation B S hS f)
    (hqc : F.IsQuasicoherentOnSite) (hft : SheafOfModules.IsFiniteTypeOnSite F)
    (V₀ : SmallEtale B S hS Y) (hV₀ : IsSurjectiveChart B S hS V₀)
    (h₀ : ∀ v : etaleChartScheme B S hS V₀,
      ∃ W : (etaleChartScheme B S hS V₀).Opens, v ∈ W ∧
        (Stacks.Divisors.schemeWeaklyAssociatedPoints (etaleChartScheme B S hS V₀) ∩
          (W : Set (etaleChartScheme B S hS V₀))).Finite) :
    IsOpen (flatLocus B S hS X.2 f F)

AlgebraicGeometry.Space.isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartRestrictionFromSite.lean, line 164. The attribute's comment: “the locus U cuts out an open subspace of X in the sense of Tag 03BZ, with all three conditions of the statement in the source's own shape, condition (3) read on one surjective etale scheme chart”.

For a morphism f : X ⟶ Y of algebraic spaces locally of finite presentation and a module which is quasi-coherent and of finite type on the small étale site of X, the relative flat locus cuts out an open subspace of X as soon as the weakly associated points of the scheme of one surjective étale chart of Y are locally finite there.

theorem isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart (f : X.1 ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (hf : IsLocallyOfFinitePresentation B S hS f)
    (hqc : F.IsQuasicoherentOnSite) (hft : SheafOfModules.IsFiniteTypeOnSite F)
    (V₀ : SmallEtale B S hS Y) (hV₀ : IsSurjectiveChart B S hS V₀)
    (h₀ : ∀ v : etaleChartScheme B S hS V₀,
      ∃ W : (etaleChartScheme B S hS V₀).Opens, v ∈ W ∧
        (Stacks.Divisors.schemeWeaklyAssociatedPoints (etaleChartScheme B S hS V₀) ∩
          (W : Set (etaleChartScheme B S hS V₀))).Finite) :
    IsOpenSubspace B S hS (flatLocusOpenSubspace B S hS X.2 f F)

AlgebraicGeometry.Space.flatLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFiniteTypeModuleLocus.lean, line 209. The attribute's comment: “the locus U of the statement: the points of the source at which the module is flat over the target, which is Tag 05VV (1), i.e. clause (1) of Tag 05VU”.

The relative flat locus of a module on an algebraic space: the set of points x of the source such that some commuting square of étale scheme charts through x witnesses flatness of the restricted module over the target chart.

noncomputable def flatLocus (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X hX) : Set (points B S hS X)

AlgebraicGeometry.Space.isFinitePresentationOnCharts_flatLocusRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFiniteTypeModuleOnFlatLocus.lean, line 309. The attribute's comment: “F|_U is an O_U-module of finite presentation, for U the open subspace cut out by the flat locus, at all three conditions of the statement in the source's own shape -- the module quasi-coherent of finite type on the small etale site and the weakly associated points of the target locally finite on one surjective etale scheme chart, as the source's proof reads condition (3); the conclusion is read on the etale scheme charts of U, as every property of a module on an algebraic space is in this development”.

Stacks 0DLR: F|_U is an 𝒪_U-module of finite presentation. For a morphism of algebraic spaces locally of finite presentation, a module quasi-coherent of finite type on the small étale site and a target whose weakly associated points are locally finite on the scheme of one surjective étale chart, the module F|_U on the open subspace U = {x ∈ |X| : F flat at x over Y} is of finite presentation.

All three conditions are the source's own, the local finiteness of the weakly associated points of Y read on one surjective étale scheme chart as the source's proof reads it; the every-chart reading the proof consumes is derived from it by AlgebraicGeometry.Space.hasLocallyFiniteWeaklyAssociatedPointsOnCharts_of_isSurjectiveChart.

The conclusion is read on the étale scheme charts of U, as every property of a module on an algebraic space is in this development. The proof is the source's: the condition is étale local, so it is enough to read it on one chart of U surjective on points, and such a chart may be chosen to lie over a chart of Y (Tag 02X1), where the scheme-level theorem Stacks 05IK applies; the passage back to every chart is AlgebraicGeometry.Space.isFinitePresentation_restrictToChartScheme_of_isSurjective.

theorem isFinitePresentationOnCharts_flatLocusRestrict (f : Xs ⟶ Ys)
    (F : Modules.{u, u} B S hS Xs.1 Xs.2) [hqc : F.IsQuasicoherentOnSite]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hft : SheafOfModules.IsFiniteTypeOnSite F) (V₀ : SmallEtale B S hS Ys.1)
    (hV₀ : IsSurjectiveChart B S hS V₀)
    (h₀ : ∀ v : etaleChartScheme B S hS V₀,
      ∃ W : (etaleChartScheme B S hS V₀).Opens, v ∈ W ∧
        (Stacks.Divisors.schemeWeaklyAssociatedPoints (etaleChartScheme B S hS V₀) ∩
          (W : Set (etaleChartScheme B S hS V₀))).Finite) :
    IsFinitePresentationOnCharts B S hS
      (flatLocusSpace B S hS f F
        (isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart B S hS Xs f.hom F hf hqc hft
          V₀ hV₀ h₀)).2
      (flatLocusRestrict B S hS f F
        (isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart B S hS Xs f.hom F hf hqc hft
          V₀ hV₀ h₀))

AlgebraicGeometry.Space.isFlatOver_flatLocusRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFiniteTypeModuleOnFlatLocus.lean, line 375. The attribute's comment: “F|_U is flat over Y along the composite U -> X -> Y, for U the open subspace cut out by the flat locus, at all three conditions of the statement in the source's own shape, condition (3) read on one surjective etale scheme chart of the target; flatness of a module on an algebraic space over the target is Tag 05VV, read on the commuting squares of etale scheme charts”.

Stacks 0DLR: F|_U is flat over Y. For a morphism of algebraic spaces locally of finite presentation, a module quasi-coherent of finite type on the small étale site and a target whose weakly associated points are locally finite on the scheme of one surjective étale chart, the module F|_U on the open subspace U = {x ∈ |X| : F flat at x over Y} is flat over Y along the composite U ⟶ X ⟶ Y, in the sense of Tag 05VV.

All three conditions are the source's own, condition (3) read on one surjective étale scheme chart of the target as the source's proof reads it.

On a commuting square of étale scheme charts of U ⟶ Y, the chart of U is a chart of X whose points all lie in the relative flat locus, so the square witnesses flatness at each of them by Stacks 05VU.

theorem isFlatOver_flatLocusRestrict (f : Xs ⟶ Ys) (F : Modules.{u, u} B S hS Xs.1 Xs.2)
    [hqc : F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hft : SheafOfModules.IsFiniteTypeOnSite F) (V₀ : SmallEtale B S hS Ys.1)
    (hV₀ : IsSurjectiveChart B S hS V₀)
    (h₀ : ∀ v : etaleChartScheme B S hS V₀,
      ∃ W : (etaleChartScheme B S hS V₀).Opens, v ∈ W ∧
        (Stacks.Divisors.schemeWeaklyAssociatedPoints (etaleChartScheme B S hS V₀) ∩
          (W : Set (etaleChartScheme B S hS V₀))).Finite) :
    IsFlatOver B S hS
      (flatLocusSpace B S hS f F
        (isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart B S hS Xs f.hom F hf hqc hft
          V₀ hV₀ h₀)).2
      ((flatLocusSpaceι B S hS f F
        (isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart B S hS Xs f.hom F hf hqc hft
          V₀ hV₀ h₀)).hom ≫ f.hom)
      (flatLocusRestrict B S hS f F
        (isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart B S hS Xs f.hom F hf hqc hft
          V₀ hV₀ h₀))

Tag 0CVW, a lemma

Tag 0CVW in the Stacks Project.

AlgebraicGeometry.Space.exists_affineChart_hasFreeSectionsAlongFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ExistenceFreeSectionsAlongFibre.lean, line 205. The attribute's comment: “the etale neighbourhood, the affine scheme and its free sections are delivered; reduced to the affine etale chart of the target”.

Stacks Project, Tag 0CVW, reduced to the affine étale chart of the target at the prescribed point.

Let f : X ⟶ Y be a finite type morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module whose restriction to every étale chart of X is quasi-coherent of finite type, and let y be a point of |Y| at which F is flat over Y along the whole set-theoretic fibre f^{-1}({y}). Then there are

an object Y₁ of the site whose scheme is affine, an étale morphism q : Y₁ ⟶ Y and a point w of Y₁ above y — the source's (Y', y') ⟶ (Y, y) before the passage to an elementary étale neighbourhood;

an étale chart U of X whose scheme is affine, and a morphism ĝ : U ⟶ Y₁ of the site making the square over q commute, such that the induced morphism from U to the base change X ×_Y Y₁ is surjective on points — the source's affine surjective étale cover X' of X ×_Y Y';

the morphism of schemes underlying ĝ is locally of finite type and quasi-compact, and the conclusion of Stacks 05L1 holds for it, for the restriction of F to U, and for the point of the scheme of Y₁ determined by w — with the covering clause of that conclusion read on the point space of X, where it says that the set-theoretic fibre f^{-1}({y}) is the image of the fibre of the affine scheme Stacks 05L1 produces.

The hypothesis hFt is the source's "F of finite type", on the small étale site of X. The chartwise finite type it gives is AlgebraicGeometry.Space.isFiniteTypeOnCharts_of_isFiniteTypeOnSite, and chartwise quasi-coherence follows from SheafOfModules.IsQuasicoherentOnSite by AlgebraicGeometry.Space.isQuasicoherent_restrictToChart.

theorem exists_affineChart_hasFreeSectionsAlongFibre {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsFiniteType B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hFt : SheafOfModules.IsFiniteTypeOnSite F)
    (y : points B S hS Y.1)
    (hflat : ∀ x : points B S hS X.1, pointsMap B S hS X.1 f.hom x = y →
      x ∈ flatLocus B S hS X.2 f.hom F) :
    ∃ (Y₁ : BigFppfOver B S hS) (q : yoneda.obj Y₁ ⟶ Y.1) (U : SmallEtale B S hS X.1)
      (ĝ : U.obj.left ⟶ Y₁) (hsq : yoneda.map ĝ ≫ q = U.obj.hom ≫ f.hom)
      (w : points B S hS (yoneda.obj Y₁)),
      IsAffine ((BigFppfOver.toScheme B S hS).obj Y₁) ∧
      IsAffine (etaleChartScheme B S hS U) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q ∧
      pointsMap B S hS (yoneda.obj Y₁) q w = y ∧
      IsSurjective B S hS (pullback.lift (yoneda.map ĝ) U.obj.hom hsq) ∧
      LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map ĝ) ∧
      QuasiCompact ((BigFppfOver.toScheme B S hS).map ĝ) ∧
      HasFreeSectionsAlongFibreOver ((BigFppfOver.toScheme B S hS).map ĝ)
        (chartModule B S hS X.2 F U) (pointsToScheme B S hS Y₁ w)
        (pointOfEtaleChart B S hS U) (pointsMap B S hS X.1 f.hom ⁻¹' {y})

AlgebraicGeometry.Space.exists_affineChart_hasFreeSectionsAlongFibre_of_isFiniteTypeOnSite, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/ExistenceFreeSectionsAlongFibreOnSite.lean, line 48. The attribute's comment: “the etale neighbourhood, the affine scheme and its free sections are delivered, reduced to the affine etale chart of the target. At the source's own hypotheses: F of finite type on the small etale site of X, from which the finite type of each chart restriction follows by isFiniteTypeOnCharts_of_isFiniteTypeOnSite, which is proved”.

Stacks 0CVW, at the source's own hypotheses. Let f : X ⟶ Y be a finite type morphism of algebraic spaces over S, let F be a finite type quasi-coherent 𝒪_X-module and let y be a point of |Y| at which F is flat along the fibre. Then there is an affine étale neighbourhood of y in Y and an affine étale chart of X over it, surjective onto the fibre, over which F has free sections along the fibre.

This is AlgebraicGeometry.Space.exists_affineChart_hasFreeSectionsAlongFibre, which takes F of finite type on the small étale site of X and derives the finite type of each chart restriction by AlgebraicGeometry.Space.isFiniteTypeOnCharts_of_isFiniteTypeOnSite.

alias exists_affineChart_hasFreeSectionsAlongFibre_of_isFiniteTypeOnSite

AlgebraicGeometry.Space.exists_etale_affine_free_sections_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/FreeSectionsAlongFibreDiagram.lean, line 270.

Stacks Project, Tag 0CVW. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let y ∈ |Y|, with fibre F = f^{-1}({y}) ⊆ |X|. Assume

f is of finite type (hf),

𝓕 is of finite type (hFt), and

𝓕 is flat over Y at every point of F (hflat).

Then there are a scheme Y' with a point y' and an étale morphism e : Y' ⟶ Y sending y' to y, an affine scheme X' with morphisms g : X' ⟶ X and k : X' ⟶ Spec 𝒪_{Y', y'} making the square over f commute, such that the induced X' ⟶ X ×_Y Spec 𝒪_{Y', y'} is étale, F is the image under g of the fibre X'_{y'} of X' over the closed point of Spec 𝒪_{Y', y'} (so |X'_{y'}| ⟶ F is surjective), and Γ(X', g^*𝓕) is a free 𝒪_{Y', y'}-module, the module structure coming from k.

The schemes Y', Spec 𝒪_{Y', y'} (AlgebraicGeometry.BigFppfOver.specStalk) and X' are objects of the big fppf site of S, morphisms of algebraic spaces out of them are morphisms out of the presheaves they represent, and Γ(X', g^*𝓕) is the module of global sections of the restriction of g^*𝓕 to the scheme X', its identity chart.

theorem exists_etale_affine_free_sections_along_fibre {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsFiniteType B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hFt : SheafOfModules.IsFiniteTypeOnSite F)
    (y : points B S hS Y.1)
    (hflat : ∀ x : points B S hS X.1, pointsMap B S hS X.1 f.hom x = y →
      x ∈ flatLocus B S hS X.2 f.hom F) :
    ∃ (Y' : BigFppfOver B S hS) (y' : (BigFppfOver.toScheme B S hS).obj Y')
      (e : yoneda.obj Y' ⟶ Y.1) (X' : BigFppfOver B S hS) (g : yoneda.obj X' ⟶ X.1)
      (k : X' ⟶ BigFppfOver.specStalk B S hS Y' y')
      (hcomm : yoneda.map k ≫ yoneda.map (BigFppfOver.specStalkTo B S hS Y' y') ≫ e =
        g ≫ f.hom),
      IsEtale B S hS e ∧
      pointsMap B S hS (yoneda.obj Y') e ((pointsEquivScheme B S hS Y').symm y') = y ∧
      IsEtale B S hS (pullback.lift (yoneda.map k) g hcomm) ∧
      pointsMap B S hS X.1 f.hom ⁻¹' {y} =
        pointsMap B S hS (yoneda.obj X') g ''
          (pointsMap B S hS (yoneda.obj X') (yoneda.map k) ⁻¹'
            {BigFppfOver.specStalkClosedPoint B S hS Y' y'}) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj X') ∧
      (let M := restrictToChart B S hS (isAlgebraicSpace_yoneda B S hS X')
          ((modulePullback B S hS (X := ⟨yoneda.obj X', isAlgebraicSpace_yoneda B S hS X'⟩)
            (Y := X) (ObjectProperty.homMk g)).obj F)
          (idEtaleChart B S hS X')
       letI : Module (((BigFppfOver.toScheme B S hS).obj Y').presheaf.stalk y') Γ(M, ⊤) :=
         globalSectionsModuleOfSpecBase ((BigFppfOver.toScheme B S hS).map k) M
       Module.Free (((BigFppfOver.toScheme B S hS).obj Y').presheaf.stalk y') Γ(M, ⊤))

Tag 0CWL, a theorem

Tag 0CWL in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverAtPoint_of_forall_isRelativeWeaklyAssociatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/FlatnessAtRelativeAssassin.lean, line 161. The attribute's comment: “the implication (2) => (1), which the tag asserts holds with no decency hypothesis: for f locally of finite type and F a finite type quasi-coherent module, flatness of F over Y at every point of the fibre over y which lies in Ass_{X/Y}(F) and specializes to x gives flatness of F over Y at x. UNCONDITIONAL -- nothing is carried: the case of schemes is More on Flatness Theorem 05UA (2) => (1), proved in this library as AlgebraicGeometry.isFlatOverAt_of_forall_mem_relativeAssassin_specializes, and the reduction to a commuting square of etale scheme charts is proved here”.

Stacks 0CWL, the implication (2) ⟹ (1). Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let 𝓕 be a quasi-coherent 𝒪_X-module of finite type and let x be a point of |X| with image y under |f|. If 𝓕 is flat over Y at every point x' of |X| which lies over y, lies in the relative weak assassin WeakAss_{X/Y}(𝓕) of Stacks 0CV0 — which is Ass_{X/Y}(𝓕) here, the fibres of f being locally Noetherian — and specializes to x, then 𝓕 is flat over Y at x.

No decency is required, as the source records. Nothing is carried: the case of schemes is AlgebraicGeometry.isFlatOverAt_of_forall_mem_relativeAssassin_specializes, More on Flatness Theorem 05UA (2) ⟹ (1) in relative-assassin form, and the reduction to a commuting square of étale scheme charts of f is what is proved here.

theorem isFlatOverAtPoint_of_forall_isRelativeWeaklyAssociatedPoint (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (hFft : SheafOfModules.IsFiniteTypeOnSite F)
    (x : points B S hS X.1)
    (h2 : ∀ x' : points B S hS X.1,
      pointsMap B S hS X.1 f.hom x' = pointsMap B S hS X.1 f.hom x →
      IsRelativeWeaklyAssociatedPoint B S hS f F x' → x' ⤳ x →
        IsFlatOverAtPoint B S hS X.2 f.hom F x') :
    IsFlatOverAtPoint B S hS X.2 f.hom F x

AlgebraicGeometry.Space.isFlatOverAtPoint_of_specializes_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/FlatnessAtRelativeAssassin.lean, line 217. The attribute's comment: “the implication (1) => (2) for decent X, UNCONDITIONALLY -- nothing is carried: flatness of F over Y at x gives flatness of F over Y at every point of |X| which specializes to x. This is stronger than the tag's clause (2) in four ways: the point is not required to lie in Ass_{X/Y}(F), it is not required to lie in the set-theoretic fibre through x, decency of Y is not needed, and f locally of finite type and F of finite type are not needed and are not hypotheses; quasi-coherence of F and decency of X are”.

Stacks 0CWL, the implication (1) ⟹ (2), for decent X. Let f : X ⟶ Y be a morphism of algebraic spaces over S with X decent and let 𝓕 be a quasi-coherent 𝒪_X-module which is flat over Y at a point x of |X|. Then 𝓕 is flat over Y at every point x' of |X| which specializes to x.

This is clause (2) of the tag and more, in four ways: the relative-assassin condition on x' is not needed; x' is not required to lie in the set-theoretic fibre of f through x; decency of Y is not needed; and neither local finiteness of the type of f nor finiteness of the type of 𝓕 is a hypothesis. Decency of X lifts the specialization to an étale scheme chart (Stacks 03IL), and the case of schemes is then AlgebraicGeometry.isFlatOverAt_of_specializes_acrossFibres, which propagates relative flatness to an arbitrary generalization and so asks nothing about the images of the two lifted points in the target chart scheme.

theorem isFlatOverAtPoint_of_specializes_of_isDecentSpace (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hXdec : IsDecentSpace B S hS X.1)
    {x x' : points B S hS X.1} (hflat : IsFlatOverAtPoint B S hS X.2 f.hom F x)
    (hspec : x' ⤳ x) :
    IsFlatOverAtPoint B S hS X.2 f.hom F x'

Tag 0CWM, a lemma

Tag 0CWM in the Stacks Project.

AlgebraicGeometry.Space.isFlatOver_of_forall_specializes_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/FlatnessOverLocalBase.lean, line 349. The attribute's comment: “the lemma's implication: from its hypotheses (1) and (2) to flatness of ℱ over the local base. UNCONDITIONAL -- nothing is carried and no decency of X is assumed: the step the source's proof invokes, the implication (2) => (1) of Stacks 0CWL, is proved here for arbitrary X and Y as isFlatOverAtPoint_of_forall_isRelativeWeaklyAssociatedPoint, and the passage of flatness from a point of the closed fibre to a point of Ass_{X/S}(F) specializing to it is proved here as isFlatOverAtPoint_of_specializes_of_isRelativeWeaklyAssociatedPoint, using only that the local base is a decent space. The closedness of s is a hypothesis of the statement that the implication does not use”.

Stacks Project, Tag 0CWM. Let S be a local scheme with closed point s, read as the target Y of a morphism of algebraic spaces: the target is represented by a scheme of the site isomorphic to the spectrum of a local ring, and s is a closed point of |Y|. Let f : X ⟶ Y be locally of finite type and let F be a finite type quasi-coherent 𝒪_X-module. Assume

every point of Ass_{X/S}(F) specializes to a point of the closed fibre X_s (hass), and

F is flat over S at every point of X_s (hflat).

Then F is flat over S.

The conclusion is the tag's, with no clause dropped and nothing carried. The representability of the target in hlocal is consumed: a representable algebraic space is decent, which is what AlgebraicGeometry.Space.isFlatOver_of_forall_specializes_fibre asks of the target. The closedness of s is a hypothesis of the tag that the implication does not use.

theorem isFlatOver_of_forall_specializes_closedFibre {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (s : points B S hS Y.1)
    (hlocal : ∃ (T : BigFppfOver B S hS) (A : CommRingCat.{u}), IsLocalRing A ∧
      Nonempty (Spec A ≅ (BigFppfOver.toScheme B S hS).obj T) ∧ Nonempty (yoneda.obj T ≅ Y.1))
    (_hs : IsClosed ({s} : Set (points B S hS Y.1)))
    (hlft : IsLocallyOfFiniteType B S hS f.hom) (hqc : F.IsQuasicoherentOnSite)
    (hft : SheafOfModules.IsFiniteTypeOnSite F)
    (hass : ∀ x' ∈ relativeWeaklyAssociatedPoints B S hS f F,
      ∃ θ : points B S hS X.1, x' ⤳ θ ∧ pointsMap B S hS X.1 f.hom θ = s)
    (hflat : ∀ θ : points B S hS X.1, pointsMap B S hS X.1 f.hom θ = s →
      IsFlatOverAtPoint B S hS X.2 f.hom F θ) :
    IsFlatOver B S hS X.2 f.hom F

Sources

LeanAlgebraicGeometry.Space.exists_affine_etale_completeDevissage_cover · AlgebraicGeometry.Space.exists_affineChart_hasCompleteDevissageCover · AlgebraicGeometry.Space.isOpen_flatLocus_setFibre · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_tensor_modulePullback_iff_of_finiteType · AlgebraicGeometry.Space.weaklyAssociatedPoints_tensor_modulePullback_eq_inter_preimage · AlgebraicGeometry.Space.isOpen_flatLocus_of_isSurjectiveChart · AlgebraicGeometry.Space.isOpenSubspace_flatLocusOpenSubspace_of_isSurjectiveChart · AlgebraicGeometry.Space.flatLocus

Section77.5 Flat finitely presented modules #

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

Tag 0CVY, a proposition

Tag 0CVY in the Stacks Project.

AlgebraicGeometry.Space.exists_isAffine_etale_chart_square_at_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSections.lean, line 222. The attribute's comment: “the commutative diagram of pointed schemes of the conclusion — affine étale charts of the source and of the target, through the given point and through its image, with a morphism between them over f — and nothing of the projectivity of the sections, which is the case of schemes, Tag 05ID”.

Stacks Project, Tag 0CVY: the diagram of the conclusion. Every point x of the source of a morphism f : X ⟶ Y of algebraic spaces over S lies in the image of a commuting square of étale scheme charts
(X, x) ←—— (U, x')
  |          |
  ↓          ↓
(Y, f x) ←— (V, y')
whose two charts U and V are affine, through a point x' of U lying over x; the point y' of V it induces then lies over the image of x.

This is the diagram of pointed schemes which Tag 0CVY asserts, and it is produced here with none of the tag's three hypotheses: neither f nor any module on X enters. What Tag 0CVY adds to it is the projectivity of Γ(U, 𝓕|_U) over Γ(V, 𝒪_V) after a further shrinking, which is the case of schemes, Tag 05ID; that is AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections.

The three conclusions after affineness are, in order: the square of charts commutes over f; the chart point lies over x; and the image of the chart point in the target chart lies over the image of x in |Y|.

theorem exists_isAffine_etale_chart_square_at_point
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (x : points B S hS X) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V)
      (x' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U))),
      IsAffine (chartScheme U) ∧ IsAffine (chartScheme V) ∧
        U.obj.hom ≫ f = yoneda.map g ≫ V.obj.hom ∧
        pointsMap B S hS _ U.obj.hom x' = x ∧
        pointsMap B S hS _ V.obj.hom (pointsMap B S hS _ (yoneda.map g) x') =
          pointsMap B S hS X f x

AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSections.lean, line 367. The attribute's comment: “the full conclusion — the pointed affine étale diagram and the projectivity of the sections — with the case of schemes, Tag 05ID, supplied by exists_isAffine_etale_hom_projective_sections, and with the tag's conditions (2) and (3) on the module in their étale-chartwise form”.

Stacks Project, Tag 0CVY. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be an 𝒪_X-module and let x be a point of |X|. Assume

f is locally of finite presentation (hfp, Stacks 03XP part (1));

F is quasi-coherent and of finite presentation (hqc, hFfp), chartwise: its restriction to every étale scheme chart of X is;

F is flat at x over Y (hflat), chartwise: on every commuting square of étale charts and at every point of the source chart over x, the restriction of F to the source chart is flat over the target chart there.

Then there are an étale chart U of X, an étale chart V of Y, affine objects X', Y' of the site with étale morphisms p : X' ⟶ U and q : Y' ⟶ V, a morphism k : X' ⟶ Y' and a point x'' of |X'| such that the composites X' → X and Y' → Y are étale, the square commutes over f, x'' lies over x, its image in |Y'| lies over the image of x, and the sections Γ(X', p^*(F|_U)) form a projective Γ(Y', 𝒪_{Y'})-module.

The conclusion is the conclusion of Tag 0CVY, with no clause dropped, and nothing is assumed beyond the tag's own hypotheses. The source's proof of Tag 0CVY is the remark that the statement reduces to the case of schemes, Tag 05ID; that case, read inside the big fppf site, is AlgebraicGeometry.Space.exists_isAffine_etale_hom_projective_sections. See the module docstring on this, and on why the module of the conclusion is named as a pullback of a chart restriction.

The hypotheses (2) and (3) are stated chartwise, which is how this development states these conditions for a module on an algebraic space: compare AlgebraicGeometry.Space.IsFlatOver, the definition of Stacks 05VV, which is the chartwise condition on every commuting square of étale charts. They are not weakenings: the chartwise form is one of the equivalent conditions of Stacks 05VU, which the source's definition Stacks 05VV names.

Everything in the conclusion except the projectivity comes from AlgebraicGeometry.Space.exists_isAffine_etale_chart_square_at_point, which is unconditional; the hypotheses are used only to feed the case of schemes.

theorem exists_isAffine_etale_charts_projective_sections
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (F : Modules.{u, u} B S hS X hX) (x : points B S hS X)
    (hfp : IsLocallyOfFinitePresentation B S hS f)
    (hqc : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX F U).IsQuasicoherent)
    (hFfp : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX F U).IsFinitePresentation)
    (hflat : ∀ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V)
      (x' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U))),
      U.obj.hom ≫ f = yoneda.map g ≫ V.obj.hom →
      pointsMap B S hS _ U.obj.hom x' = x →
      AlgebraicGeometry.IsFlatOverAt
        (LocallyRingedSpace.forgetToSheafedSpace.map
          ((BigFppfOver.toScheme B S hS).map g).toLRSHom)
        (restrictToChart B S hS hX F U) (pointsToScheme B S hS _ x')) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (U' E' : BigFppfOver B S hS)
      (p : U' ⟶ (SmallEtale.toOver B S hS X).obj U)
      (q : E' ⟶ (SmallEtale.toOver B S hS Y).obj V) (k : U' ⟶ E')
      (x'' : points B S hS (yoneda.obj U')),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map p ≫ U.obj.hom) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map q ≫ V.obj.hom) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj U') ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj E') ∧
      (yoneda.map p ≫ U.obj.hom) ≫ f = yoneda.map k ≫ yoneda.map q ≫ V.obj.hom ∧
      pointsMap B S hS _ (yoneda.map p ≫ U.obj.hom) x'' = x ∧
      pointsMap B S hS _ (yoneda.map q ≫ V.obj.hom)
          (pointsMap B S hS _ (yoneda.map k) x'') = pointsMap B S hS X f x ∧
      (let M := (Scheme.Modules.pullback ((BigFppfOver.toScheme B S hS).map p)).obj
           (restrictToChart B S hS hX F U)
       letI : Module Γ((BigFppfOver.toScheme B S hS).obj E', ⊤) Γ(M, ⊤) :=
         Module.compHom Γ(M, ⊤) ((BigFppfOver.toScheme B S hS).map k).appTop.hom
       Module.Projective Γ((BigFppfOver.toScheme B S hS).obj E', ⊤) Γ(M, ⊤))

AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_of_isFlatOverAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSections.lean, line 435.

Stacks Project, Tag 0CVY. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation, let 𝓕 be an 𝒪_X-module which is quasi-coherent and of finite presentation on every étale chart, and let x be a point of X at which 𝓕 is flat over Y. Then x lies in the image of a commuting square of étale charts, refined by affine objects U' of X and E' of Y of the site, through a point of U', such that Γ(U', 𝓕|_{U'}) is a projective Γ(E', 𝒪_{E'})-module.

This is AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections, whose proof feeds the case of schemes, Tag 05ID, through AlgebraicGeometry.Space.exists_isAffine_etale_hom_projective_sections.

theorem exists_isAffine_etale_charts_projective_sections_of_isFlatOverAt
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (F : Modules.{u, u} B S hS X hX) (x : points B S hS X)
    (hfp : IsLocallyOfFinitePresentation B S hS f)
    (hqc : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX F U).IsQuasicoherent)
    (hFfp : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX F U).IsFinitePresentation)
    (hflat : ∀ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V)
      (x' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U))),
      U.obj.hom ≫ f = yoneda.map g ≫ V.obj.hom →
      pointsMap B S hS _ U.obj.hom x' = x →
      AlgebraicGeometry.IsFlatOverAt
        (LocallyRingedSpace.forgetToSheafedSpace.map
          ((BigFppfOver.toScheme B S hS).map g).toLRSHom)
        (restrictToChart B S hS hX F U) (pointsToScheme B S hS _ x')) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (U' E' : BigFppfOver B S hS)
      (p : U' ⟶ (SmallEtale.toOver B S hS X).obj U)
      (q : E' ⟶ (SmallEtale.toOver B S hS Y).obj V) (k : U' ⟶ E')
      (x'' : points B S hS (yoneda.obj U')),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map p ≫ U.obj.hom) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map q ≫ V.obj.hom) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj U') ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj E') ∧
      (yoneda.map p ≫ U.obj.hom) ≫ f = yoneda.map k ≫ yoneda.map q ≫ V.obj.hom ∧
      pointsMap B S hS _ (yoneda.map p ≫ U.obj.hom) x'' = x ∧
      pointsMap B S hS _ (yoneda.map q ≫ V.obj.hom)
          (pointsMap B S hS _ (yoneda.map k) x'') = pointsMap B S hS X f x ∧
      (let M := (Scheme.Modules.pullback ((BigFppfOver.toScheme B S hS).map p)).obj
           (restrictToChart B S hS hX F U)
       letI : Module Γ((BigFppfOver.toScheme B S hS).obj E', ⊤) Γ(M, ⊤) :=
         Module.compHom Γ(M, ⊤) ((BigFppfOver.toScheme B S hS).map k).appTop.hom
       Module.Projective Γ((BigFppfOver.toScheme B S hS).obj E', ⊤) Γ(M, ⊤))

Tag 0CVZ, a lemma

Tag 0CVZ in the Stacks Project.

AlgebraicGeometry.Space.exists_isAffine_etale_chart_square_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSectionsAlongFibre.lean, line 267. The attribute's comment: “the affine étale diagram covering the fibre — affine étale charts of the source and of the target with a morphism between them over f, through a point of the target chart over y and with the source chart covering the fibre — and nothing of the projectivity of the sections, which is the case of schemes, Tag 05KW”.

Stacks Project, Tag 0CVZ: the diagram of the conclusion. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S and let y be a point of |Y|. Then there is a commuting square of étale scheme charts
X ←—— U
|     |
↓     ↓
Y ←—— V
whose two charts U and V are affine, together with a point y' of |V| lying over y, such that the fibre F = f^{-1}({y}) is contained in the image of |U| → |X|. Moreover every point of F is the image of a point of |U| lying over y'.

This is the diagram of Tag 0CVZ, produced with none of the tag's hypotheses on the module and with only quasi-compactness of f, which is part of the tag's hypothesis (1) and is what makes F quasi-compact. What Tag 0CVZ adds to it is the projectivity of Γ(U, 𝓕|_U) over Γ(V, 𝒪_V) after a further shrinking, which is the case of schemes, Tag 05KW; that is AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre.

The clauses after affineness are, in order: the square of charts commutes over f; the chart point lies over y; the fibre is contained in the image of the source chart; and the sharpened form of that containment, by points of the source chart lying over y'.

theorem exists_isAffine_etale_chart_square_along_fibre
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f) (y : points B S hS Y) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (k : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V)
      (y' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS Y).obj V))),
      IsAffine (chartScheme U) ∧ IsAffine (chartScheme V) ∧
        U.obj.hom ≫ f = yoneda.map k ≫ V.obj.hom ∧
        pointsMap B S hS _ V.obj.hom y' = y ∧
        {x : points B S hS X | pointsMap B S hS X f x = y} ⊆
          Set.range (pointsMap B S hS _ U.obj.hom) ∧
        ∀ x : points B S hS X, pointsMap B S hS X f x = y →
          ∃ x' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U)),
            pointsMap B S hS _ U.obj.hom x' = x ∧
            pointsMap B S hS _ (yoneda.map k) x' = y'

AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSectionsAlongFibre.lean, line 456. The attribute's comment: “the full conclusion — the affine étale diagram covering the fibre and the projectivity of the sections — with quasi-coherence and the tag's conditions (2) and (3) on the module in their étale-chartwise form, for a consumer holding chart data; the case of schemes, Tag 05KW, is discharged inside the big fppf site”.

Stacks Project, Tag 0CVZ. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be an 𝒪_X-module and let y be a point of |Y|. Assume

f is of finite presentation (hfp, Stacks 03XP part (3));

𝓕 is quasi-coherent and of finite presentation (hqc, h𝓕fp), chartwise: its restriction to every étale scheme chart of X is;

𝓕 is flat over Y at every point of the fibre F = f^{-1}({y}) (hflat), chartwise: on every commuting square of étale charts and at every point of the source chart lying over a point of F, the restriction of 𝓕 to the source chart is flat over the target chart there.

Then there are an étale chart Z of X, an étale chart V of Y, affine objects X', Y' of the site with étale morphisms p : X' ⟶ Z and q : Y' ⟶ V, a morphism k : X' ⟶ Y' and a point y' of |Y'| such that the composites X' → X and Y' → Y are étale, the square commutes over f, y' lies over y, the fibre F is contained in the image of |X'| → |X|, and the sections Γ(X', p^*(𝓕|_Z)) form a projective Γ(Y', 𝒪_{Y'})-module.

The conclusion is the conclusion of Tag 0CVZ, with no clause dropped, and nothing is granted as a hypothesis: everything except the projectivity is AlgebraicGeometry.Space.exists_isAffine_etale_chart_square_along_fibre, and the projectivity is the case of schemes, Tag 05KW, read inside the site by AlgebraicGeometry.Space.exists_isAffine_etale_hom_projective_sections_along_fibre.

Quasi-coherence and the hypotheses (2) and (3) are stated chartwise here; compare AlgebraicGeometry.Space.IsFlatOver, the definition of Stacks 05VV. This is not the source's reading of them, and it is not comparable to it: chartwise quasi-coherence and chartwise finite presentation are weaker than the source's conditions on X itself, while the chartwise flatness asked here is the every-chart-square form, which is strictly more than Stacks 05VV asks at a point. The statement at the source's own three hypotheses, with no chartwise condition on the module anywhere, is exists_isAffine_etale_charts_projective_sections_along_fibre_of_isFlatOverAtPoint, which is proved from this one. See the module docstring for the three transfers between the readings.

theorem exists_isAffine_etale_charts_projective_sections_along_fibre
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (𝓕 : Modules.{u, u} B S hS X hX) (y : points B S hS Y)
    (hfp : IsFinitePresentation B S hS f)
    (hqc : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX 𝓕 U).IsQuasicoherent)
    (h𝓕fp : ∀ U : SmallEtale B S hS X, (restrictToChart B S hS hX 𝓕 U).IsFinitePresentation)
    (hflat : ∀ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V)
      (x' : points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U))),
      U.obj.hom ≫ f = yoneda.map g ≫ V.obj.hom →
      pointsMap B S hS X f (pointsMap B S hS _ U.obj.hom x') = y →
      AlgebraicGeometry.IsFlatOverAt
        (LocallyRingedSpace.forgetToSheafedSpace.map
          ((BigFppfOver.toScheme B S hS).map g).toLRSHom)
        (restrictToChart B S hS hX 𝓕 U) (pointsToScheme B S hS _ x')) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (X' Y' : BigFppfOver B S hS)
      (p : X' ⟶ (SmallEtale.toOver B S hS X).obj U)
      (q : Y' ⟶ (SmallEtale.toOver B S hS Y).obj V) (k : X' ⟶ Y')
      (y' : points B S hS (yoneda.obj Y')),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map p ≫ U.obj.hom) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map q ≫ V.obj.hom) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj X') ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Y') ∧
      (yoneda.map p ≫ U.obj.hom) ≫ f = yoneda.map k ≫ yoneda.map q ≫ V.obj.hom ∧
      pointsMap B S hS _ (yoneda.map q ≫ V.obj.hom) y' = y ∧
      {x : points B S hS X | pointsMap B S hS X f x = y} ⊆
        Set.range (pointsMap B S hS _ (yoneda.map p ≫ U.obj.hom)) ∧
      (let M := (Scheme.Modules.pullback ((BigFppfOver.toScheme B S hS).map p)).obj
           (restrictToChart B S hS hX 𝓕 U)
       letI : Module Γ((BigFppfOver.toScheme B S hS).obj Y', ⊤) Γ(M, ⊤) :=
         Module.compHom Γ(M, ⊤) ((BigFppfOver.toScheme B S hS).map k).appTop.hom
       Module.Projective Γ((BigFppfOver.toScheme B S hS).obj Y', ⊤) Γ(M, ⊤))

AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre_of_isFlatOverAtPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFinitePresentationProjectiveSectionsAlongFibre.lean, line 619. The attribute's comment: “the full conclusion — the affine étale diagram covering the fibre and the projectivity of the sections — at the tag's own three conditions throughout: the module quasi-coherent and of finite presentation on the small étale site, and condition (3) in the some-chart form which Stacks 05VV gives it; no chartwise condition on the module appears, and the case of schemes, Tag 05KW, is discharged inside the big fppf site”.

Stacks Project, Tag 0CVZ. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let y be a point of |Y| with fibre F = f^{-1}({y}) ⊆ |X|. Assume

f is of finite presentation (hfp, Stacks 03XP part (3));

𝓕 is of finite presentation (h𝓕fp), on the small étale site of X, which is the property Stacks 05VR item (l) names;

𝓕 is flat over Y at every point of F (hflat), in the some-chart sense of Stacks 05VV, which is condition (1) of Stacks 05VU.

Then there are an étale chart Z of X, an étale chart V of Y, affine objects X', Y' of the site with étale morphisms p : X' ⟶ Z and q : Y' ⟶ V, a morphism k : X' ⟶ Y' and a point y' of |Y'| such that the composites X' → X and Y' → Y are étale, the square commutes over f, y' lies over y, the fibre F is contained in the image of |X'| → |X|, and the sections Γ(X', p^*(𝓕|_Z)) form a projective Γ(Y', 𝒪_{Y'})-module.

Every hypothesis here is the source's own, and no chartwise condition on the module appears. This is AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre with its three chartwise hypotheses on the module discharged: quasi-coherence on the small étale site gives chartwise quasi-coherence by AlgebraicGeometry.Space.isQuasicoherent_restrictToChart, finite presentation on the small étale site gives chartwise finite presentation by AlgebraicGeometry.Space.isFinitePresentationOnCharts_of_isFinitePresentationOnSite, and the some-chart form of condition (3) gives the every-chart form by Stacks 05VU, AlgebraicGeometry.Space.isFlatOverAtOnChartDiagram_of_isFlatOverAtPoint.

theorem exists_isAffine_etale_charts_projective_sections_along_fibre_of_isFlatOverAtPoint
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (𝓕 : Modules.{u, u} B S hS X hX) (y : points B S hS Y)
    (hfp : IsFinitePresentation B S hS f)
    (hqc : 𝓕.IsQuasicoherentOnSite)
    (h𝓕fp : SheafOfModules.IsFinitePresentationOnSite 𝓕)
    (hflat : ∀ x : points B S hS X, pointsMap B S hS X f x = y →
      IsFlatOverAtPoint B S hS hX f 𝓕 x) :
    ∃ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
      (X' Y' : BigFppfOver B S hS)
      (p : X' ⟶ (SmallEtale.toOver B S hS X).obj U)
      (q : Y' ⟶ (SmallEtale.toOver B S hS Y).obj V) (k : X' ⟶ Y')
      (y' : points B S hS (yoneda.obj Y')),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map p ≫ U.obj.hom) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map q ≫ V.obj.hom) ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj X') ∧
      IsAffine ((BigFppfOver.toScheme B S hS).obj Y') ∧
      (yoneda.map p ≫ U.obj.hom) ≫ f = yoneda.map k ≫ yoneda.map q ≫ V.obj.hom ∧
      pointsMap B S hS _ (yoneda.map q ≫ V.obj.hom) y' = y ∧
      {x : points B S hS X | pointsMap B S hS X f x = y} ⊆
        Set.range (pointsMap B S hS _ (yoneda.map p ≫ U.obj.hom)) ∧
      (let M := (Scheme.Modules.pullback ((BigFppfOver.toScheme B S hS).map p)).obj
           (restrictToChart B S hS hX 𝓕 U)
       letI : Module Γ((BigFppfOver.toScheme B S hS).obj Y', ⊤) Γ(M, ⊤) :=
         Module.compHom Γ(M, ⊤) ((BigFppfOver.toScheme B S hS).map k).appTop.hom
       Module.Projective Γ((BigFppfOver.toScheme B S hS).obj Y', ⊤) Γ(M, ⊤))

Sources

LeanAlgebraicGeometry.Space.exists_isAffine_etale_chart_square_at_point · AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections · AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_of_isFlatOverAt · AlgebraicGeometry.Space.exists_isAffine_etale_chart_square_along_fibre · AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre · AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_along_fibre_of_isFlatOverAtPoint

Section77.6 A criterion for purity #

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

Tag 0CW1, a lemma

Tag 0CW1 in the Stacks Project.

AlgebraicGeometry.Space.exists_specializes_isRelativeWeaklyAssociatedPoint_fibre_schemeBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PuritySchemeBase.lean, line 182. The attribute's comment: “the source's own statement, unconditionally: the base is a scheme of the site (the source's S), flatness is read on the module, Stacks 05VV at a point, exactly as the source reads it, and nothing further is required of the data -- in particular no affineness, the affine etale chart being chosen inside the proof as the source chooses it”.

Stacks 0CW1. Let X be a decent algebraic space over a scheme S of a big fppf site, let f : X ⟶ h_V be a morphism locally of finite type into the algebraic space of a scheme V of the site, let F be a finite type quasi-coherent 𝒪_X-module, and let s be a point of |h_V| such that F is flat over h_V at every point of the fibre X_s. If a point x' of the relative weak assassin WeakAss_{X/V}(F) specializes to a point of X_s — that is, if the closure of {x'} in |X| meets |X_s| — then it specializes to a point of WeakAss_{X/V}(F) lying over s, so that closure meets WeakAss_{X/V}(F) ∩ |X_s|.

The source's Ass_{X/S}(ℱ) is the relative weak assassin of Stacks 0CV0, which it writes that way because a morphism locally of finite type has locally Noetherian fibres (Stacks 0CUY); its flatness hypothesis "ℱ is flat over S at all points of X_s" is flatness of the module over the target at the points of the fibre, which is AlgebraicGeometry.Space.IsFlatOverAtPoint, Stacks 05VV at a point.

The two companions in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PuritySpecialization.lean generalize the base to an arbitrary algebraic space and carry the chart criterion as a hypothesis; neither of them is registered against this tag, which is registered here.

theorem exists_specializes_isRelativeWeaklyAssociatedPoint_fibre_schemeBase
    (V : BigFppfOver B S hS) {X : AlgebraicSpaces B S hS} (f : X ⟶ schemeSpace V)
    (hXdec : IsDecentSpace B S hS X.1) (hf : IsLocallyOfFiniteType B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteTypeOnSite F] (s : points B S hS (schemeSpace V).1)
    (hflat : ∀ t : points B S hS X.1, pointsMap B S hS X.1 f.hom t = s →
      IsFlatOverAtPoint B S hS X.2 f.hom F t)
    {x' : points B S hS X.1} (hx' : IsRelativeWeaklyAssociatedPoint B S hS f F x')
    (hmeets : ∃ t : points B S hS X.1, x' ⤳ t ∧ pointsMap B S hS X.1 f.hom t = s) :
    ∃ x : points B S hS X.1, x' ⤳ x ∧ pointsMap B S hS X.1 f.hom x = s ∧
      IsRelativeWeaklyAssociatedPoint B S hS f F x

Tag 0CW2, a lemma

Tag 0CW2 in the Stacks Project.

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_baseChange_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceBaseChange.lean, line 289. The attribute's comment: “for the relative weak assassin of Stacks 0CV0, stated for an arbitrary module in place of a quasi-coherent one and with no finiteness hypothesis on f, neither of which is used by part (1) of Stacks 0CV2 or by Stacks 03H4. The base changes are presented by cartesian squares, X'_Z as X_Z ×_X X' exactly as the source's proof does, so g is not required to be given as a morphism over Y”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S, let g : X'' ⟶ X be a morphism of algebraic spaces, and let F be an 𝒪_X-module. If WeakAss_{X/Y}(F) is contained in the image of |X''| → |X|, then for every Z ⟶ Y the set WeakAss_{X_Z/Z}(F_Z) is contained in the image of |X''_Z| → |X_Z|, where X_Z = X ×_Y Z and X''_Z = X_Z ×_X X''.

theorem relativeWeaklyAssociatedPoints_baseChange_subset_range
    {X Y Z X'' XZ X'Z : AlgebraicSpaces B S hS} {f : X ⟶ Y} {g : X'' ⟶ X} {h : Z ⟶ Y}
    {pZ : XZ ⟶ X} {qZ : XZ ⟶ Z} {gZ : X'Z ⟶ XZ} {rZ : X'Z ⟶ X''}
    (sq : IsPullback pZ.hom qZ.hom f.hom h.hom)
    (sq' : IsPullback gZ.hom rZ.hom pZ.hom g.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : relativeWeaklyAssociatedPoints B S hS f F ⊆
      Set.range (pointsMap B S hS X''.1 g.hom)) :
    relativeWeaklyAssociatedPoints B S hS qZ ((modulePullback B S hS pZ).obj F) ⊆
      Set.range (pointsMap B S hS X'Z.1 gZ.hom)

Tag 0CW3, a lemma

Tag 0CW3 in the Stacks Project.

AlgebraicGeometry.Space.EtaleOverSource.isPureAbove_of_isPureAbove_situation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphism.lean, line 464. The attribute's comment: “clause (1) for purity above y: the source's own two assumptions on the etale morphism g, that Ass_{X/Y}(F) lies in the image of |X'| and that g^*F is pure above y, give purity of F above y. Nothing beyond the source's own assumptions is used”.

Stacks 0CW3, clause (1), for purity above y. In the situation of Stacks 0CV6, let g : X' ⟶ X be étale over Y with X' ⟶ Y decent and of finite type. If the relative assassin Ass_{X/Y}(ℱ) lies in the image of |X'| → |X| and g^*ℱ is pure above y, then ℱ is pure above y.

An impurity of ℱ above y whose structure morphism is quasi-finite at t lifts to such an impurity of g^*ℱ above y: the containment passes to the base change by Stacks 0CW2, which lifts the distinguished point, and Stacks 0CUZ makes the lift relatively associated.

The containment of the assassin and purity of g^*ℱ are the two assumptions the source's own clause (1) makes, and nothing further is assumed. In particular the containment is not obtained from clause (2) of the same tag: clause (2) produces it from purity of ℱ above y — which is the conclusion here — over an affine local base whose fibre is met by the image, so none of its three inputs is available at clause (1).

theorem isPureAbove_of_isPureAbove_situation
    (hass : relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom))
    (h : IsPureAbove c.situation) : IsPureAbove P

AlgebraicGeometry.Space.EtaleOverSource.isUniversallyPureAbove_of_isUniversallyPureAbove_situation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphism.lean, line 486. The attribute's comment: “clause (1) for universal purity above y: the source's own two assumptions on the etale morphism g, that Ass_{X/Y}(F) lies in the image of |X'| and that g^*F is universally pure above y, give universal purity of F above y. Nothing beyond the source's own assumptions is used”.

Stacks 0CW3, clause (1), for universal purity above y. In the situation of Stacks 0CV6, let g : X' ⟶ X be étale over Y with X' ⟶ Y decent and of finite type. If the relative assassin Ass_{X/Y}(ℱ) lies in the image of |X'| → |X| and g^*ℱ is universally pure above y, then ℱ is universally pure above y.

Any impurity of ℱ above y lifts to an impurity of g^*ℱ above y.

The containment of the assassin and universal purity of g^*ℱ are the two assumptions the source's own clause (1) makes, and nothing further is assumed.

theorem isUniversallyPureAbove_of_isUniversallyPureAbove_situation
    (hass : relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom))
    (h : IsUniversallyPureAbove c.situation) : IsUniversallyPureAbove P

AlgebraicGeometry.Space.EtaleOverSource.relativeWeaklyAssociatedPoints_subset_range_of_isAffineLocalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphism.lean, line 789. The attribute's comment: “clause (2): purity of F above y, the image of |X'| meeting the whole fibre and an affine local base with closed point y give the containment of Ass_{X/Y}(F) in that image. Those are the source's own three assumptions, and nothing beyond them is used”.

Stacks 0CW3, clause (2), with nothing granted. In the situation of Stacks 0CV6, let g : X' ⟶ X be étale over Y with X' ⟶ Y decent and of finite type. If ℱ is pure above y, the image of |X'| → |X| contains the fibre F = f^{-1}(\{y\}), and Y is affine local with closed point y, then that image contains the whole relative assassin Ass_{X/Y}(ℱ).

This is AlgebraicGeometry.Space.EtaleOverSource.relativeWeaklyAssociatedPoints_subset_range with its specialization step discharged by AlgebraicGeometry.Space.purityFibreSpecialization, so that only the source's own hypotheses remain.

theorem relativeWeaklyAssociatedPoints_subset_range_of_isAffineLocalAt
    (hlocal : P.IsAffineLocalAt) (hpure : IsPureAbove P)
    (hfibre : pointsMap B S hS P.X P.f ⁻¹' {P.y} ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom)) :
    relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom)

AlgebraicGeometry.Space.EtaleOverSource.relativeWeaklyAssociatedPoints_subset_range_of_isFlatOver_fibre_of_isAffineLocalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphism.lean, line 952. The attribute's comment: “clause (3): purity of F above y, flatness of the module F over Y at the points of the fibre, the image of |X'| meeting Ass_{X/Y}(F) cap F and an affine local base with closed point y give the containment of Ass_{X/Y}(F) in that image. Those are the source's own four assumptions, and nothing beyond them is used”.

Stacks 0CW3, clause (3), with nothing granted. In the situation of Stacks 0CV6, let g : X' ⟶ X be étale over Y with X' ⟶ Y decent and of finite type. If ℱ is pure above y, ℱ is flat over Y at every point of the fibre F = f^{-1}(\{y\}), the image of |X'| → |X| contains Ass_{X/Y}(ℱ) ∩ F, and Y is affine local with closed point y, then that image contains the whole relative assassin Ass_{X/Y}(ℱ).

The flatness hypothesis is the source's own: flatness of the module ℱ over Y at the points of the fibre, AlgebraicGeometry.Space.IsFlatOverAtPoint, Stacks 05VV at a point in the some-chart form which is condition (1) of Stacks 05VU — and not flatness of the morphism f, which is the incomparable condition of relativeWeaklyAssociatedPoints_subset_range_of_isFlatAt_fibre_of_isAffineLocalAt in this namespace.

This is relativeWeaklyAssociatedPoints_subset_range_of_isFlatOver_fibre in this namespace with its specialization step discharged by AlgebraicGeometry.Space.purityFibreSpecialization, so that nothing beyond the source's own hypotheses is assumed.

theorem relativeWeaklyAssociatedPoints_subset_range_of_isFlatOver_fibre_of_isAffineLocalAt
    (hlocal : P.IsAffineLocalAt) (hpure : IsPureAbove P)
    (hflat : ∀ t : points B S hS P.X, pointsMap B S hS P.X P.f t = P.y →
      IsFlatOverAtPoint B S hS P.hX P.f P.F t)
    (hfibre : relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ∩
        pointsMap B S hS P.X P.f ⁻¹' {P.y} ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom)) :
    relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS c.X'.1 c.g.hom)

AlgebraicGeometry.Space.isPureAbove_of_isEtale_of_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphismClauses.lean, line 210. The attribute's comment: “clause (1), both the pure and the universally pure reading, under exactly the source's hypotheses”.

Stacks 0CW3, clause (1). Let Y be an algebraic space over S, let f : X ⟶ Y be decent and of finite type, ℱ a finite type quasi-coherent 𝒪_X-module and y ∈ |Y| (the pre-pure situation P), and let g : X' ⟶ X be étale with X' ⟶ Y decent and of finite type. If Ass_{X/Y}(ℱ) ⊆ g(|X'|) and g^*ℱ is pure above y, then ℱ is pure above y; and if Ass_{X/Y}(ℱ) ⊆ g(|X'|) and g^*ℱ is universally pure above y, then ℱ is universally pure above y.

The situation on X' carrying g^*ℱ is (EtaleOverSource.ofIsEtale P X' g hg hft hdec).situation. The relative assassin Ass_{X/Y}(ℱ) is the relative weak assassin of Stacks 0CV0, which is the set the source writes Ass_{X/Y}(ℱ) since f is of finite type.

theorem isPureAbove_of_isEtale_of_subset_range (hg : IsEtale B S hS g.hom)
    (hft : IsFiniteType B S hS (g.hom ≫ P.f)) (hdec : IsDecent B S hS (g.hom ≫ P.f))
    (hass : relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    (IsPureAbove (EtaleOverSource.ofIsEtale P X' g hg hft hdec).situation → IsPureAbove P) ∧
      (IsUniversallyPureAbove (EtaleOverSource.ofIsEtale P X' g hg hft hdec).situation →
        IsUniversallyPureAbove P)

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_subset_range_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphismClauses.lean, line 231. The attribute's comment: “clause (2), under exactly the source's hypotheses”.

Stacks 0CW3, clause (2). In the situation of clause (1), if ℱ is pure above y, the image g(|X'|) contains the fibre F = f^{-1}(\{y\}), and Y is affine local with closed point y, then Ass_{X/Y}(ℱ) ⊆ g(|X'|).

The proof is the source's: the image of an étale morphism is open (Stacks 03IR), and purity over the affine local base specializes every point of Ass_{X/Y}(ℱ) into F (AlgebraicGeometry.Space.purityFibreSpecialization). Decency and finiteness of type of X' ⟶ Y, which the source assumes throughout the lemma, are not used by this clause, so the statement omits them and is that much more general.

theorem relativeWeaklyAssociatedPoints_subset_range_of_isEtale (hg : IsEtale B S hS g.hom)
    (hpure : IsPureAbove P)
    (hfibre : pointsMap B S hS P.X P.f ⁻¹' {P.y} ⊆ Set.range (pointsMap B S hS X'.1 g.hom))
    (hlocal : P.IsAffineLocalAt) :
    relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_subset_range_of_isEtale_of_isFlatOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityEtaleMorphismClauses.lean, line 255. The attribute's comment: “clause (3), under exactly the source's hypotheses; flatness is flatness of the module over Y at the points of the fibre, as in the source”.

Stacks 0CW3, clause (3). In the situation of clause (1), if ℱ is pure above y, ℱ is flat over Y at all points of the fibre F = f^{-1}(\{y\}) (Stacks 05VV at a point), the image g(|X'|) contains Ass_{X/Y}(ℱ) ∩ F, and Y is affine local with closed point y, then Ass_{X/Y}(ℱ) ⊆ g(|X'|).

As in the source: the image of an étale morphism is open (Stacks 03IR), purity over the affine local base specializes every point of Ass_{X/Y}(ℱ) into F (AlgebraicGeometry.Space.purityFibreSpecialization), and Stacks 0CW1 over the base, which is isomorphic to a scheme of the site, improves that to a specialization into Ass_{X/Y}(ℱ) ∩ F. As for clause (2), decency and finiteness of type of X' ⟶ Y are not used, so the statement omits them and is that much more general.

theorem relativeWeaklyAssociatedPoints_subset_range_of_isEtale_of_isFlatOver
    (hg : IsEtale B S hS g.hom) (hpure : IsPureAbove P)
    (hflat : ∀ t : points B S hS P.X, pointsMap B S hS P.X P.f t = P.y →
      IsFlatOverAtPoint B S hS P.hX P.f P.F t)
    (hfibre : relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ∩
        pointsMap B S hS P.X P.f ⁻¹' {P.y} ⊆ Set.range (pointsMap B S hS X'.1 g.hom))
    (hlocal : P.IsAffineLocalAt) :
    relativeWeaklyAssociatedPoints B S hS P.structureSpaceMorphism P.F ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)

Tag 0CW4, a lemma

Tag 0CW4 in the Stacks Project.

AlgebraicGeometry.Space.isUniversallyPureAbove_of_flat_of_isPureAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/UniversalPurityOfFlatPure.lean, line 330.

Stacks 0CW4. In the situation of Stacks 0CV6 — a decent, finite type morphism f : X ⟶ Y of algebraic spaces over S, a finite type quasi-coherent 𝒪_X-module ℱ and a point y of Y — if ℱ is flat over Y at every point of X lying over y and ℱ is pure above y, then ℱ is universally pure above y.

See the module docstring for the proof: Stacks 0CVW and 05L1 over an affine elementary étale neighbourhood V of the base, the descent of Stacks 0CVG part (2) along the flat morphism Spec 𝒪_{V, v} ⟶ Y, both parts of Stacks 0CW3 over Spec 𝒪_{V, v}, and Stacks 05K6 for the affine scheme with free global sections that Stacks 05L1 produces.

theorem isUniversallyPureAbove_of_flat_of_isPureAbove (P : PrePureSituation.{u, u} B S hS)
    (hflat : ∀ x : points B S hS P.X, pointsMap B S hS P.X P.f x = P.y →
      x ∈ flatLocus B S hS P.hX P.f P.F)
    (hpure : IsPureAbove P) :
    IsUniversallyPureAbove P

Tag 0CW5, a lemma

Tag 0CW5 in the Stacks Project.

AlgebraicGeometry.Space.isPureRelative_iff_isUniversallyPureRelative_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/UniversalPurityOfFlatPure.lean, line 551.

Stacks 0CW5. In the situation of Stacks 0CV6 — a decent, finite type morphism f : X ⟶ Y of algebraic spaces over S and a finite type quasi-coherent 𝒪_X-module ℱ — if ℱ is flat over Y, then ℱ is pure relative to Y if and only if it is universally pure relative to Y.

The forward implication is Stacks 0CW4 at each point of Y, AlgebraicGeometry.Space.isUniversallyPureRelative_of_flat_of_isPureRelative; the reverse one is formal and holds with no flatness, by AlgebraicGeometry.Space.IsPureRelative.of_isUniversallyPureRelative.

theorem isPureRelative_iff_isUniversallyPureRelative_of_flat (P : PrePureSituation.{u, u} B S hS)
    (hflat : ∀ x : points B S hS P.X, x ∈ flatLocus B S hS P.hX P.f P.F) :
    IsPureRelative P ↔ IsUniversallyPureRelative P

Tag 0CW6, a lemma

Tag 0CW6 in the Stacks Project.

AlgebraicGeometry.Space.mono_unit_of_relativeWeaklyAssociatedPoints_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityFlatInjection.lean, line 470. The attribute's comment: “the injectivity assertion”.

Stacks 0CW6, injectivity. Let Y be an algebraic space over a scheme S, let g : X' ⟶ X be a flat morphism of algebraic spaces over Y with X locally of finite type over Y through f : X ⟶ Y, and let F be a finite type quasi-coherent 𝒪_X-module which is flat over Y. If the relative assassin Ass_{X/Y}(F) is contained in the image of |X'| then the canonical map F ⟶ g_*g^*F — the unit of the adjunction of Stacks 03LU — is a monomorphism.

The kernel of the canonical map is zero by AlgebraicGeometry.Space.isZero_of_comp_unit_eq_zero, which is the source's argument; the hypotheses are the tag's own.

theorem mono_unit_of_relativeWeaklyAssociatedPoints_subset_range
    {X' X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : X' ⟶ X)
    (hf : IsLocallyOfFiniteType B S hS f.hom) (hg : IsFlat B S hS g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] [F.IsFiniteType]
    (hF : IsFlatOver B S hS X.2 f.hom F)
    (hass : relativeWeaklyAssociatedPoints B S hS f F ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    Mono ((modulePullbackAdjunction B S hS g).unit.app F)

AlgebraicGeometry.Space.mono_unit_baseChange_of_relativeWeaklyAssociatedPoints_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityFlatInjection.lean, line 502. The attribute's comment: “the base-change assertion”.

Stacks 0CW6, injectivity after an arbitrary base change. In the situation of Stacks 0CW6, for every morphism h : Z ⟶ Y the canonical map F_Z ⟶ (g_Z)_*g_Z^*F_Z is a monomorphism as well.

The base changes are presented by cartesian squares, X_Z as X ×_Y Z and X'_Z as X_Z ×_X X', exactly as the source's proof does, so g is not required to be given as a morphism over Y. This is the source's own deduction: every hypothesis of the first half survives the base change, and the containment of the relative assassin does so by Stacks 0CW2. Concretely

f_Z : X_Z ⟶ Z is locally of finite type by Stacks 03XH;

g_Z : X'_Z ⟶ X_Z is flat by Stacks 03MO;

F_Z = p^*F is quasi-coherent by Stacks 03GA and of finite type by Stacks 03DL(5), both with no hypothesis on p;

F_Z is flat over Z by Stacks 05VW;

Ass_{X_Z/Z}(F_Z) ⊆ g_Z(|X'_Z|) by Stacks 0CW2.

All five are proved, so the hypotheses are the tag's own.

theorem mono_unit_baseChange_of_relativeWeaklyAssociatedPoints_subset_range
    {X' X Y Z XZ X'Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : X' ⟶ X) (h : Z ⟶ Y)
    (p : XZ ⟶ X) (fZ : XZ ⟶ Z) (q : X'Z ⟶ X') (gZ : X'Z ⟶ XZ)
    (hp : IsPullback p fZ f h) (hq : IsPullback q gZ g p)
    (hf : IsLocallyOfFiniteType B S hS f.hom) (hg : IsFlat B S hS g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] [F.IsFiniteType]
    (hF : IsFlatOver B S hS X.2 f.hom F)
    (hass : relativeWeaklyAssociatedPoints B S hS f F ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    Mono ((modulePullbackAdjunction B S hS gZ).unit.app
      ((modulePullback B S hS p).obj F))

Sources

LeanAlgebraicGeometry.Space.exists_specializes_isRelativeWeaklyAssociatedPoint_fibre_schemeBase · AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_baseChange_subset_range · AlgebraicGeometry.Space.EtaleOverSource.isPureAbove_of_isPureAbove_situation · AlgebraicGeometry.Space.EtaleOverSource.isUniversallyPureAbove_of_isUniversallyPureAbove_situation · AlgebraicGeometry.Space.EtaleOverSource.relativeWeaklyAssociatedPoints_subset_range_of_isAffineLocalAt ·

AlgebraicGeometry.Space.EtaleOverSource.relativeWeaklyAssociatedPoints_subset_range_of_isFlatOver_fibre_of_isAffineLocalAt

· AlgebraicGeometry.Space.isPureAbove_of_isEtale_of_subset_range · AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_subset_range_of_isEtale

Section77.7 Flattening functors #

Section 77.7 of the Stacks Project, Tag 083E. 9 tags here are carried by 49 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 083F, a situation

Tag 083F in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctorSmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociSmallEtale.lean, line 126. The attribute's comment: “the functor F_iso of Equation 77.7.1.1”.

Stacks 083F, Equation 77.7.1.1. The functor F_iso of a map u : ℱ ⟶ 𝒢 of quasi-coherent 𝒪_X-modules: it sends a scheme T over Y to a one-element set if the base change u_T along X ×_Y T ⟶ X is an isomorphism, and to the empty set otherwise.

The base change is taken for the inverse image of modules of Stacks 03LU for the small étale ringed sites, AlgebraicGeometry.Space.modulePullback.

abbrev isoFunctorSmallEtale : (D.SchemesOver)ᵒᵖ ⥤ Type u

AlgebraicGeometry.Space.ModuleMapSituation.surjFunctorSmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociSmallEtale.lean, line 138. The attribute's comment: “the variant F_surj”.

Stacks 083F, the variant F_surj. The functor sending a scheme T over Y to a one-element set if the base change u_T is surjective, and to the empty set otherwise.

Surjectivity is restriction-stable because the inverse image of modules is a left adjoint and so preserves epimorphisms; that is AlgebraicGeometry.Space.ModuleMapSituation.isSurjectiveAt_of_hom.

abbrev surjFunctorSmallEtale : (D.SchemesOver)ᵒᵖ ⥤ Type u

AlgebraicGeometry.Space.ModuleMapSituation.zeroFunctorSmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociSmallEtale.lean, line 146. The attribute's comment: “the variant F_zero”.

Stacks 083F, the variant F_zero. The functor sending a scheme T over Y to a one-element set if the base change u_T is zero, and to the empty set otherwise.

abbrev zeroFunctorSmallEtale : (D.SchemesOver)ᵒᵖ ⥤ Type u

AlgebraicGeometry.Space.ModuleMapSituation.IsInjAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociSmallEtale.lean, line 161. The attribute's comment: “the variant F_inj: the condition that u_T is injective”.

Stacks 083F, the variant F_inj. The condition the source asks of a scheme T over Y for its variant F_inj: that the base change u_T of u along X ×_Y T ⟶ X is injective, which for a map of sheaves of modules is being a monomorphism.

This is a condition on test schemes and not a subterminal presheaf on them: it is not stable under restriction along a morphism of test schemes, because the inverse image of modules is only right exact. The file's notes give the counterexample. The restriction-stable condition this development uses in its place is AlgebraicGeometry.Space.ModuleMapSituation.IsUniversallyInjectiveAt.

def IsInjAt (T : D.SchemesOver) : Prop

AlgebraicGeometry.Space.ModuleMapSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituation.lean, line 94. The attribute's comment: “standing data”.

Stacks 083F. The standing data of Stacks 083F: a morphism f : X ⟶ Y of algebraic spaces over S and a map u : F ⟶ G of quasi-coherent 𝒪_X-modules.

structure ModuleMapSituation

AlgebraicGeometry.Space.ModuleMapSituation.zeroSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapZeroLocusSubspace.lean, line 198. The attribute's comment: “the variant F_zero, read as a subfunctor of the base”.

F_zero as a subfunctor of the base. Its sections over an object U of the big fppf category over S are the sections x of Y over U such that the base change of u along X ×_Y U ⟶ X, the base change at the test scheme x names, is zero.

def zeroSubfunctor (D : ModuleMapSituation.{u, u} B S hS) : Subfunctor D.Y.1

Tag 083H, a lemma

Tag 083H in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isSheaf_surjFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFpqcSheaf.lean, line 106. The attribute's comment: “F_surj”.

Stacks 083H, surjectivity clause. The locus of test schemes over Y on which the base change of u is surjective is a sheaf for the fpqc topology.

The locus is subterminal, so the sheaf condition is the implication from surjectivity at every member of a covering sieve to surjectivity at its target. A covering sieve contains a flat family which is jointly surjective after base change, and surjectivity descends along such a family.

theorem isSheaf_surjFunctor :
    Presheaf.IsSheaf (fpqcTopology D.Y) (D.surjFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.isSheaf_zeroFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFpqcSheaf.lean, line 124. The attribute's comment: “F_zero”.

Stacks 083H, vanishing clause. The locus of test schemes over Y on which the base change of u vanishes is a sheaf for the fpqc topology.

The locus is subterminal, so the sheaf condition is the implication from vanishing at every member of a covering sieve to vanishing at its target, and vanishing descends along the flat jointly surjective family of base-change spaces the sieve contains.

theorem isSheaf_zeroFunctor :
    Presheaf.IsSheaf (fpqcTopology D.Y) (D.zeroFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.isSheaf_isoFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFpqcSheaf.lean, line 142. The attribute's comment: “F_iso”.

Stacks 083H, isomorphism clause. The locus of test schemes over Y on which the base change of u is an isomorphism is a sheaf for the fpqc topology.

The locus is subterminal, so the sheaf condition is the implication from being an isomorphism at every member of a covering sieve to being one at its target, and being an isomorphism descends along the flat jointly surjective family of base-change spaces the sieve contains.

theorem isSheaf_isoFunctor :
    Presheaf.IsSheaf (fpqcTopology D.Y) (D.isoFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.isSheaf_injFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFpqcSheaf.lean, line 164. The attribute's comment: “F_inj”.

Stacks 083H, universal injectivity clause. The locus of test schemes over Y on which the base change of u is universally injective is a sheaf for the fpqc topology.

The locus is subterminal, so the sheaf condition is the implication from universal injectivity at every member of a covering sieve to universal injectivity at its target. The latter asks for injectivity of the base change at every test scheme T'' over T; the inverse image of the covering sieve is a covering sieve of T'', and injectivity at each member of that sieve is one instance of universal injectivity at the corresponding member of the given sieve, so injectivity at T'' follows by descent along the flat jointly surjective family of base-change spaces.

theorem isSheaf_injFunctor :
    Presheaf.IsSheaf (fpqcTopology D.Y) (D.injFunctor (modulePullbackSystem B S hS))

Tag 083I, a lemma

Tag 083I in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.surjFunctor_and_zeroFunctor_inverseImageSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapInverseImageLoci.lean, line 90. The attribute's comment: “part (1): F_surj = F'_surj and F_zero = F'_zero”.

Stacks 083I part (1). In Situation 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' : ℱ' ⟶ 𝒢' be the pullback of u to X'. If 𝒢 is of finite type and the image of |X'| ⟶ |X| contains the support of 𝒢, then F_surj = F'_surj and F_zero = F'_zero.

theorem surjFunctor_and_zeroFunctor_inverseImageSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hGft : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hGsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.G) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.surjFunctor (modulePullbackSystem B S hS) =
        (D.inverseImageSituation g).surjFunctor (modulePullbackSystem B S hS) ∧
      D.zeroFunctor (modulePullbackSystem B S hS) =
        (D.inverseImageSituation g).zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_and_zeroFunctor_inverseImageSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapInverseImageLoci.lean, line 105. The attribute's comment: “part (2): F_inj = F'_inj and F_zero = F'_zero”.

Stacks 083I part (2). In Situation 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' : ℱ' ⟶ 𝒢' be the pullback of u to X'. If ℱ is of finite type and the image of |X'| ⟶ |X| contains the support of ℱ, then F_inj = F'_inj and F_zero = F'_zero.

theorem injFunctor_and_zeroFunctor_inverseImageSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hFsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.F) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.injFunctor (modulePullbackSystem B S hS) =
        (D.inverseImageSituation g).injFunctor (modulePullbackSystem B S hS) ∧
      D.zeroFunctor (modulePullbackSystem B S hS) =
        (D.inverseImageSituation g).zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_inverseImageSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapInverseImageLoci.lean, line 120. The attribute's comment: “part (3): F_iso = F'_iso”.

Stacks 083I part (3). In Situation 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' : ℱ' ⟶ 𝒢' be the pullback of u to X'. If ℱ and 𝒢 are of finite type and the image of |X'| ⟶ |X| contains the supports of ℱ and 𝒢, then F_iso = F'_iso.

theorem isoFunctor_inverseImageSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hGft : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hFsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.F) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom))
    (hGsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.G) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.isoFunctor (modulePullbackSystem B S hS) =
      (D.inverseImageSituation g).isoFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.surjFunctor_and_zeroFunctor_pullbackSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFlatPullback.lean, line 738. The attribute's comment: “part (1) over pullbackSituation; see inverseImageSituation”.

Stacks 083I part (1). In the situation of Stacks 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' be the inverse image of u on X'. If 𝒢 is of finite type and the image of |X'| ⟶ |X| contains the support of 𝒢, then the surjectivity loci of u and u' agree and so do their vanishing loci.

Both equalities come from the corresponding conditions at a single test scheme: the comparison X' ×_Y T ⟶ X ×_Y T of the two base changes is flat and its image contains the support of the base change of 𝒢, so surjectivity and vanishing descend along it, and the loci, being subterminal, are determined by the conditions.

The form with the quasi-coherence of g^*ℱ and g^*𝒢 discharged by Stacks 03GA is AlgebraicGeometry.Space.ModuleMapSituation.surjFunctor_and_zeroFunctor_inverseImageSituation_eq.

theorem surjFunctor_and_zeroFunctor_pullbackSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hGft : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hGsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.G) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.surjFunctor (modulePullbackSystem B S hS) =
        (D.pullbackSituation g hF hG).surjFunctor (modulePullbackSystem B S hS) ∧
      D.zeroFunctor (modulePullbackSystem B S hS) =
        (D.pullbackSituation g hF hG).zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_and_zeroFunctor_pullbackSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFlatPullback.lean, line 765. The attribute's comment: “part (2) over pullbackSituation; see inverseImageSituation”.

Stacks 083I part (2). In the situation of Stacks 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' be the inverse image of u on X'. If ℱ is of finite type and the image of |X'| ⟶ |X| contains the support of ℱ, then the universal injectivity loci of u and u' agree and so do their vanishing loci.

Universal injectivity at a test scheme is injectivity of the base change over every further test scheme, and the two situations have the same test schemes, so the equality of the two universal injectivity loci follows from injectivity agreeing at every single test scheme, which is the descent of injectivity along the comparison of the two base changes.

The form with the quasi-coherence of g^*ℱ and g^*𝒢 discharged by Stacks 03GA is AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_and_zeroFunctor_inverseImageSituation_eq.

theorem injFunctor_and_zeroFunctor_pullbackSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hFsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.F) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.injFunctor (modulePullbackSystem B S hS) =
        (D.pullbackSituation g hF hG).injFunctor (modulePullbackSystem B S hS) ∧
      D.zeroFunctor (modulePullbackSystem B S hS) =
        (D.pullbackSituation g hF hG).zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_pullbackSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociFlatPullback.lean, line 792. The attribute's comment: “part (3) over pullbackSituation; see inverseImageSituation”.

Stacks 083I part (3). In the situation of Stacks 083F let g : X' ⟶ X be a flat morphism of algebraic spaces and let u' be the inverse image of u on X'. If ℱ and 𝒢 are of finite type and the image of |X'| ⟶ |X| contains the supports of both, then the isomorphism loci of u and u' agree.

The comparison X' ×_Y T ⟶ X ×_Y T of the two base changes is flat and its image contains the supports of the base changes of ℱ and of 𝒢, so being an isomorphism descends along it at every test scheme, and the loci, being subterminal, are determined by the conditions.

The form with the quasi-coherence of g^*ℱ and g^*𝒢 discharged by Stacks 03GA is AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_inverseImageSituation_eq.

theorem isoFunctor_pullbackSituation_eq (hgflat : IsFlat B S hS g.hom)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hGft : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hFsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.F) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom))
    (hGsupp : supportOfSheaf B S hS D.X.1 ((SheafOfModules.toSheaf _).obj D.G) ⊆
      Set.range (pointsMap B S hS X'.1 g.hom)) :
    D.isoFunctor (modulePullbackSystem B S hS) =
      (D.pullbackSituation g hF hG).isoFunctor (modulePullbackSystem B S hS)

Tag 083J, a lemma

Tag 083J in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_isoFunctor_of_surj_of_inj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreserving.lean, line 317. The attribute's comment: “clause (3), reduced to clause (1) and limit preservation of F_inj; both carried”.

Stacks 083J, clause (3), reduced. The isomorphism locus F_iso is limit preserving once the surjectivity locus F_surj and the universal injectivity locus F_inj are.

The source deduces clause (3) from clauses (1) and (2) through the kernel of u_{T_0}; this is the balanced-category route, available because the categories of 𝒪-modules at hand are abelian, hence balanced. It needs no finiteness hypothesis at all. What is carried is limit preservation of F_surj — clause (1) — and of F_inj.

hinj is not supplied by Stacks 083J. The tag's three clauses are about F_surj, F_zero and F_iso; limit preservation of F_inj is asserted by none of them, so this is a reduction of clause (3) to a statement the source does not prove. Worse for its usefulness, by AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_eq_isoFunctor_of_epi the two functors F_inj and F_iso coincide as soon as u is an epimorphism, so on the situations the source's own proof of clause (3) reduces to — those where clause (1) has produced a stage with u surjective — hinj is verbatim this theorem's conclusion and hsurj holds for free. Neither carry follows from the conclusion in general, so the statement is not circular; but clause (3) is a theorem with nothing carried, AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_isoFunctor in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreservingUnconditional.lean, by the source's own route — limitPreserving_isoFunctor_iff_kernelSituation at the stage clause (1) provides, with Stacks 082T for finite type of the kernel there. Prefer that. This statement is kept because it asks for no finiteness at all.

theorem limitPreserving_isoFunctor_of_surj_of_inj
    (D : ModuleMapSituation.{u, u} B S hS) (P : ModulePullbackSystem.{u, u} B S hS)
    (hsurj : LimitPreserving.{u, u, w, w'} D.testScheme (D.surjFunctor P))
    (hinj : LimitPreserving.{u, u, w, w'} D.testScheme (D.injFunctor P)) :
    LimitPreserving.{u, u, w, w'} D.testScheme (D.isoFunctor P)

AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_surjFunctor_iff_cokernelSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreserving.lean, line 470. The attribute's comment: “clause (1), reduced to clause (2) for the cokernel situation; (2) is carried”.

Stacks 083J, clause (1), reduced to clause (2). The surjectivity locus F_surj of u is limit preserving exactly when the vanishing locus F_zero of the cokernel situation is.

The hypotheses of the two clauses match on the nose: the source module of the cokernel situation is 𝒢 (cokernelSituation_F), so clause (1)'s hypothesis that 𝒢 be of finite type with quasi-compact scheme-theoretic support over B is clause (2)'s hypothesis on the source module of the cokernel situation, and the two situations have the same test category and the same underlying-scheme functor (cokernelSituation_testScheme). What is carried is clause (2) itself — and clause (2) is now a theorem, so clause (1) is available outright as AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_surjFunctor in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreservingUnconditional.lean. This equivalence is the whole of that proof; it is stated here because it needs nothing of clause (2).

theorem limitPreserving_surjFunctor_iff_cokernelSituation :
    LimitPreserving.{u, u, w, w'} D.testScheme (D.surjFunctor (modulePullbackSystem B S hS)) ↔
      LimitPreserving.{u, u, w, w'} D.testScheme
        ((D.cokernelSituation).zeroFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_zeroFunctor_of_isQuasiCompact_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreservingUnconditional.lean, line 551. The attribute's comment: “clause (2): F_zero is limit preserving, at the source's hypotheses verbatim -- F of finite type and its scheme-theoretic support (07U1) quasi-compact over B, i.e. Z -> X -> B quasi-compact. Nothing is carried: the support hypothesis gives compactness of the support at the affine stages (hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport: 03HF on the pasted square Z x_X X_T = Z x_B T, 07U0(4), 03H4), and the rest is limitPreserving_zeroFunctor. The index universe is the universe of the schemes, and must be: the clause is FALSE one universe up, by SmallnessNecessary/Basic.lean”.

Stacks 083J, clause (2), at the source's hypotheses. In the situation of Stacks 083F, if ℱ is of finite type and the scheme-theoretic support of ℱ (Stacks 07U1) is quasi-compact over B, then the vanishing locus F_zero is limit preserving.

The support hypothesis is the source's sentence verbatim: the composite of the inclusion of the scheme-theoretic support Z ⟶ X with f : X ⟶ B is a quasi-compact morphism. It implies the compactness at the affine stages that the proof spends, by hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport, and then this is limitPreserving_zeroFunctor.

theorem limitPreserving_zeroFunctor_of_isQuasiCompact_schemeTheoreticSupport
    (D : ModuleMapSituation.{u, u} B S hS)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hFqc : IsQuasiCompact B S hS ((schemeTheoreticSupport B S hS D.X D.F).ι ≫ D.f.hom)) :
    LimitPreserving.{u, u, u, u} D.testScheme
      (D.zeroFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_surjFunctor_of_isQuasiCompact_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreservingUnconditional.lean, line 573. The attribute's comment: “clause (1): F_surj is limit preserving, at the source's hypotheses verbatim -- G of finite type and its scheme-theoretic support (07U1) quasi-compact over B, i.e. Z -> X -> B quasi-compact. Nothing is carried: the support hypothesis on G is turned into compactness at the affine stages for the cokernel situation (whose source module is G) by hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport, and the rest is limitPreserving_surjFunctor. Index universe as in clause (2)”.

Stacks 083J, clause (1), at the source's hypotheses. In the situation of Stacks 083F, if 𝒢 is of finite type and the scheme-theoretic support of 𝒢 (Stacks 07U1) is quasi-compact over B, then the surjectivity locus F_surj is limit preserving.

The cokernel situation has source module 𝒢, source space X and structure morphism f, so hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport applied to it turns the source's hypothesis on 𝒢 into the one limitPreserving_surjFunctor asks for.

theorem limitPreserving_surjFunctor_of_isQuasiCompact_schemeTheoreticSupport
    (D : ModuleMapSituation.{u, u} B S hS)
    (hGft : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hGqc : IsQuasiCompact B S hS ((schemeTheoreticSupport B S hS D.X D.G).ι ≫ D.f.hom)) :
    LimitPreserving.{u, u, u, u} D.testScheme
      (D.surjFunctor (modulePullbackSystem B S hS))

AlgebraicGeometry.Space.ModuleMapSituation.limitPreserving_isoFunctor_of_isQuasiCompact_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapLociLimitPreservingUnconditional.lean, line 600. The attribute's comment: “clause (3): F_iso is limit preserving, at the source's hypotheses verbatim -- F of finite type, G of finite presentation, and the scheme-theoretic supports (07U1) of F and G quasi-compact over B. Nothing is carried: the two support hypotheses are turned into compactness at the affine stages by hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport (for the situation and for its cokernel situation), and the rest is limitPreserving_isoFunctor, the source's own deduction of (3) from (1) and (2) through ker(u_{T_0}) and Stacks 082T. Index universe as in clause (2)”.

Stacks 083J, clause (3), at the source's hypotheses. In the situation of Stacks 083F, if ℱ is of finite type, 𝒢 is of finite presentation, and the scheme-theoretic supports of ℱ and 𝒢 (Stacks 07U1) are quasi-compact over B, then the isomorphism locus F_iso is limit preserving.

Both support hypotheses are the source's sentence verbatim, and hasQuasiCompactSupportOverTarget_of_isQuasiCompact_schemeTheoreticSupport, applied to the situation and to its cokernel situation, turns them into the ones limitPreserving_isoFunctor asks for; a module of finite presentation is of finite type.

theorem limitPreserving_isoFunctor_of_isQuasiCompact_schemeTheoreticSupport
    (D : ModuleMapSituation.{u, u} B S hS)
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite D.G)
    (hFqc : IsQuasiCompact B S hS ((schemeTheoreticSupport B S hS D.X D.F).ι ≫ D.f.hom))
    (hGqc : IsQuasiCompact B S hS ((schemeTheoreticSupport B S hS D.X D.G).ι ≫ D.f.hom)) :
    LimitPreserving.{u, u, u, u} D.testScheme
      (D.isoFunctor (modulePullbackSystem B S hS))

Tag 0CVM, a lemma

Tag 0CVM in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isIsoAt_secondMap_iff_isZeroAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationExact.lean, line 182. The attribute's comment: “pointwise”.

Stacks 0CVM, pointwise. For an exact sequence F ⟶ G ⟶ H ⟶ 0 of quasi-coherent 𝒪_X-modules and a scheme T over Y, the base change of v : G ⟶ H to X ×_Y T is an isomorphism exactly when the base change of u : F ⟶ G is zero.

theorem isIsoAt_secondMap_iff_isZeroAt (D : ModuleMapSituation.{u, u} B S hS)
    (H : Modules.{u, u} B S hS D.X.1 D.X.2) (hH : H.IsQuasicoherentOnSite)
    (v : D.G ⟶ H) (hcomp : D.u ≫ v = 0)
    (hexact : (ShortComplex.mk D.u v hcomp).Exact) [Epi v] (T : D.SchemesOver) :
    (D.secondMap H hH v).IsIsoAt (modulePullbackSystem B S hS) T ↔
      D.IsZeroAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_secondMap_eq_zeroFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationExact.lean, line 202.

Stacks 0CVM. For an exact sequence F ⟶ G ⟶ H ⟶ 0 of quasi-coherent 𝒪_X-modules, the locus of schemes over Y where the base change of v : G ⟶ H is an isomorphism coincides with the locus where the base change of u : F ⟶ G vanishes.

theorem isoFunctor_secondMap_eq_zeroFunctor (D : ModuleMapSituation.{u, u} B S hS)
    (H : Modules.{u, u} B S hS D.X.1 D.X.2) (hH : H.IsQuasicoherentOnSite)
    (v : D.G ⟶ H) (hcomp : D.u ≫ v = 0)
    (hexact : (ShortComplex.mk D.u v hcomp).Exact) [Epi v] :
    (D.secondMap H hH v).isoFunctor (modulePullbackSystem B S hS) =
      D.zeroFunctor (modulePullbackSystem B S hS)

Tag 0CW7, a lemma

Tag 0CW7 in the Stacks Project.

AlgebraicGeometry.Space.AffineAdjointData.isZeroAt_adjointSituation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 571. The attribute's comment: “part (1), pointwise”.

Stacks 0CW7, part (1), pointwise: the base change of u to a test scheme vanishes exactly when the base change of its adjoint v does.

An adjunction between preadditive categories whose right adjoint is additive carries 0 to 0 and is a bijection, so it carries nothing else to 0.

theorem isZeroAt_adjointSituation_iff (T : (A.sourceSituation hqcH).SchemesOver)
    (hT : A.AdjointAfterBaseChange hqcF hqcH T) :
    (A.adjointSituation hqcF).IsZeroAt (modulePullbackSystem B S hS) T ↔
      (A.sourceSituation hqcH).IsZeroAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.AffineAdjointData.zeroFunctor_adjointSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 603. The attribute's comment: “part (1)”.

Stacks 0CW7, part (1): F_{v,zero} = F_{u,zero}.

theorem zeroFunctor_adjointSituation_eq
    (hT : ∀ T : (A.sourceSituation hqcH).SchemesOver, A.AdjointAfterBaseChange hqcF hqcH T) :
    (A.adjointSituation hqcF).zeroFunctor (modulePullbackSystem B S hS) =
      (A.sourceSituation hqcH).zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.AffineAdjointData.isSurjectiveAt_adjointSituation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 636. The attribute's comment: “part (2), pointwise”.

Stacks 0CW7, part (2), pointwise: for a closed immersion, the base change of u to a test scheme is surjective exactly when the base change of its adjoint v is.

Forward, the factorisation u_T = unit ≫ i_{T,*}(v_T) makes i_{T,*}(v_T) an epimorphism, and the direct image along a closed immersion is fully faithful (AlgebraicGeometry.Space.fullyFaithfulModulePushforward), hence faithful, hence reflects epimorphisms. Backward, the unit is an epimorphism and the direct image preserves them.

theorem isSurjectiveAt_adjointSituation_iff (T : (A.sourceSituation hqcH).SchemesOver)
    (hT : ∃ iT : (A.adjointSituation hqcF).baseChangeSpace T ⟶
        (A.sourceSituation hqcH).baseChangeSpace T,
      A.IsAdjointAfterBaseChange hqcF hqcH T iT ∧
        A.ClosedImmersionSurjectivityInput hqcF hqcH T iT) :
    (A.adjointSituation hqcF).IsSurjectiveAt (modulePullbackSystem B S hS) T ↔
      (A.sourceSituation hqcH).IsSurjectiveAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.AffineAdjointData.surjFunctor_adjointSituation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 666. The attribute's comment: “part (2)”.

Stacks 0CW7, part (2): for a closed immersion, F_{v,surj} = F_{u,surj}.

theorem surjFunctor_adjointSituation_eq
    (hT : ∀ T : (A.sourceSituation hqcH).SchemesOver,
      ∃ iT : (A.adjointSituation hqcF).baseChangeSpace T ⟶
          (A.sourceSituation hqcH).baseChangeSpace T,
        A.IsAdjointAfterBaseChange hqcF hqcH T iT ∧
          A.ClosedImmersionSurjectivityInput hqcF hqcH T iT) :
    (A.adjointSituation hqcF).surjFunctor (modulePullbackSystem B S hS) =
      (A.sourceSituation hqcH).surjFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.AffineAdjointData.zeroFunctor_adjointSituation_eq_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffineAdjoint.lean, line 236. The attribute's comment: “part (1)”.

Stacks 0CW7, part (1), unconditionally: for an affine i : Z ⟶ X, a quasi-coherent 𝒪_Z-module H and a map u : F ⟶ i_*H with adjoint v : i^*F ⟶ H, F_{v,zero} = F_{u,zero}.

theorem zeroFunctor_adjointSituation_eq_of_isAffineHom (hi : IsAffineHom B S hS A.i.hom) :
    (A.adjointSituation A.quasicoherent_modulePullback).zeroFunctor
        (modulePullbackSystem B S hS) =
      (A.sourceSituation (A.quasicoherent_modulePushforward hi)).zeroFunctor
        (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.AffineAdjointData.surjFunctor_adjointSituation_eq_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffineAdjoint.lean, line 246. The attribute's comment: “part (2)”.

Stacks 0CW7, part (2), unconditionally: if moreover i is a closed immersion, F_{v,surj} = F_{u,surj}.

theorem surjFunctor_adjointSituation_eq_of_isClosedImmersion (hi : IsAffineHom B S hS A.i.hom)
    (hci : IsClosedImmersion B S hS A.i.hom) :
    (A.adjointSituation A.quasicoherent_modulePullback).surjFunctor
        (modulePullbackSystem B S hS) =
      (A.sourceSituation (A.quasicoherent_modulePushforward hi)).surjFunctor
        (modulePullbackSystem B S hS)

Tag 0CW8, a lemma

Tag 0CW8 in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isIsoAt_affinePushforward_iff', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 375. The attribute's comment: “the isomorphism locus, pointwise”.

Stacks 0CW8, pointwise for the isomorphism condition: the base change of u' = g_*u to a test scheme is an isomorphism exactly when the base change of u is.

theorem isIsoAt_affinePushforward_iff' (T : D.SchemesOver)
    (hT : D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).IsIsoAt (modulePullbackSystem B S hS) T ↔
      D.IsIsoAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.ModuleMapSituation.isUniversallyInjectiveAt_affinePushforward_iff', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 383. The attribute's comment: “the universal-injectivity locus, pointwise”.

Stacks 0CW8, pointwise for the injectivity condition.

theorem isUniversallyInjectiveAt_affinePushforward_iff' (T : D.SchemesOver)
    (hT : ∀ T' : D.SchemesOver, D.PushforwardIdentifiesBaseChange' g f' hg comm T') :
    (D.affinePushforward' g f' hg).IsUniversallyInjectiveAt
        (modulePullbackSystem B S hS) T ↔
      D.IsUniversallyInjectiveAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.ModuleMapSituation.isSurjectiveAt_affinePushforward_iff', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 393. The attribute's comment: “the surjectivity locus, pointwise”.

Stacks 0CW8, pointwise for the surjectivity condition.

theorem isSurjectiveAt_affinePushforward_iff' (T : D.SchemesOver)
    (hT : D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).IsSurjectiveAt (modulePullbackSystem B S hS) T ↔
      D.IsSurjectiveAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.ModuleMapSituation.isZeroAt_affinePushforward_iff', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 401. The attribute's comment: “the vanishing locus, pointwise”.

Stacks 0CW8, pointwise for the vanishing condition.

theorem isZeroAt_affinePushforward_iff' (T : D.SchemesOver)
    (hT : D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).IsZeroAt (modulePullbackSystem B S hS) T ↔
      D.IsZeroAt (modulePullbackSystem B S hS) T

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_affinePushforward_eq', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 409. The attribute's comment: “F_iso”.

Stacks 0CW8, F_{u,iso} = F_{u',iso}.

theorem isoFunctor_affinePushforward_eq'
    (hT : ∀ T : D.SchemesOver, D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).isoFunctor (modulePullbackSystem B S hS) =
      D.isoFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_affinePushforward_eq', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 421. The attribute's comment: “F_inj”.

Stacks 0CW8, F_{u,inj} = F_{u',inj}.

theorem injFunctor_affinePushforward_eq'
    (hT : ∀ T : D.SchemesOver, D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).injFunctor (modulePullbackSystem B S hS) =
      D.injFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.surjFunctor_affinePushforward_eq', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 433. The attribute's comment: “F_surj”.

Stacks 0CW8, F_{u,surj} = F_{u',surj}.

theorem surjFunctor_affinePushforward_eq'
    (hT : ∀ T : D.SchemesOver, D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).surjFunctor (modulePullbackSystem B S hS) =
      D.surjFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.zeroFunctor_affinePushforward_eq', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffine.lean, line 445. The attribute's comment: “F_zero”.

Stacks 0CW8, F_{u,zero} = F_{u',zero}.

theorem zeroFunctor_affinePushforward_eq'
    (hT : ∀ T : D.SchemesOver, D.PushforwardIdentifiesBaseChange' g f' hg comm T) :
    (D.affinePushforward' g f' hg).zeroFunctor (modulePullbackSystem B S hS) =
      D.zeroFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.isoFunctor_affinePushforward_eq_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffinePushforward.lean, line 127. The attribute's comment: “F_iso”.

Stacks 0CW8, F_{u,iso} = F_{u',iso}: for an affine morphism g : X ⟶ X' over Y, the isomorphism locus of u is that of its direct image u' = g_*u.

theorem isoFunctor_affinePushforward_eq_unconditional :
    (D.affinePushforward g f' (schemeTargetAffinePushforwardQuasicoherent B S hS) hg).isoFunctor
        (modulePullbackSystem B S hS) =
      D.isoFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.injFunctor_affinePushforward_eq_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffinePushforward.lean, line 137. The attribute's comment: “F_inj”.

Stacks 0CW8, F_{u,inj} = F_{u',inj}: for an affine morphism g : X ⟶ X' over Y, the universal-injectivity locus of u is that of its direct image u' = g_*u.

theorem injFunctor_affinePushforward_eq_unconditional :
    (D.affinePushforward g f' (schemeTargetAffinePushforwardQuasicoherent B S hS) hg).injFunctor
        (modulePullbackSystem B S hS) =
      D.injFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.surjFunctor_affinePushforward_eq_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffinePushforward.lean, line 147. The attribute's comment: “F_surj”.

Stacks 0CW8, F_{u,surj} = F_{u',surj}: for an affine morphism g : X ⟶ X' over Y, the surjectivity locus of u is that of its direct image u' = g_*u.

theorem surjFunctor_affinePushforward_eq_unconditional :
    (D.affinePushforward g f' (schemeTargetAffinePushforwardQuasicoherent B S hS) hg).surjFunctor
        (modulePullbackSystem B S hS) =
      D.surjFunctor (modulePullbackSystem B S hS)

AlgebraicGeometry.Space.ModuleMapSituation.zeroFunctor_affinePushforward_eq_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapSituationAffinePushforward.lean, line 157. The attribute's comment: “F_zero”.

Stacks 0CW8, F_{u,zero} = F_{u',zero}: for an affine morphism g : X ⟶ X' over Y, the vanishing locus of u is that of its direct image u' = g_*u.

theorem zeroFunctor_affinePushforward_eq_unconditional :
    (D.affinePushforward g f' (schemeTargetAffinePushforwardQuasicoherent B S hS) hg).zeroFunctor
        (modulePullbackSystem B S hS) =
      D.zeroFunctor (modulePullbackSystem B S hS)

Tag 0CWX, a situation

Tag 0CWX in the Stacks Project.

AlgebraicGeometry.Space.FlatnessSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctor.lean, line 126. The attribute's comment: “standing data”.

Stacks 0CWX. The standing data of Stacks 0CWX: a morphism f : X ⟶ Y of algebraic spaces over S and a quasi-coherent 𝒪_X-module F, whose base changes to the schemes over Y are tested for flatness.

structure FlatnessSituation

AlgebraicGeometry.Space.FlatnessSituation.baseChangeModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctor.lean, line 145. The attribute's comment: “the base change F_T of the module to a test scheme over the target”.

Stacks 0CWX. The base change F_T of the module to a test scheme T over Y: the pullback of F along the projection X_T = X ×_Y T ⟶ X.

def baseChangeModule (D : FlatnessSituation.{u} B S hS) (T : SchemesOver D.Y) :
    Modules.{u, u} B S hS (baseChangeSpace D.f T).1 (baseChangeSpace D.f T).2

AlgebraicGeometry.Space.FlatnessSituation.flatFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctor.lean, line 202. The attribute's comment: “the functor F_flat”.

Stacks 0CWX. The flattening functor

F_flat : (Sch/Y)ᵒᵖ ⥤ Sets, T ↦ {*} if F_T is flat over T and ∅ otherwise.

Its value at a test scheme is a subtype of a one-element type, cut out by flatness of the base change there; that this is stable under a morphism of test schemes, which is what makes the assignment a functor, is AlgebraicGeometry.Space.FlatnessSituation.isFlatAfterBaseChange_of_hom.

def flatFunctor (D : FlatnessSituation.{u} B S hS) : (SchemesOver D.Y)ᵒᵖ ⥤ Type u

Tag 0CWZ, a lemma

Tag 0CWZ in the Stacks Project.

AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorLimitPreserving.lean, line 218. The attribute's comment: “part (2), at the tag's own hypotheses; the index universe of the cofiltered system is the universe of the schemes, which is the largest Stacks 05LY admits”. References: EGA IV (11.2.6.1), “(ii)”.

Stacks 0CWZ, part (2). Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S which is locally of finite presentation and let F be a quasi-coherent 𝒪_X-module of finite presentation. Then the functor F_flat of equation 0CWY is limit preserving in the sense of Stacks 049J: it carries a cofiltered inverse limit of affine test schemes over Y to a filtered colimit of sets.

F_flat is subterminal, so limit preservation is, by AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_limitPreserving_iff, the assertion that flatness of F_T over a cofiltered limit T of affine test schemes already holds over one of the stages. Pick a stage, read the condition over it on an affine surjective étale scheme chart of X_{T_i} of finite presentation over T_i (AlgebraicGeometry.Space.FlatnessSituation.exists_affine_testChart), and the condition at every test scheme over that stage becomes flatness of the Zariski inverse image of the chart restriction over the base-changed chart scheme (AlgebraicGeometry.Space.FlatnessSituation.TestChart.isFlatAfterBaseChange_baseChange_iff). That is the statement the scheme-level descent theorem Stacks 05LY, AlgebraicGeometry.eventually_isFlatOver_modulePullback, descends to a stage; its hypotheses on the chart are finite presentation of its structure morphism and finite presentation of the restricted module, which are the two preceding results.

theorem flatFunctor_limitPreserving (D : FlatnessSituation.{u} B S hS)
    (hqc : IsQuasiCompact B S hS D.f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS D.f.hom)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite D.F) :
    LimitPreserving.{u, u, u, u, u + 1, u} D.testScheme D.flatFunctor

AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_isSeparatedFor_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorSheafAndLimits.lean, line 230. The attribute's comment: “part (1), separatedness half only; gluing half not proved”.

Stacks 0CWZ, part (1), the separatedness half of the fpqc sheaf property. Two sections of F_flat over a test scheme which agree on the members of an fpqc covering presieve of that test scheme are equal.

Every value of F_flat has at most one element, so this holds for an arbitrary presieve; the fpqc hypothesis is carried only so that the statement is the one the source makes. The existence half of the sheaf condition is fpqc descent of flatness of the base-changed module; it is proved separately, so that part (1) holds in full, as AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_isSheafFor_fpqc and AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_isSheaf_fpqcTopology.

theorem flatFunctor_isSeparatedFor_fpqc (D : FlatnessSituation.{u} B S hS)
    {T : SchemesOver D.Y} (R : Presieve T)
    (_hR : R ∈ D.testFpqcPrecoverage T) :
    Presieve.IsSeparatedFor D.flatFunctor R

AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_isSheaf_fpqcTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorSheafAndLimits.lean, line 367. The attribute's comment: “part (1)”.

Stacks 0CWZ, part (1). The functor F_flat satisfies the sheaf property for the fpqc topology on the test schemes over Y.

F_flat is subterminal, so the sheaf condition for a covering sieve is the implication from flatness of the base-changed module at every member of the sieve to flatness at its target. A covering sieve of the fpqc topology contains a flat family which is jointly surjective on points — AlgebraicGeometry.Space.exists_isFpqcCovering_jointlySurjective_family_of_mem_fpqcTopology — and flatness of the base-changed module descends along such a family by AlgebraicGeometry.Space.FlatnessSituation.isFlatAfterBaseChange_of_jointlySurjective.

theorem flatFunctor_isSheaf_fpqcTopology (D : FlatnessSituation.{u} B S hS) :
    Presheaf.IsSheaf (fpqcTopology D.Y) D.flatFunctor

AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_isSheafFor_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorSheafAndLimits.lean, line 384. The attribute's comment: “part (1), the sheaf condition for a covering presieve”.

Stacks 0CWZ, part (1), in the presieve form: F_flat satisfies the sheaf condition for every fpqc covering presieve of a test scheme over Y.

The sieve a covering presieve generates is a covering sieve of the fpqc topology, and every member of that sieve factors through a member of the presieve, along which flatness of the base-changed module is inherited by the final assertion of Stacks 05VW.

theorem flatFunctor_isSheafFor_fpqc (D : FlatnessSituation.{u} B S hS)
    {T : SchemesOver D.Y} (R : Presieve T) (hR : R ∈ D.testFpqcPrecoverage T) :
    Presieve.IsSheafFor D.flatFunctor R

AlgebraicGeometry.Space.FlatnessSituation.subsingleton_colimitType_flatFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorSheafAndLimits.lean, line 423. The attribute's comment: “part (2), injectivity half only; surjectivity not proved”.

Stacks 0CWZ, part (2), the uniqueness half of limit preservation. Along a cofiltered system of test schemes over Y, the filtered colimit of the values of F_flat has at most one element.

Limit preservation asserts that the canonical map from that colimit to the value of F_flat at the limit test scheme is a bijection. This is its injectivity half: the target also has at most one element (flatFunctor_obj_subsingleton), so no two classes in the colimit can be separated. It needs none of the hypotheses of part (2) — not quasi-compactness or local finite presentation of f, not finite presentation of F — and no restriction on the index universes. The surjectivity half does need them and is AlgebraicGeometry.Space.FlatnessSituation.flatFunctor_limitPreserving of StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFunctorLimitPreserving.lean, which is part (2) in full.

theorem subsingleton_colimitType_flatFunctor (D : FlatnessSituation.{u} B S hS)
    {I : Type w} [Category.{w'} I] [IsCofiltered I]
    (E : I ⥤ SchemesOver D.Y) :
    Subsingleton ((E.op ⋙ D.flatFunctor).ColimitType)

Sources

Section77.8 Making a map zero #

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

Tag 0CWA, a situation

Tag 0CWA in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapFlatTargetSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapFlatTargetSituation.lean, line 68.

Stacks 0CWA. The standing data of Stacks 0CWA: an affine base S = Spec R, an algebraic space X over S, and a map u : F ⟶ G of quasi-coherent 𝒪_X-modules whose target is flat over S.

structure ModuleMapFlatTargetSituation [IsAffine S]

Tag 083K, a lemma

Tag 083K in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.exists_closedSubscheme_isZeroAt_of_isZeroAt_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartMapQuasiCompactTest.lean, line 273. The attribute's comment: “main clause”.

The main clause of Stacks 083K.

In Situation 0CWA — S = \Spec(R) affine, X an algebraic space over S, u : ℱ ⟶ 𝒢 a map of quasi-coherent 𝒪_X-modules with 𝒢 flat over S — let T ⟶ S be a quasi-compact morphism of schemes such that the base change u_T is zero. Then there is a closed subscheme Z ⊆ S such that (a) T ⟶ S factors through Z and (b) the base change u_Z is zero.

The subscheme is Z = \Spec(\Gamma(S, ⊤)/I) for I = \ker(\Gamma(S, ⊤) ⟶ \Gamma(T, ⊤)), the smallest closed subscheme of S through which T ⟶ S factors; the factorisation is therefore AlgebraicGeometry.Space.exists_hom_specQuotientOver at an equality of ideals. That I kills the image of u over every affine chart is val_app_mem_ker_smul_top_of_isZeroAt_of_quasiCompact, and AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.isZeroAt_specQuotient_of_forall_mem_smul_top turns that into u_Z = 0.

theorem exists_closedSubscheme_isZeroAt_of_isZeroAt_of_quasiCompact (T : BigFppfOver B S hS)
    (hqc : QuasiCompact (B.inclusion.map T.hom))
    (hzero : (D.toModuleMapSituation B S hS).IsZeroAt (modulePullbackSystem B S hS)
      (D.baseTest B S hS T)) :
    ∃ Z : BigFppfOver B S hS,
      _root_.AlgebraicGeometry.IsClosedImmersion (B.inclusion.map Z.hom) ∧ Nonempty (T ⟶ Z) ∧
        (D.toModuleMapSituation B S hS).IsZeroAt (modulePullbackSystem B S hS)
          (D.baseTest B S hS Z)

AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.exists_closedSubscheme_isZeroAt_locallyOfFinitePresentation_of_isZeroAt_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartMapQuasiCompactTest.lean, line 349. The attribute's comment: “finite presentation clause”.

The finite-presentation clause of Stacks 083K, in the shape the source states it.

In Situation 0CWA, assume in addition that ℱ is a finite type 𝒪_X-module whose scheme theoretic support is quasi-compact, and let T ⟶ S be a quasi-compact morphism of schemes such that the base change u_T is zero. Then there is a closed subscheme Z ⊆ S, locally of finite presentation over S — and affine, hence quasi-compact and quasi-separated, so of finite presentation — through which T ⟶ S factors and at which u_Z = 0.

This is exists_fg_ideal_isZeroAt_specQuotient_of_quasiCompact with Z = \Spec(\Gamma(S, ⊤)/J), whose closed immersion into S is AlgebraicGeometry.Space.isClosedImmersion_specQuotientToBase.

theorem exists_closedSubscheme_isZeroAt_locallyOfFinitePresentation_of_isZeroAt_of_quasiCompact
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F)
    (hcpt : CompactSpace (points B S hS (schemeTheoreticSupport B S hS D.X D.F).toFunctor))
    (T : BigFppfOver B S hS) (hqc : QuasiCompact (B.inclusion.map T.hom))
    (hzero : (D.toModuleMapSituation B S hS).IsZeroAt (modulePullbackSystem B S hS)
      (D.baseTest B S hS T)) :
    ∃ Z : BigFppfOver B S hS,
      _root_.AlgebraicGeometry.IsClosedImmersion (B.inclusion.map Z.hom) ∧
        LocallyOfFinitePresentation (B.inclusion.map Z.hom) ∧ Nonempty (T ⟶ Z) ∧
        (D.toModuleMapSituation B S hS).IsZeroAt (modulePullbackSystem B S hS)
          (D.baseTest B S hS Z)

Tag 083L, a lemma

Tag 083L in the Stacks Project.

Module.exists_ideal_rTensor_eq_zero_iff_map_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/VanishingAfterBaseChange.lean, line 48.

Stacks Project, Tag 083L. If the target of a linear map is projective, the base changes on which the map vanishes are cut out by an ideal of the base ring.

theorem exists_ideal_rTensor_eq_zero_iff_map_eq_bot
    {A : Type u} [CommRing A]
    {M : Type v} [AddCommGroup M] [Module A M]
    {N : Type w} [AddCommGroup N] [Module A N]
    (f : M →ₗ[A] N) (hN : Module.Projective A N) :
    ∃ I : Ideal A, ∀ (B : Type x) [CommRing B] (φ : A →+* B),
      letI := φ.toAlgebra
      f.rTensor B = 0 ↔ Ideal.map φ I = ⊥

Tag 0CWB, a lemma

Tag 0CWB in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.fibreMapEqZero_of_mem_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleMapVanishingAlongClosureProjective.lean, line 231.

In Situation 0CWA, let T be a subset of the base and let s be a point of the closure of T. If X is locally of finite presentation over the base, 𝒢 is of finite presentation, and u_t = 0 for every t ∈ T, then u_s = 0.

The geometric reduction is ModuleMapFlatTargetSituation.fibreMapEqZero_of_mem_closure_of_forall_point, which asks for one affine étale chart per point of |X| at which the ideal condition passes from T to s. The chart is produced by Stacks 0CVY, AlgebraicGeometry.Space.exists_isAffine_etale_charts_projective_sections_of_isFlatOverAt, whose three hypotheses are discharged from the two finite-presentation hypotheses and the flatness carried by Situation 0CWA; the ideal condition at the chart it returns is ModuleMapFlatTargetSituation.forall_mem_basePointIdeal_smul_top_of_projective_pullback. See the implementation notes of this file.

theorem fibreMapEqZero_of_mem_closure
    (hfp : IsLocallyOfFinitePresentation B S hS (D.structureMorphism B S hS).hom)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite D.G)
    (T : Set S) (s : S) (hs : s ∈ closure T)
    (hT : ∀ t ∈ T, D.FibreMapEqZero B S hS t) :
    D.FibreMapEqZero B S hS s

Tag 0CWC, a lemma

Tag 0CWC in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isClosedSubspace_zeroSubfunctor_of_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroLocusClosedUnconditional.lean, line 72. The attribute's comment: “closed immersion: the vanishing locus is a closed subspace of the base, at the source's hypotheses alone”.

Stacks 0CWC, the closed-immersion clause. In Situation 083F, assume (1) f is of finite presentation and (2) 𝒢 is of finite presentation, flat over the base and pure relative to it. Then the vanishing locus of u is a closed subspace of the base.

The hypotheses are the source's, and only those: purity relative to the base is stated on the situation of Stacks 0CV6 whose finite-type and decency conditions are derived from (1) and (2) by fpTargetPrePureSituation, as the source does implicitly.

theorem isClosedSubspace_zeroSubfunctor_of_isPureRelative (D : ModuleMapSituation.{u, u} B S hS)
    (hf : IsFinitePresentation B S hS D.f.hom)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite D.G)
    (hGflat : _root_.AlgebraicGeometry.Space.IsFlatOver B S hS D.X.2 D.f.hom D.G)
    (hpure : ∀ y : points B S hS D.Y.1, IsPureRelative (D.fpTargetPrePureSituation hf hGfp y)) :
    IsClosedSubspace B S hS D.zeroSubfunctor

AlgebraicGeometry.Space.ModuleMapSituation.isFinitePresentation_zeroSubfunctor_ι_of_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroLocusClosedUnconditional.lean, line 88. The attribute's comment: “finite presentation: the vanishing locus is of finite presentation over the base when the source module is of finite type, at the source's hypotheses alone”.

Stacks 0CWC, the finite-presentation clause. Under the hypotheses of isClosedSubspace_zeroSubfunctor_of_isPureRelative, if moreover ℱ is of finite type, the vanishing locus of u is of finite presentation over the base.

theorem isFinitePresentation_zeroSubfunctor_ι_of_isPureRelative
    (D : ModuleMapSituation.{u, u} B S hS)
    (hf : IsFinitePresentation B S hS D.f.hom)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite D.G)
    (hGflat : _root_.AlgebraicGeometry.Space.IsFlatOver B S hS D.X.2 D.f.hom D.G)
    (hpure : ∀ y : points B S hS D.Y.1, IsPureRelative (D.fpTargetPrePureSituation hf hGfp y))
    (hFft : SheafOfModules.IsFiniteTypeOnSite D.F) :
    IsFinitePresentation B S hS D.zeroSubfunctor.ι

Tag 083M, a lemma

Tag 083M in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.zeroLocusRepresentation_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroLocusClosedProperSupportUnconditional.lean, line 369. The attribute's comment: “every case: f locally of finite presentation (which includes the case of the first paragraph of the proof, f of finite presentation), G of finite presentation and flat over B, the support of G proper over B; F_zero is represented by a closed subspace of B, of finite presentation over B when F is of finite type -- at the source's hypotheses alone”.

Stacks 083M. In Situation 083F, assume that 1. f is locally of finite presentation, 2. 𝒢 is an 𝒪_X-module of finite presentation flat over B, 3. the support of 𝒢 is proper over B.

Then the functor F_zero is an algebraic space and F_zero ⟶ B is a closed immersion; if ℱ is of finite type, then F_zero ⟶ B is of finite presentation.

The conclusion AlgebraicGeometry.Space.ModuleMapSituation.ZeroLocusRepresentation is the existence of a subfunctor Z of B which is a closed subspace (an algebraic space whose inclusion is a closed immersion), whose inclusion is of finite presentation when ℱ is of finite type, and which represents F_zero. The hypotheses are exactly the source's.

The proof is the source's: pass to the closed subspace cut out by the zeroth Fitting ideal of 𝒢 (AlgebraicGeometry.Space.ModuleMapSituation.nonempty_fittingReduction) and apply Stacks 0CWC there, whose dévissage is AlgebraicGeometry.Space.ModuleMapSituation.devissageInput. The case of the first paragraph of the proof, f of finite presentation, is the special case of a morphism of finite presentation, which is in particular locally of finite presentation.

theorem zeroLocusRepresentation_of_hasProperSupport (D : ModuleMapSituation.{u, u} B S hS)
    (hf : IsLocallyOfFinitePresentation B S hS D.f.hom)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite D.G)
    (hGflat : IsFlatOver B S hS D.X.property D.f.hom D.G)
    (hproper : HasProperSupport B S hS D.X.property D.Y.property D.f.hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hf)
      ((SheafOfModules.toSheaf _).obj D.G)) :
    D.ZeroLocusRepresentation

Sources

LeanAlgebraicGeometry.Space.ModuleMapFlatTargetSituation · AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.exists_closedSubscheme_isZeroAt_of_isZeroAt_of_quasiCompact ·

AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.exists_closedSubscheme_isZeroAt_locallyOfFinitePresentation_of_isZeroAt_of_quasiCompact

· Module.exists_ideal_rTensor_eq_zero_iff_map_eq_bot · AlgebraicGeometry.Space.ModuleMapFlatTargetSituation.fibreMapEqZero_of_mem_closure · AlgebraicGeometry.Space.ModuleMapSituation.isClosedSubspace_zeroSubfunctor_of_isPureRelative · AlgebraicGeometry.Space.ModuleMapSituation.isFinitePresentation_zeroSubfunctor_ι_of_isPureRelative · AlgebraicGeometry.Space.ModuleMapSituation.zeroLocusRepresentation_of_hasProperSupport

Section77.9 Flattening a map #

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

Tag 0CWD, a theorem

Tag 0CWD in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isoLocusRepresentation_of_isPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IsoLocusClosedOfPure.lean, line 117. The attribute's comment: “F_iso is represented by a closed subspace Z of the base, and Z → B is of finite presentation when 𝒢 is of finite presentation (the source's 'Z → S' is a misprint for Z → B, see the module notes)”.

Stacks 0CWD. In Situation 083F, assume (1) f is of finite presentation, (2) ℱ is of finite presentation, flat over B and pure relative to B, and (3) u is surjective. Then F_iso is representable by a closed immersion Z ⟶ B: there is a closed subspace Z of B such that a scheme T over B lies in F_iso — the base change u_T is an isomorphism — exactly when its structure morphism factors through Z. Moreover Z ⟶ B is of finite presentation if 𝒢 is of finite presentation.

The source writes Z ⟶ S in the last sentence, which is false as written; its proof gives Z ⟶ B, and that is what is stated. See the implementation notes of this file.

theorem isoLocusRepresentation_of_isPureRelative
    (D : ModuleMapSituation.{u, u} B S hS)
    (hf : IsFinitePresentation B S hS D.f.hom)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite D.F)
    (hFflat : _root_.AlgebraicGeometry.Space.IsFlatOver B S hS D.X.2 D.f.hom D.F)
    (hpure : ∀ y : points B S hS D.Y.1, IsPureRelative (D.fpSourcePrePureSituation hf hFfp y))
    [Epi D.u] :
    D.IsoLocusRepresentation

Tag 083N, a lemma

Tag 083N in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.isoLocusRepresentation_of_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IsoLocusClosedProperSupport.lean, line 74. The attribute's comment: “the full statement at the source's hypotheses alone: f locally of finite presentation, F locally of finite presentation and flat over B with support proper over B, u surjective; F_iso is represented by a closed subspace of B, of finite presentation over B when G is of finite presentation”.

Stacks 083N. In Situation 083F, assume that 1. f is locally of finite presentation, 2. ℱ is locally of finite presentation and flat over B, 3. the support of ℱ is proper over B, and 4. u is surjective.

Then the functor F_iso is an algebraic space and F_iso ⟶ B is a closed immersion; if 𝒢 is of finite presentation, then F_iso ⟶ B is of finite presentation.

The conclusion AlgebraicGeometry.Space.ModuleMapSituation.IsoLocusRepresentation is the existence of a subfunctor Z of B which is a closed subspace (an algebraic space whose inclusion is a closed immersion), whose inclusion is of finite presentation when 𝒢 is of finite presentation, and which represents F_iso. Being of finite presentation is a local condition for modules on a site, so SheafOfModules.IsFinitePresentationOnSite is the source's "locally of finite presentation". The hypotheses are exactly the source's.

The proof is the source's: Stacks 083M applied to the kernel inclusion Ker(u) ⟶ ℱ (AlgebraicGeometry.Space.ModuleMapSituation.zeroLocusRepresentation_of_hasProperSupport on AlgebraicGeometry.Space.ModuleMapSituation.kernelSituation), transported to F_iso by Stacks 0CVM and Stacks 082T (AlgebraicGeometry.Space.ModuleMapSituation.isoLocusRepresentation_of_kernelSituation).

theorem isoLocusRepresentation_of_hasProperSupport (D : ModuleMapSituation.{u, u} B S hS)
    (hf : IsLocallyOfFinitePresentation B S hS D.f.hom)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite D.F)
    (hFflat : IsFlatOver B S hS D.X.property D.f.hom D.F)
    (hproper : HasProperSupport B S hS D.X.property D.Y.property D.f.hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hf)
      ((SheafOfModules.toSheaf _).obj D.F))
    (hu : Epi D.u) :
    D.IsoLocusRepresentation

Tag 09TP, a lemma

Tag 09TP in the Stacks Project.

AlgebraicGeometry.Space.ModuleMapSituation.exists_isOpenSubspace_isSurjectiveAt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveLocusOpenSubspace.lean, line 308. References: SGA 6 XII (4.6), “partial”.

Stacks 09TP. In the situation of Stacks 083F, assume that f is locally of finite presentation, that G is of finite type and that the support of G is proper over Y. Then the locus F_surj on which the base change of u is surjective is represented by an open subspace of Y; in particular it is an algebraic space and its morphism to Y is an open immersion.

The open subspace is the one of Stacks 03BZ on the complement of |f|(Supp(Coker u)), which is open because that image is closed by Stacks 0CZG, the support of the cokernel being a closed subset of the support of G and hence proper over Y. The identification at a test scheme is AlgebraicGeometry.Space.ModuleMapSituation.isSurjectiveAt_iff_range_pointsMap_subset.

theorem exists_isOpenSubspace_isSurjectiveAt_iff
    (hf : IsLocallyOfFinitePresentation B S hS D.f.hom)
    (hG : SheafOfModules.IsFiniteTypeOnSite D.G)
    (hproper : HasProperSupport B S hS D.X.property D.Y.property D.f.hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hf)
      ((SheafOfModules.toSheaf _).obj D.G)) :
    ∃ U : Subfunctor D.Y.1, IsOpenSubspace B S hS U ∧
      ∀ T : D.SchemesOver,
        D.IsSurjectiveAt (modulePullbackSystem B S hS) T ↔
          ∃ k : yoneda.obj T.left ⟶ U.toFunctor, k ≫ U.ι = T.hom.hom

Sources

LeanAlgebraicGeometry.Space.ModuleMapSituation.isoLocusRepresentation_of_isPureRelative · AlgebraicGeometry.Space.ModuleMapSituation.isoLocusRepresentation_of_hasProperSupport · AlgebraicGeometry.Space.ModuleMapSituation.exists_isOpenSubspace_isSurjectiveAt_iff

Section77.10 Flattening in the local case #

Section 77.10 of the Stacks Project, Tag 0CWN. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CWP, a lemma

Tag 0CWP in the Stacks Project.

AlgebraicGeometry.Space.exists_idealSheafData_isFlatOverAtPoint_iff_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/LocalFlattening.lean, line 406. The attribute's comment: “the closed flattening subscheme, for an arbitrary subset E of the closed fibre: nothing is assumed beyond the source's hypotheses”.

Stacks Project, Tag 0CWP. Let S = Spec A be the spectrum of a henselian local ring with closed point s, let f : X ⟶ S be a morphism of algebraic spaces which is locally of finite type, let F be a quasi-coherent 𝒪_X-module of finite type and let E ⊆ |X_s| be a subset. There is a closed subscheme Z ⊆ S such that for every morphism of pointed schemes (T, t) ⟶ (S, s) the following are equivalent:

F_T is flat over T at all points of |X_t| which map to a point of E ⊆ |X_s|;

Spec 𝒪_{T,t} ⟶ S factors through Z.

Here X is an algebraic space over S, f its structure morphism to the terminal algebraic space S, and X_T = X ×_S T the fibre product of algebraic spaces; the points of |X_t| are the points of |X_T| over t ∈ |T|, and the closed fibre |X_s| is the set of points of |X| over s, through which a point of |X_t| maps to |X_s| by its image in |X|. Flatness of F_T over T at a point is Stacks 05VV at a point, and Z is given by its ideal sheaf.

theorem exists_idealSheafData_isFlatOverAtPoint_iff_factors [HenselianLocalRing A]
    (X : AlgebraicSpaces B (Spec (.of A)) hA) (f : X ⟶ schemeSpace (Over.mk (𝟙 (B.obj hA))))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) (hFq : F.IsQuasicoherentOnSite)
    (hFt : SheafOfModules.IsFiniteTypeOnSite F)
    (E : Set {x : points B (Spec (.of A)) hA X.1 //
      pointsMap B (Spec (.of A)) hA X.1 f.hom x = closedBasePoint A B hA}) :
    ∃ Z : (Spec (.of A)).IdealSheafData,
      ∀ (T : BigFppfOver B (Spec (.of A)) hA) (g : T ⟶ Over.mk (𝟙 (B.obj hA)))
        (t : (BigFppfOver.toScheme B (Spec (.of A)) hA).obj T),
        (BigFppfOver.toScheme B (Spec (.of A)) hA).map g t = IsLocalRing.closedPoint A →
        ((∀ x' : points B (Spec (.of A)) hA (pullback f (schemeSpaceMap g)).1,
            pointsMap B (Spec (.of A)) hA _ (pullback.snd f (schemeSpaceMap g)).hom x' =
              (pointsEquivScheme B (Spec (.of A)) hA T).symm t →
            ∀ hx : pointsMap B (Spec (.of A)) hA X.1 f.hom
                (pointsMap B (Spec (.of A)) hA _ (pullback.fst f (schemeSpaceMap g)).hom x') =
                closedBasePoint A B hA,
              (⟨_, hx⟩ : {x : points B (Spec (.of A)) hA X.1 //
                pointsMap B (Spec (.of A)) hA X.1 f.hom x = closedBasePoint A B hA}) ∈ E →
              IsFlatOverAtPoint B (Spec (.of A)) hA (pullback f (schemeSpaceMap g)).2
                (pullback.snd f (schemeSpaceMap g)).hom
                ((modulePullback B (Spec (.of A)) hA (pullback.fst f (schemeSpaceMap g))).obj F)
                x') ↔
          ∃ h : Spec (((BigFppfOver.toScheme B (Spec (.of A)) hA).obj T).presheaf.stalk t) ⟶
              Z.subscheme,
            h ≫ Z.subschemeι = ((BigFppfOver.toScheme B (Spec (.of A)) hA).obj T).fromSpecStalk t ≫
              (BigFppfOver.toScheme B (Spec (.of A)) hA).map g)

AlgebraicGeometry.Space.exists_finitePresentation_idealSheafData_isFlatOverAtPoint_iff_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/LocalFlattening.lean, line 460. The attribute's comment: “the finite-presentation assertion, for E closed and quasi-compact in |X_s|: nothing is assumed beyond the source's hypotheses”.

Stacks Project, Tag 0CWP, the final assertion. In the situation of AlgebraicGeometry.Space.exists_idealSheafData_isFlatOverAtPoint_iff_factors, if moreover X ⟶ S is locally of finite presentation, F is of finite presentation and E ⊆ |X_s| is closed and quasi-compact, then the closed subscheme Z may be chosen with Z ⟶ S of finite presentation. The topology on |X_s| is the subspace topology of the closed fibre in |X| (Stacks 03BY).

theorem exists_finitePresentation_idealSheafData_isFlatOverAtPoint_iff_factors
    [HenselianLocalRing A]
    (X : AlgebraicSpaces B (Spec (.of A)) hA) (f : X ⟶ schemeSpace (Over.mk (𝟙 (B.obj hA))))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f.hom)
    (hfp : IsLocallyOfFinitePresentation B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) (hFq : F.IsQuasicoherentOnSite)
    (hFt : SheafOfModules.IsFiniteTypeOnSite F) (hFp : SheafOfModules.IsFinitePresentationOnSite F)
    (E : Set {x : points B (Spec (.of A)) hA X.1 //
      pointsMap B (Spec (.of A)) hA X.1 f.hom x = closedBasePoint A B hA})
    (hEc : IsClosed E) (hEk : IsCompact E) :
    ∃ Z : (Spec (.of A)).IdealSheafData,
      AlgebraicGeometry.FinitePresentation Z.subschemeι ∧
      ∀ (T : BigFppfOver B (Spec (.of A)) hA) (g : T ⟶ Over.mk (𝟙 (B.obj hA)))
        (t : (BigFppfOver.toScheme B (Spec (.of A)) hA).obj T),
        (BigFppfOver.toScheme B (Spec (.of A)) hA).map g t = IsLocalRing.closedPoint A →
        ((∀ x' : points B (Spec (.of A)) hA (pullback f (schemeSpaceMap g)).1,
            pointsMap B (Spec (.of A)) hA _ (pullback.snd f (schemeSpaceMap g)).hom x' =
              (pointsEquivScheme B (Spec (.of A)) hA T).symm t →
            ∀ hx : pointsMap B (Spec (.of A)) hA X.1 f.hom
                (pointsMap B (Spec (.of A)) hA _ (pullback.fst f (schemeSpaceMap g)).hom x') =
                closedBasePoint A B hA,
              (⟨_, hx⟩ : {x : points B (Spec (.of A)) hA X.1 //
                pointsMap B (Spec (.of A)) hA X.1 f.hom x = closedBasePoint A B hA}) ∈ E →
              IsFlatOverAtPoint B (Spec (.of A)) hA (pullback f (schemeSpaceMap g)).2
                (pullback.snd f (schemeSpaceMap g)).hom
                ((modulePullback B (Spec (.of A)) hA (pullback.fst f (schemeSpaceMap g))).obj F)
                x') ↔
          ∃ h : Spec (((BigFppfOver.toScheme B (Spec (.of A)) hA).obj T).presheaf.stalk t) ⟶
              Z.subscheme,
            h ≫ Z.subschemeι = ((BigFppfOver.toScheme B (Spec (.of A)) hA).obj T).fromSpecStalk t ≫
              (BigFppfOver.toScheme B (Spec (.of A)) hA).map g)

Sources

LeanAlgebraicGeometry.Space.exists_idealSheafData_isFlatOverAtPoint_iff_factors · AlgebraicGeometry.Space.exists_finitePresentation_idealSheafData_isFlatOverAtPoint_iff_factors

Section77.11 Universal flattening #

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

Tag 0CWR, a definition

Tag 0CWR in the Stacks Project.

AlgebraicGeometry.Space.FlatnessSituation.HasUniversalFlattening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlattening.lean, line 147. The attribute's comment: “the universal flattening of a module”.

Stacks 0CWR. The universal flattening of F exists when the flatness condition of Stacks 0CWX is stable under base change and the functor F_flat it cuts out of Y is an algebraic space.

def HasUniversalFlattening (D : FlatnessSituation.{u} B S hS) : Prop

AlgebraicGeometry.Space.HasUniversalFlattening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlattening.lean, line 166. The attribute's comment: “the universal flattening of the space”.

Stacks 0CWR. The universal flattening of an algebraic space X over Y exists when the universal flattening of its structure sheaf 𝒪_X does.

def HasUniversalFlattening {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) : Prop

Tag 0CWS, a lemma

Tag 0CWS in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverInDimensionsGEOnSomeChartDiagram_iff_hasTrdegLt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleInDimensionsGE.lean, line 330. The attribute's comment: “the equivalence of conditions (1) and (3)”.

Stacks 0CWS, conditions (1) and (3). Flatness in dimensions ≥ n on some commuting square of surjective étale scheme charts is the bound trdeg < n at every point at which F is not flat over Y.

theorem isFlatOverInDimensionsGEOnSomeChartDiagram_iff_hasTrdegLt (n : ℕ) :
    IsFlatOverInDimensionsGEOnSomeChartDiagram B S hS Xs.2 f.hom F n ↔
      HasTrdegLtAtNonflatPoints B S hS Xs.2 f.hom F n

AlgebraicGeometry.Space.isFlatOverInDimensionsGEOnEveryChartDiagram_iff_hasTrdegLt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleInDimensionsGE.lean, line 344. The attribute's comment: “the equivalence of conditions (2) and (3)”.

Stacks 0CWS, conditions (2) and (3). Flatness in dimensions ≥ n on every commuting square of étale scheme charts is the bound trdeg < n at every point at which F is not flat over Y.

theorem isFlatOverInDimensionsGEOnEveryChartDiagram_iff_hasTrdegLt (n : ℕ) :
    IsFlatOverInDimensionsGEOnEveryChartDiagram B S hS Xs.2 f.hom F n ↔
      HasTrdegLtAtNonflatPoints B S hS Xs.2 f.hom F n

AlgebraicGeometry.Space.isFlatOverInDimensionsGEOnSomeChartDiagram_iff_onEveryChartDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleInDimensionsGE.lean, line 357. The attribute's comment: “the equivalence of conditions (1) and (2)”.

Stacks 0CWS, conditions (1) and (2). Flatness in dimensions ≥ n can be tested on one commuting square of surjective étale scheme charts, and then holds on every commuting square of étale scheme charts.

theorem isFlatOverInDimensionsGEOnSomeChartDiagram_iff_onEveryChartDiagram (n : ℕ) :
    IsFlatOverInDimensionsGEOnSomeChartDiagram B S hS Xs.2 f.hom F n ↔
      IsFlatOverInDimensionsGEOnEveryChartDiagram B S hS Xs.2 f.hom F n

AlgebraicGeometry.Space.isFlatOverInDimensionsGE_modulePullback_of_hasTrdegLt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleInDimensionsGE.lean, line 548. The attribute's comment: “the base-change clause: if the transcendence degree over its image of every point at which the module is not flat over the target is < n -- condition (3) of the tag, written out -- then the inverse image of the module is flat over the new target in dimensions >= n”.

Stacks 0CWS, the base-change clause. Let f : X ⟶ Y be locally of finite type, let F be quasi-coherent of finite type, and let the square be cartesian over a morphism Y' ⟶ Y. If the transcendence degree over its image of every point of |X| at which F is not flat over Y is less than n, then the inverse image (g')^*F of F on X' = X ×_Y Y' is flat over Y' in dimensions ≥ n.

The hypothesis is condition (3) of Stacks 0CWS written out: the flat locus is AlgebraicGeometry.Space.flatLocus of Stacks 0DLR and the transcendence degree is AlgebraicGeometry.Space.HasTranscendenceDegreeAt of Stacks 04NM, and by AlgebraicGeometry.Space.isFlatOverInDimensionsGE_iff_hasTrdegLt it is exactly flatness over Y in dimensions ≥ n in the sense of Stacks 0CWT, which is what AlgebraicGeometry.Space.isFlatOverInDimensionsGE_modulePullback_of_isPullback below states it as. Writing it out is what keeps the registered form of the clause free of the abbreviations introduced in this file, so that no hypothesis of it is read as standing in for an input.

The clause is that condition on the two sides together with AlgebraicGeometry.Space.hasTrdegLtAtNonflatPoints_modulePullback_of_isPullback, which is where Stacks 05VW at a point enters.

The hypotheses on F are the source's, read on the small étale site: quasi-coherence and finite type there, which the inverse image inherits by Stacks 03GA and by Stacks 03DO for the clause 03DL (5), AlgebraicGeometry.Space.isFiniteTypeOnSite_modulePullback. The chartwise forms of the two, which the equivalence of Stacks 0CWS consumes, follow for both modules by AlgebraicGeometry.Space.isQuasicoherentOnCharts_of_isQuasicoherentOnSite and AlgebraicGeometry.Space.isFiniteTypeOnCharts_of_isFiniteTypeOnSite, so neither is assumed of the inverse image.

theorem isFlatOverInDimensionsGE_modulePullback_of_hasTrdegLt
    (hftS : SheafOfModules.IsFiniteTypeOnSite F) {g' : X' ⟶ Xs} {f' : X' ⟶ Y'}
    {g : Y' ⟶ Ys} (sq : IsPullback g'.hom f'.hom f.hom g.hom) (n : ℕ)
    (h : ∀ x : points B S hS Xs.1, x ∉ flatLocus B S hS Xs.2 f.hom F →
      ∃ r : ℕ∞, HasTranscendenceDegreeAt B S hS f.hom x r ∧ r < (n : ℕ∞)) :
    IsFlatOverInDimensionsGE B S hS f' ((modulePullback B S hS g').obj F) n

Tag 0CWT, a definition

Tag 0CWT in the Stacks Project.

AlgebraicGeometry.Space.IsFlatOverInDimensionsGE, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleInDimensionsGE.lean, line 370. The attribute's comment: “the definition, taken in the form of condition (2) of Stacks 0CWS; conditions (1) and (3) are interchangeable with it by isFlatOverInDimensionsGEOnSomeChartDiagram_iff_onEveryChartDiagram and isFlatOverInDimensionsGEOnEveryChartDiagram_iff_hasTrdegLt”.

Stacks 0CWT. F is flat over Y in dimensions ≥ n. The source defines this by the equivalent conditions of Stacks 0CWS; condition (2) is taken as the definition, and the three conditions are interchangeable by the theorems above.

abbrev IsFlatOverInDimensionsGE (n : ℕ) : Prop

Tag 0CWU, a situation

Tag 0CWU in the Stacks Project.

AlgebraicGeometry.Space.FlatDimensionSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctor.lean, line 144. The attribute's comment: “standing data”.

Situation 0CWU. The standing data of Situation 0CWU: the flatness situation of Stacks 0CWX — a morphism f : X ⟶ Y of algebraic spaces over S and a quasi-coherent 𝒪_X-module F — in which moreover f is locally of finite type and F is of finite type.

structure FlatDimensionSituation extends FlatnessSituation.{u} B S hS

AlgebraicGeometry.Space.FlatDimensionSituation.isLocallyOfFiniteType_baseChangeInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctor.lean, line 165. The attribute's comment: “the base-changed morphism is locally of finite type; corrected from the source's "of finite type", which does not follow from its hypothesis that f is only locally of finite type”.

Situation 0CWU, the first observation. The base change f_T : X_T ⟶ T of a locally finite type morphism to a test scheme is again locally of finite type. This is Stacks 03XH, stability of the property under base change, at the fibre product square defining X_T.

The source says f_T is of finite type, which does not follow from its own hypotheses: f is assumed only locally of finite type, and base change preserves exactly that. The half of Stacks 03XH the source cites is the locally-of-finite-type one, and it is also what Definition 0CWT consumes, so the corrected statement is the one that is used.

theorem isLocallyOfFiniteType_baseChangeInclusion (D : FlatDimensionSituation.{u} B S hS)
    (T : SchemesOver D.Y) :
    IsLocallyOfFiniteType B S hS (baseChangeInclusion D.f T).hom

AlgebraicGeometry.Space.FlatDimensionSituation.isFiniteTypeOnSite_baseChangeModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctor.lean, line 178. The attribute's comment: “the base-changed module is of finite type”.

Situation 0CWU, the second observation. The base change F_T of a finite type module to a test scheme is again of finite type. This is Stacks 03DO for the inverse image of Stacks 03LU along the projection X_T ⟶ X.

theorem isFiniteTypeOnSite_baseChangeModule (D : FlatDimensionSituation.{u} B S hS)
    (T : SchemesOver D.Y) :
    SheafOfModules.IsFiniteTypeOnSite (D.toFlatnessSituation.baseChangeModule T)

AlgebraicGeometry.Space.FlatDimensionSituation.flatDimensionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctor.lean, line 236. The attribute's comment: “the functor F_n of equation 0CWV”.

Equation 0CWV, the functor F_n of Situation 0CWU: the functor on the test schemes over Y whose value at T is a one-point set when F_T is flat over T in dimensions ≥ n, and is empty otherwise.

That the condition is inherited along a morphism of test schemes, which is what makes the assignment a functor, is AlgebraicGeometry.Space.FlatDimensionSituation.isFlatInDimensionsGEAfterBaseChange_of_hom.

def flatDimensionFunctor (D : FlatDimensionSituation.{u} B S hS) (n : ℕ) :
    (SchemesOver D.Y)ᵒᵖ ⥤ Type u

Tag 0CWW, a lemma

Tag 0CWW in the Stacks Project.

AlgebraicGeometry.Space.FlatDimensionSituation.flatDimensionFunctor_isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctorDescent.lean, line 385. The attribute's comment: “clause (1): in Situation 0CWU the functor F_n of equation 0CWV is a sheaf for the fpqc topology on the test schemes over Y. Proved for every situation of the tag, from nothing but the data of Situation 0CWU: the functor is subterminal, so its sheaf property is fpqc locality of the condition of Stacks 0CWT on the base change, and that locality is the pointwise descent of condition (3) of Stacks 0CWS along the jointly surjective flat family a covering sieve contains”.

Stacks 0CWW, clause (1). In Situation 0CWU the functor F_n of equation 0CWV satisfies the sheaf property for the fpqc topology on the test schemes over Y.

F_n is subterminal, so its sheaf property is exactly fpqc locality of the condition of Stacks 0CWT on the base change, which is isFlatInDimensionsGEAfterBaseChange_of_mem_fpqcTopology of this namespace.

theorem flatDimensionFunctor_isSheaf_fpqc (D : FlatDimensionSituation.{u} B S hS) (n : ℕ) :
    Presheaf.IsSheaf (fpqcTopology D.Y) (D.flatDimensionFunctor n)

AlgebraicGeometry.Space.FlatDimensionSituation.flatDimensionFunctor_limitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctorDescent.lean, line 526. The attribute's comment: “clause (2), limit preservation of F_n”.

Stacks 0CWW, clause (2). In Situation 0CWU, if f is quasi-compact and locally of finite presentation and ℱ is of finite presentation, then the functor F_n of equation 0CWV is limit preserving.

The proof is the source's, with the chart presentation constructed rather than assumed. Since F_n is subterminal, limit preservation is descent of the condition of Stacks 0CWT along a cofiltered inverse system of affine test schemes with affine limit (limitPreserving_flatDimensionFunctor_iff), so a system T = lim T_i of affine test schemes may be fixed first. The presentation is then taken at one of its stages: for an index i₀, the base change X_{T_{i₀}} is quasi-compact over the affine scheme underlying T_{i₀}, hence has a surjective étale scheme chart U with affine scheme (AlgebraicGeometry.Space.exists_isAffine_isSurjective_chart_baseChangeSpace, Stacks 03H6), and U ⟶ T_{i₀} together with the restriction of F_{T_{i₀}} to U is a scheme-level situation E of Stacks 05MT (AlgebraicGeometry.Space.FlatDimensionSituation.stageSituation). That is the chart presentation of the source read over a stage instead of over Y: because T_{i₀} is represented, the target chart of the presenting square is the identity chart, so no base change of a chart of Y and no affine open of one is needed, and the value of the presentation at a test scheme T' over T_{i₀} is T' itself.

The identification of the two conditions at every test scheme over T_{i₀} is the theorem isFlatInDimensionsGEAfterBaseChange_iff_stageSituation of that same namespace, the chart clause of Stacks 0CWS at the square whose source chart is the base change of U and whose target chart is the identity chart. The system K of affine schemes over the scheme underlying T_{i₀} is the given system restricted to the indices over i₀, CategoryTheory.Over.post of T ↦ T on CategoryTheory.Over i₀; its limit is the given one because CategoryTheory.Over.forget i₀ is initial for a cofiltered index category. Limit preservation of the scheme-level F'_n is part (2) of Stacks 05MV, AlgebraicGeometry.FlatDimensionSituation.flatDimensionFunctor_limitPreserving, applied to E and to K; the three hypotheses it asks of E are the hypotheses on f and ℱ read on the presentation, and are where they enter.

The schemes live in the maximum of the two index universes of the tested inverse system and a third parameter. That is the universe signature every limit-preservation statement in this library carries: Stacks 05MY and part (2) of Stacks 05MV both have it, and it is the signature at which the limit of a cofiltered system of affine schemes indexed by a category of those universes exists in the first place. It is also the signature of the statement of Stacks 0CWW (limit preserving).

theorem flatDimensionFunctor_limitPreserving
    (D : FlatDimensionSituation.{max u w w'} B₁ S₁ hS₁) (n : ℕ)
    (hqc : IsQuasiCompact B₁ S₁ hS₁ D.f.hom)
    (hlfp : IsLocallyOfFinitePresentation B₁ S₁ hS₁ D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F) :
    LimitPreserving.{max u w w', max u w w', w, w'}
      (testSchemeFunctor D.Y) (D.flatDimensionFunctor n)

Tag 0CX0, a lemma

Tag 0CX0 in the Stacks Project.

AlgebraicGeometry.Space.FlatDimensionSituation.mono_etalePullbackComparison_and_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctorEtale.lean, line 411. The attribute's comment: “the full statement at the source's hypotheses, nothing granted or assumed: Situation 0CWU (f locally of finite type, F quasi-coherent of finite type) and h etale only. 'F_n is a subfunctor of F'_n' is that the canonical natural transformation F_n -> F'_n between these subterminal functors is a monomorphism, and 'F_n = F'_n' is that it is an isomorphism. Ass_{X/Y}(F) is the relative weak assassin of Stacks 0CV0, which the source writes Ass_{X/Y}(F) as the fibres of f are locally Noetherian, and h(X') is the image of |X'| -> |X|”.

Stacks 0CX0. In Situation 0CWU, let h : X' ⟶ X be an étale morphism, set F' = h^* F and f' = f ∘ h, and let F'_n be the functor of equation 0CWV for (f' : X' ⟶ Y, F'). Then F_n is a subfunctor of F'_n — the canonical natural transformation F_n ⟶ F'_n is a monomorphism — and if h(|X'|) ⊇ Ass_{X/Y}(F) then F_n = F'_n — that monomorphism is an isomorphism.

theorem mono_etalePullbackComparison_and_isIso (n : ℕ) :
    Mono (D.etalePullbackComparison h hh n) ∧
      (relativeWeaklyAssociatedPoints B S hS D.f D.F ⊆
          Set.range (pointsMap B S hS X'.1 h.hom) →
        IsIso (D.etalePullbackComparison h hh n))

Tag 0CX1, a theorem

Tag 0CX1 in the Stacks Project.

AlgebraicGeometry.Space.FlatDimensionSituation.isAlgebraicSpace_flatDimensionSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatDimensionFunctorRepresentable.lean, line 277. The attribute's comment: “the full statement under exactly the source's hypotheses, nothing granted or assumed: F_n is the subfunctor of Y of the maps T ⟶ Y along which F_T is flat in dimensions ≥ n (equation 0CWV); purity relative to Y is purity above every point of Y (Stacks 0CVD (5)); finite presentation of f is local finite presentation, quasi-compactness and quasi-separatedness (Stacks 03XP (3))”.

Stacks Project, Tag 0CX1. In Situation 0CWU, assume moreover that f is of finite presentation, that F is an 𝒪_X-module of finite presentation, and that F is pure relative to Y. Then F_n is an algebraic space and F_n ⟶ Y is a monomorphism of finite presentation.

F_n is AlgebraicGeometry.Space.FlatDimensionSituation.flatDimensionSubfunctor, the functor of equation 0CWV read on the big fppf site of S as a subfunctor of Y. Purity of F relative to Y is purity above every point of Y, Stacks 0CVD part (5), for the situation of Stacks 0CV6 which f and F determine; that situation is formed from the hypotheses of the theorem, since a morphism of finite presentation is of finite type and decent.

theorem isAlgebraicSpace_flatDimensionSubfunctor (n : ℕ)
    (hf : IsFinitePresentation B S hS D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F)
    (hpure : ∀ y, IsPureAbove (D.fpPrePureSituation hf y)) :
    IsAlgebraicSpace B S hS (D.flatDimensionSubfunctor n).toFunctor ∧
      Mono (D.flatDimensionSubfunctor n).ι ∧
      IsFinitePresentation B S hS (D.flatDimensionSubfunctor n).ι

Tag 0CX2, a lemma

Tag 0CX2 in the Stacks Project.

AlgebraicGeometry.Space.FlatnessSituation.hasUniversalFlattening_of_isPureAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlatteningExistence.lean, line 115. The attribute's comment: “part (1)”.

Stacks 0CX2, part (1). Let f : X ⟶ Y be a morphism of algebraic spaces of finite presentation and let F be a quasi-coherent 𝒪_X-module of finite presentation which is pure relative to Y, that is, pure above every point y ∈ |Y|. Then the universal flattening Y' ⟶ Y of F exists, and Y' ⟶ Y is a monomorphism of finite presentation.

Here Y' is the subfunctor F_flat of Y and Y' ⟶ Y is its inclusion. This is Theorem 0CX1 at n = 0, where F_0 = F_flat.

theorem hasUniversalFlattening_of_isPureAbove (D : FlatnessSituation.{u} B S hS)
    (hf : IsFinitePresentation B S hS D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F)
    (hpure : ∀ y : points B S hS D.Y.1,
      IsPureAbove ((D.toFlatDimensionSituation hf hF).fpPrePureSituation hf y)) :
    D.HasUniversalFlattening ∧ Mono (D.flatSubfunctor D.isFlatStableUnderBaseChange).ι ∧
      IsFinitePresentation B S hS (D.flatSubfunctor D.isFlatStableUnderBaseChange).ι

AlgebraicGeometry.Space.FlatnessSituation.hasUniversalFlattening_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlatteningExistence.lean, line 135. The attribute's comment: “part (3)”.

Stacks 0CX2, part (3). Let f : X ⟶ Y be a proper morphism of algebraic spaces of finite presentation and let F be a quasi-coherent 𝒪_X-module of finite presentation. Then the universal flattening Y' ⟶ Y of F exists, and Y' ⟶ Y is a monomorphism of finite presentation.

Over a proper morphism F is universally pure above every point of Y, by Stacks 0CVI, part (2). So it is pure relative to Y, and part (1) applies.

theorem hasUniversalFlattening_of_isProper (D : FlatnessSituation.{u} B S hS)
    (hproper : IsProper B S hS D.f.hom) (hf : IsFinitePresentation B S hS D.f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite D.F) :
    D.HasUniversalFlattening ∧ Mono (D.flatSubfunctor D.isFlatStableUnderBaseChange).ι ∧
      IsFinitePresentation B S hS (D.flatSubfunctor D.isFlatStableUnderBaseChange).ι

AlgebraicGeometry.Space.hasUniversalFlattening_of_isPureAbove_structure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlatteningExistence.lean, line 158. The attribute's comment: “part (2)”.

Stacks 0CX2, part (2). Let f : X ⟶ Y be a morphism of algebraic spaces of finite presentation such that X is pure relative to Y, that is, 𝒪_X is pure above every point y ∈ |Y|. Then the universal flattening Y' ⟶ Y of X exists, and Y' ⟶ Y is a monomorphism of finite presentation.

This is part (1) for the module 𝒪_X, which is of finite presentation.

theorem hasUniversalFlattening_of_isPureAbove_structure {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsFinitePresentation B S hS f.hom)
    (hpure : ∀ y : points B S hS Y.1, IsPureAbove (structurePrePureSituation X.2 Y.2 f.hom
      (isFiniteType_of_isFinitePresentation B S hS hf)
      (isDecent_of_isFinitePresentation B S hS f hf) y)) :
    HasUniversalFlattening f ∧
      Mono ((structureSheafFlatnessSituation f).flatSubfunctor
        (structureSheafFlatnessSituation f).isFlatStableUnderBaseChange).ι ∧
      IsFinitePresentation B S hS ((structureSheafFlatnessSituation f).flatSubfunctor
        (structureSheafFlatnessSituation f).isFlatStableUnderBaseChange).ι

AlgebraicGeometry.Space.hasUniversalFlattening_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFlatteningExistence.lean, line 176. The attribute's comment: “part (4)”.

Stacks 0CX2, part (4). Let f : X ⟶ Y be a proper morphism of algebraic spaces of finite presentation. Then the universal flattening of X exists.

This is part (3) for the module 𝒪_X, which is of finite presentation.

theorem hasUniversalFlattening_of_isProper {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hproper : IsProper B S hS f.hom) (hf : IsFinitePresentation B S hS f.hom) :
    HasUniversalFlattening f

Sources

Section77.12 Grothendieck's Existence Theorem #

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

Tag 0CX4, a situation

Tag 0CX4 in the Stacks Project.

AlgebraicGeometry.Space.InverseSystemExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Existence.lean, line 120.

Stacks 0CX4. The standing data of Grothendieck's existence theorem for algebraic spaces: an inverse system of rings with surjective, locally nilpotent transitions, a separated algebraic space of finite presentation over the inverse-limit ring, and a compatible system of finitely presented quasi-coherent modules on its infinitesimal base changes which are flat over, and have support proper over, the affine base at their level.

structure InverseSystemExistenceSituation

AlgebraicGeometry.Space.FlatSheafExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/FlatSheafSystem.lean, line 86. The attribute's comment: “the situation as stated: nothing is granted or assumed beyond the source's data and hypotheses; the two containment fields only say that Spec A and Spec Aₙ are schemes of the chosen big fppf site”.

Situation [Stacks, Tag 0CX4]. An inverse system of rings (Aₙ) with surjective transition maps whose kernels are locally nilpotent; an algebraic space X separated and of finite presentation over A = lim Aₙ; and a system (Fₙ, φₙ) of finitely presented 𝒪_{Xₙ}-modules on the infinitesimal base changes Xₙ = X ×_{Spec A} Spec Aₙ, each flat over Aₙ with support proper over Aₙ, together with isomorphisms φₙ from the restriction of Fₙ₊₁ to Xₙ to Fₙ.

structure FlatSheafExistenceSituation

Tag 0CX5, a lemma

Tag 0CX5 in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.derivedLimit_bounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/FlatSheafDerivedLimit.lean, line 59. The attribute's comment: “the full statement: DQ_X exists and R lim F_n exists in D(O_X); for every coherator DQ_X and every such derived limit L, K = DQ_X(L) is a derived limit of (F_n) in D_QCoh(O_X), and every derived limit K of (F_n) in D_QCoh(O_X) lies in D^b with cohomology sheaves only in degrees at least 0; nothing is granted or assumed”.

[Stacks, Tag 0CX5]. In Situation [Stacks, Tag 0CX4] consider K = R lim_{D_QCoh(𝒪_X)}(Fₙ) = DQ_X(R lim_{D(𝒪_X)} Fₙ). Then K is in D^b_QCoh(𝒪_X) and in fact K has nonzero cohomology sheaves only in degrees ≥ 0.

Formally: the coherator DQ_X, the right adjoint of D_QCoh(𝒪_X) ⥤ D(𝒪_X), exists; the system (Fₙ) (that is, (iₙ,* Fₙ) placed in degree 0) has a derived limit L = R lim_{D(𝒪_X)} Fₙ; and for every coherator DQ_X and every such L, K = DQ_X(L) is a derived limit of (Fₙ) in D_QCoh(𝒪_X), its cohomology sheaves vanish in negative degrees, and they vanish above some degree; and every derived limit K of (Fₙ) in D_QCoh(𝒪_X) has the same two properties.

theorem derivedLimit_bounded :
    (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.IsLeftAdjoint ∧
    (∃ L, IsDerivedLimit D.derivedSystem L) ∧
    (∀ (DQ : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left ⥤
        (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).FullSubcategory)
      (_ : (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι ⊣ DQ)
      (L : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left),
      IsDerivedLimit D.derivedSystem L →
        (∃ _ : HasProduct fun n : ℕ => D.quasicoherentSystem.obj ⟨n⟩,
          IsDerivedLimit D.quasicoherentSystem (DQ.obj L)) ∧
        SpaceCohomologyVanishesBelow D.X.left 0
          ((spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.obj (DQ.obj L)) ∧
        ∃ c : ℤ, SpaceCohomologyVanishesAbove D.B D.S D.containsLimitBase D.X.left c
          ((spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.obj (DQ.obj L))) ∧
    ∀ (_ : HasProduct fun n : ℕ => D.quasicoherentSystem.obj ⟨n⟩)
      (K : (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).FullSubcategory),
      IsDerivedLimit D.quasicoherentSystem K →
        SpaceCohomologyVanishesBelow D.X.left 0
          ((spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.obj K) ∧
        ∃ c : ℤ, SpaceCohomologyVanishesAbove D.B D.S D.containsLimitBase D.X.left c
          ((spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.obj K)

Tag 0CX6, a lemma

Tag 0CX6 in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.perfectSections_of_derivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/PerfectSectionsOfLimitCarrier.lean, line 76. The attribute's comment: “both parts in full, for every perfect E on X and every n, with K = DQ_X(L) for every coherator DQ_X and every L presented as R lim (i_n,* F_n) by the IsDerivedLimit triangle hp (as in derivedLimit_bounded, 0CX5): (1) RΓ(X, E ⊗^L K) is perfect in D(A) and the canonical map RΓ(X, E ⊗^L K) ⊗^L_A A_n → RΓ(X_n, E|_{X_n} ⊗^L F_n) is an isomorphism; (2) RHom_X(E, K) is perfect in D(A) and the canonical map RHom_X(E, K) ⊗^L_A A_n → RHom_{X_n}(E|_{X_n}, F_n), the map induced from (1) at E^∨ by 08JJ / 21.48.4, is an isomorphism; nothing is granted or assumed”.

[Stacks, Tag 0CX6]. In Situation [Stacks, Tag 0CX4] let K = DQ_X(L) be as in [Stacks, Tag 0CX5] (AlgebraicGeometry.Space.FlatSheafExistenceSituation.derivedLimit_bounded): DQ_X is a coherator (adj : ι ⊣ DQ_X) and p : L ⟶ ∏ (iₙ,* Fₙ)[0] is the first map of a distinguished triangle L ⟶ ∏ Fₙ ⟶ ∏ Fₙ ⟶ L[1] whose middle map is 1 - transition (hp is exactly the triangle of CategoryTheory.Pretriangulated.IsDerivedLimit with p bound), so L = R lim Fₙ. Then for every perfect E on X and every n:

RΓ(X, E ⊗^𝐋 K) is a perfect object of D(A) and the canonical map RΓ(X, E ⊗^𝐋 K) ⊗^𝐋_A Aₙ ⟶ RΓ(Xₙ, E|_{Xₙ} ⊗^𝐋 Fₙ) is an isomorphism in D(Aₙ);

RHom_X(E, K) is a perfect object of D(A) and the canonical map RHom_X(E, K) ⊗^𝐋_A Aₙ ⟶ RHom_{Xₙ}(E|_{Xₙ}, Fₙ) is an isomorphism in D(Aₙ); this map is the one induced from (1) at E^∨ by Cohomology on Sites, Lemma 21.48.4 (Stacks 08JJ).

Here E|_{Xₙ} is the derived pullback of E along iₙ : Xₙ ⟶ X.

theorem perfectSections_of_derivedLimit
    (p : L ⟶ ∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩)
    (hp : ∃ δ : (∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ => Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) (n + 1) ≫
          D.derivedSystem.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left))
    (E : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left)
    (hE : spaceIsPerfect D.B D.S D.containsLimitBase D.X.left E) (n : ℕ) :
    (StacksDraft.ringIsPerfect (D.limitTensorSections DQ L E) ∧
      IsIso (D.limitTensorSectionsBaseChangeMap adj L E p n)) ∧
    (StacksDraft.ringIsPerfect (D.limitSheafHomSections DQ L E) ∧
      IsIso (D.limitSheafHomSectionsBaseChangeMap adj L E hE p n))

Tag 0CX7, a lemma

Tag 0CX7 in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.isRelativelyPseudoCoherent_coheratorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/RelativePseudoCoherenceOfLimit.lean, line 42. The attribute's comment: “the full statement: for every coherator DQ_X and every derived limit L of (F_n) in D(O_X), the K = DQ_X(L) of 0CX5 is pseudo-coherent relative to A; nothing is granted or assumed”.

[Stacks, Tag 0CX7]. In Situation [Stacks, Tag 0CX4] let K = DQ_X(L) be as in [Stacks, Tag 0CX5]: DQ_X is a coherator (adj : ι ⊣ DQ_X, the right adjoint of the inclusion D_QCoh(𝒪_X) ⟶ D(𝒪_X)) and L is a derived limit R lim_{D(𝒪_X)} Fₙ of the system (iₙ,* Fₙ). Then K is pseudo-coherent relative to A.

theorem isRelativelyPseudoCoherent_coheratorObj
    {DQ : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left ⥤
      (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).FullSubcategory}
    (adj : (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι ⊣ DQ)
    (L : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left)
    (hL : IsDerivedLimit D.derivedSystem L) :
    IsRelativelyPseudoCoherent D.B D.S D.containsLimitBase D.X.left.1 D.X.left.2 D.X.hom.hom
      D.isLocallyOfFiniteType_structureMorphism (D.coheratorObj DQ L)

Tag 0CX8, a lemma

Tag 0CX8 in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.isIso_etaleStageBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/EtaleStageBaseChange.lean, line 60. The attribute's comment: “the full statement: for every coherator DQ_X and every presentation of L = R lim F_n in D(O_X), every n and every etale U → X with U quasi-compact and quasi-separated, the canonical map RΓ(U, K) ⊗^L_A A_n → RΓ(U_n, F_n) in D(A_n) induced by K = DQ_X(L) → F_n is an isomorphism, U_n = U ×_X X_n; nothing is granted or assumed”.

[Stacks, Tag 0CX8]. In Situation [Stacks, Tag 0CX4] let K = DQ_X(L) be as in [Stacks, Tag 0CX5]: DQ_X is a coherator (adj : ι ⊣ DQ_X) and L ⟶ ∏ Fₙ ⟶ ∏ Fₙ ⟶ L[1] (first map p) presents L as R lim_{D(𝒪_X)} Fₙ, with canonical maps φₙ : K ⟶ Fₙ the counit followed by the projections. For every n and every étale morphism j : U ⟶ X with U quasi-compact and quasi-separated, the canonical map RΓ(U, K) ⊗^𝐋_A Aₙ ⟶ RΓ(Uₙ, Fₙ) of D(Aₙ) induced by φₙ, Uₙ = U ×_X Xₙ, is an isomorphism.

theorem isIso_etaleStageBaseChangeMap
    {DQ : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left ⥤
      (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).FullSubcategory}
    (adj : (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι ⊣ DQ)
    {L : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left}
    (p : L ⟶ ∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩)
    (hp : ∃ δ : (∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ => Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) (n + 1) ≫
          D.derivedSystem.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left))
    (n : ℕ) {U : AlgebraicSpaces D.B D.S D.containsLimitBase} (j : U ⟶ D.X.left)
    (hj : IsEtale D.B D.S D.containsLimitBase j.hom)
    (hUqc : IsQuasiCompactSpace D.B D.S D.containsLimitBase U.1)
    (hUqs : IsAbsolutelyQuasiSeparated D.B D.S D.containsLimitBase D.B.contains_terminal U.1) :
    IsIso (D.etaleStageBaseChangeMap n j
      (D.isQuasiCompact_isQuasiSeparated_of_isEtale j hj hUqc hUqs).1
      (D.isQuasiCompact_isQuasiSeparated_of_isEtale j hj hUqc hUqs).2 adj p)

Tag 0CX9, a lemma

Tag 0CX9 in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_isExistenceNeighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/ExistenceNeighbourhoodExists.lean, line 56. The attribute's comment: “the full statement: for every coherator DQ_X and every presentation of L = R lim F_n in D(O_X), K = DQ_X(L) has an open subspace W containing X_0 with H^i(K)|_W = 0 for i ≠ 0, H^0(K)|_W of finite presentation, and F_n = H^0(K)|_W ⊗ O_{X_n} through the canonical maps K → F_n; nothing is granted or assumed”.

In Situation [Stacks, Tag 0CX4] let K = DQ_X(L) be as in [Stacks, Tag 0CX5]: DQ_X is a coherator (adj : ι ⊣ DQ_X) and L ⟶ ∏ Fₙ ⟶ ∏ Fₙ ⟶ L[1] (first map p) presents L as R lim_{D(𝒪_X)} Fₙ, with canonical maps K ⟶ Fₙ the counit followed by the projections. Then there is an open subspace W ⊂ X containing the points X₀ lying over Spec(A₁) such that Hⁱ(K)|_W = 0 for i ≠ 0, H⁰(K)|_W is of finite presentation, and H⁰(K)|_W ⊗_{𝒪_X} 𝒪_{Xₙ} ⟶ Fₙ induced by K ⟶ Fₙ is an isomorphism on W ×_X Xₙ for every n.

theorem exists_isExistenceNeighbourhood
    {DQ : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left ⥤
      (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).FullSubcategory}
    (adj : (spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι ⊣ DQ)
    {L : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left}
    (p : L ⟶ ∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩)
    (hp : ∃ δ : (∏ᶜ fun n : ℕ => D.derivedSystem.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ => Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ => D.derivedSystem.obj ⟨n⟩) (n + 1) ≫
          D.derivedSystem.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left)) :
    ∃ (W : Subfunctor D.X.left.1) (hW : IsOpenSubspace D.B D.S D.containsLimitBase W),
      D.IsExistenceNeighbourhood
        ((spaceQuasicoherentProp D.B D.S D.containsLimitBase D.X.left).ι.obj (DQ.obj L))
        (D.derivedLimitProjection adj p) W hW

Tag 0CXA, a lemma

Tag 0CXA in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_isExistenceNeighbourhood_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/ExistenceNeighbourhoodProperSupport.lean, line 148. The attribute's comment: “the full statement: for every K with maps to the Fₙ (in particular the K of 0CX5 with its canonical maps) and every W with the three conclusions of 0CX9, a smaller open W', still with those conclusions, on which the support of H⁰(K)|_W' is proper over A; nothing is granted or assumed”.

Stacks 0CXA. In Situation 0CX4 let K be an object of D(𝒪_X) with maps πₙ : K ⟶ Fₙ, and let W ⊆ X be an open subspace with the conclusions of Stacks 0CX9 (D.IsExistenceNeighbourhood K π W hW). Then, after shrinking W to an open subspace W' which still has the conclusions of Stacks 0CX9, the support of F = H⁰(K)|_{W'} is proper over A.

This covers the source's statement as written: its K is that of Stacks 0CX5, K = DQ_X(R lim Fₙ), here (spaceQuasicoherentProp _ _ _ _).ι.obj (DQ.obj L) with the maps D.derivedLimitProjection adj p for a coherator adj : ι ⊣ DQ and a triangle p presenting L = R lim_{D(𝒪_X)} Fₙ, and its W is any open subspace with the conclusions of Stacks 0CX9 for that K, which is what D.IsExistenceNeighbourhood K π W hW says; the statement below is the special case of the one for every K and every such W.

The source's proof, at the first level: F restricted to X₁ is F₁ by part (3) of Stacks 0CX9, since W contains X₀ = |X₁|; so the support of F meets X₁ in the support of F₁, proper over A₁, and AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_isOpenSubspace_hasProperSupport (the henselian pair (A, Ker(A → A₁)) and Stacks 0CWI) shrinks W.

theorem exists_isExistenceNeighbourhood_hasProperSupport
    {K : spaceDerivedCategory D.B D.S D.containsLimitBase D.X.left}
    {π : ∀ n : ℕ, K ⟶ D.derivedSystem.obj (op n)} {W : Subfunctor D.X.left.1}
    {hW : IsOpenSubspace D.B D.S D.containsLimitBase W}
    (hN : D.IsExistenceNeighbourhood K π W hW) :
    ∃ (W' : Subfunctor D.X.left.1) (hW' : IsOpenSubspace D.B D.S D.containsLimitBase W')
      (_ : W' ≤ W), D.IsExistenceNeighbourhood K π W' hW' ∧
      ∃ hlft : IsLocallyOfFiniteType D.B D.S D.containsLimitBase (W'.ι ≫ D.X.hom.hom),
        HasProperSupport D.B D.S D.containsLimitBase hW'.1
          (schemeSpace (limitBaseObject D.system D.B D.containsLimitBase)).2
          (W'.ι ≫ D.X.hom.hom) hlft
          ((SheafOfModules.toSheaf _).obj
            ((modulePullback D.B D.S D.containsLimitBase
              (openSubspaceHom D.B D.S D.containsLimitBase W' hW')).obj
                ((spaceDerivedHomology D.B D.S D.containsLimitBase D.X.left 0).obj K)))

Tag 0CXB, a theorem

Tag 0CXB in the Stacks Project.

AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistence/FlatExistenceTheorem.lean, line 50.

Grothendieck's existence theorem, [Stacks, Tag 0CXB]. In Situation [Stacks, Tag 0CX4] there exists a finitely presented 𝒪_X-module F, flat over A, whose support is closed and proper over A, with identifications αₙ : F ⊗_{𝒪_X} 𝒪_{Xₙ} = iₙ^* F ≅ Fₙ for all n, compatible with the maps φₙ : Fₙ₊₁ ⊗ 𝒪_{Xₙ} ≅ Fₙ through tₙ^* iₙ₊₁^* = iₙ^*.

theorem exists_algebraization :
    ∃ F : Modules.{u, u} D.B D.S D.containsLimitBase D.X.left.1 D.X.left.2,
      F.IsFinitePresentationOnSite ∧
        IsFlatOver D.B D.S D.containsLimitBase D.X.left.2 D.X.hom.hom F ∧
        ∃ hcl : IsClosed (supportOfSheaf D.B D.S D.containsLimitBase D.X.left.1
            ((SheafOfModules.toSheaf _).obj F)),
          IsProperOver D.B D.S D.containsLimitBase D.X.left.2
            (schemeSpace (limitBaseObject D.system D.B D.containsLimitBase)).2 D.X.hom.hom
            (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation D.B D.S
              D.containsLimitBase D.finitePresentation.1)
            (supportOfSheaf D.B D.S D.containsLimitBase D.X.left.1
              ((SheafOfModules.toSheaf _).obj F)) hcl ∧
          ∃ α : ∀ n : ℕ, (modulePullback D.B D.S D.containsLimitBase
              (D.closedImmersion n)).obj F ≅ D.F n,
            ∀ n : ℕ,
              (modulePullback D.B D.S D.containsLimitBase (D.transition n)).map
                  (α (n + 1)).hom ≫ (D.φ n).hom =
                (modulePullbackCompIso D.B D.S D.containsLimitBase (D.transition n)
                    (D.closedImmersion (n + 1))).hom.app F ≫
                  eqToHom (congrArg (fun g => (modulePullback D.B D.S
                    D.containsLimitBase g).obj F) (D.transition_closedImmersion n)) ≫
                  (α n).hom

Sources

LeanAlgebraicGeometry.Space.InverseSystemExistenceSituation · AlgebraicGeometry.Space.FlatSheafExistenceSituation · AlgebraicGeometry.Space.FlatSheafExistenceSituation.derivedLimit_bounded · AlgebraicGeometry.Space.FlatSheafExistenceSituation.perfectSections_of_derivedLimit · AlgebraicGeometry.Space.FlatSheafExistenceSituation.isRelativelyPseudoCoherent_coheratorObj · AlgebraicGeometry.Space.FlatSheafExistenceSituation.isIso_etaleStageBaseChangeMap · AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_isExistenceNeighbourhood · AlgebraicGeometry.Space.FlatSheafExistenceSituation.exists_isExistenceNeighbourhood_hasProperSupport

Section77.13 Grothendieck's Existence Theorem, bis #

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

Tag 0DIK, a situation

Tag 0DIK in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistence.lean, line 478.

Stacks 0DIK. The standing data of Grothendieck's existence theorem for algebraic spaces in its derived form: an inverse system of rings with surjective, locally nilpotent transitions, a proper flat algebraic space of finite presentation over the inverse-limit ring, and a compatible system of pseudo-coherent objects on its infinitesimal base changes.

structure DerivedExistenceSituation

AlgebraicGeometry.Space.DerivedExistenceSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceSystem.lean, line 105. The attribute's comment: “the situation as stated, with the derived pullback along each Xₙ → Xₙ₊₁ constructed by Stacks 06YY rather than given; nothing is granted or assumed beyond the source's data and a big fppf site containing Spec A and every Spec Aₙ”.

The standing data of Grothendieck's existence theorem for algebraic spaces in its derived form: an inverse system of rings (Aₙ) with surjective transitions whose kernels are locally nilpotent, an algebraic space X proper, flat and of finite presentation over A = lim Aₙ, and pseudo-coherent objects Kₙ of D(𝒪_{Xₙ}) on the infinitesimal base changes Xₙ = X ×_{Spec A} Spec Aₙ, with maps Liₙ^* Kₙ₊₁ ⟶ Kₙ that are isomorphisms, Liₙ^* being the derived pullback along Xₙ ⟶ Xₙ₊₁ constructed in transitionDerivedPullback.

structure DerivedExistenceSystem

Tag 0DIL, a lemma

Tag 0DIL in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSystem.derivedLimit_isBoundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceBoundedLimit.lean, line 62. The attribute's comment: “K = R lim_{D_QCoh} K_n = DQ_X(R lim_{D(O_X)} K_n) lies in D^-_QCoh(O_X), for every choice of coherator and of derived limits”.

The inclusion D_QCoh(𝒪_X) ⥤ D(𝒪_X) has a right adjoint DQ_X and the tower (Rjₙ,* Kₙ) has a derived limit L = R lim_{D(𝒪_X)} Kₙ. For every coherator DQ_X and every such L, K = DQ_X(L) is a derived limit of the tower in D_QCoh(𝒪_X) whose cohomology sheaves vanish above some degree. Every derived limit of the tower in D_QCoh(𝒪_X) lies in D⁻_QCoh(𝒪_X).

theorem derivedLimit_isBoundedAbove :
    (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase D.X.left).ι.IsLeftAdjoint ∧
    (∃ L, IsDerivedLimit D.spaceTower L) ∧
    (∀ (DQ : spaceDerivedCategory D.B (limitBase D.system) D.containsLimitBase D.X.left ⥤
        (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase
          D.X.left).FullSubcategory)
      (_ : (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase D.X.left).ι ⊣ DQ)
      (L : spaceDerivedCategory D.B (limitBase D.system) D.containsLimitBase D.X.left),
      IsDerivedLimit D.spaceTower L →
        (∃ _ : HasProduct fun n : ℕ => D.quasicoherentTower.obj ⟨n⟩,
          IsDerivedLimit D.quasicoherentTower (DQ.obj L)) ∧
        ∃ c : ℤ, SpaceCohomologyVanishesAbove D.B (limitBase D.system) D.containsLimitBase
          D.X.left c ((spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase
            D.X.left).ι.obj (DQ.obj L))) ∧
    ∀ (_ : HasProduct fun n : ℕ => D.quasicoherentTower.obj ⟨n⟩)
      (K : (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase
        D.X.left).FullSubcategory),
      IsDerivedLimit D.quasicoherentTower K →
        ∃ c : ℤ, SpaceCohomologyVanishesAbove D.B (limitBase D.system) D.containsLimitBase
          D.X.left c ((spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase
            D.X.left).ι.obj K)

Tag 0DIM, a lemma

Tag 0DIM in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSystem.isPseudoCoherent_and_isIso_stageTensorSectionsBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceTensorSectionsBaseChange.lean, line 365. The attribute's comment: “the full statement: for every perfect E, M = RΓ(X, E ⊗^L K) is pseudo-coherent and the canonical map M ⊗^L_A Aₙ ⟶ RΓ(Xₙ, Lpₙ^E ⊗^L Kₙ) is an isomorphism in D(Aₙ) for every n. D is Situation 0DIK (DerivedExistenceSystem), whose fields are only the situation's data and hypotheses: the rings Aₙ with surjective transitions with locally nilpotent kernels, the fppf site containing Spec A and every Spec Aₙ, X proper, flat and of finite presentation over A, the pseudo-coherent Kₙ, and the comparison isomorphisms Liₙ^ Kₙ₊₁ ≅ Kₙ; no result is a field. K = DQ_X(R lim Kₙ) is the object of 0DIL, built from the coherator (the right adjoint of D_QCoh(𝒪_X) ⥤ D(𝒪_X)) and a derived limit, both constructed and not assumed”.

[Stacks, Tag 0DIM]. In Situation 0DIK let K = DQ_X(R lim Kₙ) be the object of [Stacks, Tag 0DIL] and E a perfect object of D(𝒪_X). Then M = RΓ(X, E ⊗^L K) is a pseudo-coherent object of D(A), and for every n the canonical map cₙ : M ⊗^L_A Aₙ ⟶ RΓ(Xₙ, Lpₙ^*E ⊗^L Kₙ) (the base change map of RΓ, then Stacks 07A4 and Lpₙ^*E ⊗^L τₙ, with τₙ : Lpₙ^*K ⟶ Kₙ adjoint to the projection) is an isomorphism in D(Aₙ). Here K is D.quasicoherentLimit, with R lim Kₙ = D.derivedLimit and DQ_X the right adjoint D.coherator of the inclusion D_QCoh(𝒪_X) ⥤ D(𝒪_X).

theorem isPseudoCoherent_and_isIso_stageTensorSectionsBaseChange
    (E : spaceDerivedCategory D.B (limitBase D.system) D.containsLimitBase D.X.left)
    (hE : spaceIsPerfect D.B (limitBase D.system) D.containsLimitBase D.X.left E) :
    StacksDraft.PseudoCoherence.IsPseudoCoherent
        ((D.limitTensorSections E).obj ((spaceQuasicoherentProp D.B (limitBase D.system)
          D.containsLimitBase D.X.left).ι.obj D.quasicoherentLimit)) ∧
      ∀ n : ℕ, IsIso (D.stageTensorSectionsBaseChange D.coherator D.coheratorAdjunction E n)

Tag 0DIN, a lemma

Tag 0DIN in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSystem.isPseudoCoherentOnLimit_coheratorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistencePseudoCoherent.lean, line 190. The attribute's comment: “K = R lim_{D_QCoh} K_n = DQ_X(R lim_{D(O_X)} K_n) is pseudo-coherent on X, for every choice of coherator and of derived limit; nothing is granted or assumed”.

In Situation 0DIK let K = R lim_{D_QCoh(𝒪_X)}(Kₙ) = DQ_X(L) be the object of [Stacks, Tag 0DIL], for a coherator adj : ι ⊣ DQ_X and a derived limit L = R lim_{D(𝒪_X)} Kₙ of the tower (Rjₙ,* Kₙ). Then K is pseudo-coherent on X.

theorem isPseudoCoherentOnLimit_coheratorObj
    (DQ : spaceDerivedCategory D.B (limitBase D.system) D.containsLimitBase D.X.left ⥤
      (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase
        D.X.left).FullSubcategory)
    (adj : (spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase D.X.left).ι ⊣ DQ)
    (L : spaceDerivedCategory D.B (limitBase D.system) D.containsLimitBase D.X.left)
    (hL : IsDerivedLimit D.spaceTower L) :
    D.IsPseudoCoherentOnLimit
      ((spaceQuasicoherentProp D.B (limitBase D.system) D.containsLimitBase D.X.left).ι.obj
        (DQ.obj L))

Tag 0DIP, a lemma

Tag 0DIP in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSystem.isIso_etaleSectionsBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceEtaleSectionsHocolim.lean, line 128. The attribute's comment: “for U → X étale with U qcqs, RΓ(U, K) ⊗^L_A A_n → RΓ(U_n, K_n) is an isomorphism in D(A_n), U_n = U ×_X X_n; nothing is granted or assumed”.

In Situation 0DIK let K = DQ_X(R lim Kₙ) be the object of [Stacks, Tag 0DIL] (AlgebraicGeometry.Space.DerivedExistenceSystem.quasicoherentLimit, for the coherator DQ_X right adjoint to D_QCoh(𝒪_X) ⥤ D(𝒪_X)). For every étale j : U ⟶ X with U quasi-compact and quasi-separated and every n, the canonical map RΓ(U, K) ⊗^L_A Aₙ ⟶ RΓ(Uₙ, Kₙ) in D(Aₙ), with Uₙ = U ×_X Xₙ (the base change map of RΓ along Spec Aₙ ⟶ Spec A, then RΓ(Uₙ, -) of τₙ|_{Uₙ}, with τₙ : Lpₙ^*K ⟶ Kₙ adjoint to the projection), is an isomorphism.

theorem isIso_etaleSectionsBaseChangeMap
    (hj : IsEtale D.B (limitBase D.system) D.containsLimitBase j.hom)
    (hUqc : IsQuasiCompactSpace D.B (limitBase D.system) D.containsLimitBase U.1)
    (hUqs : IsAbsolutelyQuasiSeparated D.B (limitBase D.system) D.containsLimitBase
      D.B.contains_terminal U.1) (n : ℕ) :
    IsIso (D.etaleSectionsBaseChangeMap j D.coherator D.coheratorAdjunction n)

Tag 0DIQ, a theorem

Tag 0DIQ in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSystem.exists_isPseudoCoherent_stageDerivedPullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceGrothendieck.lean, line 236. The attribute's comment: “the full statement: K pseudo-coherent on X, K_n = Lj_n^* K for all n compatibly with the phi_n through the composition isomorphism of derived pullbacks; nothing is granted or assumed beyond Situation 0DIK”.

The derived Grothendieck existence theorem. In Situation 0DIK there is a pseudo-coherent K in D(𝒪_X) with Kₙ = K ⊗^L_{𝒪_X} 𝒪_{Xₙ} for all n, compatibly with the maps φₙ: isomorphisms ψₙ : Ljₙ^* K ≅ Kₙ (Ljₙ^* the derived pullback along jₙ : Xₙ ⟶ X) with ψₙ = (Ljₙ^* ≅ Liₙ^* Ljₙ₊₁^*) ≫ Liₙ^* ψₙ₊₁ ≫ φₙ, where Ljₙ^* ≅ Liₙ^* Ljₙ₊₁^* is the composition isomorphism of derived pullbacks along iₙ ≫ jₙ₊₁ = jₙ.

Proof as in the source: K = DQ_X(R lim Kₙ) is pseudo-coherent by [Stacks, Tag 0DIN] (from both halves of [Stacks, Tag 0DIM]), and the maps τₙ : Ljₙ^* K ⟶ Kₙ are isomorphisms by [Stacks, Tag 0DIP] over affine U étale over X, compatible with the φₙ.

theorem exists_isPseudoCoherent_stageDerivedPullback_iso :
    ∃ (K : D.limitDerivedCategory) (ψ : ∀ n : ℕ, (D.stageDerivedPullback n).obj K ≅ D.K n),
      D.IsPseudoCoherentOnLimit K ∧
        ∀ n : ℕ, (ψ n).hom = (D.stageDerivedPullbackCompIso n).inv.app K ≫
          (transitionDerivedPullback D.system D.B D.containsLimitBase D.containsBaseAt D.X n).map
            (ψ (n + 1)).hom ≫ D.φ n

Tag 0DIR, a remark

Tag 0DIR in the Stacks Project.

AlgebraicGeometry.Space.DerivedExistenceSituation.isSeparated_and_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceHypotheses.lean, line 90. The attribute's comment: “comparison of hypotheses on X only; the generalization is merely probable in the source, which gives no precise statement of it, and is not proved here”.

In a situation of Stacks 0DIK the structure morphism X → Spec A is separated, being proper, and is of finite presentation: the two conditions that the generalization proposed in Stacks 0DIR places on X hold.

theorem isSeparated_and_isFinitePresentation :
    IsSeparated D.B (limitBase D.system) D.containsLimitBase D.X.hom.hom ∧
      IsFinitePresentation D.B (limitBase D.system) D.containsLimitBase D.X.hom.hom

AlgebraicGeometry.Space.DerivedExistenceSituation.isProperOver_stageProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/DerivedExistenceHypotheses.lean, line 100. The attribute's comment: “comparison of hypotheses on Xₙ only; the generalization is merely probable in the source, which gives no precise statement of it, and is not proved here”.

In a situation of Stacks 0DIK every closed subset of the infinitesimal base change Xₙ is proper over Spec Aₙ, since Xₙ → Spec Aₙ is proper: the support condition that the generalization proposed in Stacks 0DIR places on Kₙ holds for every object of D(𝒪_{Xₙ}).

theorem isProperOver_stageProjection (n : ℕ)
    (T : Set (points D.B (limitBase D.system) D.containsLimitBase
      (spaceAt D.system D.B D.containsLimitBase D.containsBaseAt D.X n).1))
    (hT : _root_.IsClosed T) :
    IsProperOver D.B (limitBase D.system) D.containsLimitBase
      (spaceAt D.system D.B D.containsLimitBase D.containsBaseAt D.X n).2
      (schemeSpace
        (baseObjectAt D.system D.B D.containsLimitBase D.containsBaseAt n)).2
      (D.stageProjection n).hom (D.isLocallyOfFiniteType_stageProjection n) T hT

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

77 Flatness on Algebraic Spaces

Section77.2 Impurities#

Tag 0CV6, a situation

Tag 0CV7, an equation

Tag 0CV8, a definition

Tag 0CV9, a lemma

Tag 0CVA, a lemma

Tag 0CVB, a lemma

Sources

Section77.3 Relatively pure modules#

Tag 0CVD, a definition

Tag 0CVE, a lemma

Tag 0CVF, a lemma

Tag 0CVG, a lemma

Tag 0CVH, a lemma

Tag 0CVI, a lemma

Sources

Section77.4 Flat finite type modules#

Tag 0CWJ, a lemma

Tag 0CWK, a lemma

Tag 0CVK, a lemma

Tag 0CVL, a lemma

Tag 0DLR, a theorem

Tag 0CVW, a lemma

Tag 0CWL, a theorem

Tag 0CWM, a lemma

Sources

Section77.5 Flat finitely presented modules#

Tag 0CVY, a proposition

Tag 0CVZ, a lemma

Sources

Section77.6 A criterion for purity#

Tag 0CW1, a lemma

Tag 0CW2, a lemma

Tag 0CW3, a lemma

Tag 0CW4, a lemma

Tag 0CW5, a lemma

Tag 0CW6, a lemma

Sources

Section77.7 Flattening functors#

Tag 083F, a situation

Tag 083H, a lemma

Tag 083I, a lemma

Tag 083J, a lemma

Tag 0CVM, a lemma

Tag 0CW7, a lemma

Tag 0CW8, a lemma

Tag 0CWX, a situation

Tag 0CWZ, a lemma

Sources

Section77.8 Making a map zero#

Tag 0CWA, a situation

Tag 083K, a lemma

Tag 083L, a lemma

Tag 0CWB, a lemma

Tag 0CWC, a lemma

Tag 083M, a lemma

Sources

Section77.9 Flattening a map#

Tag 0CWD, a theorem

Tag 083N, a lemma

Tag 09TP, a lemma

Sources

Section77.10 Flattening in the local case#

Tag 0CWP, a lemma

Sources

Section77.11 Universal flattening#

Tag 0CWR, a definition

Tag 0CWS, a lemma

Tag 0CWT, a definition

Tag 0CWU, a situation

Tag 0CWW, a lemma

Tag 0CX0, a lemma

Tag 0CX1, a theorem

Tag 0CX2, a lemma

Sources

Section77.12 Grothendieck's Existence Theorem#

Tag 0CX4, a situation

Tag 0CX5, a lemma

Tag 0CX6, a lemma

Section77.2 Impurities #

Section77.3 Relatively pure modules #

Section77.4 Flat finite type modules #

Section77.5 Flat finitely presented modules #

Section77.6 A criterion for purity #

Section77.7 Flattening functors #

Section77.8 Making a map zero #

Section77.9 Flattening a map #

Section77.10 Flattening in the local case #

Section77.11 Universal flattening #

Section77.12 Grothendieck's Existence Theorem #

Section77.13 Grothendieck's Existence Theorem, bis #