76.15 Universal first order… to 76.18 Infinitesimal…

Section76.15 Universal first order thickenings#

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

Tag 0602, an equation

Tag 0602 in the Stacks Project.

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Universal.lean, line 67.

Stacks 0602. A first-order thickening Z ⊂ Z' of algebraic spaces over S, equipped with a morphism p : Z' ⟶ X, is a universal first-order thickening of Z over X when every compatible solid diagram built from a first-order thickening T ⊂ T' over X admits a unique morphism T' ⟶ Z' restricting to the given T ⟶ Z and lying over X.

structure IsUniversalFirstOrderThickening (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Z' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.1)
    (p : Z' ⟶ X) : Prop

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening', a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickening.lean, line 223. The attribute's comment: “the universal first-order thickening property of diagram (0602)”.

Stacks 0602. A first-order thickening Z ⊆ Z' over X, with structure morphism p : Z' ⟶ X, is universal when for every solid diagram of Stacks 0602 — a first-order thickening T ⊆ T' of algebraic spaces, a morphism a : T ⟶ Z and a morphism b : T' ⟶ X such that T ⟶ T' ⟶ X agrees with T ⟶ Z ⊆ Z' ⟶ X — there is a unique dotted arrow T' ⟶ Z' whose restriction to T is a and which lies over X.

structure IsUniversalFirstOrderThickening' {X Z' : AlgebraicSpaces B S hS}
    (Z : Subfunctor Z'.1) (p : Z' ⟶ X) : Prop

Tag 0603, a lemma

Tag 0603 in the Stacks Project.

AlgebraicGeometry.Space.isUniversalFirstOrderThickening_iff_affine_lifting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalCriteria.lean, line 553. The attribute's comment: “equivalence of (1) and (3)”.

Stacks 0603, the equivalence of (1) and (3). The universal property of a first-order thickening of algebraic spaces can already be checked on the diagrams of Stacks 0602 whose ambient test space is an affine scheme.

theorem isUniversalFirstOrderThickening_iff_affine_lifting
    {X Z' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.1) (p : Z' ⟶ X)
    (hZ : IsFirstOrderThickening B S hS Z' Z) :
    IsUniversalFirstOrderThickening B S hS Z p ↔
      ∀ {T' : AlgebraicSpaces B S hS} (_hT' : IsAffineSpace B S hS T'.1)
        (T : Subfunctor T'.1),
        IsFirstOrderThickening B S hS T' T →
        ∀ (a : T.toFunctor ⟶ Z.toFunctor) (b : T'.1 ⟶ X.1),
          T.ι ≫ b = a ≫ Z.ι ≫ p.hom →
          ∃! c : T'.1 ⟶ Z'.1, (T.ι ≫ c = a ≫ Z.ι) ∧ (c ≫ p.hom = b)

AlgebraicGeometry.Space.HasRepresentableLiftingProperty, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickeningCriteria.lean, line 144. The attribute's comment: “part (2), the lifting property tested on schemes”.

The lifting property of the diagrams of Stacks 0602 whose ambient test object T' is a scheme, that is, whose underlying presheaf is representable.

def HasRepresentableLiftingProperty : Prop

AlgebraicGeometry.Space.HasAffineLiftingProperty, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickeningCriteria.lean, line 154. The attribute's comment: “part (3), the lifting property tested on affine schemes”.

The lifting property of the diagrams of Stacks 0602 whose ambient test object T' is an affine scheme.

def HasAffineLiftingProperty : Prop

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

A first-order thickening Z ⊂ Z' of algebraic spaces over X is a universal first-order thickening if and only if the dotted arrow of the diagram of Stacks 0602 exists and is unique for every test thickening T ⊂ T' whose ambient space T' is a scheme.

theorem isUniversalFirstOrderThickening_iff_representable
    (hZ : IsFirstOrderThickening B S hS Z' Z) :
    IsUniversalFirstOrderThickening B S hS Z p ↔
      HasRepresentableLiftingProperty B S hS Z p

AlgebraicGeometry.Space.HasRepresentableLiftingProperty.hasAffineLiftingProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickeningCriteria.lean, line 365. The attribute's comment: “(2) implies (3)”.

The lifting property of the diagrams of Stacks 0602 tested on schemes implies the same property tested on affine schemes.

theorem HasRepresentableLiftingProperty.hasAffineLiftingProperty
    (h : HasRepresentableLiftingProperty B S hS Z p) :
    HasAffineLiftingProperty B S hS Z p

Tag 0604, a lemma

Tag 0604 in the Stacks Project.

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.comp_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FormallyEtale.lean, line 436.

Stacks 0604. A universal first-order thickening of Z over an algebraic space Y is also a universal first-order thickening of Z over an algebraic space X whenever Y ⟶ X is formally étale: the structure morphism of the thickening is composed with the formally étale morphism, and nothing else changes.

A solid diagram over X is first pushed through the formally étale morphism, which by Stacks 0611 has a unique lift against the thickening T ⊂ T'; that lift turns the diagram into a solid diagram over Y, where universality over Y applies. Uniqueness over X follows because any competing extension produces, after composition with the structure morphism, a lift of the pushed diagram, which the uniqueness clause of Stacks 0611 identifies with the chosen one.

theorem IsUniversalFirstOrderThickening.comp_formallyEtale {Z' Y X : AlgebraicSpaces B S hS}
    (Z : Subfunctor Z'.obj) (p : Z' ⟶ Y) (q : Y ⟶ X)
    (hp : IsUniversalFirstOrderThickening B S hS Z p) (hq : FormallyEtale q.hom) :
    IsUniversalFirstOrderThickening B S hS Z (p ≫ q)

Tag 0605, a lemma

Tag 0605 in the Stacks Project.

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.etalePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickeningDescent.lean, line 184. The attribute's comment: “part (1)”.

Stacks 0605, part (1). Let Y ⊂ Y' be a universal first-order thickening of Y over an algebraic space X, with structure morphism p : Y' ⟶ X. Let g : Z' ⟶ Y' be étale and let Z ⊂ Z' be a closed subspace whose inclusion sits in a cartesian square over the inclusion of Y, so that Z = Y ×_{Y'} Z'. Then Z ⊂ Z' is a universal first-order thickening of Z over X, with structure morphism g ≫ p.

The morphism Z ⟶ Y of the source appears as the top edge a of the cartesian square; it is automatically étale, being a base change of g. The source produces Z' ⟶ Y' from the topological invariance of the spaces-étale site; here it is given, so no such input is needed.

theorem IsUniversalFirstOrderThickening.etalePullback {X Y' Z' : AlgebraicSpaces B S hS}
    (Y : Subfunctor Y'.obj) (p : Y' ⟶ X)
    (hY : IsUniversalFirstOrderThickening B S hS Y p)
    (g : Z' ⟶ Y') (hg : IsEtale B S hS g.hom)
    (Z : Subfunctor Z'.obj) (a : Z.toFunctor ⟶ Y.toFunctor)
    (hsq : IsPullback a Z.ι Y.ι g.hom) :
    IsUniversalFirstOrderThickening B S hS Z (g ≫ p)

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

Stacks 0605, part (2). Let Z ⟶ Y ⟶ X be morphisms of algebraic spaces over S with a₀ : Z ⟶ Y surjective étale, let g : Z' ⟶ Y' be an étale morphism of first-order thickenings over X extending a₀, and let Z ⊂ Z' be a universal first-order thickening of Z over X. Then Y ⊂ Y' is a universal first-order thickening of Y over X.

theorem IsUniversalFirstOrderThickening.of_surjectiveEtale
    {X Y' Z' : AlgebraicSpaces B S hS} (Y : Subfunctor Y'.obj) (Z : Subfunctor Z'.obj)
    (p : Y' ⟶ X) (g : Z' ⟶ Y') (hg : IsEtale B S hS g.hom)
    (hY : IsFirstOrderThickening B S hS Y' Y)
    (a₀ : Z.toFunctor ⟶ Y.toFunctor) (hcompat : a₀ ≫ Y.ι = Z.ι ≫ g.hom)
    (ha₀ : IsEtale B S hS a₀) (hsurj : IsSurjective B S hS a₀)
    (hZ : IsUniversalFirstOrderThickening B S hS Z (g ≫ p)) :
    IsUniversalFirstOrderThickening B S hS Y p

Tag 0606, a lemma

Tag 0606 in the Stacks Project.

AlgebraicGeometry.Space.nonempty_universalFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalExistence/ExistenceAndTransport.lean, line 348.

Stacks 0606. Every formally unramified morphism h : Z ⟶ X of algebraic spaces over S admits a universal first order thickening Z ⊂ Z' of Z over X, in the sense of Stacks 0602.

theorem nonempty_universalFirstOrderThickening
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Z X : AlgebraicGeometry.AlgebraicSpaces B S hS} (h : Z ⟶ X)
    (hh : FormallyUnramified h.hom) :
    Nonempty (UniversalFirstOrderThickening B S hS h)

Tag 0607, a definition

Tag 0607 in the Stacks Project.

AlgebraicGeometry.Space.UniversalFirstOrderThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningOfFormallyUnramified.lean, line 312. The attribute's comment: “the universal first order thickening”.

Stacks 0607, part (1). A universal first order thickening of a formally unramified morphism h : Z ⟶ X of algebraic spaces over S: the thickening Z ⊂ Z' of Z over X whose existence is Stacks 0606, presented as the datum it consists of.

The ambient algebraic space is ambient, written Z' in the source, with structure morphism toBase : Z' ⟶ X; the smaller space is the closed subspace sub of Z', which sourceIso identifies with Z compatibly with h; and isUniversal is the universal property of Stacks 0602 for that thickening over X.

Stacks 0606, the existence of such a datum for every formally unramified h, is AlgebraicGeometry.Space.nonempty_universalFirstOrderThickening; it concludes Nonempty of this structure, so the datum is taken as given rather than chosen out of an existence statement, and the uniqueness clause of isUniversal is what licenses the source's definite article.

structure UniversalFirstOrderThickening {Z X : AlgebraicSpaces B S hS} (h : Z ⟶ X)

AlgebraicGeometry.Space.conormalSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningOfFormallyUnramified.lean, line 364. The attribute's comment: “the conormal sheaf”.

Stacks 0607, part (2). The conormal sheaf 𝒞_{Z/X} of a formally unramified morphism h : Z ⟶ X of algebraic spaces over S, relative to a universal first order thickening Z ⊂ Z' of Z over X: the conormal module of Stacks 04CN of the closed subspace Z ⊂ Z', transported to Z along the identification of Z with that closed subspace.

The source writes this 𝒞_{Z/X}, the same symbol Stacks 04CN uses for the conormal sheaf of an immersion, which in this library is AlgebraicGeometry.Space.conormalModule; no notation is declared, following the convention of StacksFrontier/AlgebraicGeometry/Spaces/ConormalModule.lean.

noncomputable def conormalSheaf {Z X : AlgebraicSpaces B S hS} {h : Z ⟶ X}
    (t : UniversalFirstOrderThickening B S hS h) :
    Modules.{u, u} B S hS Z.obj Z.property

Tag 0608, a lemma

Tag 0608 in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Immersion.lean, line 90. The attribute's comment: “formally unramified”.

The first clause of [Stacks Project, Tag 0608]. An immersion of algebraic spaces over S is formally unramified.

An immersion is a representable morphism whose every represented base change is an immersion of schemes, hence unramified by AlgebraicGeometry.unramified_of_isImmersion; a representable unramified morphism is formally unramified by [Stacks Project, Tag 04AL].

theorem formallyUnramified_of_isImmersion (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {Z X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (i : Z ⟶ X)
    (hi : IsImmersion B S hS i) :
    FormallyUnramified i

AlgebraicGeometry.Space.isUniversalFirstOrderThickening_infinitesimalNeighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningImmersion.lean, line 329. The attribute's comment: “part (2): the universal first order thickening is the neighbourhood”.

Let Z be a closed subspace of an open subspace U of an algebraic space X over S, so that Z is immersed in X, and let N be the first order infinitesimal neighbourhood of Z in X, that is the closed subspace of U whose kernel ideal sheaf is on every étale chart the square of that of Z. Then Z ⊂ N over X is a universal first order thickening of Z over X in the sense of Stacks 0602.

The universal property determines the thickening up to a unique isomorphism, so this is the assertion of the source that the universal first order thickening of Z over X is the first order infinitesimal neighbourhood of Z in X.

The structure morphism to X is the inclusion of N in U followed by the inclusion of U in X, and Z is read inside N as the inverse image of Z along the former.

theorem isUniversalFirstOrderThickening_infinitesimalNeighbourhood
    (hU : IsOpenSubspace B S hS U)
    (Z N : ClosedSubspaces B S hS (⟨U.toFunctor, hU.1⟩ : AlgebraicSpaces B S hS).1)
    (hN : ∀ V : SmallEtale B S hS U.toFunctor,
      ((BigFppfOver.toScheme B S hS).map (N.2.2.rep.snd V.1.hom)).ker =
        ((BigFppfOver.toScheme B S hS).map (Z.2.2.rep.snd V.1.hom)).ker ^ 2) :
    IsUniversalFirstOrderThickening B S hS (Z.1.preimage N.1.ι)
      (ObjectProperty.homMk (N.1.ι ≫ U.ι) :
        (⟨N.1.toFunctor, N.2.1⟩ : AlgebraicSpaces B S hS) ⟶ X)

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

Let i : Z ⟶ X be an immersion of algebraic spaces over S, presented by an open subspace U ⊆ X in which Z is a closed subspace, and let Z ⊂ Z' be a universal first order thickening of Z over X. The conormal sheaf of i as a formally unramified morphism, [Stacks Project, Tag 0607], is isomorphic to the conormal sheaf of i as an immersion, [Stacks Project, Tag 04CN], that is to the conormal module of Z in U.

noncomputable def conormalSheafIsoConormalModule {X : AlgebraicSpaces B S hS}
    {U : Subfunctor X.1} (hU : IsOpenSubspace B S hS U)
    (Z : ClosedSubspaces B S hS (⟨U.toFunctor, hU.1⟩ : AlgebraicSpaces B S hS).1)
    (t : UniversalFirstOrderThickening B S hS
      (ObjectProperty.homMk (Z.1.ι ≫ U.ι) :
        (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶ X)) :
    conormalSheaf B S hS t ≅ conormalModule B S hS ⟨U.toFunctor, hU.1⟩ Z

Tag 0609, a lemma

Tag 0609 in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_of_isUniversalFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningUnramified.lean, line 175.

Let Z ⊂ Z' be a universal first order thickening of Z over an algebraic space X, with structure morphism p : Z' ⟶ X. Then p is formally unramified.

theorem formallyUnramified_of_isUniversalFirstOrderThickening
    {X Z' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.1) (p : Z' ⟶ X)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p) :
    FormallyUnramified p.hom

AlgebraicGeometry.Space.UniversalFirstOrderThickening.formallyUnramified_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningUnramified.lean, line 198. The attribute's comment: “the universal first order thickening of a formally unramified morphism”.

The ambient algebraic space Z' of a universal first order thickening of a formally unramified morphism h : Z ⟶ X of algebraic spaces over S is formally unramified over X.

theorem UniversalFirstOrderThickening.formallyUnramified_toBase
    {Z X : AlgebraicSpaces B S hS} {h : Z ⟶ X} (t : UniversalFirstOrderThickening B S hS h) :
    FormallyUnramified t.toBase.hom

Tag 060A, a lemma

Tag 060A in the Stacks Project.

AlgebraicGeometry.Space.universalThickeningMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFunctorial.lean, line 146. The attribute's comment: “the canonical morphism”.

Stacks 060A, the canonical morphism. Let the square

  Z --h--→ X
  |        |
  f        g
  ↓        ↓
  W --h'-→ Y

of algebraic spaces over S commute, where h = Z.ι ≫ p.hom and h' = W.ι ≫ q.hom, let Z ⊂ Z' be a universal first-order thickening of Z over X with structure morphism p, and let W ⊂ W' be a universal first-order thickening of W over Y with structure morphism q. The canonical morphism f' : Z' ⟶ W' is the dotted arrow furnished by the universal property of W ⊂ W', applied to the first-order thickening Z ⊂ Z', the morphism f : Z ⟶ W and the morphism p ≫ g : Z' ⟶ Y.

Together with f it is the morphism (f, f') : (Z, Z') ⟶ (W, W') of thickenings over Y of the source; see AlgebraicGeometry.Space.universalThickeningHom.

noncomputable def universalThickeningMap (g : X ⟶ Y) (f : Z.toFunctor ⟶ W.toFunctor)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (hsq : Z.ι ≫ p.hom ≫ g.hom = f ≫ W.ι ≫ q.hom) :
    Z' ⟶ W'

AlgebraicGeometry.Space.universalThickeningMap_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFunctorial.lean, line 167. The attribute's comment: “commutativity: the canonical morphism restricts to f”.

Stacks 060A, commutativity: the canonical morphism restricts to f. The composite Z ⊂ Z' --f'--→ W' is Z --f--→ W ⊂ W'. This is the front face of the diagram of the source, and it says that (f, f') is a morphism of the thickenings.

theorem universalThickeningMap_restrict (g : X ⟶ Y) (f : Z.toFunctor ⟶ W.toFunctor)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (hsq : Z.ι ≫ p.hom ≫ g.hom = f ≫ W.ι ≫ q.hom) :
    Z.ι ≫ (universalThickeningMap B S hS g f hZ hW hsq).hom = f ≫ W.ι

AlgebraicGeometry.Space.universalThickeningMap_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFunctorial.lean, line 179. The attribute's comment: “commutativity: the canonical morphism lies over Y”.

Stacks 060A, commutativity: the canonical morphism is a morphism over Y. The composite Z' --f'--→ W' --q--→ Y is Z' --p--→ X --g--→ Y. This is the commutativity of the two squares of the diagram of the source which involve the base, and it says that (f, f') is a morphism of thickenings over Y.

theorem universalThickeningMap_over (g : X ⟶ Y) (f : Z.toFunctor ⟶ W.toFunctor)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (hsq : Z.ι ≫ p.hom ≫ g.hom = f ≫ W.ι ≫ q.hom) :
    universalThickeningMap B S hS g f hZ hW hsq ≫ q = p ≫ g

AlgebraicGeometry.Space.universalThickeningHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFunctorial.lean, line 210. The attribute's comment: “the canonical morphism of thickenings”.

Stacks 060A, the canonical morphism as a morphism of thickenings. The pair (f, f'), read as a morphism Arrow.mk Z.ι ⟶ Arrow.mk W.ι of the inclusions in the arrow category: a packaging of the commuting square of AlgebraicGeometry.Space.universalThickeningMap_restrict.

The arrow category records the square and nothing else; it is not the definition of a morphism of thickenings, which is Stacks 05ZK, parts (5) and (6), namely AlgebraicGeometry.Space.IsMorphismOfThickenings. That the pair is a morphism over Y — the part-(6) clause on f' — is AlgebraicGeometry.Space.universalThickeningMap_over.

noncomputable def universalThickeningHom (g : X ⟶ Y) (f : Z.toFunctor ⟶ W.toFunctor)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (hsq : Z.ι ≫ p.hom ≫ g.hom = f ≫ W.ι ≫ q.hom) :
    Arrow.mk Z.ι ⟶ Arrow.mk W.ι

AlgebraicGeometry.Space.universalThickeningConormalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFunctorial.lean, line 238. The attribute's comment: “the induced map of conormal modules”.

Stacks 060A, the induced map of conormal modules. The morphism (f, f') of thickenings induces the map f^*𝒞_{W/Y} ⟶ 𝒞_{Z/X} of the source: it is the map of Stacks 04CP, AlgebraicGeometry.Space.conormalMap, for the square of closed immersions

  Z ⊂ Z'
  |    |
  f    f'
  ↓    ↓
  W ⊂ W'

whose commutativity is AlgebraicGeometry.Space.universalThickeningMap_restrict.

By Stacks 0607 the conormal sheaf of the formally unramified h : Z ⟶ X is the conormal sheaf of Z in Z', which is how the two spellings agree; see the implementation notes of this file.

noncomputable def universalThickeningConormalMap (g : X ⟶ Y) (f : Z.toFunctor ⟶ W.toFunctor)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (hsq : Z.ι ≫ p.hom ≫ g.hom = f ≫ W.ι ≫ q.hom) :
    (modulePullback B S hS (ObjectProperty.homMk f :
          (⟨Z.toFunctor, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1.1⟩ :
            AlgebraicSpaces B S hS) ⟶
          ⟨W.toFunctor, (IsNthOrderThickening.isThickening B S hS hW.firstOrder).1.1⟩)).obj
        (conormalModule B S hS W'
          ⟨W, (IsNthOrderThickening.isThickening B S hS hW.firstOrder).1⟩) ⟶
      conormalModule B S hS Z'
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩

Tag 060B, a lemma

Tag 060B in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedBaseChange.lean, line 53. The attribute's comment: “the first assertion: in a fibre product diagram, the base change h of a formally unramified h' is formally unramified”. References: EGA IV (17.1.3), “more general”.

Stacks 0600. A base change of a formally unramified morphism of algebraic spaces is formally unramified: in a cartesian square with f formally unramified, the opposite side p of the square is formally unramified.

This is also the first assertion of Stacks 060B: in a fibre product diagram Z = X ×_Y W of algebraic spaces over S with h' : W ⟶ Y formally unramified (here f), the morphism h : Z ⟶ X (here p) is formally unramified.

theorem formallyUnramified_of_isPullback
    {F G H P : AlgebraicSpaces B S hS}
    (f : F ⟶ G) (g : H ⟶ G) (p : P ⟶ H) (q : P ⟶ F)
    (sq : IsPullback p q g f)
    (unramified : FormallyUnramified f.hom) :
    FormallyUnramified p.hom

AlgebraicGeometry.Space.isUniversalFirstOrderThickening_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningBaseChange.lean, line 250. The attribute's comment: “the second assertion: the base change of the universal first-order thickening is the universal first-order thickening of the base change”.

Stacks 060B, the second assertion. Let W ⊂ W' be a universal first-order thickening of W over Y, with structure morphism q : W' ⟶ Y, and let g : X ⟶ Y be a morphism of algebraic spaces. Then X ×_Y W ⊂ X ×_Y W' is a universal first-order thickening of X ×_Y W over X, with structure morphism the projection p : X ×_Y W' ⟶ X.

A morphism T' ⟶ X ×_Y W' is a pair of morphisms to X and to W' agreeing over Y. Given a solid diagram over X built from a first-order thickening T ⊂ T' and a morphism T ⟶ X ×_Y W, the morphism to X is the one the diagram supplies and the morphism to W' is the unique one furnished by the universal property of W ⊂ W' for the diagram pushed forward along X ×_Y W ⟶ W; uniqueness of the resulting morphism is uniqueness there together with the mapping property of the fibre product. That X ×_Y W ⊆ X ×_Y W' is a first-order thickening is AlgebraicGeometry.Space.isFirstOrderThickening_baseChangeSub, from Stacks 09ZX.

theorem isUniversalFirstOrderThickening_baseChange
    (univW : IsUniversalFirstOrderThickening B S hS W q) :
    IsUniversalFirstOrderThickening B S hS (baseChangeSub B S hS W q g)
      (baseChangeThickeningFst B S hS q g)

AlgebraicGeometry.Space.epi_universalThickeningConormalMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningBaseChange.lean, line 346. The attribute's comment: “the third assertion: surjectivity of the induced map of conormal modules”.

Stacks 060B, the third assertion. The canonical map f^*𝒞_{W/Y} ⟶ 𝒞_{Z/X} of conormal modules of Stacks 060A, attached to the cartesian square of the source, is surjective.

By AlgebraicGeometry.Space.universalThickeningMap_baseChange the morphism of ambient spaces of that map is the projection r : X ×_Y W' ⟶ W', and the closed subspace upstairs is the inverse image r⁻¹(W), so the map is the one of the fibre product square of AlgebraicGeometry.Space.epi_conormalMap, the surjectivity clause of Stacks 04CQ.

theorem epi_universalThickeningConormalMap_baseChange
    (univW : IsUniversalFirstOrderThickening B S hS W q) :
    Epi (universalThickeningConormalMap B S hS g
      (universalThickeningBaseChangeProjection B S hS W q g)
      (isUniversalFirstOrderThickening_baseChange B S hS W q g univW) univW
      (baseChangeThickening_square B S hS W q g))

Tag 060C, a lemma

Tag 060C in the Stacks Project.

AlgebraicGeometry.Space.isFlat_baseChangeThickeningSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningBaseChange.lean, line 371. The attribute's comment: “the first assertion: the induced morphism of universal first-order thickenings is flat”.

Stacks 060C, the first assertion. In the cartesian square of Stacks 060B, if g is flat then so is the induced morphism r : X ×_Y W' ⟶ W' of universal first-order thickenings.

The projection r is the base change of g along q : W' ⟶ Y, and flatness of morphisms of algebraic spaces is stable under base change by Stacks 03MO. That r is the induced morphism of universal first-order thickenings — the canonical morphism of Stacks 060A for this square — is AlgebraicGeometry.Space.universalThickeningMap_baseChange.

Flatness is AlgebraicGeometry.Space.IsFlat, the chartwise flatness of Stacks 03ML part (1), which is the notion the source assumes of g.

theorem isFlat_baseChangeThickeningSnd (g_flat : IsFlat B S hS g.hom) :
    IsFlat B S hS (baseChangeThickeningSnd B S hS q g).hom

AlgebraicGeometry.Space.isIso_universalThickeningConormalMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningBaseChange.lean, line 419. The attribute's comment: “the second assertion: the induced map of conormal modules is an isomorphism”.

Stacks 060C, the second assertion. In the cartesian square of Stacks 060B, if g is flat then the canonical map f^*𝒞_{W/Y} ⟶ 𝒞_{Z/X} of conormal modules of Stacks 060A is an isomorphism.

Flatness of g is AlgebraicGeometry.Space.IsFlat, the chartwise flatness of Stacks 03ML part (1), which is the notion the source assumes. It passes to the projection r : X ×_Y W' ⟶ W' by AlgebraicGeometry.Space.isFlat_baseChangeThickeningSnd, and from there to flatness of the induced morphism of small étale ringed topoi by Stacks 073C, AlgebraicGeometry.Space.isFlat_iff_smallEtaleRingedToposHom_isFlat, which is the hypothesis the flat clause of Stacks 04CQ consumes; the conclusion is then AlgebraicGeometry.Space.isIso_universalThickeningConormalMap_baseChange_of_isFlatRingedTopos.

Together with AlgebraicGeometry.Space.isFlat_baseChangeThickeningSnd this is Stacks 060C as the source states it: no hypothesis beyond the configuration of Stacks 060B and flatness of g.

theorem isIso_universalThickeningConormalMap_baseChange
    (univW : IsUniversalFirstOrderThickening B S hS W q) (g_flat : IsFlat B S hS g.hom) :
    IsIso (universalThickeningConormalMap B S hS g
      (universalThickeningBaseChangeProjection B S hS W q g)
      (isUniversalFirstOrderThickening_baseChange B S hS W q g univW) univW
      (baseChangeThickening_square B S hS W q g))

Tag 060D, a lemma

Tag 060D in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_of_etaleLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalFirstOrderThickeningDescent.lean, line 490. The attribute's comment: “the étale localization of a formally unramified morphism is formally unramified”.

Stacks 060D, the first of its three assertions. Let h : Z ⟶ X be a formally unramified morphism of algebraic spaces over S, and let f : V ⟶ U sit in a commutative square over it whose vertical arrows v : V ⟶ Z and u : U ⟶ X are étale. Then f is formally unramified: taking the étale localization of a formally unramified morphism preserves formal unramifiedness.

An étale morphism of algebraic spaces is formally étale by Stacks 0616, hence formally unramified, so the diagonal v ≫ h of the square is formally unramified by Stacks 049T. That diagonal is the composite f ≫ u, and a first factor of a formally unramified composite whose second factor is formally unramified is itself formally unramified by Stacks 04G5. Étaleness of v enters through formal unramifiedness of the diagonal and étaleness of u through formal unramifiedness of the second factor; formal unramifiedness of h enters through the diagonal as well. The source instead reads the statement off the étale-chart criterion of Stacks 04G8; the route taken here proves the same statement without passing through charts.

The remaining two assertions of Stacks 060D — that the universal first-order thickening of V over U is étale over the universal first-order thickening Z' of Z over X, and the resulting identification of conormal modules — are proved in the sibling module StacksFrontier.AlgebraicGeometry.Spaces.UniversalThickeningEtaleLocalization, which carries those parts of the tag; nothing in this module does.

theorem formallyUnramified_of_etaleLocalization {V U Z X : AlgebraicSpaces B S hS}
    (f : V ⟶ U) (v : V ⟶ Z) (h : Z ⟶ X) (u : U ⟶ X) (hsq : f ≫ u = v ≫ h)
    (hh : FormallyUnramified h.hom) (hv : IsEtale B S hS v.hom)
    (hu : IsEtale B S hS u.hom) :
    FormallyUnramified f.hom

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.etaleLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningEtaleLocalization.lean, line 212. The attribute's comment: “clause (2): the universal first-order thickening of the etale localization”.

Stacks 060D, clause (2). Let Z ⊂ Z' be a universal first-order thickening of Z over an algebraic space X, with structure morphism p : Z' ⟶ X, let φ : U ⟶ X be étale, let g : V' ⟶ Z' be étale with a morphism r : V' ⟶ U satisfying r ≫ φ = g ≫ p, and let V ⊂ V' be a closed subspace whose inclusion sits in a cartesian square over the inclusion of Z, so that V = Z ×_{Z'} V'. Then V ⊂ V' is a universal first-order thickening of V over U, with structure morphism r.

This says that the universal first-order thickening of V over U is the étale extension V' of V across Z ⊂ Z', and in particular that it is étale over Z', which is the assertion of the source. The extension is a hypothesis rather than a conclusion of this statement, but it is not an unavailable input: the topological invariance of the spaces-étale site which produces it, Stacks 05ZH, is proved at a first-order thickening, and Stacks.Spaces.UniversalThickening.etaleExtendsAlongFirstOrderThickening assembles the extension from it unconditionally. See the implementation notes for why the shape is kept.

The morphism V ⟶ Z of the source appears as the top edge c of the cartesian square, and is automatically étale, being a base change of g.

theorem IsUniversalFirstOrderThickening.etaleLocalization
    {X U Z' V' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.obj) (p : Z' ⟶ X)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (g : V' ⟶ Z') (hg : IsEtale B S hS g.hom) (r : V' ⟶ U) (hr : r ≫ φ = g ≫ p)
    (V : Subfunctor V'.obj) (c : V.toFunctor ⟶ Z.toFunctor)
    (hsq : IsPullback c V.ι Z.ι g.hom) :
    IsUniversalFirstOrderThickening B S hS V r

AlgebraicGeometry.Space.exists_isEtale_of_isUniversalFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningEtaleLocalization.lean, line 268. The attribute's comment: “clause (2): the universal first-order thickening is etale over the thickening of Z”.

Stacks 060D, clause (2), the étaleness assertion. With the data of clause (2), every universal first-order thickening W ⊂ W' of V over U is étale over Z': there is a morphism W' ⟶ Z' which is étale, restricts on W to the composite V ⟶ Z ⊂ Z' read through the identification of W with V, and lies over X.

This is the sentence of the source. Clause (2) identifies the étale extension V' of V across Z ⊂ Z' as a universal first-order thickening of V over U, and the universal property of Stacks 0602 makes any other one isomorphic to it over U: the two canonical morphisms of Stacks 060A between them compose, in either order, to a morphism which restricts to the identity and lies over U, hence to the identity by the uniqueness clause. Transporting the étale g : V' ⟶ Z' along that isomorphism gives the morphism asserted here.

The identification of W with V is the datum e, with he saying that it is one of spaces over U; it is needed because the smaller space of a thickening is presented as a subfunctor of its ambient space, so two thickenings of one space never have literally the same smaller space.

theorem exists_isEtale_of_isUniversalFirstOrderThickening
    {X U Z' V' W' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.obj) (p : Z' ⟶ X)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (g : V' ⟶ Z') (hg : IsEtale B S hS g.hom) (r : V' ⟶ U) (hr : r ≫ φ = g ≫ p)
    (V : Subfunctor V'.obj) (c : V.toFunctor ⟶ Z.toFunctor)
    (hsq : IsPullback c V.ι Z.ι g.hom)
    (W : Subfunctor W'.obj) (q : W' ⟶ U)
    (hW : IsUniversalFirstOrderThickening B S hS W q)
    (e : W.toFunctor ≅ V.toFunctor) (he : e.hom ≫ V.ι ≫ r.hom = W.ι ≫ q.hom) :
    ∃ m : W' ⟶ Z', IsEtale B S hS m.hom ∧ W.ι ≫ m.hom = e.hom ≫ V.ι ≫ g.hom ∧
      m ≫ p = q ≫ φ

AlgebraicGeometry.Space.conormalModuleEtaleLocalizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningEtaleLocalization.lean, line 322. The attribute's comment: “clause (3): the conormal module of the etale localization”.

Stacks 060D, clause (3). With the data of clause (2), the conormal module of Z in Z' restricts along the projection c : V ⟶ Z to the conormal module of V in V':

𝒞_{Z/X}|_V = c^*𝒞_{Z/X} ≅ 𝒞_{V/U}.

The two sides are the conormal sheaves of Stacks 0607 of the formally unramified morphisms Z ⟶ X and V ⟶ U: the left-hand one because Z ⊂ Z' is a universal first-order thickening of Z over X by hypothesis, the right-hand one because V ⊂ V' is a universal first-order thickening of V over U by clause (2).

The isomorphism is the étale base change of Stacks 04CO, AlgebraicGeometry.Space.conormalModuleEtaleRestrictionIso, for the étale morphism g : V' ⟶ Z', transported along the cartesian square: the square forces V to be the inverse image g⁻¹(Z) and c to be the canonical projection of that inverse image.

noncomputable def conormalModuleEtaleLocalizationIso {Z' V' : AlgebraicSpaces B S hS}
    (Z : ClosedSubspaces B S hS Z'.obj) (g : V' ⟶ Z') (hg : IsEtale B S hS g.hom)
    (V : Subfunctor V'.obj) (hV : IsClosedSubspace B S hS V)
    (c : V.toFunctor ⟶ Z.1.toFunctor) (hsq : IsPullback c V.ι Z.1.ι g.hom) :
    (modulePullback B S hS
          (ObjectProperty.homMk c :
            (⟨V.toFunctor, hV.1⟩ : AlgebraicSpaces B S hS) ⟶
              (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))).obj
        (conormalModule B S hS Z' Z) ≅
      conormalModule B S hS V' ⟨V, hV⟩

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.exists_etaleLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningEtaleLocalizationFull.lean, line 137. The attribute's comment: “the thickening assertion, étale extension produced from V ⟶ Z, not assumed”.

Stacks 060D, the thickening assertion, with the étale extension produced. Let Z ⊂ Z' be a universal first-order thickening of Z over an algebraic space X, with structure morphism p : Z' ⟶ X, let φ : U ⟶ X be étale, and let

  V ---→ U
  |      |
  ↓      ↓
  Z ---→ X

commute with v : V ⟶ Z étale. Then there are an algebraic space V', an étale g : V' ⟶ Z', a morphism r : V' ⟶ U with r ≫ φ = g ≫ p, a subspace V ⊂ V' sitting in a cartesian square over the inclusion of Z, and an isomorphism of that subspace with the given V compatible with the maps to Z and to U, such that V ⊂ V' is a universal first-order thickening of V over U.

Nothing about V' is assumed. It is the essential-surjectivity half of the topological invariance of the spaces-étale site at the first-order thickening Z ⊂ Z', Stacks 05ZH in the form AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening, applied to the object v of the spaces-étale site of Z: it returns an object of the spaces-étale site of Z' whose base change along the inclusion of Z is v. Its subspace is the inverse image g⁻¹(Z), which is cartesian over Z ⊂ Z' by Stacks 083Q, CategoryTheory.Subfunctor.isPullback_preimage, and is a first-order thickening because g is étale, by Stacks 09ZX in the étale case (AlgebraicGeometry.Space.isNthOrderThickening_preimage_of_isEtale). The identification of g⁻¹(Z) with the given V is the comparison of two cartesian squares on one cospan, composed with the isomorphism of objects of the site. The remaining datum, r, is the extension of V ⟶ U across g⁻¹(Z) ⊂ V': that is the unique lift of Stacks 0611 for the formally étale φ, which is where étaleness of φ — rather than of U ⟶ X only in the source's diagram — is used. That V ⊂ V' is then a universal first-order thickening of V over U is AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.etaleLocalization.

The conormal assertion applies verbatim to the data produced here: the cartesian square returned below is the hypothesis of AlgebraicGeometry.Space.conormalModuleEtaleLocalizationIso.

The attribute carries a part string rather than being bare for the reason recorded in the implementation notes: the first assertion of the source, formal unramifiedness of V ⟶ U, is independent of this statement — it is AlgebraicGeometry.Space.formallyUnramified_of_etaleLocalization, which takes formal unramifiedness of Z ⟶ X as a hypothesis, whereas here the universal property of Stacks 0602 is carried instead. The bare registration sits on AlgebraicGeometry.Space.etaleLocalization_commutes_universalFirstOrderThickening at the end of this file, which states all three assertions together.

theorem IsUniversalFirstOrderThickening.exists_etaleLocalization
    {X U Z' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.obj) (p : Z' ⟶ X)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (V₀ : AlgebraicSpaces B S hS) (v : V₀.obj ⟶ Z.toFunctor) (hv : IsEtale B S hS v)
    (u : V₀ ⟶ U) (hcomm : u.hom ≫ φ.hom = v ≫ Z.ι ≫ p.hom) :
    ∃ (V' : AlgebraicSpaces B S hS) (g : V' ⟶ Z') (r : V' ⟶ U) (V : Subfunctor V'.obj)
      (c : V.toFunctor ⟶ Z.toFunctor) (e : V.toFunctor ≅ V₀.obj),
      IsEtale B S hS g.hom ∧ IsPullback c V.ι Z.ι g.hom ∧ r ≫ φ = g ≫ p ∧
        e.hom ≫ v = c ∧ V.ι ≫ r.hom = e.hom ≫ u.hom ∧
        IsUniversalFirstOrderThickening B S hS V r

AlgebraicGeometry.Space.etaleLocalization_commutes_universalFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningEtaleLocalizationFull.lean, line 251.

Stacks 060D. Taking the universal first-order thickenings commutes with étale localization. Let h : Z ⟶ X be a formally unramified morphism of algebraic spaces over S, presented as a closed subspace Z of an algebraic space Z' with structure morphism p : Z' ⟶ X, so that h = Z.ι ≫ p.hom, and let Z ⊂ Z' be the universal first-order thickening of Z over X. Let

  V ---→ U
  |      |
  ↓      ↓
  Z ---→ X

commute with the vertical arrows v : V ⟶ Z and φ : U ⟶ X étale. Then

• f : V ⟶ U is formally unramified;
• the universal first-order thickening of V over U is étale over Z': there is one, and every one admits an étale morphism to Z' restricting on V to V ⟶ Z ⊂ Z' and lying over X;
• 𝒞_{Z/X}|_V = 𝒞_{V/U}: the canonical comparison map from the restriction along V ⟶ Z of the conormal module of Z in Z' to the conormal module of V in that thickening — the morphism underlying AlgebraicGeometry.Space.conormalModuleEtaleLocalizationIso, which is the étale base change of Stacks 04CO transported along the cartesian square — is an isomorphism.

The source draws these three assertions in continuous prose and numbers none of them.

The first is AlgebraicGeometry.Space.formallyUnramified_of_etaleLocalization. The second is AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.exists_etaleLocalization, which produces the thickening V ⊂ V' as the étale extension of V across Z ⊂ Z', together with AlgebraicGeometry.Space.exists_isEtale_of_isUniversalFirstOrderThickening, which carries the étaleness over Z' to any other universal first-order thickening of V over U — the source speaks of the thickening, which is determined up to unique isomorphism by Stacks 0602. The third is AlgebraicGeometry.Space.conormalModuleEtaleLocalizationIso.

The étaleness of g and the cartesian square are existential binders rather than conjuncts because the canonical comparison map is built from them: the third assertion then names that map, instead of asserting that the two conormal modules are isomorphic by some unnamed isomorphism. The source writes an equality, 𝒞_{Z/X}|_V = 𝒞_{V/U}, which is the canonical identification and not a bare existence claim.

The smaller space of a thickening is presented as a subfunctor of its ambient space, so the copy of V inside the thickening is never literally the given V₀; the isomorphism e, and the identification eW in the second assertion, record the comparison, and the equations that accompany them say that it is one of spaces over Z and over U.

theorem etaleLocalization_commutes_universalFirstOrderThickening
    {X U Z' : AlgebraicSpaces B S hS} (Z : Subfunctor Z'.obj) (p : Z' ⟶ X)
    (hZ : IsUniversalFirstOrderThickening B S hS Z p)
    (hh : FormallyUnramified (Z.ι ≫ p.hom))
    (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (V₀ : AlgebraicSpaces B S hS) (f : V₀ ⟶ U) (v : V₀.obj ⟶ Z.toFunctor)
    (hv : IsEtale B S hS v) (hcomm : f.hom ≫ φ.hom = v ≫ Z.ι ≫ p.hom) :
    FormallyUnramified f.hom ∧
      (∀ (W' : AlgebraicSpaces B S hS) (W : Subfunctor W'.obj) (q : W' ⟶ U)
          (eW : W.toFunctor ≅ V₀.obj), IsUniversalFirstOrderThickening B S hS W q →
          eW.hom ≫ f.hom = W.ι ≫ q.hom →
          ∃ m : W' ⟶ Z', IsEtale B S hS m.hom ∧
            W.ι ≫ m.hom = eW.hom ≫ v ≫ Z.ι ∧ m ≫ p = q ≫ φ) ∧
      ∃ (V' : AlgebraicSpaces B S hS) (g : V' ⟶ Z') (r : V' ⟶ U) (V : Subfunctor V'.obj)
        (c : V.toFunctor ⟶ Z.toFunctor) (e : V.toFunctor ≅ V₀.obj)
        (hV : IsUniversalFirstOrderThickening B S hS V r) (hg : IsEtale B S hS g.hom)
        (hsq : IsPullback c V.ι Z.ι g.hom),
        r ≫ φ = g ≫ p ∧ e.hom ≫ v = c ∧ V.ι ≫ r.hom = e.hom ≫ f.hom ∧
          IsIso (conormalModuleEtaleLocalizationIso B S hS ⟨Z, hZ.firstOrder.1.1⟩ g hg V
            hV.firstOrder.1.1 c hsq).hom

Tag 060E, a lemma

Tag 060E in the Stacks Project.

AlgebraicGeometry.Space.isIso_restrict_of_isSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningDifferentials.lean, line 312. The attribute's comment: “granted, as hetale, the étale localization of 04CU and 060D: over each object of the small étale site of Z the restriction along Z ⟶ Z' of the comparison map of 04CX is, on sections, the map 04FB of a universal first-order thickening of schemes assembled from charts of Z', X and Y over that object. The scheme case 04FB is applied, not granted; formal unramifiedness of h is not assumed, a universal first-order thickening being given”.

Stacks 060E. Let h : Z ⟶ X be a morphism of algebraic spaces over S, presented as the composite Z.ι ≫ h' of the inclusion of a closed subspace Z of an algebraic space Z' with a structure morphism h' : Z' ⟶ X, and let Z ⊂ Z' be a universal first-order thickening of Z over X. For a morphism p : X ⟶ Y to a base algebraic space, the comparison map c_{h'} : (h')^*Ω_{X/Y} ⟶ Ω_{Z'/Y} of Stacks 04CX induces an isomorphism h^*Ω_{X/Y} ⟶ Ω_{Z'/Y} ⊗ 𝒪_Z, namely its restriction along the inclusion of Z.

The map is named by the characterizing property of Stacks 04CX, which determines it uniquely by AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap; that uniqueness carries the étale-local input from the realization c₀ it is stated for to the realization c in hand. The proof is the source's: over an étale chart of Z the restricted comparison map is the map of Stacks 04FB of a universal first-order thickening of schemes, which is an isomorphism, and a morphism of 𝒪_Z-modules which is bijective on the sections over every chart is an isomorphism.

Formal unramifiedness of h, a hypothesis of the source, is not assumed: it is what makes a universal first-order thickening exist, one is given, and by Stacks 0609 it follows.

theorem isIso_restrict_of_isSheafOfDifferentialsMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (c c₀ : (modulePullback B S hS h').obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS (h' ≫ p))
    (hc : IsSheafOfDifferentialsMap B S hS h' p (h' ≫ p) c)
    (hc₀ : IsSheafOfDifferentialsMap B S hS h' p (h' ≫ p) c₀)
    (hetale : IsEtaleLocalThickeningDifferentialsMap B S hS hZ p
      ((modulePullback B S hS (universalThickeningInclusion B S hS hZ)).map c₀)) :
    IsIso ((modulePullback B S hS (universalThickeningInclusion B S hS hZ)).map c)

AlgebraicGeometry.Space.isIso_thickeningSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningDifferentials.lean, line 349. The attribute's comment: “granted, as hetale, the étale localization of 04CU and 060D, as for isIso_restrict_of_isSheafOfDifferentialsMap; stated for the comparison map of 04CX as constructed”.

Stacks 060E for the comparison map constructed by AlgebraicGeometry.Space.sheafOfDifferentialsMap: the map AlgebraicGeometry.Space.thickeningSheafOfDifferentialsMap is an isomorphism.

This is AlgebraicGeometry.Space.isIso_restrict_of_isSheafOfDifferentialsMap at the realization of the comparison map which Stacks 04CX constructs, whose characterizing property is AlgebraicGeometry.Space.isSheafOfDifferentialsMap_sheafOfDifferentialsMap.

theorem isIso_thickeningSheafOfDifferentialsMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (hetale : IsEtaleLocalThickeningDifferentialsMap B S hS hZ p
      (thickeningSheafOfDifferentialsMap B S hS hZ p)) :
    IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p)

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.isIso_restrict_of_isSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningDifferentialsIso.lean, line 69.

For a universal first-order thickening Z ⊂ Z' over X with structure morphism h', and a morphism p : X ⟶ Y, the restriction along the inclusion ι : Z ⟶ Z' of any realization c of the comparison map (h')^*Ω_{X/Y} ⟶ Ω_{Z'/Y} is an isomorphism h^*Ω_{X/Y} ≅ Ω_{Z'/Y} ⊗ 𝒪_Z.

theorem isIso_restrict_of_isSheafOfDifferentialsMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    {c : (modulePullback B S hS h').obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS (h' ≫ p)}
    (hc : IsSheafOfDifferentialsMap B S hS h' p (h' ≫ p) c) :
    IsIso ((modulePullback B S hS (universalThickeningInclusion B S hS hZ)).map c)

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.isIso_thickeningSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningDifferentialsIso.lean, line 93.

For a universal first-order thickening Z ⊂ Z' and a morphism p : X ⟶ Y, the comparison map AlgebraicGeometry.Space.thickeningSheafOfDifferentialsMap is an isomorphism.

theorem isIso_thickeningSheafOfDifferentialsMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y) :
    IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p)

Tag 060F, a lemma

Tag 060F in the Stacks Project.

AlgebraicGeometry.Space.thickeningConormalFirstMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceFormallyUnramified.lean, line 180. The attribute's comment: “the canonical first arrow 𝒞_{Z/X} ⟶ h^*Ω_{X/Y}, with 𝒞_{Z/X} the conormal module of Z ⊂ Z' of 0607(2) and the middle term read as ι^*(h')^*Ω_{X/Y}; granted as he that the map of 060E is an isomorphism, which isIso_thickeningSheafOfDifferentialsMap supplies”.

Stacks 060F, the canonical first arrow 𝒞_{Z/X} ⟶ h^*Ω_{X/Y}.

The source 𝒞_{Z/X} is the conormal module 𝒞_{Z/Z'} of the closed subspace Z ⊂ Z', which is what Stacks 0607, part (2) defines 𝒞_{Z/X} to be; the target h^*Ω_{X/Y} is read as the double inverse image ι^*(h')^*Ω_{X/Y}, as in Stacks 060E. The arrow is the first arrow AlgebraicGeometry.Space.conormalSequenceFirstMap of Stacks 05ZA for Z ⊂ Z' over Y, followed by the inverse of the isomorphism AlgebraicGeometry.Space.thickeningSheafOfDifferentialsMap of Stacks 060E.

The hypothesis he is that isomorphism, which AlgebraicGeometry.Space.isIso_thickeningSheafOfDifferentialsMap supplies.

noncomputable def thickeningConormalFirstMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (he : IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p)) :
    conormalModule B S hS Z' (thickeningClosedSubspace B S hS hZ) ⟶
      (modulePullback B S hS (universalThickeningInclusion B S hS hZ)).obj
        ((modulePullback B S hS h').obj (sheafOfDifferentials B S hS p))

AlgebraicGeometry.Space.thickeningConormalFirstMap_comp_thickeningSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceFormallyUnramified.lean, line 227. The attribute's comment: “the first arrow is induced by d_{Z'/B}: composed with the isomorphism of 060E it is the first arrow of 05ZA for Z ⊂ Z' over the base, which conormalSequenceIdealDifferential_val_app_apply identifies with d_{Z'/B} on the defining ideal sheaf; granted as he that the map of 060E is an isomorphism”.

Stacks 060F, "the first arrow is induced by d_{Z'/Y}". Composed with the isomorphism of Stacks 060E, the first arrow is the first arrow of Stacks 05ZA for the closed subspace Z ⊂ Z' over Y; and that arrow is induced by d_{Z'/Y} in the sense of AlgebraicGeometry.Space.conormalSequenceIdealDifferential_val_app_apply, namely its transpose across ι^* ⊣ ι_* carries a section of the defining ideal sheaf of Z to the universal differential d_{Z'/Y} of that section followed by the unit of the adjunction.

Since the map of Stacks 060E is an isomorphism, this equation determines the first arrow, so it is the whole of that arrow's dependence on d_{Z'/Y}. It holds by construction — it is the defining equation of AlgebraicGeometry.Space.thickeningConormalFirstMap, recorded so that consumers may rewrite with it rather than unfold the definition, as AlgebraicGeometry.Space.conormalModule_eq and AlgebraicGeometry.Space.conormalSheaf_eq are for their definitions; what carries the mathematical content of the clause is the Stacks 05ZA statement it defers to.

theorem thickeningConormalFirstMap_comp_thickeningSheafOfDifferentialsMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (he : IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p)) :
    thickeningConormalFirstMap B S hS hZ p he ≫
        thickeningSheafOfDifferentialsMap B S hS hZ p =
      conormalSequenceFirstMap B S hS (thickeningClosedSubspace B S hS hZ) (h' ≫ p)

AlgebraicGeometry.Space.epi_thickeningConormalSecondMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceFormallyUnramified.lean, line 248. The attribute's comment: “exactness at the right term: the second arrow h^*Ω_{X/Y} ⟶ Ω_{Z/Y} is an epimorphism. Granted as he that the map of 060E is an isomorphism, and as hsharp local surjectivity of ι♯ (the inverse-image form of the surjectivity clause of 03MB), which is the same hypothesis as in the exactness at the right term of 05ZA”.

Stacks 060F, exactness at the right term. The second arrow h^*Ω_{X/Y} ⟶ Ω_{Z/Y} is an epimorphism, so the sequence ends in zero.

It is the isomorphism of Stacks 060E followed by the second arrow of Stacks 05ZA, and the latter is an epimorphism by AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_of_isLocallySurjective under local surjectivity of ι♯, which is the hypothesis hsharp passed straight through.

theorem epi_thickeningConormalSecondMap
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (he : IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p))
    (hsharp : Presheaf.IsLocallySurjective
      (SmallEtale.topology B S hS (universalThickeningSubSpace B S hS hZ).obj)
      (structureSharpInverseImage B S hS (universalThickeningInclusion B S hS hZ)).hom) :
    Epi (thickeningConormalSecondMap B S hS hZ p)

AlgebraicGeometry.Space.thickeningConormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceFormallyUnramified.lean, line 287. The attribute's comment: “the composite of the two arrows is zero and the short complex is exact at the middle term h^*Ω_{X/Y} — the transport across the isomorphism of 060E, which is the whole of the tag's proof. Granted as he that the map of 060E is an isomorphism, and as hzero and h05ZA the same two clauses for the sequence of 05ZA at Z ⊂ Z' over the base, which are the two clauses 05ZA leaves open in this tree. Exactness at the right term is separate and is proved: see epi_thickeningConormalSecondMap”.

Stacks 060F, the two remaining clauses: the composite of the two arrows is zero, and the resulting short complex 𝒞_{Z/X} ⟶ h^*Ω_{X/Y} ⟶ Ω_{Z/Y} is exact at the middle term.

This is the transport the source's proof performs, and it is all that is proved here: both clauses are granted for the sequence of Stacks 05ZA at the closed subspace Z ⊂ Z' over Y, as hzero and h05ZA, and the isomorphism of Stacks 060E carries them across. The short complex of the conclusion is isomorphic to the short complex of Stacks 05ZA, by the identity on the two outer terms and that isomorphism on the middle one, so CategoryTheory.ShortComplex.exact_iff_of_iso transfers exactness.

The two granted clauses are precisely the two clauses that StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceDifferentials.lean leaves open for Stacks 05ZA, stated at its first arrow and at its second arrow AlgebraicGeometry.Space.pullbackDifferentialsMap, so proving them there discharges them here verbatim. Exactness at the right term is not among them: it is proved, by AlgebraicGeometry.Space.epi_thickeningConormalSecondMap.

theorem thickeningConormalSequence_exact
    (hZ : IsUniversalFirstOrderThickening B S hS Z h') (p : X ⟶ Y)
    (he : IsIso (thickeningSheafOfDifferentialsMap B S hS hZ p))
    (hzero : conormalSequenceFirstMap B S hS (thickeningClosedSubspace B S hS hZ) (h' ≫ p) ≫
      pullbackDifferentialsMap B S hS (universalThickeningInclusion B S hS hZ) (h' ≫ p) = 0)
    (h05ZA : (ShortComplex.mk _ _ hzero).Exact) :
    ∃ hc : thickeningConormalFirstMap B S hS hZ p he ≫
        thickeningConormalSecondMap B S hS hZ p = 0,
      (ShortComplex.mk _ _ hc).Exact

AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.exists_conormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedConormalSequence.lean, line 152.

Let h = ι ≫ h' : Z ⟶ X be formally unramified over Y, with universal first order neighbourhood Z ⊂ Z' over X given by hZ. The canonical sequence

  𝒞_{Z/X} ⟶ h^*Ω_{X/Y} ⟶ Ω_{Z/Y} ⟶ 0

is exact: the composite of its two arrows is zero, it is exact at h^*Ω_{X/Y}, and its second arrow is an epimorphism. Its first arrow is induced by d_{Z'/Y}: followed by the isomorphism h^*Ω_{X/Y} ≅ ι^*Ω_{Z'/Y} of Stacks 060E it is the arrow AlgebraicGeometry.Space.conormalSequenceFirstMap of the closed subspace Z ⊂ Z', whose transpose sends a local section of the ideal of Z to its differential (AlgebraicGeometry.Space.conormalSequenceIdealDifferential_val_app_apply).

The sequence of Stacks 05ZA for Z ⊂ Z' is exact, and the isomorphism of Stacks 060E carries it onto this one.

theorem exists_conormalSequence_exact (hZ : IsUniversalFirstOrderThickening B S hS Z h')
    (p : X ⟶ Y) :
    ∃ hc : thickeningConormalFirstMap B S hS hZ p
        (hZ.isIso_thickeningSheafOfDifferentialsMap B S hS p) ≫
          thickeningConormalSecondMap B S hS hZ p = 0,
      (ShortComplex.mk _ _ hc).Exact ∧ Epi (thickeningConormalSecondMap B S hS hZ p) ∧
        thickeningConormalFirstMap B S hS hZ p
            (hZ.isIso_thickeningSheafOfDifferentialsMap B S hS p) ≫
          thickeningSheafOfDifferentialsMap B S hS hZ p =
        conormalSequenceFirstMap B S hS (thickeningClosedSubspace B S hS hZ) (h' ≫ p)

Tag 06BE, a lemma

Tag 06BE in the Stacks Project.

AlgebraicGeometry.Space.exists_conormalPairSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceUnramifiedPairExact.lean, line 242.

Stacks 06BE. Let i : Z ⟶ X and j : Z ⟶ Y be formally unramified morphisms of algebraic spaces over S with i ≫ g = j, presented by universal first-order thickenings ti of i and tj of j. Then the canonical sequence

  𝒞_{Z/Y} ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Y} ⟶ 0

is exact: the composite of the two arrows is zero, the sequence is exact at 𝒞_{Z/X}, and the second arrow is an epimorphism. The first arrow is the map of conormal modules of Stacks 060A attached to the canonical morphism Z' ⟶ Z'' of the two thickenings, written as the conormal map of Stacks 04CP of its square of closed subspaces; the second is the canonical first arrow of Stacks 060F.

theorem exists_conormalPairSequence_exact (g : X ⟶ Y) {i : Z ⟶ X} {j : Z ⟶ Y}
    (hij : i ≫ g = j) (ti : UniversalFirstOrderThickening B S hS i)
    (tj : UniversalFirstOrderThickening B S hS j) :
    ∃ hc : conormalMap B S hS (thickeningClosedSubspace B S hS ti.isUniversal)
          (thickeningClosedSubspace B S hS tj.isUniversal)
          (universalThickeningComparison B S hS g hij ti tj)
          (ObjectProperty.homMk (universalThickeningSourceMap B S hS ti tj))
          (universalThickeningComparison_square B S hS g hij ti tj) ≫
        thickeningConormalFirstMap B S hS ti.isUniversal g
          (ti.isUniversal.isIso_thickeningSheafOfDifferentialsMap B S hS g) = 0,
      (ShortComplex.mk _ _ hc).Exact ∧
        Epi (thickeningConormalFirstMap B S hS ti.isUniversal g
          (ti.isUniversal.isIso_thickeningSheafOfDifferentialsMap B S hS g))

Tag 06BF, a lemma

Tag 06BF in the Stacks Project.

AlgebraicGeometry.Space.universalThickeningCompConormalSequence_comp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/ConormalSequenceCompositionExact.lean, line 223. The attribute's comment: “clause (2): the composite of the two maps of the sequence vanishes”.

The composite of the two arrows of the conormal sequence of the composition vanishes. By the composition law of part (3) of Stacks 04G2, AlgebraicGeometry.Space.conormalMap_comp, the composite is the map of Stacks 04CP attached to the outer rectangle, read through the composition comparison of Stacks 03LU, which is an isomorphism. The lower edge of that rectangle is the inclusion of the fibre product Y ×_{Y'} Z' into Z' followed by the morphism h : Z' ⟶ Y' of clause (1) of Stacks 06BF, and that composite factors through the closed subspace Y ⊆ Y' by the structure morphism AlgebraicGeometry.Space.universalThickeningCompStructure of the fibre product — which is what makes the fibre product a fibre product. So the map of the outer rectangle vanishes by AlgebraicGeometry.Space.conormalMap_eq_zero_of_factorization.

public theorem universalThickeningCompConormalSequence_comp_eq_zero :
    modulePullbackMap B S hS
          (preimageProjection B S hS
            (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
            ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)
          (universalThickeningCompConormalLowerMap B S hS i hZ hY hfac) ≫
      universalThickeningCompConormalRightMap B S hS i hZ hY hfac = 0

AlgebraicGeometry.Space.exact_universalThickeningCompConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/ConormalSequenceCompositionExact.lean, line 320. The attribute's comment: “clause (2): exactness at the middle term”.

Exactness at 𝒞_{Z/X} of the conormal sequence of the composition — the middle clause of Stacks 06BD in this presentation. AlgebraicGeometry.Space.exact_conormalShortComplex_preimage is that clause for a closed subspace inside the inverse image of a closed subspace downstairs, which is what the fibre product Y ×_{Y'} Z' presents; its four comparison arguments are discharged by the structural equations above, each of them an equation of single arrows.

With AlgebraicGeometry.Space.universalThickeningCompConormalSequence_comp_eq_zero above, which supplies the vanishing the short complex is formed from, this is the middle-exactness assertion of clause (2) of Stacks 06BF; the companion clauses of that tag are registered in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningComposition.lean.

public theorem exact_universalThickeningCompConormalSequence :
    (ShortComplex.mk _ _
      (universalThickeningCompConormalSequence_comp_eq_zero B S hS i hZ hY hfac)).Exact

AlgebraicGeometry.Space.universalThickeningCompMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningComposition.lean, line 198. The attribute's comment: “clause (1): the morphism Z' ⟶ Y'”.

Stacks 06BF, clause (1), the morphism Z' ⟶ Y'. Let Z ⊂ Z' be a universal first-order thickening of Z over X and let Y ⊂ Y' be a universal first-order thickening of Y over X, and let the structure morphism of Z factor through Y. The morphism h : Z' ⟶ Y' is the canonical morphism of Stacks 060A for the square with g = 𝟙 X, that is the unique morphism restricting to i : Z ⟶ Y and lying over X.

noncomputable def universalThickeningCompMap : Z' ⟶ Y'

AlgebraicGeometry.Space.isUniversalFirstOrderThickening_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningComposition.lean, line 272. The attribute's comment: “clause (1): Y ×_{Y'} Z' is the universal first-order thickening of Z over Y, the square-zero condition inside the fibre product being hypothesised”.

Stacks 06BF, clause (1), the universal first-order thickening of Z over Y. With the morphism h : Z' ⟶ Y' of AlgebraicGeometry.Space.universalThickeningCompMap, the fibre product Y ×_{Y'} Z' is a universal first-order thickening of Z over Y, with structure morphism the projection to Y.

A morphism T' ⟶ Y ×_{Y'} Z' is a pair of morphisms to Y and to Z' agreeing over Y'. Given a solid diagram over Y built from a first-order thickening T ⊂ T' and a morphism T ⟶ Z, the morphism to Y is the one the diagram supplies and the morphism e : T' ⟶ Z' is the unique one furnished by the universal property of Z ⊂ Z' over X. That the two agree over Y' is uniqueness in the universal property of Y ⊂ Y': both composites restrict to Z ⟶ Y on T and lie over X, the first because h restricts to i and lies over X. Uniqueness of the resulting morphism is uniqueness of e together with the fact that the inclusion of the fibre product into Z' is a monomorphism.

That the copy of Z is a first-order thickening of Y ×_{Y'} Z' is a hypothesis; see the implementation notes of this file.

theorem isUniversalFirstOrderThickening_comp
    (hfirst : IsFirstOrderThickening B S hS
      (universalThickeningCompFibre B S hS i hZ hY hfac)
      (universalThickeningCompSub B S hS i hZ hY hfac)) :
    IsUniversalFirstOrderThickening B S hS
      (universalThickeningCompSub B S hS i hZ hY hfac)
      (universalThickeningCompStructure B S hS i hZ hY hfac)

AlgebraicGeometry.Space.epi_conormalMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningComposition.lean, line 306. The attribute's comment: “clause (2): exactness at the right term, the canonical map 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} being surjective”.

Stacks 06BF, clause (2), at the right term. The canonical map 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of Stacks 04CP — the right-hand map of the conormal sequence of the composition — is surjective.

By Stacks 0607 the conormal module of a formally unramified morphism is the conormal module of its source inside its universal first-order thickening, so 𝒞_{Z/X} is the conormal module of Z in Z' and, by clause (1), 𝒞_{Z/Y} is the conormal module of the copy of Z inside Y ×_{Y'} Z'. The map between them is the one of Stacks 04CP for the inclusion Y ×_{Y'} Z' ⟶ Z', and surjectivity is the surjectivity clause of Stacks 04CQ, AlgebraicGeometry.Space.epi_conormalMap, for that inverse-image configuration.

The left-hand map of the sequence is AlgebraicGeometry.Space.universalThickeningConormalMap for the square of AlgebraicGeometry.Space.universalThickeningComp_square; exactness in the middle is not proved, see the "What is not proved" section of this file.

theorem epi_conormalMap_comp :
    Epi (conormalMap B S hS
      (preimageSubspace B S hS
        (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)
      ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩
      (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
      (preimageProjection B S hS
        (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)
      (conormalEtaleRestrictionSquare B S hS
        (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩))

AlgebraicGeometry.Space.isUniversalFirstOrderThickening_comp', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningCompositionComplex.lean, line 155. The attribute's comment: “clause (1): Y ×_{Y'} Z' is the universal first-order thickening of Z over Y”.

Stacks 06BF, clause (1), the universal first-order thickening of Z over Y. With the morphism h : Z' ⟶ Y' of AlgebraicGeometry.Space.universalThickeningCompMap, the fibre product Y ×_{Y'} Z' is a universal first-order thickening of Z over Y, with structure morphism the projection to Y.

A morphism T' ⟶ Y ×_{Y'} Z' is a pair of morphisms to Y and to Z' agreeing over Y'. Given a solid diagram over Y built from a first-order thickening T ⊂ T' and a morphism T ⟶ Z, the morphism to Y is the one the diagram supplies and the morphism e : T' ⟶ Z' is the unique one furnished by the universal property of Z ⊂ Z' over X. That the two agree over Y' is uniqueness in the universal property of Y ⊂ Y': both composites restrict to Z ⟶ Y on T and lie over X, the first because h restricts to i and lies over X. Uniqueness of the resulting morphism is uniqueness of e together with the fact that the inclusion of the fibre product into Z' is a monomorphism.

That the copy of Z is a first-order thickening of Y ×_{Y'} Z' needs nothing of the fibre product: it is the inverse image of Z ⊂ Z' along the inclusion Y ×_{Y'} Z' ⟶ Z', so it is one by the inverse-image clause of Stacks 09ZX, AlgebraicGeometry.Space.isFirstOrderThickening_preimage.

theorem isUniversalFirstOrderThickening_comp' :
    IsUniversalFirstOrderThickening B S hS
      (universalThickeningCompSub B S hS i hZ hY hfac)
      (universalThickeningCompStructure B S hS i hZ hY hfac)

AlgebraicGeometry.Space.universalThickeningConormalMap_comp_conormalMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningCompositionComplex.lean, line 236. The attribute's comment: “clause (2): the sequence is a complex, the composite of i^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} and 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} being zero”.

Stacks 06BF, clause (2): the sequence is a complex. The composite of the two maps i^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of the conormal sequence of the composition is zero.

The left-hand map is the inverse image, along the projection of the copy of Z inside Y ×_{Y'} Z', of the canonical map of Stacks 060A at the square of AlgebraicGeometry.Space.universalThickeningComp_square, and the right-hand map is the map of Stacks 04CP for the inclusion Y ×_{Y'} Z' ⟶ Z'. So the composite is the conormal map of the outer rectangle of those two stacked squares, by part (3) of Stacks 04G2, and the ambient morphism of that rectangle is Y ×_{Y'} Z' ⟶ Z' ⟶ Y', which factors through the inclusion of Y by AlgebraicGeometry.Space.universalThickeningCompFibreInclusion_comp_map. A conormal map whose ambient morphism factors through the lower closed subspace is zero, the defining ideal of that subspace being the kernel of the comorphism of its inclusion; that is AlgebraicGeometry.Space.comp_conormalMap_eq_zero_of_factors.

The left-hand map is written here as that map of Stacks 04CP rather than as AlgebraicGeometry.Space.universalThickeningConormalMap; the two are the same morphism, by AlgebraicGeometry.Space.universalThickeningCompConormalMap_eq. Writing it the second way makes the statement one the kernel cannot check: the definitional comparison would then sit inside the inverse image of modules and inside a composition, which is exactly what the implementation notes of StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeEpi.lean record as beyond the budget.

A consumer wanting the arrows of this sequence should take them from this theorem, as CategoryTheory.ShortComplex.f and CategoryTheory.ShortComplex.g of CategoryTheory.ShortComplex.mk _ _ applied to it, which is what AlgebraicGeometry.Space.universalThickeningCompConormalSequence_shortExact', Stacks 06CC, does. Crossing the two spellings by rewriting with AlgebraicGeometry.Space.universalThickeningCompConormalMap_eq is not an available route once the arrow sits under the inverse image of modules, and neither is naming either arrow in a definition of its own — the section How the sequence is written of the file of that theorem records what each of those costs.

theorem universalThickeningConormalMap_comp_conormalMap_eq_zero :
    (modulePullback B S hS
          (preimageProjection B S hS
            (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
            ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)).map
        (conormalMap B S hS ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩
          ⟨Y, (IsNthOrderThickening.isThickening B S hS hY.firstOrder).1⟩
          (universalThickeningCompMap B S hS i hZ hY hfac)
          (ObjectProperty.homMk i)
          (universalThickeningComp_subspace_square B S hS i hZ hY hfac)) ≫
      conormalMap B S hS
        (preimageSubspace B S hS
          (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
          ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩
        (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
        (preimageProjection B S hS
          (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
          ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩)
        (conormalEtaleRestrictionSquare B S hS
          (universalThickeningCompFibreInclusion B S hS i hZ hY hfac)
          ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩) = 0

AlgebraicGeometry.Space.exact_and_epi_universalThickeningCompConormalMapSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningCompositionExact.lean, line 89. The attribute's comment: “clause (2): the conormal sequence i^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 is exact”.

Stacks 06BF, clause (2). Let Z ⟶ Y ⟶ X be morphisms of algebraic spaces, Z ⊂ Z' and Y ⊂ Y' universal first-order thickenings over X, and h : Z' ⟶ Y' the morphism of clause (1). The conormal sequence

i^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0

is exact: exact at 𝒞_{Z/X}, and its right-hand map is an epimorphism. Here 𝒞_{Z/X} is the conormal module of Z ⊂ Z', 𝒞_{Y/X} that of Y ⊂ Y', and 𝒞_{Z/Y} that of the copy of Z inside the universal first-order thickening Y ×_{Y'} Z' = h⁻¹(Y) of clause (1); the two maps are those of Stacks 04CP, for the square of Z ⊆ Z' over Y ⊆ Y' with ambient morphism h (pulled back to the copy of Z) and for the inclusion h⁻¹(Y) ⟶ Z'. They are the arrows of AlgebraicGeometry.Space.universalThickeningConormalMap_comp_conormalMap_eq_zero, by AlgebraicGeometry.Space.universalThickeningCompConormalSequence_f_eq and ..._g_eq.

Exactness in the middle is AlgebraicGeometry.Space.exact_conormalMap_square at that square; the epimorphism is the surjectivity clause of Stacks 04CQ for the inclusion h⁻¹(Y) ⟶ Z'.

theorem exact_and_epi_universalThickeningCompConormalMapSquare :
    (ShortComplex.mk _ _ (conormalMap_square_comp_eq_zero B S hS
        (universalThickeningCompMap B S hS i hZ hY hfac)
        ⟨Y, (IsNthOrderThickening.isThickening B S hS hY.firstOrder).1⟩
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩
        (ObjectProperty.homMk i)
        (universalThickeningComp_subspace_square B S hS i hZ hY hfac))).Exact ∧
      Epi (ShortComplex.mk _ _ (conormalMap_square_comp_eq_zero B S hS
        (universalThickeningCompMap B S hS i hZ hY hfac)
        ⟨Y, (IsNthOrderThickening.isThickening B S hS hY.firstOrder).1⟩
        ⟨Z, (IsNthOrderThickening.isThickening B S hS hZ.firstOrder).1⟩
        (ObjectProperty.homMk i)
        (universalThickeningComp_subspace_square B S hS i hZ hY hfac))).g

Sources

• Section 76.15, Tag 0601
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsUniversalFirstOrderThickening · AlgebraicGeometry.Space.IsUniversalFirstOrderThickening' · AlgebraicGeometry.Space.isUniversalFirstOrderThickening_iff_affine_lifting · AlgebraicGeometry.Space.HasRepresentableLiftingProperty · AlgebraicGeometry.Space.HasAffineLiftingProperty · AlgebraicGeometry.Space.isUniversalFirstOrderThickening_iff_representable · AlgebraicGeometry.Space.HasRepresentableLiftingProperty.hasAffineLiftingProperty · AlgebraicGeometry.Space.IsUniversalFirstOrderThickening.comp_formallyEtale

Section76.16 Formally étale morphisms#

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

Tag 04GC, a definition

Tag 04GC in the Stacks Project.

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

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

public abbrev FormallyEtale {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) : Prop

Tag 04GD, a lemma

Tag 04GD in the Stacks Project.

AlgebraicGeometry.Space.formallyEtale_iff_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleChartCriterion.lean, line 130. The attribute's comment: “condition (2)”.

Stacks 04GD, the equivalence of (1) and (2). A morphism of algebraic spaces over S is formally étale exactly when the morphism of schemes underlying every commuting square of étale scheme charts is formally étale.

theorem formallyEtale_iff_etaleCharts
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallyEtale f ↔
      HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyEtale.{u} : MorphismProperty Scheme.{u}) f

AlgebraicGeometry.Space.formallyEtale_iff_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleChartCriterion.lean, line 147. The attribute's comment: “condition (3)”.

Stacks 04GD, the equivalence of (1) and (3). A morphism of algebraic spaces over S is formally étale exactly when there is one commuting square of étale scheme charts, both chart maps surjective, whose underlying morphism of schemes is formally étale.

theorem formallyEtale_iff_surjectiveEtaleChart
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallyEtale f ↔
      ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (ψ : U ⟶ V),
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Etale.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u} : MorphismProperty
          Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf b ∧
        yoneda.map ψ ≫ b = a ≫ f ∧
        _root_.AlgebraicGeometry.FormallyEtale
          ((BigFppfOver.toScheme B S hS).map ψ)

Tag 0611, a lemma

Tag 0611 in the Stacks Project.

AlgebraicGeometry.Space.FormallyEtale.existsUnique_lift_of_firstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FormallyEtale.lean, line 312.

Stacks 0611. A formally étale morphism f : X ⟶ Y of algebraic spaces over S admits exactly one dotted arrow in a solid square over a first-order thickening T ⊂ T' of algebraic spaces over S. No affineness is assumed of either space of the thickening: the affineness of the test objects in the definition of formal étaleness, Stacks 049S part (2), may be dropped.

theorem FormallyEtale.existsUnique_lift_of_firstOrderThickening
    {X Y T' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : FormallyEtale f.hom)
    (T : Subfunctor T'.obj) (hT : IsFirstOrderThickening B S hS T' T)
    (a : T.toFunctor ⟶ X.obj) (b : T'.obj ⟶ Y.obj) (hsq : a ≫ f.hom = T.ι ≫ b) :
    ∃! c : T'.obj ⟶ X.obj, T.ι ≫ c = a ∧ c ≫ f.hom = b

Tag 0612, a lemma

Tag 0612 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.formallyEtale_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Spaces.lean, line 66 (StacksFrontier).

Tag 0613, a lemma

Tag 0613 in the Stacks Project.

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

Stacks 0613. A base change of a formally étale morphism of algebraic spaces over S is formally étale: if fst, snd, f, g is a cartesian square of algebraic spaces over S and f is formally étale, then so is snd.

public theorem formallyEtale_of_isPullback (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y Z W : AlgebraicSpaces B S hS} {f : X ⟶ Z} {g : Y ⟶ Z}
    {fst : W ⟶ X} {snd : W ⟶ Y} (sq : IsPullback fst snd f g)
    (hf : FormallyEtale f.hom) : FormallyEtale snd.hom

Declarations registered for the tag:

• AlgebraicGeometry.Space.formallyEtale_baseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Spaces.lean, line 70 (StacksFrontier).

Tag 0614, a lemma

Tag 0614 in the Stacks Project.

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

Stacks 0614, the equivalence of (1) and (2). A morphism f : X ⟶ Y of algebraic spaces over S admitting a universal first order thickening X ⊂ X' over Y is formally étale exactly when that thickening is trivial, that is when the smaller space is the whole of X'.

The formal unramifiedness of f which clause (2) of the source states alongside the triviality of the thickening is part of the datum of Stacks 0607 and so does not appear; see the implementation notes.

theorem formallyEtale_iff_sub_eq_top (t : UniversalFirstOrderThickening B S hS f) :
    FormallyEtale f.hom ↔ t.sub = ⊤

AlgebraicGeometry.Space.isZero_conormalSheaf_of_sub_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 358. The attribute's comment: “(2) implies (3)”.

Stacks 0614, (2) implies (3). If the smaller space of a universal first order thickening of X over Y is the whole ambient space, then the conormal sheaf 𝒞_{X/Y} of Stacks 0607 vanishes.

The inclusion of the smaller space is then invertible, so it is retracted by its inverse and the defining ideal of the smaller space vanishes on every étale chart. The conormal sheaf is an inverse image of that ideal sheaf along two morphisms of algebraic spaces, and an inverse image of modules preserves zero objects, being a left adjoint.

theorem isZero_conormalSheaf_of_sub_eq_top (t : UniversalFirstOrderThickening B S hS f)
    (hsub : t.sub = ⊤) : IsZero (conormalSheaf B S hS t)

AlgebraicGeometry.Space.sub_eq_top_of_isZero_conormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 410. The attribute's comment: “(3) implies (2)”.

Stacks 0614, (3) implies (2). If the conormal sheaf 𝒞_{X/Y} of Stacks 0607 vanishes then the smaller space of the universal first order thickening is the whole ambient space.

This is where Stacks 04CN, part (3) is spent, in the only form the argument needs: for a first-order thickening the unit 𝓘 ⟶ i_*i^*𝓘 of i^* ⊣ i_* is an isomorphism — the identification 𝓘/𝓘² = 𝓘 of the source, which AlgebraicGeometry.Space.firstOrderConormalModuleIso supplies from the essential-image clause of Stacks 04CJ — so the vanishing of the conormal module forces the defining ideal of X in X' to vanish on every étale chart. The injectivity clause of Stacks 03MB (AlgebraicGeometry.Space.le_of_definingIdealSheaf_le) then returns t.sub = ⊤.

It is the converse of AlgebraicGeometry.Space.isZero_conormalSheaf_of_sub_eq_top, and the two are the content of the equivalence of clauses (2) and (3) of Stacks 0614. Composed with AlgebraicGeometry.Space.formallyEtale_iff_sub_eq_top it derives clause (1) from clause (3) as well, which is what closes the equivalence of (3) with the other clauses. The formal unramifiedness that clause (3) states alongside the vanishing of the conormal sheaf is part of the datum of Stacks 0607 and so does not appear; see the implementation notes.

theorem sub_eq_top_of_isZero_conormalSheaf (t : UniversalFirstOrderThickening B S hS f)
    (h : IsZero (conormalSheaf B S hS t)) : t.sub = ⊤

AlgebraicGeometry.Space.formallyEtale_of_isZero_sheafOfDifferentials_of_isZero_conormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 571. The attribute's comment: “(4) implies (1), for the datum of Stacks 0607”.

Stacks 0614, (4) implies (1), for the datum of Stacks 0607. If the sheaf of differentials Ω_{X/Y} of Stacks 04CT and the conormal sheaf 𝒞_{X/Y} of Stacks 0607 both vanish, then f : X ⟶ Y is formally étale.

The formallyUnramified field of the datum t is not an extra hypothesis: it is a consequence of the universal property that the rest of t carries, by AlgebraicGeometry.Space.formallyUnramified_of_isUniversal. The form of this implication in which that field never appears is AlgebraicGeometry.Space.formallyEtale_of_isZero_conormalSheaf_of_isUniversal, and this statement follows from it; it is kept because t is the shape every other clause of the tag is stated in.

The Ω_{X/Y} = 0 conjunct is again not consumed, for the reason recorded there: the datum already forces it.

theorem formallyEtale_of_isZero_sheafOfDifferentials_of_isZero_conormalSheaf
    (t : UniversalFirstOrderThickening B S hS f)
    (h : IsZero (sheafOfDifferentials B S hS f) ∧ IsZero (conormalSheaf B S hS t)) :
    FormallyEtale f.hom

AlgebraicGeometry.Space.isZero_sheafOfDifferentials_and_isZero_conormalSheaf_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 592. The attribute's comment: “(3) implies (4), hence also (1) implies (4) and (2) implies (4) through the proved equivalence of (1), (2) and (3)”.

Stacks 0614, (3) implies (4). If f : X ⟶ Y is formally unramified and the conormal sheaf 𝒞_{X/Y} of Stacks 0607 vanishes, then the sheaf of differentials Ω_{X/Y} of Stacks 04CT vanishes too and so does 𝒞_{X/Y}.

Since clauses (1), (2) and (3) are mutually equivalent outright — by AlgebraicGeometry.Space.formallyEtale_iff_sub_eq_top, AlgebraicGeometry.Space.isZero_conormalSheaf_of_sub_eq_top and AlgebraicGeometry.Space.sub_eq_top_of_isZero_conormalSheaf — this is at the same time the implication from clause (1) and the implication from clause (2).

The content is the forward direction of Stacks 04G9, which is available with no assumed input as AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_formallyUnramified; the second conjunct is carried through unchanged.

theorem isZero_sheafOfDifferentials_and_isZero_conormalSheaf_of_formallyUnramified
    (t : UniversalFirstOrderThickening B S hS f)
    (h : FormallyUnramified f.hom ∧ IsZero (conormalSheaf B S hS t)) :
    IsZero (sheafOfDifferentials B S hS f) ∧ IsZero (conormalSheaf B S hS t)

AlgebraicGeometry.Space.formallyEtale_tfae_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 750. The attribute's comment: “the equivalence of the four conditions, with no hypotheses: Stacks 0606 supplies the universal first order thickening”.

Stacks 0614, with no hypotheses at all. Let f : X ⟶ Y be a morphism of algebraic spaces over S. Then the four conditions

1. f is formally étale,
2. f is formally unramified and the universal first order thickening of X over Y is X,
3. f is formally unramified and 𝒞_{X/Y} = 0,
4. Ω_{X/Y} = 0 and 𝒞_{X/Y} = 0

are equivalent. Nothing is assumed about f: no universal first order thickening is a parameter, and no formal unramifiedness is a hypothesis.

How the thickening leaves the hypotheses. Stacks 0607 defines 𝒞_{X/Y} relative to a universal first order thickening, so 𝒞_{X/Y} = 0 is a statement quantified over those thickenings; AlgebraicGeometry.Space.forall_isZero_conormalSheaf_iff_exists shows the two quantifiers agree for a formally unramified f, which is the source's definite article. The quantifier written in each clause is the one the source's own reading of that clause supplies: clauses (2) and (3) state formal unramifiedness, from which Stacks 0606 produces the thickening, so they are read with ∀; clause (4) does not, and the source's remark that it "only makes sense because Ω_{X/Y} = 0 implies that 𝒞_{X/Y} is defined" is exactly the assertion that a thickening exists, so it is read with ∃.

Where Stacks 0606 is spent. In the step from (3) to (4), to produce the thickening whose conormal sheaf the existential of clause (4) names: AlgebraicGeometry.Space.nonempty_universalFirstOrderThickening of StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalExistence.lean. This is what the earlier statements of this file carried as a parameter.

The backward direction of Stacks 04G9 is still not used, and is not needed. The source gets formal unramifiedness out of clause (4) through it. Here clause (4) carries a thickening in its existential instead, and a thickening forces formal unramifiedness by AlgebraicGeometry.Space.formallyUnramified_of_isUniversal — which is also why the step from (4) to (1) needs nothing beyond the equivalence of (1) and (3).

theorem formallyEtale_tfae_unconditional :
    List.TFAE
      [FormallyEtale f.hom,
        FormallyUnramified f.hom ∧
          ∀ t : UniversalFirstOrderThickening B S hS f, t.sub = ⊤,
        FormallyUnramified f.hom ∧
          ∀ t : UniversalFirstOrderThickening B S hS f, IsZero (conormalSheaf B S hS t),
        IsZero (sheafOfDifferentials B S hS f) ∧
          ∃ t : UniversalFirstOrderThickening B S hS f, IsZero (conormalSheaf B S hS t)]

AlgebraicGeometry.Space.formallyEtale_iff_isZero_sheafOfDifferentials_and_exists_isZero_conormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalThickeningFormallyEtale.lean, line 781. The attribute's comment: “the equivalence of (1) and (4), with no hypotheses”.

Stacks 0614, the equivalence of (1) and (4), with no hypotheses. A morphism f : X ⟶ Y of algebraic spaces over S is formally étale exactly when the sheaf of differentials Ω_{X/Y} of Stacks 04CT vanishes and X admits a universal first order thickening over Y whose conormal sheaf 𝒞_{X/Y} of Stacks 0607 vanishes.

The existential is the source's reading of clause (4), whose remark on that clause is that 𝒞_{X/Y} has to be defined before the clause says anything; see AlgebraicGeometry.Space.formallyEtale_tfae_unconditional, of which this is the instance at indices 1 and 4.

theorem formallyEtale_iff_isZero_sheafOfDifferentials_and_exists_isZero_conormalSheaf :
    FormallyEtale f.hom ↔
      IsZero (sheafOfDifferentials B S hS f) ∧
        ∃ t : UniversalFirstOrderThickening B S hS f, IsZero (conormalSheaf B S hS t)

Tag 0615, a lemma

Tag 0615 in the Stacks Project.

AlgebraicGeometry.Space.formallyEtale_of_isUnramified_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleChartCriterion.lean, line 177.

Stacks 0615. A flat unramified morphism of algebraic spaces over S is formally étale.

Unramifiedness and flatness are conditions on the étale charts of the morphism, and on each chart Tag 04FF makes the morphism of schemes formally étale; Tag 04GD assembles those into formal étaleness of the morphism of algebraic spaces.

theorem formallyEtale_of_isUnramified_of_isFlat
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hu : IsUnramified B S hS f) (hflat : IsFlat B S hS f) :
    FormallyEtale f

Tag 0616, a lemma

Tag 0616 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_iff_isLocallyOfFinitePresentation_and_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleChartCriterion.lean, line 195. References: EGA IV (17.6.1), “a) <=> d)”.

Stacks 0616. A morphism of algebraic spaces over S is étale if and only if it is locally of finite presentation and formally étale.

All three conditions are conditions on the same squares of étale scheme charts — étaleness by Tag 03XT, local finite presentation by Tag 03XP and formal étaleness by Tag 04GD — so the statement is the scheme-level equivalence of Tag 02HM quantified over the charts, together with the distribution of a universal quantifier over a conjunction.

theorem isEtale_iff_isLocallyOfFinitePresentation_and_formallyEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsEtale B S hS f ↔ (IsLocallyOfFinitePresentation B S hS f ∧ FormallyEtale f)

Sources

• Section 76.16, Tag 04GB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.FormallyEtale · AlgebraicGeometry.Space.formallyEtale_iff_etaleCharts · AlgebraicGeometry.Space.formallyEtale_iff_surjectiveEtaleChart · AlgebraicGeometry.Space.FormallyEtale.existsUnique_lift_of_firstOrderThickening · AlgebraicGeometry.Space.formallyEtale_comp · AlgebraicGeometry.Space.formallyEtale_of_isPullback · AlgebraicGeometry.Space.formallyEtale_baseChange · AlgebraicGeometry.Space.formallyEtale_iff_sub_eq_top

Section76.17 Infinitesimal deformations of maps#

Section 76.17 of the Stacks Project, Tag 0617. 11 tags here are carried by 66 declarations of the repository (all in StacksFrontier) and 14 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0617, the section

Tag 0617 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.exists_derivation_of_conormalMap_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 90 (StacksFrontier): “Lemma 0618 of the section: two morphisms of first order thickenings over B with a = b and the same map of conormal modules differ by an 𝒪_B-derivation D”.
• AlgebraicGeometry.Space.derivationDirectImageEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 94 (StacksFrontier): “Equation 0619 of the section: the bijection θ ↔ D = d_{Y/B} ∘ θ between maps a^Ω_{Y/B} ⟶ C and 𝒪_B-derivations 𝒪_Y ⟶ a_C”.
• AlgebraicGeometry.Space.derivationDirectImageEquiv_apply, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 98 (StacksFrontier): “Equation 0619 of the section: the derivation attached to θ is d_{Y/B} followed by the transpose of θ”.
• AlgebraicGeometry.Space.existsUnique_hom_conormalMap_eq_derivation_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 102 (StacksFrontier): “Lemma 04D0 of the section: θ moves (a, a') to a unique morphism of pairs (a, b') with the same map of conormal modules and D = d_{Y/B} ∘ θ”.
• AlgebraicGeometry.Space.derivationMove_spec, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 106 (StacksFrontier): “Remark 0CK6 of the section: the action θ · a', whose comorphism differs from that of a' by the derivation related to θ by Equation 0619”.
• AlgebraicGeometry.Space.conormalLiftSubfunctor, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 110 (StacksFrontier): “Equation 061B of the section: the rule U' ↦ {a' : U' → Y' such that (1), (2), (3) hold} on (X')_{spaces, étale}, with restriction a' ↦ a'|_{V'}”.
• AlgebraicGeometry.Space.isSheaf_conormalLiftSubfunctor, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 114 (StacksFrontier): “Lemma 061A of the section: the rule of Equation 061B is a sheaf of sets on (X')_{spaces, étale}”.
• AlgebraicGeometry.Space.isSheaf_conormalLiftActingPresheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 118 (StacksFrontier): “Lemma 061C of the section: the sheaf SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}), read on (X')_{spaces, étale} through 05ZL, which acts”.
• AlgebraicGeometry.Space.conormalLiftSheafAddAction, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 122 (StacksFrontier): “Lemma 061C of the section: the action on the sections of the sheaf 061B”.
• AlgebraicGeometry.Space.conormalLiftAction_map, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 125 (StacksFrontier): “Lemma 061C of the section: the action commutes with restriction”.
• AlgebraicGeometry.Space.conormalLiftSheafAddAction_bijective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 128 (StacksFrontier): “Lemma 061C of the section: the action is simply transitive over every U' over which the sheaf 061B has a section”.
• AlgebraicGeometry.Space.liftSubfunctor_remark_of_eq_top, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 132 (StacksFrontier): “Remark 061D of the section: for Y = Y' the map A is zero, the sheaf of 061A is U' ↦ {a' : U' → Y over B with a'|_U = a|_U}, and SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}) acts on it”.
• AlgebraicGeometry.Space.liftSubfunctor_remark_of_cartesian, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 136 (StacksFrontier): “Remark 0CK7 of the section: for a base thickening Z ⊂ Z' and Y = Z ×_{Z'} Y' the map A is determined by a, the sheaf of 061A is U' ↦ {a' : U' → Y' over Z' with a'|_U = a|_U}, and SheafHom_{O_X}(a^*Ω_{Y/Z}, C_{X/X'}) acts on it”.
• AlgebraicGeometry.Space.derivationMove_comp_of_etale, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InfinitesimalDeformationsOfMaps.lean, line 141 (StacksFrontier): “Lemma 0CK8 of the section: for X₂ → X₁ and B₂ → B₁ étale the action is compatible with étale localization, (θ₂ · a₂') ≫ f' = h' ≫ (θ₁ · a₁')”.

Tag 0618, a lemma

Tag 0618 in the Stacks Project.

AlgebraicGeometry.Space.liftDifferenceDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceBundledDerivation.lean, line 127. The attribute's comment: “the derivation D of the source, bundled as a PresheafOfModulesOfCommRing.Derivation', for two abstract algebra maps”.

The difference of two lifts, as a bundled derivation. For f, g : R ⟶ 𝒪_X which agree after the structure map of a first-order thickening Z ⊆ X and which agree on a base sheaf of rings R₀, the sectionwise difference f - g is a Derivation' of R over R₀ with values in the defining ideal of Z.

Its four fields are AlgebraicGeometry.Space.liftDifference_add, AlgebraicGeometry.Space.liftDifference_smul_add_smul, AlgebraicGeometry.Space.liftDifference_naturality and AlgebraicGeometry.Space.liftDifference_app_eq_zero.

noncomputable def liftDifferenceDerivation (hZ : IsFirstOrderThickening B S hS X Z.1)
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (hφ : (sheafCompose (SmallEtale.topology B S hS X.1)
          (forget₂ CommRingCat.{u} RingCat.{u})).map φc ≫ f =
      (sheafCompose (SmallEtale.topology B S hS X.1)
          (forget₂ CommRingCat.{u} RingCat.{u})).map φc ≫ g) :
    PresheafOfModulesOfCommRing.Derivation' (liftDifferenceCoefficients B S hS Z f) φc.hom

AlgebraicGeometry.Space.liftPairDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceBundledDerivation.lean, line 182. The attribute's comment: “the derivation D of the source, bundled, for the two structure maps of two morphisms of a thickening agreeing on its closed subspace”.

The derivation D of [Stacks Project, Tag 0618]. Let G ⊂ X' be a first-order thickening of algebraic spaces with inclusion i : X ⟶ X' and let a', b' : X' ⟶ Y' be two morphisms with i ≫ a' = i ≫ b', both of them maps of R₀-algebras for a sheaf of commutative rings R₀ on the small étale site of X' — for two morphisms of thickenings over B the last condition is that both are maps of 𝒪_B-algebras. Then the difference of the two structure maps (a')^♯, (b')^♯ : (b')^{-1}𝒪_{Y'} ⟶ 𝒪_{X'}, the first read through AlgebraicGeometry.Space.commRingInverseImageIsoOfRestrictEq, is a derivation of (b')^{-1}𝒪_{Y'} over R₀ with values in the defining ideal of the thickening.

This is AlgebraicGeometry.Space.liftDifferenceDerivation at the pair of structure maps supplied by AlgebraicGeometry.Space.inverseImageStructureSharpOfRestrictEq_comp_structureSharp.

noncomputable def liftPairDerivation (hZ : IsFirstOrderThickening B S hS X' G)
    (hφ : (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map φc ≫
          (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map
            (inverseImageStructureSharpOfRestrictEq B S hS hG a' b' h) =
      (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map φc ≫
          (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map
            (structureSharpInverseImage B S hS b')) :
    PresheafOfModulesOfCommRing.Derivation' (liftDifferenceCoefficients B S hS ⟨G, hG.1⟩
        ((sheafCompose (SmallEtale.topology B S hS X'.1)
          (forget₂ CommRingCat.{u} RingCat.{u})).map
          (inverseImageStructureSharpOfRestrictEq B S hS hG a' b' h))) φc.hom

AlgebraicGeometry.Space.liftDifference, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 93. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The difference of two maps into the structure sheaf which agree on a closed subspace: if f, g : R ⟶ 𝒪_X become equal after the structure map i^♯ : 𝒪_X ⟶ i_*𝒪_Z of the inclusion of a closed subspace Z ⊆ X, the sectionwise difference f - g, as a section of the defining ideal of Z, the sectionwise kernel of i^♯.

noncomputable def liftDifference
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (U : (SmallEtale B S hS X.1)ᵒᵖ) (r : R.obj.obj U) :
    definingIdealAt B S hS X Z U

AlgebraicGeometry.Space.liftDifference_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 122. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The difference of two lifts is additive.

theorem liftDifference_add
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (U : (SmallEtale B S hS X.1)ᵒᵖ) (r s : R.obj.obj U) :
    liftDifference B S hS Z f g hfg U (r + s) =
      liftDifference B S hS Z f g hfg U r + liftDifference B S hS Z f g hfg U s

AlgebraicGeometry.Space.liftDifference_smul_add_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 149. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The Leibniz rule for the difference D of two lifts into a first-order thickening, for the R-action on the defining ideal obtained by restricting scalars along f: D (r * s) = f r • D s + f s • D r.

theorem liftDifference_smul_add_smul (hZ : IsFirstOrderThickening B S hS X Z.1)
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (U : (SmallEtale B S hS X.1)ᵒᵖ) (r s : R.obj.obj U) :
    liftDifference B S hS Z f g hfg U (r * s) =
      f.hom.app U r • liftDifference B S hS Z f g hfg U s +
        f.hom.app U s • liftDifference B S hS Z f g hfg U r

AlgebraicGeometry.Space.liftDifference_app_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 176. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

If the two maps agree on R₀, their difference vanishes on sections coming from R₀.

theorem liftDifference_app_eq_zero
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (hφ : φ ≫ f = φ ≫ g) (U : (SmallEtale B S hS X.1)ᵒᵖ) (r : R₀.obj.obj U) :
    liftDifference B S hS Z f g hfg U (φ.hom.app U r) = 0

AlgebraicGeometry.Space.liftDifference_eq_zero_of_apply_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 186. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The difference of two lifts annihilates a section on which the two maps agree.

theorem liftDifference_eq_zero_of_apply_eq
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    {U : (SmallEtale B S hS X.1)ᵒᵖ} {r : R.obj.obj U}
    (hr : f.hom.app U r = g.hom.app U r) :
    liftDifference B S hS Z f g hfg U r = 0

AlgebraicGeometry.Space.liftDifference_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 196. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The difference of two lifts commutes with the restriction maps of the small étale site.

theorem liftDifference_naturality
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    {U V : (SmallEtale B S hS X.1)ᵒᵖ} (h : U ⟶ V) (r : R.obj.obj U) :
    ((structureRingSheaf B S hS X).obj.map h).hom
        ((liftDifference B S hS Z f g hfg U r : definingIdealAt B S hS X Z U) :
          (structureRingSheaf B S hS X).obj.obj U) =
      ((liftDifference B S hS Z f g hfg V ((R.obj.map h).hom r) :
        definingIdealAt B S hS X Z V) : (structureRingSheaf B S hS X).obj.obj V)

AlgebraicGeometry.Space.firstOrderConormalModuleι_liftDifference, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LiftDifferenceDerivation.lean, line 215. The attribute's comment: “the derivation, for two abstract algebra maps; no descent to 𝒪_Y”.

The difference of two lifts into a first-order thickening, carried into the pushed-forward conormal module i_*𝒞_{Z/X} by AlgebraicGeometry.Space.firstOrderConormalModuleIso and included back into 𝒪_X by AlgebraicGeometry.Space.firstOrderConormalModuleι, is f - g.

theorem firstOrderConormalModuleι_liftDifference (hZ : IsFirstOrderThickening B S hS X Z.1)
    (hfg : f ≫ structureSharp B S hS (subspaceInclusion B S hS X Z) =
      g ≫ structureSharp B S hS (subspaceInclusion B S hS X Z))
    (U : (SmallEtale B S hS X.1)ᵒᵖ) (r : R.obj.obj U) :
    (firstOrderConormalModuleι B S hS Z hZ).val.app U
        ((firstOrderConormalModuleIso B S hS Z hZ).hom.val.app U
          (liftDifference B S hS Z f g hfg U r)) =
      f.hom.app U r - g.hom.app U r

AlgebraicGeometry.Space.exists_derivation_of_conormalMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/DerivationMovedLiftConormal.lean, line 232. The attribute's comment: “(a')^♯ − (b')^♯ factors as 𝒪_{Y'} → 𝒪_Y → a_𝒞_{X/X'} → a_𝒪_{X'} through an 𝒪_B-derivation D, read on the small étale site of Y”.

[Stacks Project, Tag 0618]. Let (e₀, c), (e₀, c') : (Z ⊂ X) ⟶ (W₀ ⊂ W) be two morphisms of first order thickenings over T with the same reduction e₀ (condition (1)) and the same map e₀^*𝒞_{W₀/W} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] (condition (2)). Then there is an 𝒪_T-derivation D : 𝒪_{W₀} ⟶ (e₀)_*𝒞_{Z/X} through which the difference of the comorphisms factors: read as maps j^{-1}𝒪_W ⟶ (e₀)_*(i^{-1}𝒪_X), c^♯ − (c')^♯ = ι ∘ D ∘ j^♯.

theorem exists_derivation_of_conormalMap_eq (c c' : X ⟶ W)
    (hc : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hc' : subspaceInclusion B S hS X Z ≫ c' = e₀ ≫ subspaceInclusion B S hS W W₀)
    (p : X ⟶ T) (hcq : c ≫ q = p) (hcq' : c' ≫ q = p)
    (hcon : conormalMap B S hS Z W₀ c e₀ hc = conormalMap B S hS Z W₀ c' e₀ hc') :
    ∃ D : PresheafOfModulesOfCommRing.Derivation'
        ((modulePushforward B S hS e₀).obj (conormalModule B S hS X Z)).val
        (structureSharpInverseImage B S hS (subspaceInclusion B S hS W W₀ ≫ q)).hom,
      ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : ToType ((structureRingSheafInverseImage B S hS (subspaceInclusion B S hS W
            W₀)).obj.obj V)),
        (restrictedSquareZeroValues B S hS Z W₀ e₀ hZ).ι
            (D.d (X := V) ((structureSharpRingInverseImage B S hS (subspaceInclusion B S hS W
                W₀)).hom.app V x)) =
          (restrictedSharpThroughThickening B S hS Z W₀ c e₀ hc).hom.app V x -
            (restrictedSharpThroughThickening B S hS Z W₀ c' e₀ hc').hom.app V x

AlgebraicGeometry.Space.descend_restrictedLiftDifferenceData_app_inverseImage_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceBaseVanishingPair.lean, line 110. The attribute's comment: “the descended difference of two morphisms over a base kills the functions read from that base, which is what makes it a derivation over the base”.

The descended difference of two morphisms over a base kills the functions read from that base. For c, c' : X ⟶ W agreeing on the thickening Z ⊂ X and over qb : W ⟶ Bas, the derivation their difference descends to vanishes on every section of 𝒪_{W₀} of the form j^♯(j^{-1}(qb^♯)(x)).

The two transported comorphisms agree after j^{-1}(qb^♯) — that is inverseImage_structureSharpRingInverseImage_comp_restrictedSharpThroughThickening_eq' at an arbitrary target Bas — and a difference which vanishes after a morphism into the ambient sheaf of rings descends to one vanishing on the sections that morphism accounts for, which is Stacks.Sites.LiftDifferenceData.descend_eq_zero_of_comp_eq.

This is the pair-of-morphisms counterpart of AlgebraicGeometry.Space.derivationFamilyOfHom_app_inverseImage_eq_zero.

theorem descend_restrictedLiftDifferenceData_app_inverseImage_eq_zero
    [HasSheafify (SmallEtale.topology B S hS
      (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1) AddCommGrpCat.{u}]
    (A : (SmallEtale B S hS
      (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
    (x : ToType (((smallEtaleInverseImageRing B S hS
      (subspaceInclusion B S hS W W₀)).obj
      (inverseImageStructureSheaf B S hS qb)).obj.obj A)) :
    (restrictedLiftDifferenceData B S hS Z W₀ e₀ hZ c c' h h' hker).toQuotientDerivation.descend
        ((structureSharpRingInverseImage B S hS
            (subspaceInclusion B S hS W W₀)).hom.app A
          (((inverseImageRingFunctor (smallToposMorphismTypeU B S hS
              (subspaceInclusion B S hS W W₀))).map
            (structureSharpRingInverseImage B S hS qb)).hom.app A x)) =
      0

AlgebraicGeometry.Space.descend_restrictedLiftDifferenceData_structureSharpInverseImage_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceBaseVanishingPair.lean, line 152. The attribute's comment: “the hypothesis hz of the descent, discharged: the descended difference of two morphisms over a base kills the sections read from that base along the composite”.

The descended difference of two morphisms over a base is a derivation over that base, in the shape AlgebraicGeometry.Space.liftDifferenceDifferentialsHom asks for it: it kills every section of 𝒪_{W₀} read from Bas along the composite j ≫ qb.

This is AlgebraicGeometry.Space.descend_restrictedLiftDifferenceData_app_inverseImage_eq_zero, whose sections are read through j^{-1}(qb^♯) and then j^♯, carried onto the structure map of the composite by AlgebraicGeometry.Space.app_structureSharpInverseImage_comp; the two coefficient readings of the inverse-image structure maps agree on sections by AlgebraicGeometry.Space.app_inverseImage_structureSharpRingInverseImage and AlgebraicGeometry.Space.structureSharpRingInverseImage_eq_forget₂.

Taking b := j ≫ qb for the base datum of AlgebraicGeometry.Space.liftDifferenceDifferentialsHom, this is the hypothesis hz of that descent — the second of the two vanishing conditions, the first being hypothesis (2) of [Stacks Project, Tag 0618].

theorem descend_restrictedLiftDifferenceData_structureSharpInverseImage_eq_zero
    [HasSheafify (SmallEtale.topology B S hS
      (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1) AddCommGrpCat.{u}]
    (V : (SmallEtale B S hS
      (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
    (s : ToType ((inverseImageStructureSheaf B S hS
      (subspaceInclusion B S hS W W₀ ≫ qb)).obj.obj V)) :
    (restrictedLiftDifferenceData B S hS Z W₀ e₀ hZ c c' h h' hker).toQuotientDerivation.descend
        ((structureSharpInverseImage B S hS
          (subspaceInclusion B S hS W W₀ ≫ qb)).hom.app V s) =
      0

AlgebraicGeometry.Space.restrictedLiftDifferenceHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferencePairHom.lean, line 98. The attribute's comment: “the difference of two morphisms agreeing on the thickening and over the base, as a linear map out of the pulled back differentials”.

The linear map θ : e₀^*Ω_{W₀/Bas} ⟶ 𝒞_{Z/X} by which two morphisms agreeing on the thickening and over qb differ. This is [Stacks Project, Tag 0618] together with Equation [Stacks Project, Tag 0619], in the direction from a pair of morphisms to a linear map.

The pair of comorphisms is AlgebraicGeometry.Space.restrictedLiftDifferenceData and the descent is AlgebraicGeometry.Space.liftDifferenceDifferentialsHom; its two hypotheses are the datum's own hker and AlgebraicGeometry.Space.descend_restrictedLiftDifferenceData_structureSharpInverseImage_eq_zero.

abbrev restrictedLiftDifferenceHom (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h' : subspaceInclusion B S hS X Z ≫ c' = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hker : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c' e₀ h').hom.app V x)
    (hcc : c ≫ qb = c' ≫ qb) :
    (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ qb)) ⟶
      conormalModule B S hS X Z

AlgebraicGeometry.Space.restrictedLiftDifferenceHom_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferencePairHom.lean, line 185. The attribute's comment: “a morphism does not differ from itself: the linear map of the pair (c, c) is zero”.

A morphism does not differ from itself: the linear map of the pair (c, c) is zero.

The two maps of AlgebraicGeometry.Space.restrictedLiftDifferenceData at that pair are the same transported comorphism, so AlgebraicGeometry.Space.liftDifferenceDifferentialsHom_eq_zero applies.

This is the field equiv_self of AlgebraicGeometry.Space.LiftDerivationAction read at this difference.

theorem restrictedLiftDifferenceHom_self (c : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hker : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x)
    (hcc : c ≫ qb = c ≫ qb) :
    restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c c h h hker hcc = 0

AlgebraicGeometry.Space.restrictedLiftDifferenceHom_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferencePairHom.lean, line 219. The attribute's comment: “the cocycle identity: the linear maps of three morphisms agreeing on the thickening and over the base add along the chain”.

The cocycle identity: the linear maps of three morphisms add along the chain, θ(c₁, c₂) + θ(c₂, c₃) = θ(c₁, c₃).

The three pairs of transported comorphisms are (f₁, f₂), (f₂, f₃) and (f₁, f₃) inside one and the same square-zero ideal, so AlgebraicGeometry.Space.liftDifferenceDifferentialsHom_add applies with all three of its index equations holding by AlgebraicGeometry.Space.restrictedLiftDifferenceData_f and AlgebraicGeometry.Space.restrictedLiftDifferenceData_g.

This is the field equiv_add_equiv of AlgebraicGeometry.Space.LiftDerivationAction read at this difference.

theorem restrictedLiftDifferenceHom_add (c₁ c₂ c₃ : X ⟶ W)
    (h₁ : subspaceInclusion B S hS X Z ≫ c₁ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h₂ : subspaceInclusion B S hS X Z ≫ c₂ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h₃ : subspaceInclusion B S hS X Z ≫ c₃ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hker₁₂ : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c₁ e₀ h₁).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c₂ e₀ h₂).hom.app V x)
    (hker₂₃ : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c₂ e₀ h₂).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c₃ e₀ h₃).hom.app V x)
    (hker₁₃ : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c₁ e₀ h₁).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c₃ e₀ h₃).hom.app V x)
    (hcc₁₂ : c₁ ≫ qb = c₂ ≫ qb) (hcc₂₃ : c₂ ≫ qb = c₃ ≫ qb)
    (hcc₁₃ : c₁ ≫ qb = c₃ ≫ qb) :
    restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₁ c₂ h₁ h₂ hker₁₂ hcc₁₂ +
        restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₂ c₃ h₂ h₃ hker₂₃ hcc₂₃ =
      restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₁ c₃ h₁ h₃ hker₁₃ hcc₁₃

AlgebraicGeometry.Space.exists_derivation_restrictedSharpThroughThickening_sub, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceThickeningDerivation.lean, line 133. The attribute's comment: “the full statement: for two morphisms of first order thickenings over T with equal restriction f and equal maps f^C ⟶ C of 04CP, c^♯ - c'^♯, read on the small étale site of the reduced target, factors as j^♯ : j^{-1}O_W ⟶ O_{W₀} followed by an O_T-derivation D into f_C_{Z/X} and the inclusion f_C_{Z/X} ⟶ f_(i^{-1}O_X)”.

[Stacks Project, Tag 0618]. Let Z ⊆ X and W₀ ⊆ W be first-order thickenings of algebraic spaces over an algebraic space T, and let (f, c) and (f, c') be two morphisms of thickenings over T with the same restriction f : Z ⟶ W₀ and equal canonical maps f^*𝒞_{W₀/W} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP]. Then there is an 𝒪_T-derivation D of 𝒪_{W₀} with values in f_*𝒞_{Z/X} through which c^♯ - c'^♯ factors: for every local section x of 𝒪_W, read on W₀, the difference of the two comorphisms at x is the inclusion f_*𝒞_{Z/X} ⟶ f_*𝒪_X applied to D of the image of x in 𝒪_{W₀}.

The reading of 𝒪_W, f_*𝒪_X and the comorphisms on the small étale site of W₀ is the one of the module documentation.

theorem exists_derivation_restrictedSharpThroughThickening_sub
    (hZ : IsFirstOrderThickening B S hS X Z.1)
    (hW₀ : IsFirstOrderThickening B S hS W W₀.1) (c' : X ⟶ W)
    (hsq : subspaceInclusion B S hS X Z ≫ c = f ≫ subspaceInclusion B S hS W W₀)
    (hsq' : subspaceInclusion B S hS X Z ≫ c' = f ≫ subspaceInclusion B S hS W W₀)
    {T : AlgebraicSpaces B S hS} (pX : X ⟶ T) (pW : W ⟶ T) (hc : c ≫ pW = pX)
    (hc' : c' ≫ pW = pX)
    (hC : conormalMap B S hS Z W₀ c f hsq = conormalMap B S hS Z W₀ c' f hsq') :
    ∃ D : PresheafOfModulesOfCommRing.Derivation'
        ((modulePushforward B S hS f).obj (conormalModule B S hS X Z)).val
        (structureSharpInverseImage B S hS (subspaceInclusion B S hS W W₀ ≫ pW)).hom,
      ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : ToType ((structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V)),
        (restrictedSquareZeroValues B S hS Z W₀ f hZ).ι
            (D.d ((structureSharpRingInverseImage B S hS
              (subspaceInclusion B S hS W W₀)).hom.app V x)) =
          (restrictedSharpThroughThickening B S hS Z W₀ c f hsq).hom.app V x -
            (restrictedSharpThroughThickening B S hS Z W₀ c' f hsq').hom.app V x

AlgebraicGeometry.Space.restrictedSharpThroughThickening_app_eq_of_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceTopTarget.lean, line 106. The attribute's comment: “hypothesis (2) for two morphisms into an undeformed target: the kernel of the reduction has no nonzero sections, so the two comorphisms agree on it”.

Hypothesis (2) of [Stacks Project, Tag 0618] for an undeformed target. For two morphisms c, c' : X ⟶ W whose restrictions to the thickening Z ⊂ X are both e₀ read through the inclusion of the top closed subspace of W, the two transported comorphisms agree on every section killed by the reduction: there are no such sections but zero, by AlgebraicGeometry.Space.eq_zero_of_app_structureSharpRingInverseImage_top.

This is the hypothesis hker of AlgebraicGeometry.Space.restrictedLiftDifferenceData, discharged in the case of Remark [Stacks Project, Tag 061D]: the target of the lifting problem is not deformed, so the map A out of the conormal module 𝒞_{W/W} is zero.

theorem restrictedSharpThroughThickening_app_eq_of_top {X W : AlgebraicSpaces B S hS}
    (Z : ClosedSubspaces B S hS X.1)
    (e₀ : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨(⊤ : Subfunctor W.1).toFunctor, (isClosedSubspace_top B S hS W).1⟩ :
        AlgebraicSpaces B S hS))
    (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c =
      e₀ ≫ subspaceInclusion B S hS W ⟨⊤, isClosedSubspace_top B S hS W⟩)
    (h' : subspaceInclusion B S hS X Z ≫ c' =
      e₀ ≫ subspaceInclusion B S hS W ⟨⊤, isClosedSubspace_top B S hS W⟩)
    (V : (SmallEtale B S hS
      (⟨(⊤ : Subfunctor W.1).toFunctor, (isClosedSubspace_top B S hS W).1⟩ :
        AlgebraicSpaces B S hS).1)ᵒᵖ)
    (x : (structureRingSheafInverseImage B S hS
      (subspaceInclusion B S hS W ⟨⊤, isClosedSubspace_top B S hS W⟩)).obj.obj V)
    (hx : (structureSharpRingInverseImage B S hS
      (subspaceInclusion B S hS W ⟨⊤, isClosedSubspace_top B S hS W⟩)).hom.app V x = 0) :
    (restrictedSharpThroughThickening B S hS Z
        ⟨⊤, isClosedSubspace_top B S hS W⟩ c e₀ h).hom.app V x =
      (restrictedSharpThroughThickening B S hS Z
        ⟨⊤, isClosedSubspace_top B S hS W⟩ c' e₀ h').hom.app V x

AlgebraicGeometry.Space.undeformedLiftDiff, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTarget.lean, line 159. The attribute's comment: “the difference of two lifts of a morphism over a base along a first order thickening of the source, for an UNDEFORMED target, where condition (3) of 061A is vacuous”.

The 𝒪_Z-linear map a^*Ω_{W/V} ⟶ 𝒞_{Z/X} by which two lifts into an undeformed target differ. The sectionwise difference of their two comorphisms, read as a V-derivation of 𝒪_W with values in a_*𝒞_{Z/X} and transposed to a map out of a^*Ω_{W/V}.

def undeformedLiftDiff (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = a)
    (h' : subspaceInclusion B S hS X Z ≫ c' = a) (hb : c ≫ b = c' ≫ b) :
    (modulePullback B S hS a).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z

AlgebraicGeometry.Space.structureSharpOfRestrictEq_comp_pushforward_structureSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSharpRestrictEq.lean, line 298. The attribute's comment: “the two structure maps of two lifts of one morphism become equal after the structure map of the thickening, so their difference lands in the defining ideal”.

The two structure maps of two lifts agree after the structure map of the thickening, for sheaves of rings. This is the hypothesis which [Stacks Project, Tag 0618] needs of the pair AlgebraicGeometry.Space.structureSharpOfRestrictEq, (b')^♯: read into the direct image along b' of i_*𝒪_X the two homomorphisms coincide, so their difference takes its values in the defining ideal of the thickening.

It is the set-level statement with the ring operations carried along: the forgetful functor on sheaves of rings is faithful, and both the comparison and the direct image of a homomorphism are known on underlying sheaves of sets.

theorem structureSharpOfRestrictEq_comp_pushforward_structureSharp :
    structureSharpOfRestrictEq B S hS hG a' b' h ≫
        pullbackRingSheafMap.{u, u, u, u + 1, u, u + 1} (SmallEtale.topology B S hS Y'.1)
          (smallEtaleDirectImage B S hS b')
          (structureSharp B S hS (IsThickening.inclusion B S hS hG)) =
      structureSharp B S hS b' ≫
        pullbackRingSheafMap.{u, u, u, u + 1, u, u + 1} (SmallEtale.topology B S hS Y'.1)
          (smallEtaleDirectImage B S hS b')
          (structureSharp B S hS (IsThickening.inclusion B S hS hG))

AlgebraicGeometry.Space.inverseImageStructureSharpOfRestrictEq_comp_structureSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSharpRestrictEqInverseImage.lean, line 370. The attribute's comment: “the two structure maps of two lifts, as a pair of parallel homomorphisms into the structure sheaf of the thickening which agree after the structure map of the inclusion”.

The hypothesis hfg of AlgebraicGeometry.Space.liftDifference at the pair of structure maps of two lifts. The same statement as AlgebraicGeometry.Space.inverseImageStructureSharpOfRestrictEq_comp_structureSharpCommRing, read for sheaves of rings, which is the level at which the defining ideal of the thickening lives.

The forgetful functor is applied to the whole equation, so nothing has to be known about what it does to the comparison of the two inverse images — only about the structure map of the inclusion, which is AlgebraicGeometry.Space.map_structureSharpCommRing.

theorem inverseImageStructureSharpOfRestrictEq_comp_structureSharp :
    (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map
          (inverseImageStructureSharpOfRestrictEq B S hS hG a' b' h) ≫
        structureSharp B S hS (subspaceInclusion B S hS X' ⟨G, hG.1⟩) =
      (sheafCompose (SmallEtale.topology B S hS X'.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map
          (structureSharpInverseImage B S hS b') ≫
        structureSharp B S hS (subspaceInclusion B S hS X' ⟨G, hG.1⟩)

AlgebraicGeometry.Space.liftPairDifference, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSharpRestrictEqInverseImage.lean, line 395. The attribute's comment: “the derivation, for the two structure maps of two morphisms of a thickening agreeing on its closed subspace”.

The difference of the two structure maps of two lifts, as a section of the defining ideal of the thickening. This is the derivation D of [Stacks Project, Tag 0618] for two morphisms a', b' : X' ⟶ Y' of a thickening G ⊂ X' which agree on its closed subspace: it is AlgebraicGeometry.Space.liftDifference applied to the pair of parallel homomorphisms (a')^♯, (b')^♯ : (b')^{-1}𝒪_{Y'} ⟶ 𝒪_{X'}.

Its four defining equations are AlgebraicGeometry.Space.liftDifference_add, AlgebraicGeometry.Space.liftDifference_smul_add_smul, AlgebraicGeometry.Space.liftDifference_app_eq_zero and AlgebraicGeometry.Space.liftDifference_naturality, which apply to it verbatim.

noncomputable def liftPairDifference (U : (SmallEtale B S hS X'.1)ᵒᵖ)
    (r : ((sheafCompose (SmallEtale.topology B S hS X'.1)
      (forget₂ CommRingCat.{u} RingCat.{u})).obj
        (inverseImageStructureSheaf B S hS b')).obj.obj U) :
    definingIdealAt B S hS X' ⟨G, hG.1⟩ U

Tag 0619, an equation

Tag 0619 in the Stacks Project.

Stacks.Sheaves.Differentials.universalDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsRepresentable.lean, line 115. The attribute's comment: “the factorization D = d o theta of a derivation through the universal derivation”.

Every relative derivation with values in a sheaf of modules factors through the universal derivation by a unique morphism of sheaves of modules.

theorem universalDerivation_isUniversal
    (F : SheafOfModules.{u} (underlyingRingSheaf O₂))
    (D : SheafDerivation O₁ O₂ φ F) :
    ∃! f : moduleOfDifferentials O₁ O₂ φ ⟶ F,
      (universalDerivation O₁ O₂ φ).postcomp f.val = D

AlgebraicGeometry.Space.derivationDirectImageEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivationsIntoDirectImage.lean, line 96. The attribute's comment: “the bijection θ ↔ D = d_{Y/B} ∘ θ, stated at a general target module”.

Stacks 0619. For a : X ⟶ Y, b : Y ⟶ Z 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 : Modules.{u, u} B S hS X.1 X.2) :
    ((modulePullback B S hS a).obj (sheafOfDifferentials B S hS b) ⟶ C) ≃
      PresheafOfModulesOfCommRing.Derivation' ((modulePushforward B S hS a).obj C).val
        (structureSharpInverseImage B S hS b).hom

AlgebraicGeometry.Space.derivationDirectImageEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivationsIntoDirectImage.lean, line 107. The attribute's comment: “the equation D = d_{Y/B} ∘ θ”.

Equation (0619) 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 : Modules.{u, u} B S hS X.1 X.2)
    (θ : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS b) ⟶ C) :
    derivationDirectImageEquiv B S hS a b C θ =
      (universalDerivation B S hS b).postcomp
        (((modulePullbackAdjunction B S hS a).homEquiv _ _) θ).val

AlgebraicGeometry.Space.restrictedLiftDifferenceHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferencePairHom.lean, line 98. The attribute's comment: “the linear map attached to the derivation by which the two comorphisms differ”.

The linear map θ : e₀^*Ω_{W₀/Bas} ⟶ 𝒞_{Z/X} by which two morphisms agreeing on the thickening and over qb differ. This is [Stacks Project, Tag 0618] together with Equation [Stacks Project, Tag 0619], in the direction from a pair of morphisms to a linear map.

The pair of comorphisms is AlgebraicGeometry.Space.restrictedLiftDifferenceData and the descent is AlgebraicGeometry.Space.liftDifferenceDifferentialsHom; its two hypotheses are the datum's own hker and AlgebraicGeometry.Space.descend_restrictedLiftDifferenceData_structureSharpInverseImage_eq_zero.

abbrev restrictedLiftDifferenceHom (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h' : subspaceInclusion B S hS X Z ≫ c' = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hker : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c' e₀ h').hom.app V x)
    (hcc : c ≫ qb = c' ≫ qb) :
    (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ qb)) ⟶
      conormalModule B S hS X Z

AlgebraicGeometry.Space.undeformedLiftDiff, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTarget.lean, line 159. The attribute's comment: “the difference read as a map out of the pulled back differentials, for an undeformed target”.

The 𝒪_Z-linear map a^*Ω_{W/V} ⟶ 𝒞_{Z/X} by which two lifts into an undeformed target differ. The sectionwise difference of their two comorphisms, read as a V-derivation of 𝒪_W with values in a_*𝒞_{Z/X} and transposed to a map out of a^*Ω_{W/V}.

def undeformedLiftDiff (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = a)
    (h' : subspaceInclusion B S hS X Z ≫ c' = a) (hb : c ≫ b = c' ≫ b) :
    (modulePullback B S hS a).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z

Tag 04D0, a lemma

Tag 04D0 in the Stacks Project.

AlgebraicGeometry.Space.exists_hom_restrictedSharpThroughThickening_eq_restrictedLiftSolutionOfHom_of_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationActionChart.lean, line 452. The attribute's comment: “the existence clause at the source's hypotheses: a prescribed O_X-linear map theta is realized by a morphism over the base agreeing with the given one on the thickening, its comorphism being the modification of the given one by the derivation d o theta of Equation 0619 -- with no appeal to Theorem 04KL. Uniqueness is not claimed here”.

The existence clause of [Stacks Project, Tag 04D0] at the source's hypotheses, with no appeal to Properties of Spaces, Theorem [Stacks Project, Tag 04KL].

Let Z ⊆ X be a first order thickening of algebraic spaces, W₀ ⊆ W a closed subspace with inclusion j, e₀ : Z ⟶ W₀ a morphism that c : X ⟶ W restricts to, and let c be a morphism over Bas along r : W ⟶ Bas. Let b : W₀ ⟶ Bas₀ and ib : Bas₀ ⟶ Bas satisfy the square j ≫ r = b ≫ ib, so that the differentials Ω_{W₀/Bas₀} are the ones of the source. Then every 𝒪_Z-linear map θ : (e₀)^*Ω_{W₀/Bas₀} ⟶ 𝒞_{Z/X} is realized: there is a morphism c' : X ⟶ W over Bas, agreeing with c on Z, whose comorphism read in the common target of the morphisms agreeing on the thickening is the modification c^♯ − ι ∘ (d_{W₀/Bas₀} ∘ θ) ∘ j^♯ of the comorphism of c by the derivation attached to θ. The uniqueness half of the tag is not claimed here.

theorem exists_hom_restrictedSharpThroughThickening_eq_restrictedLiftSolutionOfHom_of_square
    (hZ : IsFirstOrderThickening B S hS X Z.1) (c : X ⟶ W)
    (W₀ : ClosedSubspaces B S hS W.1)
    (e₀ : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS))
    (hce : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    {Bas₀ : AlgebraicSpaces B S hS}
    (b : (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS) ⟶ Bas₀)
    (θ : (modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z)
    (r : W ⟶ Bas) (ib : Bas₀ ⟶ Bas)
    (hsq : subspaceInclusion B S hS W W₀ ≫ r = b ≫ ib)
    (p : X ⟶ Bas) (hp : c.hom ≫ r.hom = p.hom) :
    ∃ (c' : X ⟶ W) (hcc : subspaceInclusion B S hS X Z ≫ c' =
        e₀ ≫ subspaceInclusion B S hS W W₀),
      c'.hom ≫ r.hom = p.hom ∧
        restrictedSharpThroughThickening B S hS Z W₀ c' e₀ hcc =
          restrictedLiftSolutionOfHom B S hS Z hZ c W₀ e₀ hce b θ

AlgebraicGeometry.Space.existsUnique_thickeningLiftOver_sub_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationTranslate.lean, line 345. The attribute's comment: “existence and uniqueness of the morphism of pairs (a, b') satisfying (1) and (2) of 0618 whose comorphism differs from that of a' by the derivation d o theta of Equation 0619”.

Let (e₀, c) : (Z ⊂ X) ⟶ (W₀ ⊂ W) be a morphism of first order thickenings over Bas and let θ : e₀^*Ω_{W₀/Bas₀} ⟶ 𝒞_{Z/X} be 𝒪_Z-linear. Then there is exactly one morphism of thickenings (e₀, c') over Bas — so condition (1) of [Stacks Project, Tag 0618], b = a, holds — such that

• condition (2) of Tag 0618 holds: the comorphisms of c and c' agree on the sections killed by j^♯, and
• the derivation by which the comorphisms differ is related to θ by Equation (0619): c^♯ s − c'^♯ s = ι (D (j^♯ s)) with D = d_{W₀/Bas₀} ∘ θ.

It is θ · c.

theorem existsUnique_thickeningLiftOver_sub_eq
    (θ : (modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z)
    (c : ThickeningLiftOver B S hS Z W₀ e₀ r p) :
    ∃! c' : ThickeningLiftOver B S hS Z W₀ e₀ r p,
      (∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : (structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V),
        (structureSharpRingInverseImage B S hS (subspaceInclusion B S hS W W₀)).hom.app V x =
            0 →
          (thickeningLiftSharp B S hS Z hZ W₀ e₀ c.1 c.2.1).hom.app V x =
            (thickeningLiftSharp B S hS Z hZ W₀ e₀ c'.1 c'.2.1).hom.app V x) ∧
      ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : (structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V),
        (thickeningLiftSharp B S hS Z hZ W₀ e₀ c.1 c.2.1).hom.app V x -
            (thickeningLiftSharp B S hS Z hZ W₀ e₀ c'.1 c'.2.1).hom.app V x =
          thickeningDerivationValue B S hS Z hZ W₀ e₀ b θ V x

AlgebraicGeometry.Space.existsUnique_hom_of_derivationModificationHomOfMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/DerivationModificationMorphism.lean, line 332. The attribute's comment: “the morphism of pairs (b, b') and its uniqueness, for the modified structure map alpha = (a')^sharp + D BUILT from theta by Equation 0619: alpha is constructed, and its three properties that Stacks 05ZN consumes -- locally ringed, the square, the O_T-algebra condition -- are proved outright, as is the recovery of morphisms of algebraic spaces from morphisms of their small etale ringed topoi over a base, isRecoveredFromSmallEtale_holds; the uniqueness alone is also eq_of_derivationModificationHomOfMap_induces”.

[Stacks Project, Tag 04D0], with the recovery of morphisms over the base as its only argument. For a morphism (a, a') of first order thickenings over T and an 𝒪_X-linear map θ : a^*Ω_{Y/T} ⟶ 𝒞_{X/X'} there is exactly one morphism b' : X' ⟶ Y' whose structure map is α = (a')^♯ + D, and the pair (a, b') is a morphism of thickenings over T.

Setting b = a this is the unique morphism of pairs (b, b') of the source: conditions (1) and (2) of [Stacks Project, Tag 0618] are the two displayed equations, and the derivation D is related to θ by Equation (0619) because that is how AlgebraicGeometry.Space.derivationModificationHomOfMap is built.

Unlike AlgebraicGeometry.Space.existsUnique_hom_of_derivationModification this takes no datum for the modified structure map: α is constructed from θ, and its three properties that [Stacks Project, Tag 05ZN] consumes — that it is locally ringed, that it fits the square and that it is a map of 𝒪_T-algebras — are proved above, and the recovery of morphisms of algebraic spaces from morphisms of their small étale ringed topoi over a base is AlgebraicGeometry.Space.isRecoveredFromSmallEtale_holds. So nothing is assumed.

theorem existsUnique_hom_of_derivationModificationHomOfMap
    (hW : IsFirstOrderThickening B S hS Y' W.1) :
    ∃! b' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS b'
        (derivationModificationHomOfMap B S hS Z hZ a' W p a hcompat θ) ∧
      subspaceInclusion B S hS X' Z ≫ b' = a ≫ subspaceInclusion B S hS Y' W ∧
      b' ≫ p = a' ≫ p

AlgebraicGeometry.Space.eq_of_derivationModificationHomOfMap_induces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/DerivationModificationMorphism.lean, line 364. The attribute's comment: “the uniqueness of the morphism of pairs (b, b'), for the modified structure map alpha = (a')^sharp + D built from theta by Equation 0619: no recovery of morphisms over the base (Stacks 04KL) and no property of alpha is used, only Stacks 04M6”.

The uniqueness half of [Stacks Project, Tag 04D0], with nothing assumed. Two morphisms b₁', b₂' : X' ⟶ Y' whose structure maps are both the modification α = (a')^♯ + D of the structure map of a' by the derivation attached to an 𝒪_X-linear map θ : a^*Ω_{Y/T} ⟶ 𝒞_{X/X'} are equal.

This is the "unique" of the source's "there exists a unique morphism of pairs (b, b')", and it needs neither [Stacks Project, Tag 04KL] nor any property of α: two morphisms inducing the same morphism of small étale ringed topoi are 2-isomorphic to one another, and [Stacks Project, Tag 04M6] identifies them. Since the source's construction fixes b = a, uniqueness of b' is uniqueness of the pair.

The hypotheses are exactly the source's: X ⊂ X' and Y ⊂ Y' closed subspaces with X ⊂ X' of first order, (a, a') a morphism of the pairs, p the structure morphism to the base, and θ an 𝒪_X-linear map a^*Ω_{Y/T} ⟶ 𝒞_{X/X'}.

theorem eq_of_derivationModificationHomOfMap_induces (b₁' b₂' : X' ⟶ Y')
    (h₁ : InducesSmallEtaleRingedToposHom B S hS b₁'
      (derivationModificationHomOfMap B S hS Z hZ a' W p a hcompat θ))
    (h₂ : InducesSmallEtaleRingedToposHom B S hS b₂'
      (derivationModificationHomOfMap B S hS Z hZ a' W p a hcompat θ)) :
    b₁' = b₂'

AlgebraicGeometry.Space.existsUnique_hom_conormalMap_eq_derivation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/DerivationMovedLiftConormal.lean, line 86. The attribute's comment: “the morphism of pairs (b, b') = (a, b') moved by θ: conditions (1) and (2) of 0618, with the derivation D of 0618 equal to d_{Y/B} ∘ θ (Equation 0619)”.

[Stacks Project, Tag 04D0]. Let (e₀, c) : (Z ⊂ X) ⟶ (W₀ ⊂ W) be a morphism of first order thickenings over T (i ≫ c = e₀ ≫ j and c ≫ q = p), and let θ : e₀^*Ω_{W₀/T} ⟶ 𝒞_{Z/X} be 𝒪_Z-linear. Then there is exactly one morphism b' : X ⟶ W such that (e₀, b') is a morphism of thickenings over T (i ≫ b' = e₀ ≫ j and b' ≫ q = p: condition (1) of [Stacks Project, Tag 0618], b = a), the two maps e₀^*𝒞_{W₀/W} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] are equal (condition (2)), and the comorphisms, read as maps j^{-1}𝒪_W ⟶ (e₀)_*(i^{-1}𝒪_X), differ by ι ∘ D ∘ j^♯ with D = d_{W₀/T} ∘ θ the derivation of Equation [Stacks Project, Tag 0619].

theorem existsUnique_hom_conormalMap_eq_derivation_eq
    (θ : (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ q)) ⟶
      conormalModule B S hS X Z)
    (p : X ⟶ T) (hcq : c ≫ q = p) :
    ∃! b' : X ⟶ W, ∃ (hb : subspaceInclusion B S hS X Z ≫ b' =
        e₀ ≫ subspaceInclusion B S hS W W₀),
      b' ≫ q = p ∧
        conormalMap B S hS Z W₀ c e₀ hc = conormalMap B S hS Z W₀ b' e₀ hb ∧
        ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
          (x : ToType ((structureRingSheafInverseImage B S hS
            (subspaceInclusion B S hS W W₀)).obj.obj V)),
          (restrictedSquareZeroValues B S hS Z W₀ e₀ hZ).ι
              (derivationFamilyOfHom B S hS (subspaceInclusion B S hS W W₀ ≫ q) e₀
                (conormalModule B S hS X Z) θ V
                ((structureSharpRingInverseImage B S hS
                  (subspaceInclusion B S hS W W₀)).hom.app V x)) =
            (restrictedSharpThroughThickening B S hS Z W₀ c e₀ hc).hom.app V x -
              (restrictedSharpThroughThickening B S hS Z W₀ b' e₀ hb).hom.app V x

AlgebraicGeometry.Space.exists_undeformedLiftDiff_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTargetSurjective.lean, line 314. The attribute's comment: “the existence half: every linear map is the difference from a given lift of some lift, for an UNDEFORMED target”.

The existence half of [Stacks Project, Tag 04D0] for an undeformed target. Every 𝒪_Z-linear map θ : a^*Ω_{W/V} ⟶ 𝒞_{Z/X} is the difference from c of some lift c' of a = i ≫ c over V.

The comorphism of c moved by the derivation attached to θ is a solution of the lifting problem whose descended difference from the comorphism of c is θ (AlgebraicGeometry.Space.exists_liftDifferenceData_solution_of_hom); that solution is the comorphism of an honest lift c' (AlgebraicGeometry.Space.exists_hom_structureSharpThroughThickeningAt_eq_of_solution); and the pair (c, c') then has the same two comorphisms as the pair (c^♯, g), hence the same descended difference, the comparison being made against the pair (c', c') whose descended difference vanishes.

With AlgebraicGeometry.Space.eq_of_undeformedLiftDiff_eq_zero this is the whole of [Stacks Project, Tag 04D0] in this situation, and it is unconditional.

theorem exists_undeformedLiftDiff_eq :
    ∃ (c' : X ⟶ W) (h' : subspaceInclusion B S hS X Z ≫ c' =
        subspaceInclusion B S hS X Z ≫ c) (hb : c ≫ b = c' ≫ b),
      undeformedLiftDiff B S hS Z hZ (subspaceInclusion B S hS X Z ≫ c) b c c' rfl h' hb = θ

AlgebraicGeometry.Space.existsUnique_undeformedLiftDiff_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTargetSurjective.lean, line 376. The attribute's comment: “existence and uniqueness of the lift with a prescribed difference from a given lift, for an UNDEFORMED target”.

[Stacks Project, Tag 04D0] for an undeformed target. For every 𝒪_Z-linear map θ : a^*Ω_{W/V} ⟶ 𝒞_{Z/X} there is exactly one lift of a = i ≫ c over V whose difference from c is θ.

Existence is AlgebraicGeometry.Space.exists_undeformedLiftDiff_eq and uniqueness is AlgebraicGeometry.Space.undeformedLiftDiff_injective. Together with the additivity of the difference this is the simple transitivity of [Stacks Project, Tag 061C] over the ambient space of the thickening, in the case where the target is not deformed.

theorem existsUnique_undeformedLiftDiff_eq :
    ∃! p : {c' : X ⟶ W //
        (subspaceInclusion B S hS X Z ≫ c' = subspaceInclusion B S hS X Z ≫ c) ∧
          c ≫ b = c' ≫ b},
      undeformedLiftDiff B S hS Z hZ (subspaceInclusion B S hS X Z ≫ c) b c p.1 rfl
        p.2.1 p.2.2 = θ

AlgebraicGeometry.Space.eq_of_undeformedLiftDiff_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTargetUnique.lean, line 99. The attribute's comment: “the uniqueness half: a lift is determined by its difference from a given lift, for an UNDEFORMED target”.

The uniqueness half of [Stacks Project, Tag 04D0] for an undeformed target. Two lifts of a over V along the first order thickening Z ⊂ X whose difference vanishes are equal.

theorem eq_of_undeformedLiftDiff_eq_zero (c c' : X ⟶ W)
    (h : subspaceInclusion B S hS X Z ≫ c = a)
    (h' : subspaceInclusion B S hS X Z ≫ c' = a) (hb : c ≫ b = c' ≫ b)
    (hzero : undeformedLiftDiff B S hS Z hZ a b c c' h h' hb = 0) :
    c = c'

AlgebraicGeometry.Space.eq_of_restrictedLiftDifferenceHom_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftSimpleTransitivity.lean, line 190. The attribute's comment: “the uniqueness clause: a companion of the given morphism of thickenings is determined by its difference”.

The difference determines the companion: two morphisms which restrict on the thickening to the same morphism, agree with c₀ over Bas, induce the same map of conormal modules as c₀ does, and have the same difference from c₀, are equal.

This is the uniqueness clause of [Stacks Project, Tag 04D0], and it is unconditional: the cocycle identity makes the difference of the two zero, a pair of lifts with zero descended difference has equal comorphisms by AlgebraicGeometry.Space.eq_of_liftDifferenceDifferentialsHom_eq_zero, and AlgebraicGeometry.Space.eq_of_restrictedSharpThroughThickening_eq recovers the equality of the two morphisms from that.

theorem eq_of_restrictedLiftDifferenceHom_eq (c₀ c c' : X ⟶ W)
    (h₀ : subspaceInclusion B S hS X Z ≫ c₀ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
    (h' : subspaceInclusion B S hS X Z ≫ c' = e₀ ≫ subspaceInclusion B S hS W W₀)
    (hker : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c₀ e₀ h₀).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x)
    (hker' : ∀ (V : (SmallEtale B S hS
        (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
      (x : (structureRingSheafInverseImage B S hS
        (subspaceInclusion B S hS W W₀)).obj.obj V),
      (structureSharpRingInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
        (restrictedSharpThroughThickening B S hS Z W₀ c₀ e₀ h₀).hom.app V x =
          (restrictedSharpThroughThickening B S hS Z W₀ c' e₀ h').hom.app V x)
    (hcc : c₀ ≫ qb = c ≫ qb) (hcc' : c₀ ≫ qb = c' ≫ qb)
    (heq : restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₀ c h₀ h hker hcc =
      restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₀ c' h₀ h' hker' hcc') :
    c = c'

AlgebraicGeometry.Space.exists_hom_restrictedLiftDifferenceHom_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftSimpleTransitivity.lean, line 350. The attribute's comment: “the existence clause: every linear map out of the pulled back differentials is the difference of the given morphism of thickenings and a second one”.

Every linear map is a difference. For an 𝒪_Z-linear map θ : e₀^*Ω_{W₀/Bas} ⟶ 𝒞_{Z/X} there is a morphism c : X ⟶ W restricting on the thickening to e₀ ≫ j, agreeing with c₀ over Bas, inducing the same map of conormal modules as c₀ does, and whose difference from c₀ is θ.

This is the existence clause of [Stacks Project, Tag 04D0], and it is unconditional: AlgebraicGeometry.Space.exists_hom_of_movedThickeningLift produces the morphism and AlgebraicGeometry.Space.restrictedSharpThroughThickening_eq_movedThickeningLift_g identifies its transported comorphism with the moved solution.

theorem exists_hom_restrictedLiftDifferenceHom_eq (c₀ : X ⟶ W)
    (h₀ : subspaceInclusion B S hS X Z ≫ c₀ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (θ : (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ qb)) ⟶
      conormalModule B S hS X Z) :
    ∃ (c : X ⟶ W)
      (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
      (hker : ∀ (V : (SmallEtale B S hS
          (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : (structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V),
        (structureSharpRingInverseImage B S hS
            (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
          (restrictedSharpThroughThickening B S hS Z W₀ c₀ e₀ h₀).hom.app V x =
            (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x)
      (hcc : c₀ ≫ qb = c ≫ qb),
      restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₀ c h₀ h hker hcc = θ

AlgebraicGeometry.Space.existsUnique_hom_restrictedLiftDifferenceHom_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftSimpleTransitivity.lean, line 403. The attribute's comment: “the unique second morphism of thickenings with a prescribed difference, with no stand-in: the existence of the moved solution and the faithfulness of the transported comorphism replace the recovery of a morphism from its comorphism”.

Stacks 04D0. For a morphism c₀ : X ⟶ W restricting on the first order thickening Z ⊂ X to e₀ read through the inclusion of the closed subspace W₀ ⊆ W, and for an 𝒪_Z-linear map θ : e₀^*Ω_{W₀/Bas} ⟶ 𝒞_{Z/X}, there is exactly one morphism c : X ⟶ W which restricts on Z to the same morphism, agrees with c₀ over Bas and induces the same map of conormal modules as c₀ does — hypotheses (1) and (2) of [Stacks Project, Tag 0618] — and whose difference from c₀ is θ.

This is the whole of [Stacks Project, Tag 04D0], unconditionally: the existence clause is AlgebraicGeometry.Space.exists_hom_restrictedLiftDifferenceHom_eq and the uniqueness clause is AlgebraicGeometry.Space.eq_of_restrictedLiftDifferenceHom_eq. It is also the simple transitivity of [Stacks Project, Tag 061C] read at one object of the étale site, with the acting group the global 𝒪_Z-linear maps; see the "Scope" section of the module doc for the relativisation that is still owed.

theorem existsUnique_hom_restrictedLiftDifferenceHom_eq (c₀ : X ⟶ W)
    (h₀ : subspaceInclusion B S hS X Z ≫ c₀ = e₀ ≫ subspaceInclusion B S hS W W₀)
    (θ : (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ qb)) ⟶
      conormalModule B S hS X Z) :
    ∃! c : X ⟶ W, ∃ (h : subspaceInclusion B S hS X Z ≫ c = e₀ ≫ subspaceInclusion B S hS W W₀)
      (hker : ∀ (V : (SmallEtale B S hS
          (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : (structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V),
        (structureSharpRingInverseImage B S hS
            (subspaceInclusion B S hS W W₀)).hom.app V x = 0 →
          (restrictedSharpThroughThickening B S hS Z W₀ c₀ e₀ h₀).hom.app V x =
            (restrictedSharpThroughThickening B S hS Z W₀ c e₀ h).hom.app V x)
      (hcc : c₀ ≫ qb = c ≫ qb),
      restrictedLiftDifferenceHom B S hS Z W₀ hZ e₀ qb c₀ c h₀ h hker hcc = θ

AlgebraicGeometry.Space.existsUnique_hom_of_derivationModification_of_mono_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/DerivationModification.lean, line 469. The attribute's comment: “over a base SCHEME whose canonical morphism to the spectrum of its global functions is a monomorphism -- an affine base, a quasi-affine base: the morphism of pairs and its uniqueness, with the modified structure map (a')^sharp + D taken as an argument (DerivationModification), which packages that sum as a morphism of ringed topoi together with the two 2-isomorphisms Stacks 05ZN consumes. The recovery of morphisms over the base is NOT taken as an argument any more: it is proved for such a base scheme by isRecoveredFromSmallEtale_of_mono_toSpecGamma, which is where the hypothesis on the base enters and the only place it enters”.

Stacks 04D0, with the recovery of morphisms over the base and the modification datum taken as arguments. For a morphism (a, a') of first order thickenings over T and an 𝒪_X-linear map θ : a^*Ω_{Y/T} ⟶ 𝒞_{X/X'} there is exactly one morphism b' : X' ⟶ Y' whose structure map is (a')^♯ + d_{Y/T} ∘ θ, and the pair (a, b') is a morphism of thickenings over T.

Setting b = a this is the unique morphism of pairs (b, b') of the source: conditions (1) and (2) of [Stacks Project, Tag 0618] are the two displayed equations, and the derivation D is related to θ by Equation (0619) because that is how the datum hom θ is built.

theorem existsUnique_hom_of_derivationModification_of_mono_toSpecΓ (hSmono : Mono S.toSpecΓ)
    (M : DerivationModification B S hS hG hH pX' pY' a a')
    (θ : ThickeningDerivationMap B S hS hG hH pY' a) :
    ∃! b' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS b' (M.hom θ) ∧
      IsThickening.inclusion B S hS hG ≫ b' = a ≫ IsThickening.inclusion B S hS hH ∧
      b' ≫ pY' = pX'

AlgebraicGeometry.Space.existsUnique_hom_of_derivationModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/DerivationModification.lean, line 488. The attribute's comment: “the morphism of pairs and its uniqueness, with the recovery of morphisms over the base taken as an argument (IsRecoveredFromSmallEtale, which is Stacks 04KL over a base) and with the modified structure map (a')^sharp + D taken as an argument (DerivationModification), since forming that sum needs the structure-sheaf half of 05ZM”.

Stacks 04D0 with the recovery of morphisms over the base taken as an argument.

This is the shape in which the statement was first written. The argument hKL is now available without being assumed, for a base scheme whose canonical morphism to the spectrum of its global functions is a monomorphism, so the tag is registered on AlgebraicGeometry.Space.existsUnique_hom_of_derivationModification_of_mono_toSpecΓ above rather than here.

theorem existsUnique_hom_of_derivationModification (hKL : IsRecoveredFromSmallEtale B S hS)
    (M : DerivationModification B S hS hG hH pX' pY' a a')
    (θ : ThickeningDerivationMap B S hS hG hH pY' a) :
    ∃! b' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS b' (M.hom θ) ∧
      IsThickening.inclusion B S hS hG ≫ b' = a ≫ IsThickening.inclusion B S hS hH ∧
      b' ≫ pY' = pX'

AlgebraicGeometry.Space.eq_of_derivationModification_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/DerivationModification.lean, line 525. The attribute's comment: “injectivity of the correspondence theta -> b', with the modified structure map taken as an argument (DerivationModification)”.

The correspondence of [Stacks Project, Tag 04D0] is injective. Two 𝒪_X-linear maps θ which modify the structure map of a' to the same morphism of thickenings are equal.

theorem eq_of_derivationModification_eq (M : DerivationModification B S hS hG hH pX' pY' a a')
    (θ₁ θ₂ : ThickeningDerivationMap B S hS hG hH pY' a) (b' : X' ⟶ Y')
    (h₁ : InducesSmallEtaleRingedToposHom B S hS b' (M.hom θ₁))
    (h₂ : InducesSmallEtaleRingedToposHom B S hS b' (M.hom θ₂)) :
    θ₁ = θ₂

AlgebraicGeometry.Space.eq_of_derivationModification_base_of_induces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/DerivationModification.lean, line 541. The attribute's comment: “that the zero map returns the given morphism of thickenings, with the modified structure map taken as an argument (DerivationModification). The recovery of morphisms over the base is NOT taken as an argument: only the faithfulness half of 04KL is used here, and that is proved, by eq_of_inducesCommonSmallEtaleRingedToposHom”.

The zero map of [Stacks Project, Tag 04D0] does not move a'. The morphism of thickenings whose structure map is the modification of (a')^♯ by the zero map is a' itself.

theorem eq_of_derivationModification_base_of_induces
    (M : DerivationModification B S hS hG hH pX' pY' a a') (b' : X' ⟶ Y')
    (h : InducesSmallEtaleRingedToposHom B S hS b' (M.hom M.base)) :
    b' = a'

AlgebraicGeometry.Space.eq_of_derivationModification_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/DerivationModification.lean, line 558. The attribute's comment: “that the zero map returns the given morphism of thickenings, with the recovery of morphisms over the base taken as an argument (IsRecoveredFromSmallEtale, which is Stacks 04KL over a base) and with the modified structure map taken as an argument (DerivationModification)”.

The zero map of [Stacks Project, Tag 04D0] does not move a', with the recovery of morphisms over the base taken as an argument.

This is the shape in which the statement was first written. The argument hKL is not needed: only the faithfulness half of Stacks 04KL over a base is used, and that is proved for every base, so the tag is registered on AlgebraicGeometry.Space.eq_of_derivationModification_base_of_induces above rather than here.

theorem eq_of_derivationModification_base (hKL : IsRecoveredFromSmallEtale B S hS)
    (M : DerivationModification B S hS hG hH pX' pY' a a') (b' : X' ⟶ Y')
    (h : InducesSmallEtaleRingedToposHom B S hS b' (M.hom M.base)) :
    b' = a'

Tag 0CK6, a remark

Tag 0CK6 in the Stacks Project.

AlgebraicGeometry.Space.derivationTranslate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationTranslate.lean, line 184. The attribute's comment: “the morphism theta . a' of thickenings over the base”.

The morphism θ · c. For a morphism of thickenings c extending e₀ and an 𝒪_Z-linear map θ : e₀^*Ω_{W₀/Bas₀} ⟶ 𝒞_{Z/X}, the morphism of thickenings extending e₀ whose comorphism is that of c moved by the derivation attached to θ by Equation (0619).

noncomputable def derivationTranslate
    (θ : (modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z)
    (c : ThickeningLiftOver B S hS Z W₀ e₀ r p) : ThickeningLiftOver B S hS Z W₀ e₀ r p

AlgebraicGeometry.Space.thickeningLiftSharp_sub_thickeningLiftSharp_derivationTranslate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationTranslate.lean, line 214. The attribute's comment: “the comorphisms of a' and theta . a' differ by the derivation D = d o theta of Equation 0619”.

The comorphisms of c and of θ · c differ by the derivation related to θ by Equation (0619). On every section s of j^{-1}𝒪_W,

c^♯ s − (θ · c)^♯ s = ι (D (j^♯ s)), where D = d_{W₀/Bas₀} ∘ θ.

That is, (a')^♯ − (θ · a')^♯ factors as 𝒪_{Y'} ⟶ 𝒪_Y ⟶ a_*𝒞_{X/X'} ⟶ a_*𝒪_{X'} through the derivation D that Equation (0619) attaches to θ.

theorem thickeningLiftSharp_sub_thickeningLiftSharp_derivationTranslate
    (θ : (modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z)
    (c : ThickeningLiftOver B S hS Z W₀ e₀ r p)
    (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
    (x : (structureRingSheafInverseImage B S hS (subspaceInclusion B S hS W W₀)).obj.obj V) :
    (thickeningLiftSharp B S hS Z hZ W₀ e₀ c.1 c.2.1).hom.app V x -
        (thickeningLiftSharp B S hS Z hZ W₀ e₀
          (derivationTranslate B S hS Z hZ W₀ e₀ b r ib hsq p θ c).1
          (derivationTranslate B S hS Z hZ W₀ e₀ b r ib hsq p θ c).2.1).hom.app V x =
      thickeningDerivationValue B S hS Z hZ W₀ e₀ b θ V x

AlgebraicGeometry.Space.eq_derivationTranslate_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationTranslate.lean, line 289. The attribute's comment: “that theta . a' is characterised by the comorphisms of a' and theta . a' differing by the derivation D = d o theta of Equation 0619”.

The notation θ · c means nothing else than that the comorphisms differ by the derivation related to θ by Equation (0619). A morphism of thickenings c' over Bas extending e₀ equals θ · c if and only if c^♯ s − c'^♯ s = ι (D (j^♯ s)) for every section s of j^{-1}𝒪_W, where D = d_{W₀/Bas₀} ∘ θ.

theorem eq_derivationTranslate_iff
    (θ : (modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z)
    (c c' : ThickeningLiftOver B S hS Z W₀ e₀ r p) :
    c' = derivationTranslate B S hS Z hZ W₀ e₀ b r ib hsq p θ c ↔
      ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
        (x : (structureRingSheafInverseImage B S hS
          (subspaceInclusion B S hS W W₀)).obj.obj V),
        (thickeningLiftSharp B S hS Z hZ W₀ e₀ c.1 c.2.1).hom.app V x -
            (thickeningLiftSharp B S hS Z hZ W₀ e₀ c'.1 c'.2.1).hom.app V x =
          thickeningDerivationValue B S hS Z hZ W₀ e₀ b θ V x

AlgebraicGeometry.Space.derivationAddAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftDerivationTranslate.lean, line 405. The attribute's comment: “the action of theta on a', written theta . a'”.

The action θ · c. The group of 𝒪_Z-linear maps θ : e₀^*Ω_{W₀/Bas₀} ⟶ 𝒞_{Z/X} acts on the morphisms of thickenings over Bas extending e₀ by θ +ᵥ c = θ · c.

noncomputable def derivationAddAction :
    AddAction ((modulePullback B S hS e₀).obj (sheafOfDifferentials B S hS b) ⟶
      conormalModule B S hS X Z) (ThickeningLiftOver B S hS Z W₀ e₀ r p)

AlgebraicGeometry.Space.derivationMove_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/DerivationMovedLiftConormal.lean, line 136. The attribute's comment: “the action θ · a' of a local section θ: (a')^♯ and (θ · a')^♯ differ by the derivation D related to θ by Equation 0619”.

[Stacks Project, Tag 0CK6]. The action θ · c of a local section θ of SheafHom(e₀^*Ω_{W₀/T}, 𝒞_{Z/X}) on c means nothing else than this: (e₀, θ · c) is a morphism of thickenings over T with the same map of conormal modules as (e₀, c), and c^♯ and (θ · c)^♯ differ by the derivation D = d_{W₀/T} ∘ θ of Equation [Stacks Project, Tag 0619], read as maps j^{-1}𝒪_W ⟶ (e₀)_*(i^{-1}𝒪_X).

theorem derivationMove_spec
    (θ : (modulePullback B S hS e₀).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS W W₀ ≫ q)) ⟶
      conormalModule B S hS X Z)
    (p : X ⟶ T) (hcq : c ≫ q = p) :
    ∃ (hb : subspaceInclusion B S hS X Z ≫ derivationMove B S hS Z W₀ e₀ q hZ c hc θ p hcq =
        e₀ ≫ subspaceInclusion B S hS W W₀),
      derivationMove B S hS Z W₀ e₀ q hZ c hc θ p hcq ≫ q = p ∧
        conormalMap B S hS Z W₀ c e₀ hc =
          conormalMap B S hS Z W₀ (derivationMove B S hS Z W₀ e₀ q hZ c hc θ p hcq) e₀ hb ∧
        ∀ (V : (SmallEtale B S hS (⟨W₀.1.toFunctor, W₀.2.1⟩ : AlgebraicSpaces B S hS).1)ᵒᵖ)
          (x : ToType ((structureRingSheafInverseImage B S hS (subspaceInclusion B S hS W
              W₀)).obj.obj V)),
          (restrictedSquareZeroValues B S hS Z W₀ e₀ hZ).ι
              (derivationFamilyOfHom B S hS (subspaceInclusion B S hS W W₀ ≫ q) e₀
                (conormalModule B S hS X Z) θ V
                ((structureSharpRingInverseImage B S hS (subspaceInclusion B S hS W W₀)).hom.app V
                    x)) =
            (restrictedSharpThroughThickening B S hS Z W₀ c e₀ hc).hom.app V x -
              (restrictedSharpThroughThickening B S hS Z W₀
                (derivationMove B S hS Z W₀ e₀ q hZ c hc θ p hcq) e₀ hb).hom.app V x

Tag 061A, a lemma

Tag 061A in the Stacks Project.

AlgebraicGeometry.Space.isSheaf_conormalLiftSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftSheaf/ConormalLiftSheaf.lean, line 465. The attribute's comment: “the sheaf property of the rule 061B with all three conditions”.

The rule of [Stacks, Tag 061B] — U' ↦ {a' : U' ⟶ Y'} satisfying (1) a' is a morphism over T, (2) a'|_U = a|_U and (3) the map a^*𝒞_{Y/Y'}|_U ⟶ 𝒞_{X/X'}|_U induced by a' is the restriction of A — is a sheaf of sets on the spaces-étale site of X', for arbitrary thickenings X ⊂ X', Y ⊂ Y', an arbitrary morphism a and an arbitrary map A.

theorem isSheaf_conormalLiftSubfunctor :
    Presieve.IsSheaf (SpacesEtale.topology C S hS X')
      (conormalLiftSubfunctor C S hS hG hH pX' pY' a A).toFunctor

AlgebraicGeometry.Space.isSheaf_liftSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftSheaf/LiftSubfunctor.lean, line 227. The attribute's comment: “the sheaf property of the rule of lifts, for conditions (1) and (2); the conormal condition (3) is not imposed”.

The rule of conditions (1) and (2) is a sheaf. The rule sending an algebraic space U' étale over X' to the set of morphisms a' : U' ⟶ Y' over T whose restriction to U = X ×_{X'} U' is the restriction of a is a sheaf of sets on the spaces-étale site of X'.

The conormal condition (3) of the source is not imposed. For Y = Y' it holds for every a', and the rule is then the rule of the source (Remark 061D).

theorem isSheaf_liftSubfunctor :
    Presieve.IsSheaf (SpacesEtale.topology C S hS X')
      (liftSubfunctor C S hS hG hH pX' pY' a).toFunctor

Tag 061B, an equation

Tag 061B in the Stacks Project.

AlgebraicGeometry.Space.conormalLiftSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftSheaf/ConormalLiftSheaf.lean, line 390. The attribute's comment: “the rule U' ↦ {a' : U' → Y' satisfying (1), (2), (3)}, as a subfunctor of the presheaf of morphisms into Y' on the spaces-étale site of X', for arbitrary thickenings, a and A”.

The rule of lifts satisfying conditions (1), (2) and (3). Let X ⊂ X' and Y ⊂ Y' be thickenings of algebraic spaces over a base T, let a : X ⟶ Y be a morphism and let A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} be a map of 𝒪_X-modules. The rule sending an algebraic space U' étale over X' to the set of morphisms a' : U' ⟶ Y' such that 1. a' is a morphism over T, 2. a'|_U = a|_U on U = X ×_{X'} U', and 3. the map a^*𝒞_{Y/Y'}|_U ⟶ 𝒞_{X/X'}|_U induced by a' is the restriction of A to U,

as a subfunctor of the presheaf of morphisms into Y' on the spaces-étale site of X', with restriction along V' ⟶ U' given by a' ↦ a'|_{V'}.

Conditions (1) and (2) are AlgebraicGeometry.Space.IsLiftOver, the membership condition of AlgebraicGeometry.Space.liftSubfunctor, and condition (3) is AlgebraicGeometry.Space.IsConormalLiftAtSubspace at the two closed subspaces underlying the thickenings, the prescribed a and the prescribed A, over the structure morphism U' ⟶ X'.

No hypothesis is placed on the thickenings, on a or on A; in particular the conormal module of Y ⊂ Y' is not assumed to vanish.

def conormalLiftSubfunctor : Subfunctor (spacesEtaleHomPresheaf C S hS X' Y')

Tag 061C, a lemma

Tag 061C in the Stacks Project.

AlgebraicGeometry.Space.conormalLiftAction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftActionNaturality.lean, line 433. The attribute's comment: “the action is an action of sheaves: it commutes with the restriction maps of the sheaf SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}) and of the sheaf 061B”.

The action on the sheaf of lifts commutes with restriction. For a morphism k : V' ⟶ U' of the spaces-étale site of X', a section θ of the acting sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/T}, 𝒞_{X/X'}) over U' — an 𝒪_U-linear map (a^*Ω_{Y/T})|_U ⟶ 𝒞_{X/X'}|_U — and a section a' of the sheaf of lifts of [Stacks Project, Tag 061B] over U': (θ · a')|_{V'} = θ|_{V'} · a'|_{V'}. Here θ acts through its reading a|_U^*Ω_{Y/T} ⟶ 𝒞_{U/U'} (Stacks 03LU and [Stacks Project, Tag 04CQ]), and θ|_{V'} is the restriction of θ along V ⟶ U, read through Stacks 03LU.

theorem conormalLiftAction_map {U' V' : SpacesEtale C S hS X'} (k : V' ⟶ U')
    (θ : (modulePullback C S hS
          (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj U').hom ⟨G, hG.1⟩)).obj
          ((modulePullback C S hS (Y := (⟨(⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).1.toFunctor,
            (⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).2.1⟩ : AlgebraicSpaces C S hS)) (X :=
              (⟨(⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).1.toFunctor,
                (⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).2.1⟩ : AlgebraicSpaces C S hS)) a).obj
            (sheafOfDifferentials C S hS (subspaceInclusion C S hS Y' ⟨H, hH.1⟩ ≫ pY'))) ⟶
        (modulePullback C S hS
          (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj U').hom ⟨G, hG.1⟩)).obj
          (conormalModule C S hS X' ⟨G, hG.1⟩))
    (s : (conormalLiftSubfunctor C S hS hG hH pX' pY' a A).obj (op U')) :
    (conormalLiftSubfunctor C S hS hG hH pX' pY' a A).toFunctor.map k.op
        (conormalLiftAction C S hS pX' pY' a A hG₁ hH₁ U' (Iso.homCongr
          ((modulePullbackCompIso C S hS (Z :=
            (⟨(⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).1.toFunctor,
              (⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).2.1⟩ : AlgebraicSpaces C S hS))
          (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj U').hom ⟨G, hG.1⟩)
            a).app (sheafOfDifferentials C S hS (subspaceInclusion C S hS Y' ⟨H, hH.1⟩ ≫ pY')))
          (conormalRestrictionIso C S hS hG U') θ) s) =
      conormalLiftAction C S hS pX' pY' a A hG₁ hH₁ V'
        (Iso.homCongr ((modulePullbackCompIso C S hS (Z :=
          (⟨(⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).1.toFunctor,
            (⟨H, hH.1⟩ : ClosedSubspaces C S hS Y'.1).2.1⟩ : AlgebraicSpaces C S hS))
          (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj V').hom ⟨G, hG.1⟩)
            a).app (sheafOfDifferentials C S hS (subspaceInclusion C S hS Y' ⟨H, hH.1⟩ ≫ pY')))
          (conormalRestrictionIso C S hS hG V')
          (QuasiCoherentDescent.restrictForm C S hS
            (P := (⟨((⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).1.preimage
              ((SpacesEtale.inclusion C S hS X').obj V').hom.hom).toFunctor,
              (isClosedSubspace_preimage C S hS ((SpacesEtale.inclusion C S hS X').obj V').hom.hom
                (⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).1 X'.2
                  ((SpacesEtale.inclusion C S hS X').obj V').left.2
                    (⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).2).1⟩ :
              AlgebraicSpaces C S hS))
            (Q := (⟨((⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).1.preimage
              ((SpacesEtale.inclusion C S hS X').obj U').hom.hom).toFunctor,
              (isClosedSubspace_preimage C S hS ((SpacesEtale.inclusion C S hS X').obj U').hom.hom
                (⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).1 X'.2
                  ((SpacesEtale.inclusion C S hS X').obj U').left.2
                    (⟨G, hG.1⟩ : ClosedSubspaces C S hS X'.1).2).1⟩ :
              AlgebraicSpaces C S hS))
            ((SpacesEtale.toSpaces C S hS (IsThickening.space C S hS hG)).map
              ((thickeningPreimage C S hS hG).map k))
            (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj U').hom ⟨G, hG.1⟩)
            (preimageProjection C S hS ((SpacesEtale.inclusion C S hS X').obj V').hom ⟨G, hG.1⟩)
            (SpacesEtale.toSpaces_map_comp_structure C S hS (IsThickening.space C S hS hG)
              ((thickeningPreimage C S hS hG).map k)) θ))
        ((conormalLiftSubfunctor C S hS hG hH pX' pY' a A).toFunctor.map k.op s)

AlgebraicGeometry.Space.isSheaf_conormalLiftActingPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftActionSheaf.lean, line 153. The attribute's comment: “the acting sheaf SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}), read on (X')_{spaces, étale} through the identification 05ZL, is a sheaf”.

The acting presheaf SheafHom_{𝒪_X}(a^*Ω_{Y/T}, 𝒞_{X/X'}), read through U' ↦ X ×_{X'} U', is a sheaf on the spaces-étale site of X'.

theorem isSheaf_conormalLiftActingPresheaf :
    Presieve.IsSheaf (SpacesEtale.topology C S hS X')
      (conormalLiftActingPresheaf C S hS hG hH pY' a)

AlgebraicGeometry.Space.conormalLiftSheafAddAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftActionSheaf.lean, line 242. The attribute's comment: “the action, over every object U' of (X')_{spaces, étale}, of the sections of SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}) on the sections of the sheaf 061B”.

The action on the sheaf of lifts over U'. A section θ of the acting sheaf over U' acts on a section a' of the sheaf of lifts (061B) by the action θ · a' of [Stacks Project, Tag 0CK6], θ read as a map a|_U^*Ω_{Y/T} ⟶ 𝒞_{U/U'} by AlgebraicGeometry.Space.conormalLiftActingEquiv.

def conormalLiftSheafAddAction (U' : SpacesEtale C S hS X') :
    AddAction (conormalLiftActionHom C S hS hG hH pY' a U')
      ((conormalLiftSubfunctor C S hS hG hH pX' pY' a A).obj (op U'))

AlgebraicGeometry.Space.conormalLiftSheafAddAction_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftActionSheaf.lean, line 254. The attribute's comment: “the action is simply transitive over every object U' of (X')_{spaces, étale} over which the sheaf 061B has a section”.

Simple transitivity of the action on the sheaf of lifts over every object U' over which the sheaf of lifts (061B) has a section s: θ ↦ θ · s is a bijection from the sections of the acting sheaf over U' onto the sections of the sheaf of lifts over U'.

theorem conormalLiftSheafAddAction_bijective (U' : SpacesEtale C S hS X')
    (s : (conormalLiftSubfunctor C S hS hG hH pX' pY' a A).obj (op U')) :
    letI := conormalLiftSheafAddAction C S hS pX' pY' a A hG₁ hH₁ U'
    Function.Bijective (fun θ : conormalLiftActionHom C S hS hG hH pY' a U' => θ +ᵥ s)

Tag 061D, a remark

Tag 061D in the Stacks Project.

AlgebraicGeometry.Space.conormalLiftSubfunctor_eq_liftSubfunctor_of_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftSheaf/ConormalLiftSheaf.lean, line 428. The attribute's comment: “for Y = Y' the rule of 061A is the rule U' ↦ {a' : U' → Y over B with a'|_U = a|_U}, condition (3) being vacuous”.

For Y = Y' the rule of [Stacks, Tag 061A] is just the rule U' ↦ {a' : U' ⟶ Y' over T with a'|_U = a|_U}: condition (3) is vacuous, the map A being always zero.

theorem conormalLiftSubfunctor_eq_liftSubfunctor_of_eq_top (hHtop : H = ⊤) :
    conormalLiftSubfunctor C S hS hG hH pX' pY' a A = liftSubfunctor C S hS hG hH pX' pY' a

AlgebraicGeometry.Space.liftSubfunctor_remark_of_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftTrivialTarget.lean, line 142. The attribute's comment: “the special case Y = Y': A = 0, the sheaf of 061A is the rule U' ↦ {a' : U' → Y over B with a'|_U = a|_U}, and SheafHom_{O_X}(a^*Ω_{Y/B}, C_{X/X'}) acts on it (the action of 061C), simply transitively”.

Deformations of maps into a trivial thickening. The special case Y = Y' of Lemmas 0618, 04D0, 061A and 061C (the target thickening is the trivial one, H = ⊤): 1. the map A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} is always zero; 2. the sheaf of Lemma 061A is the rule U' ↦ {a' : U' ⟶ Y over B with a'|_U = a|_U} (AlgebraicGeometry.Space.liftSubfunctor); 3. the sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/B}, 𝒞_{X/X'}) acts on it (AlgebraicGeometry.Space.liftSheafAddActionOfEqTop, the action of Lemma 061C), simply transitively over every U' over which it has a section.

Here B is the base T, X ⊂ X' is a first order thickening and a : X ⟶ Y is arbitrary; the target Y ⊂ Y' is first order because it is trivial.

theorem liftSubfunctor_remark_of_eq_top (hHtop : H = ⊤) :
    (letI := Preadditive.homGroup (C := Modules.{u, u} C S hS (IsThickening.space C S hS hG).1
       (IsThickening.space C S hS hG).2)
       ((modulePullback C S hS a).obj (conormalModule C S hS Y' ⟨H, hH.1⟩))
       (conormalModule C S hS X' ⟨G, hG.1⟩)
     ∀ A' : (modulePullback C S hS a).obj (conormalModule C S hS Y' ⟨H, hH.1⟩) ⟶
        conormalModule C S hS X' ⟨G, hG.1⟩, A' = 0) ∧
    conormalLiftSubfunctor C S hS hG hH pX' pY' a A = liftSubfunctor C S hS hG hH pX' pY' a ∧
    ∀ (U' : SpacesEtale C S hS X') (s : (liftSubfunctor C S hS hG hH pX' pY' a).obj (op U')),
      letI := liftSheafAddActionOfEqTop C S hS pX' pY' a A hG₁ hHtop U'
      Function.Bijective (fun θ : conormalLiftActionHom C S hS hG hH pY' a U' => θ +ᵥ s)

AlgebraicGeometry.Space.liftActionAbelianSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftActionSheafOnAmbient.lean, line 135. The attribute's comment: “the acting sheaf carried to the spaces-etale site of the ambient space of the thickening, which is the site the sheaf of lifts lives on”.

The acting sheaf of [Stacks Project, Tag 061D], read on the spaces-étale site of the ambient space of the thickening. This is AlgebraicGeometry.Space.liftActionSheaf, the internal hom SheafHom_{𝒪_X}(a^*Ω_{Y/B}, 𝒞_{X/X'}) on the small étale site of the subspace X, carried to the spaces-étale site of X' by AlgebraicGeometry.Space.abelianSheafOnAmbient.

It is on the site of X' that the sheaf of lifts of [Stacks Project, Tag 061A] lives, so it is there that the action of [Stacks Project, Tag 061C] has to be read; its underlying presheaf (liftActionAbelianSheaf …).obj is the shape AlgebraicGeometry.Space.LiftDerivationAction takes its acting sheaf Θ in.

def liftActionAbelianSheaf (hG : IsThickening C S hS X' G) (q : Y ⟶ B)
    (a : IsThickening.space C S hS hG ⟶ Y) :
    Sheaf (SpacesEtale.topology C S hS X') AddCommGrpCat.{u + 1}

AlgebraicGeometry.Space.liftsSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheaf.lean, line 393. The attribute's comment: “the rule U' ↦ {a' : U' ⟶ Y over B with a'|_U = a|_U}”.

Stacks 061D. The sheaf of lifts of a : X ⟶ Y along the subspace X ⊆ X', in the case where the target is not deformed: the subfunctor of the restriction of Y to the small étale site of X' whose sections over a chart U' are the morphisms a' : U' ⟶ Y over B whose restriction to X ×_{X'} U' is the restriction of a.

def liftsSubfunctor (p : X' ⟶ B) (q : Y ⟶ B) {X : Subfunctor X'.1} (a : X.toFunctor ⟶ Y.1) :
    Subfunctor ((SmallEtale.toOver C S hS X'.1).op ⋙ Y.1)

AlgebraicGeometry.Space.isSheaf_liftsSubfunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheaf.lean, line 407. The attribute's comment: “the rule of the remark is a sheaf of sets”.

Stacks 061D. The lifts form a sheaf of sets on the small étale site of X': morphisms into an algebraic space satisfy étale descent, and both clauses of the lifting condition are local.

theorem isSheaf_liftsSubfunctor (p : X' ⟶ B) (q : Y ⟶ B) {X : Subfunctor X'.1}
    (a : X.toFunctor ⟶ Y.1) :
    Presheaf.IsSheaf (SmallEtale.topology C S hS X'.1)
      (liftsSubfunctor C S hS p q a).toFunctor

AlgebraicGeometry.Space.eq_zero_of_isZero_conormalModule_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheaf.lean, line 504. The attribute's comment: “the map A is always zero”.

Stacks 061D. In the case where the target is not deformed the map A of the general lifting problem is always zero: it is a morphism of 𝒪_X-modules out of the inverse image of the conormal module 𝒞_{Y/Y}, which vanishes.

theorem eq_zero_of_isZero_conormalModule_top (Z : ClosedSubspaces C S hS X'.1)
    (a : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces C S hS) ⟶
      (⟨(⊤ : Subfunctor Y.1).toFunctor, (isClosedSubspace_top C S hS Y).1⟩ :
        AlgebraicSpaces C S hS))
    (A : (modulePullback C S hS a).obj
        (conormalModule C S hS Y ⟨⊤, isClosedSubspace_top C S hS Y⟩) ⟶
      conormalModule C S hS X' Z) :
    A = 0

AlgebraicGeometry.Space.liftActionSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheaf.lean, line 523. The attribute's comment: “the acting sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/B}, 𝒞_{X/X'})”.

Stacks 061D. The sheaf acting on the lifts: the internal hom SheafHom_{𝒪_X}(a^*Ω_{Y/B}, 𝒞_{X/X'}) of 𝒪_X-modules on the small étale site of the closed subspace X ⊆ X', for a : X ⟶ Y over B. The sheaf of lifts it acts on is AlgebraicGeometry.Space.liftsSubfunctor taken at the underlying morphism of presheaves a.hom.

noncomputable def liftActionSheaf (Z : ClosedSubspaces C S hS X'.1) (q : Y ⟶ B)
    (a : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces C S hS) ⟶ Y) :
    Modules.{u, u + 1} C S hS Z.1.toFunctor Z.2.1

AlgebraicGeometry.Space.exists_liftActionSheafChart_addAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UndeformedTargetLiftAction.lean, line 386. The attribute's comment: “the action of SheafHom_{O_X}(a^*Omega_{Y/B}, C_{X/X'}) on the sheaf of lifts U' ↦ {a' : U' → Y over B with a'|_U = a|_U}: an additive action on the sections over every étale chart, commuting with the restriction maps of both sheaves, under which the comorphisms of θ · a' and a' differ by the derivation d_{Y/B} ∘ θ”.

[Stacks Project, Tag 061D], the action. Let X ⊂ X' be a first order thickening of algebraic spaces over S, let p : X' ⟶ B and q : Y ⟶ B, and let a : X ⟶ Y. The sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/B}, 𝒞_{X/X'}), read on the étale charts of X' (AlgebraicGeometry.Space.liftActionSheafChart), acts on the sheaf of lifts U' ↦ {a' : U' ⟶ Y over B with a'|_U = a|_U} (AlgebraicGeometry.Space.liftsSubfunctor):

• for every chart U' the sections of the acting sheaf over U' act additively on the lifts over U' (AddAction: 0 · a' = a' and (θ₁ + θ₂) · a' = θ₁ · (θ₂ · a'));
• the action commutes with the restriction maps of the two sheaves along every morphism of charts U'' ⟶ U', so it is an action of the sheaf on the sheaf;
• it is the action of [Stacks Project, Tag 0CK6]: on every chart m : T ⟶ U' on which a' factors through an affine chart ε : T ⟶ Q of Y carrying an affine chart diagram over B, θ · a' factors through Q by a morphism ψ whose map of regular functions is x ↦ ε^♯ x + ι_T (D x), where D = θ ∘ d_{Y/B} is the derivation of Equation (0619) read on the chart (AlgebraicGeometry.Space.LiftChart.derivation) and ι_T : 𝒞_{X/X'}(T_X) ⟶ Γ(T, 𝒪_T) is the inclusion of the conormal module (AlgebraicGeometry.Space.conormalChartIncl). That is, the comorphisms of θ · a' and a' differ by the derivation D.

theorem exists_liftActionSheafChart_addAction (hG : IsFirstOrderThickening C S hS X' G)
    (p : X' ⟶ Bs) (q : Y ⟶ Bs) (a : IsThickening.space C S hS hG.1 ⟶ Y) :
    ∃ act : ∀ U' : SmallEtale C S hS X'.1,
        AddAction ((liftActionSheafChart C S hS hG.1 q a).obj.obj (op U'))
          ((liftsSubfunctor C S hS p q a.hom).toFunctor.obj (op U')),
      (∀ {U' U'' : SmallEtale C S hS X'.1} (k : U'' ⟶ U')
          (θ : (liftActionSheafChart C S hS hG.1 q a).obj.obj (op U'))
          (x : (liftsSubfunctor C S hS p q a.hom).toFunctor.obj (op U')),
        (liftsSubfunctor C S hS p q a.hom).toFunctor.map k.op ((act U').vadd θ x) =
          (act U'').vadd ((liftActionSheafChart C S hS hG.1 q a).obj.map k.op θ)
            ((liftsSubfunctor C S hS p q a.hom).toFunctor.map k.op x)) ∧
      ∀ (U' : SmallEtale C S hS X'.1)
        (θ : (liftActionSheafChart C S hS hG.1 q a).obj.obj (op U'))
        (x : (liftsSubfunctor C S hS p q a.hom).toFunctor.obj (op U'))
        (T : SmallEtale C S hS X'.1) (m : T ⟶ U') (Q : SmallEtale C S hS Y.1)
        (ε : (SmallEtale.toOver C S hS X'.1).obj T ⟶ (SmallEtale.toOver C S hS Y.1).obj Q)
        (w : yoneda.map ε ≫ Q.1.hom =
          yoneda.map ((SmallEtale.toOver C S hS X'.1).map m) ≫ yonedaEquiv.symm x.1),
        HasAffineChartDiagram C S hS q Q →
        ∃ ψ : (SmallEtale.toOver C S hS X'.1).obj T ⟶ (SmallEtale.toOver C S hS Y.1).obj Q,
          yoneda.map ψ ≫ Q.1.hom = yoneda.map ((SmallEtale.toOver C S hS X'.1).map m) ≫
            yonedaEquiv.symm ((act U').vadd θ x).1 ∧
          ∀ f : (structureRingSheaf C S hS Y).obj.obj (op Q),
            ((BigFppfOver.toScheme C S hS).map ψ).appTop.hom f =
              ((BigFppfOver.toScheme C S hS).map ε).appTop.hom f +
                (show Γ((BigFppfOver.toScheme C S hS).obj
                    ((SmallEtale.toOver C S hS X'.1).obj T), ⊤) from
                  conormalChartIncl C S hS ⟨G, hG.1.1⟩ hG T
                    ((⟨T, m, Q, ε, w⟩ : LiftChart C S hS U' (yonedaEquiv.symm x.1)).derivation
                      (Z := ⟨G, hG.1.1⟩) (p := p) (q := q) (a := a) x.2 θ f))

Tag 0CK7, a remark

Tag 0CK7 in the Stacks Project.

AlgebraicGeometry.Space.epi_modulePullback_conormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModulePullbackEpi.lean, line 110. The attribute's comment: “surjectivity of the inverse image along a of the conormal surjection of a cartesian thickening”.

The inverse image of the surjection of Stacks 0CK7 is surjective. Let Z' be a closed subspace of an algebraic space X', let g : X ⟶ X' be a morphism of algebraic spaces, and let a : W ⟶ g⁻¹(Z') be a morphism of algebraic spaces. The inverse image along a of the canonical map of conormal modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{g⁻¹(Z')/X} of the fibre product square is an epimorphism of 𝒪_W-modules.

In the situation of Stacks 0CK7 the base is a thickening Z ⊆ Z' and Y = Z ×_{Z'} Y', so the map h^*𝒞_{Z/Z'} ⟶ 𝒞_{Y/Y'} is the conormal map of a fibre product square and is surjective by the surjectivity clause of Stacks 04CQ; this is the passage from that surjectivity to surjectivity of a^*h^*𝒞_{Z/Z'} ⟶ a^*𝒞_{Y/Y'} along a : X ⟶ Y, which the source performs in order to see that the map A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} is determined by a.

theorem epi_modulePullback_conormalMap {X X' : AlgebraicSpaces B S hS} (g : X ⟶ X')
    (Z' : ClosedSubspaces B S hS X'.1) {W : AlgebraicSpaces B S hS}
    (a : W ⟶ (⟨(preimageSubspace B S hS g Z').1.toFunctor,
      (preimageSubspace B S hS g Z').2.1⟩ : AlgebraicSpaces B S hS)) :
    Epi ((modulePullback B S hS a).map
      (conormalMap B S hS (preimageSubspace B S hS g Z') Z' g
        (preimageProjection B S hS g Z')
        (conormalEtaleRestrictionSquare B S hS g Z')))

AlgebraicGeometry.Space.liftSubfunctor_remark_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftCartesianTarget.lean, line 612. The attribute's comment: “the special case B = Z' a thickening of Z and Y = Z ×_{Z'} Y': A is determined by a, the sheaf of 061A is the rule U' ↦ {a' : U' → Y' over Z' with a'|_U = a|_U}, and SheafHom_{O_X}(a^*Ω_{Y/Z}, C_{X/X'}) acts on it (the action of 061C), simply transitively”.

The special case of Lemmas 0618, 04D0, 061A and 061C in which the base T = Z' is itself a thickening Z ⊂ Z' (any closed subspace K) and Y = Z ×_{Z'} Y' (the thickening H of Y' is the inverse image of Z): 1. the map A : a^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} is determined by a: it is the only map whose composite with a^* of the surjection h^*𝒞_{Z/Z'} ⟶ 𝒞_{Y/Y'} is the canonical map g^*𝒞_{Z/Z'} ⟶ 𝒞_{X/X'} induced by g' (AlgebraicGeometry.Space.IsCartesianConormalCompatible, which also records g = h ∘ a); 2. for this A the sheaf of Lemma 061A is the rule U' ↦ {a' : U' ⟶ Y' over Z' with a'|_U = a|_U} (AlgebraicGeometry.Space.liftSubfunctor); 3. the sheaf SheafHom_{𝒪_X}(a^*Ω_{Y/Z}, 𝒞_{X/X'}) acts on it (AlgebraicGeometry.Space.cartesianLiftSheafAddAction, the action of Lemma 061C read through Ω_{Y/Z'} = Ω_{Y/Z}), simply transitively over every U' over which it has a section.

Here X ⊂ X' and Y ⊂ Y' are first order thickenings, as in Lemma 061C.

theorem liftSubfunctor_remark_of_cartesian
    (A : (modulePullback C S hS a).obj
        (conormalModule C S hS Y' ⟨(preimageSubspace C S hS pY' K).1, hH.1⟩) ⟶
      conormalModule C S hS X' ⟨G, hG.1⟩)
    (hA : IsCartesianConormalCompatible C S hS ⟨G, hG.1⟩ K pX' pY' a A) :
    (∀ A' : (modulePullback C S hS a).obj
        (conormalModule C S hS Y' ⟨(preimageSubspace C S hS pY' K).1, hH.1⟩) ⟶
      conormalModule C S hS X' ⟨G, hG.1⟩,
      IsCartesianConormalCompatible C S hS ⟨G, hG.1⟩ K pX' pY' a A' → A' = A) ∧
    conormalLiftSubfunctor C S hS hG hH pX' pY' a A = liftSubfunctor C S hS hG hH pX' pY' a ∧
    ∀ (U' : SpacesEtale C S hS X') (s : (liftSubfunctor C S hS hG hH pX' pY' a).obj (op U')),
      letI := cartesianLiftSheafAddAction C S hS K pX' pY' a hG₁ hH₁ A hA U'
      Function.Bijective (fun θ : cartesianLiftActionHom C S hS K hG pY' hH a U' => θ +ᵥ s)

Tag 0CK8, a lemma

Tag 0CK8 in the Stacks Project.

AlgebraicGeometry.Space.derivationMove_comp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftEtaleCompatibility.lean, line 272. The attribute's comment: “the action of Remark 0CK6 is compatible with étale localization: (θ₂ · a₂') ≫ f' = h' ≫ (θ₁ · a₁') for θ₂ the composite a₂^Ω_{X₂/B₂} = h^a₁^Ω_{X₁/B₁} → h^C_{T₁/T₁'} → C_{T₂/T₂'}, the equality sign the identification of 04CU”.

Acting by a derivation commutes with étale localization. For a commutative diagram of first order thickenings (h, h') : (T₂ ⊂ T₂') ⟶ (T₁ ⊂ T₁'), (a_i, a_i') : (T_i ⊂ T_i') ⟶ (X_i ⊂ X_i'), (f, f') : (X₂ ⊂ X₂') ⟶ (X₁ ⊂ X₁') and a commutative square f' ≫ q₁ = q₂ ≫ ε with X₂ ⟶ X₁ and ε : B₂ ⟶ B₁ étale, and for θ₁ : a₁^*Ω_{X₁/B₁} ⟶ 𝒞_{T₁/T₁'} with θ₂ its étale localization (AlgebraicGeometry.Space.etaleLocalizedDerivationDatum, its last map the conormal map of (h, h')): (θ₂ · a₂') ≫ f' = h' ≫ (θ₁ · a₁'), the actions being those of [Stacks Project, Tag 0CK6] (AlgebraicGeometry.Space.derivationMove, T_i' over B_i through a_i').

theorem derivationMove_comp_of_etale
    (hT₁ : IsFirstOrderThickening B S hS T₁' Z₁.1) (hT₂ : IsFirstOrderThickening B S hS T₂' Z₂.1)
    (hX₁ : IsFirstOrderThickening B S hS X₁' W₁.1) (hX₂ : IsFirstOrderThickening B S hS X₂' W₂.1)
    (ca' : a₂' ≫ f' = h' ≫ a₁') (ca : @CategoryStruct.comp (AlgebraicSpaces B S hS) _ _ _ _ a₂ f =
      @CategoryStruct.comp (AlgebraicSpaces B S hS) _ _ _ _ h a₁)
    (hfet : IsEtale B S hS f.hom) (hεet : IsEtale B S hS ε.hom)
    (θ₁ : (modulePullback B S hS a₁).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS X₁' W₁ ≫ q₁)) ⟶
      conormalModule B S hS T₁' Z₁) :
    derivationMove B S hS Z₂ W₂ a₂ q₂ hT₂ a₂' ha₂
        (etaleLocalizedDerivationDatum B S hS (subspaceInclusion B S hS X₂' W₂ ≫ q₂)
          (subspaceInclusion B S hS X₁' W₁ ≫ q₁) f ε
          (comp_comp_eq_of_square_of_over B S hS W₁ W₂ f' f hf q₁ q₂ ε hq) a₂ h a₁ ca.symm
          (isIso_sheafOfDifferentialsMap_of_isEtale B S hS
            (subspaceInclusion B S hS X₁' W₁ ≫ q₁) f (subspaceInclusion B S hS X₂' W₂ ≫ q₂) ε
            hfet hεet (comp_comp_eq_of_square_of_over B S hS W₁ W₂ f' f hf q₁ q₂ ε hq))
          (conormalModule B S hS T₁' Z₁) (conormalModule B S hS T₂' Z₂) θ₁
          (conormalMap B S hS Z₂ Z₁ h' h hh)) (a₂' ≫ q₂) rfl ≫ f' =
      h' ≫ derivationMove B S hS Z₁ W₁ a₁ q₁ hT₁ a₁' ha₁ θ₁ (a₁' ≫ q₁) rfl

AlgebraicGeometry.Space.restrictedLiftAction_comp_etaleLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DeformationLiftEtaleLocalizationAction.lean, line 447.

The action of a derivation on lifts is compatible with étale localization. Let S be a scheme and consider a commutative diagram of first order thickenings of algebraic spaces over S

(T₂ ⊂ T₂') --(a₂, a₂')--> (X₂ ⊂ X₂')        X₂' --q₂--> B₂
   |                          |               |          |
 (h, h')                   (f, f')            f'         ε
   v                          v               v          v
(T₁ ⊂ T₁') --(a₁, a₁')--> (X₁ ⊂ X₁')        X₁' --q₁--> B₁

together with the commutative square on the right, with f : X₂ ⟶ X₁ and ε : B₂ ⟶ B₁ étale. For an 𝒪_{T₁}-linear map θ₁ : a₁^*Ω_{X₁/B₁} ⟶ 𝒞_{T₁/T₁'} let θ₂ be the composite

a₂^*Ω_{X₂/B₂} = h^*a₁^*Ω_{X₁/B₁} --h^*θ₁--> h^*𝒞_{T₁/T₁'} ⟶ 𝒞_{T₂/T₂'},

whose equality sign is the inverse image along a₂ of the identification f^*Ω_{X₁/B₁} ≅ Ω_{X₂/B₂} of [Stacks Project, Tag 04CU] (AlgebraicGeometry.Space.localizationDifferentialsIso) followed by the comparisons a₂^*f^* ≅ (a₂ ≫ f)^* = (h ≫ a₁)^* ≅ h^*a₁^* of [Stacks Project, Tag 03LU], and whose last map is the canonical map of conormal modules induced by the comorphism of h' on the defining ideals (AlgebraicGeometry.Space.conormalComorphism, transposed). Then

(θ₂ · a₂') ≫ f' = h' ≫ (θ₁ · a₁'),

the actions being those of Remark [Stacks Project, Tag 0CK6], AlgebraicGeometry.Space.restrictedLiftAction: θ · a' is the unique morphism of thickenings over the base whose difference from a' ([Stacks Project, Tag 0618], Equation (0619)) is θ, which exists by [Stacks Project, Tag 04D0].

theorem restrictedLiftAction_comp_etaleLocalization
    (_hX₁ : IsFirstOrderThickening B S hS X₁' X₁.1)
    (_hX₂ : IsFirstOrderThickening B S hS X₂' X₂.1)
    (θ₁ : (modulePullback B S hS a₁).obj
        (sheafOfDifferentials B S hS (subspaceInclusion B S hS X₁' X₁ ≫ q₁)) ⟶
      conormalModule B S hS T₁' T₁) :
    restrictedLiftAction B S hS T₂ X₂ hT₂ a₂ q₂ a₂' ha₂
        ((modulePullback B S hS a₂).map
            (localizationDifferentialsIso B S hS X₁ X₂ f' f hf q₁ q₂ ε hq hfet hεet).inv ≫
          (modulePullbackCompIso B S hS a₂ f).hom.app
            (sheafOfDifferentials B S hS (subspaceInclusion B S hS X₁' X₁ ≫ q₁)) ≫
          (eqToHom (congrArg (modulePullback B S hS)
            (show @CategoryStruct.comp (AlgebraicSpaces B S hS) _ _ _ _ a₂ f =
            @CategoryStruct.comp (AlgebraicSpaces B S hS) _ _ _ _ h a₁ from hsq))).app
            (sheafOfDifferentials B S hS (subspaceInclusion B S hS X₁' X₁ ≫ q₁)) ≫
          (modulePullbackCompIso B S hS h a₁).inv.app
            (sheafOfDifferentials B S hS (subspaceInclusion B S hS X₁' X₁ ≫ q₁)) ≫
          (modulePullback B S hS h).map θ₁ ≫
          ((modulePullbackAdjunction B S hS h).homEquiv _ _).symm
            (conormalComorphism B S hS T₁ T₂ hT₁ hT₂ h' h hh)) ≫ f' =
      h' ≫ restrictedLiftAction B S hS T₁ X₁ hT₁ a₁ q₁ a₁' ha₁ θ₁

Sources

• Section 76.17, Tag 0617
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_derivation_of_conormalMap_eq · AlgebraicGeometry.Space.derivationDirectImageEquiv · AlgebraicGeometry.Space.derivationDirectImageEquiv_apply · AlgebraicGeometry.Space.existsUnique_hom_conormalMap_eq_derivation_eq · AlgebraicGeometry.Space.derivationMove_spec · AlgebraicGeometry.Space.conormalLiftSubfunctor · AlgebraicGeometry.Space.isSheaf_conormalLiftSubfunctor · AlgebraicGeometry.Space.isSheaf_conormalLiftActingPresheaf

Section76.18 Infinitesimal deformations of algebraic spaces#

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

Tag 06BH, a lemma

Tag 06BH in the Stacks Project.

AlgebraicGeometry.Space.isIso_conormalMap_firstOrderThickening_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFirstOrderThickening.lean, line 81. The attribute's comment: “(1) implies (2), with f' flat as a morphism of small etale ringed topoi”.

Let (f, f') : (X ⊆ X') → (Y ⊆ Y') be a morphism of first-order thickenings of algebraic spaces in which X = Y ×_{Y'} X', that is in which the upper closed subspace is the inverse image g⁻¹(Y) of the lower one along g = f' and f is the projection. If f' is flat, as a morphism of small étale ringed topoi, then the canonical map of conormal modules f^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} is an isomorphism. The first-order thickening conditions on Y ⊆ Y' and on g⁻¹(Y) ⊆ X' are taken as hypotheses.

theorem isIso_conormalMap_firstOrderThickening_of_isFlat
    (_hY : IsFirstOrderThickening B S hS Y' Y.1)
    (_hX : IsFirstOrderThickening B S hS X' (preimageSubspace B S hS g Y).1)
    (hg : (smallEtaleRingedToposHom B S hS g).IsFlat) :
    IsIso (conormalMap B S hS (preimageSubspace B S hS g Y) Y g
      (preimageProjection B S hS g Y)
      (conormalEtaleRestrictionSquare B S hS g Y))

AlgebraicGeometry.Space.isFlat_and_isPullback_iff_isIso_conormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFlatDeformation.lean, line 338.

[Stacks Project, Tag 06BH]. Let (f, f') : (X ⊆ X') → (Y ⊆ Y') be a morphism of first-order thickenings of algebraic spaces over S — X ⊆ X' and Y ⊆ Y' first-order thickenings, f' = g : X' ⟶ Y' and f : X ⟶ Y with commuting square of inclusions — and let f be flat. Then the following are equivalent:

1. f' is flat and X = Y ×_{Y'} X';
2. the canonical map f^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} of [Stacks Project, Tag 04CP] is an isomorphism.

Both flatness conditions are AlgebraicGeometry.Space.IsFlat of [Stacks Project, Tag 03ML], X = Y ×_{Y'} X' is cartesianness of the square of inclusions, and the canonical map is AlgebraicGeometry.Space.conormalMap. The first-order thickening hypotheses are used only in (2) ⟹ (1), and so is the flatness of f.

theorem isFlat_and_isPullback_iff_isIso_conormalMap
    (hX : IsFirstOrderThickening B S hS X' X.1) (hY : IsFirstOrderThickening B S hS Y' Y.1)
    (hf : IsFlat B S hS f.hom) :
    (IsFlat B S hS g.hom ∧
        IsPullback (subspaceInclusion B S hS X' X) f g (subspaceInclusion B S hS Y' Y)) ↔
      IsIso (conormalMap B S hS X Y g f hsq)

AlgebraicGeometry.Space.isFlat_and_isPullback_iff_isIso_conormalMapOfImmersions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FirstOrderThickeningFlatConormal.lean, line 265.

[Stacks Project, Tag 06BH]. Let (f, g) : (X ⊆ X') → (Y ⊆ Y') be a morphism of first-order thickenings of algebraic spaces over S (a commutative square of inclusions of closed subspaces which are first-order thickenings, [Stacks Project, Tag 05ZK]), and assume that f is flat. Then the following are equivalent:

1. g is flat and X = Y ×_{Y'} X';
2. the canonical map f^*𝒞_{Y/Y'} ⟶ 𝒞_{X/X'} of [Stacks Project, Tag 04CP] is an isomorphism.

Flatness is that of [Stacks Project, Tag 03ML], the equality X = Y ×_{Y'} X' is the square being cartesian, and the canonical map is that of the two inclusions read as immersions.

theorem isFlat_and_isPullback_iff_isIso_conormalMapOfImmersions
    (hsq : subspaceInclusion B S hS X' X ≫ g = f ≫ subspaceInclusion B S hS Y' Y)
    (hX : IsFirstOrderThickening B S hS X' X.1) (hY : IsFirstOrderThickening B S hS Y' Y.1)
    (hf : IsFlat B S hS f.hom) :
    (IsFlat B S hS g.hom ∧
        IsPullback (subspaceInclusion B S hS X' X) f g (subspaceInclusion B S hS Y' Y)) ↔
      IsIso (conormalMapOfImmersions B S hS (subspaceInclusion B S hS X' X)
        (subspaceInclusion B S hS Y' Y) f g (isImmersion_subspaceInclusion B S hS X' X)
        (isImmersion_subspaceInclusion B S hS Y' Y) hsq)

Tag 0CG5, a lemma

Tag 0CG5 in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_isFlat_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Flat.lean, line 306. The attribute's comment: “flatness of the upper morphism”.

Stacks 0CG5, flatness of the ambient morphism. In a commuting diagram of thickenings of algebraic spaces over S with the base thickening of finite order, the ambient source flat over the ambient base and both unprimed spaces the base changes of their primed counterparts, flatness of the morphism of special fibres implies flatness of its ambient deformation.

This is the forward implication of part 0CG8 of Tag 0CG6, which is AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFlat_iff.

theorem isFlat_of_isFlat_restriction
    (hiX : IsThickening B S hS X' X) (hiY : IsThickening B S hS Y' Y)
    (hiB : IsFiniteOrderThickening B S hS B' B₀)
    (hcartX : IsPullback X.ι pX pX' B₀.ι) (hcartY : IsPullback Y.ι pY pY' B₀.ι)
    (hinner : f ≫ pY = pX) (houter : f' ≫ pY' = pX')
    (hrestrict : X.ι ≫ f' = f ≫ Y.ι)
    (hXflat : IsFlat B S hS pX') (hfflat : IsFlat B S hS f) :
    IsFlat B S hS f'

AlgebraicGeometry.Space.isFlatAt_base_of_isFlat_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Flat.lean, line 322. The attribute's comment: “flatness of the upper target at image points”.

Stacks 0CG5, flatness of the ambient target along the image. In the situation of AlgebraicGeometry.Space.isFlat_of_isFlat_restriction the ambient target is flat over the ambient base at every point in the image of the ambient morphism.

theorem isFlatAt_base_of_isFlat_restriction
    (hiX : IsThickening B S hS X' X) (hiY : IsThickening B S hS Y' Y)
    (hiB : IsFiniteOrderThickening B S hS B' B₀)
    (hcartX : IsPullback X.ι pX pX' B₀.ι) (hcartY : IsPullback Y.ι pY pY' B₀.ι)
    (hinner : f ≫ pY = pX) (houter : f' ≫ pY' = pX')
    (hrestrict : X.ι ≫ f' = f ≫ Y.ι)
    (hXflat : IsFlat B S hS pX') (hfflat : IsFlat B S hS f)
    (x' : points B S hS X'.1) :
    IsFlatAt B S hS pY' (pointsMap B S hS X'.1 f' x')

Tag 0CG6, a lemma

Tag 0CG6 in the Stacks Project.

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFiniteLocallyFree_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FiniteLocallyFreeProperty.lean, line 145. The attribute's comment: “0CGV: finite locally free”.

Stacks 0CG6, part 0CGV. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is finite locally free if and only if its ambient deformation is.

theorem isFiniteLocallyFree_iff :
    IsFiniteLocallyFree T S hS D.smallHom ↔ IsFiniteLocallyFree T S hS D.ambientHom

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFiniteLocallyFreeOfRank_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FiniteLocallyFreeProperty.lean, line 159. The attribute's comment: “0CGV: finite locally free of rank d”.

Stacks 0CG6, part 0CGV, with the rank. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is finite locally free of rank d if and only if its ambient deformation is.

theorem isFiniteLocallyFreeOfRank_iff (d : ℕ) :
    IsFiniteLocallyFreeOfRank T S hS D.smallHom d ↔
      IsFiniteLocallyFreeOfRank T S hS D.ambientHom d

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFlat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 109. The attribute's comment: “0CG8: flat”.

Stacks 0CG6, part 0CG8. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is flat if and only if its ambient deformation is.

theorem isFlat_iff : IsFlat T S hS D.f ↔ IsFlat T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isSurjective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 116. The attribute's comment: “0CGF: surjective”.

Stacks 0CG6, part 0CGF. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is surjective if and only if its ambient deformation is.

theorem isSurjective_iff : IsSurjective T S hS D.f ↔ IsSurjective T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isLocallyOfFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 124. The attribute's comment: “0CGI: locally of finite type”.

Stacks 0CG6, part 0CGI. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is locally of finite type if and only if its ambient deformation is.

theorem isLocallyOfFiniteType_iff :
    IsLocallyOfFiniteType T S hS D.f ↔ IsLocallyOfFiniteType T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isLocallyQuasiFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 134. The attribute's comment: “0CGJ: locally quasi-finite”.

Stacks 0CG6, part 0CGJ. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is locally quasi-finite if and only if its ambient deformation is.

theorem isLocallyQuasiFinite_iff :
    IsLocallyQuasiFinite T S hS D.f ↔ IsLocallyQuasiFinite T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isLocallyOfFinitePresentation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 144. The attribute's comment: “0CGK: locally of finite presentation”.

Stacks 0CG6, part 0CGK. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is locally of finite presentation if and only if its ambient deformation is.

theorem isLocallyOfFinitePresentation_iff :
    IsLocallyOfFinitePresentation T S hS D.f ↔ IsLocallyOfFinitePresentation T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isSyntomic_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 153. The attribute's comment: “0CGN: syntomic”.

Stacks 0CG6, part 0CGN. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is syntomic if and only if its ambient deformation is.

theorem isSyntomic_iff : IsSyntomic T S hS D.f ↔ IsSyntomic T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isSmooth_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 160. The attribute's comment: “0CGP: smooth”.

Stacks 0CG6, part 0CGP. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is smooth if and only if its ambient deformation is.

theorem isSmooth_iff : IsSmooth T S hS D.f ↔ IsSmooth T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isUnramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 167. The attribute's comment: “0CGQ: unramified”.

Stacks 0CG6, part 0CGQ. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is unramified if and only if its ambient deformation is.

theorem isUnramified_iff : IsUnramified T S hS D.f ↔ IsUnramified T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isEtale_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Properties.lean, line 174. The attribute's comment: “0CGR: étale”.

Stacks 0CG6, part 0CGR. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is étale if and only if its ambient deformation is.

theorem isEtale_iff : IsEtale T S hS D.f ↔ IsEtale T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isRelativelyRepresentable_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 150. The attribute's comment: “0CG7: representable”.

Stacks 0CG6, part 0CG7. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is representable if and only if its ambient deformation is.

theorem isRelativelyRepresentable_iff :
    yoneda.relativelyRepresentable D.f ↔ yoneda.relativelyRepresentable D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isQuasiCompact_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 158. The attribute's comment: “0CGB: quasi-compact”.

Stacks 0CG6, part 0CGB. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is quasi-compact if and only if its ambient deformation is.

theorem isQuasiCompact_iff : IsQuasiCompact T S hS D.f ↔ IsQuasiCompact T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.universallyClosed_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 165. The attribute's comment: “0CGC: universally closed”.

Stacks 0CG6, part 0CGC. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is universally closed if and only if its ambient deformation is.

theorem universallyClosed_iff : UniversallyClosed T S hS D.f ↔ UniversallyClosed T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isSeparated_iff_and_isQuasiSeparated_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 173. The attribute's comment: “0CGD: separated, and quasi-separated”.

Stacks 0CG6, part 0CGD. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is separated if and only if its ambient deformation is, and it is quasi-separated if and only if its ambient deformation is.

theorem isSeparated_iff_and_isQuasiSeparated_iff :
    (IsSeparated T S hS D.f ↔ IsSeparated T S hS D.f') ∧
      (IsQuasiSeparated T S hS D.f ↔ IsQuasiSeparated T S hS D.f')

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.universallyInjective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 183. The attribute's comment: “0CGG: universally injective”.

Stacks 0CG6, part 0CGG. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is universally injective if and only if its ambient deformation is.

theorem universallyInjective_iff :
    UniversallyInjective T S hS D.f ↔ UniversallyInjective T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isAffineHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 191. The attribute's comment: “0CGH: affine”.

Stacks 0CG6, part 0CGH. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is affine if and only if its ambient deformation is.

theorem isAffineHom_iff : IsAffineHom T S hS D.f ↔ IsAffineHom T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.universallyOpen_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 198. The attribute's comment: “0CGM: universally open”.

Stacks 0CG6, part 0CGM. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is universally open if and only if its ambient deformation is.

theorem universallyOpen_iff : UniversallyOpen T S hS D.f ↔ UniversallyOpen T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isIntegralHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 205. The attribute's comment: “0CGT: integral”.

Stacks 0CG6, part 0CGT. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is integral if and only if its ambient deformation is.

theorem isIntegralHom_iff : IsIntegralHom T S hS D.f ↔ IsIntegralHom T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 214. The attribute's comment: “0CGE: monomorphism”.

Stacks 0CG6, part 0CGE. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is a monomorphism if and only if its ambient deformation is.

theorem mono_iff : Mono D.f ↔ Mono D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isLocallyOfFiniteType_and_hasRelativeDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 221. The attribute's comment: “0CGL: locally of finite type of relative dimension d”.

Stacks 0CG6, part 0CGL. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is locally of finite type of relative dimension d if and only if its ambient deformation is.

theorem isLocallyOfFiniteType_and_hasRelativeDimension_iff (d : ℕ) :
    (IsLocallyOfFiniteType T S hS D.f ∧ HasRelativeDimension d T S hS D.f) ↔
      (IsLocallyOfFiniteType T S hS D.f' ∧ HasRelativeDimension d T S hS D.f')

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 230. The attribute's comment: “0CGS: proper”.

Stacks 0CG6, part 0CGS. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is proper if and only if its ambient deformation is.

theorem isProper_iff : IsProper T S hS D.f ↔ IsProper T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 236. The attribute's comment: “0CGU: finite”.

Stacks 0CG6, part 0CGU. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is finite if and only if its ambient deformation is.

theorem isFinite_iff : IsFinite T S hS D.f ↔ IsFinite T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isOpenImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 266. The attribute's comment: “0CGA: open immersion”.

Stacks 0CG6, part 0CGA. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is an open immersion if and only if its ambient deformation is.

theorem isOpenImmersion_iff : IsOpenImmersion T S hS D.f ↔ IsOpenImmersion T S hS D.f'

AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isIso_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/ThickeningProperties.lean, line 279. The attribute's comment: “0CG9: isomorphism”.

Stacks 0CG6, part 0CG9. In a cartesian finite-order deformation of algebraic spaces the morphism of special fibres is an isomorphism if and only if its ambient deformation is.

theorem isIso_iff : IsIso D.f ↔ IsIso D.f'

Tag 0CGW, a lemma

Tag 0CGW in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Flatness.lean, line 48. The attribute's comment: “flatness of the ambient morphism”.

In a flat deformation diagram of algebraic spaces, flatness of the morphism of special fibres implies flatness of its ambient deformation.

theorem isFlat_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS)
    (hf : IsFlat B S hS D.f.hom) : IsFlat B S hS D.f'.hom

AlgebraicGeometry.Space.isFlatAt_target_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/Flatness.lean, line 56. The attribute's comment: “flatness of the ambient target over the ambient base along the image”.

In a flat deformation diagram of algebraic spaces whose morphism of special fibres is flat, the ambient target is flat over the ambient base at every point in the image of the ambient morphism.

theorem isFlatAt_target_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS)
    (hf : IsFlat B S hS D.f.hom) (x' : points B S hS D.X'.1) :
    IsFlatAt B S hS D.g'.hom (pointsMap B S hS D.X'.1 D.f'.hom x')

Tag 0CGX, a lemma

Tag 0CGX in the Stacks Project.

AlgebraicGeometry.Space.isFlat_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 155. The attribute's comment: “part (2): flat”.

Stacks 0CGX, part (2). Flatness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isFlat_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsFlat B S hS D.f.hom ↔ IsFlat B S hS D.f'.hom

AlgebraicGeometry.Space.isSurjective_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 198. The attribute's comment: “part (9): surjective”.

Stacks 0CGX, part (9). Surjectivity of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isSurjective_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsSurjective B S hS D.f.hom ↔ IsSurjective B S hS D.f'.hom

AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 210. The attribute's comment: “part (12): locally quasi-finite”.

Stacks 0CGX, part (12). Local quasi-finiteness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isLocallyQuasiFinite_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsLocallyQuasiFinite B S hS D.f.hom ↔ IsLocallyQuasiFinite B S hS D.f'.hom

AlgebraicGeometry.Space.isSyntomic_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 219. The attribute's comment: “part (15): syntomic”.

Stacks 0CGX, part (15). Syntomicity of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isSyntomic_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsSyntomic B S hS D.f.hom ↔ IsSyntomic B S hS D.f'.hom

AlgebraicGeometry.Space.isSmooth_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 227. The attribute's comment: “part (16): smooth”.

Stacks 0CGX, part (16). Smoothness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isSmooth_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsSmooth B S hS D.f.hom ↔ IsSmooth B S hS D.f'.hom

AlgebraicGeometry.Space.isUnramified_iff_isUnramified_deformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 235. The attribute's comment: “part (17): unramified”.

Stacks 0CGX, part (17). Unramifiedness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isUnramified_iff_isUnramified_deformation (D : FlatDeformationDiagram B S hS) :
    IsUnramified B S hS D.f.hom ↔ IsUnramified B S hS D.f'.hom

AlgebraicGeometry.Space.isEtale_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 243. The attribute's comment: “part (18): étale”.

Stacks 0CGX, part (18). Étaleness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isEtale_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsEtale B S hS D.f.hom ↔ IsEtale B S hS D.f'.hom

AlgebraicGeometry.Space.universallyInjective_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 334. The attribute's comment: “part (10): universally injective”.

Stacks 0CGX, part (10). Universal injectivity of a morphism of algebraic spaces is invariant under a flat deformation.

theorem universallyInjective_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    UniversallyInjective B S hS D.f.hom ↔ UniversallyInjective B S hS D.f'.hom

AlgebraicGeometry.Space.isIso_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformation.lean, line 350. The attribute's comment: “part (3): isomorphism”.

Stacks 0CGX, part (3). Being an isomorphism is invariant under a flat deformation of algebraic spaces.

theorem isIso_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsIso D.f.hom ↔ IsIso D.f'.hom

AlgebraicGeometry.Space.isFiniteLocallyFree_iff_and_isFiniteLocallyFreeOfRank_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationFiniteLocallyFree.lean, line 161. The attribute's comment: “part (21): finite locally free, and finite locally free of rank d”.

Stacks 0CGX, part (21). Being finite locally free, and being finite locally free of a given rank d, in the sense of Stacks 03ZV — affine, with f_*𝒪_X a finite locally free 𝒪_Y-module (of rank d) — are each invariant under a flat deformation of algebraic spaces.

theorem isFiniteLocallyFree_iff_and_isFiniteLocallyFreeOfRank_iff_of_flatDeformationDiagram
    (D : FlatDeformationDiagram B S hS) :
    (IsFiniteLocallyFree B S hS D.f ↔ IsFiniteLocallyFree B S hS D.f') ∧
      ∀ d : ℕ,
        IsFiniteLocallyFreeOfRank B S hS D.f d ↔ IsFiniteLocallyFreeOfRank B S hS D.f' d

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

Representability of a morphism of algebraic spaces is invariant under a flat deformation.

theorem relativelyRepresentable_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    yoneda.relativelyRepresentable D.f.hom ↔ yoneda.relativelyRepresentable D.f'.hom

AlgebraicGeometry.Space.isQuasiCompact_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 123. The attribute's comment: “part (5): quasi-compact”.

Quasi-compactness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isQuasiCompact_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsQuasiCompact B S hS D.f.hom ↔ IsQuasiCompact B S hS D.f'.hom

AlgebraicGeometry.Space.universallyClosed_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 132. The attribute's comment: “part (6): universally closed”.

Universal closedness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem universallyClosed_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    UniversallyClosed B S hS D.f.hom ↔ UniversallyClosed B S hS D.f'.hom

AlgebraicGeometry.Space.isSeparated_iff_and_isQuasiSeparated_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 141. The attribute's comment: “part (7): separated, and quasi-separated”.

Separatedness, and quasi-separatedness, of a morphism of algebraic spaces are each invariant under a flat deformation.

theorem isSeparated_iff_and_isQuasiSeparated_iff_of_flatDeformationDiagram
    (D : FlatDeformationDiagram B S hS) :
    (IsSeparated B S hS D.f.hom ↔ IsSeparated B S hS D.f'.hom) ∧
      (IsQuasiSeparated B S hS D.f.hom ↔ IsQuasiSeparated B S hS D.f'.hom)

AlgebraicGeometry.Space.isAffineHom_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 156. The attribute's comment: “part (11): affine”.

Affineness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isAffineHom_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsAffineHom B S hS D.f.hom ↔ IsAffineHom B S hS D.f'.hom

AlgebraicGeometry.Space.universallyOpen_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 164. The attribute's comment: “part (14): universally open”.

Universal openness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem universallyOpen_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    UniversallyOpen B S hS D.f.hom ↔ UniversallyOpen B S hS D.f'.hom

AlgebraicGeometry.Space.mono_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 181. The attribute's comment: “part (8): monomorphism”.

Being a monomorphism is invariant under a flat deformation of algebraic spaces.

theorem mono_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    Mono D.f.hom ↔ Mono D.f'.hom

AlgebraicGeometry.Space.isLocallyOfFiniteType_and_hasRelativeDimension_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 196. The attribute's comment: “part (13): locally of finite type of relative dimension d”.

Being locally of finite type of relative dimension d is invariant under a flat deformation of algebraic spaces: the morphism under study is locally of finite type of relative dimension d exactly when its ambient deformation is.

theorem isLocallyOfFiniteType_and_hasRelativeDimension_iff_of_flatDeformationDiagram
    (D : FlatDeformationDiagram B S hS) (d : ℕ) :
    (IsLocallyOfFiniteType B S hS D.f.hom ∧ HasRelativeDimension d B S hS D.f.hom) ↔
      (IsLocallyOfFiniteType B S hS D.f'.hom ∧ HasRelativeDimension d B S hS D.f'.hom)

AlgebraicGeometry.Space.isProper_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 212. The attribute's comment: “part (19): proper”.

Properness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isProper_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsProper B S hS D.f.hom ↔ IsProper B S hS D.f'.hom

AlgebraicGeometry.Space.isFinite_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationMorphismClasses.lean, line 221. The attribute's comment: “part (20): finite”.

Finiteness of a morphism of algebraic spaces is invariant under a flat deformation.

theorem isFinite_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsFinite B S hS D.f.hom ↔ IsFinite B S hS D.f'.hom

AlgebraicGeometry.Space.isOpenImmersion_iff_of_flatDeformationDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Deformations/FlatDeformationOpenImmersion.lean, line 41. The attribute's comment: “part (4): open immersion”.

Being an open immersion is invariant under a flat deformation of algebraic spaces: f is an open immersion if and only if f' is.

theorem isOpenImmersion_iff_of_flatDeformationDiagram (D : FlatDeformationDiagram B S hS) :
    IsOpenImmersion B S hS D.f.hom ↔ IsOpenImmersion B S hS D.f'.hom

Sources

• Section 76.18, Tag 06BG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isIso_conormalMap_firstOrderThickening_of_isFlat · AlgebraicGeometry.Space.isFlat_and_isPullback_iff_isIso_conormalMap · AlgebraicGeometry.Space.isFlat_and_isPullback_iff_isIso_conormalMapOfImmersions · AlgebraicGeometry.Space.isFlat_of_isFlat_restriction · AlgebraicGeometry.Space.isFlatAt_base_of_isFlat_restriction · AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFiniteLocallyFree_iff · AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFiniteLocallyFreeOfRank_iff · AlgebraicGeometry.Space.CartesianFiniteOrderDeformation.isFlat_iff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.