76.19 Formally smooth morphisms to 76.32 Catenary algebraic spaces

Section76.19 Formally smooth morphisms#

Section 76.19 of the Stacks Project, Tag 049R. 14 tags here are carried by 22 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 060G, a definition

Tag 060G in the Stacks Project.

AlgebraicGeometry.Space.FormallySmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Defs.lean, line 68. The attribute's comment: “formal smoothness of a morphism of algebraic spaces”. References: SGA 3 XI (1.6), “formally smooth”.

Stacks 049S, part (1). Every commutative affine square against a square-zero closed immersion admits a lift.

public abbrev FormallySmooth {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) : Prop
Tag 061E, a lemma

Tag 061E in the Stacks Project.

Declarations registered for the tag:

Tag 061F, a lemma

Tag 061F in the Stacks Project.

Declarations registered for the tag:

Tag 061G, a lemma

Tag 061G in the Stacks Project.

Declarations registered for the tag:

Tag 061H, a lemma

Tag 061H in the Stacks Project.

AlgebraicGeometry.Space.formallySmooth_of_isEtale_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleSquare.lean, line 56.

Stacks 061H. Let ψ : U ⟶ V, u : U ⟶ X, v : V ⟶ Y and f : X ⟶ Y be morphisms of algebraic spaces over S forming a commuting square. If the two vertical arrows u and v are étale and f is formally smooth, then ψ is formally smooth.

theorem formallySmooth_of_isEtale_square
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {U V X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : IsAlgebraicSpace B S hS U) (hV : IsAlgebraicSpace B S hS V)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (ψ : U ⟶ V) (u : U ⟶ X) (v : V ⟶ Y) (f : X ⟶ Y)
    (hsq : u ≫ f = ψ ≫ v)
    (hu : IsEtale B S hS u) (hv : IsEtale B S hS v)
    (hf : FormallySmooth f) :
    FormallySmooth ψ
Tag 04AM, a lemma

Tag 04AM in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_iff_isLocallyOfFinitePresentation_and_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/OfIsSmooth.lean, line 417.

Stacks 04AM. A morphism of algebraic spaces over S is smooth exactly when it is locally of finite presentation and formally smooth.

theorem isSmooth_iff_isLocallyOfFinitePresentation_and_formallySmooth
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsSmooth B S hS f ↔ IsLocallyOfFinitePresentation B S hS f ∧ FormallySmooth f

AlgebraicGeometry.Space.isSmooth_of_isLocallyOfFinitePresentation_of_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothFormallySmooth.lean, line 735. The attribute's comment: “condition (2) implies condition (1)”.

Stacks 04AM, the implication towards smoothness. A morphism of algebraic spaces over S which is locally of finite presentation and formally smooth is smooth.

Smoothness of f is a property of its étale charts, so there is nothing to descend: a chart h : U ⟶ V is locally of finite presentation by hypothesis, and AlgebraicGeometry.Space.exists_lift_scheme_of_formallySmooth solves every lifting problem for it along a first-order thickening of affine schemes contained in the site. That is exactly the hypothesis of Stacks.Smooth.smooth_of_exists_lift_of_size_lt, which upgrades it to smoothness: the only thickening the criterion needs is the spectrum of a polynomial presentation of the sections over an affine chart, and the site contains it.

theorem isSmooth_of_isLocallyOfFinitePresentation_of_formallySmooth
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y}
    (hlfp : IsLocallyOfFinitePresentation B S hS f) (hf : FormallySmooth f) :
    IsSmooth B S hS f

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_and_formallySmooth_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothFormallySmooth.lean, line 758. The attribute's comment: “condition (1) implies condition (2), for a representable morphism”.

Stacks 04AM, the implication from smoothness, for a representable morphism. A smooth representable morphism of algebraic spaces over S is locally of finite presentation and formally smooth.

Local finite presentation is Tag 04AJ. For formal smoothness, smoothness of a representable morphism is smoothness of each of its base changes to an object of the site by Tag 03MJ, so the base change of f along a section y of the target over the thickened test object is a smooth morphism of schemes; the scheme case Tag 02H6 extends the section of that base change cut out by the given section of X over the test object, and the extension is a morphism of the site because the inclusion of the site into schemes is fully faithful.

theorem isLocallyOfFinitePresentation_and_formallySmooth_of_isSmooth
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hrep : yoneda.relativelyRepresentable f) (hf : IsSmooth B S hS f) :
    IsLocallyOfFinitePresentation B S hS f ∧ FormallySmooth f
Tag 0CHJ, a lemma

Tag 0CHJ in the Stacks Project.

AlgebraicGeometry.Space.exists_isEtaleCovering_lift_of_isSmooth_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothStrongLift.lean, line 193.

Stacks 0CHJ. Let S be a scheme and consider a commutative square of algebraic spaces over S 

X ←--a-- T
|        |
f        i
↓        ↓
Y ←--b-- T'
in which f is smooth and i is a thickening. Then there is an étale covering of T' by affine schemes T'ₚ of the site such that over each member the square can be filled in: there is a ψ : T'ₚ ⟶ X with ψ over Y equal to T'ₚ ⟶ T' ⟶ Y and with the restriction of ψ to T ×_{T'} T'ₚ equal to the restriction of a.

The covering is indexed by the points of T', and the member at a point contains that point.

The proof follows the source, with the three reductions performed in one step for each member of the covering rather than globally. Write Z = X ×_Y T'; it is smooth over T' because f is, and the given data provide a section σ : T ⟶ Z of Z ⟶ T' over T. Given a point of T', choose an affine étale chart P of T' through it (Stacks 03FX, in the pointwise form AlgebraicGeometry.Space.exists_affine_etale_chart_at_point) and let J = T ×_{T'} P, an affine scheme and a thickening of P. Pulling an atlas of Z back along J ⟶ Z and intersecting with the base change of P to that atlas produces an affine chart U of Z lying over P — so that U ⟶ P is a smooth morphism of affine schemes, since smoothness of Z ⟶ T' is exactly the condition on every square of étale charts — together with an étale N ⟶ J through the chosen point and a morphism N ⟶ U over Z. Topological invariance of the étale site (Stacks 039R, in the size-controlled cartesian form AlgebraicGeometry.Space.exists_etaleLift_isPullback_of_chart) lifts N ⟶ J to an étale V ⟶ P with N = T ×_{T'} V; shrinking V to an affine open through the point makes it affine, and Stacks.Smooth.exists_lift_of_isClosedImmersion_of_surjective — the geometric form of Algebra, Lemma 10.138.17 — then extends T ×_{T'} V' ⟶ U over the thickening to V' ⟶ U. The member of the covering is V', and ψ is V' ⟶ U ⟶ Z ⟶ X.

theorem exists_isEtaleCovering_lift_of_isSmooth_of_isThickeningHom
    {X Y T T' : AlgebraicSpaces B S hS} {f : X ⟶ Y} (hf : IsSmooth B S hS f.hom)
    {i : T ⟶ T'} (hi : IsThickeningHom B S hS i) (a : T ⟶ X) (b : T' ⟶ Y)
    (hcomm : a ≫ f = i ≫ b) :
    ∃ (Z : points B S hS T'.obj → BigFppfOver B S hS)
      (q : ∀ p, yoneda.obj (Z p) ⟶ T'.obj),
      (∀ p, IsAffine ((BigFppfOver.toScheme B S hS).obj (Z p))) ∧
      IsEtaleCovering B S hS (fun p ↦ yoneda.obj (Z p)) q ∧
      ∀ p, ∃ ψ : yoneda.obj (Z p) ⟶ X.obj,
        ψ ≫ f.hom = q p ≫ b.hom ∧
        pullback.snd i.hom (q p) ≫ ψ = pullback.fst i.hom (q p) ≫ a.hom
Tag 061I, a lemma

Tag 061I in the Stacks Project.

AlgebraicGeometry.isLocallyProjective_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/Differentials.lean, line 78. The attribute's comment: “for morphisms of schemes”. References: EGA IV (17.2.3), “(i) locally projective”.

Stacks 06B5. The sheaf of relative differentials of a formally smooth morphism of schemes is locally projective on its source. This is Stacks 061I for a morphism of algebraic spaces that is a morphism of schemes.

theorem isLocallyProjective_relativeDifferentials {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : FormallySmooth f) :
    Scheme.Modules.IsLocallyProjective (Scheme.Hom.relativeDifferentials f)

AlgebraicGeometry.Space.isLocallyProjective_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsLocallyProjective.lean, line 206.

Stacks 061I. The sheaf of relative differentials Ω_{X/Y} of a formally smooth morphism f : X ⟶ Y of algebraic spaces over a scheme S is locally projective on X.

theorem isLocallyProjective_sheafOfDifferentials {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : FormallySmooth f.hom) :
    IsLocallyProjective B S hS X.2
      ⟨sheafOfDifferentials B S hS f, isQuasicoherentOnSite_sheafOfDifferentials B S hS f⟩
Tag 061J, a lemma

Tag 061J in the Stacks Project.

AlgebraicGeometry.SmallEtale.subsingleton_sheafH_one_sheafHom_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/InternalHomAffineVanishing.lean, line 341.

Stacks 061J for an associated module. Let T be an affine scheme and let M be a locally projective quasi-coherent 𝒪_T-module. The first cohomology of the internal hom from the associated module M^a to an 𝒪-module 𝓖 on the small étale site of T vanishes.

public theorem subsingleton_sheafH_one_sheafHom_associatedModule
    [AlgebraicGeometry.IsAffine T] (M : T.Modules)
    [M.IsQuasicoherent] (hM : Scheme.Modules.IsLocallyProjective M)
    (G : SheafOfModules.{u} (structureSheaf B T hT)) [G.IsQuasicoherentOnSite] :
    Subsingleton (Sheaf.H.{w}
      ((SheafOfModules.toSheaf (structureSheaf B T hT)).obj
        (sheafHom B T hT ((associatedModule B T hT).obj M) G)) 1)

AlgebraicGeometry.SmallEtale.subsingleton_sheafH_one_sheafHom_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/InternalHomAffineVanishing.lean, line 357.

Stacks 061J. Let T be an affine scheme and let 𝓕 and 𝓖 be quasi-coherent 𝒪-modules on the small étale site of T. If 𝓕 is locally projective — that is, if its restriction to the small Zariski site of T is a locally projective 𝒪_T-module, which is what Stacks 060R defines local projectivity to mean — then the first cohomology of the internal hom 𝓗om_𝒪(𝓕, 𝓖) vanishes.

public theorem subsingleton_sheafH_one_sheafHom_of_isLocallyProjective
    [AlgebraicGeometry.IsAffine T]
    (F G : SheafOfModules.{u} (structureSheaf B T hT)) [F.IsQuasicoherentOnSite]
    [G.IsQuasicoherentOnSite]
    (hF : Scheme.Modules.IsLocallyProjective ((restrictModule B T hT).obj F)) :
    Subsingleton (Sheaf.H.{w}
      ((SheafOfModules.toSheaf (structureSheaf B T hT)).obj (sheafHom B T hT F G)) 1)
Tag 061K, a lemma

Tag 061K in the Stacks Project.

AlgebraicGeometry.Space.formallySmooth_tfae_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/ChartGlue/Main061K.lean, line 316.

For a morphism f : X ⟶ Y of algebraic spaces over S, the following are equivalent: 1. f is formally smooth; 2. for every commuting square of étale scheme charts a : U ⟶ X, b : V ⟶ Y, ψ : U ⟶ V, the morphism of schemes ψ is formally smooth; 3. there is a commuting square of étale scheme charts with a and b surjective and ψ formally smooth.

theorem formallySmooth_tfae_etaleCharts (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [FormallySmooth f,
      HoldsOnEveryEtaleChart B S hS (@Stacks.Smooth.FormallySmoothScheme.{u}) f,
      ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (ψ : U ⟶ V),
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        yoneda.map ψ ≫ b = a ≫ f ∧
        Stacks.Smooth.FormallySmoothScheme ((BigFppfOver.toScheme B S hS).map ψ)]

AlgebraicGeometry.Space.formallySmooth_iff_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmoothChartBiconditional.lean, line 282. The attribute's comment: “condition (2), granted Stacks 0D0F (3) ⟹ (1) and the pseudo-torsor triviality of 03AJ”.

Stacks 061K, the equivalence of (1) and (2). A morphism of algebraic spaces over S is formally smooth exactly when the morphism of schemes underlying every commuting square of étale scheme charts is formally smooth, granted the scheme-level implication (3) ⟹ (1) of [Stacks Project, Tag 0D0F] and the triviality of the pseudo-torsor of lifts.

theorem formallySmooth_iff_etaleCharts
    (h0D0F : ∀ {X' Y' : Scheme.{u}} (g : X' ⟶ Y'),
      Stacks.Smooth.FormallySmoothAffineLocally g → Stacks.Smooth.FormallySmoothScheme g)
    (hGlue : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' →
      FormallySmoothEtaleLocally B S hS g → FormallySmooth g)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallySmooth f ↔
      HoldsOnEveryEtaleChart B S hS (@Stacks.Smooth.FormallySmoothScheme.{u}) f

AlgebraicGeometry.Space.formallySmooth_iff_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmoothChartBiconditional.lean, line 305. The attribute's comment: “condition (3), granted Stacks 0D0F (3) ⟹ (1) and the pseudo-torsor triviality of 03AJ”.

Stacks 061K, the equivalence of (1) and (3). A morphism of algebraic spaces over S is formally smooth exactly when there is one commuting square of étale scheme charts, both chart maps surjective, whose underlying morphism of schemes is formally smooth, granted the scheme-level implication (3) ⟹ (1) of [Stacks Project, Tag 0D0F] and the triviality of the pseudo-torsor of lifts.

theorem formallySmooth_iff_surjectiveEtaleChart
    (h0D0F : ∀ {X' Y' : Scheme.{u}} (g : X' ⟶ Y'),
      Stacks.Smooth.FormallySmoothAffineLocally g → Stacks.Smooth.FormallySmoothScheme g)
    (hGlue : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' →
      FormallySmoothEtaleLocally B S hS g → FormallySmooth g)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallySmooth f ↔
      ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (ψ : U ⟶ V),
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        yoneda.map ψ ≫ b = a ≫ f ∧
        Stacks.Smooth.FormallySmoothScheme ((BigFppfOver.toScheme B S hS).map ψ)
Tag 06CS, a lemma

Tag 06CS in the Stacks Project.

AlgebraicGeometry.Space.formallySmooth_isLocalAtTarget_fpqc', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/FpqcLocalAtTarget.lean, line 55.

Formal smoothness of morphisms of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH: for every fpqc covering {Yᵢ ⟶ Y} of algebraic spaces, a morphism f : X ⟶ Y is formally smooth if and only if every base change X ×_Y Yᵢ ⟶ Yᵢ is.

theorem formallySmooth_isLocalAtTarget_fpqc' (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (formallySmoothProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

AlgebraicGeometry.Space.formallySmooth_isLocalAtTarget_fpqc_of_chartDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmoothFpqcLocalAtTarget.lean, line 389. The attribute's comment: “granting the implication (3) ⟹ (1) of Stacks 061K with condition (3) read on affine opens; the library's own Stacks 061K is itself conditional on the implication (3) ⟹ (1) of Stacks 0D0F and on the pseudo-torsor triviality of Stacks 03AJ, and this grant is implied by those two, so it is the weaker assumption”.

Stacks 06CS, granting the implication (3) ⟹ (1) of Stacks 061K. Formal smoothness of morphisms of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

The ascent half is Stacks 049U. For the descent half, a lifting problem for f : X ⟶ Y is one for the base change of f along a point of Y with affine source (AlgebraicGeometry.Space.formallySmooth_iff_affine_pullback); over such a point the fpqc condition of Stacks 03MQ supplies a finite family of affine objects covering it and refining the given covering, and AlgebraicGeometry.Space.formallySmooth_of_affineFpqcPresieve descends along that family.

theorem formallySmooth_isLocalAtTarget_fpqc_of_chartDescent (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (hchart : FormallySmoothEtaleChartDescent B S hS) :
    (formallySmoothProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

AlgebraicGeometry.Space.formallySmooth_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmoothFpqcLocalAtTarget.lean, line 432. The attribute's comment: “granting the implication (3) ⟹ (1) of Stacks 061K with condition (3) read on affine opens; the library's own Stacks 061K is itself conditional on the implication (3) ⟹ (1) of Stacks 0D0F and on the pseudo-torsor triviality of Stacks 03AJ, and this grant is implied by those two, so it is the weaker assumption”.

Stacks 06CS. Formal smoothness of morphisms of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

The one input not available in this library is the implication (3) ⟹ (1) of Stacks 061K, read on affine opens, which is carried as the instance hypothesis AlgebraicGeometry.Space.FormallySmoothEtaleChartDescent; see AlgebraicGeometry.Space.formallySmooth_isLocalAtTarget_fpqc_of_chartDescent, where it appears as an explicit hypothesis, for the argument.

instance formallySmooth_isLocalAtTarget_fpqc (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) [hchart : FormallySmoothEtaleChartDescent B S hS] :
    (formallySmoothProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)
Tag 06BI, a lemma

Tag 06BI in the Stacks Project.

AlgebraicGeometry.Space.triangleDifferentials_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDifferentialsShortExact.lean, line 264. The attribute's comment: “granted as hchart the étale localization of 04CU and 04CS identifying the restriction of the comparison map of Ω to a surjective étale chart with the chart morphisms' own comparison map of Ω”.

Stacks 06BI. For morphisms f : X ⟶ Y and g : Y ⟶ B of algebraic spaces over S with f formally smooth, the transitivity sequence 0 ⟶ f^*Ω_{Y/B} ⟶ Ω_{X/B} ⟶ Ω_{X/Y} ⟶ 0 of Stacks 05Z8 is short exact.

Short exactness adds monomorphy of the first map to the three clauses of Stacks 05Z8, and AlgebraicGeometry.Space.pullbackDifferentialsMap_mono_of_formallySmooth supplies it from the case of schemes by étale localization, granted the chart comparison.

theorem triangleDifferentials_shortExact (f : X ⟶ Y) (g : Y ⟶ Z) (hf : FormallySmooth f.hom)
    (hchart : PullbackDifferentialsMapChartComparison B S hS f g) :
    ∃ h : pullbackDifferentialsMap B S hS f g ≫ toRelativeDifferentials B S hS f g = 0,
      (ShortComplex.mk _ _ h).ShortExact

AlgebraicGeometry.Space.triangleDifferentials_shortExact_of_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeComparisonMapSquare.lean, line 570.

Stacks 06BI. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over S with f formally smooth. Then the sequence 0 ⟶ f^*Ω_{Y/Z} ⟶ Ω_{X/Z} ⟶ Ω_{X/Y} ⟶ 0 of Stacks 05Z8 is short exact.

The first map is a monomorphism étale locally: on compatible étale charts U ⟶ V ⟶ W with U ⟶ V formally smooth (Stacks 061K) it is the scheme statement (Stacks 02HP), carried to the spaces by Stacks 04CU and 04CS (AlgebraicGeometry.Space.pullbackDifferentialsMapSchemeSpaceComparison); exactness at the other two terms is Stacks 05Z8.

theorem triangleDifferentials_shortExact_of_formallySmooth (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : FormallySmooth f.hom) :
    ∃ h : pullbackDifferentialsMap B S hS f g ≫ toRelativeDifferentials B S hS f g = 0,
      (ShortComplex.mk _ _ h).ShortExact
Tag 06BJ, a lemma

Tag 06BJ in the Stacks Project.

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.conormalSequence_shortExact_of_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceFormallySmoothShortExact.lean, line 190.

Stacks 06BJ. Let h = ι ≫ h' : Z ⟶ X be a formally unramified morphism of algebraic spaces over Y, with universal first order thickening Z ⊂ Z' over X given by hZ, and assume Z is formally smooth over Y. Then the canonical exact sequence 

  0 ⟶ 𝒞_{Z/X} ⟶ h^*Ω_{X/Y} ⟶ Ω_{Z/Y} ⟶ 0
of Stacks 060F, AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.conormalSequence, is short exact.

Exactness at the middle and the epimorphism on the right are Stacks 060F. The first arrow followed by the isomorphism of Stacks 060E is the first arrow of Stacks 05ZA for Z ⊂ Z', which is a monomorphism by AlgebraicGeometry.Space.mono_conormalSequenceFirstMap_of_formallySmooth.

theorem conormalSequence_shortExact_of_formallySmooth
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (hsm : FormallySmooth (universalThickeningInclusion B S hS hZ ≫ h' ≫ p).hom) :
    ShortComplex.ShortExact (C := Modules.{u, u} B S hS (universalThickeningSubSpace B S hS hZ).obj
      (universalThickeningSubSpace B S hS hZ).property) (hZ.conormalSequence B S hS p)
Tag 06BK, a lemma

Tag 06BK in the Stacks Project.

AlgebraicGeometry.Space.exists_retraction_modulePullback_conormalMap_universalThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceUnramifiedPairSplitting.lean, line 307. The attribute's comment: “the first arrow of the conormal sequence is split over an affine étale chart”.

Stacks 06BK: the first arrow of the conormal sequence is étale-locally split. Let i : Z ⟶ X and j : Z ⟶ Y sit in a commutative triangle i ≫ g = j with g formally smooth, let Z ⊂ Z' be a universal first-order thickening of Z over X and Z ⊂ Z'' one of Z over Y, and let V ⟶ Z'' be an étale chart with V affine. Then the inverse image along the projection Z ×_{Z''} V ⟶ Z of the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of the conormal sequence of [Stacks Project, Tag 06BE] admits a retraction.

The first arrow is named here through its definition: it is the conormal map of [Stacks Project, Tag 04CP] for the square of [Stacks Project, Tag 060A] built from the canonical morphism Z' ⟶ Z'' and the identification of the two smaller spaces, which is what AlgebraicGeometry.Space.universalThickeningConormalMap abbreviates.

theorem exists_retraction_modulePullback_conormalMap_universalThickening (g : X ⟶ Y)
    {i : Z ⟶ X} {j : Z ⟶ Y} (hij : i ≫ g = j)
    (ti : UniversalFirstOrderThickening B S hS i)
    (tj : UniversalFirstOrderThickening B S hS j) (hg : FormallySmooth g.hom)
    (V : BigFppfOver B S hS) (v : yoneda.obj V ⟶ tj.ambient.obj) (hv : IsEtale B S hS v)
    (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj V)) :
    ∃ r, (modulePullback B S hS (thickeningChartProjection B S hS ti tj V v)).map
        (@conormalMap B S hS ti.ambient tj.ambient ti.closedSub tj.closedSub
          (universalThickeningComparison B S hS g hij ti tj)
          (ObjectProperty.homMk (universalThickeningSourceMap B S hS ti tj))
          (universalThickeningComparison_square B S hS g hij ti tj)) ≫ r = 𝟙 _

AlgebraicGeometry.Space.exists_retraction_cover_modulePullback_conormalMap_universalThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceUnramifiedPairSplitting.lean, line 405. The attribute's comment: “the first arrow of the conormal sequence is split over a covering by affine étale charts”.

Stacks 06BK, in a covering form. Under the hypotheses of AlgebraicGeometry.Space.exists_retraction_modulePullback_conormalMap_universalThickening, an arbitrary étale chart V ⟶ Z'' is covered by affine étale charts over whose chart of Z the first arrow of the conormal sequence admits a retraction.

theorem exists_retraction_cover_modulePullback_conormalMap_universalThickening (g : X ⟶ Y)
    {i : Z ⟶ X} {j : Z ⟶ Y} (hij : i ≫ g = j)
    (ti : UniversalFirstOrderThickening B S hS i)
    (tj : UniversalFirstOrderThickening B S hS j) (hg : FormallySmooth g.hom)
    (V : BigFppfOver B S hS) (v : yoneda.obj V ⟶ tj.ambient.obj) (hv : IsEtale B S hS v) :
    ∃ (I : Type u) (V' : I → BigFppfOver B S hS) (π : ∀ k, V' k ⟶ V),
      Sieve.generate (Presieve.ofArrows V' π) ∈ BigFppfOver.topology B S hS V ∧
        ∀ k, ∃ r, (modulePullback B S hS
              (thickeningChartProjection B S hS ti tj (V' k) (yoneda.map (π k) ≫ v))).map
            (@conormalMap B S hS ti.ambient tj.ambient ti.closedSub tj.closedSub
              (universalThickeningComparison B S hS g hij ti tj)
              (ObjectProperty.homMk (universalThickeningSourceMap B S hS ti tj))
              (universalThickeningComparison_square B S hS g hij ti tj)) ≫ r = 𝟙 _

AlgebraicGeometry.Space.mono_conormalMap_universalThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceUnramifiedPairSplitting.lean, line 438. The attribute's comment: “the conormal sequence is exact on the left”.

Stacks 06BK: the conormal sequence is exact on the left. Let i : Z ⟶ X and j : Z ⟶ Y sit in a commutative triangle i ≫ g = j with g formally smooth, and let Z ⊂ Z' be a universal first-order thickening of Z over X and Z ⊂ Z'' one of Z over Y. Then the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of the conormal sequence of [Stacks Project, Tag 06BE] is a monomorphism.

The first arrow is named through its definition, as the conormal map of [Stacks Project, Tag 04CP] for the square of [Stacks Project, Tag 060A]; see the implementation notes of this file. It is split injective over each affine étale chart of Z'' by AlgebraicGeometry.Space.exists_retraction_modulePullback_conormalMap_universalThickening, and the charts of Z cut out by the affine étale charts of an atlas of Z'' form an étale covering of Z, so the two inverse images of a pair of morphisms it equalises agree on that covering and the pair is equal.

theorem mono_conormalMap_universalThickening (g : X ⟶ Y) {i : Z ⟶ X} {j : Z ⟶ Y}
    (hij : i ≫ g = j) (ti : UniversalFirstOrderThickening B S hS i)
    (tj : UniversalFirstOrderThickening B S hS j) (hg : FormallySmooth g.hom) :
    Mono (@conormalMap B S hS ti.ambient tj.ambient ti.closedSub tj.closedSub
      (universalThickeningComparison B S hS g hij ti tj)
      (ObjectProperty.homMk (universalThickeningSourceMap B S hS ti tj))
      (universalThickeningComparison_square B S hS g hij ti tj))
Sources
LeanAlgebraicGeometry.Space.FormallySmooth · AlgebraicGeometry.Space.FormallySmooth.comp · AlgebraicGeometry.Space.FormallySmooth.baseChange · AlgebraicGeometry.formallyEtale_iff_formallySmooth_and_formallyUnramified · AlgebraicGeometry.Space.formallySmooth_of_isEtale_square · AlgebraicGeometry.Space.isSmooth_iff_isLocallyOfFinitePresentation_and_formallySmooth · AlgebraicGeometry.Space.isSmooth_of_isLocallyOfFinitePresentation_of_formallySmooth · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_and_formallySmooth_of_isSmooth

Section76.20 Smoothness over a Noetherian base#

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

Tag 0APN, a lemma

Tag 0APN in the Stacks Project.

AlgebraicGeometry.Space.LiftsAt.mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtInfinitesimalLifting.lean, line 331. The attribute's comment: “condition (2) implies condition (3)”.

Stacks 0APN, (2) implies (3). The lifting property at a point against a class of extensions implies the lifting property against any subclass.

theorem LiftsAt.mono {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y}
    {x : points B S hS X}
    {extension extension' : ∀ ⦃R' R : CommRingCat.{u}⦄, (R' ⟶ R) → Prop}
    (hsub : ∀ ⦃R' R : CommRingCat.{u}⦄ (φ : R' ⟶ R), extension' φ → extension φ)
    (h : LiftsAt B S hS f x extension) :
    LiftsAt B S hS f x extension'

AlgebraicGeometry.Space.isSmoothAt_of_liftsAt_isSmallExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtInfinitesimalLifting.lean, line 752. The attribute's comment: “condition (3) implies condition (1)”.

Stacks 0APN, (3) implies (1). A morphism of algebraic spaces over S which is locally of finite type, whose target is locally Noetherian, and which has the lifting property at a point of its source against small extensions, is smooth at that point.

A pointed étale chart at the point with locally Noetherian target chart receives every lifting problem for its morphism of charts along a residually trivial small extension, so Stacks 02HX makes that morphism of charts smooth at the chart point; smoothness at a point being an étale-local property of germs, Stacks 04NC reads that back as smoothness of the morphism at the point.

theorem isSmoothAt_of_liftsAt_isSmallExtension
    {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)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (hFiniteType : IsLocallyOfFiniteType B S hS f)
    (hlift : LiftsAt B S hS f x fun ⦃_ _⦄ φ => InfinitesimalLifting.IsSmallExtension φ) :
    IsSmoothAt B S hS f x

AlgebraicGeometry.Space.IsSmoothAt.liftsAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtLiftingCriterion.lean, line 98. The attribute's comment: “condition (1) implies conditions (2) and (3)”. References: SGA 3 XI (1.5), “partial”.

Stacks 0APN, (1) implies (2) and (3). A morphism of algebraic spaces over S which is smooth at a point of its source has the lifting property at that point against every class of square-zero surjections of local rings.

Smoothness at the point gives an open subspace of the source containing it on which the morphism is smooth, hence formally smooth by Stacks 04AM (AlgebraicGeometry.Space.formallySmooth_of_isSmooth'); the spectrum of a local ring whose closed point lies over the given point factors through that open subspace, because the closed point specializes from every point, so the lifting problem is a lifting problem for the restricted morphism.

theorem IsSmoothAt.liftsAt
    {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}
    (hsm : IsSmoothAt B S hS f x)
    (extension : ∀ ⦃R' R : CommRingCat.{u}⦄, (R' ⟶ R) → Prop)
    (hextension : ∀ ⦃R' R : CommRingCat.{u}⦄ (φ : R' ⟶ R),
      extension φ → InfinitesimalLifting.IsSquareZeroSurjection φ) :
    LiftsAt B S hS f x extension

AlgebraicGeometry.Space.tfae_isSmoothAt_liftsAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtLiftingCriterion.lean, line 156. References: SGA 3 XI (1.5), “partial”.

Stacks 0APN. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y locally Noetherian, and let x be a point of X. Then the following are equivalent: f is smooth at x; every lifting problem at x along a surjection of local rings with square-zero kernel has a solution; every lifting problem at x along a small extension has a solution.

The implication from (1) to (2) is AlgebraicGeometry.Space.IsSmoothAt.liftsAt, from (2) to (3) is AlgebraicGeometry.Space.LiftsAt.mono and from (3) to (1) is AlgebraicGeometry.Space.isSmoothAt_of_liftsAt_isSmallExtension.

theorem tfae_isSmoothAt_liftsAt
    {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)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (hFiniteType : IsLocallyOfFiniteType B S hS f) :
    [IsSmoothAt B S hS f x,
      LiftsAt B S hS f x fun ⦃_ _⦄ φ => InfinitesimalLifting.IsSquareZeroSurjection φ,
      LiftsAt B S hS f x fun ⦃_ _⦄ φ =>
        InfinitesimalLifting.IsSmallExtension φ].TFAE
Tag 0APP, a lemma

Tag 0APP in the Stacks Project.

AlgebraicGeometry.Space.not_forall_isSmooth_iff_liftsAgainstFiniteTypeSmallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothnessFiniteTypeLiftingCounterexample.lean, line 444. The attribute's comment: “the statement with the test morphism Spec B' ⟶ Y of finite type is false: the point Spec ℚ ⟶ 𝔸¹_ℚ/ℤ of the zero section satisfies that condition (2) and is not smooth. The corrected form, with Spec B' ⟶ Y locally of finite type, is isSmooth_iff_forall_exists_lift_isSmallExtension”.

Stacks 0APP, as stated, is false. The equivalence of smoothness with condition (2) of Stacks 0APP, in which the test morphism Spec B' ⟶ Y is required to be of finite type, fails for some morphism of algebraic spaces locally of finite type over a locally Noetherian target: the point Spec ℚ ⟶ 𝔸¹_ℚ/ℤ of exists_not_isSmooth_liftsAgainstFiniteTypeSmallExtensions satisfies condition (2) and is not smooth.

The implication from smoothness does hold, and is AlgebraicGeometry.Space.IsSmooth.liftsAgainstFiniteTypeSmallExtensions; the corrected equivalence, with the test morphism required only to be locally of finite type, is AlgebraicGeometry.Space.isSmooth_iff_forall_exists_lift_isSmallExtension.

theorem not_forall_isSmooth_iff_liftsAgainstFiniteTypeSmallExtensions :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
      IsAlgebraicSpace B S hS Y → ∀ f : X ⟶ Y,
      HasEtaleLocalProperty B S hS Y (fun Z : Scheme.{u} => IsLocallyNoetherian Z) →
      IsLocallyOfFiniteType B S hS f →
      (IsSmooth B S hS f ↔ LiftsAgainstFiniteTypeSmallExtensions B S hS f)

AlgebraicGeometry.Space.IsSmooth.liftsAgainstFiniteTypeSmallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothnessOverNoetherianBaseLifting.lean, line 172. The attribute's comment: “(1) implies (2) as stated, with the test morphism Spec B' ⟶ Y of finite type”.

Stacks 0APP, (1) implies (2), as stated. A smooth morphism of algebraic spaces satisfies condition (2) of Stacks 0APP with the test morphism of finite type. No hypothesis on the target is needed.

theorem IsSmooth.liftsAgainstFiniteTypeSmallExtensions
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsSmooth B S hS f) : LiftsAgainstFiniteTypeSmallExtensions B S hS f

AlgebraicGeometry.Space.isSmooth_iff_forall_exists_lift_isSmallExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothnessOverNoetherianBaseLifting.lean, line 408. The attribute's comment: “corrected form: the test morphism Spec R' ⟶ Y is required to be locally of finite type. With it of finite type, as in the source, the statement is false: not_forall_isSmooth_iff_liftsAgainstFiniteTypeSmallExtensions”. References: SGA 1 III (3.1), “(iii), (iii)⇒(i)”.

Stacks 0APP. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y locally Noetherian. Then f is smooth if and only if every solid square whose vertical map is induced by a small extension φ : R' ⟶ R of Artinian local rings and whose map Spec R' ⟶ Y is locally of finite type admits a dotted arrow making the diagram commute.

The implication towards the lifting property is the formal smoothness of a smooth morphism (Stacks 04AM). The converse runs the scheme-level criterion of Stacks 02HY on each commuting square of étale charts, pushing each scheme-level lifting problem into the algebraic spaces and pulling its solution back along the formally étale charts.

The source asks the map Spec R' ⟶ Y to be of finite type; with that condition the equivalence is false, by AlgebraicGeometry.Space.not_forall_isSmooth_iff_liftsAgainstFiniteTypeSmallExtensions, so here the map is asked only to be locally of finite type. See the module documentation.

theorem isSmooth_iff_forall_exists_lift_isSmallExtension
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (hFiniteType : IsLocallyOfFiniteType B S hS f) :
    IsSmooth B S hS f ↔
      ∀ ⦃R' R : CommRingCat.{u}⦄ (φ : R' ⟶ R),
        InfinitesimalLifting.IsSmallExtension φ →
        ∀ (T T' : BigFppfOver B S hS) (i : T ⟶ T')
          (e : (BigFppfOver.toScheme B S hS).obj T ≅ Spec R)
          (e' : (BigFppfOver.toScheme B S hS).obj T' ≅ Spec R'),
          (BigFppfOver.toScheme B S hS).map i = e.hom ≫ Spec.map φ ≫ e'.inv →
          ∀ (α : yoneda.obj T ⟶ X) (β : yoneda.obj T' ⟶ Y),
            IsLocallyOfFiniteType B S hS β →
            α ≫ f = yoneda.map i ≫ β →
            ∃ γ : yoneda.obj T' ⟶ X, yoneda.map i ≫ γ = α ∧ γ ≫ f = β
Tag 0APQ, a lemma

Tag 0APQ in the Stacks Project.

AlgebraicGeometry.Space.isSmoothAt_of_isSmooth_nthOrderInfinitesimalNeighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothnessOnInfinitesimalNeighbourhoods.lean, line 97. The attribute's comment: “part (1): smooth. Z is an arbitrary closed subspace and Zₙ its nth infinitesimal neighbourhood (Tag 05ZV), built on a surjective étale chart from the invariant ideal sheaf cutting out Z, which exists and is unique by exists_isInvariantIdealSheaf_invariantSubspace_eq and ker_rep_snd_eq_of_invariantSubspace_eq; Xₙ is any fibre product Zₙ ×_Y X”.

Stacks 0APQ, part (1). Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y locally Noetherian. Let Z ⊆ Y be a closed subspace, cut out on a surjective étale chart φ : U ⟶ Y by the invariant sheaf of ideals J, so that its nth infinitesimal neighbourhood is Zₙ = nthOrderInfinitesimalNeighbourhood φ J n, and let Xₙ = Zₙ ×_Y X. If Xₙ ⟶ Zₙ is smooth for every n, then f is smooth at every point of f⁻¹(Z).

Every closed subspace is cut out on every surjective étale chart by exactly one invariant sheaf of ideals (AlgebraicGeometry.Space.exists_isInvariantIdealSheaf_invariantSubspace_eq), so this applies to every closed subspace of Y.

theorem isSmoothAt_of_isSmooth_nthOrderInfinitesimalNeighbourhood
    (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y.1)
    (hNoeth : HasEtaleLocalProperty B S hS Y.1 (fun W : Scheme.{u} => IsLocallyNoetherian W))
    (hFiniteType : IsLocallyOfFiniteType B S hS f)
    (Z : ClosedSubspaces B S hS Y.1)
    {J : ((BigFppfOver.toScheme B S hS).obj U).IdealSheafData}
    (hJ : IsInvariantIdealSheaf B S hS hs J)
    (hZJ : invariantSubspace B S hS φ (Subobject.mk J.subschemeι) = Z.1)
    (Xn : ℕ → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (fn : ∀ n, Xn n ⟶ (nthOrderInfinitesimalNeighbourhood B S hS φ J n).toFunctor)
    (pn : ∀ n, Xn n ⟶ X)
    (hcart : ∀ n, IsPullback (pn n) (fn n) f (nthOrderInfinitesimalNeighbourhood B S hS φ J n).ι)
    (hsmooth : ∀ n, IsSmooth B S hS (fn n))
    (x : points B S hS X)
    (hx : pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS Z.1.toFunctor Z.1.ι)) :
    IsSmoothAt B S hS f x

AlgebraicGeometry.Space.isEtaleAt_of_isEtale_nthOrderInfinitesimalNeighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothnessOnInfinitesimalNeighbourhoods.lean, line 164. The attribute's comment: “part (2): étale. Z is an arbitrary closed subspace and Zₙ its nth infinitesimal neighbourhood (Tag 05ZV), built on a surjective étale chart from the invariant ideal sheaf cutting out Z, which exists and is unique by exists_isInvariantIdealSheaf_invariantSubspace_eq and ker_rep_snd_eq_of_invariantSubspace_eq; Xₙ is any fibre product Zₙ ×_Y X”.

Stacks 0APQ, part (2). In the situation of AlgebraicGeometry.Space.isSmoothAt_of_isSmooth_nthOrderInfinitesimalNeighbourhood, if Xₙ = Zₙ ×_Y X ⟶ Zₙ is étale for every n, then f is étale at every point of f⁻¹(Z).

Étaleness of every base change gives smoothness of every base change, hence smoothness of f at the point by part (1). It also gives unramifiedness of the zeroth base change, hence unramifiedness of f at the point, which lies in the image of X₀ because the zeroth square is cartesian. Stacks 02GK for algebraic spaces assembles the two.

theorem isEtaleAt_of_isEtale_nthOrderInfinitesimalNeighbourhood
    (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y.1)
    (hNoeth : HasEtaleLocalProperty B S hS Y.1 (fun W : Scheme.{u} => IsLocallyNoetherian W))
    (hFiniteType : IsLocallyOfFiniteType B S hS f)
    (Z : ClosedSubspaces B S hS Y.1)
    {J : ((BigFppfOver.toScheme B S hS).obj U).IdealSheafData}
    (hJ : IsInvariantIdealSheaf B S hS hs J)
    (hZJ : invariantSubspace B S hS φ (Subobject.mk J.subschemeι) = Z.1)
    (Xn : ℕ → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (fn : ∀ n, Xn n ⟶ (nthOrderInfinitesimalNeighbourhood B S hS φ J n).toFunctor)
    (pn : ∀ n, Xn n ⟶ X)
    (hcart : ∀ n, IsPullback (pn n) (fn n) f (nthOrderInfinitesimalNeighbourhood B S hS φ J n).ι)
    (hetale : ∀ n, IsEtale B S hS (fn n))
    (x : points B S hS X)
    (hx : pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS Z.1.toFunctor Z.1.ι)) :
    IsEtaleAt B S hS f x
Sources
LeanAlgebraicGeometry.Space.LiftsAt.mono · AlgebraicGeometry.Space.isSmoothAt_of_liftsAt_isSmallExtension · AlgebraicGeometry.Space.IsSmoothAt.liftsAt · AlgebraicGeometry.Space.tfae_isSmoothAt_liftsAt · AlgebraicGeometry.Space.not_forall_isSmooth_iff_liftsAgainstFiniteTypeSmallExtensions · AlgebraicGeometry.Space.IsSmooth.liftsAgainstFiniteTypeSmallExtensions · AlgebraicGeometry.Space.isSmooth_iff_forall_exists_lift_isSmallExtension · AlgebraicGeometry.Space.isSmoothAt_of_isSmooth_nthOrderInfinitesimalNeighbourhood

Section76.21 The naive cotangent complex#

Section 76.21 of the Stacks Project, Tag 0D0U. 8 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0D0V, a definition

Tag 0D0V in the Stacks Project.

AlgebraicGeometry.Space.naiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentComplex.lean, line 58.

Stacks 0D0V. The naive cotangent complex NL_{X/Y} = NL_f of a morphism f : X ⟶ Y of algebraic spaces: the naive cotangent complex of the inverse-image form f⁻¹𝒪_Y ⟶ 𝒪_X of the structure map of the morphism of small étale ringed topoi of f.

noncomputable def naiveCotangentComplex (f : X ⟶ Y) :
    CochainComplex (_root_.SheafOfModules.{u + 1, u, u + 1, u}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u}
        (smallEtaleRingedTopos B S hS X).O)) ℤ
Tag 0D0W, a lemma

Tag 0D0W in the Stacks Project.

AlgebraicGeometry.Space.naiveCotangentEtaleLocalisationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentEtaleLocalisation.lean, line 183. The attribute's comment: “the canonical identification NL_{X/Y}|_{U_étale} = NL_{U/V} for a commutative square of algebraic spaces with p and q étale, REDUCED TO THE SECOND HALF OF THE SOURCE'S PROOF. What is proved is NL_{p⁻¹O_X / p⁻¹f⁻¹O_Y} ≅ NL_{U/V}: the two identifications of Tag 03LV, p⁻¹O_X = O_U and q⁻¹O_Y = O_V, together with the composition law of Tag 03G8 for the square, make the data defining the two complexes correspond, and the canonical chain map of Tag 08TX between them is then an isomorphism. The FIRST half, p⁻¹NL_{X/Y} = NL_{p⁻¹O_X / p⁻¹f⁻¹O_Y} (Modules on Sites, Lemma 08TZ), is not instantiated here, so the source of this isomorphism is not yet known to be the restriction NL_{X/Y}|_{U_étale}. Tag 08TZ itself IS carried for sites, as Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso, for an arbitrary morphism of topoi; what is missing is only its universe shape, which ties the ambient section universe of each topos to a universe containing its site's object universe, whereas the small étale site has objects in Type (u + 1) and structure sheaves in CommRingCat.{u}. Carried beyond the source's statement: the étale hypotheses are hypotheses IsEtale p.hom and IsEtale q.hom in the big-fppf-site presentation of algebraic spaces; the identification is an isomorphism of cochain complexes of sheaves of p⁻¹O_X-modules, the target being NL_{U/V} read there by restriction of scalars along p⁻¹O_X ≅ O_U, and NOTHING is asserted in the derived category D(O_U)”.

Stacks 0D0W, the identification of the two naive cotangent complexes. For a commuting square p ≫ f = g ≫ q of algebraic spaces over S with p and q étale,

NL_{p⁻¹𝒪_X / p⁻¹f⁻¹𝒪_Y} ≅ NL_{U/V},

the target read in complexes of sheaves of p⁻¹𝒪_X-modules through the identification p⁻¹𝒪_X ≅ 𝒪_U of Stacks 03LV.

Both horizontal morphisms of the square of sheaves of rings 

p⁻¹𝒪_X ──────▸ 𝒪_U
   ▲             ▲
   │             │
p⁻¹f⁻¹𝒪_Y ────▸ g⁻¹𝒪_V
are isomorphisms — the top one by Stacks 03LV at the étale morphism p, the bottom one by AlgebraicGeometry.Space.etaleSquareBaseRingIso — so the canonical chain map of Stacks 08TX attached to it is an isomorphism.

noncomputable def naiveCotangentEtaleLocalisationIso {p : U ⟶ X} {f : X ⟶ Y} {g : U ⟶ V}
    {q : V ⟶ Y} (h : p ≫ f = g ≫ q) (hp : IsEtale B S hS p.hom) (hq : IsEtale B S hS q.hom) :
    inverseImageNaiveCotangentComplex B S hS p f ≅
      ((_root_.SheafOfModules.restrictScalars.{u + 1}
          (underlyingRingHomOfSite.{u, u + 1, u}
            (etaleInverseImageStructureSheafIso B S hS p hp).hom)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj (naiveCotangentComplex B S hS g)

AlgebraicGeometry.Space.naiveCotangentEtaleLocalisationIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentEtaleLocalisation.lean, line 200. The attribute's comment: “the identification is the canonical chain map of Tag 08TX, not an arbitrary isomorphism; same scope as naiveCotangentEtaleLocalisationIso”.

The forward map of AlgebraicGeometry.Space.naiveCotangentEtaleLocalisationIso is the canonical chain map of Stacks 08TX attached to the square of sheaves of rings, so the identification is canonical.

theorem naiveCotangentEtaleLocalisationIso_hom {p : U ⟶ X} {f : X ⟶ Y} {g : U ⟶ V}
    {q : V ⟶ Y} (h : p ≫ f = g ≫ q) (hp : IsEtale B S hS p.hom)
    (hq : IsEtale B S hS q.hom) :
    (naiveCotangentEtaleLocalisationIso B S hS h hp hq).hom =
      Stacks.SheafOfModules.naiveCotangentComplexMapOfSquare.{u, u + 1, u, u}
        (smallEtaleRingedTopos B S hS U).J _ _ _ _ _ _
        (etaleSquareBaseRingIso B S hS h hq).hom
        (etaleInverseImageStructureSheafIso B S hS p hp).hom
        (etaleSquareBaseRingIso_fSharpInverseImage B S hS h hq)

AlgebraicGeometry.Space.naiveCotangentEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentEtaleRestriction.lean, line 184. The attribute's comment: “the canonical identification NL_{X/Y}|_{U_étale} = NL_{U/V}, as an isomorphism of complexes of sheaves of O_U-modules, of which the identification in D(O_U) is the image. The restriction is along the postcomposition functor U_étale ⥤ X_étale, i.e. p_small⁻¹ (Tag 03LQ), with O_X|_{U_étale} = O_U (Tag 03LV); formation of the naive cotangent complex commutes with it (Tag 08TZ for that functor), and the square of structure maps is identified through Tags 03LV and 03G8”.

Stacks 0D0W, as an isomorphism of complexes. For a commutative square p ≫ f = g ≫ q of algebraic spaces over S with p and q étale, the restriction to the small étale site of U of the naive cotangent complex of f is the naive cotangent complex of g:

NL_{X/Y}|_{U_étale} ≅ NL_{U/V},

as complexes of sheaves of 𝒪_U-modules. It is the restriction of scalars along 𝒪_U ≅ 𝒪_X|_{U_étale} of Stacks.SheafOfModules.restrictionNaiveCotangentComplexIso, which identifies NL_{X/Y}|_{U_étale} with the naive cotangent complex of (f⁻¹𝒪_Y)|_{U_étale} ⟶ 𝒪_X|_{U_étale}, followed by the inverse of the canonical chain map of Stacks 08TX attached to the square of sheaves of rings of AlgebraicGeometry.Space.etaleRestrictionNaiveBaseRingIso_fSharp.

noncomputable def naiveCotangentEtaleRestrictionIso {p : U ⟶ X} {f : X ⟶ Y} {g : U ⟶ V}
    {q : V ⟶ Y} (h : p ≫ f = g ≫ q) (hp : IsEtale B S hS p.hom) (hq : IsEtale B S hS q.hom) :
    ((etaleModuleRestriction B S hS p hp).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (naiveCotangentComplex B S hS f) ≅
      naiveCotangentComplex B S hS g

AlgebraicGeometry.Space.naiveCotangentEtaleRestrictionDerivedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentEtaleRestriction.lean, line 228. The attribute's comment: “the canonical identification NL_{X/Y}|_{U_étale} = NL_{U/V} in D(O_U) for a commutative square of algebraic spaces over S with p and q étale”.

Stacks 0D0W. For a commutative square p ≫ f = g ≫ q of algebraic spaces over S with p and q étale, there is a canonical identification

NL_{X/Y}|_{U_étale} = NL_{U/V} in D(𝒪_U):

the image in the derived category of sheaves of 𝒪_U-modules of the isomorphism of complexes AlgebraicGeometry.Space.naiveCotangentEtaleRestrictionIso.

noncomputable def naiveCotangentEtaleRestrictionDerivedIso {p : U ⟶ X} {f : X ⟶ Y} {g : U ⟶ V}
    {q : V ⟶ Y} (h : p ≫ f = g ≫ q) (hp : IsEtale B S hS p.hom) (hq : IsEtale B S hS q.hom)
    [HasDerivedCategory.{t} (_root_.SheafOfModules.{u + 1}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u} (smallEtaleRingedTopos B S hS U).O))] :
    DerivedCategory.Q.obj
        (((etaleModuleRestriction B S hS p hp).mapHomologicalComplex (ComplexShape.up ℤ)).obj
          (naiveCotangentComplex B S hS f)) ≅
      DerivedCategory.Q.obj (naiveCotangentComplex B S hS g)
Tag 0D0X, a lemma

Tag 0D0X in the Stacks Project.

AlgebraicGeometry.Space.representedNaiveCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentRepresentableComparison.lean, line 245. The attribute's comment: “the canonical map ε^*NL_{X₀/Y₀} ⟶ NL_{X/Y} of the source's proof, in its ε⁻¹-adjoint form, for the morphism of algebraic spaces represented by a morphism T₁ ⟶ T₂ of the big fppf site over S (so X, Y are represented by the schemes X₀, Y₀ underlying T₁, T₂); ε is the comparison of Section 071P (representedToZariskiRingedToposHom). WHAT IS PROVED IS THE SECOND STEP OF THE SOURCE'S PROOF: the canonical chain map of Tag 08TX attached to the square of Remark 08GH, representedBaseMap_square, from the naive cotangent complex of the inverse image along ε of the structure map of f₀. Its source is identified with ε⁻¹NL_{X₀/Y₀}, which is the source's FIRST step (Modules on Sites, Lemma 08TZ), separately by representedInverseImageNaiveCotangentComplexIso; the composite of the two is representedPulledBackNaiveCotangentComparison. THE SOURCE'S THIRD STEP IS NOT PROVED: the map is NOT shown to be an ISOMORPHISM; nothing is asserted in the derived category D(O_X). The source checks that on stalks at geometric points, where the stalk maps of ε and of representedBaseMap are strict henselizations (Tags 04K5, 04KF, 05V1) and the conclusion is More on Algebra, Lemma 0D08; NL has no fundamental triangle, so the two-vanishing-vertices factorisation that quasiIso_representedCotangentComparison uses for Tag 08VF is unavailable. Carried beyond the source's statement: sections are lifted to CommRingCat.{u + 1} throughout, which is the only universe at which ε exists, so both ends are the naive cotangent complexes of the lifted structure maps and NOT Space.naiveCotangentComplex of Tag 0D0V, whose sections are in CommRingCat.{u}; an NL analogue of Scheme.Hom.cotangentComplexULiftIso is the one remaining input needed to read this at Tag 0D0V. The target is read in complexes of ε⁻¹O_{X₀}-modules through restriction of scalars along ε♯, the adjoint form of a map out of ε^*NL_{X₀/Y₀}”.

The canonical chain map NL_{ε⁻¹𝒪_{X₀}/ε⁻¹f₀⁻¹𝒪_{Y₀}} ⟶ NL_{X/Y} of the proof of Stacks 0D0X. It is the map of Stacks 08TX attached to the square of sheaves of commutative rings on the small étale site of X 

ε⁻¹𝒪_{X₀} ─────ε♯────▸ 𝒪_X
    ▲                    ▲
    │                    │
ε⁻¹f₀⁻¹𝒪_{Y₀} ─────────▸ f_small⁻¹𝒪_Y
whose bottom arrow is AlgebraicGeometry.Space.representedBaseMap and whose commutativity is the square of Remark 08GH, AlgebraicGeometry.Space.representedBaseMap_square. The target is read in complexes of sheaves of ε⁻¹𝒪_{X₀}-modules through restriction of scalars along ε♯; this is the adjoint form of a map out of ε^*NL_{X₀/Y₀} = ε⁻¹NL_{X₀/Y₀} ⊗_{ε⁻¹𝒪_{X₀}} 𝒪_X.

noncomputable def representedNaiveCotangentComparison :
    representedInverseImageNaiveCotangentComplex B S hS h ⟶
      ((_root_.SheafOfModules.restrictScalars.{u + 1}
            (underlyingRingHomOfSite.{u, u + 1, u + 1}
              (representedToZariskiRingedToposHom B S hS T₁).fSharpInverseImage)
          ).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (representedNaiveCotangentComplexULift B S hS h)

AlgebraicGeometry.Space.representedPulledBackNaiveCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentRepresentableComparison.lean, line 316. The attribute's comment: “the canonical map ε^*NL_{X₀/Y₀} ⟶ NL_{X/Y} of the source's proof, in its ε⁻¹-adjoint form, for the morphism of algebraic spaces represented by a morphism T₁ ⟶ T₂ of the big fppf site over S (so X, Y are represented by the schemes X₀, Y₀ underlying T₁, T₂); ε is the comparison of Section 071P (representedToZariskiRingedToposHom). THE FIRST TWO STEPS OF THE SOURCE'S PROOF ARE WHAT IS PROVED: the identification ε⁻¹NL_{X₀/Y₀} = NL_{ε⁻¹O_{X₀}/ε⁻¹f₀⁻¹O_{Y₀}} of Modules on Sites, Lemma 08TZ, instantiated at ε (representedInverseImageNaiveCotangentComplexIso), and then the canonical chain map of Tag 08TX attached to the square of Remark 08GH, representedBaseMap_square (representedNaiveCotangentComparison). THE THIRD STEP IS NOT PROVED: this map is NOT shown to be an ISOMORPHISM, and nothing is asserted in the derived category D(O_X). The source checks that on stalks at geometric points, where the stalk maps of ε and of representedBaseMap are strict henselizations (Tags 04K5, 04KF, 05V1) and the conclusion is More on Algebra, Lemma 0D08; NL has no fundamental triangle, so the two-vanishing-vertices factorisation that quasiIso_representedCotangentComparison uses for Tag 08VF is unavailable. Carried beyond the source's statement: sections are lifted to CommRingCat.{u + 1} throughout, which is the only universe at which ε exists, so the two ends are the naive cotangent complexes of the lifted structure maps and NOT Space.naiveCotangentComplex of Tag 0D0V, whose sections are in CommRingCat.{u}, nor the scheme-level complex of Definition 0D0H at its own section universe; an NL analogue of Scheme.Hom.cotangentComplexULiftIso is the one remaining input needed to read this at Tag 0D0V. The target is read in complexes of ε⁻¹O_{X₀}-modules through restriction of scalars along ε♯, the adjoint form of a map out of ε^*NL_{X₀/Y₀}”.

The canonical map ε⁻¹NL_{X₀/Y₀} ⟶ NL_{X/Y} of the proof of Stacks 0D0X. The identification of Lemma 08TZ at ε (AlgebraicGeometry.Space.representedInverseImageNaiveCotangentComplexIso) followed by the canonical chain map of Stacks 08TX over the square of Remark 08GH (AlgebraicGeometry.Space.representedNaiveCotangentComparison). Read through restriction of scalars along ε♯, this is the adjoint form of the map ε^*NL_{X₀/Y₀} ⟶ NL_{X/Y} that Stacks 0D0X asserts to be an isomorphism.

noncomputable def representedPulledBackNaiveCotangentComparison :
    ((inverseImageTargetModules.{u + 1, u, u, u, u, u + 1}
          (SmallEtale.topology B S hS (yoneda.obj T₁))
          (Opens.grothendieckTopology ((BigFppfOver.toScheme B S hS).obj T₁))
          (representedToZariskiMorphismOfTopoi B S hS T₁)).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj (representedZariskiNaiveCotangentComplex B S hS h) ⟶
      ((_root_.SheafOfModules.restrictScalars.{u + 1}
            (underlyingRingHomOfSite.{u, u + 1, u + 1}
              (representedToZariskiRingedToposHom B S hS T₁).fSharpInverseImage)
          ).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (representedNaiveCotangentComplexULift B S hS h)

AlgebraicGeometry.Space.quasiIso_representableEpsilonNaiveCotangentIdentification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableNaiveCotangentIdentification.lean, line 262. The attribute's comment: “the canonical map ε^*NL_{X₀/Y₀} ⟶ NL_{X/Y} is a quasi-isomorphism, i.e. the canonical identification NL_{X/Y} = ε^*NL_{X₀/Y₀} in D(O_X), for an arbitrary morphism f : X ⟶ Y of algebraic spaces with X ≅ h_U, Y ≅ h_V representable by schemes, NL_{X/Y} read on the small étale site of X₀ through the identification (X₀)_étale ≌ X_étale that the representing isomorphism gives”.

Stacks 0D0X. Let f : X ⟶ Y be a morphism of algebraic spaces over S with X and Y representable by schemes X₀ and Y₀, through α : h_U ≅ X and β : h_V ≅ Y for objects U, V of the big fppf site of S with underlying schemes X₀, Y₀, and let f₀ : X₀ ⟶ Y₀ be the morphism of schemes corresponding to f (AlgebraicGeometry.Space.representingMorphism). Let ε : ((X₀)_étale, 𝒪) ⟶ ((X₀)_Zar, 𝒪_{X₀}) be the comparison morphism of Stacks 08H7. Then the canonical map

ε^*NL_{X₀/Y₀} ⟶ NL_{X/Y}

— the termwise pullback along ε of (the universe lift of) NL_{X₀/Y₀} of Stacks 0D0H, followed by the map of Stacks 08TX of the square of Stacks 08GH into NL_{h_U/h_V}, followed by the identification of NL_{h_U/h_V} with NL_{X/Y} of Stacks 0D0V read on (X₀)_étale through the identification (X₀)_étale ≌ X_étale given by α (AlgebraicGeometry.Space.representingNaiveCotangentComplexIso) — is a quasi-isomorphism, so it identifies NL_{X/Y} with ε^*NL_{X₀/Y₀} in D(𝒪_X).

theorem quasiIso_representableEpsilonNaiveCotangentIdentification (f : X ⟶ Y) :
    QuasiIso ((((representedEpsilonModulePullback B S hS U).mapHomologicalComplex
        (ComplexShape.up ℤ)).map (representedZariskiNaiveCotangentComplexIso B S hS
          (representingMorphism B S hS α β f)).inv ≫
      representedEpsilonNaiveCotangentMap B S hS (representingMorphism B S hS α β f)) ≫
        (representingNaiveCotangentComplexIso B S hS α β
          (comp_eq_representedSpaceMap_representingMorphism B S hS α β f)).hom)
Tag 0D0Y, a lemma

Tag 0D0Y in the Stacks Project.

AlgebraicGeometry.Space.naiveCotangentComplex_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentHomologyQuasicoherent.lean, line 113.

Stacks 0D0Y. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S. The cohomology sheaves of the naive cotangent complex NL_{X/Y} are quasi-coherent, zero outside degrees -1 and 0, and equal to Ω_{X/Y} in degree 0.

Ω_{X/Y} is the sheaf of differentials of Stacks 04CT, with its sections lifted to the universe of the sections of NL_{X/Y}; see the implementation notes.

theorem naiveCotangentComplex_homology :
    (∀ i : ℤ, ((naiveCotangentComplex B S hS f).homology i).IsQuasicoherentOnSite) ∧
      (∀ i : ℤ, i ≠ -1 → i ≠ 0 → IsZero ((naiveCotangentComplex B S hS f).homology i)) ∧
      Nonempty ((naiveCotangentComplex B S hS f).homology 0 ≅
        SheafOfModules.uliftForPresentation.{u + 1, u, u, u, u + 1}
          (sheafOfDifferentials B S hS f))
Tag 0D0Z, a lemma

Tag 0D0Z in the Stacks Project.

AlgebraicGeometry.Space.exists_quasiIso_naiveCotangentComplex_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentEtaleLocalFinitePresentation.lean, line 311. The attribute's comment: “the whole statement. etale locally on X is read on the small etale site of X: every etale chart U of X has an etale covering {W_i -> U} (a covering sieve of SmallEtale.topology) such that NL_{X/Y} restricted to the slice at each W_i receives a quasi-isomorphism from a complex F concentrated in degrees -1 and 0 with F^0 quasi-coherent and of finite presentation and F^{-1} quasi-coherent and of finite type -- the two degrees carrying DIFFERENT finiteness conditions, exactly as the tag states. The source's NL_{X/Y} is quasi-isomorphic to F is realized by a quasi-isomorphism FROM F, which is the same content. The only hypothesis is the source's: f locally of finite presentation (IsLocallyOfFinitePresentation, Stacks 03XP). Nothing is assumed: the covering is by the affine chart diagrams, on which F = NL(P) (x)_A O for a finite presentation P of the chart ring A over R, the comparison with (NL_{A/R}) (x)_A O is the Stacks 00S1 homotopy equivalence, and (NL_{A/R}) (x)_A O -> NL_{X/Y}|_V is proved to be a quasi-isomorphism on kernels (H^{-1} = H_1(L_{A/R}) (x)_A O, using flatness of the etale stalks) and on cokernels (Omega_{X/Y}|_V = Omega_{A/R} (x)_A O, Stacks 0D08 in degree 0 and Stacks 08TP)”.

Stacks 0D0Z. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation. Then NL_{X/Y} is étale locally on X quasi-isomorphic to a complex … → 0 → 𝓕⁻¹ → 𝓕⁰ → 0 → … of quasi-coherent 𝒪_X-modules with 𝓕⁰ of finite presentation and 𝓕⁻¹ of finite type.

"Étale locally on X" is read as on the small étale site of X: every étale scheme chart U of X has an étale covering {Wᵢ ⟶ U} such that the restriction of NL_{X/Y} to the small étale site of X localized at each Wᵢ receives a quasi-isomorphism φ from a complex F of sheaves of modules over the restricted structure sheaf which vanishes outside degrees -1 and 0, whose degree 0 term is quasi-coherent and of finite presentation and whose degree -1 term is quasi-coherent and of finite type. NL_{X/Y} is AlgebraicGeometry.Space.naiveCotangentComplex (Stacks 0D0V) and the restriction is SheafOfModules.overFunctor applied termwise.

theorem exists_quasiIso_naiveCotangentComplex_of_isLocallyOfFinitePresentation
    (hf : IsLocallyOfFinitePresentation B S hS f.hom) (U : SmallEtale B S hS X.1) :
    ∃ (I : Type (u + 1)) (W : I → SmallEtale B S hS X.1) (g : ∀ i, W i ⟶ U),
      Sieve.ofArrows W g ∈ SmallEtale.topology B S hS X.1 U ∧
      ∀ i, ∃ (F : CochainComplex (_root_.SheafOfModules.{u + 1}
          ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedTopos B S hS X).O).over
            (W i))) ℤ)
        (φ : F ⟶ ((_root_.SheafOfModules.overFunctor.{u + 1}
            (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedTopos B S hS X).O)
              (W i)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
          (naiveCotangentComplex B S hS f)),
        (∀ j : ℤ, j ≠ -1 → j ≠ 0 → IsZero (F.X j)) ∧ QuasiIso φ ∧
          (F.X 0).IsQuasicoherentOnSite ∧ (F.X 0).IsFinitePresentationOnSite ∧
          (F.X (-1)).IsQuasicoherentOnSite ∧ (F.X (-1)).IsFiniteTypeOnSite
Tag 0D10, a lemma

Tag 0D10 in the Stacks Project.

AlgebraicGeometry.Space.formallySmooth_iff_isZero_homology_negOne_and_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentFormallySmooth.lean, line 134. The attribute's comment: “the second condition read on the sheaf of differentials Ω_{X/Y} of 04CT, which the source identifies with H⁰(NL_{X/Y}) (0D0Y)”.

Stacks 0D10. A morphism f : X ⟶ Y of algebraic spaces over a scheme S is formally smooth if and only if the cohomology sheaf H⁻¹(NL_{X/Y}) of its naive cotangent complex vanishes and its sheaf of differentials Ω_{X/Y} = H⁰(NL_{X/Y}) is locally projective.

Ω_{X/Y} is the degree-zero cohomology sheaf of NL_{X/Y} by Stacks 0D0Y, AlgebraicGeometry.Space.naiveCotangentComplexHomologyZeroIsoSheafOfDifferentials, and is quasi-coherent by Stacks 04CV, which is the standing hypothesis of local projectivity (Stacks 060R).

theorem formallySmooth_iff_isZero_homology_negOne_and_isLocallyProjective
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    FormallySmooth f.hom ↔
      (IsZero ((naiveCotangentComplex B S hS f).homology (-1)) ∧
        IsLocallyProjective B S hS X.2
          ⟨sheafOfDifferentials B S hS f,
            isQuasicoherentOnSite_sheafOfDifferentials B S hS f⟩)
Tag 0D11, a lemma

Tag 0D11 in the Stacks Project.

Declarations registered for the tag:

Tag 0D12, a lemma

Tag 0D12 in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_iff_isZero_homology_negOne_and_isFiniteLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NaiveCotangentSmoothCriterion.lean, line 81. The attribute's comment: “the third clause read on the sheaf of differentials Ω_{X/Y} of 04CT, which the source identifies with H⁰(NL_{X/Y})”.

Stacks 0D12. A morphism f : X ⟶ Y of algebraic spaces over a scheme S is smooth if and only if it is locally of finite presentation, the cohomology sheaf H⁻¹(NL_{X/Y}) of its naive cotangent complex vanishes, and its sheaf of differentials Ω_{X/Y} = H⁰(NL_{X/Y}) is finite locally free on the small étale site of X.

theorem isSmooth_iff_isZero_homology_negOne_and_isFiniteLocallyFreeOnSite
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    IsSmooth B S hS f.hom ↔
      (IsLocallyOfFinitePresentation B S hS f.hom ∧
        IsZero ((naiveCotangentComplex B S hS f).homology (-1)) ∧
        SheafOfModules.IsFiniteLocallyFreeOnSite (sheafOfDifferentials B S hS f))

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Space.naiveCotangentComplex · AlgebraicGeometry.Space.naiveCotangentEtaleLocalisationIso · AlgebraicGeometry.Space.naiveCotangentEtaleLocalisationIso_hom · AlgebraicGeometry.Space.naiveCotangentEtaleRestrictionIso · AlgebraicGeometry.Space.naiveCotangentEtaleRestrictionDerivedIso · AlgebraicGeometry.Space.representedNaiveCotangentComparison · AlgebraicGeometry.Space.representedPulledBackNaiveCotangentComparison · AlgebraicGeometry.Space.quasiIso_representableEpsilonNaiveCotangentIdentification

Section76.22 Openness of the flat locus#

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

Tag 05WV, a theorem

Tag 05WV in the Stacks Project.

AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusOpen.lean, line 105. The attribute's comment: “openness of the flat locus; quasi-coherence and finite presentation of the module are read on the Zariski site of every etale scheme chart”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation and let F be an 𝒪_X-module which is quasi-coherent of finite presentation on charts. The set of points of |X| at which F is flat over Y is open.

theorem isOpen_flatLocus_of_isFinitePresentationOnCharts (hX : IsAlgebraicSpace B S hS X)
    (f : X ⟶ Y) (F : Modules.{u, u} B S hS X hX)
    (hf : IsLocallyOfFinitePresentation B S hS f)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hfp : IsFinitePresentationOnCharts B S hS hX F) :
    IsOpen (flatLocus B S hS hX f F)

AlgebraicGeometry.Space.isOpen_setOf_forall_isFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusOpen.lean, line 176. The attribute's comment: “openness of the flat locus, read through condition (2) of Stacks 05VU; finite presentation of the module is read on the Zariski site of every etale scheme chart”.

For a morphism of algebraic spaces locally of finite presentation and a quasi-coherent module which is of finite presentation on charts, the set of points of the source over which the geometric stalks of the module are flat over the étale local rings of the target is open.

theorem isOpen_setOf_forall_isFlatOverAtGeometricPoint (f : Xs ⟶ Ys)
    (F : Modules.{u, u} B S hS Xs.1 Xs.2) [F.IsQuasicoherentOnSite]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS Xs.2 F) :
    IsOpen {x : points B S hS Xs.1 | ∀ xbar : GeometricPoint B S hS Xs.1,
      xbar.image = x → IsFlatOverAtGeometricPoint B S hS f F xbar}
Tag 05WW, a lemma

Tag 05WW in the Stacks Project.

AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusBaseChange.lean, line 161. The attribute's comment: “the set equality, with Stacks 05VW at a point carried as the hypothesis h05VW; the finite-presentation hypotheses of the source are not needed for it and enter through Stacks 05WV in flatLocus_modulePullback_eq_preimage_and_isOpen”.

Stacks 05WW, the set equality. In a cartesian square of algebraic spaces over S with f : X ⟶ Y, g : Y' ⟶ Y, f' : X' ⟶ Y' and g' : X' ⟶ X whose base morphism g is flat, the locus of points of |X'| at which the inverse image (g')^*F of a quasi-coherent 𝒪_X-module is flat over Y' is the inverse image under |g'| : |X'| ⟶ |X| of the locus of points of |X| at which F is flat over Y.

Both inclusions are the two implications of Stacks 05VW at a point, carried as h05VW: the inclusion ⊆ is its second implication, flatness of g being read pointwise by Stacks 03MM (AlgebraicGeometry.Space.isFlat_iff_forall_isFlatAt), and the inclusion ⊇ is its first. The finite-presentation hypotheses of Stacks 05WW are not needed for the equality; they are what makes the right-hand side open, by Stacks 05WV, and are carried by AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_and_isOpen.

theorem flatLocus_modulePullback_eq_preimage
    (h05VW : IsFlatAtPointStableUnderBaseChange B S hS) {f : X ⟶ Y} {g : Y' ⟶ Y} {f' : X' ⟶ Y'}
    {g' : X' ⟶ X} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hqc : IsQuasicoherentOnCharts B S hS X.2 F)
    (hg : IsFlat B S hS g.hom) :
    flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' flatLocus B S hS X.2 f.hom F

AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_and_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusBaseChange.lean, line 187. The attribute's comment: “the locus on the base change is the inverse image of the open subset of Stacks 05WV, hence open; Stacks 05VW at a point is carried as the hypothesis h05VW”.

Stacks 05WW. Let a cartesian square of algebraic spaces over S be given, with f : X ⟶ Y, g : Y' ⟶ Y, f' : X' ⟶ Y' and g' : X' ⟶ X. Assume g is flat, f is locally of finite presentation, and the 𝒪_X-module F is quasi-coherent of finite presentation on the étale scheme charts. Then the locus of points of |X'| at which the inverse image (g')^*F is flat over Y' is the inverse image under |g'| : |X'| ⟶ |X| of the open subset of Stacks 05WV, and is therefore itself open.

The equality is AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage, which is where the carried Stacks 05VW and the flatness of g are used. Openness of the subset of |X| is Stacks 05WV, AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnCharts, which is where the two finite-presentation hypotheses are used, and the map on points is continuous by clause (2) of Stacks 03BX.

theorem flatLocus_modulePullback_eq_preimage_and_isOpen
    (h05VW : IsFlatAtPointStableUnderBaseChange B S hS) {f : X ⟶ Y} {g : Y' ⟶ Y} {f' : X' ⟶ Y'}
    {g' : X' ⟶ X} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hg : IsFlat B S hS g.hom)
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hqc : IsQuasicoherentOnCharts B S hS X.2 F)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F) :
    flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) =
        pointsMap B S hS X'.1 g'.hom ⁻¹' flatLocus B S hS X.2 f.hom F ∧
      IsOpen (flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F))

AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_of_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusBaseChangeFinitePresentation.lean, line 73. The attribute's comment: “the set equality; the finite-presentation hypotheses of the source enter through Stacks 05WV in flatLocus_modulePullback_eq_preimage_and_isOpen_of_isFinitePresentationOnSite”.

Stacks 05WW, the set equality, with no hypothesis beyond the source's own. In a cartesian square of algebraic spaces over S with f : X ⟶ Y, g : Y' ⟶ Y, f' : X' ⟶ Y' and g' : X' ⟶ X whose base morphism g is flat, the locus of points of |X'| at which the inverse image (g')^*F of an 𝒪_X-module of finite presentation on the small étale site is flat over Y' is the inverse image under |g'| : |X'| ⟶ |X| of the locus of points of |X| at which F is flat over Y.

Both inclusions are the two implications of Stacks 05VW, read at a geometric representative of the point: the inclusion ⊆ is AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_modulePullback, flatness of g being read pointwise by Stacks 03MM (AlgebraicGeometry.Space.isFlat_iff_forall_isFlatAt), and the inclusion ⊇ is AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_modulePullback. So nothing is carried here: AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage states the same equality for a module which is quasi-coherent only on the charts, and has to carry Stacks 05VW as a hypothesis because the comparison with geometric points is unavailable at that reading.

Finite presentation of f is not needed for the equality, and finite presentation of F enters only as the quasi-coherence of F and of its inverse image under which flatness at a point of |X| agrees with flatness at a geometric point above it; the finite-presentation hypotheses of Stacks 05WW are what makes the right-hand side open, by Stacks 05WV, and are carried by flatLocus_modulePullback_eq_preimage_and_isOpen_of_isFinitePresentationOnSite.

theorem flatLocus_modulePullback_eq_preimage_of_isFinitePresentationOnSite
    {f : X ⟶ Y} {g : Y' ⟶ Y} {f' : X' ⟶ Y'}
    {g' : X' ⟶ X} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : SheafOfModules.IsFinitePresentationOnSite F)
    (hg : IsFlat B S hS g.hom) :
    flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' flatLocus B S hS X.2 f.hom F

AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_and_isOpen_of_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusBaseChangeFinitePresentation.lean, line 113. The attribute's comment: “the locus on the base change is the inverse image of the open subset of Stacks 05WV, hence open”.

Stacks 05WW, with no hypothesis beyond the source's own. Let a cartesian square of algebraic spaces over S be given, with f : X ⟶ Y, g : Y' ⟶ Y, f' : X' ⟶ Y' and g' : X' ⟶ X. Assume g is flat, f is locally of finite presentation, and the 𝒪_X-module F is of finite presentation on the small étale site. Then the locus of points of |X'| at which the inverse image (g')^*F is flat over Y' is the inverse image under |g'| : |X'| ⟶ |X| of the open subset of Stacks 05WV, and is therefore itself open.

The equality is AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_of_isFinitePresentationOnSite, which is where Stacks 05VW and the flatness of g are used. Openness of the subset of |X| is Stacks 05WV, AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnCharts, whose chartwise hypotheses on F are supplied by the finite presentation of F on the site, and the map on points is continuous by clause (2) of Stacks 03BX.

theorem flatLocus_modulePullback_eq_preimage_and_isOpen_of_isFinitePresentationOnSite
    {f : X ⟶ Y} {g : Y' ⟶ Y} {f' : X' ⟶ Y'}
    {g' : X' ⟶ X} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hg : IsFlat B S hS g.hom)
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hF : SheafOfModules.IsFinitePresentationOnSite F) :
    flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) =
        pointsMap B S hS X'.1 g'.hom ⁻¹' flatLocus B S hS X.2 f.hom F ∧
      IsOpen (flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F))
Sources
LeanAlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnCharts · AlgebraicGeometry.Space.isOpen_setOf_forall_isFlatOverAtGeometricPoint · AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage · AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_and_isOpen · AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_of_isFinitePresentationOnSite · AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_and_isOpen_of_isFinitePresentationOnSite

Section76.23 Critère de platitude par fibres#

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

Tag 05WY, a lemma

Tag 05WY in the Stacks Project.

AlgebraicGeometry.Space.exists_chartPoint_isFibreFlatOnChartSquares_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessChartPoint.lean, line 211. The attribute's comment: “(1) iff (3), with condition (3) carrying a point u of U above x as the source states it rather than a lift of the geometric point; condition (3) read on the local rings of the charts”.

Stacks 05WY: condition (3) if and only if condition (1), with condition (3) carrying a point of U above x. In Situation 05WX the following are equivalent, for a geometric point x̄ of X:

  1. writing ȳ = f ∘ x̄ and z̄ = h ∘ ȳ, the fibre F_x̄ / 𝔪_z̄ F_x̄ is flat over 𝒪_{Y, ȳ} / 𝔪_z̄ 𝒪_{Y, ȳ};
  2. there is a commuting diagram of schemes U ⟶ V ⟶ W étale over f and h, and a point u of U mapping to the image of x̄ in |X|, at which the fibre of F|_U over the fibre of V is flat.

This is condition (3) as the source states it: the source picks a diagram and a point u ∈ U mapping to x, with no lift of the geometric point chosen. AlgebraicGeometry.Space.exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint is the same equivalence with the point presented as a lift of x̄ to the chart.

Condition (3) is read on the local rings of the charts rather than on the scheme-theoretic fibres U_w and V_w, through the canonical identifications 𝒪_{V_w, v} = 𝒪_{V, v}/𝔪_w 𝒪_{V, v} and (F_w)_u = (F|_U)_u/𝔪_w (F|_U)_u which the source records at the start of its proof.

theorem exists_chartPoint_isFibreFlatOnChartSquares_iff_isFibreFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (xbar : GeometricPoint B S hS X.1) :
    (∃ (U : SmallEtale B S hS X.1) (Vc : SmallEtale B S hS Y.1) (Wc : SmallEtale B S hS Z.1)
        (g₁ : U.obj.left ⟶ Vc.obj.left)
        (_hcomm₁ : U.obj.hom ≫ f.hom = yoneda.map g₁ ≫ Vc.obj.hom)
        (g₂ : Vc.obj.left ⟶ Wc.obj.left)
        (_hcomm₂ : Vc.obj.hom ≫ h.hom = yoneda.map g₂ ≫ Wc.obj.hom)
        (u : chartScheme U),
      ChartPoint B S hS U.obj.left U.obj.hom u xbar.image ∧
        IsFibreFlatOnChartSquares B S hS X.1 X.2 F U Vc Wc g₁ g₂ u) ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar

AlgebraicGeometry.Space.isFibreFlatOverAtGeometricPoint_congr_of_image_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessChartPoint.lean, line 243. The attribute's comment: “well-posedness of 'pick a geometric point xbar of X lying over x' in condition (1): the condition at a geometric point depends only on its image in |X|”.

The condition of Stacks 05WY at a geometric point depends only on the point of |X| it lies over. For two geometric points x̄, x̄' of X with the same image in |X|, condition (1) of Stacks 05WY holds at x̄ exactly when it holds at x̄'.

theorem isFibreFlatOverAtGeometricPoint_congr_of_image_eq {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (h : Y ⟶ Z) (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (xbar xbar' : GeometricPoint B S hS X.1) (himage : xbar.image = xbar'.image) :
    IsFibreFlatOverAtGeometricPoint B S hS f h F xbar ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar'

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldFibre.lean, line 477. The attribute's comment: “(1) iff (2): flatness of the pullback of F to the field fibre X_z over Y_z at a geometric point of X_z, read at a geometric point as in Stacks 05VU, iff condition (1) at the image of that point in X”.

Stacks 05WY: condition (2) if and only if condition (1). In Situation 05WX let z be a field-valued point of Z with field of definition K, let X_z = Spec(K) ×_{z, Z} X and Y_z = Spec(K) ×_{z, Z} Y be the field fibres and let F_z be the pullback of F to X_z. Then for a geometric point x̄_z of X_z, the module F_z is flat over Y_z at x̄_z exactly when condition (1) of Stacks 05WY holds at the image x̄ of x̄_z in X.

This is condition (2) of the source. Relative flatness at a point is read at a geometric point, as condition (2) of Stacks 05VU (AlgebraicGeometry.Space.isFlatOverAt_exists_chartDiagram_iff_isFlatOverAtGeometricPoint identifies that with the chartwise condition of Definition 05VV which the source cites), and the statement is at every geometric point of X_z rather than only at one above the K-rational point x of X_z that the source's representative x : Spec(K) ⟶ X defines — which is the source's condition (2) together with its independence of the choice of representative, since condition (1) at the image of x̄_z depends only on that image (AlgebraicGeometry.Space.isFibreFlatOverAtGeometricPoint_congr_of_image_eq).

theorem isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) (z : FieldValuedPoint B S hS Z.1)
    (xz : GeometricPoint B S hS (fieldFibreSpace (f ≫ h) z).1) :
    IsFlatOverAtGeometricPoint B S hS
        (ObjectProperty.homMk (fieldFibreSourceMap B S hS f.hom h.hom z) :
          fieldFibreSpace (f ≫ h) z ⟶ fieldFibreSpace h z)
        ((modulePullback B S hS (ObjectProperty.homMk
            (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
              fieldFibreSpace (f ≫ h) z ⟶ X)).obj F) xz ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F
        (geometricPointMap (ObjectProperty.homMk
          (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
            fieldFibreSpace (f ≫ h) z ⟶ X).hom xz)

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint_of_image_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldFibre.lean, line 505. The attribute's comment: “(1) iff (2) with condition (1) at an arbitrary chosen geometric point of X above the point, as the source states condition (1)”.

Stacks 05WY, condition (2) against condition (1) at a chosen geometric point of X. Condition (2) at a geometric point x̄_z of the field fibre X_z holds exactly when condition (1) holds at any geometric point x̄ of X with the same image in |X| as the image of x̄_z.

This is the form the source's condition (1) takes: "pick a geometric point x̄ of X lying over x".

theorem isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint_of_image_eq
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (z : FieldValuedPoint B S hS Z.1)
    (xz : GeometricPoint B S hS (fieldFibreSpace (f ≫ h) z).1)
    (xbar : GeometricPoint B S hS X.1)
    (himage : (geometricPointMap (ObjectProperty.homMk
        (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
          fieldFibreSpace (f ≫ h) z ⟶ X).hom xz).image = xbar.image) :
    IsFlatOverAtGeometricPoint B S hS
        (ObjectProperty.homMk (fieldFibreSourceMap B S hS f.hom h.hom z) :
          fieldFibreSpace (f ≫ h) z ⟶ fieldFibreSpace h z)
        ((modulePullback B S hS (ObjectProperty.homMk
            (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
              fieldFibreSpace (f ≫ h) z ⟶ X)).obj F) xz ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar

AlgebraicGeometry.Space.isFlatOverAtPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldFibre.lean, line 534. The attribute's comment: “(1) iff (2) with condition (2) in the chartwise form of Definition 05VV, which is the predicate the source cites”.

Stacks 05WY: condition (2) in the chartwise form of Definition 05VV, if and only if condition (1). The pullback F_z of F to the field fibre X_z is flat at the image in |X_z| of a geometric point x̄_z, over Y_z, in the sense of Definition 05VV, exactly when condition (1) of Stacks 05WY holds at the image of x̄_z in X.

This is condition (2) with flatness at a point spelled by AlgebraicGeometry.Space.IsFlatOverAtPoint, the predicate of Definition 05VV that the source cites, rather than at a geometric point.

theorem isFlatOverAtPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (z : FieldValuedPoint B S hS Z.1)
    (xz : GeometricPoint B S hS (fieldFibreSpace (f ≫ h) z).1) :
    IsFlatOverAtPoint B S hS (fieldFibreSpace (f ≫ h) z).2
        (ObjectProperty.homMk (fieldFibreSourceMap B S hS f.hom h.hom z) :
          fieldFibreSpace (f ≫ h) z ⟶ fieldFibreSpace h z).hom
        ((modulePullback B S hS (ObjectProperty.homMk
            (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
              fieldFibreSpace (f ≫ h) z ⟶ X)).obj F) xz.image ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F
        (geometricPointMap (ObjectProperty.homMk
          (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
            fieldFibreSpace (f ≫ h) z ⟶ X).hom xz)

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_exists_chartPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldFibre.lean, line 564. The attribute's comment: “(2) iff (3), composed through condition (1); condition (3) carrying a point u of U above x as the source states it, read on the local rings of the charts”.

Stacks 05WY: condition (2) if and only if condition (3). In Situation 05WX, flatness of the pullback F_z over Y_z at a geometric point x̄_z of the field fibre X_z holds exactly when there is a commuting diagram of schemes U ⟶ V ⟶ W étale over f and h and a point u of U above the image of x̄_z in |X|, at which the fibre of F|_U over the fibre of V is flat.

theorem isFlatOverAtGeometricPoint_fieldFibreSpace_iff_exists_chartPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (z : FieldValuedPoint B S hS Z.1)
    (xz : GeometricPoint B S hS (fieldFibreSpace (f ≫ h) z).1) :
    IsFlatOverAtGeometricPoint B S hS
        (ObjectProperty.homMk (fieldFibreSourceMap B S hS f.hom h.hom z) :
          fieldFibreSpace (f ≫ h) z ⟶ fieldFibreSpace h z)
        ((modulePullback B S hS (ObjectProperty.homMk
            (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
              fieldFibreSpace (f ≫ h) z ⟶ X)).obj F) xz ↔
      ∃ (U : SmallEtale B S hS X.1) (Vc : SmallEtale B S hS Y.1) (Wc : SmallEtale B S hS Z.1)
          (g₁ : U.obj.left ⟶ Vc.obj.left)
          (_hcomm₁ : U.obj.hom ≫ f.hom = yoneda.map g₁ ≫ Vc.obj.hom)
          (g₂ : Vc.obj.left ⟶ Wc.obj.left)
          (_hcomm₂ : Vc.obj.hom ≫ h.hom = yoneda.map g₂ ≫ Wc.obj.hom)
          (u : chartScheme U),
        ChartPoint B S hS U.obj.left U.obj.hom u
            (geometricPointMap (ObjectProperty.homMk
              (pullback.fst (f.hom ≫ h.hom) (yonedaEquiv.symm z.value)) :
                fieldFibreSpace (f ≫ h) z ⟶ X).hom xz).image ∧
          IsFibreFlatOnChartSquares B S hS X.1 X.2 F U Vc Wc g₁ g₂ u

AlgebraicGeometry.Space.isFlatOnFibreAtFieldValuedPoint_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldValuedPoint.lean, line 703. The attribute's comment: “(1) iff (2), for every geometric point over x and every field-valued representative of x”.

Stacks 05WY, (1) ⟺ (2). Let f : X ⟶ Y and h : Y ⟶ Z be morphisms of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let x be a point of |X|. For every geometric point x̄ of X lying over x and every field-valued point x : Spec(K) ⟶ X in the class of x, with z = h ∘ f ∘ x, the following are equivalent:

  1. the module F_{x̄}/𝔪_{z̄} F_{x̄} is flat over 𝒪_{Y, ȳ}/𝔪_{z̄} 𝒪_{Y, ȳ}, where ȳ = f ∘ x̄ and z̄ = h ∘ ȳ;
  2. the pullback F_z of F to X_z = Spec(K) ×_{z, Z} X is flat over Y_z = Spec(K) ×_{z, Z} Y at the K-rational point of X_z determined by x, in the sense of Stacks 05VV.

In particular neither condition depends on the choices made.

theorem isFlatOnFibreAtFieldValuedPoint_iff_isFibreFlatOverAtGeometricPoint
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1)
    (xbar : GeometricPoint B S hS X.1) (hxbar : xbar.LiesOver x)
    (hp : p.class B S hS X.1 = x) :
    IsFlatOnFibreAtFieldValuedPoint B S hS f h p F ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar

AlgebraicGeometry.Space.exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessGeometricPoint.lean, line 638. The attribute's comment: “(1) iff (3), condition (3) read on the local rings of the charts”.

Stacks 05WY: condition (3) if and only if condition (1). In Situation 05WX — a scheme S, algebraic spaces X, Y, Z over S with f : X ⟶ Y and h : Y ⟶ Z, a quasi-coherent 𝒪_X-module F and a geometric point x̄ of X — the following are equivalent:

  1. writing ȳ = f ∘ x̄ and z̄ = h ∘ ȳ, the fibre F_x̄ / 𝔪_z̄ F_x̄ is flat over 𝒪_{Y, ȳ} / 𝔪_z̄ 𝒪_{Y, ȳ};
  2. there is a commuting diagram of schemes U ⟶ V ⟶ W étale over f and h, and a point u of U above the image of x̄, at which the fibre of F|_U over the fibre of V is flat.

Condition (3) of the source reads the second condition on the scheme-theoretic fibres U_w and V_w; here it is read on their local rings, through the canonical identifications 𝒪_{V_w, v} = 𝒪_{V, v}/𝔪_w 𝒪_{V, v} and (F_w)_u = (F|_U)_u/𝔪_w (F|_U)_u which the source records at the start of its proof. The point u above x̄ is presented as a lift of x̄ to the chart, which is the same data by Stacks 05VN (AlgebraicGeometry.Space.exists_chartLift_of_chartPoint and AlgebraicGeometry.Space.chartPoint_isChartPoint).

Condition (2) of the source, flatness of the pullback of F to the fibre X_z over Y_z in the sense of Stacks 05VV, is not among the conditions compared here; it is Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint of StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessFieldFibre.lean, and AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_exists_chartPoint composes it with this lemma.

Such a diagram always exists (AlgebraicGeometry.Space.exists_chartSquares), which is what the second direction uses: take W ⟶ Z surjective étale, then V ⟶ W ×_Z Y and U ⟶ V ×_Y X surjective étale, and a point of U above the image of x̄. Since no diagram is privileged, condition (3) in fact holds at every diagram as soon as it holds at one, which is AlgebraicGeometry.Space.forall_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint.

theorem exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (xbar : GeometricPoint B S hS X.1) :
    (∃ (N : SmallEtaleNeighborhood xbar) (Vc : SmallEtale B S hS Y.1)
        (g₁ : N.chart.obj.left ⟶ Vc.obj.left)
        (hcomm₁ : N.chart.obj.hom ≫ f.hom = yoneda.map g₁ ≫ Vc.obj.hom)
        (Wc : SmallEtale B S hS Z.1) (g₂ : Vc.obj.left ⟶ Wc.obj.left)
        (hcomm₂ : Vc.obj.hom ≫ h.hom = yoneda.map g₂ ≫ Wc.obj.hom),
      Module.FlatQuotSMul
        (((BigFppfOver.toScheme B S hS).map g₁).stalkMap (chartPoint B S hS X.1 N)).hom
        ((maximalIdeal ↥(chartLocalRing B S hS Z.1 (targetNeighborhood B S hS
              (targetNeighborhood B S hS N Vc g₁ hcomm₁) Wc g₂ hcomm₂))).map
          (((BigFppfOver.toScheme B S hS).map g₂).stalkMap
            (chartPoint B S hS Y.1 (targetNeighborhood B S hS N Vc g₁ hcomm₁))).hom)
        (((maximalIdeal ↥(chartLocalRing B S hS Z.1 (targetNeighborhood B S hS
                (targetNeighborhood B S hS N Vc g₁ hcomm₁) Wc g₂ hcomm₂))).map
            (((BigFppfOver.toScheme B S hS).map g₂).stalkMap
              (chartPoint B S hS Y.1 (targetNeighborhood B S hS N Vc g₁ hcomm₁))).hom).map
          (((BigFppfOver.toScheme B S hS).map g₁).stalkMap (chartPoint B S hS X.1 N)).hom)
        rfl ↥(chartZariskiModuleStalk B S hS X.1 X.2 N F)) ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar

AlgebraicGeometry.Space.forall_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessGeometricPoint.lean, line 682. The attribute's comment: “(1) iff (3) at an arbitrary chosen diagram: the every-diagram reading of condition (3), read on the local rings of the charts”.

Stacks 05WY: condition (3) at an arbitrary chosen diagram if and only if condition (1). In Situation 05WX the chart condition (3) of Stacks 05WY holds on every pointed pair of composable commuting squares of étale scheme charts U ⟶ V ⟶ W of f and h exactly when condition (1) holds at x̄.

This is the "any choice works" reading of condition (3) the source intends: the source says "choose a commutative diagram", so the condition must not depend on the choice. Together with AlgebraicGeometry.Space.exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint it says that the some-diagram and every-diagram readings of condition (3) agree, a diagram existing by AlgebraicGeometry.Space.exists_chartSquares.

theorem forall_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (xbar : GeometricPoint B S hS X.1) :
    (∀ (N : SmallEtaleNeighborhood xbar) (Vc : SmallEtale B S hS Y.1)
        (g₁ : N.chart.obj.left ⟶ Vc.obj.left)
        (hcomm₁ : N.chart.obj.hom ≫ f.hom = yoneda.map g₁ ≫ Vc.obj.hom)
        (Wc : SmallEtale B S hS Z.1) (g₂ : Vc.obj.left ⟶ Wc.obj.left)
        (hcomm₂ : Vc.obj.hom ≫ h.hom = yoneda.map g₂ ≫ Wc.obj.hom),
      Module.FlatQuotSMul
        (((BigFppfOver.toScheme B S hS).map g₁).stalkMap (chartPoint B S hS X.1 N)).hom
        ((maximalIdeal ↥(chartLocalRing B S hS Z.1 (targetNeighborhood B S hS
              (targetNeighborhood B S hS N Vc g₁ hcomm₁) Wc g₂ hcomm₂))).map
          (((BigFppfOver.toScheme B S hS).map g₂).stalkMap
            (chartPoint B S hS Y.1 (targetNeighborhood B S hS N Vc g₁ hcomm₁))).hom)
        (((maximalIdeal ↥(chartLocalRing B S hS Z.1 (targetNeighborhood B S hS
                (targetNeighborhood B S hS N Vc g₁ hcomm₁) Wc g₂ hcomm₂))).map
            (((BigFppfOver.toScheme B S hS).map g₂).stalkMap
              (chartPoint B S hS Y.1 (targetNeighborhood B S hS N Vc g₁ hcomm₁))).hom).map
          (((BigFppfOver.toScheme B S hS).map g₁).stalkMap (chartPoint B S hS X.1 N)).hom)
        rfl ↥(chartZariskiModuleStalk B S hS X.1 X.2 N F)) ↔
      IsFibreFlatOverAtGeometricPoint B S hS f h F xbar
Tag 05WZ, a definition

Tag 05WZ in the Stacks Project.

AlgebraicGeometry.Space.IsFlatOnFibreAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessAtPoint.lean, line 121. The attribute's comment: “part (1), defined through the Lemma 05WY notion IsFibreFlatOverAtGeometricPoint (its condition (1)), asked at every geometric point over x; equal to that condition at any one such point by isFlatOnFibreAt_iff_...”.

Stacks 05WZ, part (1). The restriction of an 𝒪_X-module F to its fibre over the image z of a point x of |X| is flat at x over the fibre of Y over z when the condition of Stacks 05WY holds at every geometric point of X above x.

The source defines this by "the equivalent conditions of Lemma 05WY are satisfied"; the condition used is AlgebraicGeometry.Space.IsFibreFlatOverAtGeometricPoint, condition (1) of that lemma, whose equivalence with condition (3) is AlgebraicGeometry.Space.exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint. See AlgebraicGeometry.Space.isFlatOnFibreAt_iff_isFibreFlatOverAtGeometricPoint for the reading at a single chosen geometric point.

def IsFlatOnFibreAt {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (F : Modules.{u, m} B S hS X.1 X.2) (x : points B S hS X.1) : Prop

AlgebraicGeometry.Space.IsFlatFibreAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessAtPoint.lean, line 166. The attribute's comment: “part (2), part (1) at F = O_X, hence defined through the Lemma 05WY notion IsFibreFlatOverAtGeometricPoint at every geometric point over x”.

Stacks 05WZ, part (2). The fibre of X over the image z of a point x of |X| is flat at x over the fibre of Y over z when part (1) holds for F = 𝒪_X.

def IsFlatFibreAt {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (x : points B S hS X.1) : Prop

AlgebraicGeometry.Space.IsFlatFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreFlatnessAtPoint.lean, line 174. The attribute's comment: “part (3), part (2) at every point of |X| over z, hence defined through the Lemma 05WY notion IsFibreFlatOverAtGeometricPoint”.

Stacks 05WZ, part (3). The fibre of X over a point z of |Z| is flat over the fibre of Y over z when part (2) holds at every point of |X| lying over z.

def IsFlatFibre {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (h : Y ⟶ Z)
    (z : points B S hS Z.1) : Prop
Tag 05X0, a theorem

Tag 05X0 in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_and_isFibreFlat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleFibreCriterion.lean, line 312. The attribute's comment: “the equivalence of (1) and (2) at a geometric point x̄: flatness over Z and over Y at x̄ are condition (2) of Stacks 05VU, the fibre condition of (1) is the one of Stacks 05WY named by the source's definition 05WZ, and flatness of Y over Z at ȳ is Space.IsFlatAt at its image point. Hypothesis (2) of the source is read on the Zariski site of every etale chart; the openness assertion is isOpen_setOf_... below.”.

Stacks 05X0. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over a scheme S, let F be an 𝒪_X-module which is quasi-coherent on the small étale site and of finite presentation on charts, and let x̄ be a geometric point of X with images ȳ and z̄. Assume X is locally of finite presentation over Z and Y is locally of finite type over Z, and assume F_{x̄} ≠ 0. Then

  1. F is flat over Z at x̄ and the restriction of F to its fibre over z̄ is flat at x̄ over the fibre of Y over z̄

holds exactly when

  1. Y is flat over Z at ȳ and F is flat over Y at x̄

holds. The fibre condition of (1) is the one of Stacks 05WY, as the source's definition (Stacks 05WZ) prescribes.

theorem isFlatOverAtGeometricPoint_and_isFibreFlat_iff {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hp : IsLocallyOfFinitePresentation B S hS (f ≫ g).hom)
    (hq : IsLocallyOfFiniteType B S hS g.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (xbar : GeometricPoint B S hS X.1)
    (hne : Nontrivial (geometricModuleStalk B S hS X xbar F)) :
    (IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar ∧
        IsFibreFlatOverAtGeometricPoint B S hS f g F xbar) ↔
      (IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image ∧
        IsFlatOverAtGeometricPoint B S hS f F xbar)

AlgebraicGeometry.Space.setOf_isFlatOverAtGeometricPoint_and_isFibreFlat_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleFibreCriterion.lean, line 478. The attribute's comment: “the openness assertion: the locus where (1) and (2) hold is the support of the module intersected with the locus where the module is flat over both Z and Y, which is open by Space.isOpen_flatLocus_inter_flatLocus. Conditions (1) and (2) are read at every geometric point above the point of |X|, which is no restriction: by Stacks 05VU the conditions do not depend on the geometric point chosen above it.”.

Stacks 05X0, the openness assertion. Under the hypotheses of Stacks 05X0, the set of points of |X| lying in the support of F at which conditions (1) and (2) hold at every geometric point above them is the intersection of that support with the open set AlgebraicGeometry.Space.isOpen_flatLocus_inter_flatLocus is about, namely the locus where F is flat both over Z and over Y. So that set is open in the support of F.

A point of the support at which (1) and (2) hold lies in both flat loci by (1) and (2); and at a point of the support lying in both loci condition (1) holds, the fibre condition being a base change of flatness over Y, hence so does condition (2) by the equivalence.

theorem setOf_isFlatOverAtGeometricPoint_and_isFibreFlat_eq (f : X ⟶ Y) (g : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hp : IsLocallyOfFinitePresentation B S hS (f ≫ g).hom)
    (hq : IsLocallyOfFiniteType B S hS g.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F) :
    {x : points B S hS X.1 |
        x ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) ∧
        ∀ xbar : GeometricPoint B S hS X.1, xbar.image = x →
          (IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar ∧
              IsFibreFlatOverAtGeometricPoint B S hS f g F xbar) ∧
            (IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image ∧
              IsFlatOverAtGeometricPoint B S hS f F xbar)} =
      (flatLocus B S hS X.2 (f ≫ g).hom F ∩ flatLocus B S hS X.2 f.hom F) ∩
        supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)

AlgebraicGeometry.Space.isOpen_setOf_isFlatOverAtGeometricPoint_and_isFibreFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleFibreCriterion.lean, line 524. The attribute's comment: “the openness assertion, read in the subspace topology of the support: the locus where (1) and (2) hold is open in Supp(F). Conditions (1) and (2) are read at every geometric point above the point of |X|, which by Stacks 05VU does not depend on the geometric point chosen. Finite presentation of the module is read on the Zariski site of every etale scheme chart.”.

Stacks 05X0, the openness assertion in the subspace of the support. Under the hypotheses of Stacks 05X0 the set of points of the support of F at which conditions (1) and (2) hold is open in the support.

This is AlgebraicGeometry.Space.setOf_isFlatOverAtGeometricPoint_and_isFibreFlat_eq read in the subspace topology: the set is the inverse image in the support of the open set of AlgebraicGeometry.Space.isOpen_flatLocus_inter_flatLocus.

theorem isOpen_setOf_isFlatOverAtGeometricPoint_and_isFibreFlat (f : X ⟶ Y) (g : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hp : IsLocallyOfFinitePresentation B S hS (f ≫ g).hom)
    (hq : IsLocallyOfFiniteType B S hS g.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F) :
    IsOpen {x : (supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) :
        Set (points B S hS X.1)) |
      ∀ xbar : GeometricPoint B S hS X.1, xbar.image = (x : points B S hS X.1) →
        (IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar ∧
            IsFibreFlatOverAtGeometricPoint B S hS f g F xbar) ∧
          (IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image ∧
            IsFlatOverAtGeometricPoint B S hS f F xbar)}
Tag 05X1, a lemma

Tag 05X1 in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_flatFibreCharts_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatFibrewiseFinitePresentation.lean, line 195. The attribute's comment: “the first conclusion: flatness of f. Hypotheses (1), (2) and (4) are the library spellings Space.IsLocallyOfFinitePresentation of f ≫ g, Space.IsFlat of f ≫ g and Space.IsLocallyOfFiniteType of g; hypothesis (3) is CARRIED in its every-etale-chart reading Space.HasFlatFibreCharts, as in the locally Noetherian form Space.isFlat_of_flatFibreCharts of Stacks 0APS, the comparison of a fibre of an algebraic space with the scheme-theoretic fibre of a chart being available in this library only for properties of objects (Space.hasEtaleLocalProperty_fiberAt_iff) and not for a property of a morphism between two such fibres.”.

Stacks Project, Tag 05X1, the first conclusion. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over a scheme S. If X is locally of finite presentation over Z, X is flat over Z, the fibres of X over the points of Z are flat over the corresponding fibres of Y in the chart sense of AlgebraicGeometry.Space.HasFlatFibreCharts, and Y is locally of finite type over Z, then f is flat.

theorem isFlat_of_flatFibreCharts_finitePresentation
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfp : IsLocallyOfFinitePresentation B S hS (f ≫ g))
    (hflat : IsFlat B S hS (f ≫ g)) (hft : IsLocallyOfFiniteType B S hS g)
    (hfib : HasFlatFibreCharts B S hS f g) :
    IsFlat B S hS f

AlgebraicGeometry.Space.isFlat_of_flatFibreCharts_finitePresentation_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatFibrewiseFinitePresentation.lean, line 219. The attribute's comment: “the second conclusion: flatness of Y over Z for surjective f, with surjectivity taken as Space.IsSurjective of Stacks 03ME. Hypotheses (1), (2) and (4) are the library spellings Space.IsLocallyOfFinitePresentation of f ≫ g, Space.IsFlat of f ≫ g and Space.IsLocallyOfFiniteType of g; hypothesis (3) is CARRIED in its every-etale-chart reading Space.HasFlatFibreCharts, as in the locally Noetherian form Space.isFlat_of_flatFibreCharts_of_isSurjective of Stacks 0APS, the comparison of a fibre of an algebraic space with the scheme-theoretic fibre of a chart being available in this library only for properties of objects and not for a property of a morphism between two such fibres.”.

Stacks Project, Tag 05X1, the second conclusion. In the situation of AlgebraicGeometry.Space.isFlat_of_flatFibreCharts_finitePresentation, if f is in addition surjective then Y is flat over Z.

theorem isFlat_of_flatFibreCharts_finitePresentation_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfp : IsLocallyOfFinitePresentation B S hS (f ≫ g))
    (hflat : IsFlat B S hS (f ≫ g)) (hft : IsLocallyOfFiniteType B S hS g)
    (hfib : HasFlatFibreCharts B S hS f g) (hfs : IsSurjective B S hS f) :
    IsFlat B S hS g
Tag 05X2, a lemma

Tag 05X2 in the Stacks Project.

AlgebraicGeometry.Space.flatLocus_modulePullback_eq_preimage_of_isFlatOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusBaseChangeOverBase.lean, line 139. The attribute's comment: “base change: the locus on the base change is the inverse image of the locus downstairs. Hypotheses (1)-(4) of the source are the finite presentation of X over Z, of the module on the small etale site, the flatness of the module over Z, and the finite type of Y over Z. The openness assertion is Space.isOpen_flatLocus_of_isLocallyOfFinitePresentation_comp.”.

Stacks 05X2, the base-change assertion. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over an algebraic space Z by f ≫ q and q : Y ⟶ Z, and let F be a quasi-coherent 𝒪_X-module. Assume X is locally of finite presentation over Z, that F is of finite presentation, that F is flat over Z, and that Y is locally of finite type over Z. Then for a base change along an arbitrary morphism h : Z' ⟶ Z, presented by the cartesian squares Y' = Y ×_Z Z' and X' = X ×_Y Y', the locus of points of |X'| at which the inverse image of F is flat over Y' is the inverse image under |X'| ⟶ |X| of the locus of points of |X| at which F is flat over Y.

theorem flatLocus_modulePullback_eq_preimage_of_isFlatOverBase
    {f : X ⟶ Y} {q : Y ⟶ Z} {h : Z' ⟶ Z} {g : Y' ⟶ Y} {q' : Y' ⟶ Z'}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'}
    (sqY : IsPullback g q' q h) (sqX : IsPullback g' f' f g)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hFfp : F.IsFinitePresentation)
    (hp : IsLocallyOfFinitePresentation B S hS (f ≫ q).hom)
    (hq : IsLocallyOfFiniteType B S hS q.hom)
    (hFZ : IsFlatOver B S hS X.2 (f ≫ q).hom F) :
    flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' flatLocus B S hS X.2 f.hom F

AlgebraicGeometry.Space.isOpen_flatLocus_of_isLocallyOfFinitePresentation_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusOverBase.lean, line 73. The attribute's comment: “openness; hypothesis (3), flatness over the base, is not needed for this half”.

Stacks 05X2, the openness assertion. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over an algebraic space Z by p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation and q is locally of finite type, then the locus of points of |X| at which an 𝒪_X-module which is quasi-coherent of finite presentation on charts is flat over Y is open.

The tag sits on AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnSite_comp, which is this assertion with hypothesis (2) of the source read where the source reads it, on the small étale site; this form is the special case of it at a module whose finite presentation is available only chartwise.

theorem isOpen_flatLocus_of_isLocallyOfFinitePresentation_comp
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (F : Modules.{u, u} B S hS X hX)
    (hp : IsLocallyOfFinitePresentation B S hS p)
    (hq : IsLocallyOfFiniteType B S hS q)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hfp : IsFinitePresentationOnCharts B S hS hX F) :
    IsOpen (flatLocus B S hS hX f F)

AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnSite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleLocusOverBase.lean, line 102. The attribute's comment: “openness; hypothesis (3), flatness over the base, is not needed for this half”.

Stacks 05X2, the openness assertion, from finite presentation on the small étale site. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over an algebraic space Z by p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation and q is locally of finite type, then the locus of points of |X| at which an 𝒪_X-module of finite presentation on the small étale site is flat over Y is open.

Hypothesis (2) of the source, finite presentation of the module, is Stacks 03DL (7) on the small étale site of X; the quasi-coherence of the module which the source assumes in its preamble follows from it, by SheafOfModules.isQuasicoherentOnSite_of_isFinitePresentationOnSite. Both are passed to the charts by AlgebraicGeometry.Space.isFinitePresentationOnCharts_of_isFinitePresentationOnSite and AlgebraicGeometry.Space.isQuasicoherentOnCharts_of_isFinitePresentationOnSite, so this form asks no chartwise hypothesis and AlgebraicGeometry.Space.isOpen_flatLocus_of_isLocallyOfFinitePresentation_comp is the special case of it at a module whose finite presentation is only available chartwise.

theorem isOpen_flatLocus_of_isFinitePresentationOnSite_comp
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (F : Modules.{u, u} B S hS X hX)
    (hp : IsLocallyOfFinitePresentation B S hS p)
    (hq : IsLocallyOfFiniteType B S hS q)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite F) :
    IsOpen (flatLocus B S hS hX f F)
Tag 05X3, a lemma

Tag 05X3 in the Stacks Project.

AlgebraicGeometry.Space.isOpen_setOf_isFlatAt_of_isLocallyOfFinitePresentation_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatLocus.lean, line 194. The attribute's comment: “openness of the flat locus”. References: SGA 3 VIB (1.3), “more general”; SGA 3 X (4.4), “partial”.

Stacks 05X3, the openness assertion. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation and q is locally of finite type, then the set of points of |X| at which f is flat is open.

Flatness of p, which the source assumes, is not needed here: the two finiteness hypotheses already make f locally of finite presentation by Stacks 05WT, so the openness of the flat locus of a morphism locally of finite presentation applies to f itself. The same reduction is how the scheme-level assertion of Stacks 05VK is proved.

theorem isOpen_setOf_isFlatAt_of_isLocallyOfFinitePresentation_comp
    {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFinitePresentation B S hS p)
    (hq : IsLocallyOfFiniteType B S hS q) :
    IsOpen {x : points B S hS X | IsFlatAt B S hS f x}

AlgebraicGeometry.Space.flatLocusOpenAndStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatLocusBaseChange.lean, line 536. The attribute's comment: “openness and base change of the relative flat locus”.

Stacks 05X3. For a commutative triangle of algebraic spaces over S given by f : X ⟶ Y, p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p, with p locally of finite presentation and flat and q locally of finite type, the locus of points of |X| at which f is flat is open and its formation commutes with base change along any morphism Z' ⟶ Z.

The openness assertion is AlgebraicGeometry.Space.isOpen_setOf_isFlatAt_of_isLocallyOfFinitePresentation_comp and the base-change assertion is AlgebraicGeometry.Space.isFlatAt_baseChangeOverBase_iff.

theorem flatLocusOpenAndStableUnderBaseChange
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFinitePresentation B S hS p) (hpflat : IsFlat B S hS p)
    (hq : IsLocallyOfFiniteType B S hS q) :
    IsOpen {x : points B S hS X | IsFlatAt B S hS f x} ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Z' →
        ∀ (g : Z' ⟶ Z) (x' : points B S hS (pullback p g)),
          IsFlatAt B S hS (baseChangeOverBase B S hS f p q hfq g) x' ↔
            IsFlatAt B S hS f
              (pointsMap B S hS (pullback p g) (pullback.fst p g) x')
Tag 0CZS, a lemma

Tag 0CZS in the Stacks Project.

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusChartComparison.lean, line 208. The attribute's comment: “clause (4) in the SMALL-ETALE-SITE reading: the source's Zariski-chart reading of clause (4) at a geometric point xbar implies that the image point of xbar lies in the locus of points of |X| admitting an etale morphism of algebraic spaces a : V -> X through them along which the inverse image of F is finite free in the sense of 03DE(2), which is the locus of Stacks 0CZT”.

Clause (4) of Stacks 0CZS in the small-étale-site reading of Stacks 0CZT. If a quasi-coherent 𝒪_X-module M is finite free in an étale neighbourhood of a geometric point x̄ of X in the Zariski-chart sense of AlgebraicGeometry.Space.IsFiniteFreeNearGeometricPoint — the source's own reading — then the image point of x̄ lies in the finite-free étale locus AlgebraicGeometry.Space.etaleFiniteFreeLocus, the locus of Stacks 0CZT.

theorem mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint
    {X : AlgebraicSpaces B S hS} (M : Modules.{u, u} B S hS X.1 X.2)
    (hM : M.IsQuasicoherentOnSite) (xbar : GeometricPoint B S hS X.1)
    (h : IsFiniteFreeNearGeometricPoint B S hS xbar M) :
    xbar.image ∈ etaleFiniteFreeLocus B S hS M

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusChartComparison.lean, line 248. The attribute's comment: “(1) implies (4) with clause (4) in the SMALL-ETALE-SITE reading, i.e. membership in the locus of Stacks 0CZT; the fibre stalk and its base ring are in the QUOTIENT FORM M_xbar / m_ybar M_xbar over O_{X, xbar} / m_ybar O_{X, xbar}, whose identification with the stalk on the geometric fibre X_ybar is condition (2) of Stacks 05WY and is not available”.

Clause (1) implies clause (4), in the small-étale-site reading of Stacks 0CZT. Let f : X ⟶ Y be locally of finite presentation, let M be a quasi-coherent 𝒪_X-module of finite presentation on charts and let x̄ be a geometric point of X. If M is flat at x over Y and the geometric fibre stalk (M_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module, then the image point of x̄ lies in the finite-free étale locus of Stacks 0CZT. The fibre stalk and its base ring are in the quotient form M_{x̄} / 𝔪_{ȳ} M_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}.

theorem mem_etaleFiniteFreeLocus_of_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (M : Modules.{u, u} B S hS X.1 X.2)
    [M.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 M)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f M xbar)
    (hfibre : Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f M xbar)) :
    xbar.image ∈ etaleFiniteFreeLocus B S hS M

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_geometricFibre_of_isFiniteFreeNearGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreEtaleFreeLocus.lean, line 278. The attribute's comment: “(4) implies (3), with the geometric fibre X_ybar formed as the fibre product of f with the geometric point ybar = f o xbar in the category of algebraic spaces over S (02X2), the etale neighbourhood of xbar inside X_ybar read as in the locus of 0CZT, and clause (4) in the source's Zariski-chart reading”.

Stacks 0CZS, (4) implies (3). If a quasi-coherent 𝒪_X-module M is finite free in an étale neighbourhood of a geometric point x̄ of X — clause (4), in the source's Zariski-chart reading — then the inverse image of M to the geometric fibre X_ȳ through x̄ is finite free in an étale neighbourhood of the lift of x̄ to that fibre, which is clause (3).

The source calls this implication immediate, and so it is: clause (4) puts x in the finite-free étale locus of M on |X| (AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint), and that locus only grows under an inverse image, the lift of x̄ lying over x̄ by AlgebraicGeometry.Space.pointsMap_geometricFibreToSource_geometricFibrePoint.

theorem mem_etaleFiniteFreeLocus_geometricFibre_of_isFiniteFreeNearGeometricPoint
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (M : Modules.{u, u} B S hS X.1 X.2)
    (hM : M.IsQuasicoherentOnSite) (xbar : GeometricPoint B S hS X.1)
    (h : IsFiniteFreeNearGeometricPoint B S hS xbar M) :
    (geometricFibrePoint B S hS f xbar).image ∈
      etaleFiniteFreeLocus B S hS ((modulePullback B S hS
        (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj M)

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_geometricFibre_of_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreEtaleFreeLocus.lean, line 304. The attribute's comment: “(1) implies (3), with the geometric fibre X_ybar formed as the fibre product of f with ybar = f o xbar (02X2) and the fibre stalk of clause (1) in the QUOTIENT FORM M_xbar / m_ybar M_xbar over O_{X, xbar} / m_ybar O_{X, xbar}, whose identification with the etale local ring of that fibre is condition (2) of Stacks 05WY and is not available”.

Stacks 0CZS, (1) implies (3). Let f : X ⟶ Y be locally of finite presentation, let M be a quasi-coherent 𝒪_X-module of finite presentation on charts and let x̄ be a geometric point of X. If M is flat at x over Y and the geometric fibre stalk (M_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module, then the inverse image of M to the geometric fibre is finite free in an étale neighbourhood of the lift of x̄.

This is (1) ⟹ (4) followed by (4) ⟹ (3). The fibre stalk and its base ring are in the quotient form M_{x̄} / 𝔪_{ȳ} M_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}, as they are throughout this development; the identification of that quotient with the étale local ring of the geometric fibre constructed here is condition (2) of Stacks 05WY and is not available.

theorem mem_etaleFiniteFreeLocus_geometricFibre_of_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (M : Modules.{u, u} B S hS X.1 X.2)
    [M.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 M)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f M xbar)
    (hfibre : Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f M xbar)) :
    (geometricFibrePoint B S hS f xbar).image ∈
      etaleFiniteFreeLocus B S hS ((modulePullback B S hS
        (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj M)

AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_of_isFiniteFreeNearGeometricFibrePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkClauseThree.lean, line 263. The attribute's comment: “(3) implies (1), with the geometric fibre X_ybar formed as the fibre product of f with ybar = f o xbar in the category of algebraic spaces over S (02X2), clause (3) read as finite freeness of the inverse image of F to X_ybar on a Zariski open of an etale SCHEME chart of X_ybar around a point above the canonical lift of xbar, and the fibre stalk of clause (1) in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar}; flatness of F over Y, local finite presentation of f and finite presentation of F are not assumed”.

Stacks 0CZS, (3) implies (1). Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let x̄ be a geometric point of X with image ȳ. If the inverse image of F to the geometric fibre X_ȳ is finite free in an étale neighbourhood of the lift of x̄ — clause (3) — then the fibre stalk (F_ȳ)_x̄ is a flat 𝒪_{X_ȳ, x̄}-module, which is clause (1).

The defining square of X_ȳ is cartesian, so clause (1) for f at x̄ and clause (1) for the structure morphism X_ȳ ⟶ Spec(κ(ȳ)) at the lift are the same condition (AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_modulePullback_iff). Clause (3) is clause (4) for the inverse image on the fibre, so (4) ⟹ (2) ⟹ (1) on the fibre gives clause (1) at the lift, and the comparison carries it down. Condition (2) of Stacks 05WY — the identification of the fibre stalk with the stalk on X_ȳ — is not used: both sides of the comparison are taken in the quotient form.

Neither flatness of F over Y, nor local finite presentation of f, nor finite presentation of F is assumed, which generalises the source.

theorem flat_geometricFibreModuleStalk_of_isFiniteFreeNearGeometricFibrePoint
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (xbar : GeometricPoint B S hS X.1)
    (h : IsFiniteFreeNearGeometricPoint B S hS (geometricFibrePoint B S hS f xbar)
      ((modulePullback B S hS
        (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F)) :
    Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)

AlgebraicGeometry.Space.isFiniteFreeNearGeometricFibrePoint_of_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkClauseThree.lean, line 303. The attribute's comment: “(1) implies (3), with the geometric fibre X_ybar formed as the fibre product of f with ybar = f o xbar in the category of algebraic spaces over S (02X2), the fibre stalk of clause (1) in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar}, and clause (3) read as finite freeness of the inverse image of F to X_ybar on a Zariski open of an etale SCHEME chart of X_ybar around a point above the canonical lift of xbar”.

Stacks 0CZS, (1) implies (3). Let f : X ⟶ Y be locally of finite presentation, let F be a finitely presented quasi-coherent 𝒪_X-module and let x̄ be a geometric point of X with image ȳ. If F is flat at x over Y and the fibre stalk (F_ȳ)_x̄ is a flat 𝒪_{X_ȳ, x̄}-module, then the inverse image of F to the geometric fibre X_ȳ is finite free in an étale neighbourhood of the lift of x̄, which is clause (3).

Clause (1) at x̄ is clause (1) for the structure morphism X_ȳ ⟶ Spec(κ(ȳ)) at the lift, by the comparison across the cartesian defining square of X_ȳ, and (1) ⟹ (4) applied on the fibre is clause (3). Its hypotheses there are the base changes of the hypotheses here: Stacks 03XR for local finite presentation of the structure morphism, the inverse image of a finitely presented module for finite presentation on charts, and Stacks 05VW (1) for flatness at the lift.

theorem isFiniteFreeNearGeometricFibrePoint_of_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] [SheafOfModules.IsFinitePresentationOnSite F]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar)
    (hfibre : Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)) :
    IsFiniteFreeNearGeometricPoint B S hS (geometricFibrePoint B S hS f xbar)
      ((modulePullback B S hS
        (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F)

AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_geometricFibre_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkClauseThree.lean, line 368. The attribute's comment: “clauses (1), (2), (3) and (4) are equivalent, under the source's own hypotheses; the geometric fibre X_ybar is formed as the fibre product of f with ybar = f o xbar in the category of algebraic spaces over S (02X2), clauses (3) and (4) are read as finite freeness on a Zariski open of an etale SCHEME chart around a point above the relevant geometric point, and clauses (1) and (2) appear BOTH in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} and in the LITERAL FORM on X_ybar, i.e. the geometric stalk of the inverse image of F at the canonical lift of xbar over the etale local ring of X_ybar there; the agreement of the two forms is a consequence of the equivalence and is NOT condition (2) of Stacks 05WY, which stays unavailable”.

Stacks 0CZS, the equivalence of all four clauses. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation, let F be a finitely presented quasi-coherent 𝒪_X-module and let x̄ be a geometric point of X with image ȳ. If F is flat at x over Y, then

  1. (F_ȳ)_x̄ is a flat 𝒪_{X_ȳ, x̄}-module,
  2. (F_ȳ)_x̄ is a free 𝒪_{X_ȳ, x̄}-module,
  3. F_ȳ is finite free in an étale neighbourhood of x̄ in X_ȳ,
  4. F is finite free in an étale neighbourhood of x in X

are equivalent. Clauses (1) and (2) appear twice: in the quotient form F_x̄ / 𝔪_ȳ F_x̄ over 𝒪_{X, x̄} / 𝔪_ȳ 𝒪_{X, x̄} in which this development carries them, and in the literal form on the geometric fibre X_ȳ of StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreEtaleFreeLocus.lean — the honest geometric stalk of the inverse image of F at the canonical lift of x̄, over the honest étale local ring of X_ȳ there. The entries are, in order: clause (1) in the quotient form, clause (2) in the quotient form, clause (1) in the literal form, clause (2) in the literal form, clause (3), and clause (4).

The equivalence of the two forms of clauses (1) and (2) is not condition (2) of Stacks 05WY, and does not supply it: no identification of the quotient with the stalk on X_ȳ is produced, only the agreement of the flatness and freeness conditions, which clause (3) mediates.

theorem flat_geometricFibreModuleStalk_geometricFibre_tfae
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] [SheafOfModules.IsFinitePresentationOnSite F]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar) :
    [Module.Flat (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar),
      Module.Free (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar),
      Module.Flat
        ↥(etaleLocalRing B S hS (geometricFibre B S hS f (geometricPointMap f.hom xbar)).1
          (geometricFibrePoint B S hS f xbar))
        ↥(geometricModuleStalk B S hS (geometricFibre B S hS f (geometricPointMap f.hom xbar))
          (geometricFibrePoint B S hS f xbar)
          ((modulePullback B S hS
            (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F)),
      Module.Free
        ↥(etaleLocalRing B S hS (geometricFibre B S hS f (geometricPointMap f.hom xbar)).1
          (geometricFibrePoint B S hS f xbar))
        ↥(geometricModuleStalk B S hS (geometricFibre B S hS f (geometricPointMap f.hom xbar))
          (geometricFibrePoint B S hS f xbar)
          ((modulePullback B S hS
            (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F)),
      IsFiniteFreeNearGeometricPoint B S hS (geometricFibrePoint B S hS f xbar)
        ((modulePullback B S hS
          (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F),
      IsFiniteFreeNearGeometricPoint B S hS xbar F].TFAE

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_mem_etaleFiniteFreeLocus_geometricFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkClauseThree.lean, line 453. The attribute's comment: “(3) implies (4) with BOTH clauses in the SMALL-ETALE-SITE reading, i.e. membership in the locus of Stacks 0CZT on the geometric fibre X_ybar and on X respectively, X_ybar being the fibre product of f with ybar = f o xbar in the category of algebraic spaces over S (02X2); the source's flatness of F over Y at x is STRENGTHENED to flatness of F over Y everywhere, because the Zariski-chart reading upstairs is recovered only at a geometric point chosen over the image of the lift of xbar”.

Stacks 0CZS, (3) implies (4), both clauses in the small-étale-site reading of the locus of Stacks 0CZT. Let f : X ⟶ Y be locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation on charts which is flat over Y, and let x̄ be a geometric point of X with image ȳ. If the image of the canonical lift of x̄ lies in the finite-free étale locus of the inverse image of F to the geometric fibre X_ȳ, then the image of x̄ lies in the finite-free étale locus of F.

This is the reverse inclusion of the base-change clause of Stacks 0CZT — AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint_modulePullback — at the cartesian defining square of X_ȳ, with the Zariski-chart reading upstairs supplied at a chosen geometric point over the image of the lift (AlgebraicGeometry.Space.exists_isFiniteFreeNearGeometricPoint_of_mem_etaleFiniteFreeLocus); only the image point of the chosen point enters the conclusion, and it is the image of the lift, which is the image of x̄.

Because the chosen point need not be x̄, the source's hypothesis of flatness of F over Y at x is strengthened here to flatness over Y everywhere. The equivalence AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_geometricFibre_tfae carries the source's own hypothesis, at the Zariski-chart reading of clause (3).

theorem mem_etaleFiniteFreeLocus_of_mem_etaleFiniteFreeLocus_geometricFibre
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (hF : IsFlatOver B S hS X.2 f.hom F) (xbar : GeometricPoint B S hS X.1)
    (h : (geometricFibrePoint B S hS f xbar).image ∈ etaleFiniteFreeLocus B S hS
      ((modulePullback B S hS
        (geometricFibreToSource B S hS f (geometricPointMap f.hom xbar))).obj F)) :
    xbar.image ∈ etaleFiniteFreeLocus B S hS F

AlgebraicGeometry.Space.isFiniteFreeNearGeometricPoint_of_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFiniteFree.lean, line 315. The attribute's comment: “(1) implies (4), with the etale neighbourhood of x taken to be a Zariski open of an etale SCHEME chart of X around a point above x and finite freeness read on the Zariski site of that chart (the source's own route through More on Morphisms 080Q); the fibre stalk and its base ring are in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar}, whose identification with the stalk on the geometric fibre X_ybar is condition (2) of Stacks 05WY and is not available”.

Stacks 0CZS, (1) implies (4). Let f : X ⟶ Y be locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation on charts and let x̄ be a geometric point of X. If F is flat at x over Y and the fibre stalk (F_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module, then F is finite free in an étale neighbourhood of x in X.

The route is the source's: clause (1) together with the standing flatness makes the geometric stalk F_{x̄} free over 𝒪_{X, x̄} (AlgebraicGeometry.Space.free_geometricModuleStalk_of_flat_geometricFibreModuleStalk, which is Stacks 05X0 at 𝟙 X over f); freeness descends to the Zariski stalk of an étale scheme chart; and Stacks 0B8J trivialises the chart restriction on a Zariski open of the chart. The fibre stalk and its base ring are taken in the quotient form F_{x̄} / 𝔪_{ȳ} F_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}, as in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFreeness.lean.

theorem isFiniteFreeNearGeometricPoint_of_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar)
    (hfibre : Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)) :
    IsFiniteFreeNearGeometricPoint B S hS xbar F

AlgebraicGeometry.Space.free_geometricFibreModuleStalk_of_isFiniteFreeNearGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFiniteFree.lean, line 342. The attribute's comment: “(4) implies (2), with the etale neighbourhood of x a Zariski open of an etale SCHEME chart of X and the fibre stalk in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar}; flatness of F over Y, local finite presentation of f and finite presentation of F are not assumed”.

Stacks 0CZS, (4) implies (2). If F is finite free in an étale neighbourhood of x in X, then the fibre stalk (F_{ȳ})_{x̄} is a free 𝒪_{X_{ȳ}, x̄}-module.

The trivialization makes the Zariski stalk of the chart restriction free, freeness ascends to the geometric stalk by Stacks 05VP, and the fibre stalk is the reduction of the geometric stalk modulo 𝔪_{ȳ} 𝒪_{X, x̄}. Neither flatness of F over Y, nor local finite presentation of f, nor finite presentation of F is used, which generalises the source.

theorem free_geometricFibreModuleStalk_of_isFiniteFreeNearGeometricPoint
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (xbar : GeometricPoint B S hS X.1)
    (h : IsFiniteFreeNearGeometricPoint B S hS xbar F) :
    Module.Free (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)

AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFiniteFree.lean, line 379. The attribute's comment: “clauses (1), (2) and (4) are equivalent, under the source's own hypotheses, with the fibre stalk and its base ring in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} and clause (4) read as finite freeness on a Zariski open of an etale SCHEME chart of X around a point above x”.

Stacks 0CZS, the equivalence of clauses (1), (2) and (4). Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation, let F be a finitely presented quasi-coherent 𝒪_X-module and let x̄ be a geometric point of X with image ȳ. If F is flat at x over Y, then

  1. (F_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module,
  2. (F_{ȳ})_{x̄} is a free 𝒪_{X_{ȳ}, x̄}-module,
  3. F is finite free in an étale neighbourhood of x in X

are equivalent. The fibre stalk and its base ring are taken in the quotient form F_{x̄} / 𝔪_{ȳ} F_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}, which is how the source's own proof reads clause (1), and clause (4) is read on a Zariski open of an étale scheme chart. Clause (3) is not among the entries here: it is proved from clause (4) in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreEtaleFreeLocus.lean, and it is added to the equivalence — in its Zariski-chart reading on the geometric fibre, together with clauses (1) and (2) in their literal form on that fibre — by AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_geometricFibre_tfae of StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkClauseThree.lean. The source's reverse implication (3) ⟹ (2) goes through the identification of the stalk on the geometric fibre with the quotient, which is condition (2) of Stacks 05WY and is still not available; the equivalence does not need it, only the agreement of the two flatness conditions across the cartesian defining square of the fibre.

theorem flat_geometricFibreModuleStalk_tfae
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] [SheafOfModules.IsFinitePresentationOnSite F]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar) :
    [Module.Flat (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar),
      Module.Free (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar),
      IsFiniteFreeNearGeometricPoint B S hS xbar F].TFAE

AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_of_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFreeness.lean, line 415. The attribute's comment: “(2) implies (1), with the fibre stalk and its base ring in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} (the geometric fibre X_ybar is not constructed in this library); flatness of F over Y and finite presentation are not assumed”.

Stacks 0CZS, (2) implies (1). A free fibre stalk (F_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module.

The fibre stalk and its base ring are taken in the quotient form F_{x̄} / 𝔪_{ȳ} F_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}, which is condition (1) of Stacks 05WY for X ⟶ X ⟶ Y and is how the source's own proof reads clause (1); their identification with the étale local ring and the geometric stalk on a geometric fibre X_{ȳ} is not available, the fibre of a morphism of algebraic spaces over a point of the target not being constructed in this library. Neither flatness of F at x over Y, nor local finite presentation of f, nor finite presentation of F is assumed, which generalises the source.

theorem flat_geometricFibreModuleStalk_of_free {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, m} B S hS X.1 X.2) (xbar : GeometricPoint B S hS X.1)
    (hfree : Module.Free (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)) :
    Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)

AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_iff_free_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFreeness.lean, line 480. The attribute's comment: “(1) iff (2) under the source's own hypotheses, with the fibre stalk and base ring in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} (the geometric fibre X_ybar is not constructed in this library)”.

Stacks 0CZS, (1) is equivalent to (2). For a finitely presented 𝒪_X-module F, flatness and freeness of the fibre stalk (F_{ȳ})_{x̄} over the local ring 𝒪_{X_{ȳ}, x̄} of the geometric fibre agree.

The fibre stalk and its base ring are taken in the quotient form F_{x̄} / 𝔪_{ȳ} F_{x̄} over 𝒪_{X, x̄} / 𝔪_{ȳ} 𝒪_{X, x̄}, which is condition (1) of Stacks 05WY for X ⟶ X ⟶ Y and is how the source's own proof reads clause (1); the geometric fibre X_{ȳ} itself is not constructed in this library. Neither flatness of F at x over Y nor local finite presentation of f is assumed, which generalises the source: both clauses are conditions on the fibre stalk alone.

theorem flat_geometricFibreModuleStalk_iff_free_of_isFinitePresentation
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsFinitePresentationOnSite] (xbar : GeometricPoint B S hS X.1) :
    Module.Flat (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar) ↔
      Module.Free (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar)

AlgebraicGeometry.Space.exists_chartOpen_over_iso_free_of_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFreeness.lean, line 732. The attribute's comment: “(1) implies (4) under the source's own hypotheses, with clause (1) in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} (the geometric fibre X_ybar is not constructed in this library) and clause (4) in the reading the source's proof produces: an etale SCHEME chart (U, u) over (X, xbar) together with a Zariski open W of U containing u on which the chart restriction phi^ F becomes free on finitely many generators. That W is an etale neighbourhood of xbar in X by chartOpenNeighborhood. The finite freeness is read as freeness of (phi^ F)|_W on the slice of the Zariski site of U at W; identifying that with the chart restriction of F to W read on the Zariski site of W itself is an equivalence of sites and is NOT claimed. Clause (3) is not statable: it needs the geometric fibre X_ybar as an algebraic space.”.

Stacks 0CZS, clause (4). Let f : X ⟶ Y be locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation on charts and let x̄ be a geometric point of X. If F is flat at x over Y and the fibre stalk (F_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module — clause (1) — then F is finite free in an étale neighbourhood of x in X: there are an étale scheme chart φ : (U, u) → (X, x̄), a Zariski open W ⊆ U containing u and a rank r such that (φ^* F)|_W is free on r generators.

This is the source's own (1) ⟹ (4), in the reading its proof produces. Clause (1) makes the geometric stalk F_{x̄} free over 𝒪_{X, x̄} (AlgebraicGeometry.Space.free_geometricModuleStalk_of_flat_geometricFibreModuleStalk, which is Stacks 05X0 at 𝟙 X over f); that descends along the faithfully flat comparison of Stacks 05VP to freeness of the Zariski stalk (φ^* F)_u over 𝒪_{U, u} (AlgebraicGeometry.Space.free_chartZariskiModuleStalk_of_free_geometricModuleStalk); and the chart restriction is of finite presentation on the Zariski site of U, which is what AlgebraicGeometry.Space.IsFinitePresentationOnCharts says, so Stacks 0B8J spreads a basis of that stalk to a trivialization on a Zariski open neighbourhood of u. 0B8J is used through Stacks.StalkFiniteType.exists_over_iso_free_of_stalk_basis, which takes the basis over the local ring 𝒪_{U, u} rather than over the RingCat-valued stalk. The open W is itself an étale neighbourhood of x̄ in X, by AlgebraicGeometry.Space.chartOpenNeighborhood.

theorem exists_chartOpen_over_iso_free_of_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar)
    (hfibre : Module.Flat (geometricFibreLocalRing B S hS f xbar)
      (geometricFibreModuleStalk B S hS f F xbar)) :
    ∃ (N : SmallEtaleNeighborhood xbar) (W : (chartScheme N.chart).Opens)
        (_ : chartPoint B S hS X.1 N ∈ W) (r : ℕ),
      Nonempty ((restrictToChart B S hS X.2 F N.chart).over W ≅
        SheafOfModules.free (ULift.{u} (Fin r)))

AlgebraicGeometry.Space.exists_chartOpen_over_iso_free_iff_flat_geometricFibreModuleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreStalkFreeness.lean, line 858. The attribute's comment: “(1) iff (4), clause (1) in the QUOTIENT FORM F_xbar / m_ybar F_xbar over O_{X, xbar} / m_ybar O_{X, xbar} (the geometric fibre X_ybar is not constructed in this library) and clause (4) in the reading the source's proof produces: an etale SCHEME chart (U, u) over (X, xbar) with a Zariski open W of U containing u on which phi^* F becomes free on finitely many generators, the finite freeness read on the slice of the Zariski site of U at W. Identifying that slice reading with the chart restriction of F to W read on the Zariski site of W itself is an equivalence of sites and is NOT claimed; neither is the identification of clause (4) with the small-etale reading of the locus of Tag 0CZT. The (4) => (1) direction needs NONE of the source's hypotheses except quasi-coherence of F. Clause (3) is not statable: it needs the geometric fibre X_ybar as an algebraic space.”.

Stacks 0CZS, clause (1) if and only if clause (4). For f : X ⟶ Y locally of finite presentation, F a quasi-coherent 𝒪_X-module of finite presentation on charts flat at x over Y, and x̄ a geometric point of X: the fibre stalk (F_{ȳ})_{x̄} is a flat 𝒪_{X_{ȳ}, x̄}-module exactly when F becomes free on finitely many generators on a Zariski open neighbourhood of u in some étale scheme chart (U, u) of x̄.

Clause (4) is read as the source's own proof produces it, on the slice of the Zariski site of the chart at the open; identifying that with the chart restriction of F read on the Zariski site of the open itself is an equivalence of sites and is not claimed. The reverse implication uses only quasi-coherence of F.

theorem exists_chartOpen_over_iso_free_iff_flat_geometricFibreModuleStalk
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (xbar : GeometricPoint B S hS X.1)
    (hflat : IsFlatOverAtGeometricPoint B S hS f F xbar) :
    (∃ (N : SmallEtaleNeighborhood xbar) (W : (chartScheme N.chart).Opens)
        (_ : chartPoint B S hS X.1 N ∈ W) (r : ℕ),
      Nonempty ((restrictToChart B S hS X.2 F N.chart).over W ≅
        SheafOfModules.free (ULift.{u} (Fin r)))) ↔
      Module.Flat (geometricFibreLocalRing B S hS f xbar)
        (geometricFibreModuleStalk B S hS f F xbar)
Tag 0CZT, a lemma

Tag 0CZT in the Stacks Project.

AlgebraicGeometry.Space.isOpen_etaleFreeLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocus.lean, line 180. The attribute's comment: “openness”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation and let F be a finitely presented 𝒪_X-module which is flat over Y. Then the set of points of |X| at which F is free in an étale neighbourhood is open in |X|.

theorem isOpen_etaleFreeLocus {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (_hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2)
    [SheafOfModules.IsFinitePresentationOnSite F]
    (_hF : IsFlatOver B S hS X.2 f.hom F) :
    @IsOpen _ (pointTopology B S hS X.1) (etaleFreeLocus B S hS F)

AlgebraicGeometry.Space.etaleFreeLocus_modulePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusBaseChange.lean, line 327. The attribute's comment: “the base-change clause: the formation of the locus W commutes with arbitrary base change, as the EQUALITY W((g')^* F) = |g'|^(-1)(W(F)) of subsets of |X'|, at an arbitrary cartesian square of algebraic spaces over S. The openness clause is isOpen_etaleFreeLocus of Spaces/EtaleFreeLocus.lean; the two together are the whole tag. Hypotheses are the source's own and are asked DOWNSTAIRS only, of f and F: f locally of finite presentation, F quasi-coherent, F of finite presentation on the small etale site, and F flat over Y. Nothing is asked of f' or of the inverse image of F, so no stability of the hypotheses under base change is used. The test scheme T of the source is not named: the statement is at a cartesian square, of which the square of a morphism of test schemes is an instance by isPullback_baseChangeMap. Freeness is IsFreeModule, the universal-property reading on the small etale site, at an arbitrary index type.”.

Stacks 0CZT, the base-change clause. Let

X' --g'--> X
|f'        |f
v          v
Y' --g---> Y

be a cartesian square of algebraic spaces over S, let f be locally of finite presentation and let F be a quasi-coherent 𝒪_X-module of finite presentation on the small étale site which is flat over Y. Then the étale free locus of the inverse image of F on X' is the inverse image of the étale free locus of F:

W((g')^* F) = |g'|⁻¹(W(F)).

The hypotheses are asked of f and F only, which is what the source asks; nothing is required of f' or of (g')^* F, so no stability of the hypotheses under base change is used.

The inclusion ⊇ is AlgebraicGeometry.Space.preimage_etaleFreeLocus_subset and holds for an arbitrary morphism with no hypothesis. The inclusion ⊆ is the source's argument, transporting clause (1) of Stacks 0CZS across the square by AlgebraicGeometry.Space.flat_geometricFibreModuleStalk_modulePullback_iff, between the two ends exists_geometricPoint_flat_geometricFibreModuleStalk_of_mem_etaleFreeLocus and AlgebraicGeometry.Space.mem_etaleFreeLocus_of_flat_geometricFibreModuleStalk.

theorem etaleFreeLocus_modulePullback_eq
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    (hqc : F.IsQuasicoherentOnSite) (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : SheafOfModules.IsFinitePresentationOnSite F)
    (hflat : IsFlatOver B S hS X.2 f.hom F) :
    etaleFreeLocus B S hS ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' etaleFreeLocus B S hS F

AlgebraicGeometry.Space.mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusBaseChangeReverse.lean, line 77. The attribute's comment: “the reverse inclusion W' ⊆ |g'|^{-1}(W) of the base-change clause, with membership in W' read at a geometric point xbar' of X' in the source's own Zariski-chart reading of clause (4) of Stacks 0CZS -- a Zariski open of an etale SCHEME chart of X' on which the chart restriction of (g')^*F is finite free -- and W the locus of points of |X| admitting an etale morphism of algebraic spaces through them along which the inverse image of F is finite free in the sense of 03DE(2)”.

The reverse inclusion of the base-change clause. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation on charts which is flat over Y, and let

X' --g'--> X
|f'        |f
v          v
Y' --g---> Y

be a cartesian square. If the inverse image (g')^*F is finite free in an étale neighbourhood of a geometric point x̄' of X' — clause (4) of Stacks 0CZS in the source's Zariski-chart reading — then the image of x̄' in |X| lies in the finite-free étale locus of F.

theorem mem_etaleFiniteFreeLocus_of_isFiniteFreeNearGeometricPoint_modulePullback
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hfp : IsFinitePresentationOnCharts B S hS X.2 F)
    (hF : IsFlatOver B S hS X.2 f.hom F) (xbar' : GeometricPoint B S hS X'.1)
    (h : IsFiniteFreeNearGeometricPoint B S hS xbar' ((modulePullback B S hS g').obj F)) :
    pointsMap B S hS X'.1 g'.hom xbar'.image ∈ etaleFiniteFreeLocus B S hS F

AlgebraicGeometry.Space.etaleFreeLocus_modulePullback_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFreeLocusFinitePresentation.lean, line 331. The attribute's comment: “the base-change clause: the etale free locus of (g')^*F on |X'| is the preimage under |g'| of the etale free locus of F on |X|, at the PLAIN-FREENESS locus the source defines and the openness clause carries, with finite presentation of F read on the small etale site”.

The base-change clause for the étale free locus. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation, let F be a quasi-coherent 𝒪_X-module of finite presentation on charts which is flat over Y, and let

X' --g'--> X
|f'        |f
v          v
Y' --g---> Y

be a cartesian square. Then the étale free locus of the inverse image (g')^*F on |X'| is the inverse image under |g'| of the étale free locus of F on |X|.

The locus is AlgebraicGeometry.Space.etaleFreeLocus, the plain-freeness locus by which the source defines it, and finite presentation of F is taken on the small étale site.

theorem etaleFreeLocus_modulePullback_eq_preimage_of_isPullback
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    [SheafOfModules.IsFinitePresentationOnSite F]
    (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (hF : IsFlatOver B S hS X.2 f.hom F) :
    etaleFreeLocus B S hS ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' etaleFreeLocus B S hS F
Sources
LeanAlgebraicGeometry.Space.exists_chartPoint_isFibreFlatOnChartSquares_iff_isFibreFlatOverAtGeometricPoint · AlgebraicGeometry.Space.isFibreFlatOverAtGeometricPoint_congr_of_image_eq · AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint · AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint_of_image_eq · AlgebraicGeometry.Space.isFlatOverAtPoint_fieldFibreSpace_iff_isFibreFlatOverAtGeometricPoint · AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_fieldFibreSpace_iff_exists_chartPoint · AlgebraicGeometry.Space.isFlatOnFibreAtFieldValuedPoint_iff_isFibreFlatOverAtGeometricPoint · AlgebraicGeometry.Space.exists_flatQuotSMul_chart_iff_isFibreFlatOverAtGeometricPoint

Section76.24 Flatness over a Noetherian base#

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

Tag 0APR, a theorem

Tag 0APR in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_and_isFlatOnFibre_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleNoetherianFibreCriterion.lean, line 128. The attribute's comment: “The full equivalence, at a geometric point x̄ of X: condition (1) is flatness of F over Z at x̄ (condition (2) of Stacks 05VU for X ⟶ Z) together with the fibre condition read on geometric stalks as in part (1) of Stacks 05WY, and condition (2) is flatness of Y over Z at the image point of ȳ together with flatness of F over Y at x̄. Local Noetherianity of X, Y, Z is the étale-local scheme property; coherence of F is used only through finiteness of F_{x̄} over 𝒪_{X, x̄}, which is hypothesised, so quasi-coherence of F is not assumed. NOT covered: the identification of the fibre condition with flatness of a pullback of F to a genuine fibre product over a field-valued representative of z̄, which is Stacks 05WY.”.

Stacks 0APR. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over S with X, Y, Z locally Noetherian, let F be an 𝒪_X-module and let x̄ be a geometric point of X whose geometric stalk F_{x̄} is a nonzero finite 𝒪_{X, x̄}-module. Then F is flat over Z at x̄ and flat on the fibre over z̄ relative to the fibre of Y exactly when Y is flat over Z at ȳ and F is flat over Y at x̄.

Over the étale local rings 𝒪_{Z, z̄} → 𝒪_{Y, ȳ} → 𝒪_{X, x̄} this is Stacks 00MP in one direction, and transitivity of flatness together with base change along 𝒪_{Y, ȳ} → 𝒪_{Y, ȳ}/𝔪_{z̄}𝒪_{Y, ȳ} in the other.

theorem isFlatOverAtGeometricPoint_and_isFlatOnFibre_iff {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (F : Modules.{u, m} B S hS X.1 X.2)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hZ : HasEtaleLocalProperty B S hS Z.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (xbar : GeometricPoint B S hS X.1)
    (hfin : Module.Finite (etaleLocalRing B S hS X.1 xbar)
      (geometricModuleStalk B S hS X xbar F))
    (hne : Nontrivial (geometricModuleStalk B S hS X xbar F)) :
    (IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar ∧
        IsFlatOnFibreAtGeometricPoint B S hS f g F xbar) ↔
      (IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image ∧
        IsFlatOverAtGeometricPoint B S hS f F xbar)

AlgebraicGeometry.Space.isFlatOverAtPoint_comp_and_isFlatOnFibreAtFieldValuedPoint_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleNoetherianFibreCriterionFibreProduct.lean, line 89. The attribute's comment: “The full statement: flatness of F over Z and over Y at x is the definition of Stacks 05VV (IsFlatOverAtPoint), flatness of Y over Z at y is that of Stacks 03ML, and the fibre clause is flatness of the pullback of F to the fibre product Spec(K) x_Z X over Spec(K) x_Z Y at the K-point, for every field-valued representative of x (condition (2) of Stacks 05WY); F is coherent and X, Y, Z are locally Noetherian.”.

Stacks 0APR. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally Noetherian algebraic spaces over S, let F be a coherent 𝒪_X-module and let x ∈ |X|, with image y ∈ |Y|. Suppose F_{x̄} ≠ 0 for a geometric point x̄ of X over x. Then for every field-valued point Spec(K) ⟶ X in the class of x the following are equivalent:

  1. F is flat over Z at x, and the pullback of F to the fibre X_z = Spec(K) ×_Z X over the image z of the point is flat over Y_z = Spec(K) ×_Z Y at the K-rational point of X_z;
  2. Y is flat over Z at y, and F is flat over Y at x.

Flatness at a point is the definition of Stacks 05VV for modules and of Stacks 03ML for morphisms.

theorem isFlatOverAtPoint_comp_and_isFlatOnFibreAtFieldValuedPoint_iff
    {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) [IsCoherent B S hS X.1 X.2 F]
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hZ : HasEtaleLocalProperty B S hS Z.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (x : points B S hS X.1) (xbar : GeometricPoint B S hS X.1) (hxbar : xbar.LiesOver x)
    (hne : Nontrivial (geometricModuleStalk B S hS X xbar F))
    (p : FieldValuedPoint B S hS X.1) (hp : p.class B S hS X.1 = x) :
    (IsFlatOverAtPoint B S hS X.2 (f ≫ g).hom F x ∧
        IsFlatOnFibreAtFieldValuedPoint B S hS f g p F) ↔
      (IsFlatAt B S hS g.hom (pointsMap B S hS X.1 f.hom x) ∧
        IsFlatOverAtPoint B S hS X.2 f.hom F x)
Tag 0APS, a lemma

Tag 0APS in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_flatFibreCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatFibrewiseCriterion.lean, line 208. The attribute's comment: “conclusion (A): flatness of the morphism; hypothesis (3) in its every-étale-chart reading AlgebraicGeometry.Space.HasFlatFibreCharts”.

Stacks Project, Tag 0APS, conclusion (A). Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over a scheme S. If X, Y, Z are locally Noetherian, X is flat over Z, and the fibres of X over the points of Z are flat over the corresponding fibres of Y in the chart sense of AlgebraicGeometry.Space.HasFlatFibreCharts, then f is flat.

theorem isFlat_of_flatFibreCharts
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hXn : HasEtaleLocalProperty B S hS X
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hYn : HasEtaleLocalProperty B S hS Y
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hZn : HasEtaleLocalProperty B S hS Z
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hflat : IsFlat B S hS (f ≫ g)) (hfib : HasFlatFibreCharts B S hS f g) :
    IsFlat B S hS f

AlgebraicGeometry.Space.isFlat_of_flatFibreCharts_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatFibrewiseCriterion.lean, line 230. The attribute's comment: “conclusion (B): flatness of the target over the base for surjective f; hypothesis (3) in its every-étale-chart reading AlgebraicGeometry.Space.HasFlatFibreCharts”.

Stacks Project, Tag 0APS, conclusion (B). In the situation of AlgebraicGeometry.Space.isFlat_of_flatFibreCharts, if f is in addition surjective then Y is flat over Z.

theorem isFlat_of_flatFibreCharts_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hXn : HasEtaleLocalProperty B S hS X
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hYn : HasEtaleLocalProperty B S hS Y
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hZn : HasEtaleLocalProperty B S hS Z
      (fun A : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian A))
    (hflat : IsFlat B S hS (f ≫ g)) (hfib : HasFlatFibreCharts B S hS f g)
    (hfs : IsSurjective B S hS f) :
    IsFlat B S hS g
Tag 08VP, a lemma

Tag 08VP in the Stacks Project.

AlgebraicGeometry.Space.isOpen_flatLocus_and_preimage_subset_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatLocusAdicThickenings.lean, line 576.

Stacks 08VP. Let A be a Noetherian ring, I ⊆ A an ideal, and X an algebraic space locally of finite presentation over S = Spec A. For n ≥ 0 let Xₙ = Spec(A/Iⁿ⁺¹) ×_S X be the adic fibres, and let F be a coherent 𝒪_X-module whose pullback Fₙ to every Xₙ is flat over Spec(A/Iⁿ⁺¹). Then the locus of points of |X| where F is flat over S is open, and it contains the inverse image of V(I) = |Spec(A/I)| under |X| ⟶ |S|.

The source's thickenings are indexed by n ≥ 1 and are Spec(A/Iⁿ); here they are indexed by n ≥ 0 and are Spec(A/Iⁿ⁺¹), the convention of AlgebraicGeometry.Space.adicFibre. The flatness of Fₙ is Stacks 05VV for the projection Xₙ ⟶ Spec(A/Iⁿ⁺¹), and the flat locus is AlgebraicGeometry.Space.flatLocus of Stacks 05VV (1). Openness is Stacks 05WV.

At a geometric point x̄ above V(I) the proof follows the source's reduction to Stacks 0523, carried out on étale local rings rather than on an affine étale chart: x̄ lifts to every Xₙ, flatness of the stalks of Fₙ gives flatness of (A/Iⁿ⁺¹) ⊗_A F_{x̄} over A/Iⁿ⁺¹ (AlgebraicGeometry.Space.flat_quotient_tensor_geometricModuleStalk), and Stacks 0523 over the Noetherian ring A, applied to the finite module F_{x̄} over the Noetherian local ring 𝒪_{X, x̄}, gives flatness over A, hence over the weakly étale A-algebra 𝒪_{S, ȳ}.

theorem isOpen_flatLocus_and_preimage_subset_flatLocus [IsNoetherianRing A]
    (X : AlgebraicSpaces B (Spec (.of A)) hA) (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsLocallyOfFinitePresentation B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (hflat : ∀ n : ℕ, IsFlatOver B (Spec (.of A)) hA (adicFibreSpaceOf A I B hA X f n).2
      (adicFibreProjection A I B hA X f n).hom
      ((modulePullback B (Spec (.of A)) hA (adicFibreInclusion A I B hA X f n)).obj F)) :
    IsOpen (flatLocus B (Spec (.of A)) hA X.2 f.hom F) ∧
      pointsMap B (Spec (.of A)) hA X.1 f.hom ⁻¹'
          Set.range (pointsMap B (Spec (.of A)) hA
            (yoneda.obj (adicThickeningObject A I B hA (contains_adicThickening A I B hA) 0))
            (yoneda.map (adicThickeningMap A I B hA (contains_adicThickening A I B hA) 0))) ⊆
        flatLocus B (Spec (.of A)) hA X.2 f.hom F

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_flat_quotient_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAdicThickenings.lean, line 116. The attribute's comment: “the local step at a geometric point lying over V(J)”.

The local step of Stacks 08VP. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be an 𝒪_X-module and let x̄ be a geometric point of X whose étale local ring T = 𝒪_{X, x̄} and whose image's étale local ring R = 𝒪_{Y, ȳ} are Noetherian, with geometric stalk M = F_{x̄} finite over T. Let J ⊆ R be an ideal whose image in T is a proper ideal, which is the condition that x̄ lies over V(J). If M/JⁿM is flat over R/Jⁿ for every n ≥ 1, then F is flat over Y at x̄.

The scalars of M over R are restricted along the canonical homomorphism of étale local rings AlgebraicGeometry.Space.etaleLocalRingMap of Stacks 04NG, as they are in the conclusion AlgebraicGeometry.Space.IsFlatOverAtGeometricPoint.

The statement does not include the openness of the flat locus (Stacks 05WV), the identification of the hypothesis with flatness of the pullbacks F_n to the thickenings X_n (Stacks 05VQ), or the passage from the base ring A and its ideal I to the étale local ring of the base.

theorem isFlatOverAtGeometricPoint_of_flat_quotient_pow
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, m} B S hS X.1 X.2) (xbar : GeometricPoint B S hS X.1)
    [IsNoetherianRing (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))]
    [IsNoetherianRing (etaleLocalRing B S hS X.1 xbar)]
    [Module.Finite (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F)]
    (J : Ideal (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar)))
    (hJ : J.map (etaleLocalRingMap X.2 f.hom xbar) ≠ ⊤)
    (hflat : ∀ n : ℕ, 1 ≤ n →
      letI : Module (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
          (geometricModuleStalk B S hS X xbar F) :=
        Module.compHom _ (etaleLocalRingMap X.2 f.hom xbar)
      Module.Flat (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar) ⧸ J ^ n)
        (geometricModuleStalk B S hS X xbar F ⧸
          (J ^ n • (⊤ : Submodule (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
            (geometricModuleStalk B S hS X xbar F))))) :
    IsFlatOverAtGeometricPoint B S hS f F xbar

AlgebraicGeometry.Space.preimage_zeroLocus_subset_flatLocus_of_isFlatOver_adicFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAdicThickeningsFibre.lean, line 601.

Stacks 08VP. Let A be a Noetherian ring, let I ⊆ A be an ideal and let X be an algebraic space locally of finite presentation over S = Spec A. For n ≥ 1 set S_n = Spec (A / Iⁿ) and X_n = S_n ×_S X, and let F be a coherent 𝒪_X-module. If for every n ≥ 1 the pullback F_n of F to X_n is flat over S_n, then the locus where F is flat over S is open and contains the inverse image of V(I) under X → S.

The openness is Stacks 05WV, AlgebraicGeometry.Space.isOpen_flatLocus_of_isFinitePresentationOnCharts, a coherent module being of finite presentation. Here X_n is AlgebraicGeometry.Space.adicFibreSpace, the fibre product of algebraic spaces X ×_S S_n with S_n = Spec (A / I^{n+1}) for n : ℕ, so that n runs over the exponents ≥ 1; F_n is the pullback of modules AlgebraicGeometry.Space.modulePullback along the projection AlgebraicGeometry.Space.adicFibreFst; flatness over S_n is AlgebraicGeometry.Space.IsFlatOver of Stacks 05VV along AlgebraicGeometry.Space.adicFibreSnd; coherence is AlgebraicGeometry.Space.IsCoherent of Stacks 07UA; and the locus is AlgebraicGeometry.Space.flatLocus.

theorem preimage_zeroLocus_subset_flatLocus_of_isFlatOver_adicFibre [IsNoetherianRing A]
    (hf : IsLocallyOfFinitePresentation B (Spec (.of A)) hA f)
    (F : Modules.{u, u} B (Spec (.of A)) hA X hX) [IsCoherent B (Spec (.of A)) hA X hX F]
    (hflat : ∀ n : ℕ, IsFlatOver B (Spec (.of A)) hA (adicFibreSpace A I B hA hX f n).2
      (adicFibreSnd A I B hA f n)
      ((modulePullback B (Spec (.of A)) hA (adicFibreFst A I B hA hX f n)).obj F)) :
    IsOpen (flatLocus B (Spec (.of A)) hA hX f F) ∧
      (fun x => pointsToScheme B (Spec (.of A)) hA (baseObject A B hA)
          (pointsMap B (Spec (.of A)) hA X f x)) ⁻¹'
        PrimeSpectrum.zeroLocus (I : Set A) ⊆
        flatLocus B (Spec (.of A)) hA hX f F
Sources
LeanAlgebraicGeometry.Space.isFlatOverAtGeometricPoint_and_isFlatOnFibre_iff · AlgebraicGeometry.Space.isFlatOverAtPoint_comp_and_isFlatOnFibreAtFieldValuedPoint_iff · AlgebraicGeometry.Space.isFlat_of_flatFibreCharts · AlgebraicGeometry.Space.isFlat_of_flatFibreCharts_of_isSurjective · AlgebraicGeometry.Space.isOpen_flatLocus_and_preimage_subset_flatLocus · AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_flat_quotient_pow · AlgebraicGeometry.Space.preimage_zeroLocus_subset_flatLocus_of_isFlatOver_adicFibre

Section76.25 Normalization revisited#

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

Tag 082E, a lemma

Tag 082E in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_algebraPullback_integralClosureSheaf_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralClosureSmoothPullbackUnconditional.lean, line 243. References: SGA 3 X (8.9), “partial”.

Stacks 082E. Let f : Y ⟶ X be a smooth morphism of algebraic spaces over S and let A be a quasi-coherent sheaf of commutative 𝒪_X-algebras. The integral closure of 𝒪_Y in f^*A is f^*A', where A' ⊆ A is the integral closure of 𝒪_X in A: there is an isomorphism f^*A' ≅ (f^*A)' of algebra sheaves on Y whose composite with the inclusion of (f^*A)' into f^*A is the pullback of the inclusion of A' into A.

theorem exists_iso_algebraPullback_integralClosureSheaf_unconditional (f : Y ⟶ X)
    (hf : IsSmooth B S hS f.hom)
    (A : AlgebraSheaf.{u, u} B S hS X.1 X.2) (hA : A.IsQuasicoherent) :
    ∃ e : (algebraPullback B S hS f).obj (AlgebraSheaf.integralClosureSheaf A) ≅
        AlgebraSheaf.integralClosureSheaf ((algebraPullback B S hS f).obj A),
      e.hom ≫ AlgebraSheaf.integralClosureInclusion ((algebraPullback B S hS f).obj A) =
        (algebraPullback B S hS f).map (AlgebraSheaf.integralClosureInclusion A)
Tag 082F, a lemma

Tag 082F in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeNormalization.existsUnique_iso_baseChange_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInSmoothBaseChange.lean, line 174. The attribute's comment: “X₂' ≅ X₂ ×_{X₁} X₁' for f qcqs and φ smooth, for normalizations given by the universal property of Tag 0823”.

Stacks 082F. Let Y₂ = X₂ ×_{X₁} Y₁ be a fibre square of algebraic spaces over S with f : Y₁ ⟶ X₁ quasi-compact and quasi-separated and φ : X₂ ⟶ X₁ smooth, and let Yᵢ ⟶ Xᵢ' ⟶ Xᵢ be the normalization of Xᵢ in Yᵢ (Stacks 0823). Then X₂' ≅ X₂ ×_{X₁} X₁', by a unique isomorphism compatible with the two factorizations of f₂ and with the two morphisms to X₂.

theorem existsUnique_iso_baseChange_of_isSmooth
    (hnorm₁ : IsRelativeNormalization B S hS f ν₁ f₁')
    (hnorm₂ : IsRelativeNormalization B S hS f₂ ν₂ f₂')
    (hX₁ : IsAlgebraicSpace B S hS X₁) (hX₂ : IsAlgebraicSpace B S hS X₂)
    (hY₁ : IsAlgebraicSpace B S hS Y₁) (hX₁' : IsAlgebraicSpace B S hS X₁')
    (hX₂' : IsAlgebraicSpace B S hS X₂')
    (hfqc : IsQuasiCompact B S hS f) (hfqs : IsQuasiSeparated B S hS f)
    (hφ : IsSmooth B S hS φ)
    (sq : IsPullback g f₂ f φ) (sqP : IsPullback p q φ ν₁) :
    ∃! e : X₂' ≅ P, f₂' ≫ e.hom = hnorm₁.baseChangeFactorization sq sqP ∧ e.hom ≫ p = ν₂

AlgebraicGeometry.Space.existsUnique_iso_normalizationInQcqs_baseChange_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInSmoothBaseChange.lean, line 203. The attribute's comment: “X₂' ≅ X₂ ×_{X₁} X₁' for f qcqs and φ smooth, for the normalizations of Tag 0822”.

Stacks 082F, for the normalizations of Stacks 0822. Let Y₂ = X₂ ×_{X₁} Y₁ be a fibre square of algebraic spaces over S with f : Y₁ ⟶ X₁ quasi-compact and quasi-separated and φ : X₂ ⟶ X₁ smooth, and let P = X₂ ×_{X₁} X₁' for X₁' the normalization of X₁ in Y₁, with f₂P : Y₂ ⟶ P the base change of Y₁ ⟶ X₁'. Then f₂ : Y₂ ⟶ X₂ is quasi-compact and quasi-separated, and the normalization X₂' of X₂ in Y₂ is isomorphic to P by a unique isomorphism compatible with the two factorizations of f₂ and the two morphisms to X₂.

theorem existsUnique_iso_normalizationInQcqs_baseChange_of_isSmooth (f : Y₁ ⟶ X₁)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    {φ : X₂ ⟶ X₁} (hφ : IsSmooth B S hS φ.hom) {g : Y₂ ⟶ Y₁} {f₂ : Y₂ ⟶ X₂}
    (sq : IsPullback g f₂ f φ) {p : P ⟶ X₂} {q : P ⟶ normalizationInQcqs B S hS f hfqc hfqs}
    (sqP : IsPullback p q φ (normalizationInQcqsHom B S hS f hfqc hfqs)) {f₂P : Y₂ ⟶ P}
    (h₁ : f₂P ≫ q = g ≫ toNormalizationInQcqs f hfqc hfqs) (h₂ : f₂P ≫ p = f₂) :
    ∃ (hqc₂ : IsQuasiCompact B S hS f₂.hom) (hqs₂ : IsQuasiSeparated B S hS f₂.hom),
      ∃! e : (normalizationInQcqs B S hS f₂ hqc₂ hqs₂).1 ≅ P.1,
        (toNormalizationInQcqs f₂ hqc₂ hqs₂).hom ≫ e.hom = f₂P.hom ∧
          e.hom ≫ p.hom = (normalizationInQcqsHom B S hS f₂ hqc₂ hqs₂).hom

AlgebraicGeometry.Space.IsRelativeNormalization.existsUnique_baseChangeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationSmoothBaseChange.lean, line 166. The attribute's comment: “the morphism h of the proof: the base change X₂ ×_{X₁} X₁' ⟶ X₂ is integral and f₂ factors through it, so the universal property of Tag 0823 supplies a unique h”.

Stacks 082F, the morphism h. The base change X₂ ×_{X₁} X₁' ⟶ X₂ is an integral morphism through which f₂ factors, so the universal property of the normalization X₂' of X₂ in Y₂ supplies a unique morphism h : X₂' ⟶ X₂ ×_{X₁} X₁' compatible with the two factorizations of f₂ and with the two morphisms to X₂.

theorem existsUnique_baseChangeComparison
    (hnorm₁ : IsRelativeNormalization B S hS f ν₁ f₁')
    (hnorm₂ : IsRelativeNormalization B S hS f₂ ν₂ f₂')
    (hX₁ : IsAlgebraicSpace B S hS X₁) (hX₂ : IsAlgebraicSpace B S hS X₂)
    (hX₁' : IsAlgebraicSpace B S hS X₁')
    (sq : IsPullback g f₂ f φ) (sqP : IsPullback p q φ ν₁) :
    ∃! h : X₂' ⟶ P, f₂' ≫ h = hnorm₁.baseChangeFactorization sq sqP ∧ h ≫ p = ν₂
Sources
LeanAlgebraicGeometry.Space.exists_iso_algebraPullback_integralClosureSheaf_unconditional · AlgebraicGeometry.Space.IsRelativeNormalization.existsUnique_iso_baseChange_of_isSmooth · AlgebraicGeometry.Space.existsUnique_iso_normalizationInQcqs_baseChange_of_isSmooth · AlgebraicGeometry.Space.IsRelativeNormalization.existsUnique_baseChangeComparison

Section76.26 Cohen-Macaulay morphisms#

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

Tag 0E0U, a lemma

Tag 0E0U in the Stacks Project.

AlgebraicGeometry.hasCohenMacaulayFiberLocalRing_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/CohenMacaulayFiber.lean, line 434.

Having a Noetherian and Cohen–Macaulay local ring of the fibre is étale local on the source and target germs.

public theorem hasCohenMacaulayFiberLocalRing_isEtaleLocalOnSourceAndTarget :
    MorphismOfGerms.IsEtaleLocalOnSourceAndTarget
      (@HasCohenMacaulayFiberLocalRing.{u})
Tag 0E0V, a definition

Tag 0E0V in the Stacks Project.

AlgebraicGeometry.Space.IsCohenMacaulayAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Defs.lean, line 38. The attribute's comment: “part (1): at a point”.

A morphism of algebraic spaces over S is Cohen–Macaulay at a point x of its source when it is flat at x and the local ring of its fibre is Noetherian and Cohen–Macaulay in every pointed étale scheme chart at x.

abbrev IsCohenMacaulayAt (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (x : points B S hS X) : Prop

AlgebraicGeometry.Space.IsCohenMacaulay, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Defs.lean, line 46. The attribute's comment: “part (2): morphism”.

A morphism of algebraic spaces over S is Cohen–Macaulay when it is Cohen–Macaulay at every point of its source.

abbrev IsCohenMacaulay (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop
Tag 0E0W, a lemma

Tag 0E0W in the Stacks Project.

AlgebraicGeometry.Space.HasCohenMacaulayFibersOnChart, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/EtaleCharts.lean, line 186. The attribute's comment: “the fibre condition on an étale scheme chart of the target”.

Stacks 0E0W. The fibres of f over the points of the étale scheme chart g : h_V ⟶ Y are Cohen–Macaulay algebraic spaces.

abbrev HasCohenMacaulayFibersOnChart {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y) : Prop

AlgebraicGeometry.Space.isCohenMacaulay_tfae_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/EtaleCharts.lean, line 471. The attribute's comment: “equivalence of conditions (1), (2) and (3)”.

Stacks 0E0W. For a morphism of algebraic spaces over S with locally Noetherian fibres, Cohen–Macaulayness is equivalent to flatness together with Cohen–Macaulayness of the fibres after some, equivalently after every, étale scheme chart of the target.

theorem isCohenMacaulay_tfae_etaleCharts (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : HasLocallyNoetherianFibers B S hS f) :
    List.TFAE [
      IsCohenMacaulay B S hS f,
      IsFlat B S hS f ∧
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          (MorphismProperty.presheaf (MorphismProperty.inverseImage
            (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS))) g ∧
          IsEtale B S hS g ∧ HasCohenMacaulayFibersOnChart B S hS f V g,
      IsFlat B S hS f ∧
        ∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsEtale B S hS g → HasCohenMacaulayFibersOnChart B S hS f V g]

AlgebraicGeometry.Space.isCohenMacaulayAt_iff_etaleLocalRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/EtaleCharts.lean, line 926. The attribute's comment: “equivalence of conditions (a) and (b)”.

Stacks 0E0W. A morphism of algebraic spaces over S is Cohen–Macaulay at the image of a geometric point x of its source exactly when the canonical homomorphism of étale local rings at x is flat and its local fibre ring is Noetherian, local and Cohen–Macaulay.

theorem isCohenMacaulayAt_iff_etaleLocalRingMap (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (x : GeometricPoint B S hS X) :
    IsCohenMacaulayAt B S hS f x.image ↔
      ((etaleLocalRingMap hX f x).Flat ∧
        ∃ (hN : IsNoetherianRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x))
          (hL : IsLocalRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x)),
          @IsCohenMacaulayLocalRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x) _ hN hL)
Tag 0E0X, a lemma

Tag 0E0X in the Stacks Project.

AlgebraicGeometry.Space.isCohenMacaulayAt_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 85. The attribute's comment: “part (1)”. References: EGA IV (6.6.1), “a) of (i)”; EGA IV (6.8.3), “(i), Cohen-Macaulay”.

Stacks 0E0X, part (1). The composite of two morphisms of algebraic spaces with locally Noetherian fibres is Cohen–Macaulay at a point of its source as soon as the first is Cohen–Macaulay there and the second is Cohen–Macaulay at the image of that point.

theorem isCohenMacaulayAt_comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hfx : IsCohenMacaulayAt B S hS f x)
    (hgy : IsCohenMacaulayAt B S hS g (pointsMap B S hS X f x)) :
    IsCohenMacaulayAt B S hS (f ≫ g) x

AlgebraicGeometry.Space.isCohenMacaulay_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 106. The attribute's comment: “part (2)”.

Stacks 0E0X, part (2). The composite of two Cohen–Macaulay morphisms of algebraic spaces with locally Noetherian fibres is Cohen–Macaulay.

theorem isCohenMacaulay_comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hfm : IsCohenMacaulay B S hS f) (hgm : IsCohenMacaulay B S hS g) :
    IsCohenMacaulay B S hS (f ≫ g)

AlgebraicGeometry.Space.isCohenMacaulayAt_left_of_comp_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 146. The attribute's comment: “part (3), first conclusion”.

Stacks 0E0X, part (3), first conclusion. If the composite is Cohen–Macaulay at x and the first morphism is flat at x, then the first morphism is Cohen–Macaulay at x.

theorem isCohenMacaulayAt_left_of_comp_of_isFlatAt
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hcomp : IsCohenMacaulayAt B S hS (f ≫ g) x)
    (hflat : IsFlatAt B S hS f x) : IsCohenMacaulayAt B S hS f x

AlgebraicGeometry.Space.isCohenMacaulayAt_right_of_comp_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 160. The attribute's comment: “part (3), second conclusion”.

Stacks 0E0X, part (3), second conclusion. If the composite is Cohen–Macaulay at x and the first morphism is flat at x, then the second morphism is Cohen–Macaulay at the image of x.

theorem isCohenMacaulayAt_right_of_comp_of_isFlatAt
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hcomp : IsCohenMacaulayAt B S hS (f ≫ g) x)
    (hflat : IsFlatAt B S hS f x) :
    IsCohenMacaulayAt B S hS g (pointsMap B S hS X f x)

AlgebraicGeometry.Space.isCohenMacaulay_left_of_comp_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 174. The attribute's comment: “part (4), first conclusion”.

Stacks 0E0X, part (4), first conclusion. If the composite is Cohen–Macaulay and the first morphism is flat, then the first morphism is Cohen–Macaulay.

theorem isCohenMacaulay_left_of_comp_of_isFlat
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hcomp : IsCohenMacaulay B S hS (f ≫ g)) (hflat : IsFlat B S hS f) :
    IsCohenMacaulay B S hS f

AlgebraicGeometry.Space.isCohenMacaulayAt_right_of_comp_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/Composition.lean, line 191. The attribute's comment: “part (4), second conclusion”. References: EGA IV (6.6.1), “a) of (ii)”; EGA IV (6.8.3), “(ii), Cohen-Macaulay”.

Stacks 0E0X, part (4), second conclusion. If the composite is Cohen–Macaulay and the first morphism is flat, then the second morphism is Cohen–Macaulay at every point in the image of the first.

theorem isCohenMacaulayAt_right_of_comp_of_isFlat
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hcomp : IsCohenMacaulay B S hS (f ≫ g)) (hflat : IsFlat B S hS f)
    (x : points B S hS X) :
    IsCohenMacaulayAt B S hS g (pointsMap B S hS X f x)
Tag 0E0Y, a lemma

Tag 0E0Y in the Stacks Project.

AlgebraicGeometry.Space.isCohenMacaulay_of_isCohenMacaulay_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/Source.lean, line 212. The attribute's comment: “the morphism is Cohen-Macaulay”.

Stacks 0E0Y. A flat morphism of locally Noetherian algebraic spaces over S whose source is a Cohen–Macaulay algebraic space is a Cohen–Macaulay morphism.

theorem isCohenMacaulay_of_isCohenMacaulay_source (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hNX : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hNY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hCM : HasEtaleLocalProperty B S hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsCohenMacaulay T))
    (f : X ⟶ Y) (hf : IsFlat B S hS f) :
    IsCohenMacaulay B S hS f

AlgebraicGeometry.Space.isCohenMacaulayLocalRing_etaleLocalRing_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/Source.lean, line 385. The attribute's comment: “the target étale local rings are Cohen-Macaulay”.

Stacks 0E0Y. For a flat morphism of locally Noetherian algebraic spaces over S whose source is a Cohen–Macaulay algebraic space, the étale local ring of the target at the image of any geometric point of the source is Cohen–Macaulay.

theorem isCohenMacaulayLocalRing_etaleLocalRing_target (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hNX : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hNY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hCM : HasEtaleLocalProperty B S hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsCohenMacaulay T))
    (f : X ⟶ Y) (hf : IsFlat B S hS f) (x : GeometricPoint B S hS X) :
    letI : IsLocalRing (etaleLocalRing B S hS Y (geometricPointMap f x)) :=
      isLocalRing_etaleLocalRing B S hS Y hY (geometricPointMap f x)
    letI : IsNoetherianRing (etaleLocalRing B S hS Y (geometricPointMap f x)) :=
      isNoetherianRing_etaleLocalRing_of_isLocallyNoetherian B S hS Y hY hNY
        (geometricPointMap f x)
    IsCohenMacaulayLocalRing (etaleLocalRing B S hS Y (geometricPointMap f x))
Tag 0E0Z, a lemma

Tag 0E0Z in the Stacks Project.

AlgebraicGeometry.Space.isCohenMacaulayAt_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/BaseChange.lean, line 209. The attribute's comment: “part (1)”. References: EGA IV (6.8.3), “(iii) CM, h loc fin type”.

Stacks 0E0Z, part (1). Cohen–Macaulayness of a morphism of algebraic spaces with locally Noetherian fibres at a point is preserved by base change along a morphism locally of finite type.

theorem isCohenMacaulayAt_pullback_snd
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hcm : IsCohenMacaulayAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')) :
    IsCohenMacaulayAt B S hS (pullback.snd f g) x'

AlgebraicGeometry.Space.isCohenMacaulayAt_of_pullback_snd_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/BaseChange.lean, line 227. The attribute's comment: “part (2)”.

Stacks 0E0Z, part (2). Cohen–Macaulayness descends from the base change when the original morphism is flat at the point in question.

theorem isCohenMacaulayAt_of_pullback_snd_of_isFlatAt
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hflat : IsFlatAt B S hS f (pointsMap B S hS (pullback f g) (pullback.fst f g) x'))
    (hcm : IsCohenMacaulayAt B S hS (pullback.snd f g) x') :
    IsCohenMacaulayAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')

AlgebraicGeometry.Space.isCohenMacaulayAt_of_pullback_snd_of_isFlatAt_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulay/BaseChange.lean, line 251. The attribute's comment: “part (3)”. References: EGA IV (6.8.3), “(iii) converse, CM”.

Stacks 0E0Z, part (3). Cohen–Macaulayness descends from the base change when the base morphism is flat at the corresponding point.

theorem isCohenMacaulayAt_of_pullback_snd_of_isFlatAt_base
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hflat : IsFlatAt B S hS g (pointsMap B S hS (pullback f g) (pullback.snd f g) x'))
    (hcm : IsCohenMacaulayAt B S hS (pullback.snd f g) x') :
    IsCohenMacaulayAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')
Tag 0E10, a lemma

Tag 0E10 in the Stacks Project.

AlgebraicGeometry.Space.isOpen_setOf_isCohenMacaulayAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/Locus.lean, line 136. The attribute's comment: “openness of the Cohen–Macaulay locus”. References: EGA IV (12.1.1), “(vi), F = O_X”.

Stacks 0E10. The Cohen–Macaulay locus of a flat morphism of algebraic spaces over S which is locally of finite presentation is open in the canonical topology of Tag 03BX on the point space of its source.

theorem isOpen_setOf_isCohenMacaulayAt {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf_flat : IsFlat B S hS f) (hf_lfp : IsLocallyOfFinitePresentation B S hS f) :
    IsOpen {x : points B S hS X | IsCohenMacaulayAt B S hS f x}

AlgebraicGeometry.Space.isCohenMacaulayAt_pullback_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/Locus.lean, line 165. The attribute's comment: “base change of the Cohen–Macaulay locus”. References: EGA IV (6.8.2), “(ii)”.

Stacks 0E10. The Cohen–Macaulay locus of a flat morphism of algebraic spaces over S which is locally of finite presentation commutes with arbitrary base change: the locus of the base change X ×_Y Y' ⟶ Y' is the inverse image of the locus of f : X ⟶ Y under the projection to X.

theorem isCohenMacaulayAt_pullback_locus {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y' ⟶ Y) (hf_flat : IsFlat B S hS f.hom)
    (hf_lfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    {x' : points B S hS (pullback f.hom g.hom) |
        IsCohenMacaulayAt B S hS (pullback.snd f.hom g.hom) x'} =
      pointsMap B S hS (pullback f.hom g.hom) (pullback.fst f.hom g.hom) ⁻¹'
        {x : points B S hS X.1 | IsCohenMacaulayAt B S hS f.hom x}
Tag 0E11, a lemma

Tag 0E11 in the Stacks Project.

AlgebraicGeometry.Space.exists_clopen_relativeDimension_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohenMacaulay/RelativeDimensionDecomposition.lean, line 278.

Stacks 0E11. A locally finitely presented Cohen–Macaulay morphism of algebraic spaces over S decomposes its source into open-and-closed subspaces of constant relative dimension: there is a family Xd : ℕ → Subfunctor X of subfunctors which are both open and closed subspaces of X in the sense of Tag 02YU, whose point sets cover the point space of X and are pairwise disjoint, and such that the restriction of f to the d-th piece has relative dimension d.

The pieces are given by their point sets rather than by a supremum of subfunctors: the ranges of their inclusions are subpresheaves, so a section over a test object which the decomposition splits into several pieces lies in no single piece before refinement.

theorem exists_clopen_relativeDimension_decomposition (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hfp : IsLocallyOfFinitePresentation B S hS f) (hCM : IsCohenMacaulay B S hS f) :
    ∃ Xd : ℕ → Subfunctor X,
      (∀ d : ℕ, IsOpenSubspace B S hS (Xd d) ∧ IsClosedSubspace B S hS (Xd d)) ∧
      (∀ x : points B S hS X, ∃ d : ℕ,
        x ∈ Set.range (pointsMap B S hS (Xd d).toFunctor (Xd d).ι)) ∧
      Pairwise (Disjoint on fun d : ℕ =>
        Set.range (pointsMap B S hS (Xd d).toFunctor (Xd d).ι)) ∧
      (∀ d : ℕ, HasRelativeDimension d B S hS ((Xd d).ι ≫ f))
Sources
LeanAlgebraicGeometry.hasCohenMacaulayFiberLocalRing_isEtaleLocalOnSourceAndTarget · AlgebraicGeometry.Space.IsCohenMacaulayAt · AlgebraicGeometry.Space.IsCohenMacaulay · AlgebraicGeometry.Space.HasCohenMacaulayFibersOnChart · AlgebraicGeometry.Space.isCohenMacaulay_tfae_etaleCharts · AlgebraicGeometry.Space.isCohenMacaulayAt_iff_etaleLocalRingMap · AlgebraicGeometry.Space.isCohenMacaulayAt_comp · AlgebraicGeometry.Space.isCohenMacaulay_comp

Section76.27 Gorenstein morphisms#

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

Tag 0E13, a lemma

Tag 0E13 in the Stacks Project.

AlgebraicGeometry.hasGorensteinFiberLocalRing_isEtaleLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/GorensteinFiber.lean, line 456.

Stacks Project, Tag 0E13. Having a Noetherian and Gorenstein local ring of the fibre is étale local on the source and target germs.

public theorem hasGorensteinFiberLocalRing_isEtaleLocalOnSourceAndTarget :
    MorphismOfGerms.IsEtaleLocalOnSourceAndTarget
      (@HasGorensteinFiberLocalRing.{u})
Tag 0E14, a definition

Tag 0E14 in the Stacks Project.

AlgebraicGeometry.Space.IsGorensteinAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Defs.lean, line 53. The attribute's comment: “part (1): at a point”.

Stacks 0E14, part (1). A morphism of algebraic spaces over S is Gorenstein at a point x of its source when it is flat at x and the local ring of its fibre is Noetherian and Gorenstein in every pointed étale scheme chart at x.

abbrev IsGorensteinAt (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (x : points B S hS X) : Prop

AlgebraicGeometry.Space.IsGorenstein, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Defs.lean, line 61. The attribute's comment: “part (2): morphism”.

Stacks 0E14, part (2). A morphism of algebraic spaces over S is Gorenstein when it is Gorenstein at every point of its source.

abbrev IsGorenstein (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop
Tag 0E15, a lemma

Tag 0E15 in the Stacks Project.

AlgebraicGeometry.Space.isGorenstein_tfae_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/EtaleCharts.lean, line 216. The attribute's comment: “global_gorenstein_equivalence”.

Stacks 0E15. For a morphism of algebraic spaces over S with locally Noetherian fibres, Gorensteinness is equivalent to flatness together with Gorensteinness of the fibres after some, equivalently after every, étale scheme chart of the target.

theorem isGorenstein_tfae_etaleCharts (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : HasLocallyNoetherianFibers B S hS f) :
    List.TFAE [
      IsGorenstein B S hS f,
      IsFlat B S hS f ∧
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          (MorphismProperty.presheaf (MorphismProperty.inverseImage
            (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS))) g ∧
          IsEtale B S hS g ∧ HasGorensteinFibersOnChart B S hS f V g,
      IsFlat B S hS f ∧
        ∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
          IsEtale B S hS g → HasGorensteinFibersOnChart B S hS f V g]

AlgebraicGeometry.Space.isGorensteinAt_iff_etaleLocalRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/EtaleLocalRings.lean, line 238. The attribute's comment: “etale_local_ring_criterion”.

Stacks 0E15. A morphism of algebraic spaces over S is Gorenstein at the image of a geometric point x of its source exactly when the canonical homomorphism of étale local rings at x is flat and its local fibre ring is Noetherian, local and Gorenstein.

theorem isGorensteinAt_iff_etaleLocalRingMap (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (x : GeometricPoint B S hS X) :
    IsGorensteinAt B S hS f x.image ↔
      ((etaleLocalRingMap hX f x).Flat ∧
        ∃ (hN : IsNoetherianRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x))
          (hL : IsLocalRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x)),
          @Dualizing.IsGorensteinLocalRing
            (etaleLocalRing B S hS X x ⧸ etaleLocalFiberIdeal B S hS hX hY f x) _ hN hL)
Tag 0E16, a lemma

Tag 0E16 in the Stacks Project.

AlgebraicGeometry.Space.isGorensteinAt_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 90. The attribute's comment: “part (1)”.

Stacks 0E16, part (1). The composite of two morphisms of algebraic spaces with locally Noetherian fibres is Gorenstein at a point of its source as soon as the first is Gorenstein there and the second is Gorenstein at the image of that point.

theorem isGorensteinAt_comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hfx : IsGorensteinAt B S hS f x)
    (hgy : IsGorensteinAt B S hS g (pointsMap B S hS X f x)) :
    IsGorensteinAt B S hS (f ≫ g) x

AlgebraicGeometry.Space.isGorenstein_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 111. The attribute's comment: “part (2)”.

Stacks 0E16, part (2). The composite of two Gorenstein morphisms of algebraic spaces with locally Noetherian fibres is Gorenstein.

theorem isGorenstein_comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hfm : IsGorenstein B S hS f) (hgm : IsGorenstein B S hS g) :
    IsGorenstein B S hS (f ≫ g)

AlgebraicGeometry.Space.isGorensteinAt_left_of_comp_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 150. The attribute's comment: “part (3), first conclusion”.

Stacks 0E16, part (3), first conclusion. If the composite is Gorenstein at x and the first morphism is flat at x, then the first morphism is Gorenstein at x.

theorem isGorensteinAt_left_of_comp_of_isFlatAt
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hcomp : IsGorensteinAt B S hS (f ≫ g) x)
    (hflat : IsFlatAt B S hS f x) : IsGorensteinAt B S hS f x

AlgebraicGeometry.Space.isGorensteinAt_right_of_comp_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 164. The attribute's comment: “part (3), second conclusion”.

Stacks 0E16, part (3), second conclusion. If the composite is Gorenstein at x and the first morphism is flat at x, then the second morphism is Gorenstein at the image of x.

theorem isGorensteinAt_right_of_comp_of_isFlatAt
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (x : points B S hS X) (hcomp : IsGorensteinAt B S hS (f ≫ g) x)
    (hflat : IsFlatAt B S hS f x) :
    IsGorensteinAt B S hS g (pointsMap B S hS X f x)

AlgebraicGeometry.Space.isGorenstein_left_of_comp_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 179. The attribute's comment: “part (4), first conclusion”.

Stacks 0E16, part (4), first conclusion. If the composite is Gorenstein and the first morphism is flat, then the first morphism is Gorenstein.

theorem isGorenstein_left_of_comp_of_isFlat
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hcomp : IsGorenstein B S hS (f ≫ g)) (hflat : IsFlat B S hS f) :
    IsGorenstein B S hS f

AlgebraicGeometry.Space.isGorensteinAt_right_of_comp_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Composition.lean, line 195. The attribute's comment: “part (4), second conclusion”.

Stacks 0E16, part (4), second conclusion. If the composite is Gorenstein and the first morphism is flat, then the second morphism is Gorenstein at every point in the image of the first.

theorem isGorensteinAt_right_of_comp_of_isFlat
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : HasLocallyNoetherianFibersAtPoints B S hS g)
    (hgf : HasLocallyNoetherianFibersAtPoints B S hS (f ≫ g))
    (hcomp : IsGorenstein B S hS (f ≫ g)) (hflat : IsFlat B S hS f)
    (x : points B S hS X) :
    IsGorensteinAt B S hS g (pointsMap B S hS X f x)
Tag 0E17, a lemma

Tag 0E17 in the Stacks Project.

AlgebraicGeometry.Space.isGorenstein_of_isGorenstein_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/FlatSource.lean, line 161. The attribute's comment: “the morphism is Gorenstein”.

Stacks 0E17. A flat morphism of locally Noetherian algebraic spaces over S whose source is a Gorenstein algebraic space is a Gorenstein morphism.

theorem isGorenstein_of_isGorenstein_source (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hNX : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hNY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hG : HasEtaleLocalProperty B S hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsGorenstein T))
    (f : X ⟶ Y) (hf : IsFlat B S hS f) :
    IsGorenstein B S hS f

AlgebraicGeometry.Space.isGorensteinLocalRing_etaleLocalRing_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/FlatSource.lean, line 199. The attribute's comment: “the target étale local rings are Gorenstein”.

Stacks 0E17. For a flat morphism of locally Noetherian algebraic spaces over S whose source is a Gorenstein algebraic space, the étale local ring of the target at the image of any geometric point of the source is Gorenstein.

theorem isGorensteinLocalRing_etaleLocalRing_target (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hNX : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hNY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hG : HasEtaleLocalProperty B S hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsGorenstein T))
    (f : X ⟶ Y) (hf : IsFlat B S hS f) (x : GeometricPoint B S hS X) :
    letI : IsLocalRing (etaleLocalRing B S hS Y (geometricPointMap f x)) :=
      isLocalRing_etaleLocalRing B S hS Y hY (geometricPointMap f x)
    letI : IsNoetherianRing (etaleLocalRing B S hS Y (geometricPointMap f x)) :=
      isNoetherianRing_etaleLocalRing_of_isLocallyNoetherian B S hS Y hY hNY
        (geometricPointMap f x)
    Dualizing.IsGorensteinLocalRing (etaleLocalRing B S hS Y (geometricPointMap f x))
Tag 0E18, a lemma

Tag 0E18 in the Stacks Project.

AlgebraicGeometry.Space.isGorensteinAt_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/BaseChange.lean, line 227. The attribute's comment: “part (1)”.

Stacks 0E18, part (1). Gorensteinness of a morphism of algebraic spaces with locally Noetherian fibres at a point is preserved by base change along a morphism locally of finite type.

theorem isGorensteinAt_pullback_snd
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hgor : IsGorensteinAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')) :
    IsGorensteinAt B S hS (pullback.snd f g) x'

AlgebraicGeometry.Space.isGorensteinAt_of_pullback_snd_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/BaseChange.lean, line 245. The attribute's comment: “part (2)”.

Stacks 0E18, part (2). Gorensteinness descends from the base change when the original morphism is flat at the point in question.

theorem isGorensteinAt_of_pullback_snd_of_isFlatAt
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hflat : IsFlatAt B S hS f (pointsMap B S hS (pullback f g) (pullback.fst f g) x'))
    (hgor : IsGorensteinAt B S hS (pullback.snd f g) x') :
    IsGorensteinAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')

AlgebraicGeometry.Space.isGorensteinAt_of_pullback_snd_of_isFlatAt_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/BaseChange.lean, line 268. The attribute's comment: “part (3)”.

Stacks 0E18, part (3). Gorensteinness descends from the base change when the base morphism is flat at the corresponding point.

theorem isGorensteinAt_of_pullback_snd_of_isFlatAt_base
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasLocallyNoetherianFibersAtPoints B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) (x' : points B S hS (pullback f g))
    (hflat : IsFlatAt B S hS g (pointsMap B S hS (pullback f g) (pullback.snd f g) x'))
    (hgor : IsGorensteinAt B S hS (pullback.snd f g) x') :
    IsGorensteinAt B S hS f
      (pointsMap B S hS (pullback f g) (pullback.fst f g) x')
Tag 0E19, a lemma

Tag 0E19 in the Stacks Project.

AlgebraicGeometry.Space.isOpen_setOf_isGorensteinAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Locus.lean, line 110. The attribute's comment: “openness of the Gorenstein locus”.

Stacks 0E19. The Gorenstein locus of a flat morphism of algebraic spaces over S which is locally of finite presentation is open in the canonical topology of Tag 03BX on the point space of its source.

theorem isOpen_setOf_isGorensteinAt {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf_flat : IsFlat B S hS f) (hf_lfp : IsLocallyOfFinitePresentation B S hS f) :
    IsOpen {x : points B S hS X | IsGorensteinAt B S hS f x}

AlgebraicGeometry.Space.isGorensteinAt_pullback_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Gorenstein/Locus.lean, line 148. The attribute's comment: “base change of the Gorenstein locus”.

Stacks 0E19. The Gorenstein locus of a flat morphism of algebraic spaces over S which is locally of finite presentation commutes with arbitrary base change: the locus of the base change X ×_Y Y' ⟶ Y' is the inverse image of the locus of f : X ⟶ Y under the projection to X.

theorem isGorensteinAt_pullback_locus {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y' ⟶ Y) (hf_flat : IsFlat B S hS f.hom)
    (hf_lfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    {x' : points B S hS (pullback f.hom g.hom) |
        IsGorensteinAt B S hS (pullback.snd f.hom g.hom) x'} =
      pointsMap B S hS (pullback f.hom g.hom) (pullback.fst f.hom g.hom) ⁻¹'
        {x : points B S hS X.1 | IsGorensteinAt B S hS f.hom x}
Sources
LeanAlgebraicGeometry.hasGorensteinFiberLocalRing_isEtaleLocalOnSourceAndTarget · AlgebraicGeometry.Space.IsGorensteinAt · AlgebraicGeometry.Space.IsGorenstein · AlgebraicGeometry.Space.isGorenstein_tfae_etaleCharts · AlgebraicGeometry.Space.isGorensteinAt_iff_etaleLocalRingMap · AlgebraicGeometry.Space.isGorensteinAt_comp · AlgebraicGeometry.Space.isGorenstein_comp · AlgebraicGeometry.Space.isGorensteinAt_left_of_comp_of_isFlatAt

Section76.28 Slicing Cohen-Macaulay morphisms#

Section 76.28 of the Stacks Project, Tag 06LV. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06LW, a lemma

Tag 06LW in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isFlat_vanishingSubfunctor_of_isRegular_geometricFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSliceFlatnessEnlargement.lean, line 117. The attribute's comment: “the flatness half of the conclusion”.

Stacks 06LW, the flatness half of the conclusion. Let g : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite presentation, let f₁, …, f_r ∈ Γ(X, 𝒪_X), let Spec k ⟶ Y be a field-valued point of the target, let ξ : F ⟶ X and π : F ⟶ Spec k present F as the fibre X ×_Y Spec k and let z be a geometric point of F at which the images of the f_i in the étale local ring 𝒪_{F, z̄} form a regular sequence.

Then there is an open subspace W ⊆ X containing the image of z such that V(f₁, …, f_r) ∩ W ⟶ Y is flat.

The hypothesis is taken in the form the source's conclusion is used in — quantified over the small étale neighbourhoods of the image of z in X — which is the same condition for one neighbourhood as for all, the image of a germ of a global function under the comparison homomorphism of Stacks 04NG not depending on the neighbourhood. It is the form in which Stacks 06MD states it, AlgebraicGeometry.Stack.FibreIsRegularSequenceAt.

theorem exists_isOpenSubspace_isFlat_vanishingSubfunctor_of_isRegular_geometricFiber
    (X Y F : AlgebraicSpaces B S hS) (g : X.1 ⟶ Y.1)
    (hgflat : IsFlat B S hS g) (hglfp : IsLocallyOfFinitePresentation B S hS g)
    {r : ℕ} (fs : Fin r → (SheafOfModules.unit (structureRingSheaf B S hS X)).sections)
    {k : Type u} [Field k] (hk : B.Contains (Spec (.of k))) (b : Spec (.of k) ⟶ S)
    (t : yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)) ⟶ Y.1)
    (ξ : F ⟶ X) {π : F.1 ⟶ yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS))}
    (sq : IsPullback ξ.hom π g t)
    (z : GeometricPoint B S hS F.1)
    (hreg : ∀ Nx : SmallEtaleNeighborhood (geometricPointMap ξ.hom z),
      RingTheory.Sequence.IsRegular (etaleLocalRing B S hS F.1 z)
        (List.ofFn fun i : Fin r => etaleLocalRingMap F.2 ξ.hom z
          (etaleLocalRingGerm B S hS X.1 (geometricPointMap ξ.hom z) (op Nx)
            ((fs i).eval (op Nx.chart))))) :
    ∃ (W : Subfunctor X.1) (_ : IsOpenSubspace B S hS W),
      pointsMap B S hS F.1 ξ.hom z.image ∈
          Set.range (pointsMap B S hS W.toFunctor W.ι) ∧
        IsFlat B S hS (((vanishingSubfunctor B S hS X fs).preimage W.ι).ι ≫ W.ι ≫ g)

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_vanishingSubfunctor_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulaySlice.lean, line 229. The attribute's comment: “locally of finite presentation, given it for V(f₁,…,f_r) ⟶ X”.

If X ⟶ Y is locally of finite presentation and the closed immersion of the subspace V(f₁, …, f_r) ⊆ X cut out by global regular functions f₁, …, f_r is locally of finite presentation, then so is V(f₁, …, f_r) ⟶ Y.

theorem isLocallyOfFinitePresentation_vanishingSubfunctor_comp (X Y : AlgebraicSpaces B S hS)
    (g : X.1 ⟶ Y.1) {r : ℕ}
    (f : Fin r → (SheafOfModules.unit (structureRingSheaf B S hS X)).sections)
    (hslice : IsLocallyOfFinitePresentation B S hS (vanishingSubfunctor B S hS X f).ι)
    (hg : IsLocallyOfFinitePresentation B S hS g) :
    IsLocallyOfFinitePresentation B S hS ((vanishingSubfunctor B S hS X f).ι ≫ g)

AlgebraicGeometry.Space.exists_openSubspace_isFlat_isLocallyOfFinitePresentation_vanishingSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/CohenMacaulaySlice.lean, line 281.

Let X ⟶ Y be flat and locally of finite presentation, let a cartesian square exhibit F as the fibre X ×_Y Spec(k) over a field-valued point of Y, and let z be a geometric point of F at which the f_i map to a regular sequence in 𝒪_{F, z̄}. Then there is an open subspace V ⊆ X containing p(z) over which V(f₁, …, f_r) ⟶ Y is flat and locally of finite presentation.

theorem exists_openSubspace_isFlat_isLocallyOfFinitePresentation_vanishingSubfunctor
    (X Y : AlgebraicSpaces B S hS) (g : X.1 ⟶ Y.1) (pt : FieldValuedPoint B S hS Y.1)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F) (p : F ⟶ X.1)
    (q : F ⟶ yoneda.obj (FieldValuedPoint.siteObject B S hS Y.1 pt))
    (hcart : IsPullback p q g (yonedaEquiv.symm pt.value)) {r : ℕ}
    (f : Fin r → (SheafOfModules.unit (structureRingSheaf B S hS X)).sections)
    (hflat : IsFlat B S hS g) (hg : IsLocallyOfFinitePresentation B S hS g)
    (z : GeometricPoint B S hS F)
    (hreg : FibreIsRegularSequenceAt B S hS X f hF p z) :
    ∃ (V : Subfunctor X.1) (_ : IsOpenSubspace B S hS V),
      pointsMap B S hS F p z.image ∈ Set.range (pointsMap B S hS V.toFunctor V.ι) ∧
        IsFlat B S hS (((vanishingSubfunctor B S hS X f).preimage V.ι).ι ≫ V.ι ≫ g) ∧
          IsLocallyOfFinitePresentation B S hS
            (((vanishingSubfunctor B S hS X f).preimage V.ι).ι ≫ V.ι ≫ g)
Sources
LeanAlgebraicGeometry.Space.exists_isOpenSubspace_isFlat_vanishingSubfunctor_of_isRegular_geometricFiber · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_vanishingSubfunctor_comp · AlgebraicGeometry.Space.exists_openSubspace_isFlat_isLocallyOfFinitePresentation_vanishingSubfunctor

Section76.29 Reduced fibres#

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

Tag 0E07, a lemma

Tag 0E07 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyReducedFibre_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricallyReduced.lean, line 442.

Stacks 0E07. For a morphism f : X ⟶ Y of algebraic spaces over S and a point y of |Y| the following are equivalent: (1) the fibre X_k is geometrically reduced over k for some morphism Spec k ⟶ Y in the equivalence class of y; (2) the same for every such morphism; (3) the fibre X_k is reduced for every such morphism.

Conditions (1) and (2) agree because geometric reducedness of the fibre only depends on the point of |Y| represented by the field-valued point, two representatives of one point having a common extension. Condition (3) implies (2) because every representative is dominated by one whose field of definition is algebraically closed, hence perfect, where reducedness of the fibre already gives geometric reducedness.

theorem isGeometricallyReducedFibre_tfae (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (y : points B S hS Y) :
    List.TFAE
      [ ∃ p : FieldValuedPoint B S hS Y, p.class B S hS Y = y ∧
          IsGeometricallyReducedFibre B S hS f hX hY p,
        ∀ p : FieldValuedPoint B S hS Y, p.class B S hS Y = y →
          IsGeometricallyReducedFibre B S hS f hX hY p,
        ∀ p : FieldValuedPoint B S hS Y, p.class B S hS Y = y →
          HasEtaleLocalProperty B (Spec (.of p.carrier)) p.contained
            (fibreOverFieldValuedPoint B S hS f p) (fun T : Scheme.{u} => IsReduced T) ]
Tag 0E08, a definition

Tag 0E08 in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyReducedFibreAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricallyReduced.lean, line 372.

Stacks 0E08. The fibre of f : X ⟶ Y at a point y of |Y| is geometrically reduced when the equivalent conditions of Stacks 0E07 hold: the fibre over some — equivalently, every — field-valued representative of y is geometrically reduced over the field of that representative.

abbrev IsGeometricallyReducedFibreAt (y : points B S hS Y) : Prop
Tag 0E09, a lemma

Tag 0E09 in the Stacks Project.

AlgebraicGeometry.Space.geometricallyReducedFibreLocus_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricallyReduced.lean, line 389.

Stacks 0E09. The locus of points with geometrically reduced fibre commutes with base change: the fibre of the base change X ×_Y Y' ⟶ Y' over a point of |Y'| is geometrically reduced exactly when the fibre of f over the image of that point in |Y| is.

theorem geometricallyReducedFibreLocus_pullback {Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hY' : IsAlgebraicSpace B S hS Y') :
    geometricallyReducedFibreLocus B S hS (pullback.snd f g)
        (isAlgebraicSpace_pullback B S hS f g hX hY' hY) hY' =
      pointsMap B S hS Y' g ⁻¹' geometricallyReducedFibreLocus B S hS f hX hY
Tag 0E0A, a lemma

Tag 0E0A in the Stacks Project.

AlgebraicGeometry.Space.isEtaleLocallyConstructible_geometricallyReducedFibreLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricallyReducedLocus.lean, line 428. References: EGA IV (9.7.7), “more general”.

Stacks 0E0A. For a quasi-compact morphism of algebraic spaces over S which is locally of finite presentation, the set of points of |Y| whose fibre is geometrically reduced is étale locally constructible.

Constructibility is tested on an affine étale chart h_V ⟶ Y. There the locus is, by Stacks 0E09, the locus of the base change X ×_Y h_V ⟶ h_V, which is a quasi-compact algebraic space and so has an affine surjective étale chart h_A ⟶ X ×_Y h_V. The induced morphism of affine schemes A ⟶ V is of finite presentation, its scheme-theoretic fibres are surjective étale charts of the fibres of the base change, and so the locus is the geometrically reduced fibre locus of A ⟶ V; that set is locally constructible by Stacks 0579.

theorem isEtaleLocallyConstructible_geometricallyReducedFibreLocus
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiCompact B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f) :
    IsEtaleLocallyConstructible B S hS Y (geometricallyReducedFibreLocus B S hS f hX hY)
Tag 0E0B, a lemma

Tag 0E0B in the Stacks Project.

AlgebraicGeometry.Space.isReduced_of_isReduced_specialFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/Reduced.lean, line 824. The attribute's comment: “total space”.

Stacks 0E0B. A proper flat algebraic space over a discrete valuation ring is reduced when its special fibre is reduced.

public theorem isReduced_of_isReduced_specialFiber
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (B : BigFppfSite.{u})
    (hR : B.Contains (Spec (.of R)))
    (hk : B.Contains (Spec (.of (IsLocalRing.ResidueField R))))
    (X : (BigFppfOver B (Spec (.of R)) hR)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of R)) hR X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hR))))
    (hproper : IsProper B (Spec (.of R)) hR f)
    (hflat : IsFlat B (Spec (.of R)) hR f)
    (hspecial :
      let g : B.obj hk ⟶ B.obj hR :=
        B.inclusion.preimage
          (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))
      HasEtaleLocalProperty B
        (Spec (.of (IsLocalRing.ResidueField R))) hk
        ((OverShriek.relocalizeRestrict g).obj X)
        (fun T : Scheme.{u} => IsReduced T)) :
    HasEtaleLocalProperty B (Spec (.of R)) hR X
      (fun T : Scheme.{u} => IsReduced T)

AlgebraicGeometry.Space.isReduced_genericFiber_of_isReduced_specialFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/Reduced.lean, line 968. The attribute's comment: “generic fibre”.

Stacks 0E0B. The generic fibre of a proper flat algebraic space over a discrete valuation ring with reduced special fibre is reduced.

public theorem isReduced_genericFiber_of_isReduced_specialFiber
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (B : BigFppfSite.{u})
    (hR : B.Contains (Spec (.of R)))
    (hk : B.Contains (Spec (.of (IsLocalRing.ResidueField R))))
    (hK : B.Contains (Spec (.of (FractionRing R))))
    (X : (BigFppfOver B (Spec (.of R)) hR)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of R)) hR X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hR))))
    (hproper : IsProper B (Spec (.of R)) hR f)
    (hflat : IsFlat B (Spec (.of R)) hR f)
    (hspecial :
      let g : B.obj hk ⟶ B.obj hR :=
        B.inclusion.preimage
          (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))
      HasEtaleLocalProperty B
        (Spec (.of (IsLocalRing.ResidueField R))) hk
        ((OverShriek.relocalizeRestrict g).obj X)
        (fun T : Scheme.{u} => IsReduced T)) :
    let g : B.obj hK ⟶ B.obj hR :=
      B.inclusion.preimage
        (Spec.map (CommRingCat.ofHom (algebraMap R (FractionRing R))))
    HasEtaleLocalProperty B (Spec (.of (FractionRing R))) hK
      ((OverShriek.relocalizeRestrict g).obj X)
      (fun T : Scheme.{u} => IsReduced T)
Tag 0E0C, a lemma

Tag 0E0C in the Stacks Project.

AlgebraicGeometry.Space.isOpen_geometricallyReducedFibreLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricallyReducedOpenLocus.lean, line 304. References: EGA IV (12.2.4), “more general”.

Stacks 0E0C. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat, proper and of finite presentation. Then the set of points of |Y| at which the fibre of f is geometrically reduced is open in |Y|.

The locus is étale locally constructible, Stacks 0E0A, and on every étale scheme chart its inverse image is stable under generalization, AlgebraicGeometry.Space.stableUnderGeneralization_preimage_geometricallyReducedFibreLocus; so AlgebraicGeometry.Space.isOpen_geometricallyReducedFibreLocus_of_chart_generalization applies.

theorem isOpen_geometricallyReducedFibreLocus
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hflat : IsFlat B S hS f) (hproper : IsProper B S hS f)
    (hfp : IsFinitePresentation B S hS f) :
    IsOpen (geometricallyReducedFibreLocus B S hS f hX hY)
Sources
LeanAlgebraicGeometry.Space.isGeometricallyReducedFibre_tfae · AlgebraicGeometry.Space.IsGeometricallyReducedFibreAt · AlgebraicGeometry.Space.geometricallyReducedFibreLocus_pullback · AlgebraicGeometry.Space.isEtaleLocallyConstructible_geometricallyReducedFibreLocus · AlgebraicGeometry.Space.isReduced_of_isReduced_specialFiber · AlgebraicGeometry.Space.isReduced_genericFiber_of_isReduced_specialFiber · AlgebraicGeometry.Space.isOpen_geometricallyReducedFibreLocus

Section76.30 Connected components of fibres#

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

Tag 0E1B, a lemma

Tag 0E1B in the Stacks Project.

AlgebraicGeometry.Space.numberGeometricConnectedComponents_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricComponentCount.lean, line 352. The attribute's comment: “well-definedness”. References: EGA III (4.3.4), “more general”; EGA IV (4.5.1), “partial”.

Stacks 0E1B. The number of geometric connected components of the fibres of a morphism of algebraic spaces is, at the image of a geometric point, the number of connected components of the fibre over that geometric point. In particular the defining infimum is attained at every geometric representative.

theorem numberGeometricConnectedComponents_eq (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (p : GeometricPoint B S hS G) :
    numberGeometricConnectedComponents B S hS f p.image =
      geometricFiberComponentCount B S hS f p.val

AlgebraicGeometry.Space.numberGeometricConnectedComponents_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricComponentCount.lean, line 372. The attribute's comment: “base change”.

Stacks 0E1B. Formation of the number of geometric connected components of the fibres commutes with arbitrary base change: the function attached to the projection F ×_G H ⟶ H is the function attached to f : F ⟶ G composed with the map |H| → |G| on points.

theorem numberGeometricConnectedComponents_baseChange
    {H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (hH : IsAlgebraicSpace B S hS H) (f : F ⟶ G) (g : H ⟶ G) :
    numberGeometricConnectedComponents B S hS (pullback.snd f g) =
      numberGeometricConnectedComponents B S hS f ∘ pointsMap B S hS H g

AlgebraicGeometry.Space.numberGeometricConnectedComponents, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricComponents.lean, line 114. The attribute's comment: “function”. References: EGA III (4.3.4); EGA IV (4.5.2), “partial”.

Stacks 0E1B. The number of geometric connected components of the fibres of a morphism of algebraic spaces: the function on the points of the target whose value at y is the number of connected components of the fibre over any geometric point representing y.

By AlgebraicGeometry.Space.exists_geometricRepresentative the set whose infimum is taken is nonempty, and the source lemma is that all of its elements agree.

noncomputable def numberGeometricConnectedComponents
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : points B S hS G → ℕ∞
Sources
LeanAlgebraicGeometry.Space.numberGeometricConnectedComponents_eq · AlgebraicGeometry.Space.numberGeometricConnectedComponents_baseChange · AlgebraicGeometry.Space.numberGeometricConnectedComponents

Section76.31 Dimension of fibres#

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

Tag 0D4M, a lemma

Tag 0D4M in the Stacks Project.

AlgebraicGeometry.Space.fiberDimension_eq_dimension_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/DimensionFieldFibre.lean, line 212.

Stacks 0D4M. For a morphism of algebraic spaces over S of finite type and a field-valued point p of its target, the fibre dimension at the point p represents is the dimension of the fibre of f over p, and it is not ⊤.

theorem fiberDimension_eq_dimension_pullback
    (hf : IsFiniteType B S hS f) (p : FieldValuedPoint B S hS Y) :
    fiberDimension B S hS f (p.class B S hS Y) =
      dimension B S hS (pullback (yonedaEquiv.symm p.value) f)
        (isAlgebraicSpace_pullback B S hS (yonedaEquiv.symm p.value) f
          (isAlgebraicSpace_yoneda B S hS (p.siteObject B S hS Y)) hX hY) ∧
      fiberDimension B S hS f (p.class B S hS Y) ≠ ⊤
Tag 0D4N, a lemma

Tag 0D4N in the Stacks Project.

AlgebraicGeometry.Space.fiberDimension_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/DimensionBaseChange.lean, line 56.

Stacks 0D4N. The fibre-dimension function of the base change of a finite type morphism of algebraic spaces over S is the pullback of the fibre-dimension function of the morphism along the map on points of the morphism of targets.

theorem fiberDimension_pullback_snd {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (hf : IsFiniteType B S hS f) :
    fiberDimension B S hS (pullback.snd f g) =
      fiberDimension B S hS f ∘ pointsMap B S hS Y' g
Tag 0D4P, a lemma

Tag 0D4P in the Stacks Project.

AlgebraicGeometry.Space.lowerSemicontinuous_fiberDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/DimensionLowerSemicontinuity.lean, line 323.

Stacks 0D4P. The fibre-dimension function of a flat morphism of algebraic spaces over S of finite presentation is lower semicontinuous on the points of its target.

theorem lowerSemicontinuous_fiberDimension
    (hflat : IsFlat B S hS f) (hfp : IsFinitePresentation B S hS f) :
    LowerSemicontinuous (fiberDimension B S hS f)
Tag 0D4Q, a lemma

Tag 0D4Q in the Stacks Project.

AlgebraicGeometry.Space.upperSemicontinuous_fiberDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/DimensionUpperSemicontinuity.lean, line 94.

Stacks 0D4Q. The fibre-dimension function of a proper morphism of algebraic spaces over S is upper semicontinuous on the points of its target.

theorem upperSemicontinuous_fiberDimension (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsProper B S hS f) :
    UpperSemicontinuous (fiberDimension B S hS f)
Tag 0D4R, a lemma

Tag 0D4R in the Stacks Project.

AlgebraicGeometry.Space.isLocallyConstant_fiberDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/DimensionLocallyConstant.lean, line 49. References: EGA IV (14.2.5), “flat fin. pres. case”.

Stacks 0D4R. The fibre-dimension function of a proper flat morphism of algebraic spaces over S of finite presentation is locally constant on the points of its target.

theorem isLocallyConstant_fiberDimension (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hProper : IsProper B S hS f)
    (hFlat : IsFlat B S hS f) (hFP : IsFinitePresentation B S hS f) :
    IsLocallyConstant (fiberDimension B S hS f)
Sources
LeanAlgebraicGeometry.Space.fiberDimension_eq_dimension_pullback · AlgebraicGeometry.Space.fiberDimension_pullback_snd · AlgebraicGeometry.Space.lowerSemicontinuous_fiberDimension · AlgebraicGeometry.Space.upperSemicontinuous_fiberDimension · AlgebraicGeometry.Space.isLocallyConstant_fiberDimension

Section76.32 Catenary algebraic spaces#

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

Tag 0EDM, a lemma

Tag 0EDM in the Stacks Project.

AlgebraicGeometry.Space.exists_glueingSpace_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GlueingSpaceAway.lean, line 538.

Stacks 0EDM. Let f : X ⟶ Y be an integral morphism of algebraic spaces over S, and let y : Spec k ⟶ Y be a closed immersion. Then f factors as X ⟶ X' ⟶ Y with

  1. X' ⟶ Y integral,
  2. X ⟶ X' an isomorphism over the open complement X' ∖ X'_y of the fibre X'_y = |h|⁻¹ {y},
  3. X'_y a single point p, which is the point of a closed immersion x' : Spec k ⟶ X' over y, so that κ(p) = k,

and moreover X' ⟶ Y is finite when f is finite and Y is locally Noetherian.

The space X' is the quotient of the chart-level pushout over a separated étale chart of Y (AlgebraicGeometry.Space.EtaleChartRelation.exists_of_isAlgebraicSpace) by the étale equivalence relation induced by the chart's kernel pair; the sheafification it needs is AlgebraicGeometry.BigFppfOver.hasSheafify_type. "Locally Noetherian" is the source's definition for algebraic spaces, a locally Noetherian surjective étale atlas (AlgebraicGeometry.Space.HasEtaleLocalProperty, Stacks 03E6), and it gives local Noetherianity of the chosen chart by Stacks 03E8.

theorem exists_glueingSpace_factorization {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsIntegralHom B S hS f.hom) {k : Type u} [Field k]
    (hk : B.Contains (Spec (CommRingCat.of k))) (σ : Spec (CommRingCat.of k) ⟶ S)
    (y : yoneda.obj (BigFppfOver.mk B S hS hk σ) ⟶ Y.1) (hy : IsClosedImmersion B S hS y) :
    ∃ (X' : AlgebraicSpaces B S hS) (g : X ⟶ X') (h : X' ⟶ Y),
      g ≫ h = f ∧
      IsIntegralHom B S hS h.hom ∧
      IsIso (openComplementRestriction B S hS g.hom
        (pointsMap B S hS X'.1 h.hom ⁻¹'
          Set.range (pointsMap B S hS (yoneda.obj (BigFppfOver.mk B S hS hk σ)) y))) ∧
      (∃ (x' : yoneda.obj (BigFppfOver.mk B S hS hk σ) ⟶ X'.1) (p : points B S hS X'.1),
        IsClosedImmersion B S hS x' ∧ x' ≫ h.hom = y ∧
        pointsMap B S hS X'.1 h.hom ⁻¹'
            Set.range (pointsMap B S hS (yoneda.obj (BigFppfOver.mk B S hS hk σ)) y) = {p} ∧
        Set.range (pointsMap B S hS (yoneda.obj (BigFppfOver.mk B S hS hk σ)) x') = {p}) ∧
      (IsFinite B S hS f.hom →
        HasEtaleLocalProperty B S hS Y.1
          (fun T : Scheme.{u} ↦ _root_.AlgebraicGeometry.IsLocallyNoetherian T) →
        IsFinite B S hS h.hom)
Tag 0EDN, a lemma

Tag 0EDN in the Stacks Project.

AlgebraicGeometry.Space.exists_dimensionFunction_inducedDimensionValue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InducedDimensionFunction.lean, line 72.

Stacks 0EDN. Let Y be a decent, locally Noetherian, universally catenary algebraic space and δ a dimension function on |Y|. If X is a decent algebraic space and f : X ⟶ Y is locally of finite type, then δ_X, the value of δ at the image of a point plus the transcendence degree of the point over its image, is a dimension function on |X|.

theorem exists_dimensionFunction_inducedDimensionValue (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y) (hYdec : IsDecentSpace B S hS Y)
    (hYN : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hYcat : IsUniversallyCatenary B S hS Y) (δ : DimensionFunction (points B S hS Y))
    (hX : IsAlgebraicSpace B S hS X) (hXdec : IsDecentSpace B S hS X) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ d : DimensionFunction (points B S hS X), ∀ x : points B S hS X,
      d x = inducedDimensionValue B S hS δ f x
Sources
LeanAlgebraicGeometry.Space.exists_glueingSpace_factorization · AlgebraicGeometry.Space.exists_dimensionFunction_inducedDimensionValue

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.