37.2 Thickenings to 37.11 Formally smooth morphisms

Section37.2 Thickenings #

Section 37.2 of the Stacks Project, Tag 04EW. 6 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04EX, a definition

Tag 04EX in the Stacks Project.

Stacks.Thickenings.IsThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings.lean, line 71. The attribute's comment: “part (1): thickening”.

A thickening is a closed immersion i : X ⟶ X' whose underlying map of topological spaces is surjective, so that the closed subscheme X and the ambient scheme X' have the same underlying topological space.

abbrev IsThickening {X X' : Scheme.{u}} (i : X ⟶ X') : Prop

Stacks.Thickenings.IsFirstOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings.lean, line 77. The attribute's comment: “part (2): first-order thickening”.

A first-order thickening is a closed immersion whose kernel ideal sheaf is square-zero.

abbrev IsFirstOrderThickening {X X' : Scheme.{u}} (i : X ⟶ X') : Prop

Stacks.Thickenings.IsFiniteOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings.lean, line 83. The attribute's comment: “part (3): finite-order thickening”.

A finite-order thickening is a closed immersion whose kernel ideal sheaf is nilpotent.

abbrev IsFiniteOrderThickening {X X' : Scheme.{u}} (i : X ⟶ X') : Prop

Stacks.Thickenings.IsNthOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings.lean, line 89. The attribute's comment: “part (4): nth-order thickening”.

An nth-order thickening is a closed immersion whose kernel ideal sheaf has vanishing (n+1)st power.

abbrev IsNthOrderThickening {X X' : Scheme.{u}} (n : ℕ) (i : X ⟶ X') : Prop

Declarations registered for the tag:

CategoryTheory.Arrow.Hom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Thickenings.lean, line 124 (StacksFrontier): “parts (5) and (6): morphisms of thickenings, also over a base”.

Tag 05YV, a lemma

Tag 05YV in the Stacks Project.

Stacks.Thickenings.firstOrderThickening_squareZeroExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/SquareZeroExtension/OfFirstOrderThickening.lean, line 425. The attribute's comment: “converse: every first-order thickening has this form”.

Every first-order thickening over a base is obtained from a square-zero extension.

public theorem firstOrderThickening_squareZeroExtension {X Y S : Scheme.{u}}
    (i : X ⟶ Y) (g : Y ⟶ S) (hi : Stacks.Thickenings.IsFirstOrderThickening i) :
    ∃ E : SquareZeroExtension (i ≫ g),
      ∃ r : Realization E, r.ambient = Y ∧ HEq r.immersion i ∧ HEq r.toBase g

Stacks.Thickenings.squareZeroExtension_realization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/SquareZeroExtension/Realization.lean, line 744. The attribute's comment: “construction from a square-zero extension”.

A square-zero extension with quasi-coherent kernel gives a first-order thickening.

public theorem squareZeroExtension_realization {X S : Scheme.{u}} {f : X ⟶ S}
    (E : SquareZeroExtension f) : Nonempty (Realization E)

Tag 06AD, a lemma

Tag 06AD in the Stacks Project.

Stacks.Thickenings.isAffine_of_isThickening_of_surjective_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningAffine.lean, line 190.

A thickening of an affine scheme whose map on global sections is surjective has affine ambient scheme. This is [Stacks Project, Tag 06AD] with its cohomological content — the surjectivity of i.appTop — as the explicit hypothesis hsurj, which is the only thing assumed: everything else in the tag is proved here, through the affineness criterion of [Stacks Project, Tag 01QF]. The hypothesis is not needed for the tag itself: it is dropped in Stacks.Thickenings.isAffine_of_isThickening, which proves Tag 06AD outright from [Stacks Project, Tag 01ZT].

theorem isAffine_of_isThickening_of_surjective_appTop [IsAffine X] {i : X ⟶ X'}
    (hi : IsThickening i) (hsurj : Function.Surjective i.appTop.hom) : IsAffine X'

Stacks.Thickenings.isAffine_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningAffineFirstOrder.lean, line 199. The attribute's comment: “the finite-order case, the second proof the source gives (EGA I, Prop 5.1.9)”.

Any finite-order thickening of an affine scheme is affine. The adic filtration of the defining ideal sheaf interpolates between the closed subscheme and the ambient scheme by first-order thickenings.

theorem isAffine_of_isFiniteOrderThickening {i : X ⟶ X'} (hi : IsFiniteOrderThickening i)
    [IsAffine X] : IsAffine X'

Stacks.Thickenings.isAffine_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Affine.lean, line 39.

A thickening of an affine scheme is affine. A closed immersion is a finite morphism, and a thickening is surjective, so this is the affineness of the target of a finite surjective morphism with affine source.

theorem isAffine_of_isThickening {X X' : Scheme.{u}} {i : X ⟶ X'} (hi : IsThickening i)
    [IsAffine X] : IsAffine X'

Tag 09ZU, a lemma

Tag 09ZU in the Stacks Project.

Stacks.Thickenings.baseChangeHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Stability.lean, line 237. The attribute's comment: “canonical morphism of thickenings”.

The canonical morphism from the base change of a thickening i : S ⟶ S' along f : X' ⟶ S' to i itself: the commutative square given by the pullback.

noncomputable def baseChangeHom {S S' X' : Scheme.{u}}
    (i : S ⟶ S') (f : X' ⟶ S') :
    Arrow.mk (pullback.snd i f) ⟶ Arrow.mk i

Stacks.Thickenings.isThickening_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Stability.lean, line 244. The attribute's comment: “base change of thickenings”.

Thickenings of schemes are stable under arbitrary base change.

instance isThickening_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsThickening : MorphismProperty Scheme.{u})

Stacks.Thickenings.isFirstOrderThickening_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Stability.lean, line 253. The attribute's comment: “base change of first-order thickenings”.

First-order thickenings of schemes are stable under arbitrary base change.

instance isFirstOrderThickening_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsFirstOrderThickening : MorphismProperty Scheme.{u})

Stacks.Thickenings.isFiniteOrderThickening_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Stability.lean, line 267. The attribute's comment: “base change of finite-order thickenings”.

Finite-order thickenings of schemes are stable under arbitrary base change.

instance isFiniteOrderThickening_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsFiniteOrderThickening : MorphismProperty Scheme.{u})

Stacks.Thickenings.isThickening_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/BaseChange.lean, line 134. The attribute's comment: “a base change of a thickening is a thickening”. References: EGA I (4.3.2), “thickenings”.

A base change of a thickening is a thickening. If i : Z ⟶ Y is a thickening and the square with sides f' : P ⟶ X, g' : P ⟶ Z, f : X ⟶ Y and i is a pullback square, then f' is a thickening.

theorem isThickening_of_isPullback {f' : P ⟶ X} {g' : P ⟶ Z} {f : X ⟶ Y} {i : Z ⟶ Y}
    (h : IsPullback f' g' f i) (hi : IsThickening i) : IsThickening f'

Stacks.Thickenings.isNthOrderThickening_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/BaseChange.lean, line 143. The attribute's comment: “a base change of an nth-order thickening is an nth-order thickening”.

A base change of an nth-order thickening is an nth-order thickening. If i is an nth-order thickening and the square with sides f', g', f and i is a pullback square, then f' is an nth-order thickening.

theorem isNthOrderThickening_of_isPullback {f' : P ⟶ X} {g' : P ⟶ Z} {f : X ⟶ Y} {i : Z ⟶ Y}
    {n : ℕ} (h : IsPullback f' g' f i) (hi : IsNthOrderThickening n i) :
    IsNthOrderThickening n f'

Stacks.Thickenings.isFirstOrderThickening_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/BaseChange.lean, line 152. The attribute's comment: “a base change of a first-order thickening is a first-order thickening”.

A base change of a first-order thickening is a first-order thickening. If i is a first-order thickening and the square with sides f', g', f and i is a pullback square, then f' is a first-order thickening.

theorem isFirstOrderThickening_of_isPullback {f' : P ⟶ X} {g' : P ⟶ Z} {f : X ⟶ Y} {i : Z ⟶ Y}
    (h : IsPullback f' g' f i) (hi : IsFirstOrderThickening i) :
    IsFirstOrderThickening f'

Stacks.Thickenings.isFiniteOrderThickening_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/BaseChange.lean, line 161. The attribute's comment: “a base change of a finite-order thickening is a finite-order thickening”.

A base change of a finite-order thickening is a finite-order thickening. If i is a finite-order thickening and the square with sides f', g', f and i is a pullback square, then f' is a finite-order thickening.

theorem isFiniteOrderThickening_of_isPullback {f' : P ⟶ X} {g' : P ⟶ Z} {f : X ⟶ Y} {i : Z ⟶ Y}
    (h : IsPullback f' g' f i) (hi : IsFiniteOrderThickening i) :
    IsFiniteOrderThickening f'

Tag 0BPE, a lemma

Tag 0BPE in the Stacks Project.

Stacks.Thickenings.isThickening_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Stability.lean, line 275.

A composite of thickenings is a thickening.

theorem isThickening_comp {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsThickening f) (hg : IsThickening g) : IsThickening (f ≫ g)

Tag 0BPF, a lemma

Tag 0BPF in the Stacks Project.

Stacks.Thickenings.isThickening_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/FpqcLocal.lean, line 64. The attribute's comment: “thickenings”.

Stacks Project, Tag 0BPF. Being a thickening is fpqc local on the target: a morphism whose base changes along the members of an fpqc covering of the target are all thickenings is itself a thickening.

instance isThickening_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsThickening : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Stacks.Thickenings.isFirstOrderThickening_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/FpqcLocal.lean, line 146. The attribute's comment: “first-order thickenings”.

Stacks Project, Tag 0BPF. Being a first-order thickening is fpqc local on the target: a morphism whose base changes along the members of an fpqc covering of the target are all first-order thickenings is itself a first-order thickening.

instance isFirstOrderThickening_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsFirstOrderThickening : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Sources

LeanStacks.Thickenings.IsThickening · Stacks.Thickenings.IsFirstOrderThickening · Stacks.Thickenings.IsFiniteOrderThickening · Stacks.Thickenings.IsNthOrderThickening · CategoryTheory.Arrow.Hom · Stacks.Thickenings.firstOrderThickening_squareZeroExtension · Stacks.Thickenings.squareZeroExtension_realization · Stacks.Thickenings.isAffine_of_isThickening_of_surjective_appTop

Section37.3 Morphisms of thickenings #

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

Tag 09ZV, a lemma

Tag 09ZV in the Stacks Project.

Stacks.Thickenings.isAffineHom_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Affine.lean, line 218. The attribute's comment: “affine”.

Part (1) of [Stacks Project, Tag 09ZV]. For a morphism of thickenings, the morphism of closed subschemes is affine if and only if the morphism of ambient schemes is affine.

Affineness of a morphism quantifies over the affine opens of its target, and Stacks.Thickenings.isAffineOpen_iff_isAffineOpen_preimage matches the affine opens of S with those of S'; the inverse images of matching opens along φ.left and φ.right are then matched by the same criterion for the thickening i.

theorem isAffineHom_left_iff_right {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j) (φ : Arrow.mk i ⟶ Arrow.mk j) :
    IsAffineHom φ.left ↔ IsAffineHom φ.right

Stacks.Thickenings.isIntegralHom_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Affine.lean, line 239. The attribute's comment: “integral”.

Part (5) of [Stacks Project, Tag 09ZV]. For a morphism of thickenings, the morphism of closed subschemes is integral if and only if the morphism of ambient schemes is integral.

A morphism is integral exactly when it is universally closed and affine — [Stacks Project, Tag 01WM], which is AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom — so this is part (4) of the tag together with part (1).

theorem isIntegralHom_left_iff_right {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j) (φ : Arrow.mk i ⟶ Arrow.mk j) :
    IsIntegralHom φ.left ↔ IsIntegralHom φ.right

Stacks.Thickenings.isQuasiAffineHom_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/QuasiAffineLimit.lean, line 330. The attribute's comment: “quasi_affine”.

Part (9) of [Stacks Project, Tag 09ZV]. For a morphism of thickenings — a commutative square whose horizontal arrows are thickenings — the morphism of closed subschemes is quasi-affine if and only if the morphism of ambient schemes is. No hypothesis on the schemes.

The mpr half is Stacks.Thickenings.isQuasiAffineHom_left_of_right, which needs nothing; the mp half is Stacks.Thickenings.isQuasiAffineHom_right_of_left fed the absolute statement Stacks.Thickenings.quasiAffineAscendsAlongThickening.

theorem isQuasiAffineHom_left_iff_right {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j) (φ : Arrow.mk i ⟶ Arrow.mk j) :
    IsQuasiAffineHom φ.left ↔ IsQuasiAffineHom φ.right

Stacks.Thickenings.isSeparated_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Separated.lean, line 63. The attribute's comment: “separated”.

Separatedness is invariant under a morphism of thickenings.

theorem isSeparated_left_iff_right
    {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j)
    (φ : Arrow.mk i ⟶ Arrow.mk j) :
    IsSeparated φ.left ↔ IsSeparated φ.right

Stacks.Thickenings.quasiSeparated_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Separated.lean, line 76. The attribute's comment: “quasi_separated”.

Quasi-separatedness of a morphism of schemes is unchanged by passing between the closed subschemes and the ambient schemes of a morphism of thickenings.

theorem quasiSeparated_left_iff_right {X S : Arrow (Scheme.{u})}
    (φ : X ⟶ S) (hX : IsThickening X.hom)
    (hS : IsThickening S.hom) :
    QuasiSeparated φ.left ↔ QuasiSeparated φ.right

Stacks.Thickenings.quasiCompact_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Topological.lean, line 73. The attribute's comment: “quasi_compact”.

Quasi-compactness is preserved and reflected by a morphism of thickenings.

theorem quasiCompact_left_iff_right
    {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (φ : Arrow.mk i ⟶ Arrow.mk j)
    (hi : IsThickening i) (hj : IsThickening j) :
    QuasiCompact φ.left ↔ QuasiCompact φ.right

Stacks.Thickenings.surjective_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Topological.lean, line 107. The attribute's comment: “surjective”.

The two vertical maps in a morphism of thickenings are simultaneously surjective.

theorem surjective_left_iff_right
    {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j)
    (f : Arrow.mk i ⟶ Arrow.mk j) :
    Surjective f.left ↔ Surjective f.right

Stacks.Thickenings.universallyClosed_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Topological.lean, line 126. The attribute's comment: “universally_closed”.

Universal closedness is invariant under a morphism of thickenings.

theorem universallyClosed_left_iff_right {i j : Arrow Scheme.{u}} (φ : i ⟶ j)
    (hi : IsThickening i.hom) (hj : IsThickening j.hom) :
    UniversallyClosed φ.left ↔ UniversallyClosed φ.right

Stacks.Thickenings.universallyInjective_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Topological.lean, line 157. The attribute's comment: “universally_injective”.

Universal injectivity is unchanged when a morphism of thickenings is passed from the closed subschemes to the ambient schemes.

theorem universallyInjective_left_iff_right {X X' S S' : Scheme.{u}}
    {i : X ⟶ X'} {j : S ⟶ S'} (hi : IsThickening i)
    (hj : IsThickening j) (f : Arrow.mk i ⟶ Arrow.mk j) :
    UniversallyInjective f.left ↔ UniversallyInjective f.right

Stacks.Thickenings.universallyOpen_left_iff_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Topological.lean, line 245. The attribute's comment: “universally_open”.

Universal openness is unchanged when a morphism of schemes is replaced by the corresponding morphism of thickenings.

theorem universallyOpen_left_iff_right
    {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'}
    (hi : IsThickening i) (hj : IsThickening j)
    (f : Arrow.mk i ⟶ Arrow.mk j) :
    UniversallyOpen f.left ↔ UniversallyOpen f.right

Tag 0D2R, a lemma

Tag 0D2R in the Stacks Project.

Stacks.AmpleThickeningAscent.isRelativelyAmple_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleThickeningAscent/Basic.lean, line 81.

[Stacks, Tag 0D2R]. Let (f, f') : (X ⊆ X') → (S ⊆ S') be a morphism of thickenings — a commutative square i ≫ f' = f ≫ j in which i : X ⟶ X' and j : S ⟶ S' are thickenings — and let 𝓛' be an invertible 𝒪_{X'}-module, with restriction 𝓛 = i^* 𝓛' to X. Then 𝓛' is f'-ample if and only if 𝓛 is f-ample.

This is Stacks.ThickeningInvertible.isRelativelyAmple_iff with its hypothesis Stacks.ThickeningInvertible.AmpleReflectedByThickening discharged by Stacks.AmpleThickeningAscent.ampleReflectedByThickening.

theorem isRelativelyAmple_iff {X X' S S' : Scheme.{u}} {i : X ⟶ X'} {j : S ⟶ S'} {f : X ⟶ S}
    {f' : X' ⟶ S'} (hi : IsThickening i) (hj : IsThickening j) (hsq : i ≫ f' = f ≫ j)
    (L' : X'.Modules) [IsInvertibleModule X' L'] :
    IsRelativelyAmple f' L' ↔ IsRelativelyAmple f (pullbackModule i L')

Stacks.ThickeningInvertible.isRelativelyAmple_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ThickeningInvertible/Basic.lean, line 342. The attribute's comment: “the implication ℒ' is f'-ample ⟹ ℒ is f-ample, nothing carried”.

[Stacks, Tag 0D2R], the implication ℒ' is f'-ample ⟹ ℒ is f-ample. For a morphism of thickenings (f, f') : (X ⊆ X') → (S ⊆ S') and an invertible 𝒪_{X'}-module ℒ' with restriction ℒ = i^* ℒ' to X, relative ampleness of ℒ' over f' gives relative ampleness of ℒ over f.

Nothing is carried. The source checks relative ampleness at every affine open of S and gets the correspondence with the affine opens of S' from [Stacks, Tag 06AD]; here the opens j^{-1}V', for V' an affine open of S', are an affine open covering of S — affine because j is a closed immersion, covering because j is surjective — and that is enough by [Stacks, Tag 01VJ]. Over each member the implication is the closed-immersion case of [Stacks, Tag 0B3E] applied to i ∣_ (f'^{-1}V').

theorem isRelativelyAmple_pullback (hi : IsThickening i) (hj : IsThickening j)
    (hsq : i ≫ f' = f ≫ j) (hL' : IsRelativelyAmple f' L') :
    IsRelativelyAmple f (pullbackModule i L')

Stacks.ThickeningInvertible.isRelativelyAmple_of_isRelativelyAmple_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ThickeningInvertible/Basic.lean, line 383. The attribute's comment: “the implication ℒ is f-ample ⟹ ℒ' is f'-ample, carrying href = [Tag 09MW] mp”.

[Stacks, Tag 0D2R], the implication ℒ is f-ample ⟹ ℒ' is f'-ample, granted [Stacks, Tag 09MW]. For a morphism of thickenings (f, f') : (X ⊆ X') → (S ⊆ S') and an invertible 𝒪_{X'}-module ℒ' with restriction ℒ = i^* ℒ' to X, relative ampleness of ℒ over f gives relative ampleness of ℒ' over f'.

One hypothesis is carried, href : Stacks.ThickeningInvertible.AmpleReflectedByThickening, which is the implication k^* M ample ⟹ M ample of [Stacks, Tag 09MW] with the source's own hypotheses. The source's proof of [Stacks, Tag 0D2R] cites [Stacks, Tag 09MW] at exactly this point. Everything else is proved: an affine open V' of S' has j^{-1}V' affine because j is a closed immersion, the commutative square identifies f^{-1}(j^{-1}V') with i^{-1}(f'^{-1}V'), and the restricted morphism i ∣_ (f'^{-1}V') is again a thickening.

theorem isRelativelyAmple_of_isRelativelyAmple_pullback (href : AmpleReflectedByThickening.{u})
    (hi : IsThickening i) (hj : IsThickening j) (hsq : i ≫ f' = f ≫ j)
    (hL : IsRelativelyAmple f (pullbackModule i L')) :
    IsRelativelyAmple f' L'

Stacks.ThickeningInvertible.isRelativelyAmple_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ThickeningInvertible/Basic.lean, line 401. The attribute's comment: “the biconditional, carrying href = the mp half of [Tag 09MW]”.

[Stacks, Tag 0D2R], granted [Stacks, Tag 09MW]. For a morphism of thickenings (f, f') : (X ⊆ X') → (S ⊆ S') and an invertible 𝒪_{X'}-module ℒ' with restriction ℒ = i^* ℒ' to X, the module ℒ' is f'-ample if and only if ℒ is f-ample.

The mp half is Stacks.ThickeningInvertible.isRelativelyAmple_pullback and uses no hypothesis beyond the source's; the mpr half is Stacks.ThickeningInvertible.isRelativelyAmple_of_isRelativelyAmple_pullback and carries href.

theorem isRelativelyAmple_iff (href : AmpleReflectedByThickening.{u}) (hi : IsThickening i)
    (hj : IsThickening j) (hsq : i ≫ f' = f ≫ j) :
    IsRelativelyAmple f' L' ↔ IsRelativelyAmple f (pullbackModule i L')

Tag 09ZW, a lemma

Tag 09ZW in the Stacks Project.

Stacks.Thickenings.locallyOfFiniteType_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Cartesian.lean, line 170. The attribute's comment: “locally_finite_type”.

Local finite type ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem locallyOfFiniteType_iff_of_isFiniteOrderThickening
    {X X' S S' : Scheme.{u}} (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S')
    (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) :
    LocallyOfFiniteType f ↔ LocallyOfFiniteType f'

Stacks.Thickenings.locallyQuasiFinite_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Cartesian.lean, line 235. The attribute's comment: “locally_quasi_finite”.

Local quasi-finiteness is invariant under a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem locallyQuasiFinite_iff_of_isFiniteOrderThickening
    {X X' S S' : Scheme.{u}} (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S')
    (hi : IsThickening i)
    (hj : IsFiniteOrderThickening j)
    (sq : IsPullback i f f' j) :
    (LocallyOfFiniteType f ∧ LocallyQuasiFinite f) ↔
      (LocallyOfFiniteType f' ∧ LocallyQuasiFinite f')

Stacks.Thickenings.isProper_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Cartesian.lean, line 254. The attribute's comment: “proper”.

Properness ascends and descends along a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem isProper_iff_of_isFiniteOrderThickening
    {X X' S S' : Scheme.{u}} (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S')
    (hi : IsThickening i)
    (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) :
    IsProper f ↔ IsProper f'

Stacks.Thickenings.formallyUnramified_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianDifferentials.lean, line 180. The attribute's comment: “vanishing_differentials”.

Stacks 09ZW, part (5). The relative differentials of f vanish exactly when the relative differentials of f' vanish, for a cartesian morphism of thickenings whose base thickening has finite order.

theorem formallyUnramified_iff_of_isFiniteOrderThickening
    {X X' S S' : Scheme.{u}} (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S')
    (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) :
    FormallyUnramified f ↔ FormallyUnramified f'

Stacks.Thickenings.isClosedImmersion_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianImmersions.lean, line 135. The attribute's comment: “closed_immersion”.

Stacks 09ZW, part (1). Being a closed immersion ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem isClosedImmersion_iff_of_isFiniteOrderThickening (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S') (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) : IsClosedImmersion f ↔ IsClosedImmersion f'

Stacks.Thickenings.isFinite_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianImmersions.lean, line 144. The attribute's comment: “finite”.

Stacks 09ZW, part (8). Being finite ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem isFinite_iff_of_isFiniteOrderThickening (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S') (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) : IsFinite f ↔ IsFinite f'

Stacks.Thickenings.isImmersion_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianImmersions.lean, line 153. The attribute's comment: “immersion”.

Stacks 09ZW, part (10). Being an immersion ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem isImmersion_iff_of_isFiniteOrderThickening (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S') (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) : IsImmersion f ↔ IsImmersion f'

Stacks.Thickenings.mono_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianImmersions.lean, line 248. The attribute's comment: “monomorphism”.

Stacks 09ZW, part (9). Being a monomorphism ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

theorem mono_iff_of_isFiniteOrderThickening (i : X ⟶ X') (j : S ⟶ S')
    (f : X ⟶ S) (f' : X' ⟶ S') (hj : IsFiniteOrderThickening j)
    (hcart : IsPullback i f f' j) : Mono f ↔ Mono f'

Stacks.Thickenings.locallyOfFiniteType_and_relativeDimension_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/CartesianRelativeDimension.lean, line 143. The attribute's comment: “relative_dimension”.

Stacks 09ZW, part (4). Being locally of finite type of relative dimension d ascends and descends across a cartesian morphism of thickenings when the thickening of the base has finite order.

The property is the conjunction of local finite type and relative dimension d, and the statement is that conjunction; its first half is part (2) of the same tag.

theorem locallyOfFiniteType_and_relativeDimension_iff_of_isFiniteOrderThickening
    (i : X ⟶ X') (j : S ⟶ S') (f : X ⟶ S) (f' : X' ⟶ S')
    (hj : IsFiniteOrderThickening j) (hcart : IsPullback i f f' j) (d : ℕ) :
    (∃ _ : LocallyOfFiniteType f, RelativeDimension f d) ↔
      (∃ _ : LocallyOfFiniteType f', RelativeDimension f' d)

Stacks.Thickenings.unramified_iff_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismEtaleLocal.lean, line 111. The attribute's comment: “unramified”.

Stacks 09ZW, part (6). Unramifiedness ascends and descends across a cartesian morphism of thickenings of schemes when the thickening of the base has finite order.

The invariance of unramifiedness under a cartesian morphism of thickenings, Stacks.Thickenings.IsThickening.unramified_iff_of_isPullback, needs the deformation f' to be locally of finite type; the finite order of j provides it from local finite type of f, by part (2) of this tag. No finiteness hypothesis on the source thickening i is used.

theorem unramified_iff_of_isFiniteOrderThickening
    {X X' S S' : Scheme.{u}} (i : X ⟶ X') (j : S ⟶ S') (f : X ⟶ S) (f' : X' ⟶ S')
    (hj : Stacks.Thickenings.IsFiniteOrderThickening j) (hcart : IsPullback i f f' j) :
    Unramified f ↔ Unramified f'

Tag 0BPG, a lemma

Tag 0BPG in the Stacks Project.

Stacks.Thickenings.CartesianFiniteTypeMorphism.locallyQuasiFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/EtaleLocalProperties.lean, line 89. The attribute's comment: “locally_quasi_finite”.

Stacks 0BPG, part (1). Being locally quasi-finite is invariant under a cartesian, locally finite type morphism of thickenings of schemes.

theorem CartesianFiniteTypeMorphism.locallyQuasiFinite_iff
    (S : CartesianFiniteTypeMorphism.{u}) :
    (LocallyOfFiniteType S.f ∧ LocallyQuasiFinite S.f) ↔
      (LocallyOfFiniteType S.f' ∧ LocallyQuasiFinite S.f')

Stacks.Thickenings.CartesianFiniteTypeMorphism.isClosedImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Extension.lean, line 122. The attribute's comment: “closed_immersion”.

Being a closed immersion is invariant under a cartesian, locally finite type morphism of thickenings.

theorem isClosedImmersion_iff (S : CartesianFiniteTypeMorphism.{u}) :
    IsClosedImmersion S.f ↔ IsClosedImmersion S.f'

Stacks.Thickenings.CartesianFiniteTypeMorphism.isImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Extension.lean, line 150. The attribute's comment: “immersion”.

Being an immersion is invariant under a cartesian, locally finite type morphism of thickenings.

theorem isImmersion_iff (S : CartesianFiniteTypeMorphism.{u}) :
    IsImmersion S.f ↔ IsImmersion S.f'

Stacks.Thickenings.CartesianFiniteTypeMorphism.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Extension.lean, line 274. The attribute's comment: “proper”.

Properness is invariant under a cartesian, locally finite type morphism of thickenings.

theorem isProper_iff (S : CartesianFiniteTypeMorphism.{u}) :
    IsProper S.f ↔ IsProper S.f'

Stacks.Thickenings.CartesianFiniteTypeMorphism.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Extension.lean, line 286. The attribute's comment: “finite”.

Finiteness is invariant under a cartesian, locally finite type morphism of thickenings: a morphism of schemes is finite exactly when it is proper and locally quasi-finite, and both of those are invariant.

theorem isFinite_iff (S : CartesianFiniteTypeMorphism.{u}) :
    IsFinite S.f ↔ IsFinite S.f'

Stacks.Thickenings.CartesianFiniteTypeMorphism.isZero_relativeDifferentials_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Monomorphism.lean, line 68. The attribute's comment: “vanishing_differentials”.

Stacks 0BPG, part (4). In a cartesian morphism of thickenings whose two component morphisms are locally of finite type, the sheaf of relative differentials Ω_{X/Y} is zero if and only if Ω_{X'/Y'} is zero.

theorem isZero_relativeDifferentials_iff (S : CartesianFiniteTypeMorphism.{u}) :
    IsZero S.f.relativeDifferentials ↔ IsZero S.f'.relativeDifferentials

Stacks.Thickenings.CartesianFiniteTypeMorphism.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Monomorphism.lean, line 109. The attribute's comment: “monomorphism”.

Stacks 0BPG, part (6). Being a monomorphism is invariant under a cartesian, locally finite type morphism of thickenings.

theorem mono_iff (S : CartesianFiniteTypeMorphism.{u}) : Mono S.f ↔ Mono S.f'

Stacks.Thickenings.CartesianFiniteTypeMorphism.unramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Unramified.lean, line 103. The attribute's comment: “unramified”.

Being unramified is invariant under a cartesian, locally finite type morphism of thickenings.

theorem CartesianFiniteTypeMorphism.unramified_iff (S : CartesianFiniteTypeMorphism.{u}) :
    Unramified S.f ↔ Unramified S.f'

Sources

LeanStacks.Thickenings.isAffineHom_left_iff_right · Stacks.Thickenings.isIntegralHom_left_iff_right · Stacks.Thickenings.isQuasiAffineHom_left_iff_right · Stacks.Thickenings.isSeparated_left_iff_right · Stacks.Thickenings.quasiSeparated_left_iff_right · Stacks.Thickenings.quasiCompact_left_iff_right · Stacks.Thickenings.surjective_left_iff_right · Stacks.Thickenings.universallyClosed_left_iff_right

Section37.4 Picard groups of thickenings #

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

Tag 0C6R, a lemma

Tag 0C6R in the Stacks Project.

Stacks.Thickenings.thickeningShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 823. The attribute's comment: “the short exact sequence of sheaves”.

The sequence of sheaves 0 ⟶ ℐ ⟶ 𝒪_{X'}^* ⟶ i_* 𝒪_X^* ⟶ 0 of a first-order thickening is short exact.

theorem thickeningShortComplex_shortExact (i : X ⟶ X') (hi : IsFirstOrderThickening i) :
    (thickeningShortComplex i hi).ShortExact

Stacks.Thickenings.injective_idealToUnitsCohomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 916. The attribute's comment: “injectivity at the global sections of the ideal”.

The sequence starts with an injection: a global section of the ideal sheaf giving the unit 1 is zero.

theorem injective_idealToUnitsCohomology_zero (i : X ⟶ X')
    (hi : IsFirstOrderThickening i) :
    Function.Injective (idealToUnitsCohomology i hi 0)

Stacks.Thickenings.exact_idealToUnitsCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 923. The attribute's comment: “exactness at the cohomology of the units of the thickening”.

Exactness at H^n(X', 𝒪_{X'}^*).

theorem exact_idealToUnitsCohomology (i : X ⟶ X') (hi : IsFirstOrderThickening i)
    (n : ℕ) :
    Function.Exact (idealToUnitsCohomology i hi n) (unitsToSubCohomology i n)

Stacks.Thickenings.exact_unitsToSubCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 930. The attribute's comment: “exactness at the cohomology of the units of the closed subscheme”.

Exactness at H^n(X, 𝒪_X^*).

theorem exact_unitsToSubCohomology (i : X ⟶ X') (hi : IsFirstOrderThickening i)
    (n : ℕ) :
    Function.Exact (unitsToSubCohomology i n) (thickeningBoundary i hi n)

Stacks.Thickenings.exact_thickeningBoundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 937. The attribute's comment: “exactness at the cohomology of the ideal”.

Exactness at H^{n+1}(X, ℐ).

theorem exact_thickeningBoundary (i : X ⟶ X') (hi : IsFirstOrderThickening i) (n : ℕ) :
    Function.Exact (thickeningBoundary i hi n) (idealToUnitsCohomology i hi (n + 1))

Stacks.Thickenings.exact_picardOfIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 943. The attribute's comment: “exactness at the Picard group of the thickening”.

Exactness at Pic(X').

theorem exact_picardOfIdeal (i : X ⟶ X') (hi : IsFirstOrderThickening i) :
    Function.Exact (picardOfIdeal i hi) (picardRestriction i hi)

Stacks.Thickenings.exact_picardRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardSequence.lean, line 952. The attribute's comment: “exactness at the Picard group of the closed subscheme”.

Exactness at Pic(X).

theorem exact_picardRestriction (i : X ⟶ X') (hi : IsFirstOrderThickening i) :
    Function.Exact (picardRestriction i hi) (picardBoundary i hi)

Stacks.Thickenings.unitsKernelShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardTorsionGeneral.lean, line 435. The attribute's comment: “the short exact sequence of sheaves, for an arbitrary thickening, with the sheaf of units congruent to one presented as a kernel”.

Stacks Project, Tag 0C6R for an arbitrary thickening: the sequence of sheaves 0 ⟶ 𝒦 ⟶ 𝒪_{X'}^* ⟶ i_* 𝒪_X^* ⟶ 0 is short exact, where 𝒦 is the kernel of restriction of units, i.e. the sheaf of units congruent to 1 modulo the ideal of X.

theorem unitsKernelShortComplex_shortExact (i : X ⟶ X') (hi : IsThickening i) :
    (unitsKernelShortComplex i).ShortExact

Tag 0C6S, a lemma

Tag 0C6S in the Stacks Project.

Stacks.Thickenings.bijOn_schemePullbackClass_zsmulTorsion_of_globalUnitsPowerLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/PicardTorsionGeneral.lean, line 845.

Stacks Project, Tag 0C6S in its corrected form (an erratum to the printed statement). For a thickening i : X ⟶ X' and an integer n invertible in 𝒪_X, assuming every invertible global function on X is an n-th power times the restriction of an invertible global function on X', restriction of invertible modules is a bijection Pic(X')[n] → Pic(X)[n].

The original statement omitted that assumption and is refuted by Stacks.Examples.TwistedDoubledLine.not_forall_bijOn_schemePullbackClass_zsmulTorsion; the assumption is not merely sufficient but necessary, by Stacks.Thickenings.bijOn_schemePullbackClass_zsmulTorsion_iff.

theorem bijOn_schemePullbackClass_zsmulTorsion_of_globalUnitsPowerLift (i : X ⟶ X')
    (hi : IsThickening i) {n : ℤ} (hn : IsUnit ((n : ℤ) : Γ(X, ⊤)))
    (hpow : GlobalUnitsPowerLift i n) :
    Set.BijOn (schemePullbackClass i) (zsmulTorsion (ofScheme X') n)
      (zsmulTorsion (ofScheme X) n)

Sources

LeanStacks.Thickenings.thickeningShortComplex_shortExact · Stacks.Thickenings.injective_idealToUnitsCohomology_zero · Stacks.Thickenings.exact_idealToUnitsCohomology · Stacks.Thickenings.exact_unitsToSubCohomology · Stacks.Thickenings.exact_thickeningBoundary · Stacks.Thickenings.exact_picardOfIdeal · Stacks.Thickenings.exact_picardRestriction · Stacks.Thickenings.unitsKernelShortComplex_shortExact

Section37.5 Infinitesimal neighbourhoods #

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

Tag 04EY, a definition

Tag 04EY in the Stacks Project.

Stacks.Thickenings.nthOrderInfinitesimalNeighbourhood, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 81. The attribute's comment: “part (2): nth-order infinitesimal neighbourhood”. References: EGA IV (16.1.2), “special case”; EGA IV (19.4.6); SGA 2 XI (3.18), “more general”.

Stacks Project, Tag 04EY, part (2). The nth-order infinitesimal neighbourhood of Z in X for an immersion i : Z ⟶ X: the closed subscheme of the canonical open neighbourhood AlgebraicGeometry.Scheme.Hom.coborderRange of the image of i cut out by the (n+1)st power of the defining ideal sheaf of AlgebraicGeometry.Scheme.Hom.liftCoborder.

def nthOrderInfinitesimalNeighbourhood (n : ℕ) : Scheme.{u}

Stacks.Thickenings.firstOrderInfinitesimalNeighbourhood, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 88. The attribute's comment: “part (1): first-order infinitesimal neighbourhood”. References: EGA IV (16.1.2), “Y^{(1)}, immersions”.

Stacks Project, Tag 04EY, part (1). The first-order infinitesimal neighbourhood of Z in X, cut out by the square of the defining ideal sheaf of the immersion.

abbrev firstOrderInfinitesimalNeighbourhood : Scheme.{u}

Stacks.Thickenings.nthOrderInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 111. The attribute's comment: “part (2): inclusion into the nth-order neighbourhood”. References: EGA IV (16.1.2), “Y^{(n)} inclusion”.

The inclusion of Z into its nth-order infinitesimal neighbourhood.

def nthOrderInclusion (n : ℕ) : Z ⟶ nthOrderInfinitesimalNeighbourhood i n

Stacks.Thickenings.nthOrderToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 120. The attribute's comment: “part (2): map from the nth-order neighbourhood to the base”.

The structure morphism from the nth-order infinitesimal neighbourhood of Z in X to X.

def nthOrderToBase (n : ℕ) : nthOrderInfinitesimalNeighbourhood i n ⟶ X

Stacks.Thickenings.nthOrderInclusion_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 141. The attribute's comment: “part (2): factorization over the base”.

The inclusion of Z into its nth-order infinitesimal neighbourhood, followed by the structure morphism to X, is the original immersion.

theorem nthOrderInclusion_toBase (n : ℕ) :
    nthOrderInclusion i n ≫ nthOrderToBase i n = i

Stacks.Thickenings.nthOrderInclusion_isNthOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 181. The attribute's comment: “part (2): nth-order thickening”.

Stacks Project, Tag 04EY, part (2). The inclusion of Z into its nth-order infinitesimal neighbourhood is an nth-order thickening: it is a closed immersion whose defining ideal sheaf has vanishing (n+1)st power.

Affine-locally on the open neighbourhood AlgebraicGeometry.Scheme.Hom.coborderRange, the (n+1)st power of the ideal sheaf of i.liftCoborder is the kernel of the surjection onto the sections of the neighbourhood, so the (n+1)st power of its image vanishes.

theorem nthOrderInclusion_isNthOrderThickening (n : ℕ) :
    IsNthOrderThickening n (nthOrderInclusion i n)

Stacks.Thickenings.nthOrderInclusion_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 216. The attribute's comment: “part (1): first-order thickening”.

Stacks Project, Tag 04EY, part (1). The inclusion of Z into its first-order infinitesimal neighbourhood is a first-order thickening.

theorem nthOrderInclusion_isFirstOrderThickening :
    IsFirstOrderThickening (nthOrderInclusion i 1)

Tag 04EZ, a lemma

Tag 04EZ in the Stacks Project.

Stacks.Thickenings.existsUnique_nthOrderLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 385. The attribute's comment: “part (2): nth-order universal property”.

Stacks Project, Tag 04EZ, part (2). The universal property of the nth-order infinitesimal neighbourhood: given an nth-order thickening j : T ⟶ T', a morphism a : T ⟶ Z and a morphism b : T' ⟶ X making the square commute, there is a unique morphism T' ⟶ Z_n extending a and lying over b.

Since j is surjective on points, b lands in the open subscheme AlgebraicGeometry.Scheme.Hom.coborderRange and so factors as f ≫ i.coborderRange.ι. The square then reads j ≫ f = a ≫ i.liftCoborder, so Stacks.Thickenings.ker_pow_le_ker_of_comm_square gives i.liftCoborder.ker ^ (n + 1) ≤ f.ker and f factors through the closed subscheme cut out by i.liftCoborder.ker ^ (n + 1), which is Z_n. Uniqueness is monomorphicity of the two immersions.

The source's hypothesis 1 ≤ n is retained for faithfulness but is not needed: the argument is uniform in n, and at n = 0 both sides degenerate to Z itself.

theorem existsUnique_nthOrderLift {T T' : Scheme.{u}}
    (n : ℕ) (_hn : 1 ≤ n) (j : T ⟶ T') (hj : IsNthOrderThickening n j)
    (a : T ⟶ Z) (b : T' ⟶ X) (h : j ≫ b = a ≫ i) :
    ∃! a' : T' ⟶ nthOrderInfinitesimalNeighbourhood i n,
      (j ≫ a' = a ≫ nthOrderInclusion i n) ∧ (a' ≫ nthOrderToBase i n = b)

Stacks.Thickenings.existsUnique_firstOrderLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Infinitesimal.lean, line 432. The attribute's comment: “part (1): first-order universal property”.

Stacks Project, Tag 04EZ, part (1). The universal property of the first-order infinitesimal neighbourhood, the case n = 1 of Stacks.Thickenings.existsUnique_nthOrderLift.

theorem existsUnique_firstOrderLift {T T' : Scheme.{u}}
    (j : T ⟶ T') (hj : IsFirstOrderThickening j)
    (a : T ⟶ Z) (b : T' ⟶ X) (h : j ≫ b = a ≫ i) :
    ∃! a' : T' ⟶ firstOrderInfinitesimalNeighbourhood i,
      (j ≫ a' = a ≫ nthOrderInclusion i 1) ∧ (a' ≫ nthOrderToBase i 1 = b)

Tag 04F0, a lemma

Tag 04F0 in the Stacks Project.

Stacks.Thickenings.isIso_conormalTransitivityMap_nthOrderInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/InfinitesimalConormalSheaf.lean, line 460.

Stacks Project, Tag 04F0. For an immersion i : Z ⟶ X with first-order infinitesimal neighbourhood Z ⊂ Z' of [Stacks Project, Tag 04EY], the canonical map of conormal sheaves 𝒞_{Z/X} ⟶ 𝒞_{Z/Z'} of [Stacks Project, Tag 01R4] is an isomorphism.

The map is Stacks.ConormalSequenceTwoImmersions.conormalTransitivityMap for the factorization Z ⟶ Z' ⟶ X of i, which is the map of [Stacks Project, Tag 01R4] for the square with horizontal arrows Z ⟶ Z' and Z ⟶ X and vertical arrows the identity of Z and Z' ⟶ X.

theorem isIso_conormalTransitivityMap_nthOrderInclusion :
    IsIso (Stacks.ConormalSequenceTwoImmersions.conormalTransitivityMap
      (nthOrderInclusion i 1) i (nthOrderToBase i 1) (nthOrderInclusion_toBase i 1))

Sources

LeanStacks.Thickenings.nthOrderInfinitesimalNeighbourhood · Stacks.Thickenings.firstOrderInfinitesimalNeighbourhood · Stacks.Thickenings.nthOrderInclusion · Stacks.Thickenings.nthOrderToBase · Stacks.Thickenings.nthOrderInclusion_toBase · Stacks.Thickenings.nthOrderInclusion_isNthOrderThickening · Stacks.Thickenings.nthOrderInclusion_isFirstOrderThickening · Stacks.Thickenings.existsUnique_nthOrderLift

Section37.6 Formally unramified morphisms #

Section 37.6 of the Stacks Project, Tag 02H7. 7 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02H8, a definition

Tag 02H8 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormallyUnramified registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 24 (StacksFrontier): “Mathlib's definition: the ring maps on affine opens are formally unramified”. References: EGA IV (17.1.1); SGA 3 XI (1.1); SGA 3 XI (1.6), “special case”.
AlgebraicGeometry.FormallyUnramified.hom_ext registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 26 (StacksFrontier): “a formally unramified morphism has at most one dotted arrow, for any nilpotent closed immersion (in particular a first order thickening)”. References: EGA IV (17.1.1), “partial”; EGA IV (17.1.2), “special case”; SGA 1 I (5.6), “special case”; SGA 3 XI (1.1), “partial”; SGA 3 XI (1.5), “partial”; SGA 3 XI (1.6), “represented functors”.
AlgebraicGeometry.FormallyUnramified.of_hom_ext registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 29 (StacksFrontier): “conversely, at most one dotted arrow for first order thickenings of affine schemes implies formally unramified”. References: EGA 0 (19.10.4), “partial”; EGA IV (17.1.1), “partial”; SGA 3 XI (1.1), “partial”; SGA 3 XI (1.6), “represented functors”.

Tag 02HA, a lemma

Tag 02HA in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 31 (StacksFrontier). References: EGA IV (17.1.3), “clause (ii)”; EGA IV (17.1.5), “partial”.

Tag 02HB, a lemma

Tag 02HB in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 32 (StacksFrontier). References: EGA IV (17.1.3), “clause (iii)”; EGA IV (17.7.3), “partial”; SGA 3 XI (1.6), “partial”.

Tag 02HC, a lemma

Tag 02HC in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 33 (StacksFrontier): “formally unramified is the affine-local property of formally unramified ring maps, hence local on the source and on the target”.
AlgebraicGeometry.IsZariskiLocalAtSource.resLE registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 36 (StacksFrontier): “a property local on the source and the target is preserved by restriction f|_U : U → V”.

Tag 02HD, a lemma

Tag 02HD in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 38 (StacksFrontier): “formally unramified is the affine-local property of formally unramified ring maps”.
AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 40 (StacksFrontier): “for X and S affine, such a property holds iff it holds for the ring map on global sections”.

Tag 02H9, a lemma

Tag 02H9 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.formallyUnramified_iff_isZero_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Differentials.lean, line 68. References: EGA IV (17.2.1); EGA IV (17.2.2), “case Z = Y”; EGA IV (17.4.2), “a) ⇔ c)”.

A morphism of schemes is formally unramified if and only if its sheaf of relative differentials is a zero object.

theorem formallyUnramified_iff_isZero_relativeDifferentials (f : X ⟶ S) :
    FormallyUnramified f ↔ IsZero (relativeDifferentials f)

Tag 02HE, a lemma

Tag 02HE in the Stacks Project.

AlgebraicGeometry.unramified_iff_locallyOfFiniteType_and_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 215. The attribute's comment: “unramified case”. References: EGA IV (17.4.1.2), “a) formally unramified”; EGA IV (17.4.2), “a) ⇔ e)”; EGA IV (17.4.1), “a) <=> e)”.

A morphism of schemes is unramified if and only if it is locally of finite type and formally unramified.

public theorem unramified_iff_locallyOfFiniteType_and_formallyUnramified (f : X ⟶ S) :
    Unramified f ↔ (LocallyOfFiniteType f ∧ FormallyUnramified f)

AlgebraicGeometry.gUnramified_iff_locallyOfFinitePresentation_and_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Properties.lean, line 227. The attribute's comment: “G-unramified case”. References: EGA IV (17.3.2), “(ii) unramified”; EGA IV (17.4.2), “a) ⇔ e)”; EGA IV (17.4.1), “a) <=> e)”; EGA IV (17.3.1), “unramified (net)”.

A morphism of schemes is G-unramified if and only if it is locally of finite presentation and formally unramified.

public theorem gUnramified_iff_locallyOfFinitePresentation_and_formallyUnramified (f : X ⟶ S) :
    GUnramified f ↔ (LocallyOfFinitePresentation f ∧ FormallyUnramified f)

Sources

LeanAlgebraicGeometry.FormallyUnramified · AlgebraicGeometry.FormallyUnramified.hom_ext · AlgebraicGeometry.FormallyUnramified.of_hom_ext · AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme · AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme · AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified · AlgebraicGeometry.IsZariskiLocalAtSource.resLE · AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine

Section37.7 Universal first order thickenings #

Section 37.7 of the Stacks Project, Tag 04F2. 12 tags here are carried by 44 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04F3, a lemma

Tag 04F3 in the Stacks Project.

Stacks.Thickenings.nonempty_universalFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Existence/Gluing.lean, line 494.

Stacks Project, Tag 04F3. A formally unramified morphism of schemes admits a universal first-order thickening. It is constructed by gluing the thickenings of the charts of an affine open cover of Z subordinate to an affine open cover of X; the affine charts come from the algebraic universal first-order thickening (Algebra.FormallyUnramified.universalFirstOrderThickening, Tag 04EB).

theorem nonempty_universalFirstOrderThickening {Z X : Scheme.{u}} (h : Z ⟶ X)
    [FormallyUnramified h] : Nonempty (UniversalFirstOrderThickening h)

Stacks.Thickenings.universalFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Existence/Gluing.lean, line 542.

Stacks Project, Tag 04F3. The universal first-order thickening of a formally unramified morphism h : Z ⟶ X, chosen by Stacks.Thickenings.nonempty_universalFirstOrderThickening.

The universal property is part of the data, as the field Stacks.Thickenings.UniversalFirstOrderThickening.isUniversal; it is spelled out in Stacks.Thickenings.universalFirstOrderThickening_isUniversal and its consequences below. Nothing beyond that property should be used: by Stacks.Thickenings.UniversalFirstOrderThickening.canonicalIso the choice is unique up to unique isomorphism, which is why the ambient scheme is left opaque here rather than exposed as the glued scheme.

noncomputable def universalFirstOrderThickening {Z X : Scheme.{u}} (h : Z ⟶ X)
    [FormallyUnramified h] : UniversalFirstOrderThickening h

Tag 04F4, a definition

Tag 04F4 in the Stacks Project.

Stacks.Thickenings.universalConormalSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormalSheaf.lean, line 144. The attribute's comment: “part (2): conormal sheaf”.

Stacks Project, Tag 04F4, part (2). The conormal sheaf 𝒞_{Z/X} of a formally unramified morphism h : Z ⟶ X: the conormal sheaf, in the sense of Stacks.Thickenings.immersionConormalSheaf ([Stacks Project, Tag 01R2]), of the inclusion of Z into the universal first-order thickening of Z over X chosen by Stacks.Thickenings.universalFirstOrderThickening.

The inclusion is a closed immersion, hence an immersion, by Stacks.Thickenings.UniversalFirstOrderThickening.isClosedImmersion_inclusion.

noncomputable abbrev universalConormalSheaf {Z X : Scheme.{u}} (h : Z ⟶ X)
    [FormallyUnramified h] :
    SheafOfModules.{u} (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace)

Declarations registered for the tag:

Stacks.Thickenings.universalFirstOrderThickening, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormalSheaf.lean, line 132 (StacksFrontier): “part (1): universal first-order thickening”.

Tag 04F5, a lemma

Tag 04F5 in the Stacks Project.

Stacks.Thickenings.universalThickeningIsoFirstOrderNeighbourhood, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/ImmersionConormalIdentification.lean, line 119. The attribute's comment: “part (2): the chosen universal first-order thickening is the first-order infinitesimal neighbourhood”.

The ambient scheme of the universal first-order thickening of an immersion i : Z ⟶ X chosen by Stacks.Thickenings.universalFirstOrderThickening is isomorphic to the first-order infinitesimal neighbourhood of Z in X of [Stacks Project, Tag 04EY].

The isomorphism is the canonical one between two universal first-order thickenings of the same morphism, Stacks.Thickenings.UniversalFirstOrderThickening.canonicalIso. It is the unique isomorphism of thickenings of Z over X, by Stacks.Thickenings.UniversalFirstOrderThickening.existsUnique_canonicalMap.

def universalThickeningIsoFirstOrderNeighbourhood :
    (universalFirstOrderThickening i).ambient ≅ firstOrderInfinitesimalNeighbourhood i

Stacks.Thickenings.immersionConormalSheafIsoUniversalConormalSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/ImmersionConormalIdentification.lean, line 201. The attribute's comment: “part (3): the two conormal sheaves agree”.

For an immersion i : Z ⟶ X, the conormal sheaf of i in the sense of [Stacks Project, Tag 01R2], Stacks.Thickenings.immersionConormalSheaf i, agrees with the conormal sheaf of i in the sense of [Stacks Project, Tag 04F4], Stacks.Thickenings.universalConormalSheaf i, built from the universal first-order thickening chosen by Stacks.Thickenings.universalFirstOrderThickening.

It is the composite of the comparison Stacks.Thickenings.infinitesimalConormalTransitivityMap of [Stacks Project, Tag 04F0], Stacks.Immersion.conormalSheafSelfIso for the inclusion Z ⟶ Z₁, and Stacks.Thickenings.universalConormalSheafIsoFirstOrderNeighbourhood.

def immersionConormalSheafIsoUniversalConormalSheaf :
    immersionConormalSheaf i ≅ universalConormalSheaf i

Declarations registered for the tag:

Stacks.Thickenings.formallyUnramified_of_isImmersion, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Thickenings/ImmersionConormalIdentification.lean, line 98 (StacksFrontier): “part (1): an immersion of schemes is formally unramified”.
Stacks.Thickenings.isUniversalFirstOrderThickening_nthOrderInclusion_one, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Thickenings/ImmersionConormalIdentification.lean, line 103 (StacksFrontier): “part (2): the first-order infinitesimal neighbourhood has the universal property of a first-order thickening over the base”.

Tag 04F6, a lemma

Tag 04F6 in the Stacks Project.

Stacks.Thickenings.UniversalFirstOrderThickening.formallyUnramified_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormalSheaf.lean, line 160.

Stacks Project, Tag 04F6. The ambient scheme of a universal first-order thickening of a formally unramified morphism h : Z ⟶ X is formally unramified over X.

The thickening produced by the gluing construction of [Stacks Project, Tag 04F3] has this property, by Stacks.Thickenings.exists_universalFirstOrderThickening_formallyUnramified_toBase, and any other universal first-order thickening of h is isomorphic to it over X by Stacks.Thickenings.UniversalFirstOrderThickening.canonicalIso.

theorem UniversalFirstOrderThickening.formallyUnramified_toBase {Z X : Scheme.{u}} {h : Z ⟶ X}
    [FormallyUnramified h] (t : UniversalFirstOrderThickening h) :
    FormallyUnramified t.toBase

Tag 04F7, a lemma

Tag 04F7 in the Stacks Project.

Stacks.Thickenings.universalConormalSheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/ConormalSheaf.lean, line 291. The attribute's comment: “the induced morphism of conormal sheaves”.

Stacks 04F7, the conormal half. Let h : Z ⟶ X and h' : W ⟶ Y be formally unramified, let Z ⊂ Z' and W ⊂ W' be universal first-order thickenings of h and of h', and let h ≫ g = f ≫ h' be a commutative square. The canonical morphism (f, f') of thickenings of Stacks.Thickenings.universalFirstOrderThickeningMap induces a morphism of conormal sheaves

f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X}.

It is the map of [Stacks Project, Tag 01R4] applied to the square (Z ⊂ Z') → (W ⊂ W'), namely Stacks.ClosedImmersion.conormalSheafMap, which for the inclusions of thickenings needs no reduction of immersions to closed immersions and no quotient by the square of the defining ideal. Its characterising property is Stacks.ClosedImmersion.conormalSheafMap_comp_pullback_ι.

noncomputable def universalConormalSheafMap
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    (modulePullback f.toLRSHom.toShHom).obj (schemeConormalSheaf tW.inclusion) ⟶
      schemeConormalSheaf tZ.inclusion

Stacks.Thickenings.UniversalFirstOrderThickening.existsUnique_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Universal.lean, line 152. The attribute's comment: “unique existence of the canonical morphism of thickenings”.

There is a unique morphism between the ambient schemes of two universal first-order thickenings which restricts to f on the closed subschemes and is compatible with the structure morphisms over g. This is the unique-existence statement behind the canonical morphism of Tag 04F7, obtained by applying the universal property of tW to the first-order thickening tZ.inclusion.

theorem existsUnique_map (tZ : UniversalFirstOrderThickening h)
    (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    ∃! k : tZ.ambient ⟶ tW.ambient,
      (tZ.inclusion ≫ k = f ≫ tW.inclusion) ∧ (k ≫ tW.toBase = tZ.toBase ≫ g)

Stacks.Thickenings.universalFirstOrderThickeningMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Universal.lean, line 169. The attribute's comment: “the canonical morphism of thickenings”.

The canonical morphism between the ambient schemes of two universal first-order thickenings associated to a commutative square. It is selected by the unique lifting property of the target thickening.

noncomputable def universalFirstOrderThickeningMap
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    tZ.ambient ⟶ tW.ambient

Stacks.Thickenings.universalFirstOrderThickeningMap_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Universal.lean, line 177. The attribute's comment: “compatibility with the inclusions”.

The canonical morphism restricts to f on the closed subscheme.

theorem universalFirstOrderThickeningMap_inclusion
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    tZ.inclusion ≫ universalFirstOrderThickeningMap tZ tW f g comm = f ≫ tW.inclusion

Stacks.Thickenings.universalFirstOrderThickeningMap_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Universal.lean, line 185. The attribute's comment: “compatibility with the base”.

The canonical morphism is a morphism over Y.

theorem universalFirstOrderThickeningMap_toBase
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    universalFirstOrderThickeningMap tZ tW f g comm ≫ tW.toBase = tZ.toBase ≫ g

Stacks.Thickenings.universalFirstOrderThickeningMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Universal.lean, line 194. The attribute's comment: “uniqueness of the canonical morphism”.

The canonical morphism is the unique extension of f over Y: any morphism of the ambient schemes restricting to f and compatible with the structure morphisms over g equals it.

theorem universalFirstOrderThickeningMap_unique
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h')
    (k : tZ.ambient ⟶ tW.ambient)
    (hk₁ : tZ.inclusion ≫ k = f ≫ tW.inclusion)
    (hk₂ : k ≫ tW.toBase = tZ.toBase ≫ g) :
    k = universalFirstOrderThickeningMap tZ tW f g comm

Stacks.Thickenings.universalConormalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormal.lean, line 208. The attribute's comment: “the induced morphism of conormal modules, on affine ambient thickenings”.

The map of conormal modules induced by the canonical morphism of universal first-order thickenings. For universal first-order thickenings tZ of h : Z ⟶ X and tW of h' : W ⟶ Y with affine ambient schemes, and a commutative square h ≫ g = f ≫ h', the canonical morphism tZ.ambient ⟶ tW.ambient of Stacks.Thickenings.universalFirstOrderThickeningMap carries the conormal module of tW into the conormal module of tZ, linearly over Γ(W, ⊤) acting through f.

This is the affine, module-level avatar of the morphism of conormal sheaves f^*𝒞_{W/Y} → 𝒞_{Z/X} asserted by [Stacks Project, Tag 04F7]; it is not that morphism, which lives on all of Z.

noncomputable def universalConormalMap (tZ : UniversalFirstOrderThickening h)
    (tW : UniversalFirstOrderThickening h') [IsAffine tZ.ambient] [IsAffine tW.ambient]
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    letI := Smooth.thickeningKerModule tW.isUniversal.isFirstOrderThickening
    letI := conormalModuleAlong tZ.isUniversal.isFirstOrderThickening f
    RingHom.ker tW.inclusion.appTop.hom →ₗ[Γ(W, (⊤ : W.Opens))]
      RingHom.ker tZ.inclusion.appTop.hom

Stacks.Thickenings.universalConormalMap_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormal.lean, line 227. The attribute's comment: “affine characterization of the induced morphism of conormal modules”.

The affine characterization of the induced map of conormal modules. On underlying sections the map of Stacks.Thickenings.universalConormalMap is the ring map of the canonical morphism tZ.ambient ⟶ tW.ambient of universal first-order thickenings.

This is the characterizing property of [Stacks Project, Tag 01R4] for the square (Z ⊂ Z') → (W ⊂ W'): a section of the defining ideal of W in W' goes to its image under the ambient ring map. For a first-order thickening the defining ideal is already its own conormal module, so there is no quotient by the square of the ideal.

theorem universalConormalMap_apply (tZ : UniversalFirstOrderThickening h)
    (tW : UniversalFirstOrderThickening h') [IsAffine tZ.ambient] [IsAffine tW.ambient]
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h')
    (x : RingHom.ker tW.inclusion.appTop.hom) :
    ((universalConormalMap tZ tW f g comm x : RingHom.ker tZ.inclusion.appTop.hom) :
        Γ(tZ.ambient, (⊤ : tZ.ambient.Opens)))
      = (universalFirstOrderThickeningMap tZ tW f g comm).appTop.hom
          (x : Γ(tW.ambient, (⊤ : tW.ambient.Opens)))

Stacks.Thickenings.isInducedConormalSheafMap_universalImmersionConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalConormalGenerators.lean, line 446. The attribute's comment: “affine characterization of the induced conormal-sheaf morphism”.

The affine characterization of the induced morphism of conormal sheaves. Let h : Z ⟶ X and h' : W ⟶ Y be formally unramified, let Z ⊂ Z' and W ⊂ W' be universal first-order thickenings of h and of h', and let h ≫ g = f ≫ h' be a commutative square. The morphism of conormal sheaves f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X} induced by the canonical morphism (f, f') of thickenings is the map of [Stacks Project, Tag 01R4] for the square (Z ⊂ Z') → (W ⊂ W'): on a compatible pair of affine opens V ⊆ W' and U ⊆ Z' cut out by ideals J and I, it carries the class of a : J in J/J² to the class in I/I² of the image of a under the ring map of f'.

theorem isInducedConormalSheafMap_universalImmersionConormalSheafMap
    (tZ : UniversalFirstOrderThickening h) (tW : UniversalFirstOrderThickening h')
    (f : Z ⟶ W) (g : X ⟶ Y) (comm : h ≫ g = f ≫ h') :
    IsInducedConormalSheafMap tZ.inclusion tW.inclusion f
      (universalFirstOrderThickeningMap tZ tW f g comm)
      (universalFirstOrderThickeningMap_inclusion tZ tW f g comm)
      (universalImmersionConormalSheafMap tZ tW f g comm)

Tag 04F8, a lemma

Tag 04F8 in the Stacks Project.

Stacks.Thickenings.formallyUnramified_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 116. The attribute's comment: “part (1): the base change of a formally unramified morphism”.

In a cartesian square of schemes, the base change of a formally unramified morphism is formally unramified.

theorem formallyUnramified_of_isPullback (sq : IsPullback h f g h')
    [FormallyUnramified h'] : FormallyUnramified h

Stacks.Thickenings.isUniversal_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 180. The attribute's comment: “part (2): X ×_Y W' is the universal first-order thickening of Z over X”.

The fibre product X ×_Y W' is a universal first-order thickening of Z = X ×_Y W over X.

theorem isUniversal_baseChange (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') :
    IsUniversalFirstOrderThickening h (baseChangeInclusion sq t) (baseChangeToBase g t)

Stacks.Thickenings.epi_immersionConormalSheafMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 308. The attribute's comment: “part (3): the canonical map f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X} is surjective”. References: EGA IV (17.13.1), “more general”.

For a cartesian square of schemes, with no flatness hypothesis on g, the canonical map of conormal sheaves f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 01R4] between the inclusions of universal first-order thickenings is surjective.

theorem epi_immersionConormalSheafMap_of_isPullback (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') :
    Epi (Stacks.Immersion.immersionConormalSheafMap tZ.inclusion t.inclusion f
      (universalFirstOrderThickeningMap tZ t f g sq.w)
      (Stacks.Immersion.toShHom_square
        (universalFirstOrderThickeningMap_inclusion tZ t f g sq.w)))

Stacks.Thickenings.epi_universalConormalSheafMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 321. The attribute's comment: “part (3): the canonical map of conormal sheaves of Tag 04F7 is surjective”.

For a cartesian square of schemes, the morphism of conormal sheaves Stacks.Thickenings.universalConormalSheafMap of [Stacks Project, Tag 04F7], induced by the canonical morphism of universal first-order thickenings, is surjective.

theorem epi_universalConormalSheafMap_of_isPullback (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') :
    Epi (universalConormalSheafMap tZ t f g sq.w)

Tag 04F9, a lemma

Tag 04F9 in the Stacks Project.

Stacks.Thickenings.flat_universalFirstOrderThickeningMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 277. The attribute's comment: “the morphism Z' ⟶ W' of universal first-order thickenings is flat”.

Let
Z --h--→ X
|        |
f        g
↓        ↓
W --h'-→ Y
be a cartesian square of schemes with g flat, let Z ⊂ Z' be a universal first-order thickening of h over X and W ⊂ W' one of h' over Y. Then the canonical morphism Z' ⟶ W' of [Stacks Project, Tag 04F7] is flat.

theorem flat_universalFirstOrderThickeningMap (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') [Flat g] :
    Flat (universalFirstOrderThickeningMap tZ t f g sq.w)

Stacks.Thickenings.isIso_immersionConormalSheafMap_of_isPullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 336. The attribute's comment: “the induced map f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X} of conormal sheaves is an isomorphism”.

For a cartesian square of schemes with g flat, the canonical map of conormal sheaves f^* 𝒞_{W/Y} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 01R4] between the inclusions of the two universal first-order thickenings is an isomorphism.

theorem isIso_immersionConormalSheafMap_of_isPullback_of_flat (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') [Flat g] :
    IsIso (Stacks.Immersion.immersionConormalSheafMap tZ.inclusion t.inclusion f
      (universalFirstOrderThickeningMap tZ t f g sq.w)
      (Stacks.Immersion.toShHom_square
        (universalFirstOrderThickeningMap_inclusion tZ t f g sq.w)))

Stacks.Thickenings.isIso_universalConormalSheafMap_of_isPullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/FlatBaseChange.lean, line 350. The attribute's comment: “the induced map of conormal sheaves of Tag 04F7 is an isomorphism”.

For a cartesian square of schemes with g flat, the morphism of conormal sheaves Stacks.Thickenings.universalConormalSheafMap of [Stacks Project, Tag 04F7], induced by the canonical morphism of universal first-order thickenings, is an isomorphism.

theorem isIso_universalConormalSheafMap_of_isPullback_of_flat (sq : IsPullback h f g h')
    (t : UniversalFirstOrderThickening h') [Flat g] :
    IsIso (universalConormalSheafMap tZ t f g sq.w)

Tag 04FA, a lemma

Tag 04FA in the Stacks Project.

AlgebraicGeometry.universalConormalSheafRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/UnramifiedConormal.lean, line 112. The attribute's comment: “restriction of the conormal sheaf to an open, as an isomorphism of sheaves of modules on that open”.

Stacks 04FA, the restriction of the conormal sheaf, as an isomorphism. For opens U of the source and V of the target of a formally unramified morphism f : X ⟶ S with f (U) ⊆ V, the restriction to U of the conormal sheaf of f is the conormal sheaf of the restriction of f to a morphism U ⟶ V.

noncomputable def universalConormalSheafRestrictIso {X S : Scheme.{u}} (f : X ⟶ S)
    [FormallyUnramified f] {V : S.Opens} {U : X.Opens} (hUV : U ≤ f ⁻¹ᵁ V)
    [FormallyUnramified (f.resLE V U hUV)] :
    (Scheme.Modules.restrictFunctor U.ι).obj (universalConormalSheaf f) ≅
      universalConormalSheaf (f.resLE V U hUV)

Stacks.Thickenings.isUniversalFirstOrderThickening_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Existence/Affine.lean, line 581. The attribute's comment: “the universal first-order thickening of an open is the corresponding open”.

Stacks Project, Tag 04FA, the second assertion. Let i : Z ⟶ Z' with structure morphism p : Z' ⟶ X be a universal first-order thickening of h : Z ⟶ X over X. Let U ⊆ X and V ⊆ Z be opens with h(V) ⊆ U, and let W ⊆ Z' be an open with Z ∩ W = V and p(W) ⊆ U. Then the restrictions i.resLE W V : V ⟶ W and p.resLE U W : W ⟶ U are a universal first-order thickening of h|_V : V ⟶ U over U.

That V ⟶ W is a first-order thickening is the statement that the restriction of a first-order thickening to an open subscheme of the ambient scheme is again one. The lifting property is the lifting property of Z' followed by the observation that the resulting lift T' ⟶ Z' factors through the open W: the points of T' are the points of T, which land in V, hence in W.

theorem isUniversalFirstOrderThickening_resLE {Z' : Scheme.{u}} {i : Z ⟶ Z'} {p : Z' ⟶ X}
    (hi : IsUniversalFirstOrderThickening h i p) {U : X.Opens} {V : Z.Opens} {W : Z'.Opens}
    (hWV : i ⁻¹ᵁ W = V) (hWU : W ≤ p ⁻¹ᵁ U) (hVU : V ≤ h ⁻¹ᵁ U) :
    IsUniversalFirstOrderThickening (h.resLE U V hVU) (i.resLE W V hWV.ge) (p.resLE U W hWU)

Stacks.Thickenings.formallyUnramified_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/OpenRestriction.lean, line 94. The attribute's comment: “formal unramifiedness of the restriction”.

Formal unramifiedness restricts to opens. If h : Z ⟶ X is formally unramified and V ⊆ Z, U ⊆ X are opens with h(V) ⊆ U, then h|_V : V ⟶ U is formally unramified.

theorem formallyUnramified_resLE (h : Z ⟶ X) [FormallyUnramified h] {U : X.Opens} {V : Z.Opens}
    (hVU : V ≤ h ⁻¹ᵁ U) : FormallyUnramified (h.resLE U V hVU)

Stacks.Thickenings.isIso_universalImmersionConormalSheafMap_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/OpenRestriction.lean, line 240. The attribute's comment: “restriction of the conormal sheaf”.

𝒞_{Z/X}|_V = 𝒞_{V/U}. For universal first-order thickenings Z ⊂ Z' of h : Z ⟶ X and V ⊂ V'' of h|_V : V ⟶ U, the canonical morphism of conormal sheaves (ι_V)^* 𝒞_{Z/X} ⟶ 𝒞_{V/U} of [Stacks Project, Tag 04F7] is an isomorphism.

theorem isIso_universalImmersionConormalSheafMap_resLE
    (t : UniversalFirstOrderThickening h) {U : X.Opens} {V : Z.Opens} (hVU : V ≤ h ⁻¹ᵁ U)
    (tV : UniversalFirstOrderThickening (h.resLE U V hVU)) :
    IsIso (universalImmersionConormalSheafMap tV t V.ι U.ι (Scheme.Hom.resLE_comp_ι h hVU))

Stacks.Thickenings.isIso_universalConormalSheafMap_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/OpenRestriction.lean, line 255. The attribute's comment: “restriction of the conormal sheaf, at the chosen thickenings”.

𝒞_{Z/X}|_V = 𝒞_{V/U} at the chosen thickenings. For a formally unramified h : Z ⟶ X and opens V ⊆ Z, U ⊆ X with h(V) ⊆ U, the canonical morphism (ι_V)^* 𝒞_{Z/X} ⟶ 𝒞_{V/U} between the conormal sheaves Stacks.Thickenings.universalConormalSheaf h and Stacks.Thickenings.universalConormalSheaf (h|_V) is an isomorphism.

theorem isIso_universalConormalSheafMap_resLE (h : Z ⟶ X) [FormallyUnramified h] {U : X.Opens}
    {V : Z.Opens} (hVU : V ≤ h ⁻¹ᵁ U) :
    letI : FormallyUnramified (h.resLE U V hVU) := formallyUnramified_resLE h hVU
    IsIso (universalImmersionConormalSheafMap
      (universalFirstOrderThickening (h.resLE U V hVU)) (universalFirstOrderThickening h)
      V.ι U.ι (Scheme.Hom.resLE_comp_ι h hVU))

Tag 04FB, a lemma

Tag 04FB in the Stacks Project.

Stacks.Thickenings.isIso_thickeningRelativeDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UniversalDifferentials.lean, line 573. The attribute's comment: “the restriction along the inclusion of a universal first-order thickening of the canonical map on relative differentials is an isomorphism; formal unramifiedness of h is not assumed, a universal first-order thickening being given”.

Let h : Z ⟶ X be a morphism of schemes over S and let i : Z ⟶ Z' with structure morphism h' : Z' ⟶ X be a universal first-order thickening of Z over X. The canonical map c_{h'} : (h')^* Ω_{X/S} ⟶ Ω_{Z'/S} induces an isomorphism h^* Ω_{X/S} ⟶ Ω_{Z'/S} ⊗ 𝒪_Z, namely its restriction along i.

Formal unramifiedness of h, a hypothesis of the source, is not needed here: it is what makes a universal first-order thickening exist, and one is given.

public theorem isIso_thickeningRelativeDifferentialsMap {Z X Z' S : Scheme.{u}} {h : Z ⟶ X}
    {i : Z ⟶ Z'} {h' : Z' ⟶ X} (hi : IsUniversalFirstOrderThickening h i h') (p : X ⟶ S) :
    IsIso (Scheme.Hom.thickeningRelativeDifferentialsMap i h' p)

Tag 04FC, a lemma

Tag 04FC in the Stacks Project.

Stacks.ConormalSequenceRight.epi_relativeDifferentialsMap_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/FormallyUnramified.lean, line 120. The attribute's comment: “exactness at the right term”.

[Stacks, Tag 04FC], exactness at the right term. For a formally unramified morphism h : Z ⟶ X of schemes over S, the canonical map h^*Ω_{X/S} ⟶ Ω_{Z/S} of [Stacks, Tag 01UV] is an epimorphism, so the differential sequence of h ends in zero.

A formally unramified morphism has Ω_{Z/X} = 0 by [Stacks, Tag 02G4], so this is epi_relativeDifferentialsMap_of_isZero_relativeDifferentials.

theorem epi_relativeDifferentialsMap_of_formallyUnramified (h : Z ⟶ X) [FormallyUnramified h]
    (p : X ⟶ S) :
    Epi (Scheme.Hom.relativeDifferentialsMap h p (h ≫ p) (𝟙 S) (by simp))

Stacks.ConormalSequenceRight.universalConormalDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/FormallyUnramifiedConormal.lean, line 232. The attribute's comment: “the first arrow induced by the universal derivation”.

[Stacks, Tag 04FC], the first arrow. For a formally unramified morphism h : Z ⟶ X of schemes over S, the canonical morphism 𝒞_{Z/X} ⟶ h^*Ω_{X/S} induced by the universal derivation d_{Z'/S} on the ambient scheme of the universal first-order thickening of Z over X.

It is the first arrow of [Stacks, Tag 01UZ] for the closed immersion ι : Z ⟶ Z' over h' ≫ p, whose source is the conormal sheaf of ι, that is 𝒞_{Z/X} by the definition [Stacks, Tag 04F4] makes, and whose target is moved onto h^*Ω_{X/S} by [Stacks, Tag 04FB].

noncomputable def universalConormalDifferential :
    Stacks.ConormalSequenceUnramifiedPair.conormalSheafModules h ⟶
      (Scheme.Modules.pullback h).obj (Scheme.Hom.relativeDifferentials p)

Stacks.ConormalSequenceRight.universalConormalShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/FormallyUnramifiedConormal.lean, line 284. The attribute's comment: “exactness at the middle term”. References: SGA 7 XI (1.3), “partial”.

[Stacks, Tag 04FC], exactness at the middle term. For a formally unramified morphism h : Z ⟶ X of schemes over S the sequence 𝒞_{Z/X} ⟶ h^*Ω_{X/S} ⟶ Ω_{Z/S} is exact at h^*Ω_{X/S}.

This is [Stacks, Tag 01UZ] for the closed immersion of Z into the ambient scheme of its universal first-order thickening over X, transported along the identifications of Stacks.ConormalSequenceRight.universalConormalShortComplexIso.

theorem universalConormalShortComplex_exact :
    (universalConormalShortComplex h p).Exact

Declarations registered for the tag:

AlgebraicGeometry.Scheme.Hom.relativeDifferentialsMap, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/ConormalSequenceRight/FormallyUnramified.lean, line 134 (StacksFrontier): “the second arrow”.

Tag 067V, a lemma

Tag 067V in the Stacks Project.

Stacks.ConormalSequenceUnramifiedPair.universalConormalTransitivityMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairConormalSequence.lean, line 153. The attribute's comment: “the first arrow”.

[Stacks, Tag 067V], the first arrow. For formally unramified i : Z ⟶ X and j : Z ⟶ Y in a commutative triangle i ≫ p = j, the canonical map 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of conormal sheaves in the sense of [Stacks, Tag 04F4] part (2).

It is the morphism of conormal sheaves of [Stacks, Tag 04F7] for the square whose top morphism is 𝟙 Z and whose bottom morphism is p, transported along the identification of pullback along an identity with the identity functor and along the identifications of the conormal sheaves of the two inclusions with those of their closed-immersion factorizations.

def universalConormalTransitivityMap (h : i ≫ p = j) :
    universalConormalSheaf j ⟶ universalConormalSheaf i

Stacks.ConormalSequenceUnramifiedPair.conormalSequenceSecondArrow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 448. The attribute's comment: “the second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}, built as the conormal differential of Tag 01UZ for Z ⟶ Z' over Z'' and moved along the identification thirdTermIso of the third term”.

The second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} of [Stacks, Tag 067V]. It is the conormal differential of [Stacks, Tag 01UZ] for the closed immersion Z ⟶ Z' of Z into the ambient scheme of its universal first-order thickening over X, taken over the ambient scheme Z'' of the universal first-order thickening over Y — that is, the second arrow of the sequence of [Stacks, Tag 067L] that the proof of [Stacks, Tag 067V] reduces to — with its target moved onto i^*Ω_{X/Y} by Stacks.ConormalSequenceUnramifiedPair.thirdTermIso and its source read through Stacks.ConormalSequenceUnramifiedPair.conormalSheafComparisonIso.

def conormalSequenceSecondArrow (h : i ≫ p = j) :
    conormalSheafModules i ⟶
      (Scheme.Modules.pullback i).obj (Scheme.Hom.relativeDifferentials p)

Stacks.ConormalSequenceUnramifiedPair.conormalSequenceComp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1081. The attribute's comment: “the composite of the two arrows 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} vanishes, so the two arrows form a complex”.

[Stacks, Tag 067V]: the two arrows form a complex. The composite 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} vanishes.

theorem conormalSequenceComp_eq_zero (h : i ≫ p = j) :
    conormalSequenceFirstArrow i j p h ≫ conormalSequenceSecondArrow i j p h = 0

Stacks.ConormalSequenceUnramifiedPair.epi_conormalSequenceSecondArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1093. The attribute's comment: “surjectivity of the second arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/Y}, which is the ⟶ 0 at the right-hand end of the sequence”.

[Stacks, Tag 067V]: the second arrow is an epimorphism. This is the ⟶ 0 at the right-hand end of the sequence.

theorem epi_conormalSequenceSecondArrow (h : i ≫ p = j) :
    Epi (conormalSequenceSecondArrow i j p h)

Stacks.ConormalSequenceUnramifiedPair.conormalSequenceShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1110. The attribute's comment: “exactness at the middle term 𝒞_{Z/X}: the kernel of the second arrow is the image of the first”.

[Stacks, Tag 067V]: the sequence is exact at 𝒞_{Z/X}. The kernel of the second arrow is the image of the first.

theorem conormalSequenceShortComplex_exact (h : i ≫ p = j) :
    (ShortComplex.mk _ _ (conormalSequenceComp_eq_zero i j p h)).Exact

Tag 06AE, a lemma

Tag 06AE in the Stacks Project.

Stacks.Thickenings.transitivityMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Transitivity.lean, line 81. The attribute's comment: “part (1): the morphism Z' ⟶ Y'”.

The morphism Z' ⟶ Y' of part (1) of [Stacks Project, Tag 06AE]. For a universal first-order thickening Z ⊂ Z' of Z over X and one Y ⊂ Y' of Y over X, this is the canonical morphism of [Stacks Project, Tag 04F7] for the square over X with vertical maps i and 𝟙 X.

noncomputable def transitivityMap (tZ : UniversalFirstOrderThickening (i ≫ p))
    (tY : UniversalFirstOrderThickening p) : tZ.ambient ⟶ tY.ambient

Stacks.Thickenings.isUniversal_relative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Transitivity.lean, line 149. The attribute's comment: “part (1): Y ×_{Y'} Z' is the universal first-order thickening of Z over Y”.

Part (1) of [Stacks Project, Tag 06AE]. Let Z --i--→ Y --p--→ X be morphisms of schemes, let Z ⊂ Z' be a universal first-order thickening of Z over X and Y ⊂ Y' one of Y over X. Then the fibre product Y ×_{Y'} Z' along the morphism Stacks.Thickenings.transitivityMap is a universal first-order thickening of Z over Y.

theorem isUniversal_relative :
    IsUniversalFirstOrderThickening i (relativeInclusion i p tZ tY)
      (relativeToBase i p tZ tY)

Stacks.Thickenings.transitivityConormalLeftMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 94. The attribute's comment: “part (2): the first arrow i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X}”.

The first arrow i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} of the conormal sequence of part (2) of [Stacks Project, Tag 06AE]. It is the canonical map of [Stacks Project, Tag 01R4] for the square of inclusions with vertical maps i and the morphism Z' ⟶ Y' of Stacks.Thickenings.transitivityMap.

def transitivityConormalLeftMap :
    (modulePullback i.toLRSHom.toShHom).obj
        (conormalSheaf tY.inclusion.liftCoborder.toLRSHom.toShHom) ⟶
      conormalSheaf tZ.inclusion.liftCoborder.toLRSHom.toShHom

Stacks.Thickenings.transitivityConormalRightMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 116. The attribute's comment: “part (2): the second arrow 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}”.

The second arrow 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of the conormal sequence of part (2) of [Stacks Project, Tag 06AE]. It is the canonical map of [Stacks Project, Tag 01R4] for the square of inclusions with vertical maps 𝟙 Z and the projection Y ×_{Y'} Z' ⟶ Z', read through the identification of pullback along the identity with the identity functor.

def transitivityConormalRightMap :
    conormalSheaf tZ.inclusion.liftCoborder.toLRSHom.toShHom ⟶
      conormalSheaf (relativeInclusion i p tZ tY).liftCoborder.toLRSHom.toShHom

Stacks.Thickenings.epi_transitivityConormalRightMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 129. The attribute's comment: “part (2): exactness at the right term”. References: SGA 6 VIII (2.6), “right exactness”.

Part (2) of [Stacks Project, Tag 06AE], exactness at 𝒞_{Z/Y}. The second arrow 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of the conormal sequence is an epimorphism, which is the ⟶ 0 at the right-hand end of the canonical sequence i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0.

theorem epi_transitivityConormalRightMap :
    Epi (transitivityConormalRightMap i p tZ tY)

Stacks.Thickenings.transitivityConormalLeftMap_comp_rightMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 276. The attribute's comment: “part (2): the two arrows of the sequence compose to zero”.

The two arrows of the conormal sequence of part (2) of [Stacks Project, Tag 06AE] compose to zero.

theorem transitivityConormalLeftMap_comp_rightMap :
    transitivityConormalLeftMap i p tZ tY ≫ transitivityConormalRightMap i p tZ tY = 0

Stacks.Thickenings.transitivityConormalShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 288. The attribute's comment: “part (2): the sequence as a short complex”.

The conormal sequence of part (2) of [Stacks Project, Tag 06AE] as a two-term complex of 𝒪_Z-modules, i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}.

def transitivityConormalShortComplex :
    ShortComplex (SheafOfModules.{u} (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace))

Stacks.Thickenings.transitivityConormalShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/TransitivityConormal.lean, line 614. The attribute's comment: “part (2): exactness at the middle term”. References: SGA 6 VIII (2.2), “partial”; SGA 6 VIII (2.6), “partial”.

Part (2) of [Stacks Project, Tag 06AE], exactness at 𝒞_{Z/X}. The conormal sequence i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} is exact at its middle term; with Stacks.Thickenings.epi_transitivityConormalRightMap this makes i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 exact.

theorem transitivityConormalShortComplex_exact :
    (transitivityConormalShortComplex i p tZ tY).Exact

Sources

LeanStacks.Thickenings.nonempty_universalFirstOrderThickening · Stacks.Thickenings.universalFirstOrderThickening · Stacks.Thickenings.universalConormalSheaf · Stacks.Thickenings.universalThickeningIsoFirstOrderNeighbourhood · Stacks.Thickenings.immersionConormalSheafIsoUniversalConormalSheaf · Stacks.Thickenings.formallyUnramified_of_isImmersion · Stacks.Thickenings.isUniversalFirstOrderThickening_nthOrderInclusion_one · Stacks.Thickenings.UniversalFirstOrderThickening.formallyUnramified_toBase

Section37.8 Formally étale morphisms #

Section 37.8 of the Stacks Project, Tag 02HF. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02HG, a definition

Tag 02HG in the Stacks Project.

AlgebraicGeometry.FormallyEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleScheme.lean, line 118. References: EGA IV (17.1.1); SGA 3 XI (1.1).

A morphism of schemes f : X ⟶ S is formally étale when it has the unique infinitesimal lifting property: for every first-order thickening i : T ⟶ T' of affine schemes, every commutative square
T  --g--→ X
|         |
i         f
↓         ↓
T' --p--→ S
has exactly one diagonal filler h : T' ⟶ X, that is exactly one morphism with i ≫ h = g and h ≫ f = p.

abbrev FormallyEtale {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 04FD, a lemma

Tag 04FD in the Stacks Project.

AlgebraicGeometry.FormallyEtale.existsUnique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallyEtale/Lifting.lean, line 78.

A formally étale morphism admits a unique lift across any first-order thickening of schemes over its base, without affineness assumptions.

theorem FormallyEtale.existsUnique_lift
    {X S T T' : Scheme.{u}} (f : X ⟶ S) (hf : FormallyEtale f)
    (i : T ⟶ T') (hi : IsFirstOrderThickening i)
    (p : T' ⟶ S) (g : T ⟶ X) (hg : g ≫ f = i ≫ p) :
    ∃! h : T' ⟶ X, i ≫ h = g ∧ h ≫ f = p

Tag 02HI, a lemma

Tag 02HI in the Stacks Project.

AlgebraicGeometry.FormallyEtale.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallyEtale/Basic.lean, line 51.

A composition of formally étale morphisms is formally étale.

theorem FormallyEtale.comp {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    (hf : FormallyEtale f) (hg : FormallyEtale g) :
    FormallyEtale (f ≫ g)

Tag 02HJ, a lemma

Tag 02HJ in the Stacks Project.

AlgebraicGeometry.FormallyEtale.pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallyEtale/Basic.lean, line 63.

A base change of a formally étale morphism is formally étale.

theorem FormallyEtale.pullback_snd {X S S' : Scheme.{u}}
    (f : X ⟶ S) (g : S' ⟶ S) (hf : FormallyEtale f) :
    FormallyEtale (pullback.snd f g)

Tag 02HK, a lemma

Tag 02HK in the Stacks Project.

AlgebraicGeometry.FormallyEtale.resLE, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallyEtale/Basic.lean, line 85.

Formal étaleness is preserved when a morphism is restricted to compatible open subschemes of its source and target.

lemma FormallyEtale.resLE {X S : Scheme.{u}} (f : X ⟶ S)
    (U : X.Opens) (V : S.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
    (hf : FormallyEtale f) :
    FormallyEtale (f.resLE V U hUV)

Tag 04FE, a lemma

Tag 04FE in the Stacks Project.

AlgebraicGeometry.formallyEtale_iff_isIso_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleConormal.lean, line 95. The attribute's comment: “equivalence of (1) and (2)”.

Stacks Project, Tag 04FE, equivalence of (1) and (2). A morphism of schemes is formally étale if and only if it is formally unramified and the inclusion of its source into its universal first-order thickening is an isomorphism, that is, the universal first-order thickening of X over S is X itself.

Formal unramifiedness is part of the right-hand side because the universal first-order thickening is only defined under it; for a formally étale morphism it comes from [Stacks Project, Tag 02HH].

Forwards, the unique lifting property of [Stacks Project, Tag 04FD] applied to the thickening itself produces a retraction of the inclusion, and the universal property of the thickening identifies the other composite with the identity. Backwards, a lifting problem for f is transported along the isomorphism and solved by the universal property, uniquely because the universal property's lift is unique.

public theorem formallyEtale_iff_isIso_inclusion (f : X ⟶ S) :
    FormallyEtale f ↔
      ∃ hf : FormallyUnramified f,
        letI : FormallyUnramified f := hf
        IsIso (universalFirstOrderThickening f).inclusion

AlgebraicGeometry.formallyEtale_iff_isZero_universalConormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleConormal.lean, line 159. The attribute's comment: “equivalence of (1) and (3)”.

Stacks Project, Tag 04FE, equivalence of (1) and (3). A morphism of schemes is formally étale if and only if it is formally unramified and its conormal sheaf 𝒞_{X/S} vanishes.

This is the equivalence of (1) and (2) combined with AlgebraicGeometry.isIso_inclusion_iff_isZero_universalConormalSheaf.

public theorem formallyEtale_iff_isZero_universalConormalSheaf (f : X ⟶ S) :
    FormallyEtale f ↔
      ∃ hf : FormallyUnramified f,
        letI : FormallyUnramified f := hf
        IsZero (universalConormalSheaf f)

AlgebraicGeometry.formallyEtale_iff_isZero_relativeDifferentials_and_universalConormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleConormal.lean, line 176. The attribute's comment: “equivalence of (1) and (4)”.

Stacks Project, Tag 04FE, equivalence of (1) and (4). A morphism of schemes is formally étale if and only if both its sheaf of relative differentials Ω_{X/S} and its conormal sheaf 𝒞_{X/S} vanish.

The formal unramifiedness needed to form the conormal sheaf is supplied by the vanishing of the differentials, through [Stacks Project, Tag 02H9].

public theorem formallyEtale_iff_isZero_relativeDifferentials_and_universalConormalSheaf
    (f : X ⟶ S) :
    FormallyEtale f ↔
      ∃ hΩ : IsZero (Scheme.Hom.relativeDifferentials f),
        letI : FormallyUnramified f :=
          (Scheme.Hom.formallyUnramified_iff_isZero_relativeDifferentials f).mpr hΩ
        IsZero (universalConormalSheaf f)

Tag 04FF, a lemma

Tag 04FF in the Stacks Project.

AlgebraicGeometry.formallyEtale_of_unramified_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleScheme.lean, line 214.

An unramified flat morphism of schemes is formally étale. Existence of the filler is local on the thickening by AlgebraicGeometry.exists_isAffineOpen_lift_of_unramified_flat; the local fillers agree on overlaps by Stacks.Smooth.lift_unique applied to the restricted thickening, so they glue by Stacks.Smooth.exists_lift_of_isOpenCover; and that same uniqueness is the ∃!.

theorem formallyEtale_of_unramified_flat {X S : Scheme.{u}} (f : X ⟶ S) [Unramified f] [Flat f] :
    FormallyEtale f

Tag 02HL, a lemma

Tag 02HL in the Stacks Project.

AlgebraicGeometry.formallyEtale_iff_globalSectionsMap_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleAffine.lean, line 38.

A morphism of affine schemes is formally étale if and only if its pullback map on global functions is a formally étale ring map.

theorem formallyEtale_iff_globalSectionsMap_formallyEtale
    {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S) :
    FormallyEtale f ↔ (Scheme.Γ.map f.op).hom.FormallyEtale

Tag 02HM, a lemma

Tag 02HM in the Stacks Project.

AlgebraicGeometry.etale_iff_locallyOfFinitePresentation_and_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/EtaleIffFormallyEtale.lean, line 46. References: EGA IV (17.3.2), “(ii) etale”; EGA IV (17.6.1), “a) <=> d)”; EGA IV (17.3.1); SGA 3 XI (1.6), “étale case”; SGA 4 VII (1.1), “functorial criterion”; SGA 3 XI (1.1); SGA 4½ Arcata (2.1.1), “more general”.

A morphism of schemes is étale exactly when it is locally of finite presentation and formally étale.

theorem etale_iff_locallyOfFinitePresentation_and_formallyEtale
    {X S : Scheme.{u}} (f : X ⟶ S) :
    Etale f ↔ (LocallyOfFinitePresentation f ∧ FormallyEtale f)

Sources

LeanAlgebraicGeometry.FormallyEtale · AlgebraicGeometry.FormallyEtale.existsUnique_lift · AlgebraicGeometry.FormallyEtale.comp · AlgebraicGeometry.FormallyEtale.pullback_snd · AlgebraicGeometry.FormallyEtale.resLE · AlgebraicGeometry.formallyEtale_iff_isIso_inclusion · AlgebraicGeometry.formallyEtale_iff_isZero_universalConormalSheaf · AlgebraicGeometry.formallyEtale_iff_isZero_relativeDifferentials_and_universalConormalSheaf

Section37.9 Infinitesimal deformations of maps #

Section 37.9 of the Stacks Project, Tag 04BU. 13 tags here are carried by 44 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04FG, a lemma

Tag 04FG in the Stacks Project.

Stacks.Thickenings.mapDifferenceDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivation.lean, line 307. The attribute's comment: “affine case”.

The difference of two infinitesimal deformations of a map is a derivation, affine case of [Stacks Project, Tag 04FG]. Let i : X ⟶ X' and j : Y ⟶ Y' be first-order thickenings with X' and Y' affine, let p : X' ⟶ S and q : Y' ⟶ S make them thickenings over S, and let (a, a') and (a, b') be two morphisms of thickenings over S with the same reduction a — hypothesis (1) of the source. Assume the two induced maps of conormal modules agree — hypothesis (2). Then the difference of the two comorphisms descends to a Γ(S, ⊤)-derivation of Γ(Y, ⊤) with values in the conormal module of i.

The conormal module carries two module structures here: over Γ(Y, ⊤) along a, and over Γ(S, ⊤) along the structure morphism i ≫ p of X over S.

noncomputable def mapDifferenceDerivation [IsAffine X'] [IsAffine Y']
    (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j)
    (ha' : a' ≫ q = p) (hb' : b' ≫ q = p)
    (hC : conormalMap hi hj comm_a = conormalMap hi hj comm_b) :
    letI := appTopAlgebra (j ≫ q)
    letI := conormalModuleAlong hi a
    letI := conormalModuleAlong hi (i ≫ p)
    Derivation Γ(S, (⊤ : S.Opens)) Γ(Y, (⊤ : Y.Opens)) (RingHom.ker i.appTop.hom)

Stacks.Thickenings.mapDifferenceDerivation_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivation.lean, line 351. The attribute's comment: “affine case”.

The factorization of [Stacks Project, Tag 04FG], affine case. The difference of the two comorphisms a'.appTop and b'.appTop on Γ(Y', ⊤) is the composite
Γ(Y', ⊤) --j.appTop--> Γ(Y, ⊤) --D--> RingHom.ker i.appTop.hom ⊆ Γ(X', ⊤)
where D is the Γ(S, ⊤)-derivation Stacks.Thickenings.mapDifferenceDerivation.

theorem mapDifferenceDerivation_appTop [IsAffine X'] [IsAffine Y']
    (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j)
    (ha' : a' ≫ q = p) (hb' : b' ≫ q = p)
    (hC : conormalMap hi hj comm_a = conormalMap hi hj comm_b)
    (x : Γ(Y', (⊤ : Y'.Opens))) :
    letI := appTopAlgebra (j ≫ q)
    letI := conormalModuleAlong hi a
    letI := conormalModuleAlong hi (i ≫ p)
    ((mapDifferenceDerivation hi hj comm_a comm_b ha' hb' hC (j.appTop.hom x) :
        RingHom.ker i.appTop.hom) : Γ(X', (⊤ : X'.Opens)))
      = a'.appTop.hom x - b'.appTop.hom x

Stacks.Thickenings.mapDifferenceSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 474. The attribute's comment: “the derivation D”.

The derivation D of [Stacks Project, Tag 04FG]. For an open V of Y' this is the map Γ(Y, j ⁻¹ᵁ V) → Γ(X', a' ⁻¹ᵁ V), that is 𝒪_Y ⟶ a_*𝒞_{X/X'} on sections over V, through which (a')^♯ - (b')^♯ factors. It is characterised by Stacks.Thickenings.mapDifferenceSheaf_spec.

noncomputable def mapDifferenceSheaf (hi : IsFirstOrderThickening i)
    (hj : IsFirstOrderThickening j) (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j)
    (hC : AgreeOnIdeal j a' b') (V : Y'.Opens) (s : Γ(Y, j ⁻¹ᵁ V)) : Γ(X', a' ⁻¹ᵁ V)

Stacks.Thickenings.mapDifferenceSheaf_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 520. The attribute's comment: “the factorization”.

The factorization of [Stacks Project, Tag 04FG]. The difference of the two comorphisms on Γ(Y', V) is the composite of j^♯ : 𝒪_{Y'} ⟶ 𝒪_Y with the derivation D.

theorem mapDifferenceSheaf_app (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j) (hC : AgreeOnIdeal j a' b')
    (V : Y'.Opens) (x : Γ(Y', V)) :
    mapDifferenceSheaf hi hj comm_a comm_b hC V ((j.app V).hom x)
      = mapDifferenceLE (le_refl (a' ⁻¹ᵁ V)) (preimage_le_preimage hi comm_a comm_b V) x

Stacks.Thickenings.app_mapDifferenceSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 535. The attribute's comment: “the factorization passes through the conormal sheaf”.

The derivation takes values in the conormal sheaf. The value of D is killed by the comorphism of i, i.e. it is a section of the defining ideal of X ⊂ X', which for a first-order thickening is 𝒞_{X/X'}. This is what makes the factorization of Stacks.Thickenings.mapDifferenceSheaf_app pass through a_*𝒞_{X/X'} and not merely through a_*𝒪_{X'}.

theorem app_mapDifferenceSheaf (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j) (hC : AgreeOnIdeal j a' b')
    (V : Y'.Opens) (s : Γ(Y, j ⁻¹ᵁ V)) :
    (i.app (a' ⁻¹ᵁ V)).hom (mapDifferenceSheaf hi hj comm_a comm_b hC V s) = 0

Stacks.Thickenings.mapDifferenceSheaf_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 554. The attribute's comment: “D is a map of sheaves”.

D is a map of sheaves: it commutes with restriction.

theorem mapDifferenceSheaf_map (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j) (hC : AgreeOnIdeal j a' b')
    {V V' : Y'.Opens} (hV : V' ≤ V) (s : Γ(Y, j ⁻¹ᵁ V)) :
    resOpen (a'.preimage_mono hV) (mapDifferenceSheaf hi hj comm_a comm_b hC V s)
      = mapDifferenceSheaf hi hj comm_a comm_b hC V' (resOpen (j.preimage_mono hV) s)

Stacks.Thickenings.mapDifferenceSheaf_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 566. The attribute's comment: “D is additive”.

D is additive.

theorem mapDifferenceSheaf_add (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j) (hC : AgreeOnIdeal j a' b')
    (V : Y'.Opens) (s t : Γ(Y, j ⁻¹ᵁ V)) :
    mapDifferenceSheaf hi hj comm_a comm_b hC V (s + t)
      = mapDifferenceSheaf hi hj comm_a comm_b hC V s
        + mapDifferenceSheaf hi hj comm_a comm_b hC V t

Stacks.Thickenings.mapDifferenceSheaf_appLE_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 587. The attribute's comment: “D is 𝒪_S-linear”.

D kills the sections pulled back from the base. This is 𝒪_S-linearity: a section of 𝒪_S over an open Z of S pulls back to a section of 𝒪_Y over j ⁻¹ᵁ V for V ≤ q ⁻¹ᵁ Z, and D vanishes on it, because the two lifts a' and b' are morphisms over S and therefore agree on sections coming from S.

theorem mapDifferenceSheaf_appLE_base (hi : IsFirstOrderThickening i)
    (hj : IsFirstOrderThickening j) (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j)
    (hC : AgreeOnIdeal j a' b') (ha' : a' ≫ q = p) (hb' : b' ≫ q = p) {Z : S.Opens}
    {V : Y'.Opens} (hV : V ≤ q ⁻¹ᵁ Z) (hjV : j ⁻¹ᵁ V ≤ (j ≫ q) ⁻¹ᵁ Z) (r : Γ(S, Z)) :
    mapDifferenceSheaf hi hj comm_a comm_b hC V
        (((j ≫ q).appLE Z (j ⁻¹ᵁ V) hjV).hom r) = 0

Stacks.Thickenings.mapDifferenceSheaf_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationGlobal.lean, line 688. The attribute's comment: “the Leibniz rule for D”.

The Leibniz rule for D. This is the last clause of [Stacks Project, Tag 04FG]: together with Stacks.Thickenings.mapDifferenceSheaf_add and Stacks.Thickenings.mapDifferenceSheaf_appLE_base it says that D is an 𝒪_S-derivation of 𝒪_Y with values in a_*𝒞_{X/X'}.

The proof is the computation of the affine case, read on an affine open of Y' after lifting the two sections: the difference of the two comorphisms on a product is Δ(u)·(a')^♯ v + (b')^♯ u·Δ(v), and this agrees with (a')^♯ u·Δ(v) + (a')^♯ v·Δ(u) because the two differences lie in the defining ideal of i, whose square vanishes.

theorem mapDifferenceSheaf_mul (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (comm_a : i ≫ a' = a ≫ j) (comm_b : i ≫ b' = a ≫ j) (hC : AgreeOnIdeal j a' b')
    (V : Y'.Opens) (s t : Γ(Y, j ⁻¹ᵁ V)) :
    mapDifferenceSheaf hi hj comm_a comm_b hC V (s * t)
      = conormalSmul hi hj comm_a V (mapDifferenceSheaf hi hj comm_a comm_b hC V t)
            (app_mapDifferenceSheaf hi hj comm_a comm_b hC V t) s
        + conormalSmul hi hj comm_a V (mapDifferenceSheaf hi hj comm_a comm_b hC V s)
            (app_mapDifferenceSheaf hi hj comm_a comm_b hC V s) t

Stacks.Thickenings.differenceDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationSheaf.lean, line 739. The attribute's comment: “the derivation D, for arbitrary X' and Y'”.

The 𝒪_S-derivation D : 𝒪_Y ⟶ a_*𝒞_{X/X'} of [Stacks Project, Tag 04FG], at sheaf level. Let i : X ⟶ X' be a first-order thickening, let j : Y ⟶ Y' be an immersion with structure morphism q : Y' ⟶ S, and let (a, a') and (a, b') be two morphisms of thickenings over S with the same reduction a — hypothesis (1) of the source — whose two induced maps a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} of [Stacks Project, Tag 01R4] agree — hypothesis (2). Then the difference (a')^♯ - (b')^♯ factors through this derivation; the factorization is Stacks.Thickenings.firstOrderImmersionConormalSheafι_differenceDerivation_d.

It is Stacks.Thickenings.differenceDerivationHom composed with the universal relative derivation of Y over S, so that it is an 𝒪_S-derivation by construction.

def differenceDerivation (hi : i.ker ^ 2 = ⊥) (hq : b' ≫ q = a' ≫ q) (ca : i ≫ a' = a ≫ j)
    (cb : i ≫ b' = a ≫ j)
    (hC : Stacks.Immersion.immersionConormalSheafMap i j a a'
        (Stacks.Immersion.toShHom_square ca) =
      Stacks.Immersion.immersionConormalSheafMap i j a b'
        (Stacks.Immersion.toShHom_square cb)) :
    SheafOfModules.SheafDerivation (inverseImageStructureMap (j ≫ q))
      ((Scheme.Modules.pushforward a).obj (Stacks.Conormal.conormalSheaf i))

Stacks.Thickenings.firstOrderImmersionConormalSheafι_differenceDerivation_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDerivationSheaf.lean, line 794. The attribute's comment: “the factorization, for arbitrary X' and Y'”.

The factorization of [Stacks Project, Tag 04FG], at sheaf level. The difference (a')^♯ s - (b')^♯ s of the two comorphisms, on a section s of 𝒪_{Y'} over V and read over the open (b')⁻¹V ⊓ (a')⁻¹V of X' where both are defined, is the image of D (j^♯ s) under the inclusion 𝒞_{X/X'} ⟶ 𝒪_{X'} of the conormal sheaf of the first-order thickening i.

That is the composite 𝒪_{Y'} ⟶ 𝒪_Y --D--> a_*𝒞_{X/X'} ⟶ a_*𝒪_{X'} of the source.

theorem firstOrderImmersionConormalSheafι_differenceDerivation_d (hi : i.ker ^ 2 = ⊥)
    (hq : b' ≫ q = a' ≫ q) (ca : i ≫ a' = a ≫ j) (cb : i ≫ b' = a ≫ j)
    (hC : Stacks.Immersion.immersionConormalSheafMap i j a a'
        (Stacks.Immersion.toShHom_square ca) =
      Stacks.Immersion.immersionConormalSheafMap i j a b'
        (Stacks.Immersion.toShHom_square cb))
    (V : Y'.Opens) (s : Γ(Y', V)) :
    (Stacks.Thickenings.firstOrderImmersionConormalSheafι i hi).val.app
        (op (liftPairOpen a' b' V))
        ((Stacks.Conormal.conormalSheaf i).val.map
          (homOfLE (preimage_liftPairOpen ca cb V).le).op
          ((differenceDerivation q hi hq ca cb hC).d (X := op (j ⁻¹ᵁ V))
            ((j.app V).hom s))) =
      (a'.appLE V (liftPairOpen a' b' V) inf_le_right).hom s -
        (b'.appLE V (liftPairOpen a' b' V) inf_le_left).hom s

Tag 04BV, an equation

Tag 04BV in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.derivationDirectImageEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DerivationsIntoDirectImage.lean, line 73. The attribute's comment: “the bijection θ ↔ D = d_{Y/S} ∘ θ at scheme level on the Zariski site, stated at a general target module”.

Equation (04BV). For a : X ⟶ Y, b : Y ⟶ Z morphisms of schemes and an 𝒪_X-module C, the 𝒪_X-linear maps θ : a^*Ω_{Y/Z} ⟶ C correspond bijectively to the Z-derivations D : 𝒪_Y ⟶ a_*C, by D = d_{Y/Z} ∘ θ with θ transposed along the adjunction a^* ⊣ a_*.

def derivationDirectImageEquiv (a : X ⟶ Y) (b : Y ⟶ Z) (C : X.Modules) :
    ((Scheme.Modules.pullback a).obj (relativeDifferentials b) ⟶ C) ≃
      SheafOfModules.SheafDerivation (inverseImageStructureMap b)
        ((Scheme.Modules.pushforward a).obj C)

AlgebraicGeometry.Scheme.Hom.derivationDirectImageEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/DerivationsIntoDirectImage.lean, line 84. The attribute's comment: “the equation D = d_{Y/S} ∘ θ at scheme level on the Zariski site”.

Equation (04BV) itself. The derivation attached to θ : a^*Ω_{Y/Z} ⟶ C is the universal derivation d_{Y/Z} followed by the transpose of θ along a^* ⊣ a_*.

theorem derivationDirectImageEquiv_apply (a : X ⟶ Y) (b : Y ⟶ Z) (C : X.Modules)
    (θ : (Scheme.Modules.pullback a).obj (relativeDifferentials b) ⟶ C) :
    derivationDirectImageEquiv a b C θ =
      (universalRelativeDerivation b).postcomp
        (((Scheme.Modules.pullbackPushforwardAdjunction a).homEquiv
          (relativeDifferentials b) C) θ).val

AlgebraicGeometry.SheafOfModules.universalDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials.lean, line 130. The attribute's comment: “the factorization D = d o theta of a derivation through the universal derivation”. References: EGA IV (16.5.3), “(ii)”.

Stacks Project, Tag 08RM. Postcomposition with the universal derivation gives the unique morphism from the module of relative differentials to any coefficient sheaf.

theorem universalDerivation_isUniversal {X : TopCat.{u}}
    {O₁ O₂ : TopCat.Sheaf CommRingCat.{max u v} X} (φ : O₁ ⟶ O₂) :
    IsUniversal.{u, v, u_1} (universalDerivation.{u, v, u_1} φ)

Tag 02H5, a lemma

Tag 02H5 in the Stacks Project.

Stacks.Thickenings.existsUnique_derivationActionGlobal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDerivationActionGlobal.lean, line 714. References: SGA 3 III (4.9), “Perturbation clause”.

A derivation acts in exactly one way on a lift of a map, [Stacks Project, Tag 02H5]. Let S be a scheme, let i : X ⟶ X' and j : Y ⟶ Y' be first-order thickenings, let p : X' ⟶ S and q : Y' ⟶ S be the structure morphisms, and let (a, a') be a morphism of thickenings (X ⊂ X') ⟶ (Y ⊂ Y') over S. Then for every 𝒪_X-linear map θ : a^*Ω_{Y/S} ⟶ 𝒞_{X/X'} there is exactly one morphism b' : X' ⟶ Y' such that (a, b') is again a morphism of thickenings over S — conditions (1) and (2) of [Stacks Project, Tag 04FG] for the pair (a', b') — and the derivation D of [Stacks Project, Tag 04FG] attached to the pair is related to θ by Equation [Stacks Project, Tag 04BV], D = θ ∘ d_{Y/S}.

Nothing is affine, and the datum is the one of the source: a morphism of sheaves of 𝒪_X-modules out of the pulled-back sheaf of relative differentials.

Tag 04FG numbers two conditions; with Equation 04BV they make the three requirements written out on sections below. Condition (1), that the two reductions agree, is comm_b : i ≫ b' = a ≫ j, the same a as for a'; that b' is a morphism over S is b' ≫ q = p. Condition (2), that the two induced maps a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} of [Stacks Project, Tag 01R4] agree, is the first conjunct: for a first-order thickening j the conormal sheaf 𝒞_{Y/Y'} is the defining ideal of j and the induced map is the comorphism, so the condition says that (a')^♯ and (b')^♯ agree on the sections killed by j^♯. Equation [Stacks Project, Tag 04BV] is the second conjunct: the difference (b')^♯ - (a')^♯, which is the derivation D of [Stacks Project, Tag 04FG] read through the inclusion 𝒞_{X/X'} ⟶ 𝒪_{X'} of Stacks.Thickenings.firstOrderImmersionConormalSheafι, is θ applied to the pulled-back universal differential Stacks.Smooth.pullbackD.

Because d_{Y/S} kills j^♯ of a section of the defining ideal of j, the second conjunct implies the first, so the morphism characterised here is the same whether condition (2) is read as above or as the equality of the two maps of conormal sheaves. For the same reason j need only be a morphism of schemes: the source asks it to be a first-order thickening, and at that hypothesis the first conjunct is exactly its condition (2), since 𝒞_{Y/Y'} is then the defining ideal of j and the map of [Stacks Project, Tag 01R4] is the comorphism.

theorem existsUnique_derivationActionGlobal (ha' : a' ≫ q = p) :
    ∃! b' : X' ⟶ Y', ∃ (comm_b : i ≫ b' = a ≫ j) (_ : b' ≫ q = p),
      (∀ (W : Y'.Opens) (V : X'.Opens) (hA : V ≤ a' ⁻¹ᵁ W) (g : Γ(Y', W)),
          (j.app W).hom g = 0 →
            (b'.appLE W V (le_preimage_of_comm hsq comm_a comm_b hA)).hom g
              = (a'.appLE W V hA).hom g)
        ∧ ∀ (W : Y'.Opens) (V : X'.Opens) (hA : V ≤ a' ⁻¹ᵁ W) (g : Γ(Y', W)),
            (b'.appLE W V (le_preimage_of_comm hsq comm_a comm_b hA)).hom g
              = (a'.appLE W V hA).hom g
                + derivationSection hsq θ W V (preimage_le_of_comm comm_a hA) g

Tag 0CK1, a remark

Tag 0CK1 in the Stacks Project.

Stacks.Thickenings.differenceDerivation_derivationActionSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDerivationActionDifference.lean, line 413.

[Stacks Project, Tag 0CK1], for arbitrary schemes. Let S be a scheme, let i : X ⟶ X' be a first-order thickening, let j : Y ⟶ Y' be an immersion with structure morphism q : Y' ⟶ S, let (a, a') be a morphism of thickenings (X ⊂ X') ⟶ (Y ⊂ Y') over S, and let θ : a^*Ω_{Y/S} ⟶ 𝒞_{X/X'} be an 𝒪_X-linear map. The source writes θ ⬝ a' for the lift [Stacks Project, Tag 02H5] attaches to θ, which is Stacks.Thickenings.derivationActionSheaf, and says that this notation means nothing else than the following two things.

The derivation D of [Stacks Project, Tag 04FG] attached to the pair (a', θ ⬝ a') — the 𝒪_S-derivation 𝒪_Y ⟶ a_*𝒞_{X/X'} of Stacks.Thickenings.derivationActionDifferenceDerivation — is related to θ by Equation [Stacks Project, Tag 04BV]: it is d_{Y/S} followed by θ, read through the transpose of θ along a^* ⊣ a_*. That is the first conjunct.

The comorphisms (a')^♯ and (θ ⬝ a')^♯ differ by D: on a section s of 𝒪_{Y'} over an open V, (θ ⬝ a')^♯ s = (a')^♯ s + D (j^♯ s), the value of D being read inside 𝒪_{X'} through the inclusion 𝒞_{X/X'} ⟶ 𝒪_{X'} by Stacks.Thickenings.conormalSectionι. That is the second conjunct.

Nothing is affine, and the datum is the one of the source: a morphism of sheaves of 𝒪_X-modules out of the pulled-back sheaf of relative differentials. The derivation is the one [Stacks Project, Tag 04FG] attaches to the pair, with all three of that tag's hypotheses discharged for it — in particular condition (2), which is Stacks.Thickenings.immersionConormalSheafMap_derivationActionSheaf.

theorem differenceDerivation_derivationActionSheaf :
    derivationActionDifferenceDerivation hi q ca θ =
        (Scheme.Hom.universalRelativeDerivation (j ≫ q)).postcomp
          ((Scheme.Modules.pullbackPushforwardAdjunction a).homEquiv
            (Scheme.Hom.relativeDifferentials (j ≫ q))
            (Stacks.Conormal.conormalSheaf i) θ).val ∧
      ∀ (V : Y'.Opens) (s : Γ(Y', V)),
        ((derivationActionSheaf hi q ca θ).app V).hom s =
          (a'.app V).hom s +
            conormalSectionι hi ca V
              ((derivationActionDifferenceDerivation hi q ca θ).d (X := op (j ⁻¹ᵁ V))
                ((j.app V).hom s))

Tag 04FH, a lemma

Tag 04FH in the Stacks Project.

Stacks.Thickenings.isSheaf_compatibleLiftsPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationGluing.lean, line 320.

[Stacks Project, Tag 04FH]. For a scheme S, immersions i : X ⟶ X' and j : Y ⟶ Y', a morphism a : X ⟶ Y and a map A : a^* 𝒞_{Y/Y'} ⟶ 𝒞_{X/X'}, the rule assigning to an open V of X' the set of morphisms V ⟶ Y' over S restricting to a on i⁻¹V and inducing the restriction of A there is a sheaf of sets on X'.

The proof is the unique-gluing form of the sheaf condition. A compatible family of lifts glues to a morphism by Stacks.Thickenings.glueCompatibleLifts, that morphism is again a compatible lift by Stacks.Thickenings.isCompatibleLift_glueCompatibleLifts, and a lift over the union is determined by its restrictions to the cover.

theorem isSheaf_compatibleLiftsPresheaf (pX' : X' ⟶ S) (pY' : Y' ⟶ S) (a : X ⟶ Y)
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) :
    (compatibleLiftsPresheaf pX' pY' a A).IsSheaf

Stacks.Thickenings.IsCompatibleLift.restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationSheaf.lean, line 232. The attribute's comment: “the restriction maps”.

The three conditions of [Stacks Project, Tag 04FI] are stable under restriction. A lift of a over an open V of X' compatible with A restricts to a compatible lift over any smaller open V'.

theorem IsCompatibleLift.restrict (hb : IsCompatibleLift pX' pY' a A V b)
    {V' : X'.Opens} (hV : V' ≤ V) :
    IsCompatibleLift pX' pY' a A V' (X'.homOfLE hV ≫ b)

Stacks.Thickenings.compatibleLiftsPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationSheaf.lean, line 258. The attribute's comment: “the restriction maps”.

The presheaf of compatible lifts. The rule assigning to an open V of X' the set of morphisms V ⟶ Y' over S restricting to a on i⁻¹V and inducing the restriction of A there, with the restriction maps of Stacks.Thickenings.compatibleLiftsRestrict.

def compatibleLiftsPresheaf (pX' : X' ⟶ S) (pY' : Y' ⟶ S) (a : X ⟶ Y)
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) :
    TopCat.Presheaf (Type u) X'.carrier

Tag 04FI, an equation

Tag 04FI in the Stacks Project.

Stacks.Thickenings.firstOrderCompatibleLifts, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationMaps.lean, line 129.

The set of compatible lifts for first-order thickenings. The set Stacks.Thickenings.compatibleLifts when i and j are first-order thickenings in the sense of [Stacks Project, Tag 04EX].

abbrev firstOrderCompatibleLifts (hi : IsFirstOrderThickening i)
    (hj : IsFirstOrderThickening j) (pX' : X' ⟶ S) (pY' : Y' ⟶ S) (a : X ⟶ Y)
    (A : letI := hi.1; letI := hj.1;
      (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
        immersionConormalSheaf i)
    (V : X'.Opens) : Type u

Tag 04FJ, a lemma

Tag 04FJ in the Stacks Project.

Stacks.Thickenings.exists_addAction_compatibleLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationSheafHomAction.lean, line 856. The attribute's comment: “the action of SheafHom(a^*Ω, 𝒞) on the sheaf of Tag 04FI, for arbitrary schemes”.

The sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) acts on the sheaf of [Stacks Project, Tag 04FI], [Stacks Project, Tag 04FJ] for arbitrary schemes.

Let S be a scheme, let i : X ⟶ X' be a first-order thickening, let j : Y ⟶ Y' be an immersion, let p : X' ⟶ S and q : Y' ⟶ S be the structure morphisms, let a : X ⟶ Y and let A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} be a map of 𝒪_X-modules. For every open V of X' the additive group of sections of SheafHom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) over the part i⁻¹V of X cut out by V acts on the set Stacks.Thickenings.compatibleLifts of [Stacks Project, Tag 04FI] of lifts of a over V inducing A, and the action commutes with the restriction maps of the sheaf Stacks.Thickenings.compatibleLiftsPresheaf of [Stacks Project, Tag 04FH]: it is an action of sheaves.

Nothing is affine, the datum is the one of the source — a morphism of sheaves of 𝒪_X-modules out of the pulled-back sheaf of relative differentials, read over an open — and the third condition of [Stacks Project, Tag 04FI] is the equality of maps of conormal sheaves.

The action is Stacks.Thickenings.compatibleLiftsVAdd, the group laws are Stacks.Thickenings.homSectionAct_zero and Stacks.Thickenings.homSectionAct_add, and the compatibility with restriction is Stacks.Thickenings.compatibleLiftsRestrict_compatibleLiftsVAdd.

theorem exists_addAction_compatibleLifts (hsq : i.ker ^ 2 = ⊥) (pX' : X' ⟶ S) (pY' : Y' ⟶ S)
    (a : X ⟶ Y)
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) :
    ∃ act : ∀ V : X'.Opens, deformationHomSections i a (j ≫ pY') V →
        compatibleLifts pX' pY' a A V → compatibleLifts pX' pY' a A V,
      (∀ (V : X'.Opens) (c : compatibleLifts pX' pY' a A V), act V 0 c = c) ∧
        (∀ (V : X'.Opens) (θ η : deformationHomSections i a (j ≫ pY') V)
          (c : compatibleLifts pX' pY' a A V), act V (θ + η) c = act V θ (act V η c)) ∧
        ∀ (V V' : X'.Opens) (hV : V' ≤ V) (θ : deformationHomSections i a (j ≫ pY') V)
          (c : compatibleLifts pX' pY' a A V),
          compatibleLiftsRestrict pX' pY' a A hV (act V θ c)
            = act V' (moduleHomSections.restrict (i.preimage_mono hV) θ)
                (compatibleLiftsRestrict pX' pY' a A hV c)

Stacks.Thickenings.existsUnique_compatibleLiftsVAdd_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationSheafHomTransitivity.lean, line 636. The attribute's comment: “simple transitivity over an open carrying a lift, for arbitrary schemes”. References: EGA IV (16.5.14), “more general”.

[Stacks Project, Tag 04FJ], the transitivity clause, for arbitrary schemes. Let S be a scheme, let i : X ⟶ X' be a first-order thickening, let j : Y ⟶ Y' be an immersion, let a : X ⟶ Y be a morphism and let A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} be a map of 𝒪_X-modules. Over an open V of X' carrying a lift, the action of SheafHom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) of Stacks.Thickenings.compatibleLiftsVAdd on the lifts of [Stacks Project, Tag 04FI] is simply transitive: for any two lifts b₀, c₀ over V there is exactly one section carrying b₀ to c₀.

No affineness is assumed, of S, X', Y' or V.

Existence is the unrestricted [Stacks Project, Tag 04FG] read for the restricted thickening i ∣_ V and transported to the deformation sheaf's conormal track (Stacks.Thickenings.exists_isDerivationAction_over), followed by the uniqueness half of [Stacks Project, Tag 02H5] (Stacks.Thickenings.eq_of_isDerivationAction) identifying the lift it produces with θ ⬝ b₀ (Stacks.Thickenings.homSectionAct_eq_derivationActionSheaf). Uniqueness of the section is Stacks.Thickenings.deformationHomSections_ext.

theorem existsUnique_compatibleLiftsVAdd_eq (hsq : i.ker ^ 2 = ⊥) (pX' : X' ⟶ S) (pY' : Y' ⟶ S)
    (a : X ⟶ Y)
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) (V : X'.Opens) (b₀ c₀ : compatibleLifts pX' pY' a A V) :
    ∃! θ : deformationHomSections i a (j ≫ pY') V,
      compatibleLiftsVAdd hsq pX' pY' a A V θ b₀ = c₀

Stacks.Thickenings.deformationAddAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDerivationAction.lean, line 719. The attribute's comment: “the action on the deformations with a fixed conormal map, over affine schemes”.

The action of [Stacks Project, Tag 04FJ], affine case. The additive group of Γ(Y, ⊤)-linear maps Ω[Γ(Y, ⊤)⁄Γ(S, ⊤)] ⟶ 𝒞_{X/X'} — the sections over the affine X' of SheafHom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) — acts on the deformations of a with conormal map A, by Stacks.Thickenings.Deformation.act.

noncomputable def deformationAddAction [IsAffine S] [IsAffine X'] [IsAffine Y']
    (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j) (p : X' ⟶ S) (q : Y' ⟶ S)
    (a : X ⟶ Y)
    (A : letI := Smooth.thickeningKerModule hj
      letI := conormalModuleAlong hi a
      RingHom.ker j.appTop.hom →ₗ[Γ(Y, (⊤ : Y.Opens))] RingHom.ker i.appTop.hom) :
    letI := appTopAlgebra (j ≫ q)
    letI := conormalModuleAlong hi a
    AddAction (Ω[Γ(Y, (⊤ : Y.Opens))⁄Γ(S, (⊤ : S.Opens))] →ₗ[Γ(Y, (⊤ : Y.Opens))]
        RingHom.ker i.appTop.hom) (Deformation hi hj p q a A)

Tag 04FK, a remark

Tag 04FK in the Stacks Project.

Stacks.Thickenings.eq_zero_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationUnthickenedTarget.lean, line 108. The attribute's comment: “the vanishing of the conormal datum A”.

The map A of [Stacks Project, Tag 04FH] is zero when Y = Y'. This is the first assertion of [Stacks Project, Tag 04FK]: in the case Y = Y' the conormal datum "is always zero".

theorem eq_zero_of_isIso [IsIso j] (a : X ⟶ Y)
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) : A = 0

Stacks.Thickenings.compatibleLiftsPresheafIsoLiftsOverBasePresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationUnthickenedTarget.lean, line 185. The attribute's comment: “the elementary description of the lifting sheaf”.

The sheaf of [Stacks Project, Tag 04FH] is the elementary rule when Y = Y'. The presheaf of compatible lifts for a datum A is isomorphic to the presheaf of lifts over S extending a, by the isomorphism which is the identity on underlying morphisms.

This is the description of the sheaf asserted by [Stacks Project, Tag 04FK]. The simply transitive action of Hom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) on the elementary rule — the last assertion of that remark — is Stacks.Thickenings.exists_simplyTransitive_addAction_liftsOverBase in StacksFrontier.AlgebraicGeometry.MoreMorphisms.InfinitesimalDeformationUnthickenedTargetAction, obtained by transporting the unrestricted [Stacks Project, Tag 04FJ] along this very isomorphism.

def compatibleLiftsPresheafIsoLiftsOverBasePresheaf [IsIso j]
    (A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i) :
    compatibleLiftsPresheaf pX' pY' a A ≅ liftsOverBasePresheaf i j pX' pY' a

Stacks.Thickenings.exists_simplyTransitive_addAction_liftsOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationUnthickenedTargetAction.lean, line 166. The attribute's comment: “the action of Hom(a^*Ω_{Y/S}, 𝒞_{X/X'}) on the elementary lifting rule, with the group laws, the compatibility with restriction, and simple transitivity over an open carrying a lift”. References: SGA 3 XII (9.4), “partial”.

The action clause of [Stacks Project, Tag 04FK]. Let S be a scheme, let i : X ⟶ X' be a first order thickening, let j : Y ⟶ Y' be an isomorphism — the case Y = Y' of the remark — let p : X' ⟶ S and q : Y' ⟶ S be the structure morphisms and let a : X ⟶ Y. The sheaf Hom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) acts on the elementary rule Stacks.Thickenings.liftsOverBasePresheaf of the remark: over every open V of X' the additive group of sections of SheafHom_{𝒪_X}(a^*Ω_{Y/S}, 𝒞_{X/X'}) over i⁻¹V acts on the morphisms V ⟶ Y' over S restricting to a on i⁻¹V, the action commutes with the restriction maps of that rule, and over an open carrying a lift it is simply transitive.

No affineness is assumed, of S, X', Y' or V, and no condition on conormal sheaves appears anywhere: this is the action on the elementary rule itself, which is what the remark asserts.

The action is Stacks.Thickenings.liftsOverBaseVAdd; everything about it is the unrestricted [Stacks Project, Tag 04FJ] transported along Stacks.Thickenings.compatibleLiftsEquivLiftsOverBase.

theorem exists_simplyTransitive_addAction_liftsOverBase (hsq : i.ker ^ 2 = ⊥) (pX' : X' ⟶ S)
    (pY' : Y' ⟶ S) (a : X ⟶ Y) :
    ∃ act : ∀ V : X'.Opens, deformationHomSections i a (j ≫ pY') V →
        liftsOverBase i j pX' pY' a V → liftsOverBase i j pX' pY' a V,
      (∀ (V : X'.Opens) (c : liftsOverBase i j pX' pY' a V), act V 0 c = c) ∧
        (∀ (V : X'.Opens) (θ η : deformationHomSections i a (j ≫ pY') V)
          (c : liftsOverBase i j pX' pY' a V), act V (θ + η) c = act V θ (act V η c)) ∧
        (∀ (V V' : X'.Opens) (hV : V' ≤ V) (θ : deformationHomSections i a (j ≫ pY') V)
          (c : liftsOverBase i j pX' pY' a V),
          liftsOverBaseRestrict i j pX' pY' a hV (act V θ c)
            = act V' (moduleHomSections.restrict (i.preimage_mono hV) θ)
                (liftsOverBaseRestrict i j pX' pY' a hV c)) ∧
        ∀ (V : X'.Opens) (b₀ c₀ : liftsOverBase i j pX' pY' a V),
          ∃! θ : deformationHomSections i a (j ≫ pY') V, act V θ b₀ = c₀

Tag 0CK2, a remark

Tag 0CK2 in the Stacks Project.

Stacks.Thickenings.epi_modulePullback_immersionConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 143. The attribute's comment: “surjectivity of the conormal map coming from the base, after pullback”.

The canonical map of conormal sheaves coming from the base stays surjective after pullback. For Y = Z ×_{Z'} Y' the canonical map h^* 𝒞_{Z/Z'} ⟶ 𝒞_{Y/Y'} of [Stacks Project, Tag 01R4] is an epimorphism by [Stacks Project, Tag 0473], and the module pullback along any morphism c : W ⟶ Y preserves epimorphisms, being a left adjoint.

Taken at c = a this is the surjectivity of g^* 𝒞_{Z/Z'} ⟶ a^* 𝒞_{Y/Y'} used in [Stacks Project, Tag 0CK2]; taken at c = ι_{i⁻¹V} ≫ a it is the same statement over an open of X'.

theorem epi_modulePullback_immersionConormalSheafMap [IsImmersion j] [IsImmersion k]
    {W : Scheme.{u}} {h : Y ⟶ Z} {h' : Y' ⟶ Z'} (sq : IsPullback j h h' k) (c : W ⟶ Y) :
    Epi ((modulePullback c.toLRSHom.toShHom).map
      (immersionConormalSheafMap j k h h' (toShHom_square sq.w)))

Stacks.Thickenings.eq_of_isBaseCompatibleConormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 191. The attribute's comment: “the conormal datum is determined by the map on the closed subschemes”.

The conormal datum of [Stacks Project, Tag 04FH] is determined by a over a thickened base. If two maps A, B : a^* 𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} are both compatible with the base, they are equal: the map they are precomposed with is an epimorphism by Stacks.Thickenings.epi_modulePullback_immersionConormalSheafMap.

theorem eq_of_isBaseCompatibleConormalMap (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k)
    {A B : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i}
    (hA : IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci A)
    (hB : IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci B) : A = B

Stacks.Thickenings.isBaseCompatibleConormalMap_of_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 284. The attribute's comment: “the composition g^𝒞_{Z/Z'} ⟶ a^𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} is the canonical map induced by g', for the datum of a lift”.

The conormal datum of a lift over the base is compatible with the base. For a morphism b : V ⟶ Y' over Z' restricting to a on i⁻¹V, the canonical map of conormal sheaves of the square it forms is compatible with the base: stacking that square on the cartesian square gives the square (i ∣_ V) ≫ (V.ι ≫ g') = (ι_{i⁻¹V} ≫ a ≫ h) ≫ k, whose canonical map does not involve b.

This is the assertion of [Stacks Project, Tag 0CK2] that the composition g^*𝒞_{Z/Z'} ⟶ a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} "has to be the canonical map induced by g'", read for the datum attached to an actual lift.

theorem isBaseCompatibleConormalMap_of_lift (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k) {V : X'.Opens} {b : V.toScheme ⟶ Y'}
    (hb₁ : b ≫ h' = V.ι ≫ g') (hb₂ : i ∣_ V ≫ b = ((i ⁻¹ᵁ V).ι ≫ a) ≫ j) :
    IsBaseCompatibleConormalMap (i ∣_ V) j k h h' (V.ι ≫ g') ((i ⁻¹ᵁ V).ι ≫ a) sq.w
      (comm_restrict_base i k h g' a ci V)
      (immersionConormalSheafMap (i ∣_ V) j ((i ⁻¹ᵁ V).ι ≫ a) b (toShHom_square hb₂))

Stacks.Thickenings.isBaseCompatibleConormalMap_of_isCompatibleLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 313. The attribute's comment: “the composition g^𝒞_{Z/Z'} ⟶ a^𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} has to be the canonical map induced by g', for the given datum: a datum with a compatible lift over an open is base compatible there”.

A conormal datum that admits a compatible lift is compatible with the base. If some morphism b : V ⟶ Y' out of an open V of X' is a compatible lift of a for the datum A, then the restriction of A to V is compatible with the base: condition (3) of [Stacks Project, Tag 04FI] identifies that restriction with the canonical map of the square b forms, which is compatible with the base by Stacks.Thickenings.isBaseCompatibleConormalMap_of_lift.

This is the assertion of [Stacks Project, Tag 0CK2] that the composition g^*𝒞_{Z/Z'} ⟶ a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} has to be the canonical map induced by g', read for the given datum: wherever the sheaf of [Stacks Project, Tag 04FH] has a section, A is forced to be base compatible, and by Stacks.Thickenings.eq_of_isBaseCompatibleConormalMap that pins it down. So base compatibility is not a restriction on the data the source considers; it is the source's determination of A by a.

theorem isBaseCompatibleConormalMap_of_isCompatibleLift (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k)
    {A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i} {V : X'.Opens} {b : V.toScheme ⟶ Y'}
    (hb : IsCompatibleLift g' h' a A V b) :
    IsBaseCompatibleConormalMap (i ∣_ V) j k h h' (V.ι ≫ g') ((i ⁻¹ᵁ V).ι ≫ a) sq.w
      (comm_restrict_base i k h g' a ci V) (restrictConormalSheafMap a A V)

Stacks.Thickenings.isCompatibleLift_iff_of_isBaseCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 327. The attribute's comment: “the conormal condition on a lift is automatic”.

The third condition of [Stacks Project, Tag 04FI] is automatic over a thickened base. For A compatible with the base, a morphism b : V ⟶ Y' out of an open V of X' is a compatible lift of a exactly when it is a morphism over Z' restricting to a on i⁻¹V.

theorem isCompatibleLift_iff_of_isBaseCompatible (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k)
    {A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i}
    (hA : IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci A) (V : X'.Opens)
    (b : V.toScheme ⟶ Y') :
    IsCompatibleLift g' h' a A V b ↔
      b ≫ h' = V.ι ≫ g' ∧ i ∣_ V ≫ b = ((i ⁻¹ᵁ V).ι ≫ a) ≫ j

Stacks.Thickenings.compatibleLiftsPresheafIsoLiftsOverBasePresheafOfBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBase.lean, line 354. The attribute's comment: “the elementary description of the lifting sheaf”.

The sheaf of [Stacks Project, Tag 04FH] is the elementary rule over a thickened base. For A compatible with the base, the presheaf of compatible lifts of a is isomorphic to the presheaf Stacks.Thickenings.liftsOverBasePresheaf of morphisms V ⟶ Y' over Z' restricting to a on i⁻¹V, by the isomorphism which is the identity on underlying morphisms.

This is the description of the sheaf asserted by [Stacks Project, Tag 0CK2]. The simply transitive action of Hom_{𝒪_X}(a^*Ω_{Y/Z}, 𝒞_{X/X'}) on the elementary rule — the last assertion of that remark — is Stacks.Thickenings.exists_simplyTransitive_addAction_liftsOverBaseOfBase in StacksFrontier.AlgebraicGeometry.MoreMorphisms.InfinitesimalDeformationThickenedBaseAction, obtained by transporting the unrestricted [Stacks Project, Tag 04FJ] for the base Z' along this isomorphism and along the identification Ω_{Y/Z'} ≅ Ω_{Y/Z} that holds because k is an immersion.

def compatibleLiftsPresheafIsoLiftsOverBasePresheafOfBase (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k)
    {A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i}
    (hA : IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci A) :
    compatibleLiftsPresheaf g' h' a A ≅ liftsOverBasePresheaf i j g' h' a

Stacks.Thickenings.exists_simplyTransitive_addAction_liftsOverBaseOfBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBaseAction.lean, line 265. The attribute's comment: “the action of Hom(a^*Ω_{Y/Z}, 𝒞_{X/X'}) on the elementary lifting rule, with the group laws, the compatibility with restriction, and simple transitivity over an open carrying a lift”. References: SGA 3 XII (9.4), “partial”.

The action clause of [Stacks Project, Tag 0CK2]. Let k : Z ⟶ Z' be an immersion, let i : X ⟶ X' be a first order thickening and j : Y ⟶ Y' an immersion, both over Z' by g' : X' ⟶ Z' and h' : Y' ⟶ Z', assume Y = Z ×_{Z'} Y', let a : X ⟶ Y and let A be a conormal datum compatible with the base. Then the sheaf Hom_{𝒪_X}(a^*Ω_{Y/Z}, 𝒞_{X/X'}) — differentials relative to Z, as the source writes them — acts on the elementary rule Stacks.Thickenings.liftsOverBasePresheaf of the remark: over every open V of X' the additive group of its sections over i⁻¹V acts on the morphisms V ⟶ Y' over Z' restricting to a on i⁻¹V, the action commutes with the restriction maps of that rule, and over an open carrying a lift it is simply transitive.

No affineness is assumed, of Z', X', Y' or V, and no condition on conormal sheaves appears in the conclusion: this is the action on the elementary rule itself, which is what the remark asserts.

The action is Stacks.Thickenings.liftsOverBaseVAddOfBase: the unrestricted [Stacks Project, Tag 04FJ] for the base Z', carried over by the identification Ω_{Y/Z'} ≅ Ω_{Y/Z} of Stacks.Thickenings.pullbackCotangentSheafIsoOfBase and by the identification of the two notions of lift.

theorem exists_simplyTransitive_addAction_liftsOverBaseOfBase (hsq : i.ker ^ 2 = ⊥)
    (sq : IsPullback j h h' k) (ci : i ≫ g' = (a ≫ h) ≫ k)
    {A : (modulePullback a.toLRSHom.toShHom).obj (immersionConormalSheaf j) ⟶
      immersionConormalSheaf i}
    (hA : IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci A) :
    ∃ act : ∀ V : X'.Opens, deformationHomSections i a h V →
        liftsOverBase i j g' h' a V → liftsOverBase i j g' h' a V,
      (∀ (V : X'.Opens) (c : liftsOverBase i j g' h' a V), act V 0 c = c) ∧
        (∀ (V : X'.Opens) (θ η : deformationHomSections i a h V)
          (c : liftsOverBase i j g' h' a V), act V (θ + η) c = act V θ (act V η c)) ∧
        (∀ (V V' : X'.Opens) (hV : V' ≤ V) (θ : deformationHomSections i a h V)
          (c : liftsOverBase i j g' h' a V),
          liftsOverBaseRestrict i j g' h' a hV (act V θ c)
            = act V' (moduleHomSections.restrict (i.preimage_mono hV) θ)
                (liftsOverBaseRestrict i j g' h' a hV c)) ∧
        ∀ (V : X'.Opens) (b₀ c₀ : liftsOverBase i j g' h' a V),
          ∃! θ : deformationHomSections i a h V, act V θ b₀ = c₀

Stacks.Thickenings.liftsOverBaseVAddOfBase_comp_of_homSectionValue_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBaseActionNaturality.lean, line 200. The attribute's comment: “the action of Hom(a^*Ω_{Y/Z}, 𝒞_{X/X'}) on the elementary lifting rule is natural in the thickening: for two situations of the tag with vertical maps, acting and pushing a lift forward commute, given the commuting square of Tag 04BZ for the two acting sections. This is naturality of the action, not a new construction of it”.

The action of [Stacks Project, Tag 0CK2] on the elementary lifting rule is natural in the thickening. This is the input a statement about a sum of first-order deformations needs: the sum is realized over the doubled coordinate module M × M (Deformation.exists_linearFunctorLift_sum), so the action has to be run once over k[M × M] and pushed forward along the two projections k[M × M] ⟶ k[M] and their sum, and this is the compatibility of the action with those pushforwards.

Let two situations of [Stacks Project, Tag 0CK2] be given, with vertical maps (wX, w) of the thickenings and (vY, v) of the targets. Let c be an elementary lift over an open V₁ of X₁', let d be one over an open V₂ of X₂' with d ≫ v = w ≫ c on underlying morphisms, and let θ₁ and θ₂ be sections of the two acting sheaves whose perturbations correspond under w^♯ and v^♯. Then acting and pushing forward commute:

(θ₂ ⬝ d) ≫ v = w ≫ (θ₁ ⬝ c)

on underlying morphisms. The hypothesis hθ is the commuting square of [Stacks Project, Tag 04BZ] read on the conormal sections the two sections produce, and it is transported to the acting sheaf of the source — the differentials relative to Z₁ and to Z₂ — by Stacks.Thickenings.baseDeformationHomSectionsEquiv, which is the identification the action is defined through.

theorem liftsOverBaseVAddOfBase_comp_of_homSectionValue_comm
    (hsq₁ : i₁.ker ^ 2 = ⊥) (hsq₂ : i₂.ker ^ 2 = ⊥)
    (sq₁ : IsPullback j₁ h₁ h₁' k₁) (sq₂ : IsPullback j₂ h₂ h₂' k₂)
    (ci₁ : i₁ ≫ g₁' = (a₁ ≫ h₁) ≫ k₁) (ci₂ : i₂ ≫ g₂' = (a₂ ≫ h₂) ≫ k₂)
    {A₁ : (modulePullback a₁.toLRSHom.toShHom).obj (immersionConormalSheaf j₁) ⟶
      immersionConormalSheaf i₁}
    {A₂ : (modulePullback a₂.toLRSHom.toShHom).obj (immersionConormalSheaf j₂) ⟶
      immersionConormalSheaf i₂}
    (hA₁ : IsBaseCompatibleConormalMap i₁ j₁ k₁ h₁ h₁' g₁' a₁ sq₁.w ci₁ A₁)
    (hA₂ : IsBaseCompatibleConormalMap i₂ j₂ k₂ h₂ h₂' g₂' a₂ sq₂.w ci₂ A₂)
    (V₁ : X₁'.Opens) (V₂ : X₂'.Opens)
    (θ₁ : deformationHomSections i₁ a₁ h₁ V₁) (θ₂ : deformationHomSections i₂ a₂ h₂ V₂)
    (c : liftsOverBase i₁ j₁ g₁' h₁' a₁ V₁) (d : liftsOverBase i₂ j₂ g₂' h₂' a₂ V₂)
    {wX : (i₂ ⁻¹ᵁ V₂).toScheme ⟶ (i₁ ⁻¹ᵁ V₁).toScheme} {w : V₂.toScheme ⟶ V₁.toScheme}
    {vY : Y₂ ⟶ Y₁} {v : Y₂' ⟶ Y₁'}
    (cT : i₂ ∣_ V₂ ≫ w = wX ≫ i₁ ∣_ V₁) (cj : j₂ ≫ v = vY ≫ j₁)
    (cX : ((i₂ ⁻¹ᵁ V₂).ι ≫ a₂) ≫ vY = wX ≫ ((i₁ ⁻¹ᵁ V₁).ι ≫ a₁))
    (cA : d.1 ≫ v = w ≫ c.1)
    (hθ : ∀ (W : Y₁'.Opens) (s : Γ(Y₁', W)),
      (V₂.toScheme.presheaf.map (eqToHom (preimage_comp_eq cA W)).op).hom
          ((w.app (c.1 ⁻¹ᵁ W)).hom
            (homSectionValue hsq₁ h₁' c.2.2
              (baseDeformationHomSectionsEquiv sq₁ a₁ V₁ θ₁) W s))
        = homSectionValue hsq₂ h₂' d.2.2
            (baseDeformationHomSectionsEquiv sq₂ a₂ V₂ θ₂) (v ⁻¹ᵁ W) ((v.app W).hom s)) :
    (liftsOverBaseVAddOfBase hsq₂ sq₂ ci₂ hA₂ V₂ θ₂ d).1 ≫ v =
      w ≫ (liftsOverBaseVAddOfBase hsq₁ sq₁ ci₁ hA₁ V₁ θ₁ c).1

Stacks.Thickenings.isBaseCompatibleConormalMap_of_globalLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBaseGlobalLift.lean, line 83. The attribute's comment: “the composition g^C_{Z/Z'} -> a^C_{Y/Y'} -> C_{X/X'} is the canonical map induced by g', for the datum of a lift defined on all of X'”.

The conormal datum of a lift defined on all of X' is compatible with the base. For a morphism b : X' ⟶ Y' over Z' whose restriction along i is a, the square it forms with i and j has a canonical map of conormal sheaves; stacking that square on the cartesian square of the base gives the square i ≫ g' = (a ≫ h) ≫ k, whose canonical map does not mention b. This is the assertion of [Stacks Project, Tag 0CK2] that the composite g^*𝒞_{Z/Z'} ⟶ a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} "has to be the canonical map induced by g'", read for a lift over the whole space.

Stacks.Thickenings.isBaseCompatibleConormalMap_of_lift is the same statement for a lift defined on an open V of X', where the thickening is i ∣_ V.

theorem isBaseCompatibleConormalMap_of_globalLift (sq : IsPullback j h h' k)
    (ci : i ≫ g' = (a ≫ h) ≫ k) {b : X' ⟶ Y'} (hb₁ : b ≫ h' = g') (hb₂ : i ≫ b = a ≫ j) :
    IsBaseCompatibleConormalMap i j k h h' g' a sq.w ci
      (immersionConormalSheafMap i j a b (toShHom_square hb₂))

Stacks.Thickenings.exists_simplyTransitive_addAction_liftsOverBaseOfGlobalLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationThickenedBaseGlobalLift.lean, line 110. The attribute's comment: “the simply transitive action of Hom(a^*Omega_{Y/Z}, C_{X/X'}) on the lifts of a over the whole space, with the conormal datum discharged by an actual lift”. References: SGA 3 XII (9.4), “partial”.

The action clause of [Stacks Project, Tag 0CK2] over the whole space, from a lift. Let k : Z ⟶ Z' be an immersion, let i : X ⟶ X' be a first order thickening and j : Y ⟶ Y' an immersion, both over Z' by g' and h', assume Y = Z ×_{Z'} Y', and let a : X ⟶ Y admit a lift b : X' ⟶ Y', that is, a morphism over Z' whose restriction along i is a. Then the additive group of sections over X of SheafHom_{𝒪_X}(a^*Ω_{Y/Z}, 𝒞_{X/X'}) — differentials relative to Z, as the source writes them — acts simply transitively on the morphisms X' ⟶ Y' over Z' restricting to a along i.

No conormal datum appears: the lift produces one, by Stacks.Thickenings.isBaseCompatibleConormalMap_of_globalLift, and it is the only one compatible with the base by Stacks.Thickenings.eq_of_isBaseCompatibleConormalMap. No affineness is assumed, of Z', X' or Y', and the hypothesis that the open carries a lift — which is what makes the action of that tag simply transitive — is discharged by b.

theorem exists_simplyTransitive_addAction_liftsOverBaseOfGlobalLift [IsClosedImmersion i]
    (hsq : i.ker ^ 2 = ⊥) (sq : IsPullback j h h' k) (ci : i ≫ g' = (a ≫ h) ≫ k)
    {b : X' ⟶ Y'} (hb₁ : b ≫ h' = g') (hb₂ : i ≫ b = a ≫ j) :
    ∃ act : deformationHomSections i a h ⊤ →
        liftsOverBase i j g' h' a ⊤ → liftsOverBase i j g' h' a ⊤,
      (∀ c : liftsOverBase i j g' h' a ⊤, act 0 c = c) ∧
        (∀ (θ η : deformationHomSections i a h ⊤) (c : liftsOverBase i j g' h' a ⊤),
          act (θ + η) c = act θ (act η c)) ∧
          ∀ c₀ c₁ : liftsOverBase i j g' h' a ⊤, ∃! θ : deformationHomSections i a h ⊤,
            act θ c₀ = c₁

Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeDeformationConormalBaseChange.lean, line 225. The attribute's comment: “the conormal map of an arrow of deformations is a conormal datum compatible with the base: its composite with the flat base change of the source deformation is the canonical map of Tag 01R4 for the square carrying the special fibre of the target over the closed point of the source's base. This is the factorisation through the total space of the source, not an identification of the map on the base with the map of maximal ideals”.

The conormal map of an arrow of deformations is compatible with the base. The special-fibre immersion of Q sits over the closed point of Spec A through Q.toBase ≫ Spec φ.base, and that square factors through P.scheme: the arrow's square followed by the special-fibre square of P. Reading the canonical map of [Stacks Project, Tag 01R4] along that factorisation is exactly the compatibility of [Stacks Project, Tag 0CK2] for the conormal map of the arrow, with the flat-base-change map of P as the datum coming from the base.

This is Stacks.Immersion.immersionConormalSheafMap_comp and nothing else; the content is that the two squares of a deformation and of an arrow of deformations stack to the square the flat-base-change map of the target is read on.

theorem isBaseCompatibleConormalMap_deformationConormalMap (φ : P ⟶ Q) :
    IsBaseCompatibleConormalMap Q.specialMap P.specialMap (residueSpecMap P.base)
      X.hom P.toBase (φ.map ≫ P.toBase) (𝟙 X.left)
      P.specialCartesian.w (square_comp (specialMap_comp_map φ) P.specialCartesian.w)
      (immersionConormalSheafMap Q.specialMap P.specialMap (𝟙 X.left) φ.map
        (toShHom_square (specialMap_comp_map φ)))

Deformation.Examples.eq_of_isBaseCompatibleConormalMap_deformationConormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeDeformationConormalBaseChange.lean, line 275. The attribute's comment: “the conormal map of an arrow of deformations is the UNIQUE conormal datum compatible with the base, the special-fibre square of the source being cartesian. This pins the map by the base object; it does not compute it on sections”.

The conormal map of an arrow of deformations is the unique conormal datum compatible with the base. The special-fibre square of P is cartesian, so Stacks.Thickenings.eq_of_isBaseCompatibleConormalMap applies: any map 𝟙_X^* 𝒞_{X/P.scheme} ⟶ 𝒞_{X/Q.scheme} whose composite with the flat base change of P is the canonical map of the composite square is the conormal map of φ.

This is the sense in which the conormal map of an arrow of deformations "is" the map of the base objects: it is determined by the square over Spec A, and Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalBaseChangeIso exhibits that square as the one the flat base change of Q and the conormal map of φ.base are read on.

theorem eq_of_isBaseCompatibleConormalMap_deformationConormalMap (φ : P ⟶ Q)
    {A : (modulePullback (Scheme.Hom.toLRSHom (𝟙 X.left)).toShHom).obj
        (immersionConormalSheaf P.specialMap) ⟶ immersionConormalSheaf Q.specialMap}
    (hA : IsBaseCompatibleConormalMap Q.specialMap P.specialMap (residueSpecMap P.base)
      X.hom P.toBase (φ.map ≫ P.toBase) (𝟙 X.left)
      P.specialCartesian.w (square_comp (specialMap_comp_map φ) P.specialCartesian.w) A) :
    A = immersionConormalSheafMap Q.specialMap P.specialMap (𝟙 X.left) φ.map
      (toShHom_square (specialMap_comp_map φ))

Deformation.Examples.isBaseCompatibleConormalMap_baseChangeDeformationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeDeformationConormalBaseChange.lean, line 378. The attribute's comment: “at the base change of a deformation: the conormal map of the arrow of a deformation onto its base change along a morphism of C_Lambda is a conormal datum compatible with the base. This is the general statement for an arrow of deformations instantiated at baseChangeDeformationHom, not a separate computation”.

The conormal map of the arrow of a deformation onto its base change is compatible with the base. This is Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalMap at Deformation.Examples.baseChangeDeformationHom, the arrow the cofibered structure of the deformation category produces, whose morphism of total spaces is the first projection of the fibre product and whose base component is g.

Taken together with Deformation.Examples.isBaseCompatibleConormalMap_deformationConormalBaseChangeIso and the uniqueness Deformation.Examples.eq_of_isBaseCompatibleConormalMap_deformationConormalMap, this says that the conormal map 𝒞_{X/P.scheme} ⟶ 𝒞_{X/(P ×_A B).scheme} of the base change is determined by g through the conormal map Deformation.Examples.residueConormalMap of the base objects.

theorem isBaseCompatibleConormalMap_baseChangeDeformationHom :
    IsBaseCompatibleConormalMap (baseChangeDeformation P g).specialMap P.specialMap
      (residueSpecMap P.base) X.hom P.toBase
      ((baseChangeDeformationHom P g).map ≫ P.toBase) (𝟙 X.left)
      P.specialCartesian.w
      (square_comp (specialMap_comp_map (baseChangeDeformationHom P g)) P.specialCartesian.w)
      (immersionConormalSheafMap (baseChangeDeformation P g).specialMap P.specialMap
        (𝟙 X.left) (baseChangeDeformationHom P g).map
        (toShHom_square (specialMap_comp_map (baseChangeDeformationHom P g))))

Tag 04FL, a lemma

Tag 04FL in the Stacks Project.

Stacks.Thickenings.homEquiv_diagonalConormalSheafMap_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/MapDifferenceDiagonalSheaf.lean, line 592.

The difference of two maps to a fixed scheme, through the diagonal, [Stacks, Tag 04FL].

theorem homEquiv_diagonalConormalSheafMap_d [IsImmersion i] (hq : b' ≫ q = a' ≫ q)
    (comm_a : i ≫ a' = a) (comm_b : i ≫ b' = a) (V : Y.Opens) (s : Γ(Y, V)) :
    (((modulePullbackPushforwardAdjunction a.toLRSHom.toShHom).homEquiv _ _
          (diagonalConormalSheafMap hq comm_a comm_b)).val.app (op V))
        (q.universalRelativeDerivation.d s) =
      conormalClass i (liftPairOpen a' b' V) (le_preimage_liftPairOpen comm_a comm_b V)
        (liftDiffSection a' b' V s) (app_liftDiffSection comm_a comm_b V s)

Tag 04BX, a lemma

Tag 04BX in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isIso_relativeDifferentialsMap_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/Etale.lean, line 111.

Stacks Project, Tag 04BX. In a commutative square of schemes whose two horizontal arrows f : X₂ ⟶ X₁ and g : S₂ ⟶ S₁ are étale, the canonical map f^* Ω_{X₁/S₁} ⟶ Ω_{X₂/S₂} is an isomorphism.

theorem isIso_relativeDifferentialsMap_of_etale {X₁ X₂ S₁ S₂ : Scheme.{u}} (f : X₂ ⟶ X₁)
    (p₁ : X₁ ⟶ S₁) (p₂ : X₂ ⟶ S₂) (g : S₂ ⟶ S₁) (hcomm : f ≫ p₁ = p₂ ≫ g)
    [Etale f] [Etale g] :
    IsIso (relativeDifferentialsMap f p₁ p₂ g hcomm)

Tag 04BY, a lemma

Tag 04BY in the Stacks Project.

Stacks.Thickenings.derivationActionSheaf_comp_etaleLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationEtaleLocalizationSheaf.lean, line 481.

Acting by a derivation commutes with an étale localization. Let (h, h') : (T₂ ⊂ T₂') ⟶ (T₁ ⊂ T₁') be a morphism of first-order thickenings, let (f, f') : (X₂ ⟶ X₂') ⟶ (X₁ ⟶ X₁') be a morphism of the right-hand pairs, let (a₁, a₁') and (a₂, a₂') be morphisms of thickenings compatible with them, and let p₁ : X₁' ⟶ S₁, p₂ : X₂' ⟶ S₂ and k : S₂ ⟶ S₁ form a commutative square with f. Assume f and k are étale. Then for every 𝒪_{T₁}-linear θ₁ : a₁^*Ω_{X₁/S₁} ⟶ 𝒞_{T₁/T₁'}, the lifts θ₁ ⬝ a₁' and θ₂ ⬝ a₂' of [Stacks Project, Tag 0CK1] — for θ₂ the transported datum Stacks.Thickenings.localizedDerivationSheaf — give a commutative square:
(θ₂ ⬝ a₂') ≫ f' = h' ≫ (θ₁ ⬝ a₁').
Nothing is assumed affine, and both actions are the ones constructed by Stacks.Thickenings.derivationActionSheaf, not morphisms assumed to satisfy a relation.

j₁ and j₂ are not assumed to be first-order thickenings, and the commutativity of the square of bases is assumed only as the square f ≫ (j₁ ≫ p₁) = (j₂ ≫ p₂) ≫ k of the closed subschemes, which the ambient square f' ≫ p₁ = p₂ ≫ k implies.

theorem derivationActionSheaf_comp_etaleLocalization
    (hi₁ : i₁.ker ^ 2 = ⊥) (hi₂ : i₂.ker ^ 2 = ⊥)
    (ca₁ : i₁ ≫ a₁' = a₁ ≫ j₁) (ca₂ : i₂ ≫ a₂' = a₂ ≫ j₂)
    (cT : i₂ ≫ h' = h ≫ i₁) (cj : j₂ ≫ f' = f ≫ j₁) (cX : a₂ ≫ f = h ≫ a₁)
    (cA : a₂' ≫ f' = h' ≫ a₁') (cS : f ≫ (j₁ ≫ p₁) = (j₂ ≫ p₂) ≫ k)
    [AlgebraicGeometry.Etale f] [AlgebraicGeometry.Etale k]
    (θ₁ : (Scheme.Modules.pullback a₁).obj (Scheme.Hom.relativeDifferentials (j₁ ≫ p₁)) ⟶
      Stacks.Conormal.conormalSheaf i₁) :
    derivationActionSheaf hi₂ p₂ ca₂ (localizedDerivationSheaf cT cX cS θ₁) ≫ f' =
      h' ≫ derivationActionSheaf hi₁ p₁ ca₁ θ₁

Tag 04BZ, a remark

Tag 04BZ in the Stacks Project.

Stacks.Thickenings.derivationAction_comp_of_derivation_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationGivenDerivation.lean, line 130. The attribute's comment: “affine case, with the two actions of Tag 0CK1 constructed by Stacks.Thickenings.derivationAction; the remark for arbitrary schemes is Stacks.Thickenings.derivationActionSheaf_comp_of_derivationSection_comm”.

Acting by compatible derivation data commutes with the vertical maps, the affine case of [Stacks Project, Tag 04BZ]. Let (h, h') and (f, f') be the vertical maps of a diagram of first-order thickenings with affine ambient schemes as in [Stacks Project, Tag 04BY], let (a₁, a₁') and (a₂, a₂') be morphisms of thickenings compatible with them, and let p₁ : X₁' ⟶ S₁ and p₂ : X₂' ⟶ S₂ be the structure morphisms. Nothing is assumed étale. Given Γ(X₁, ⊤)-linear θ₁ : Ω[Γ(X₁, ⊤)⁄Γ(S₁, ⊤)] ⟶ 𝒞_{T₁/T₁'} and Γ(X₂, ⊤)-linear θ₂ : Ω[Γ(X₂, ⊤)⁄Γ(S₂, ⊤)] ⟶ 𝒞_{T₂/T₂'} whose derivations D_n = θ_n ∘ d_{X_n/S_n} of Equation [Stacks Project, Tag 04BV] satisfy D₂ (f^♯ y) = (h')^♯ (D₁ y) — the commuting square of the source — acting by θ₁ on a₁' and by θ₂ on a₂' gives a commutative square:
(θ₂ ⬝ a₂') ≫ f' = h' ≫ (θ₁ ⬝ a₁').
In [Stacks Project, Tag 04BY] the second datum is built from the first out of the étale hypotheses, and the hypothesis hθ here is then its defining property Stacks.Thickenings.localizedDerivation_apply; see Stacks.Thickenings.derivationAction_comp_localizedDerivation.

theorem derivationAction_comp_of_derivation_comm [IsAffine T₁'] [IsAffine T₂'] [IsAffine X₁']
    [IsAffine X₂'] (hi₁ : IsFirstOrderThickening i₁) (hi₂ : IsFirstOrderThickening i₂)
    (ca₁ : i₁ ≫ a₁' = a₁ ≫ j₁) (ca₂ : i₂ ≫ a₂' = a₂ ≫ j₂) (cj : j₂ ≫ f' = f ≫ j₁)
    (cA : a₂' ≫ f' = h' ≫ a₁') :
    letI := appTopAlgebra (j₁ ≫ p₁)
    letI := conormalModuleAlong hi₁ a₁
    letI := appTopAlgebra (j₂ ≫ p₂)
    letI := conormalModuleAlong hi₂ a₂
    ∀ (θ₁ : Ω[Γ(X₁, (⊤ : X₁.Opens))⁄Γ(S₁, (⊤ : S₁.Opens))] →ₗ[Γ(X₁, (⊤ : X₁.Opens))]
        RingHom.ker i₁.appTop.hom)
      (θ₂ : Ω[Γ(X₂, (⊤ : X₂.Opens))⁄Γ(S₂, (⊤ : S₂.Opens))] →ₗ[Γ(X₂, (⊤ : X₂.Opens))]
        RingHom.ker i₂.appTop.hom),
      (∀ y : Γ(X₁, (⊤ : X₁.Opens)),
          ((θ₂ (KaehlerDifferential.D _ _ (f.appTop.hom y)) : RingHom.ker i₂.appTop.hom) :
              Γ(T₂', (⊤ : T₂'.Opens)))
            = h'.appTop.hom ((θ₁ (KaehlerDifferential.D _ _ y) : RingHom.ker i₁.appTop.hom) :
              Γ(T₁', (⊤ : T₁'.Opens)))) →
        derivationAction hi₂ ca₂ p₂ θ₂ ≫ f' = h' ≫ derivationAction hi₁ ca₁ p₁ θ₁

Stacks.Thickenings.derivationActionSheaf_comp_of_derivationSection_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/InfinitesimalDeformationSheafAction.lean, line 282. The attribute's comment: “the two actions of Tag 0CK1 constructed by Stacks.Thickenings.derivationActionSheaf”.

Acting by compatible derivation data commutes with the vertical maps, [Stacks Project, Tag 04BZ] for arbitrary schemes, with both actions constructed. Let (h, h') and (f, f') be the vertical maps of a diagram of first-order thickenings as in [Stacks Project, Tag 04BY], let (a₁, a₁') and (a₂, a₂') be morphisms of thickenings compatible with them, and let p₁ : X₁' ⟶ S₁ and p₂ : X₂' ⟶ S₂ be the structure morphisms. Nothing is assumed étale and nothing is assumed affine. Given θ₁ : a₁^*Ω_{X₁/S₁} ⟶ 𝒞_{T₁/T₁'} and θ₂ : a₂^*Ω_{X₂/S₂} ⟶ 𝒞_{T₂/T₂'} whose derivations D_n = θ_n ∘ d_{X_n/S_n} of Equation [Stacks Project, Tag 04BV] satisfy D₂ (f^♯ y) = (h')^♯ (D₁ y) — the commuting square of the source, read inside the ambient structure sheaves — the lifts θ₁ ⬝ a₁' and θ₂ ⬝ a₂' of [Stacks Project, Tag 0CK1] give a commutative square:
(θ₂ ⬝ a₂') ≫ f' = h' ≫ (θ₁ ⬝ a₁').
This is Stacks.Thickenings.derivationAction_comp_of_derivationSection_comm with its two hypotheses Stacks.Thickenings.IsDerivationAction discharged by Stacks.Thickenings.isDerivationAction_derivationActionSheaf: the lifts are the morphisms constructed by Stacks.Thickenings.derivationActionSheaf, not morphisms assumed to satisfy a relation.

theorem derivationActionSheaf_comp_of_derivationSection_comm
    (hi₁ : i₁.ker ^ 2 = ⊥) (hi₂ : i₂.ker ^ 2 = ⊥)
    (p₁ : X₁' ⟶ S₁) (p₂ : X₂' ⟶ S₂)
    (ca₁ : i₁ ≫ a₁' = a₁ ≫ j₁) (ca₂ : i₂ ≫ a₂' = a₂ ≫ j₂)
    (cT : i₂ ≫ h' = h ≫ i₁) (cj : j₂ ≫ f' = f ≫ j₁) (cX : a₂ ≫ f = h ≫ a₁)
    (cA : a₂' ≫ f' = h' ≫ a₁')
    {θ₁ : (Scheme.Modules.pullback a₁).obj (Scheme.Hom.relativeDifferentials (j₁ ≫ p₁)) ⟶
      Stacks.Conormal.conormalSheaf i₁}
    {θ₂ : (Scheme.Modules.pullback a₂).obj (Scheme.Hom.relativeDifferentials (j₂ ≫ p₂)) ⟶
      Stacks.Conormal.conormalSheaf i₂}
    (hθ : ∀ (V : X₁'.Opens) (s : Γ(X₁', V)),
      (T₂'.presheaf.map (eqToHom (preimage_comp_eq cA V)).op).hom
          ((h'.app (a₁' ⁻¹ᵁ V)).hom (derivationSectionι hi₁ p₁ ca₁ θ₁ V ((j₁.app V).hom s)))
        = derivationSectionι hi₂ p₂ ca₂ θ₂ (f' ⁻¹ᵁ V)
            ((j₂.app (f' ⁻¹ᵁ V)).hom ((f'.app V).hom s))) :
    derivationActionSheaf hi₂ p₂ ca₂ θ₂ ≫ f' = h' ≫ derivationActionSheaf hi₁ p₁ ca₁ θ₁

Sources

LeanStacks.Thickenings.mapDifferenceDerivation · Stacks.Thickenings.mapDifferenceDerivation_appTop · Stacks.Thickenings.mapDifferenceSheaf · Stacks.Thickenings.mapDifferenceSheaf_app · Stacks.Thickenings.app_mapDifferenceSheaf · Stacks.Thickenings.mapDifferenceSheaf_map · Stacks.Thickenings.mapDifferenceSheaf_add · Stacks.Thickenings.mapDifferenceSheaf_appLE_base

Section37.10 Infinitesimal deformations of schemes #

Section 37.10 of the Stacks Project, Tag 063X. 6 tags here are carried by 50 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 063Y, a lemma

Tag 063Y in the Stacks Project.

Stacks.Thickenings.flat_and_isPullback_of_isIso_firstOrderThickeningConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FirstOrderThickeningConormalConverse.lean, line 585. The attribute's comment: “(2) ⟹ (1) for schemes”.

[Stacks Project, Tag 063Y], (2) ⟹ (1), for schemes. Let (f, f') : (X ⊂ X') → (S ⊂ S') be a morphism of first-order thickenings of schemes, with f = φ.left and f' = φ.right, and let f be flat. If the canonical map f^* 𝒞_{S/S'} ⟶ 𝒞_{X/X'} is an isomorphism, then f' is flat and X = S ×_{S'} X'.

The hypothesis is condition (2) of the tag and the conclusion is its condition (1): Flat φ.right is flatness of f' and IsPullback i φ.left φ.right j is the base-change identity X = S ×_{S'} X'. The flatness of f is the tag's standing hypothesis, and here it is used: it is what makes Γ(S, j⁻¹V) ⟶ Γ(X, i⁻¹U) flat, which is a hypothesis of the commutative algebra Ideal.bijective_fibreTensorSMulHomToKer_iff.

theorem flat_and_isPullback_of_isIso_firstOrderThickeningConormalSheafMap {i : X ⟶ X'}
    {j : S ⟶ S'} (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (φ : Arrow.mk i ⟶ Arrow.mk j) [Flat φ.left]
    (hiso : letI := hi.1
      letI := hj.1
      IsIso (firstOrderThickeningConormalSheafMap hi hj φ)) :
    Flat φ.right ∧ IsPullback i φ.left φ.right j

Stacks.Thickenings.flat_and_isPullback_iff_isIso_firstOrderThickeningConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FirstOrderThickeningConormalConverse.lean, line 609.

[Stacks Project, Tag 063Y] for schemes. Let (f, f') : (X ⊂ X') → (S ⊂ S') be a morphism of first-order thickenings of schemes with f = φ.left flat. Then the following are equivalent:

(1) f' is flat and X = S ×_{S'} X';

(2) the canonical map f^* 𝒞_{S/S'} ⟶ 𝒞_{X/X'} is an isomorphism.

The two directions are Stacks.Thickenings.isIso_firstOrderThickeningConormalSheafMap and Stacks.Thickenings.flat_and_isPullback_of_isIso_firstOrderThickeningConormalSheafMap. The standing hypothesis that f be flat is not needed for (1) ⟹ (2), where it follows from the other two; it is needed for (2) ⟹ (1).

theorem flat_and_isPullback_iff_isIso_firstOrderThickeningConormalSheafMap {i : X ⟶ X'}
    {j : S ⟶ S'} (hi : IsFirstOrderThickening i) (hj : IsFirstOrderThickening j)
    (φ : Arrow.mk i ⟶ Arrow.mk j) [Flat φ.left] :
    letI := hi.1
    letI := hj.1
    (Flat φ.right ∧ IsPullback i φ.left φ.right j) ↔
      IsIso (firstOrderThickeningConormalSheafMap hi hj φ)

Stacks.Thickenings.epi_firstOrderThickeningConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FirstOrderThickeningConormalMap.lean, line 137. The attribute's comment: “(1) ⟹ (2) for schemes, surjectivity”.

The surjectivity half of condition (2) of [Stacks Project, Tag 063Y], for schemes. For a morphism of first-order thickenings whose square is cartesian, so that X = S ×_{S'} X', the canonical map f^* 𝒞_{S/S'} ⟶ 𝒞_{X/X'} is an epimorphism.

No flatness is used: cartesianness alone gives surjectivity, by Stacks.Immersion.epi_immersionConormalSheafMap, which is the surjectivity clause of [Stacks Project, Tag 0473] for a cartesian square of immersions. The cartesian hypothesis is the second half of condition (1) of the tag, so this is the half of (1) ⟹ (2) that the flatness hypotheses are not needed for.

theorem epi_firstOrderThickeningConormalSheafMap (hi : IsFirstOrderThickening i)
    (hj : IsFirstOrderThickening j) (φ : Arrow.mk i ⟶ Arrow.mk j)
    (sq : IsPullback i φ.left φ.right j) :
    letI := hi.1
    letI := hj.1
    Epi (firstOrderThickeningConormalSheafMap hi hj φ)

Stacks.Thickenings.isIso_firstOrderThickeningConormalSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FirstOrderThickeningConormalMap.lean, line 183. The attribute's comment: “(1) ⟹ (2) for schemes”.

[Stacks Project, Tag 063Y], (1) ⟹ (2), for schemes. Let (f, f') : (X ⊂ X') → (S ⊂ S') be a morphism of first-order thickenings of schemes, with f = φ.left and f' = φ.right. If f' is flat and X = S ×_{S'} X', then the canonical map f^* 𝒞_{S/S'} ⟶ 𝒞_{X/X'} is an isomorphism.

The two hypotheses are exactly the two halves of condition (1) of the tag: Flat φ.right is flatness of f', and sq is the base-change identity X = S ×_{S'} X'. The conclusion is condition (2). The standing hypothesis of the tag that f be flat is not needed, because it is a consequence of the other two.

This is Stacks.Immersion.isIso_immersionConormalSheafMap_of_flat, the flat base-change clause of [Stacks Project, Tag 0473], applied to the square of immersions underlying the morphism of thickenings.

theorem isIso_firstOrderThickeningConormalSheafMap (hi : IsFirstOrderThickening i)
    (hj : IsFirstOrderThickening j) (φ : Arrow.mk i ⟶ Arrow.mk j) [Flat φ.right]
    (sq : IsPullback i φ.left φ.right j) :
    letI := hi.1
    letI := hj.1
    IsIso (firstOrderThickeningConormalSheafMap hi hj φ)

Ideal.bijective_tensorSMulHomToKer_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/SquareZeroConormal.lean, line 346. The attribute's comment: “affine case”. References: SGA 3 III (0.14), “partial”; SGA 3 XV (2.7), “affine case”.

Stacks 063Y, the affine case. Let I ^ 2 = 0 in A', write A = A' ⧸ I, let B be a quotient of the A'-algebra B' which is compatibly an A-algebra, and let J be the kernel of B' → B. Assume A → B flat. Then the canonical map I ⊗[A'] B' → J is an isomorphism if and only if A' → B' is flat and J = I B'.

The second condition says that X = Spec B is the fibre product S ×_{S'} X', and I ⊗[A'] B' is the pullback to X of the conormal module of S ⊂ S' by Ideal.tensorEquivTensorQuot.

theorem bijective_tensorSMulHomToKer_iff (hI2 : I ^ 2 = ⊥)
    (hsurj : Function.Surjective (algebraMap B' B)) (hflat : Module.Flat (A' ⧸ I) B) :
    Function.Bijective (I.tensorSMulHomToKer B' B) ↔
      Module.Flat A' B' ∧
        (RingHom.ker (algebraMap B' B)).restrictScalars A' = I • (⊤ : Submodule A' B')

Ideal.bijective_fibreTensorSMulHomToKer_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/SquareZeroConormal.lean, line 521. The attribute's comment: “affine case, with the source the pullback of the conormal module”.

Stacks 063Y in the affine case, with the source as the pullback of the conormal module. Let I ^ 2 = 0 in A', write A = A' ⧸ I, let B be a quotient of the A'-algebra B' which is compatibly an A-algebra, and let J be the kernel of B' → B. Assume J ^ 2 = 0 and A → B flat. Then the canonical map I ⊗[A'] B → J is an isomorphism if and only if A' → B' is flat and J = I B'.

This is Ideal.bijective_tensorSMulHomToKer_iff with the source replaced by the pullback I ⊗[A'] B of the conormal module of S ⊂ S' to X, which is the module condition (2) of the source speaks about; that form needs J ^ 2 = 0, which the version with source I ⊗[A'] B' does not.

theorem bijective_fibreTensorSMulHomToKer_iff (hI2 : I ^ 2 = ⊥)
    (hJ2 : RingHom.ker (algebraMap B' B) ^ 2 = ⊥)
    (hsurj : Function.Surjective (algebraMap B' B)) (hflat : Module.Flat (A' ⧸ I) B) :
    Function.Bijective (I.fibreTensorSMulHomToKer B' B hJ2 hsurj) ↔
      Module.Flat A' B' ∧
        (RingHom.ker (algebraMap B' B)).restrictScalars A' = I • (⊤ : Submodule A' B')

Tag 06AF, a lemma

Tag 06AF in the Stacks Project.

AlgebraicGeometry.flat_of_flat_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Flatness.lean, line 750. The attribute's comment: “flatness of the upper morphism”.

Flatness of a morphism lifts from its reduction over a finite-order thickening when its source is flat over the thickened base.

public theorem flat_of_flat_reduction
    (hiX : IsThickening iX)
    (hiY : IsThickening iY)
    (hiS : IsFiniteOrderThickening iS)
    (hX : IsPullback iX pX pX' iS)
    (hY : IsPullback iY pY pY' iS)
    (hf : iX ≫ f' = f ≫ iY)
    (hfbase : f ≫ pY = pX)
    (hf'base : f' ≫ pY' = pX')
    (hflatX' : Flat pX') (hflatf : Flat f) : Flat f'

AlgebraicGeometry.flatAt_target_of_flat_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/Flatness.lean, line 766. The attribute's comment: “flatness of the upper target along the image”.

The thickened target is flat over the thickened base at every point in the image of the upper morphism.

public theorem flatAt_target_of_flat_reduction
    (hiX : IsThickening iX)
    (hiY : IsThickening iY)
    (hiS : IsFiniteOrderThickening iS)
    (hX : IsPullback iX pX pX' iS)
    (hY : IsPullback iY pY pY' iS)
    (hf : iX ≫ f' = f ≫ iY)
    (hfbase : f ≫ pY = pX)
    (hf'base : f' ≫ pY' = pX')
    (hflatX' : Flat pX') (hflatf : Flat f)
    (x' : X') : IsFlatAt pY'.toLRSHom.toShHom (f' x')

Tag 06AG, a lemma

Tag 06AG in the Stacks Project.

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.locallyOfFinitePresentation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/FinitePresentation.lean, line 353. The attribute's comment: “locally_finite_presentation”.

Local finite presentation is invariant under a cartesian finite-order deformation when the enlarged source is flat over the enlarged base.

theorem locallyOfFinitePresentation_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    LocallyOfFinitePresentation D.f ↔ LocallyOfFinitePresentation D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.locallyOfFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 70. The attribute's comment: “locally_finite_type”.

Local finite type is invariant under a cartesian finite-order deformation.

theorem locallyOfFiniteType_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    LocallyOfFiniteType D.f ↔ LocallyOfFiniteType D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.locallyQuasiFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 83. The attribute's comment: “locally_quasi_finite”.

Local quasi-finiteness is invariant under a cartesian finite-order deformation with flat enlarged source.

theorem locallyQuasiFinite_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    (LocallyOfFiniteType D.f ∧ LocallyQuasiFinite D.f) ↔
      (LocallyOfFiniteType D.f' ∧ LocallyQuasiFinite D.f')

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 108. The attribute's comment: “proper”.

Properness is invariant under a cartesian finite-order deformation.

theorem isProper_iff (d : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsProper d.f ↔ IsProper d.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isAffineHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Affine.lean, line 96. The attribute's comment: “affine”.

Stacks 06AG, affine case. Affineness is invariant under a cartesian finite-order deformation with flat ambient source.

theorem isAffineHom_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsAffineHom D.f ↔ IsAffineHom D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isIntegralHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Affine.lean, line 104. The attribute's comment: “integral”.

Stacks 06AG, integral case. Integrality is invariant under a cartesian finite-order deformation with flat ambient source: it is universal closedness together with affineness.

theorem isIntegralHom_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsIntegralHom D.f ↔ IsIntegralHom D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Affine.lean, line 115. The attribute's comment: “finite”.

Stacks 06AG, finite case. Finiteness is invariant under a cartesian finite-order deformation with flat ambient source: it is integrality together with local finite type.

theorem isFinite_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsFinite D.f ↔ IsFinite D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.etale_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Etale.lean, line 89. The attribute's comment: “etale”.

Stacks 06AG, étale case. Étaleness is invariant under a cartesian finite-order deformation with flat ambient source.

theorem CartesianFiniteOrderDeformationDiagram.etale_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) : Etale D.f ↔ Etale D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isFiniteLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FiniteLocallyFree.lean, line 84. The attribute's comment: “finite_locally_free”.

In a cartesian finite-order deformation diagram, f is finite, flat and locally of finite presentation if and only if f' is.

theorem isFiniteLocallyFree_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    (IsFinite D.f ∧ Flat D.f ∧ LocallyOfFinitePresentation D.f) ↔
      (IsFinite D.f' ∧ Flat D.f' ∧ LocallyOfFinitePresentation D.f')

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isFiniteLocallyFreeOfRank_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FiniteLocallyFree.lean, line 92. The attribute's comment: “finite_locally_free_of_rank”.

In a cartesian finite-order deformation diagram, f is finite locally free of rank d if and only if f' is.

theorem isFiniteLocallyFreeOfRank_iff (D : CartesianFiniteOrderDeformationDiagram.{u})
    (d : ℕ) :
    (IsFinite D.f ∧ Flat D.f ∧ LocallyOfFinitePresentation D.f ∧
        ∀ y : D.Y, D.f.finrank y = d) ↔
      (IsFinite D.f' ∧ Flat D.f' ∧ LocallyOfFinitePresentation D.f' ∧
        ∀ y' : D.Y', D.f'.finrank y' = d)

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.flat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Flat.lean, line 71. The attribute's comment: “flat”.

Stacks 06AG, flat case. Flatness is invariant under a cartesian finite-order deformation with flat ambient source.

theorem CartesianFiniteOrderDeformationDiagram.flat_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) : Flat D.f ↔ Flat D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isOpenImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 95. The attribute's comment: “open_immersion”.

Being an open immersion is invariant under a cartesian finite-order deformation with flat ambient source.

theorem isOpenImmersion_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsOpenImmersion D.f ↔ IsOpenImmersion D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.isIso_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 107. The attribute's comment: “isomorphism”.

Being an isomorphism is invariant under a cartesian finite-order deformation with flat ambient source.

theorem isIso_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    IsIso D.f ↔ IsIso D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 166. The attribute's comment: “monomorphism”.

Being a monomorphism is invariant under a cartesian finite-order deformation with flat ambient source.

theorem mono_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) :
    Mono D.f ↔ Mono D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.relativeDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/RelativeDimension.lean, line 65. The attribute's comment: “relative_dimension”.

Being locally of finite type of relative dimension d is invariant under a cartesian finite-order deformation with flat ambient source.

theorem relativeDimension_iff (D : CartesianFiniteOrderDeformationDiagram.{u}) (d : ℕ) :
    (∃ _ : LocallyOfFiniteType D.f, RelativeDimension D.f d) ↔
      (∃ _ : LocallyOfFiniteType D.f', RelativeDimension D.f' d)

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.smooth_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Smooth.lean, line 82. The attribute's comment: “smooth”.

Stacks 06AG, smooth case. Smoothness is invariant under a cartesian finite-order deformation with flat ambient source.

theorem CartesianFiniteOrderDeformationDiagram.smooth_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) : Smooth D.f ↔ Smooth D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.syntomic_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Syntomic.lean, line 80. The attribute's comment: “syntomic”.

Stacks 06AG, syntomic case. Syntomicity is invariant under a cartesian finite-order deformation with flat ambient source.

theorem CartesianFiniteOrderDeformationDiagram.syntomic_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) : Syntomic D.f ↔ Syntomic D.f'

Stacks.Thickenings.CartesianFiniteOrderDeformationDiagram.unramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Unramified.lean, line 87. The attribute's comment: “unramified”.

Stacks 06AG, unramified case. Unramifiedness is invariant under a cartesian finite-order deformation with flat ambient source.

theorem CartesianFiniteOrderDeformationDiagram.unramified_iff
    (D : CartesianFiniteOrderDeformationDiagram.{u}) : Unramified D.f ↔ Unramified D.f'

Declarations registered for the tag:

Stacks.Thickenings.quasiCompact_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 122 (StacksFrontier): “quasi_compact”.
Stacks.Thickenings.isSeparated_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 123 (StacksFrontier): “separated”.
Stacks.Thickenings.quasiSeparated_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 124 (StacksFrontier): “separated”.
Stacks.Thickenings.surjective_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 125 (StacksFrontier): “surjective”.
Stacks.Thickenings.universallyClosed_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 126 (StacksFrontier): “universally_closed”.
Stacks.Thickenings.universallyInjective_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 127 (StacksFrontier): “universally_injective”.
Stacks.Thickenings.universallyOpen_left_iff_right, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Deformation/Properties.lean, line 128 (StacksFrontier): “universally_open”.

Tag 0CF3, a lemma

Tag 0CF3 in the Stacks Project.

Stacks.Flatness.flat_of_flat_baseChange_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ThickeningBaseChange.lean, line 315. The attribute's comment: “flatness of the ambient morphism”.

Flatness lifts across cartesian thickenings. Let iX : X ⟶ X', iY : Y ⟶ Y' and iS : S ⟶ S' be thickenings, let f : X ⟶ Y and f' : X' ⟶ Y' be compatible morphisms over S and S', and let both X and Y be the base change of S along X' ⟶ S' and Y' ⟶ S'. If Y' ⟶ S' is locally of finite type, X' ⟶ S' is flat and locally of finite presentation and f is flat, then f' is flat.

theorem flat_of_flat_baseChange_thickening
    {X X' Y Y' S S' : Scheme.{u}}
    (iX : X ⟶ X') (iY : Y ⟶ Y') (iS : S ⟶ S')
    (f : X ⟶ Y) (f' : X' ⟶ Y')
    (gX : X ⟶ S) (gX' : X' ⟶ S')
    (gY : Y ⟶ S) (gY' : Y' ⟶ S')
    (hiX : IsThickening iX)
    (hiY : IsThickening iY)
    (hiS : IsThickening iS)
    (hcomm : f ≫ iY = iX ≫ f')
    (hover : f ≫ gY = gX)
    (hover' : f' ≫ gY' = gX')
    (hX : IsPullback iX gX gX' iS)
    (hY : IsPullback iY gY gY' iS)
    [LocallyOfFiniteType gY'] [Flat gX'] [LocallyOfFinitePresentation gX']
    (hf : Flat f) : Flat f'

Stacks.Flatness.flat_stalkMap_of_flat_baseChange_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ThickeningBaseChange.lean, line 338. The attribute's comment: “flatness of the target local ring”.

The local ring of the target is flat over the base. In the situation of Stacks Tag 0CF3, the local ring of Y' at the image of a point of X' is flat over the local ring of S'.

theorem flat_stalkMap_of_flat_baseChange_thickening
    {X X' Y Y' S S' : Scheme.{u}}
    (iX : X ⟶ X') (iY : Y ⟶ Y') (iS : S ⟶ S')
    (f : X ⟶ Y) (f' : X' ⟶ Y')
    (gX : X ⟶ S) (gX' : X' ⟶ S')
    (gY : Y ⟶ S) (gY' : Y' ⟶ S')
    (hiX : IsThickening iX)
    (hiY : IsThickening iY)
    (hiS : IsThickening iS)
    (hcomm : f ≫ iY = iX ≫ f')
    (hover : f ≫ gY = gX)
    (hover' : f' ≫ gY' = gX')
    (hX : IsPullback iX gX gX' iS)
    (hY : IsPullback iY gY gY' iS)
    [LocallyOfFiniteType gY'] [Flat gX'] [LocallyOfFinitePresentation gX']
    (hf : Flat f) (x' : X') : (gY'.stalkMap (f' x')).hom.Flat

Stacks.Flatness.essentiallyOfFinitePresentation_stalkMap_of_flat_baseChange_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/ThickeningBaseChange.lean, line 361. The attribute's comment: “essential finite presentation of the target local ring”.

The local ring of the target is essentially of finite presentation over the base. In the situation of Stacks Tag 0CF3, the local ring of Y' at the image of a point of X' is essentially of finite presentation over the local ring of S'.

theorem essentiallyOfFinitePresentation_stalkMap_of_flat_baseChange_thickening
    {X X' Y Y' S S' : Scheme.{u}}
    (iX : X ⟶ X') (iY : Y ⟶ Y') (iS : S ⟶ S')
    (f : X ⟶ Y) (f' : X' ⟶ Y')
    (gX : X ⟶ S) (gX' : X' ⟶ S')
    (gY : Y ⟶ S) (gY' : Y' ⟶ S')
    (hiX : IsThickening iX)
    (hiY : IsThickening iY)
    (hiS : IsThickening iS)
    (hcomm : f ≫ iY = iX ≫ f')
    (hover : f ≫ gY = gX)
    (hover' : f' ≫ gY' = gX')
    (hX : IsPullback iX gX gX' iS)
    (hY : IsPullback iY gY gY' iS)
    [LocallyOfFiniteType gY'] [Flat gX'] [LocallyOfFinitePresentation gX']
    (hf : Flat f) (x' : X') :
    IsEssentiallyOfFinitePresentation
      (S'.presheaf.stalk (gY' (f' x')))
      (Y'.presheaf.stalk (f' x'))
      (gY'.stalkMap (f' x')).hom

Tag 0CF4, a lemma

Tag 0CF4 in the Stacks Project.

Stacks.Thickenings.FlatDeformationDiagram.isAffineHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Affine.lean, line 127. The attribute's comment: “affine”.

Affineness is invariant under a flat deformation diagram.

theorem isAffineHom_iff (D : FlatDeformationDiagram.{u}) :
    IsAffineHom D.f ↔ IsAffineHom D.f'

Stacks.Thickenings.FlatDeformationDiagram.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Affine.lean, line 143. The attribute's comment: “finite”.

Finiteness is invariant under a flat deformation diagram: it is integrality together with local finite type, and both horizontal morphisms are locally of finite type.

theorem isFinite_iff (D : FlatDeformationDiagram.{u}) : IsFinite D.f ↔ IsFinite D.f'

Stacks.Thickenings.FlatDeformationDiagram.etale_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Etale.lean, line 74. The attribute's comment: “etale”.

Étaleness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.etale_iff (D : FlatDeformationDiagram.{u}) :
    Etale D.f ↔ Etale D.f'

Stacks.Thickenings.FlatDeformationDiagram.finiteLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FiniteLocallyFree.lean, line 133. The attribute's comment: “finite_locally_free”.

Being finite locally free, and being finite locally free of a given rank d, are each invariant under a flat deformation diagram.

theorem finiteLocallyFree_iff (D : FlatDeformationDiagram.{u}) :
    ((IsFinite D.f ∧ Flat D.f ∧ LocallyOfFinitePresentation D.f) ↔
      (IsFinite D.f' ∧ Flat D.f' ∧ LocallyOfFinitePresentation D.f')) ∧
    ∀ d : ℕ, (IsFinite D.f ∧ Flat D.f ∧ LocallyOfFinitePresentation D.f ∧
        ∀ y : D.Y, D.f.finrank y = d) ↔
      (IsFinite D.f' ∧ Flat D.f' ∧ LocallyOfFinitePresentation D.f' ∧
        ∀ y' : D.Y', D.f'.finrank y' = d)

Stacks.Thickenings.FlatDeformationDiagram.flat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Flat.lean, line 57. The attribute's comment: “flat”.

Flatness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.flat_iff (D : FlatDeformationDiagram.{u}) :
    Flat D.f ↔ Flat D.f'

Stacks.Thickenings.FlatDeformationDiagram.quasiCompact_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 60. The attribute's comment: “quasi_compact”.

Quasi-compactness is invariant under a flat deformation diagram.

theorem quasiCompact_iff : QuasiCompact D.f ↔ QuasiCompact D.f'

Stacks.Thickenings.FlatDeformationDiagram.universallyClosed_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 65. The attribute's comment: “universally_closed”.

Universal closedness is invariant under a flat deformation diagram.

theorem universallyClosed_iff : UniversallyClosed D.f ↔ UniversallyClosed D.f'

Stacks.Thickenings.FlatDeformationDiagram.separated_and_quasiSeparated_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 71. The attribute's comment: “separated”.

Separatedness and quasi-separatedness are each invariant under a flat deformation diagram.

theorem separated_and_quasiSeparated_iff :
    (IsSeparated D.f ↔ IsSeparated D.f') ∧ (QuasiSeparated D.f ↔ QuasiSeparated D.f')

Stacks.Thickenings.FlatDeformationDiagram.surjective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 78. The attribute's comment: “surjective”.

Surjectivity is invariant under a flat deformation diagram.

theorem surjective_iff : Surjective D.f ↔ Surjective D.f'

Stacks.Thickenings.FlatDeformationDiagram.universallyInjective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 83. The attribute's comment: “universally_injective”.

Universal injectivity is invariant under a flat deformation diagram.

theorem universallyInjective_iff : UniversallyInjective D.f ↔ UniversallyInjective D.f'

Stacks.Thickenings.FlatDeformationDiagram.universallyOpen_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/FromThickeningMorphism.lean, line 88. The attribute's comment: “universally_open”.

Universal openness is invariant under a flat deformation diagram.

theorem universallyOpen_iff : UniversallyOpen D.f ↔ UniversallyOpen D.f'

Stacks.Thickenings.FlatDeformationDiagram.isOpenImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 178. The attribute's comment: “open_immersion”.

Being an open immersion is invariant under a flat deformation diagram.

theorem isOpenImmersion_iff (D : FlatDeformationDiagram.{u}) :
    IsOpenImmersion D.f ↔ IsOpenImmersion D.f'

Stacks.Thickenings.FlatDeformationDiagram.isIso_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 187. The attribute's comment: “isomorphism”.

Being an isomorphism is invariant under a flat deformation diagram.

theorem isIso_iff (D : FlatDeformationDiagram.{u}) : IsIso D.f ↔ IsIso D.f'

Stacks.Thickenings.FlatDeformationDiagram.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/OpenImmersion.lean, line 194. The attribute's comment: “monomorphism”.

Being a monomorphism is invariant under a flat deformation diagram.

theorem mono_iff (D : FlatDeformationDiagram.{u}) : Mono D.f ↔ Mono D.f'

Stacks.Thickenings.FlatDeformationDiagram.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Proper.lean, line 47. The attribute's comment: “proper”.

Properness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.isProper_iff (d : FlatDeformationDiagram.{u}) :
    IsProper d.f ↔ IsProper d.f'

Stacks.Thickenings.FlatDeformationDiagram.locallyQuasiFinite_conditions_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/QuasiFinite.lean, line 46. The attribute's comment: “locally_quasi_finite”.

Local quasi-finiteness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.locallyQuasiFinite_conditions_iff
    (D : FlatDeformationDiagram.{u}) :
    (LocallyOfFiniteType D.f ∧ LocallyQuasiFinite D.f) ↔
      (LocallyOfFiniteType D.f' ∧ LocallyQuasiFinite D.f')

Stacks.Thickenings.FlatDeformationDiagram.relativeDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/RelativeDimension.lean, line 92. The attribute's comment: “relative_dimension”.

Being locally of finite type of relative dimension d is invariant under a flat deformation diagram.

theorem relativeDimension_iff (D : FlatDeformationDiagram.{u}) (d : ℕ) :
    (∃ _ : LocallyOfFiniteType D.f, RelativeDimension D.f d) ↔
      (∃ _ : LocallyOfFiniteType D.f', RelativeDimension D.f' d)

Stacks.Thickenings.FlatDeformationDiagram.smooth_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Smooth.lean, line 69. The attribute's comment: “smooth”.

Smoothness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.smooth_iff (D : FlatDeformationDiagram.{u}) :
    Smooth D.f ↔ Smooth D.f'

Stacks.Thickenings.FlatDeformationDiagram.syntomic_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Syntomic.lean, line 60. The attribute's comment: “syntomic”.

Syntomicity is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.syntomic_iff (D : FlatDeformationDiagram.{u}) :
    Syntomic D.f ↔ Syntomic D.f'

Stacks.Thickenings.FlatDeformationDiagram.unramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DeformationFiniteOrder/Unramified.lean, line 76. The attribute's comment: “unramified”.

Unramifiedness is invariant under a flat deformation diagram.

theorem FlatDeformationDiagram.unramified_iff (D : FlatDeformationDiagram.{u}) :
    Unramified D.f ↔ Unramified D.f'

Tag 0D4F, a lemma

Tag 0D4F in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveDeformation.exists_uniform_degreeBound_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveDeformation/DeformationsOfProjectiveSchemesFunctorial.lean, line 75.

Deformations of projective schemes ([Stacks, Tag 0D4F]). Let (f : X ⟶ S, ℒ) be a polarized family: f proper, flat and of finite presentation, S quasi-compact, ℒ invertible and ample relative to f. There is a positive d₀ such that for every admissible deformation (X', S', i, i', f', ℒ') of it — a cartesian square over a thickening S ⊂ S' with f' proper, flat and of finite presentation, and ℒ' invertible with ℒ ≅ (i')^* ℒ':

R^p (f')_* (ℒ')^{⊗ d} = 0 for all p > 0 and d ≥ d₀;

𝒜'_d = (f')_* (ℒ')^{⊗ d} is finite locally free for d ≥ d₀;

𝒜' = 𝒪_{S'} ⊕ ⨁_{d ≥ d₀} 𝒜'_d (truncatedSectionAlgebra) is a quasi-coherent graded 𝒪_{S'}-algebra with these pieces, its comparison 𝒜' ⟶ ⨁_{d ≥ 0} 𝒜'_d (sectionAlgebraComparison) is an isomorphism in every degree ≥ d₀, and 𝒜' is of finite presentation over every affine open of S';

the canonical morphism r' : X' ⟶ Proj_{S'}(𝒜') (canonicalProjHom) is an isomorphism over S';

the canonical map θ' : (r')^* 𝒪_{Proj_{S'}(𝒜')}(1) ⟶ ℒ' (canonicalTwistMap) is an isomorphism;

and the formation of each 𝒜'_d, d ≥ d₀, commutes with arbitrary base change.

Functoriality. For every morphism φ : D₁ ⟶ D₂ of admissible deformations (a cartesian square g' : X'₁ ⟶ X'₂ over g : S'₁ ⟶ S'₂ compatible with the immersions of the family, with polarization g'^* ℒ'₂ ≅ ℒ'₁):

𝒜' is functorial: the homomorphism of graded algebras g^* 𝒜'(D₂) ⟶ 𝒜'(D₁) obtained by pulling sections back (algebraPullbackHom) is an isomorphism in every degree;

r' is functorial: with M : Proj_{S'₁}(𝒜'(D₁)) ⟶ Proj_{S'₂}(𝒜'(D₂)) the morphism it induces followed by the base change morphism of [Stacks, Tag 01O3] (projBaseChangeHom), r'₁ ≫ M = g' ≫ r'₂;

θ' is functorial: g'^* θ'₂ followed by the polarization equals, through g'^* (r'₂)^* ≅ (r'₁ ≫ M)^* ≅ (r'₁)^* M^*, the inverse image along r'₁ of the map of Serre twists M^* 𝒪(1) ⟶ 𝒪(1) of [Stacks, Tags 01O3, 07ZJ] (projBaseChangeTwistMap) followed by θ'₁.

public theorem exists_uniform_degreeBound_functorial (P : PolarizedFamily.{u}) :
    ∃ (d₀ : ℕ) (hd₀ : 0 < d₀), (∀ D : P.AdmissibleDeformation,
      (∀ d : ℕ, d₀ ≤ d → ∀ p : ℤ, 0 < p →
          IsZero (((Scheme.Modules.pushforward D.f').rightDerivedPlus p).obj
            (tensorPowModule D.X' D.L' (d : ℤ)))) ∧
        (∀ d : ℕ, d₀ ≤ d →
          _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
            (R := D.S'.ringCatSheaf) (D.sectionPiece d)) ∧
        (D.IsTruncatedSectionAlgebraWithComparison d₀ (D.truncatedSectionAlgebra d₀ hd₀) ∧
          (∀ d : ℕ, d₀ ≤ d → IsIso ((D.sectionAlgebraComparison d₀ hd₀).app (d : ℤ))) ∧
          (∀ U : D.S'.Opens, IsAffineOpen U →
            RingHom.FinitePresentation ((D.truncatedSectionAlgebra d₀ hd₀).strHom U))) ∧
        (IsIso (D.canonicalProjHom d₀ hd₀) ∧
          D.canonicalProjHom d₀ hd₀ ≫ (relativeProj (D.truncatedSectionAlgebra d₀ hd₀)).toBase =
            D.f') ∧
        IsIso (D.canonicalTwistMap d₀ hd₀) ∧
        ∀ d : ℕ, d₀ ≤ d → ∀ (T Y : Scheme.{u}) (h : T ⟶ D.S') (fT : Y ⟶ T) (h' : Y ⟶ D.X')
          (hsq : IsPullback h' fT D.f' h),
          IsIso ((Stacks.AlgebraicGeometry.AffinePushforward.baseChangeNatTrans hsq.w).app
            (tensorPowModule D.X' D.L' (d : ℤ)))) ∧
      ∀ (D₁ D₂ : P.AdmissibleDeformation) (φ : Hom D₁ D₂),
        ∃ hiso : ∀ n : ℤ, IsIso ((algebraPullbackHom φ d₀ hd₀).app n),
          D₁.canonicalProjHom d₀ hd₀ ≫ projBaseChangeHom φ d₀ hd₀ hiso =
            φ.total ≫ D₂.canonicalProjHom d₀ hd₀ ∧
          (Scheme.Modules.pullback φ.total).map (D₂.canonicalTwistMap d₀ hd₀) ≫
              φ.polarization.hom =
            (Scheme.Modules.pullbackComp φ.total (D₂.canonicalProjHom d₀ hd₀)).hom.app _ ≫
              (Scheme.Modules.pullbackCongr
                (canonicalProjHom_comp_projBaseChangeHom φ d₀ hd₀ hiso).symm).hom.app _ ≫
              (Scheme.Modules.pullbackComp (D₁.canonicalProjHom d₀ hd₀)
                (projBaseChangeHom φ d₀ hd₀ hiso)).inv.app _ ≫
              (Scheme.Modules.pullback (D₁.canonicalProjHom d₀ hd₀)).map
                (projBaseChangeTwistMap φ d₀ hd₀ hiso) ≫
              D₁.canonicalTwistMap d₀ hd₀

Sources

LeanStacks.Thickenings.flat_and_isPullback_of_isIso_firstOrderThickeningConormalSheafMap · Stacks.Thickenings.flat_and_isPullback_iff_isIso_firstOrderThickeningConormalSheafMap · Stacks.Thickenings.epi_firstOrderThickeningConormalSheafMap · Stacks.Thickenings.isIso_firstOrderThickeningConormalSheafMap · Ideal.bijective_tensorSMulHomToKer_iff · Ideal.bijective_fibreTensorSMulHomToKer_iff · AlgebraicGeometry.flat_of_flat_reduction · AlgebraicGeometry.flatAt_target_of_flat_reduction

Section37.11 Formally smooth morphisms #

Section 37.11 of the Stacks Project, Tag 02GZ. 13 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02H0, a definition

Tag 02H0 in the Stacks Project.

Stacks.Smooth.FormallySmoothScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/FormallySmoothScheme.lean, line 103. References: EGA IV (17.1.1); SGA 3 XVII (5.7.1).

A morphism of schemes f : X ⟶ S is formally smooth when it has the infinitesimal lifting property: for every first-order thickening i : T ⟶ T' of affine schemes, every commutative square
T  --g--→ X
|         |
i         f
↓         ↓
T' --h--→ S
has a diagonal filler g' : T' ⟶ X, that is a morphism with g' ≫ f = h and i ≫ g' = g.

abbrev FormallySmoothScheme {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 02H1, a lemma

Tag 02H1 in the Stacks Project.

AlgebraicGeometry.FormallySmooth.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/Basic.lean, line 60.

A composition of formally smooth morphisms is formally smooth.

theorem FormallySmooth.comp {X Y S : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ S}
    (hf : FormallySmooth f) (hg : FormallySmooth g) :
    FormallySmooth (f ≫ g)

Tag 02H2, a lemma

Tag 02H2 in the Stacks Project.

AlgebraicGeometry.FormallySmooth.pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/Basic.lean, line 70.

An arbitrary base change of a formally smooth morphism is formally smooth.

theorem FormallySmooth.pullback_snd {X S S' : Scheme.{u}} (f : X ⟶ S)
    (g : S' ⟶ S) (hf : FormallySmooth f) :
    FormallySmooth (pullback.snd f g)

Tag 02HH, a lemma

Tag 02HH in the Stacks Project.

AlgebraicGeometry.formallyEtale_iff_formallySmooth_and_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FormallyEtaleSmoothUnramified.lean, line 46. References: EGA IV (17.1.1), “étale ⟺ smooth+unram”.

A morphism of schemes is formally étale if and only if it is formally smooth and formally unramified.

theorem formallyEtale_iff_formallySmooth_and_formallyUnramified
    {X S : Scheme.{u}} (f : X ⟶ S) :
    FormallyEtale f ↔ (FormallySmooth f ∧ FormallyUnramified f)

Tag 02H3, a lemma

Tag 02H3 in the Stacks Project.

AlgebraicGeometry.FormallySmooth.resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/Basic.lean, line 82.

Formal smoothness is preserved by restriction to compatible open subschemes.

theorem FormallySmooth.resLE {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : FormallySmooth f) (U : X.Opens) (V : S.Opens)
    (hUV : U ≤ f ⁻¹ᵁ V) :
    FormallySmooth (f.resLE V U hUV)

Stacks.Smooth.FormallySmooth.resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/FormallySmoothCriterion.lean, line 208.

Stacks Project, Tag 02H3. Formal smoothness passes to the restriction of a morphism to opens of the source and of the target. The point is that a first-order thickening of affine schemes is surjective on points, so a lift over the ambient morphism has the same image as the morphism it extends and therefore factors through the given open of the source.

theorem FormallySmooth.resLE {X S : Scheme.{u}} {f : X ⟶ S} (hf : FormallySmooth f)
    {U : S.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U) : FormallySmooth (f.resLE U V e)

Tag 02H4, a lemma

Tag 02H4 in the Stacks Project.

AlgebraicGeometry.formallySmooth_iff_appTop_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/Basic.lean, line 92.

A morphism of affine schemes is formally smooth if and only if its map on global sections is formally smooth.

theorem formallySmooth_iff_appTop_formallySmooth
    {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S) :
    FormallySmooth f ↔ f.appTop.hom.FormallySmooth

Tag 02H6, a lemma

Tag 02H6 in the Stacks Project.

Stacks.Smooth.smooth_iff_locallyOfFinitePresentation_and_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/SmoothFormallySmoothTag.lean, line 684. References: EGA IV (17.3.2), “(ii) smooth”; EGA 0 (19.0.1); EGA IV (17.3.1); SGA 3 XI (1.1); SGA 3 XV (1.1), “more general”.

A scheme morphism is smooth exactly when it is locally of finite presentation and formally smooth. This is the infinitesimal lifting criterion for smoothness.

The implication from the right is Stacks.Smooth.smooth_of_formallySmoothScheme, and the implication to the right is Stacks.Smooth.formallySmoothScheme_of_smooth together with the fact that a smooth morphism is locally of finite presentation.

theorem smooth_iff_locallyOfFinitePresentation_and_formallySmooth {X S : Scheme.{u}}
    (f : X ⟶ S) :
    AlgebraicGeometry.Smooth f ↔
      (AlgebraicGeometry.LocallyOfFinitePresentation f ∧ FormallySmoothScheme f)

Tag 06B5, a lemma

Tag 06B5 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. 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)

Tag 0D0E, a lemma

Tag 0D0E in the Stacks Project.

Stacks.Cohomology.Affine.isZero_firstCohomology_sheafHom_of_isLocallyProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineCohomologyVanishing/InternalHom.lean, line 168.

The first cohomology of an internal hom out of a locally projective module on an affine scheme vanishes. The source is a retract of a free module, so the internal hom is a retract of the internal hom out of that free module, which is a product of copies of the target; the first cohomology of that product vanishes because the first cohomology of a quasi-coherent module on an affine scheme does.

theorem isZero_firstCohomology_sheafHom_of_isLocallyProjective (T : Scheme.{u}) [IsAffine T]
    (F G : T.Modules) [F.IsQuasicoherent] [G.IsQuasicoherent] (H : SheafHom T.sheaf F G)
    (hF : Scheme.Modules.IsLocallyProjective F) :
    IsZero (Hgroup T.ringCatSheaf ⊤ 1 H.obj)

Tag 0D0F, a lemma

Tag 0D0F in the Stacks Project.

Stacks.Smooth.formallySmooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/FormallySmoothTFAE.lean, line 833. The attribute's comment: “all four criteria, for an arbitrary morphism of schemes”.

[Stacks Project, Tag 0D0F]. For a morphism of schemes f : X ⟶ Y the following are equivalent: f is formally smooth; f is formally smooth on a neighbourhood of every point of X; the ring map Γ(Y, V) ⟶ Γ(X, U) is formally smooth for every pair of affine opens with f(U) ⊆ V; and there is one affine open covering of Y together with, over each of its members, an affine open covering of its inverse image, on whose charts those ring maps are formally smooth.

The implications 1 → 3, 1 → 2, 3 → 4, 4 → 2 and 2 → 3 are the formal manipulations of [Stacks Project, Tag 02H3] and the affine criterion [Stacks Project, Tag 02H4] together with the affine-locality of formal smoothness of ring maps. The remaining implication 3 → 1 is Stacks.Smooth.formallySmooth_of_formallySmooth_appLE, the torsor argument of the source, whose pseudo-torsor is Stacks.Smooth.isLiftPseudoTorsor.

theorem formallySmooth_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
    List.TFAE
      [AlgebraicGeometry.FormallySmooth f,
        ∀ x : X, ∃ (U : X.Opens) (V : Y.Opens), x ∈ U ∧ f.base x ∈ V ∧
          ∃ hUV : U ≤ f ⁻¹ᵁ V, AlgebraicGeometry.FormallySmooth (f.resLE V U hUV),
        ∀ U : X.Opens, IsAffineOpen U → ∀ V : Y.Opens, IsAffineOpen V →
          ∀ hUV : U ≤ f ⁻¹ᵁ V, (f.appLE V U hUV).hom.FormallySmooth,
        ∃ (J : Type u) (V : J → Y.Opens), IsOpenCover V ∧ (∀ j, IsAffineOpen (V j)) ∧
          ∀ j, ∃ (I : Type u) (U : I → X.Opens) (hU : (⨆ i, U i) = f ⁻¹ᵁ V j),
            (∀ i, IsAffineOpen (U i)) ∧
              ∀ i, (f.appLE (V j) (U i) ((le_iSup U i).trans hU.le)).hom.FormallySmooth]

Tag 06B6, a lemma

Tag 06B6 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.toRelativeDifferentials_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/FormallySmooth.lean, line 318. References: EGA IV (17.2.3).

For morphisms of schemes f : X ⟶ Y and g : Y ⟶ S with f formally smooth, the canonical sequence 0 ⟶ f^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} ⟶ 0 of 𝒪_X-modules is short exact. The case of a smooth f is the special case obtained from Stacks.Smooth.smooth_iff_locallyOfFinitePresentation_and_formallySmooth.

theorem toRelativeDifferentials_shortExact (f : X ⟶ Y) (g : Y ⟶ S) (hf : FormallySmooth f) :
    ∃ h : relativeDifferentialsMap f g (f ≫ g) (𝟙 S) (Category.comp_id (f ≫ g)).symm ≫
        f.toRelativeDifferentials g = 0,
      (ShortComplex.mk _ _ h).ShortExact

Tag 06B7, a lemma

Tag 06B7 in the Stacks Project.

Stacks.UnramifiedConormalSequence.exists_localRetraction_of_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/UnramifiedConormalSequence.lean, line 145. The attribute's comment: “the step of the proof using formal smoothness of Z over S: locally on the universal first-order thickening Z' there is a left inverse Z' ⟶ Z over S”.

A local left inverse Z' ⟶ Z over S, from formal smoothness of Z over S. Let i : Z ⟶ Z' with structure morphism h' : Z' ⟶ X be a universal first-order thickening of h : Z ⟶ X, let p : X ⟶ S, and assume Z is formally smooth over S, that is h ≫ p : Z ⟶ S has the lifting property of [Stacks, Tag 02H0]. Then every point z of Z has an open neighbourhood V and an open W ⊆ Z' such that i restricts to j : V ⟶ W and j admits a left inverse g : W ⟶ V over S.

This is the step of the proof of [Stacks, Tag 06B7] reading "by formal smoothness of Z over S there exists, after replacing Z' by an open neighbourhood, a left inverse Z' ⟶ Z over S". V is any affine open neighbourhood of z and W is the open of Z' attached to it by Stacks.Thickenings.UniversalFirstOrderThickening.ambientOpens, which is affine because V ⟶ W is a first-order thickening of V; the lifting property applies to that affine first-order thickening, and the resulting lift W ⟶ Z factors through V because V ⟶ W is surjective on points.

theorem exists_localRetraction_of_formallySmooth {Z' : Scheme.{u}} {h : Z ⟶ X} {i : Z ⟶ Z'}
    {h' : Z' ⟶ X} (hi : Stacks.Thickenings.IsUniversalFirstOrderThickening h i h') (p : X ⟶ S)
    (hZ : FormallySmooth (h ≫ p)) (z : Z) :
    ∃ (V : Z.Opens) (W : Z'.Opens) (j : V.toScheme ⟶ W.toScheme)
      (g : W.toScheme ⟶ V.toScheme), z ∈ V ∧ V.ι ≫ i = j ≫ W.ι ∧
        j ≫ g = 𝟙 V.toScheme ∧ g ≫ (V.ι ≫ (h ≫ p)) = W.ι ≫ (h' ≫ p)

Stacks.UnramifiedConormalSequence.forall_exists_isSplitEpi_restrict_relativeDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/UnramifiedConormalSequence.lean, line 251. The attribute's comment: “the conclusion of the source's proof before Tag 0474 is invoked: the sequence is locally split, i.e. the second arrow h^*Ω_{X/S} ⟶ Ω_{Z/S} restricts to a split epimorphism on a neighbourhood of every point of Z. Left exactness, the assertion of the tag, is not this declaration: it is conormalShortComplex_shortExact of StacksFrontier.AlgebraicGeometry.MoreMorphisms.FormallySmooth.UnramifiedConormalShortExact”.

[Stacks, Tag 06B7]: the conormal sequence of a formally unramified morphism with formally smooth source is locally split. Let h : Z ⟶ X be formally unramified, let p : X ⟶ S, and assume Z is formally smooth over S. Then the second arrow h^*Ω_{X/S} ⟶ Ω_{Z/S} of the sequence of [Stacks, Tag 04FC] — the canonical map of [Stacks, Tag 01UV] — restricts to a split epimorphism on a neighbourhood of every point of Z.

A split epimorphism being an epimorphism, this contains local surjectivity of that arrow, which [Stacks, Tag 01UZ] supplies only for a morphism surjective on stalks; splitness is what formal smoothness buys, and it is the source's "hence the sequence is locally split". Left exactness of the sequence, which is the assertion of the tag, is not proved here; it is Stacks.UnramifiedConormalSequence.conormalShortComplex_shortExact in StacksFrontier.AlgebraicGeometry.MoreMorphisms.FormallySmooth.UnramifiedConormalShortExact.

theorem forall_exists_isSplitEpi_restrict_relativeDifferentialsMap (h : Z ⟶ X)
    [FormallyUnramified h] (p : X ⟶ S) (hZ : FormallySmooth (h ≫ p)) (z : Z) :
    ∃ V : Z.Opens, z ∈ V ∧ IsSplitEpi ((Scheme.Modules.pullback V.ι).map
      (relativeDifferentialsMap h p (h ≫ p) (𝟙 S)
        (show h ≫ p = (h ≫ p) ≫ 𝟙 S by simp)))

Stacks.UnramifiedConormalSequence.conormalShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FormallySmooth/UnramifiedConormalShortExact.lean, line 318. References: EGA IV (17.2.5), “more general”; SGA 7 XI (1.3), “partial”; SGA 7 XVII (5.1), “more general”.

Let h : Z ⟶ X be a formally unramified morphism of schemes over p : X ⟶ S and assume Z is formally smooth over S. Then the canonical sequence
0 ⟶ 𝒞_{Z/X} ⟶ h^*Ω_{X/S} ⟶ Ω_{Z/S} ⟶ 0
is short exact: the first arrow is a monomorphism, the sequence is exact at h^*Ω_{X/S}, and the second arrow is an epimorphism. Here 𝒞_{Z/X} is the conormal sheaf of the inclusion of Z into the universal first-order thickening of Z over X.

theorem conormalShortComplex_shortExact
    (hZ : AlgebraicGeometry.FormallySmooth (h ≫ p)) :
    (conormalShortComplex h p).ShortExact

Tag 067W, a lemma

Tag 067W in the Stacks Project.

Stacks.ConormalSequenceUnramifiedPair.exists_retraction_restrict_universalConormalTransitivityMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 360. The attribute's comment: “locally split, in the sense the source's proof produces and its final sentence defines: every point of Z has an open neighbourhood over which the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of Tag 067V admits a retraction”.

[Stacks, Tag 067W]: the conormal sequence is locally split. For formally unramified i : Z ⟶ X and j : Z ⟶ Y in a commutative triangle i ≫ p = j with p formally smooth, every point of Z has an open neighbourhood V over which the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of [Stacks, Tag 067V] admits a retraction.

theorem exists_retraction_restrict_universalConormalTransitivityMap (h : i ≫ p = j)
    (hp : FormallySmooth p) (z : Z) :
    ∃ V : Z.Opens, z ∈ V ∧
      ∃ r : (Scheme.Modules.restrictFunctor V.ι).obj (universalConormalSheaf i) ⟶
          (Scheme.Modules.restrictFunctor V.ι).obj (universalConormalSheaf j),
        (Scheme.Modules.restrictFunctor V.ι).map (universalConormalTransitivityMap i j p h) ≫ r =
          𝟙 _

Stacks.ConormalSequenceUnramifiedPair.mono_conormalSequenceFirstArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 462. The attribute's comment: “exact on the left: the first arrow 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} of Tag 067V is a monomorphism, which is the only strengthening of Tag 067V's right-exact sequence to a short exact one that this tag asserts; obtained from the local splitting”.

[Stacks, Tag 067W]: the first arrow of the conormal sequence is a monomorphism. This is the 0 ⟶ at the left-hand end of the sequence, and the only strengthening of the right-exact sequence of [Stacks, Tag 067V] to a short exact one.

theorem mono_conormalSequenceFirstArrow (h : i ≫ p = j) (hp : FormallySmooth p) :
    Mono (conormalSequenceFirstArrow i j p h)

Stacks.ConormalSequenceUnramifiedPair.exists_retraction_restrict_conormalSequenceFirstArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 478. The attribute's comment: “locally split, in the shape of the locallySplit clause the library uses for the sibling tag 062S”.

The local splitting, stated for Stacks.ConormalSequenceUnramifiedPair.conormalSequenceFirstArrow. This is the locallySplit clause in the shape the library uses for the sibling tag [Stacks, Tag 062S], namely Stacks.AlgebraicGeometry.IsSplitExactConormalSequence.locallySplit.

theorem exists_retraction_restrict_conormalSequenceFirstArrow (h : i ≫ p = j)
    (hp : FormallySmooth p) (z : Z) :
    ∃ V : Z.Opens, z ∈ V ∧
      ∃ r : (Scheme.Modules.restrictFunctor V.ι).obj (conormalSheafModules i) ⟶
          (Scheme.Modules.restrictFunctor V.ι).obj (conormalSheafModules j),
        (Scheme.Modules.restrictFunctor V.ι).map (conormalSequenceFirstArrow i j p h) ≫ r =
          𝟙 _

Stacks.ConormalSequenceUnramifiedPair.shortExact_of_comp_eq_zero_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Thickenings/UnramifiedPairSplitConormalSequence.lean, line 1130. The attribute's comment: “the sequence of Tag 067V is short exact: exactness at the middle term and surjectivity of the second arrow are the assertions of Tag 067V, and injectivity of the first arrow is what this tag adds, by way of the local splitting its proof produces”.

[Stacks, Tag 067W]: the conormal sequence is short exact. For formally unramified i : Z ⟶ X and j : Z ⟶ Y in a commutative triangle i ≫ p = j with p formally smooth, the sequence 0 ⟶ 𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} ⟶ 0 of [Stacks, Tag 067V] is short exact.

Exactness at the middle term and surjectivity of the second arrow are the assertions of [Stacks, Tag 067V]; what this tag adds is injectivity of the first arrow.

theorem shortExact_of_comp_eq_zero_of_exact (h : i ≫ p = j) (hp : FormallySmooth p) :
    (ShortComplex.mk _ _ (conormalSequenceComp_eq_zero i j p h)).ShortExact

Sources

LeanStacks.Smooth.FormallySmoothScheme · AlgebraicGeometry.FormallySmooth.comp · AlgebraicGeometry.FormallySmooth.pullback_snd · AlgebraicGeometry.formallyEtale_iff_formallySmooth_and_formallyUnramified · AlgebraicGeometry.FormallySmooth.resLE · Stacks.Smooth.FormallySmooth.resLE · AlgebraicGeometry.formallySmooth_iff_appTop_formallySmooth · Stacks.Smooth.smooth_iff_locallyOfFinitePresentation_and_formallySmooth

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

37.2 Thickenings to 37.11 Formally smooth morphisms

Section37.2 Thickenings#

Tag 04EX, a definition

Tag 05YV, a lemma

Tag 06AD, a lemma

Tag 09ZU, a lemma

Tag 0BPE, a lemma

Tag 0BPF, a lemma

Sources

Section37.3 Morphisms of thickenings#

Tag 09ZV, a lemma

Tag 0D2R, a lemma

Tag 09ZW, a lemma

Tag 0BPG, a lemma

Sources

Section37.4 Picard groups of thickenings#

Tag 0C6R, a lemma

Tag 0C6S, a lemma

Sources

Section37.5 Infinitesimal neighbourhoods#

Tag 04EY, a definition

Tag 04EZ, a lemma

Tag 04F0, a lemma

Sources

Section37.6 Formally unramified morphisms#

Tag 02H8, a definition

Tag 02HA, a lemma

Tag 02HB, a lemma

Tag 02HC, a lemma

Tag 02HD, a lemma

Tag 02H9, a lemma

Tag 02HE, a lemma

Sources

Section37.7 Universal first order thickenings#

Tag 04F3, a lemma

Tag 04F4, a definition

Tag 04F5, a lemma

Tag 04F6, a lemma

Tag 04F7, a lemma

Tag 04F8, a lemma

Tag 04F9, a lemma

Tag 04FA, a lemma

Tag 04FB, a lemma

Tag 04FC, a lemma

Tag 067V, a lemma

Tag 06AE, a lemma

Sources

Section37.8 Formally étale morphisms#

Tag 02HG, a definition

Tag 04FD, a lemma

Tag 02HI, a lemma

Tag 02HJ, a lemma

Tag 02HK, a lemma

Tag 04FE, a lemma

Tag 04FF, a lemma

Tag 02HL, a lemma

Tag 02HM, a lemma

Sources

Section37.9 Infinitesimal deformations of maps#

Tag 04FG, a lemma

Tag 04BV, an equation

Tag 02H5, a lemma

Tag 0CK1, a remark

Tag 04FH, a lemma

Tag 04FI, an equation

Tag 04FJ, a lemma

Tag 04FK, a remark

Tag 0CK2, a remark

Tag 04FL, a lemma

Tag 04BX, a lemma

Tag 04BY, a lemma

Tag 04BZ, a remark

Sources

Section37.10 Infinitesimal deformations of schemes#

Tag 063Y, a lemma

Tag 06AF, a lemma

Tag 06AG, a lemma

Tag 0CF3, a lemma

Tag 0CF4, a lemma

Tag 0D4F, a lemma

Section37.2 Thickenings #

Section37.3 Morphisms of thickenings #

Section37.4 Picard groups of thickenings #

Section37.5 Infinitesimal neighbourhoods #

Section37.6 Formally unramified morphisms #

Section37.7 Universal first order thickenings #

Section37.8 Formally étale morphisms #

Section37.9 Infinitesimal deformations of maps #

Section37.10 Infinitesimal deformations of schemes #

Section37.11 Formally smooth morphisms #