76.3 Radicial morphisms to 76.7 Sheaf of differentials of…

Section76.3 Radicial morphisms #

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

Tag 0481, a definition

Tag 0481 in the Stacks Project.

AlgebraicGeometry.Space.IsRadicial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 153.

Stacks 0481. A morphism of algebraic spaces over S is radicial if for every field k in the chosen site and every k-valued point of the target, the reduction of the fibre is either empty or is represented, over Spec(k), by the spectrum of a purely inseparable extension of k.

def IsRadicial (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) : Prop

Tag 0482, a lemma

Tag 0482 in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_of_isRadicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 338. References: EGA I (3.5.11), “radicial => univ. inj.”.

Stacks 0482. A radicial morphism of algebraic spaces is universally injective.

On a field-valued point of the target the fibre's reduction is either empty, excluding the point, or the spectrum of a purely inseparable extension, and a scheme-theoretic section of such a spectrum over the base field is unique; two points of the fibre therefore agree.

theorem universallyInjective_of_isRadicial
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hf : IsRadicial B S hS hX hY f) :
    UniversallyInjective B S hS f

Tag 0483, an example

Tag 0483 in the Stacks Project.

AlgebraicGeometry.RationalGaloisQuotient.universallyInjective_galoisQuotientToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotient.lean, line 349. The attribute's comment: “universally injective”.

Stacks 0483. The Galois quotient of Spec ℚ̄ is universally injective over Spec ℚ, although it is not radicial.

Universal injectivity is tested on field-valued points, so it suffices to make two sections of the quotient over the spectrum of a field agree over a further field spectrum. The projection of Spec ℚ̄ onto the quotient is locally surjective, so after two successive restrictions both sections come from morphisms to Spec ℚ̄, that is from two ℚ-embeddings of ℚ̄ into the field of the second restriction; those differ by an element of the Galois group, which is exactly what the quotient divides out.

theorem universallyInjective_galoisQuotientToBase :
    Space.UniversallyInjective B base hS (galoisQuotientToBase B hS hU)

AlgebraicGeometry.RationalGaloisQuotient.not_isRadicial_galoisQuotientToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotientNotRadicial.lean, line 171. The attribute's comment: “not radicial”.

Stacks 0483. The structure morphism of the Galois quotient of Spec ℚ̄ to Spec ℚ is not radicial.

Radicialness is tested at the field ℚ itself, on the terminal object of the site with the identity point of the base, so that the fibre is the quotient itself. Its reduction is not pointless, because the ℚ̄-valued point coming from the projection of Spec ℚ̄ survives to the reduction; and it is not the spectrum of a purely inseparable extension L of ℚ either: ℚ is perfect, so the structure map ℚ → L is surjective, while a field algebraic over ℚ carrying a point of the quotient is a copy of ℚ̄ or of the real algebraic numbers by AlgebraicGeometry.RationalGaloisQuotient.fieldPoint_algEquiv_algebraicClosure_or_real, and the structure map of ℚ into either of those is not surjective, both fields containing a square root of two.

theorem not_isRadicial_galoisQuotientToBase :
    ¬ Space.IsRadicial B base hS (isAlgebraicSpace_galoisQuotient B hS hU)
      (isAlgebraicSpace_yoneda B base hS (Over.mk (𝟙 (B.obj hS))))
      (galoisQuotientToBase B hS hU)

AlgebraicGeometry.RationalGaloisQuotient.universallyInjective_and_not_isRadicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotientNotRadicial.lean, line 213. The attribute's comment: “the two halves together, over a big fppf site containing the two spectra”.

Stacks 0483. The structure morphism of the Galois quotient of Spec ℚ̄ to Spec ℚ is universally injective but is not radicial: for algebraic spaces, unlike for schemes, universal injectivity is strictly weaker than radicialness.

This is the conjunction over a fixed big fppf site containing the two spectra; AlgebraicGeometry.RationalGaloisQuotient.exists_universallyInjective_not_isRadicial exhibits such a site and so asserts the non-equivalence outright.

theorem universallyInjective_and_not_isRadicial :
    Space.UniversallyInjective B base hS (galoisQuotientToBase B hS hU) ∧
      ¬ Space.IsRadicial B base hS (isAlgebraicSpace_galoisQuotient B hS hU)
        (isAlgebraicSpace_yoneda B base hS (Over.mk (𝟙 (B.obj hS))))
        (galoisQuotientToBase B hS hU)

AlgebraicGeometry.RationalGaloisQuotient.exists_universallyInjective_not_isRadicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotientNotRadicial.lean, line 234.

Stacks 0483. Universal injectivity is not equivalent to radicialness for morphisms of algebraic spaces: there are a big fppf site over Spec ℚ, an algebraic space over Spec ℚ in it, and a structure morphism of that space to Spec ℚ which is universally injective and is not radicial.

Nothing is assumed: the site is the one AlgebraicGeometry.BigFppfSite.exists_containing supplies for the two schemes Spec ℚ and Spec ℚ̄, and the space is the Galois quotient of Spec ℚ̄, so this is AlgebraicGeometry.RationalGaloisQuotient.universallyInjective_and_not_isRadicial with its site hypotheses discharged.

theorem exists_universallyInjective_not_isRadicial :
    ∃ (B : BigFppfSite.{0}) (hS : B.Contains base)
      (X : (BigFppfOver B base hS)ᵒᵖ ⥤ Type 0) (hX : IsAlgebraicSpace B base hS X)
      (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hS)))),
      Space.UniversallyInjective B base hS f ∧
        ¬ Space.IsRadicial B base hS hX
          (isAlgebraicSpace_yoneda B base hS (Over.mk (𝟙 (B.obj hS)))) f

Tag 0484, a lemma

Tag 0484 in the Stacks Project.

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

Stacks 0484, part (1). A universally injective decent morphism of algebraic spaces over S is radicial.

Over a field-valued point of the target the reduction of the fibre is a reduced decent algebraic space whose point set is a subsingleton, hence empty or the spectrum of a field by Stacks 047Z, and the resulting extension is purely inseparable because its spectrum map is again universally injective.

theorem isRadicial_of_universallyInjective_of_isDecent
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hinj : UniversallyInjective B S hS f)
    (hdecent : IsDecent B S hS f) :
    IsRadicial B S hS hX hY f

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

Stacks 0484, part (2). A universally injective quasi-separated morphism of algebraic spaces over S is radicial: a quasi-separated morphism is very reasonable, hence reasonable, hence decent.

theorem isRadicial_of_universallyInjective_of_isQuasiSeparated
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hinj : UniversallyInjective B S hS f)
    (hqs : IsQuasiSeparated B S hS f) :
    IsRadicial B S hS hX hY f

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

Stacks 0484, part (3). A universally injective locally separated morphism of algebraic spaces over S is radicial.

Universal injectivity makes the relative diagonal surjective and local separatedness makes it an immersion, so it is a closed immersion; the morphism is therefore separated, in particular quasi-separated.

theorem isRadicial_of_universallyInjective_of_isLocallySeparated
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hinj : UniversallyInjective B S hS f)
    (hls : IsLocallySeparated B S hS f) :
    IsRadicial B S hS hX hY f

Tag 049E, a remark

Tag 049E in the Stacks Project.

AlgebraicGeometry.RationalGaloisQuotient.isWeaklyRadicial_galoisQuotientBaseChangeToCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotientBaseChange.lean, line 439. The attribute's comment: “the base change of Example 0483 to ℚ̄ is weakly radicial”.

Stacks 049E. The base change X_ℚ̄ ⟶ Spec ℚ̄ of the morphism of Stacks 0483 is weakly radicial.

Over a field-valued point Spec(K) ⟶ Spec ℚ̄ the fibre has a section, through the projection of Spec ℚ̄ onto the Galois quotient; a section is a monomorphism, and it exhibits the trivial, purely inseparable, extension K ⊂ K. The point set of the fibre is a singleton because it receives the point of the section and because the base change of the universally injective morphism of Stacks 0483 is universally injective.

theorem isWeaklyRadicial_galoisQuotientBaseChangeToCover :
    Space.IsWeaklyRadicial B base hS (isAlgebraicSpace_galoisQuotientBaseChange B hS hU)
      (isAlgebraicSpace_yoneda B base hS _) (galoisQuotientBaseChangeToCover B hS hU)

AlgebraicGeometry.RationalGaloisQuotient.not_isRadicial_galoisQuotientBaseChangeToCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RationalGaloisQuotientBaseChange.lean, line 546. The attribute's comment: “the base change of Example 0483 to ℚ̄ is not radicial”.

Stacks 049E. The base change X_ℚ̄ ⟶ Spec ℚ̄ of the morphism of Stacks 0483 is not radicial.

Were it radicial, the two projections Spec ℚ̄ ×_ℚ Spec ℚ̄ ⟶ Spec ℚ̄, which are morphisms from the reduced scheme Spec(ℚ̄ ⊗_ℚ ℚ̄), would have the same image in the Galois quotient (AlgebraicGeometry.RationalGaloisQuotient.galoisChart_eq_of_isRadicial). The graph of the Galois action is the kernel pair of the projection of Spec ℚ̄ onto its quotient, so the two projections would be related by a morphism Spec(ℚ̄ ⊗_ℚ ℚ̄) ⟶ ∐_{g} Spec ℚ̄, which by quasi-compactness forces the absolute Galois group of ℚ to be finite (AlgebraicGeometry.RationalGaloisQuotient.finite_galoisGroup_of_rel); it is not (AlgebraicGeometry.RationalGaloisQuotient.infinite_galoisGroup).

theorem not_isRadicial_galoisQuotientBaseChangeToCover :
    ¬ Space.IsRadicial B base hS (isAlgebraicSpace_galoisQuotientBaseChange B hS hU)
      (isAlgebraicSpace_yoneda B base hS _) (galoisQuotientBaseChangeToCover B hS hU)

AlgebraicGeometry.Space.IsWeaklyRadicial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 629. The attribute's comment: “the definition of a weakly radicial morphism”.

Stacks 049E. A morphism of algebraic spaces over S is weakly radicial if for every field K in the chosen site and every K-valued point of the target, the point set of the fibre is a singleton and the fibre admits, over Spec(K), a monomorphism from the spectrum of a purely inseparable extension of K.

def IsWeaklyRadicial (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.surjective_app_of_isWeaklyRadicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 703. The attribute's comment: “surjectivity on k-points for k algebraically closed”.

Stacks 049E. A weakly radicial morphism of algebraic spaces over S is surjective on k-valued points for every algebraically closed field k in the chosen site.

The fibre over a k-valued point of the target receives a monomorphism from the spectrum of a purely inseparable extension of k, and such an extension of an algebraically closed field is trivial; the induced morphism of field spectra is therefore an isomorphism, and inverting it produces a section of the fibre's projection, hence a k-valued point of the source over the given one.

theorem surjective_app_of_isWeaklyRadicial
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsWeaklyRadicial B S hS hX hY f)
    (k : Type u) [Field k] [IsAlgClosed k] (hk : B.Contains (Spec (.of k)))
    (s : Spec (.of k) ⟶ S) :
    Function.Surjective (f.app (Opposite.op
      (Over.mk (⟨s⟩ : B.obj hk ⟶ B.obj hS) : BigFppfOver B S hS)))

AlgebraicGeometry.Space.isWeaklyRadicial_of_universallyInjective_of_hasPropertyBeta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 762. The attribute's comment: “analogue of 0484: (β) + universally injective + surjective ⇒ weakly radicial”.

Stacks 049E, the analogue of Stacks 0484. A surjective, universally injective morphism of algebraic spaces over S with property (β) is weakly radicial.

The source states this without the surjectivity hypothesis, and in that form it is false: a weakly radicial morphism is surjective (AlgebraicGeometry.Space.isSurjective_of_isWeaklyRadicial), while the inclusion of the empty scheme is universally injective and has property (β), see AlgebraicGeometry.Space.exists_universallyInjective_hasPropertyBeta_not_isWeaklyRadicial.

Over a field-valued point Spec(K) ⟶ Y the fibre has a subsingleton point set by universal injectivity and a nonempty one by surjectivity. Property (β) at its unique point is condition (1) of Stacks 03JU, which is equivalent to condition (4): a monomorphism from the spectrum of a field L representing the point. The composite Spec(L) ⟶ Spec(K) is universally injective, a monomorphism being universally injective, so K ⊂ L is purely inseparable, exactly as in the proof of Stacks 0484.

theorem isWeaklyRadicial_of_universallyInjective_of_hasPropertyBeta
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hinj : UniversallyInjective B S hS f)
    (hbeta : HasPropertyBeta B S hS f)
    (hsurj : IsSurjective B S hS f) :
    IsWeaklyRadicial B S hS hX hY f

AlgebraicGeometry.Space.exists_universallyInjective_hasPropertyBeta_not_isWeaklyRadicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Radicial.lean, line 820. The attribute's comment: “the analogue of Lemma 0484 without surjectivity is false: a counterexample”.

Stacks 049E, the analogue of Stacks 0484 as stated is false. As soon as the site contains the spectrum of a field, there is a universally injective morphism of algebraic spaces with property (β) which is not weakly radicial: the inclusion into Spec(K) of the empty scheme. Its fibre over Spec(K) has no point, whereas a weakly radicial morphism has a one-point fibre over every field-valued point.

The corrected statement, with surjectivity added, is AlgebraicGeometry.Space.isWeaklyRadicial_of_universallyInjective_of_hasPropertyBeta.

theorem exists_universallyInjective_hasPropertyBeta_not_isWeaklyRadicial
    (K : Type u) [Field K] (hK : B.Contains (Spec (.of K))) (s : Spec (.of K) ⟶ S) :
    ∃ (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
      (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y),
      UniversallyInjective B S hS f ∧ HasPropertyBeta B S hS f ∧
        ¬ IsWeaklyRadicial B S hS hX hY f

Tag 0AGE, a lemma

Tag 0AGE in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_of_injective_pointsMap_pullback_of_isEtale_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjectiveEtaleCriterion.lean, line 449.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, and assume that for every étale morphism V ⟶ Y from a scheme V the map |X ×_Y V| → |V| is injective. Then f is universally injective.

theorem universallyInjective_of_injective_pointsMap_pullback_of_isEtale_yoneda
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hinj : ∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y), IsEtale B S hS g →
      Function.Injective (pointsMap B S hS (pullback g f) (pullback.fst g f))) :
    UniversallyInjective B S hS f

Sources

LeanAlgebraicGeometry.Space.IsRadicial · AlgebraicGeometry.Space.universallyInjective_of_isRadicial · AlgebraicGeometry.RationalGaloisQuotient.universallyInjective_galoisQuotientToBase · AlgebraicGeometry.RationalGaloisQuotient.not_isRadicial_galoisQuotientToBase · AlgebraicGeometry.RationalGaloisQuotient.universallyInjective_and_not_isRadicial · AlgebraicGeometry.RationalGaloisQuotient.exists_universallyInjective_not_isRadicial · AlgebraicGeometry.Space.isRadicial_of_universallyInjective_of_isDecent · AlgebraicGeometry.Space.isRadicial_of_universallyInjective_of_isQuasiSeparated

Section76.4 Monomorphisms #

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

Tag 0B8A, a lemma

Tag 0B8A in the Stacks Project.

AlgebraicGeometry.Space.relativelyRepresentable_of_isFlat_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatMonomorphismRepresentable.lean, line 712.

Stacks 0B8A (David Rydh). A flat monomorphism of algebraic spaces is representable by schemes.

theorem relativelyRepresentable_of_isFlat_of_mono {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) [Mono f]
    (hf : IsFlat B S hS f) : yoneda.relativelyRepresentable f

Tag 0B8B, a lemma

Tag 0B8B in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_mono_of_forall_baseChange_mono_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MonomorphismInjectiveStructureMap.lean, line 699.

Stacks 0B8B. A quasi-compact monomorphism of algebraic spaces over S whose structure homomorphism 𝒪_T ⟶ f_{T,*}𝒪_{X ×_Y T} is a monomorphism for every T ⟶ Y is an isomorphism.

public theorem isIso_of_mono_of_forall_baseChange_mono_fSharp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hqc : Space.IsQuasiCompact B S hS f.hom) [Mono f]
    (hinj : ∀ (T : AlgebraicSpaces B S hS) (g : T ⟶ Y),
      Mono (Space.smallEtaleRingedToposHom B S hS
        (ObjectProperty.homMk (pullback.fst g.hom f.hom) :
          AlgebraicSpaces.fiberProduct B S hS g f ⟶ T)).fSharp) :
    IsIso f

Tag 0B8C, a lemma

Tag 0B8C in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_mono_of_isQuasiCompact_of_isFlat_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatSurjectiveMonomorphism.lean, line 138.

Stacks 0B8C. A quasi-compact, flat and surjective monomorphism of algebraic spaces over S is an isomorphism.

theorem isIso_of_mono_of_isQuasiCompact_of_isFlat_of_isSurjective
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) [Mono f]
    (hqc : IsQuasiCompact B S hS f.hom) (hflat : IsFlat B S hS f.hom)
    (hsurj : IsSurjective B S hS f.hom) :
    IsIso f

Sources

LeanAlgebraicGeometry.Space.relativelyRepresentable_of_isFlat_of_mono · AlgebraicGeometry.Space.isIso_of_mono_of_forall_baseChange_mono_fSharp · AlgebraicGeometry.Space.isIso_of_mono_of_isQuasiCompact_of_isFlat_of_isSurjective

Section76.5 Conormal sheaf of an immersion #

Section 76.5 of the Stacks Project, Tag 04CM. 6 tags here are carried by 36 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04CN, a definition

Tag 04CN in the Stacks Project.

AlgebraicGeometry.Space.conormalModuleOfImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebra.lean, line 410. The attribute's comment: “construction as the pullback of the ideal sheaf, via the closed factorisation”.

Stacks 04CN for an immersion. The conormal module 𝒞_{Z/X} of an immersion i : Z ⟶ X of algebraic spaces: the inverse image along the closed factorisation Z ⟶ X ∖ ∂Z of the defining ideal sheaf of the image of that factorisation.

Stacks 76.5 defines the conormal sheaf of an immersion to be the conormal sheaf of the closed immersion i : Z ⟶ X ∖ ∂Z of Stacks 04CE, which is what this is. Unlike AlgebraicGeometry.Space.conormalModule, which returns a module on the closed subspace's own functor, this is a module on Z itself, as the source asks; the two are related by AlgebraicGeometry.Space.conormalModuleOfImmersion_eq_conormalAlgebraOfImmersion_piece_one below, which identifies this module with the degree-one piece of the conormal algebra AlgebraicGeometry.Space.conormalAlgebraOfImmersion.

The source describes the module as 𝓘/𝓘², which is i_*i^*𝓘; the module documentation of StacksFrontier.AlgebraicGeometry.Spaces.ConormalModule records why i^*𝓘 is that module and that the identification is not formalized, and the "What is not proved" section of this file records that quasi-coherence is not established either.

noncomputable def conormalModuleOfImmersion (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    Modules.{u, u} B S hS Z₀ hZ

AlgebraicGeometry.Space.conormalModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModule.lean, line 192. The attribute's comment: “construction as the pullback of the ideal sheaf, closed immersion”. References: SGA 6 0 (2.1), “more general”.

Stacks 04CN for a closed immersion. The conormal module 𝒞_{Z/X} of a closed subspace Z of an algebraic space X: the inverse image along the inclusion i : Z ⟶ X of the defining ideal sheaf 𝓘_Z ⊆ 𝒪_X of Stacks 03MB.

Stacks 76.5 describes this 𝒪_Z-module as 𝓘/𝓘², which is i_*i^*𝓘; the implementation notes of this file record why i^*𝓘 is that module and that the identification is not formalized here, and that this is the convention of the scheme-level Stacks.Conormal.conormalSheaf.

noncomputable def conormalModule (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) :
    Modules.{u, u} B S hS Z.1.toFunctor Z.2.1

AlgebraicGeometry.Space.conormalIdealQuotientIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersion.lean, line 518. The attribute's comment: “the identification of the conormal module with 𝓘/𝓘², for a closed immersion”.

Stacks 04CN, the identification with 𝓘/𝓘². For a closed immersion i : Z ⟶ X of algebraic spaces the canonical map induced by the unit of i^* ⊣ i_* is an isomorphism

𝓘/𝓘² ≅ i_*𝒞_{Z/X},

so the 𝒪_Z-module 𝒞_{Z/X} = i^*𝓘 of AlgebraicGeometry.Space.conormalModuleOfHom is the one Stacks 76.5 describes as 𝓘/𝓘². The characterising property is AlgebraicGeometry.Space.conormalIdealQuotientπ_comp_toPushforward: composed with the projection 𝓘 ⟶ 𝓘/𝓘² it is the unit.

def conormalIdealQuotientIso (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom) :
    conormalIdealQuotient B S hS i ≅
      (modulePushforward B S hS i).obj (conormalModuleOfHom B S hS i)

AlgebraicGeometry.Space.isQuasicoherentOnSite_conormalModuleOfImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersion.lean, line 569. The attribute's comment: “the conormal sheaf is a quasi-coherent module”.

The quasi-coherence clause of Stacks 04CN for an arbitrary immersion, unconditionally: the closed factorisation of Stacks 04CE is a closed immersion, where AlgebraicGeometry.Space.isQuasicoherentOnSite_conormalModuleOfHom applies.

The definition of the source calls 𝒞_{Z/X} the quasi-coherent 𝒪_Z-module 𝓘/𝓘²; this is that clause of the definition, which AlgebraicGeometry.Space.conormalModuleOfImmersion — being a definition — cannot itself state.

theorem isQuasicoherentOnSite_conormalModuleOfImmersion (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    (conormalModuleOfImmersion B S hS hX hZ i hi).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_and_nonempty_conormalIdealQuotientIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersion.lean, line 599.

Stacks Project, Tag 04CN. The conormal sheaf 𝒞_{Z/X} of an immersion i : Z ⟶ X of algebraic spaces over S, constructed as AlgebraicGeometry.Space.conormalModuleOfImmersion through the closed immersion of Z into the complement X ∖ ∂Z of the boundary of its image (Stacks 04CE), is the quasi-coherent 𝒪_Z-module 𝓘/𝓘² of the source: it is quasi-coherent, and for 𝓘 the ideal sheaf of Z in X ∖ ∂Z its direct image along that closed immersion is 𝓘/𝓘².

theorem isQuasicoherentOnSite_and_nonempty_conormalIdealQuotientIso
    (hX : IsAlgebraicSpace B S hS X₀) (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀)
    (hi : IsImmersion B S hS i) :
    (conormalModuleOfImmersion B S hS hX hZ i hi).IsQuasicoherentOnSite ∧
      Nonempty (conormalIdealQuotient B S hS (immersionClosedFactorization B S hS hX hZ i hi) ≅
        (modulePushforward B S hS (immersionClosedFactorization B S hS hX hZ i hi)).obj
          (conormalModuleOfImmersion B S hS hX hZ i hi))

Tag 04CO, a lemma

Tag 04CO in the Stacks Project.

AlgebraicGeometry.Space.conormalModuleEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleEtaleRestriction.lean, line 954. The attribute's comment: “the conormal module commutes with etale base change”. References: SGA 3 I (6.8.5), “étale base change”.

Stacks 04CO for the conormal module. Let φ : U ⟶ X be an étale morphism of algebraic spaces and Z ⊆ X a closed subspace, with inverse image Z_U = U ×_X Z and projection p : Z_U ⟶ Z. Then the inverse image along p of the conormal module of Z in X is the conormal module of Z_U in U:

𝒞_{Z/X}|_{Z_U} = p^*𝒞_{Z/X} ≅ 𝒞_{Z_U/U}.

The isomorphism is the square comparison p^*i^* ≅ i_U^*φ^* of AlgebraicGeometry.Space.conormalPullbackCompIso, then the inverse image along i_U of the identification of φ^* with étale restriction of [Stacks Project, Tag 03LW], then the equality 𝓘_Z|_U = 𝓘_{Z_U} of defining ideal sheaves.

noncomputable def conormalModuleEtaleRestrictionIso (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (Z : ClosedSubspaces B S hS X.1) :
    (modulePullback B S hS
          (ObjectProperty.homMk (Z.1.fromPreimage φ.hom) :
            (⟨(Z.1.preimage φ.hom).toFunctor,
                (isClosedSubspace_preimage B S hS φ.hom Z.1 X.2 U.2 Z.2).1⟩ :
              AlgebraicSpaces B S hS) ⟶
            (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))).obj
        (conormalModule B S hS X Z) ≅
      conormalModule B S hS U (⟨Z.1.preimage φ.hom,
        isClosedSubspace_preimage B S hS φ.hom Z.1 X.2 U.2 Z.2⟩ :
        ClosedSubspaces B S hS U.1)

AlgebraicGeometry.Space.conormalModuleEtaleRestrictionCanonicalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleEtaleRestrictionCanonical.lean, line 189. The attribute's comment: “the identification, as the canonical map of 04CP, for an etale source”.

Stacks 04CO. Let Z ⊆ X be a closed subspace of an algebraic space over S, let g : X' ⟶ X be étale — written φ : U ⟶ X in the source — and let
Z_U --f--> Z
|          |
U  --g-->  X
be a cartesian square, so that Z_U = U ×_X Z is the inverse image of Z. Then the inverse image along f of the conormal module of Z in X is the conormal module of Z_U in U:

𝒞_{Z/X}|_{Z_U} = f^*𝒞_{Z/X} ≅ 𝒞_{Z_U/U}.

The identification is the canonical map of Stacks 04CP itself, which is invertible by AlgebraicGeometry.Space.isIso_conormalMap_of_isPullback_of_isEtale; it is therefore canonical by construction, and functorial in the étale source by AlgebraicGeometry.Space.conormalModuleEtaleRestrictionCanonicalIso_comp.

noncomputable def conormalModuleEtaleRestrictionCanonicalIso
    (Z : ClosedSubspaces B S hS X.1) (Z' : ClosedSubspaces B S hS X'.1) (g : X ⟶ X')
    (f : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z')
    (hcart : IsPullback Z.1.ι f.hom g.hom Z'.1.ι)
    (hg : IsEtale B S hS g.hom) :
    (modulePullback B S hS f).obj (conormalModule B S hS X' Z') ≅
      conormalModule B S hS X Z

AlgebraicGeometry.Space.conormalModuleEtaleRestrictionCanonicalIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleEtaleRestrictionCanonical.lean, line 239. The attribute's comment: “functoriality in the etale source U”.

Stacks 04CO, the functoriality in the étale source U. Let Z ⊆ X be a closed subspace, let g' : X' ⟶ X'' and g : X ⟶ X' be étale — written φ : U ⟶ X and ψ : V ⟶ U in the source — and let the two squares
Z   --f--> Z'  --f'--> Z''
|          |           |
X   --g--> X'  --g'--> X''
both be cartesian. Then the identification of Stacks 04CO for the composite g ≫ g' is the composition comparison of Stacks 03LU for f and f', followed by the inverse image along f of the identification for g', followed by the identification for g.

The étaleness of the composite and the cartesianness of the outer rectangle are derived from the hypotheses, so what is assumed is exactly what the tag assumes. The proof is the composition law for the canonical map, part (3) of Stacks 04G2 (AlgebraicGeometry.Space.conormalMap_comp), together with AlgebraicGeometry.Space.conormalModuleEtaleRestrictionCanonicalIso_hom: because the identification is the canonical map, its functoriality is that law and needs nothing further. In particular the composition law for the identification of Stacks 03LW is not needed, which is what blocks the functoriality of the separately built isomorphism of StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleEtaleRestriction.lean.

theorem conormalModuleEtaleRestrictionCanonicalIso_comp
    (Z : ClosedSubspaces B S hS X.1) (Z' : ClosedSubspaces B S hS X'.1)
    (Z'' : ClosedSubspaces B S hS X''.1) (g : X ⟶ X') (g' : X' ⟶ X'')
    (f : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (f' : (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z''.1.toFunctor, Z''.2.1⟩ : AlgebraicSpaces B S hS))
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z')
    (hsq' : subspaceInclusion B S hS X' Z' ≫ g' = f' ≫ subspaceInclusion B S hS X'' Z'')
    (hcart : IsPullback Z.1.ι f.hom g.hom Z'.1.ι)
    (hcart' : IsPullback Z'.1.ι f'.hom g'.hom Z''.1.ι)
    (hg : IsEtale B S hS g.hom) (hg' : IsEtale B S hS g'.hom) :
    (conormalModuleEtaleRestrictionCanonicalIso B S hS Z Z'' (g ≫ g') (f ≫ f')
          (by rw [← Category.assoc, hsq, Category.assoc, hsq', Category.assoc])
          ((hcart.flip.paste_horiz hcart'.flip).flip)
          (isEtale_comp B S hS hg hg')).hom =
      (modulePullbackCompIso B S hS f f').inv.app (conormalModule B S hS X'' Z'') ≫
        (modulePullback B S hS f).map
            (conormalModuleEtaleRestrictionCanonicalIso B S hS Z' Z'' g' f' hsq' hcart' hg').hom ≫
          (conormalModuleEtaleRestrictionCanonicalIso B S hS Z Z' g f hsq hcart hg).hom

AlgebraicGeometry.Space.isLocallyClosedSubspace_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersionEtaleRestriction.lean, line 168. The attribute's comment: “Z_U = U ×_X Z is a locally closed subspace of U”.

Stacks 04CO, the locally closed clause. The inverse image of a locally closed subspace of an algebraic space along a morphism of algebraic spaces over S is a locally closed subspace of the source.

For an étale f this is the clause of Stacks 04CO that Z_U = U ×_X Z is a locally closed subspace of U; no étaleness is needed, the inverse image being the fibre product by Stacks 083Q and immersions being stable under base change by Stacks 02YW.

theorem isLocallyClosedSubspace_preimage
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : Y ⟶ X) (Z : Subfunctor X)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsLocallyClosedSubspace B S hS Z) :
    IsLocallyClosedSubspace B S hS (Z.preimage f)

AlgebraicGeometry.Space.conormalModuleOfImmersionEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersionEtaleRestriction.lean, line 295. The attribute's comment: “the conormal module of an immersion commutes with etale localisation”.

Stacks 04CO. Let i : Z ⟶ X be an immersion of algebraic spaces over S, let φ : U ⟶ X be étale and let Z_U = U ×_X Z with projections p : Z_U ⟶ Z and i_U : Z_U ⟶ U. Then the inverse image along p of the conormal module of Z in X is the conormal module of Z_U in U:

𝒞_{Z/X}|_{Z_U} = p^*𝒞_{Z/X} ≅ 𝒞_{Z_U/U}.

Both conormal modules are taken through the closed factorisation of Stacks 04CE, as AlgebraicGeometry.Space.immersionConormalModule; i_U is an immersion because immersions are stable under base change. The isomorphism is the degree-one instance of the conormal-algebra isomorphism of Stacks 09RR, conjugated by the bridge AlgebraicGeometry.Space.conormalAlgebraOfImmersionPieceIso at i and at i_U.

noncomputable def conormalModuleOfImmersionEtaleRestrictionIso (p : ZU ⟶ Z) (iU : ZU ⟶ U)
    (i : Z ⟶ X) (φ : U ⟶ X) (sq : IsPullback p iU i φ) (hi : IsImmersion B S hS i.hom)
    (hφ : IsEtale B S hS φ.hom) :
    (modulePullback B S hS p).obj (immersionConormalModule B S hS i hi) ≅
      immersionConormalModule B S hS iU (isImmersion_of_isPullback B S hS sq hi)

AlgebraicGeometry.Space.conormalModuleSubspaceEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersionEtaleRestriction.lean, line 334. The attribute's comment: “the conormal module of a locally closed subspace commutes with etale localisation”.

Stacks 04CO in the shape the source states it. Let Z be a locally closed subspace of an algebraic space X over S, let φ : U ⟶ X be étale and let Z_U = U ×_X Z be the inverse image of Z, a locally closed subspace of U by AlgebraicGeometry.Space.isLocallyClosedSubspace_preimage. Then the inverse image along the projection p : Z_U ⟶ Z of the conormal module of Z in X is the conormal module of Z_U in U.

This is AlgebraicGeometry.Space.conormalModuleOfImmersionEtaleRestrictionIso at the cartesian square of Stacks 083Q, the inverse image being the fibre product by CategoryTheory.Subfunctor.isPullback_preimage.

noncomputable def conormalModuleSubspaceEtaleRestrictionIso (φ : U ⟶ X)
    (hφ : IsEtale B S hS φ.hom) (Z : Subfunctor X.1)
    (hZ : IsLocallyClosedSubspace B S hS Z) :
    (modulePullback B S hS (ObjectProperty.homMk (Z.fromPreimage φ.hom) :
          (⟨(Z.preimage φ.hom).toFunctor,
              (isLocallyClosedSubspace_preimage B S hS φ.hom Z X.2 U.2 hZ).1⟩ :
            AlgebraicSpaces B S hS) ⟶
          (⟨Z.toFunctor, hZ.1⟩ : AlgebraicSpaces B S hS))).obj
        (immersionConormalModule B S hS
          (ObjectProperty.homMk Z.ι : (⟨Z.toFunctor, hZ.1⟩ : AlgebraicSpaces B S hS) ⟶ X)
          hZ.2) ≅
      immersionConormalModule B S hS
        (ObjectProperty.homMk (Z.preimage φ.hom).ι :
          (⟨(Z.preimage φ.hom).toFunctor,
              (isLocallyClosedSubspace_preimage B S hS φ.hom Z X.2 U.2 hZ).1⟩ :
            AlgebraicSpaces B S hS) ⟶ U)
        (isLocallyClosedSubspace_preimage B S hS φ.hom Z X.2 U.2 hZ).2

AlgebraicGeometry.Space.conormalModuleSchemeEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleSchemeEtaleRestriction.lean, line 208.

Stacks 04CO. Let i : Z ⟶ X be an immersion of algebraic spaces over S, let U be a scheme of the site and φ : U ⟶ X étale. Then

the fibre product Z_U = U ×_X Z is a scheme R of the site, and for every presentation of it by a cartesian square with j : R ⟶ U and p : Z_U ⟶ Z:

j is an immersion of schemes, so Z_U is a locally closed subscheme of U;

the canonical map 𝒞_{Z/X}|_{Z_U} = p^*𝒞_{Z/X} ⟶ 𝒞_{Z_U/U} — the canonical map of [Stacks Project, Tag 04CP] of the square followed by part (1) of [Stacks Project, Tag 04G2], whose target is the conormal sheaf Stacks.Conormal.conormalSheaf of the immersion of schemes j of Morphisms, Definition [Stacks Project, Tag 01R2] read on the small étale site — is an isomorphism;

this identification is functorial in U: for a morphism ψ : U' ⟶ U of schemes over X with induced b : Z_{U'} ⟶ Z_U, the identification for U' is the restriction along b of the identification for U followed by the canonical map of Morphisms, Lemma [Stacks Project, Tag 01R4] of the schemes.

theorem conormalModuleSchemeEtaleRestriction (i : Z ⟶ X) (hi : IsImmersion B S hS i.hom)
    (φ : (⟨yoneda.obj V, isAlgebraicSpace_yoneda B S hS V⟩ : AlgebraicSpaces B S hS) ⟶ X)
    (hφ : IsEtale B S hS φ.hom) :
    (∃ (R : BigFppfOver B S hS) (j : R ⟶ V)
      (p : (⟨yoneda.obj R, isAlgebraicSpace_yoneda B S hS R⟩ : AlgebraicSpaces B S hS) ⟶ Z),
      IsPullback p (representedSpaceMap B S hS j) i φ) ∧
    ∀ {R : BigFppfOver B S hS} (j : R ⟶ V)
      (p : (⟨yoneda.obj R, isAlgebraicSpace_yoneda B S hS R⟩ : AlgebraicSpaces B S hS) ⟶ Z)
      (sq : IsPullback p (representedSpaceMap B S hS j) i φ),
      AlgebraicGeometry.IsImmersion ((BigFppfOver.toScheme B S hS).map j) ∧
      (haveI := isImmersion_toScheme_of_isPullback B S hS sq hi
      IsIso (conormalMapOfImmersions B S hS (representedSpaceMap B S hS j) i
        p φ
        (isImmersion_representedSpaceMap B S hS j) hi sq.w.symm ≫
        (conormalModuleOfImmersionRepresentedIso B S hS j).hom)) ∧
      ∀ {R' V' : BigFppfOver B S hS} (ψ : V' ⟶ V) (j' : R' ⟶ V') (b : R' ⟶ R)
        (hb : j' ≫ ψ = b ≫ j)
        (sq' : IsPullback (representedSpaceMap B S hS b ≫ p) (representedSpaceMap B S hS j') i
          (representedSpaceMap B S hS ψ ≫ φ)),
        haveI := isImmersion_toScheme_of_isPullback B S hS sq hi
        haveI := isImmersion_toScheme_of_isPullback B S hS sq' hi
        conormalMapOfImmersions B S hS (representedSpaceMap B S hS j') i
            (representedSpaceMap B S hS b ≫ p) (representedSpaceMap B S hS ψ ≫ φ)
            (isImmersion_representedSpaceMap B S hS j') hi sq'.w.symm ≫
          (conormalModuleOfImmersionRepresentedIso B S hS j').hom =
          (modulePullbackCompIso B S hS (representedSpaceMap B S hS b) p).inv.app
              (immersionConormalModule B S hS i hi) ≫
            (modulePullback B S hS (representedSpaceMap B S hS b)).map
              (conormalMapOfImmersions B S hS (representedSpaceMap B S hS j) i
            p φ
            (isImmersion_representedSpaceMap B S hS j) hi sq.w.symm ≫
                (conormalModuleOfImmersionRepresentedIso B S hS j).hom) ≫
            (representedAssociatedModulePullbackIso B S hS b
                (relativelyRepresentable_yoneda_map B S hS b)
                (Stacks.Conormal.conormalSheaf ((BigFppfOver.toScheme B S hS).map j))).hom ≫
            (representedSmallEtaleModuleEquivalence B S hS R').functor.map
              ((_root_.AlgebraicGeometry.SmallEtale.associatedModule (associatedBigEtaleSite B)
                  ((BigFppfOver.toScheme B S hS).obj R') R'.left.property).map
                (Stacks.Immersion.immersionConormalSheafMap
                  ((BigFppfOver.toScheme B S hS).map j')
                  ((BigFppfOver.toScheme B S hS).map j)
                  ((BigFppfOver.toScheme B S hS).map b)
                  ((BigFppfOver.toScheme B S hS).map ψ)
                  (toShHom_square_of_comp_eq B S hS j' j b ψ hb)))

AlgebraicGeometry.Space.etaleIdealSheafRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleIdealSheafRestriction.lean, line 196. The attribute's comment: “the ideal sheaf of the inverse image is the restriction of the ideal sheaf”.

Stacks 04CO. The étale restriction of the defining ideal sheaf of a closed subspace Z ⊆ X along an étale φ : U ⟶ X is the defining ideal sheaf of the inverse image φ⁻¹(Z).

Over every étale chart of U the two sheaves have the same sections, by AlgebraicGeometry.Space.definingIdealAt_preimage_eq_definingIdealAt_postcomp, and this isomorphism is the identity on the underlying regular functions there.

noncomputable def etaleIdealSheafRestrictionIso (φ : U ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (Z : ClosedSubspaces B S hS X.1) :
    (etaleModulePullback.{u, u} B S hS φ hφ).obj
        (definingIdealSheaf B S hS X Z).toSheafOfModules ≅
      (definingIdealSheaf B S hS U (⟨Z.1.preimage φ.hom,
        isClosedSubspace_preimage B S hS φ.hom Z.1 X.2 U.2 Z.2⟩ :
        ClosedSubspaces B S hS U.1)).toSheafOfModules

AlgebraicGeometry.Space.conormalModuleEtaleRestrictionIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsConormalAction.lean, line 294. The attribute's comment: “functoriality in the étale source”.

The functoriality of Stacks 04CO in the étale source. For étale morphisms ψ : V ⟶ U and φ : U ⟶ X of algebraic spaces with étale composite and a closed subspace Z ⊆ X, the identification p^*𝒞_{Z/X} ≅ 𝒞_{Z_V/V} of [Stacks Project, Tag 04CO] taken in two steps — the comparison of the inverse images along the two projections of [Stacks Project, Tag 03LU], then the inverse image along q : ψ⁻¹(φ⁻¹Z) ⟶ φ⁻¹Z of the identification for φ, then the identification for ψ over φ⁻¹(Z) — is the identification for ψ ≫ φ taken in one step. This is the "functorially in U" of the source.

The route is the one of [Stacks Project, Tag 04CP]: both sides are read through AlgebraicGeometry.Space.conormalMap_eq_conormalModuleEtaleRestrictionIso_hom, which identifies the canonical map of that tag at an étale restriction square with the forward map constructed by [Stacks Project, Tag 04CO], and the clause becomes part (3) of [Stacks Project, Tag 04G2] at the two stacked étale restriction squares, in the form AlgebraicGeometry.Space.conormalMap_comp_of_spaces. The one-step identification for ψ ≫ φ is read at the iterated spelling ψ⁻¹(φ⁻¹Z) of the upper closed subspace and with the projection written as the composite q ≫ p, which costs nothing: an iota-crossing in a first-order argument position of AlgebraicGeometry.Space.conormalMap is free, so neither AlgebraicGeometry.Space.closedSubspacePreimage_comp nor AlgebraicGeometry.Space.subspaceProjection_comp has to be rewritten.

The two-step composite is written out here rather than quoted as AlgebraicGeometry.Space.conormalEtaleRestrictionTwoStep; the implementation notes of this file record why, and that the difference is one of spelling and not of content.

theorem conormalModuleEtaleRestrictionIso_hom_comp (ψ : V ⟶ U) (φ : U ⟶ X)
    (hψ : IsEtale C S hS ψ.hom) (hφ : IsEtale C S hS φ.hom)
    (hψφ : IsEtale C S hS (ψ ≫ φ).hom) (Z : ClosedSubspaces C S hS X.1) :
    (modulePullbackCompIso C S hS
          (ObjectProperty.homMk ((Z.1.preimage φ.hom).fromPreimage ψ.hom) :
        (⟨((Z.1.preimage φ.hom).preimage ψ.hom).toFunctor,
          (isClosedSubspace_preimage C S hS ψ.hom (Z.1.preimage φ.hom) U.2 V.2
            (isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2)).1⟩ :
        AlgebraicSpaces C S hS) ⟶
        (⟨(Z.1.preimage φ.hom).toFunctor,
          (isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2).1⟩ :
        AlgebraicSpaces C S hS))
          (ObjectProperty.homMk (Z.1.fromPreimage φ.hom) :
        (⟨(Z.1.preimage φ.hom).toFunctor,
          (isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2).1⟩ :
        AlgebraicSpaces C S hS) ⟶
        (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces C S hS))).inv.app (conormalModule C S hS X Z) ≫
        (modulePullback C S hS
            (ObjectProperty.homMk ((Z.1.preimage φ.hom).fromPreimage ψ.hom) :
        (⟨((Z.1.preimage φ.hom).preimage ψ.hom).toFunctor,
          (isClosedSubspace_preimage C S hS ψ.hom (Z.1.preimage φ.hom) U.2 V.2
            (isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2)).1⟩ :
        AlgebraicSpaces C S hS) ⟶
        (⟨(Z.1.preimage φ.hom).toFunctor,
          (isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2).1⟩ :
        AlgebraicSpaces C S hS))).map
          (conormalModuleEtaleRestrictionIso C S hS φ hφ Z).hom ≫
          (conormalModuleEtaleRestrictionIso C S hS ψ hψ
            (⟨Z.1.preimage φ.hom,
          isClosedSubspace_preimage C S hS φ.hom Z.1 X.2 U.2 Z.2⟩ :
          ClosedSubspaces C S hS U.1)).hom =
      (conormalModuleEtaleRestrictionIso C S hS (ψ ≫ φ) hψφ Z).hom

Tag 04CP, a lemma

Tag 04CP in the Stacks Project.

AlgebraicGeometry.Space.conormalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFunctorial.lean, line 283. The attribute's comment: “the canonical map, for closed immersions”.

Stacks 04CP for closed immersions. The canonical map of 𝒪_Z-modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} attached to a commutative square of algebraic spaces in which Z is a closed subspace of X and Z' a closed subspace of X': the inverse image along the inclusion of Z of AlgebraicGeometry.Space.idealSheafMap, read through the identification f^*(i')^* ≅ i^*g^* of AlgebraicGeometry.Space.conormalPullbackCompIso.

The source states the lemma for immersions and reduces it to closed immersions at the start of its proof; the lemma for arbitrary immersions is AlgebraicGeometry.Space.conormalMapOfImmersions, and the implementation notes of this file say why the closed case is the one carried here.

noncomputable def conormalMap
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z') :
    (modulePullback B S hS f).obj (conormalModule B S hS X' Z') ⟶
      conormalModule B S hS X Z

AlgebraicGeometry.Space.conormalMapOfImmersions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleImmersionFunctorial.lean, line 601. The attribute's comment: “the canonical map, for arbitrary immersions”.

Stacks 04CP. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a commutative square of algebraic spaces over S in which i and i' are immersions. Then there is a canonical map of 𝒪_Z-modules

f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X}

between the conormal modules of the two immersions.

The conormal modules are AlgebraicGeometry.Space.immersionConormalModule, the conormal modules taken through the canonical closed factorisation of Stacks 04CE, which is how the source's reduction of an immersion to a closed immersion into an open subspace is carried. The map is the degree-one canonical map AlgebraicGeometry.Space.conormalAlgebraSquarePieceMap of the square, conjugated by the bridge AlgebraicGeometry.Space.conormalAlgebraOfImmersionPieceIso at i' and at i; the module documentation of this file explains why that construction needs no choice of ambient open subspaces and no hypothesis beyond the commutativity of the square.

noncomputable def conormalMapOfImmersions (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    (hi : IsImmersion B S hS i.hom) (hi' : IsImmersion B S hS i'.hom)
    (hsq : i ≫ g = f ≫ i') :
    (modulePullback B S hS f).obj (immersionConormalModule B S hS i' hi') ⟶
      immersionConormalModule B S hS i hi

Tag 04G2, a lemma

Tag 04G2 in the Stacks Project.

Stacks.Immersion.immersionConormalSheafMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/SquareMap.lean, line 454. The attribute's comment: “part (3) for schemes”.

[Stacks Project, Tag 01R4] is functorial for stacked squares. For two commutative squares of immersions stacked vertically, the induced map of conormal sheaves of the composite square is the composite of the two induced maps, read through the pullback composition isomorphism RingedSpaceModuleAdjunction.modulePullbackComp.

The source states no such law; it is what makes the map of the tag a map of pseudofunctors, and it is what transports the map along a restriction of the ambient scheme.

The proof is Stacks.Immersion.immersionConormalSheafMap_unique: the composite is shown to satisfy the affine characterisation of the composite square. A pair of affine opens U ⊆ X₁ and P ⊆ X₃ need not factor through an affine open of X₂, so the characterisation is verified after restricting to the affine opens U₀ ⊆ U that do, by Stacks.Immersion.transpose_comp_eq_of_affineModel and Stacks.Tag01R3PartTwo.affineConormalIsoCotangent_restrict; those cover i₁⁻¹U, since the square carries a point of it into the coborder of the range of i₂.

theorem immersionConormalSheafMap_comp {Z₁ Z₂ Z₃ X₁ X₂ X₃ : Scheme.{u}}
    (i₁ : Z₁ ⟶ X₁) (i₂ : Z₂ ⟶ X₂) (i₃ : Z₃ ⟶ X₃)
    [IsImmersion i₁] [IsImmersion i₂] [IsImmersion i₃]
    (f₁ : Z₁ ⟶ Z₂) (g₁ : X₁ ⟶ X₂) (comm₁ : i₁ ≫ g₁ = f₁ ≫ i₂)
    (f₂ : Z₂ ⟶ Z₃) (g₂ : X₂ ⟶ X₃) (comm₂ : i₂ ≫ g₂ = f₂ ≫ i₃) :
    immersionConormalSheafMap i₁ i₃ (f₁ ≫ f₂) (g₁ ≫ g₂)
        (toShHom_square (square_comp comm₁ comm₂)) =
      (modulePullbackComp f₁.toLRSHom.toShHom f₂.toLRSHom.toShHom).hom.app
          (conormalSheaf i₃.liftCoborder.toLRSHom.toShHom) ≫
        (modulePullback f₁.toLRSHom.toShHom).map
          (immersionConormalSheafMap i₂ i₃ f₂ g₂ (toShHom_square comm₂)) ≫
        immersionConormalSheafMap i₁ i₂ f₁ g₁ (toShHom_square comm₁)

AlgebraicGeometry.Space.conormalModuleOfImmersionRepresentedIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalLeadingIdentityStack.lean, line 657. The attribute's comment: “part (2): for a commutative square of the big fppf site whose two horizontal morphisms are immersions of schemes, the comparison of part (1) carries the canonical map of conormal modules of 04CP to the associated module of the canonical map of Morphisms, Lemma 01R4”.

Part (2) of [Stacks Project, Tag 04G2] at immersion generality.

For a commutative square of the big fppf category over S whose horizontal morphisms are immersions of schemes — the generality at which [Stacks Project, Tag 04CP] states its hypothesis, and so the generality of the clause — the comparison of part (1) (AlgebraicGeometry.Space.conormalModuleOfImmersionRepresentedIso) carries the canonical map of conormal modules of [Stacks Project, Tag 04CP] to the associated module of Stacks.Immersion.immersionConormalSheafMap, the canonical map of Morphisms, Lemma [Stacks Project, Tag 01R4].

AlgebraicGeometry.Space.conormalMapOfImmersions_conormalModuleOfImmersionRepresentedIso with its hypothesis hnat supplied by AlgebraicGeometry.Space.conormalMapOfImmersions_naturality_of_immersions.

theorem conormalModuleOfImmersionRepresentedIso_naturality (hsq : j ≫ a = b ≫ j') :
    conormalMapOfImmersions B S hS (representedSpaceMap B S hS j)
          (representedSpaceMap B S hS j') (representedSpaceMap B S hS b)
          (representedSpaceMap B S hS a) (isImmersion_representedSpaceMap B S hS j)
          (isImmersion_representedSpaceMap B S hS j')
          (representedSpaceMap_square_of_comp_eq B S hS j j' b a hsq) ≫
        (conormalModuleOfImmersionRepresentedIso B S hS j).hom =
      (modulePullback B S hS (representedSpaceMap B S hS b)).map
          (conormalModuleOfImmersionRepresentedIso B S hS j').hom ≫
        (representedAssociatedModulePullbackIso B S hS b
              (relativelyRepresentable_yoneda_map B S hS b)
              (Stacks.Conormal.conormalSheaf
                ((BigFppfOver.toScheme B S hS).map j'))).hom ≫
          (representedSmallEtaleModuleEquivalence B S hS R).functor.map
            ((_root_.AlgebraicGeometry.SmallEtale.associatedModule (associatedBigEtaleSite B)
                ((BigFppfOver.toScheme B S hS).obj R) R.left.property).map
              (Stacks.Immersion.immersionConormalSheafMap
                ((BigFppfOver.toScheme B S hS).map j)
                ((BigFppfOver.toScheme B S hS).map j')
                ((BigFppfOver.toScheme B S hS).map b)
                ((BigFppfOver.toScheme B S hS).map a)
                (toShHom_square_of_comp_eq B S hS j j' b a hsq)))

AlgebraicGeometry.Space.isIso_comp_conormalMap_of_isIso_conormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleComposition.lean, line 574. The attribute's comment: “invertibility of the conormal map of a composite, on the small étale site of an algebraic space”.

Invertibility of the conormal map of a composite descends to the two factors, part (3) of [Stacks Project, Tag 04G2] in the form invertibility consumes. If the conormal map of the outer rectangle is an isomorphism then so is the inverse image along f of the conormal map of the lower square followed by the conormal map of the upper square.

Both composites have the inverse image along the inclusion of Z of the two maps of defining ideal sheaves of [Stacks Project, Tag 04CP] as a right factor, and in both the left factor is a composite of comparison isomorphisms; so the hypothesis makes that common right factor invertible, and with it the second composite.

theorem isIso_comp_conormalMap_of_isIso_conormalMap
    (hiso : IsIso (conormalMap B S hS Z Z'' (g ≫ g') (f ≫ f') hsq'')) :
    IsIso ((modulePullback B S hS f).map (conormalMap B S hS Z' Z'' g' f' hsq') ≫
      conormalMap B S hS Z Z' g f hsq)

AlgebraicGeometry.Space.conormalMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleComposition.lean, line 641. The attribute's comment: “part (3), for closed subspaces of algebraic spaces”.

The composition formula for conormal maps, part (3) of [Stacks Project, Tag 04G2], for closed subspaces of algebraic spaces. For two vertically composable commutative squares of closed subspaces, the conormal map (f ≫ f')^*𝒞_{Z''/X''} ⟶ 𝒞_{Z/X} of the outer rectangle is the inverse image along f of the conormal map of the lower square followed by the conormal map of the upper square, read through the composition comparison AlgebraicGeometry.Space.modulePullbackCompIso of [Stacks Project, Tag 03LU].

Both sides have the inverse image along the inclusion of Z of the two maps of defining ideal sheaves as a right factor, by AlgebraicGeometry.Space.idealSheafMap_comp; the two left factors agree by the pasting AlgebraicGeometry.Space.conormalPullbackCompIso_paste_app of the comparisons of the two squares.

theorem conormalMap_comp :
    conormalMap B S hS Z Z'' (g ≫ g') (f ≫ f') hsq'' =
      (modulePullbackCompIso B S hS f f').inv.app (conormalModule B S hS X'' Z'') ≫
        (modulePullback B S hS f).map (conormalMap B S hS Z' Z'' g' f' hsq') ≫
          conormalMap B S hS Z Z' g f hsq

AlgebraicGeometry.Space.conormalMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleComposition.lean, line 641. The attribute's comment: “part (3): the composition law for the conormal map, on the small étale site of an algebraic space”.

The composition formula for conormal maps, part (3) of [Stacks Project, Tag 04G2], for closed subspaces of algebraic spaces. For two vertically composable commutative squares of closed subspaces, the conormal map (f ≫ f')^*𝒞_{Z''/X''} ⟶ 𝒞_{Z/X} of the outer rectangle is the inverse image along f of the conormal map of the lower square followed by the conormal map of the upper square, read through the composition comparison AlgebraicGeometry.Space.modulePullbackCompIso of [Stacks Project, Tag 03LU].

Both sides have the inverse image along the inclusion of Z of the two maps of defining ideal sheaves as a right factor, by AlgebraicGeometry.Space.idealSheafMap_comp; the two left factors agree by the pasting AlgebraicGeometry.Space.conormalPullbackCompIso_paste_app of the comparisons of the two squares.

theorem conormalMap_comp :
    conormalMap B S hS Z Z'' (g ≫ g') (f ≫ f') hsq'' =
      (modulePullbackCompIso B S hS f f').inv.app (conormalModule B S hS X'' Z'') ≫
        (modulePullback B S hS f).map (conormalMap B S hS Z' Z'' g' f' hsq') ≫
          conormalMap B S hS Z Z' g f hsq

AlgebraicGeometry.Space.conormalModuleClosedSubspaceRangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleSchemeAgreement.lean, line 427. The attribute's comment: “part (1): the conormal sheaf of a closed immersion of schemes of the site is the associated module of the conormal sheaf of Morphisms, Definition 01R2”.

Stacks 04G2, part (1). For a morphism j of the big fppf category over S whose underlying morphism of schemes is a closed immersion, the conormal module of [Stacks Project, Tag 04CN] of the closed subspace which j cuts out of yoneda.obj V — read on yoneda.obj R along the identification AlgebraicGeometry.Space.rangeSpaceIso of that subspace with it — is the module which the conormal sheaf of [Stacks Project, Tag 01R2] of the underlying morphism of schemes becomes on the small étale site.

This is the closed case. The clause at the immersion generality the source states it at is AlgebraicGeometry.Space.conormalModuleOfImmersionRepresentedIso, which is this comparison applied to the factorisation of the immersion through its ambient open.

noncomputable def conormalModuleClosedSubspaceRangeIso :
    (modulePullback B S hS (rangeSpaceIso B S hS j hj).hom).obj
        (conormalModule B S hS ⟨yoneda.obj V, isAlgebraicSpace_yoneda B S hS V⟩
          (closedSubspaceRange B S hS j hj)) ≅
      (representedSmallEtaleModuleEquivalence B S hS R).functor.obj
        ((_root_.AlgebraicGeometry.SmallEtale.associatedModule (associatedBigEtaleSite B)
            ((BigFppfOver.toScheme B S hS).obj R) R.left.property).obj
          (Stacks.Conormal.conormalSheaf ((BigFppfOver.toScheme B S hS).map j)))

AlgebraicGeometry.Space.conormalModuleOfImmersionRepresentedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleSchemeAgreementImmersion.lean, line 196. The attribute's comment: “part (1): for an immersion of schemes of the site, the conormal sheaf of 04CN of the represented morphism is the associated module of the conormal sheaf of Morphisms, Definition 01R2”.

Stacks 04G2, part (1). For a morphism j : R ⟶ V of the big fppf category over S whose underlying morphism of schemes is an immersion, the conormal module of [Stacks Project, Tag 04CN] of the morphism of algebraic spaces yoneda.obj R ⟶ yoneda.obj V which j represents is the module which the conormal sheaf of Morphisms, Definition [Stacks Project, Tag 01R2] of the underlying morphism of schemes becomes on the small étale site of yoneda.obj R.

No hypothesis beyond the immersion of the source is carried: the closed case is AlgebraicGeometry.Space.conormalModuleClosedSubspaceRangeIso, and this is that comparison applied over the ambient open of [Stacks Project, Tag 04CE], transported back to j by [Stacks Project, Tag 04CO].

def conormalModuleOfImmersionRepresentedIso (j : R ⟶ V)
    [AlgebraicGeometry.IsImmersion ((BigFppfOver.toScheme B S hS).map j)] :
    immersionConormalModule B S hS (representedSpaceMap B S hS j)
        (isImmersion_representedSpaceMap B S hS j) ≅
      (representedSmallEtaleModuleEquivalence B S hS R).functor.obj
        ((_root_.AlgebraicGeometry.SmallEtale.associatedModule (associatedBigEtaleSite B)
            ((BigFppfOver.toScheme B S hS).obj R) R.left.property).obj
          (Stacks.Conormal.conormalSheaf ((BigFppfOver.toScheme B S hS).map j)))

AlgebraicGeometry.Space.conormalMapOfImmersions_comp_of_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSquarePieceMapCompositionLaw.lean, line 359. The attribute's comment: “part (3): the composition law for the canonical map of 04CP, for arbitrary immersions of algebraic spaces”.

Stacks 04G2, part (3), at the generality the source states it. Let
Z₁ --i₁--→ X₁
|          |
f₁         g₁
↓          ↓
Z₂ --i₂--→ X₂
|          |
f₂         g₂
↓          ↓
Z₃ --i₃--→ X₃
be two commutative squares of algebraic spaces over S whose horizontal arrows are immersions, stacked vertically. Then the canonical map (f₁ ≫ f₂)^*𝒞_{Z₃/X₃} ⟶ 𝒞_{Z₁/X₁} of [Stacks Project, Tag 04CP] attached to the outer rectangle is the composition comparison of [Stacks Project, Tag 03LU] for f₁ and f₂, followed by the inverse image along f₁ of the map f₂^*𝒞_{Z₃/X₃} ⟶ 𝒞_{Z₂/X₂} of the lower square, followed by the map f₁^*𝒞_{Z₂/X₂} ⟶ 𝒞_{Z₁/X₁} of the upper square.

The hypotheses are exactly the source's: the three immersions and the two commutativities, the commutativity of the outer rectangle being derived by AlgebraicGeometry.Space.stackedSquare_comm. Nothing is assumed about closedness, quasi-compactness or quasi-coherence.

theorem conormalMapOfImmersions_comp_of_comm :
    conormalMapOfImmersions B S hS i₁ i₃ (f₁ ≫ f₂) (g₁ ≫ g₂) hi₁ hi₃
        (stackedSquare_comm B S hS i₁ i₂ i₃ f₁ g₁ f₂ g₂ hsq₁ hsq₂) =
      (modulePullbackCompIso B S hS f₁ f₂).inv.app
          (immersionConormalModule B S hS i₃ hi₃) ≫
        (modulePullback B S hS f₁).map
            (conormalMapOfImmersions B S hS i₂ i₃ f₂ g₂ hi₂ hi₃ hsq₂) ≫
          conormalMapOfImmersions B S hS i₁ i₂ f₁ g₁ hi₁ hi₂ hsq₁

Tag 04CQ, a lemma

Tag 04CQ in the Stacks Project.

AlgebraicGeometry.Space.epi_conormalMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeCartesian.lean, line 269. The attribute's comment: “surjectivity, at an arbitrary fibre product square”.

The surjectivity clause of [Stacks Project, Tag 04CQ]. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a fibre product square of algebraic spaces over S in which Z ⊆ X and Z' ⊆ X' are closed subspaces and i, i' are their inclusions. Then the canonical map of conormal modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] is an epimorphism of 𝒪_Z-modules.

This is AlgebraicGeometry.Space.epi_conormalMap released from the canonical inverse-image square: by AlgebraicGeometry.Space.closedSubspaces_eq_preimageSubspace_of_isPullback the cartesian hypothesis makes Z the inverse image g⁻¹(Z') and by AlgebraicGeometry.Space.vertical_eq_preimageProjection_of_isPullback it makes f the projection, after which the square's commutativity proof and the canonical one are proofs of the same proposition.

The horizontal arrows are closed immersions, where the source takes immersions; the implementation notes of this file record what the passage to the immersion case still needs.

theorem epi_conormalMap_of_isPullback
    (Z : ClosedSubspaces B S hS X.1) (Z' : ClosedSubspaces B S hS X'.1) (g : X ⟶ X')
    (f : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z')
    (hcart : IsPullback Z.1.ι f.hom g.hom Z'.1.ι) :
    Epi (conormalMap B S hS Z Z' g f hsq)

AlgebraicGeometry.Space.isIso_conormalMap_of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeCartesian.lean, line 289. The attribute's comment: “flat isomorphism, at an arbitrary fibre product square”.

The flat clause of [Stacks Project, Tag 04CQ]. For a fibre product square as in AgebraicGeometry.Space.epi_conormalMap_of_isPullback, if g is flat — that is, if the morphism of small étale ringed topoi it induces is flat in the sense of [Stacks Project, Tag 04JB] — then the canonical map of conormal modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] is an isomorphism.

This is AlgebraicGeometry.Space.isIso_conormalMap_of_isFlat released from the canonical inverse-image square, by the same two identifications.

theorem isIso_conormalMap_of_isPullback_of_isFlat
    (Z : ClosedSubspaces B S hS X.1) (Z' : ClosedSubspaces B S hS X'.1) (g : X ⟶ X')
    (f : (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z')
    (hcart : IsPullback Z.1.ι f.hom g.hom Z'.1.ι)
    (hg : (smallEtaleRingedToposHom B S hS g).IsFlat) :
    IsIso (conormalMap B S hS Z Z' g f hsq)

AlgebraicGeometry.Space.epi_conormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeEpi.lean, line 230. The attribute's comment: “surjectivity”.

The surjectivity clause of [Stacks Project, Tag 04CQ], for closed immersions. Let Z' be a closed subspace of an algebraic space X' and let g : X ⟶ X' be a morphism of algebraic spaces. For the fibre product square — the one whose upper closed subspace is the inverse image g⁻¹(Z') ⊆ X of [Stacks Project, Tag 083Q] and whose vertical morphism is the projection g⁻¹(Z') ⟶ Z' — the canonical map of conormal modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{g⁻¹(Z')/X} of [Stacks Project, Tag 04CP] is an epimorphism of 𝒪_{g⁻¹(Z')}-modules.

The source states the lemma for immersions and reduces it to closed immersions at the start of the proof of [Stacks Project, Tag 04CP]; the closed case is the one this development carries, for the reasons recorded in the implementation notes of StacksFrontier/AlgebraicGeometry/Spaces/ConormalModule.lean. The flat clause of the tag is not proved; see the "What is not proved" section of this file.

Surjectivity of a map of modules on the small étale site means that the map is an epimorphism, which by [Stacks Project, Tag 01AH] is local surjectivity; the chartwise statement behind it is AlgebraicGeometry.Space.surjective_idealSheafMap_val_app.

theorem epi_conormalMap (g : X ⟶ X') (Z' : ClosedSubspaces B S hS X'.1) :
    Epi (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.isIso_conormalMap_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeFlat.lean, line 783. The attribute's comment: “isomorphism when the morphism of small etale ringed topoi is flat”.

The flat clause of [Stacks Project, Tag 04CQ], for closed immersions. If g is flat — that is, if the morphism of small étale ringed topoi it induces is flat in the sense of [Stacks Project, Tag 04JB] — then the canonical map of conormal modules f^*𝒞_{Z'/X'} ⟶ 𝒞_{g⁻¹(Z')/X} of [Stacks Project, Tag 04CP] attached to the fibre product square is an isomorphism.

theorem isIso_conormalMap_of_isFlat (g : X ⟶ X') (Z' : ClosedSubspaces B S hS X'.1)
    (hg : (smallEtaleRingedToposHom B S hS g).IsFlat) :
    IsIso (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.epi_conormalMap_of_epi_idealSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFlatBaseChange.lean, line 111. The attribute's comment: “surjectivity, reduced to surjectivity of the map of defining ideal sheaves”.

The surjectivity clause of Stacks 04CQ, reduced to the map of defining ideal sheaves. If the map g^*𝓘' ⟶ 𝓘 of AlgebraicGeometry.Space.idealSheafMap attached to a commutative square of closed subspaces is surjective, then so is the map f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} of conormal modules of [Stacks Project, Tag 04CP].

AlgebraicGeometry.Space.conormalMap is the isomorphism AlgebraicGeometry.Space.conormalPullbackComparison followed by the inverse image along the inclusion of Z of the map of defining ideal sheaves. The inverse image of modules is a left adjoint, by the adjunction of [Stacks Project, Tag 03LU], and a left adjoint preserves epimorphisms.

Surjectivity of g^*𝓘' ⟶ 𝓘 is what [Stacks Project, Tag 04CQ] obtains from cartesianness of the square, by reduction to the scheme-level [Stacks Project, Tag 0473]; that reduction is not carried in this development, so the hypothesis is assumed. The invertibility clause reduces the same way, by AlgebraicGeometry.Space.isIso_conormalMap_of_isIso_idealSheafMap.

theorem epi_conormalMap_of_epi_idealSheafMap
    (hsq : subspaceInclusion B S hS X Z ≫ g = f ≫ subspaceInclusion B S hS X' Z')
    (h : Epi (idealSheafMap B S hS Z Z' g f hsq)) :
    Epi (conormalMap B S hS Z Z' g f hsq)

AlgebraicGeometry.Space.epi_conormalMapOfImmersions_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleOfImmersionBaseChange.lean, line 577. The attribute's comment: “surjectivity, for a fibre product square of immersions”.

The surjectivity clause of [Stacks Project, Tag 04CQ]. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a fibre product square of algebraic spaces over S in which i and i' are immersions. Then the canonical map f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] between the conormal modules of the two immersions is an epimorphism of 𝒪_Z-modules.

theorem epi_conormalMapOfImmersions_of_isPullback
    (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    (hi : IsImmersion B S hS i.hom) (hi' : IsImmersion B S hS i'.hom)
    (hcart : IsPullback i f g i') :
    Epi (conormalMapOfImmersions B S hS i i' f g hi hi' hcart.w)

AlgebraicGeometry.Space.isIso_conormalMapOfImmersions_of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleOfImmersionBaseChange.lean, line 606. The attribute's comment: “isomorphism when g is flat, for a fibre product square of immersions”.

The flat clause of [Stacks Project, Tag 04CQ]. For a fibre product square as in AlgebraicGeometry.Space.epi_conormalMapOfImmersions_of_isPullback, if g is flat as a morphism of algebraic spaces (Stacks 03ML), then the canonical map f^*𝒞_{Z'/X'} ⟶ 𝒞_{Z/X} of [Stacks Project, Tag 04CP] is an isomorphism.

theorem isIso_conormalMapOfImmersions_of_isPullback_of_isFlat
    (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    (hi : IsImmersion B S hS i.hom) (hi' : IsImmersion B S hS i'.hom)
    (hcart : IsPullback i f g i') (hg : IsFlat B S hS g.hom) :
    IsIso (conormalMapOfImmersions B S hS i i' f g hi hi' hcart.w)

Tag 06BD, a lemma

Tag 06BD in the Stacks Project.

AlgebraicGeometry.Space.epi_conormalMap_closedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeEpi.lean, line 255. The attribute's comment: “exactness at the right term”.

Exactness at the right term of [Stacks Project, Tag 06BD]. Let Y and Z be closed subspaces of an algebraic space X with Z ⊆ Y. The canonical map 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of [Stacks Project, Tag 04CP], the right-hand map of the conormal sequence of the pair, is an epimorphism.

This is the surjectivity clause of [Stacks Project, Tag 04CQ] at the fibre product square whose morphism of ambient spaces is the inclusion j : Y ⟶ X: the inverse image j⁻¹(Z) is Z read as a closed subspace of Y, and 𝒞_{Z/Y} is its conormal module there. The subspace of Y is taken as that inverse image rather than as Z itself because this development has no composition of closed subspaces, so no closed subspace of Y is attached to Z by any other route. The hypothesis Z ⊆ Y is what makes that inverse image the subspace the source calls Z, and it is carried for that reason alone: the proof is the instance of Stacks 04CQ, which holds for any pair, so the hypothesis is not used and its name is prefixed accordingly.

The exactness in the middle is not proved; see the "What is not proved" section of this file, which also names the composite-is-zero clause.

theorem epi_conormalMap_closedSubspaces (Y Z : ClosedSubspaces B S hS X.1)
    (_hZY : Z.1 ≤ Y.1) :
    Epi (conormalMap B S hS
      (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z) Z
      (subspaceInclusion B S hS X Y)
      (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)
      (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Y) Z))

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

The composite-is-zero clause of [Stacks Project, Tag 06BD]. Let Y and Z be closed subspaces of an algebraic space X with Z contained in Y through f : Z ⟶ Y. The composite of the two maps i^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} of the conormal sequence of the pair is zero, so that the sequence is a complex; together with AlgebraicGeometry.Space.epi_conormalMap_closedSubspaces this makes it a complex, exact at its right term.

Both maps are maps of [Stacks Project, Tag 04CP], the left one at the square of AlgebraicGeometry.Space.closedSubspacesConormal_square and the right one at the fibre product square of the inclusion j : Y ⟶ X. By part (3) of [Stacks Project, Tag 04G2] their composite is the conormal map of the outer rectangle, whose morphism of ambient spaces is j ≫ 𝟙 X = j; that factors through the inclusion of Y, so AlgebraicGeometry.Space.comp_conormalMap_eq_zero_of_factors applies.

Exactness in the middle is not proved; see the "What is not proved" section of StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleBaseChangeEpi.lean.

theorem conormalMap_comp_conormalMap_closedSubspaces_eq_zero
    (hf : f ≫ subspaceInclusion B S hS X Y = subspaceInclusion B S hS X Z) :
    (modulePullback B S hS
          (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)).map
        (conormalMap B S hS Z Y (𝟙 X : X ⟶ X) f
          (closedSubspacesConormal_square B S hS Y Z f hf)) ≫
      conormalMap B S hS
        (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z) Z
        (subspaceInclusion B S hS X Y)
        (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)
        (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Y) Z) = 0

AlgebraicGeometry.Space.conormalSequenceImmersion_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersion.lean, line 263. The attribute's comment: “the canonical exact sequence i^*C_{Y/X} → C_{Z/X} → C_{Z/Y} → 0 for immersions Z → Y → X of algebraic spaces, with the maps of Tag 04CP: the composite is zero, the sequence is exact at C_{Z/X}, and C_{Z/X} → C_{Z/Y} is an epimorphism”.

[Stacks Project, Tag 06BD]. Let i : Z ⟶ Y and j : Y ⟶ X be immersions of algebraic spaces over S. The canonical sequence of 𝒪_Z-modules

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

of the conormal modules of Stacks 04CN, with the maps of Stacks 04CP (AlgebraicGeometry.Space.conormalSequenceImmersionFirstMap and AlgebraicGeometry.Space.conormalSequenceImmersionSecondMap), is exact: the two maps compose to zero, the resulting short complex is exact, and the second map is an epimorphism.

It is isomorphic to the sequence i^*c^*Ker(c^♯) ⟶ (i ≫ c)^*Ker((i ≫ c)^♯) ⟶ i^*Ker(i^♯) ⟶ 0 of the closed factorisation c : Y ⟶ X ∖ ∂Y of j, which is exact by AlgebraicGeometry.Space.kernelConormalSequenceShortComplex_exact.

theorem conormalSequenceImmersion_exact :
    ∃ h : conormalSequenceImmersionFirstMap B S hS hX hY hZ i j hi hj ≫
        conormalSequenceImmersionSecondMap B S hS hX hY hZ i j hi hj = 0,
      (ShortComplex.mk _ _ h).Exact ∧
        Epi (conormalSequenceImmersionSecondMap B S hS hX hY hZ i j hi hj)

AlgebraicGeometry.Space.conormalMap_comp_conormalMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealSheafMapVanishing.lean, line 214. The attribute's comment: “the vanishing of the composite of the two maps of the sequence”.

The vanishing of the composite in Stacks 06BD. Let Y and Z be closed subspaces of an algebraic space X with Z ⊆ Y, let j : Y ⟶ X be the inclusion and let p : j⁻¹(Z) ⟶ Z be the projection. The two arrows of the conormal sequence of the pair,

p^*(i^*𝒞_{Y/X}) ⟶ p^*𝒞_{Z/X} ⟶ 𝒞_{j⁻¹(Z)/Y},

compose to zero. The first is the inverse image along p of the map of [Stacks Project, Tag 04CP] at the square of AlgebraicGeometry.Space.subspaceInclusion_homOfLe_square, the second is the map of [Stacks Project, Tag 04CP] at the inverse-image square, whose surjectivity is AlgebraicGeometry.Space.epi_conormalMap_closedSubspaces.

By the composition law of part (3) of [Stacks Project, Tag 04G2], AlgebraicGeometry.Space.conormalMap_comp, the composite is the map of [Stacks Project, Tag 04CP] attached to the outer rectangle, read through the composition comparison of [Stacks Project, Tag 03LU], which is an isomorphism. The lower edge of that rectangle is j ≫ 𝟙 X = j, which factors through Y by the identity of Y, so the map of the outer rectangle vanishes by AlgebraicGeometry.Space.conormalMap_eq_zero_of_factorization.

theorem conormalMap_comp_conormalMap_eq_zero {X : AlgebraicSpaces B S hS}
    (Y Z : ClosedSubspaces B S hS X.1) (hZY : Z.1 ≤ Y.1) :
    (modulePullback B S hS
          (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)).map
        (conormalMap B S hS Z Y (𝟙 X)
          (ObjectProperty.homMk (Subfunctor.homOfLe hZY))
          (subspaceInclusion_homOfLe_square B S hS Y Z hZY)) ≫
      conormalMap B S hS (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z) Z
        (subspaceInclusion B S hS X Y)
        (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)
        (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Y) Z) = 0

AlgebraicGeometry.Space.exact_conormalShortComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealSheafSequenceExact.lean, line 676. The attribute's comment: “exactness at the middle term”. References: SGA 6 VIII (2.2), “partial”.

Exactness in the middle of [Stacks Project, Tag 06BD]. Let Y and Z be closed subspaces of an algebraic space X with Z ⊆ Y, let j : Y ⟶ X be the inclusion and let p : j⁻¹(Z) ⟶ Z be the projection. The conormal sequence of the pair,

p^*(i^*𝒞_{Y/X}) ⟶ p^*𝒞_{Z/X} ⟶ 𝒞_{j⁻¹(Z)/Y},

is exact in the middle.

The sequence is the inverse image along j, and then along the inclusion of j⁻¹(Z), of the sequence of defining ideal sheaves (𝟙 X)^*𝓘_Y ⟶ 𝓘_Z ⟶ j_*𝓘_{j⁻¹(Z)}, which is exact in the middle and whose second map is an epimorphism, so exactness in the middle survives both inverse images (AlgebraicGeometry.Space.exact_map_idealSheafSequence, written out as AlgebraicGeometry.Space.exact_mk_map_idealSheafSequence). The identification of the two sequences is the pair of squares AlgebraicGeometry.Space.conormalSequence_comparison_square₁₂ and AlgebraicGeometry.Space.conormalSequence_comparison_square₂₃, whose vertical maps are isomorphisms — the inverse image along p of AlgebraicGeometry.Space.conormalPullbackComparison followed by a component of AlgebraicGeometry.Space.conormalPullbackCompIso, that component at the defining ideal sheaf of Z, and the identity — and the transport along them is CategoryTheory.Limits.exact_mk_of_squares.

The companion clauses of the tag are AlgebraicGeometry.Space.conormalMap_comp_conormalMap_eq_zero, which says that the two arrows compose to zero, and AlgebraicGeometry.Space.epi_conormalMap_closedSubspaces, which says the second is an epimorphism; with this clause the tag carries all three.

The source and target of the inverse-image functor along p are supplied explicitly, as the projections of the two subspaces, and the vanishing is taken from AlgebraicGeometry.Space.conormalMap_comp_conormalMap_eq_zero_chain rather than from the clause-one instance; the implementation notes record why.

theorem exact_conormalShortComplex :
    (ShortComplex.mk
      ((@modulePullback B S hS
          (⟨(preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z).1.toFunctor,
              (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z).2.1⟩ :
            AlgebraicSpaces B S hS)
          (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS)
          (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)).map
        (conormalMap B S hS Z Y (𝟙 X) (ObjectProperty.homMk (Subfunctor.homOfLe hZY))
          (subspaceInclusion_homOfLe_square B S hS Y Z hZY)))
      (conormalMap B S hS (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z) Z
        (subspaceInclusion B S hS X Y)
        (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)
        (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Y) Z))
      (conormalMap_comp_conormalMap_eq_zero_chain B S hS Y Z hZY
        (preimageSubspace B S hS (subspaceInclusion B S hS X Y) Z)
        (preimageProjection B S hS (subspaceInclusion B S hS X Y) Z)
        (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Y) Z))).Exact

Sources

Section76.6 The normal cone of an immersion #

Section 76.6 of the Stacks Project, Tag 09RM. 7 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09RN, a definition

Tag 09RN in the Stacks Project.

AlgebraicGeometry.Space.conormalAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebra.lean, line 211. The attribute's comment: “the conormal algebra of a closed immersion”.

Stacks Project, Tag 09RN. The conormal algebra 𝒞_{Z/X,*} of a closed immersion i : Z ⟶ X of algebraic spaces: the inverse image along i of the sheaf of graded 𝒪_X-algebras ⨁_{n ≥ 0} 𝓘ⁿ, for 𝓘 the ideal sheaf of i.

Its degree-n piece is i^*(𝓘ⁿ), which is the 𝒪_Z-module the source describes as 𝓘ⁿ/𝓘ⁿ⁺¹; the module documentation records why, and that the identification is deferred, as it is in the degree-one case AlgebraicGeometry.Space.conormalModule.

noncomputable def conormalAlgebra (i : Z ⟶ X) :
    SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf B S hS Z)

AlgebraicGeometry.Space.conormalAlgebraOfImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebra.lean, line 319. The attribute's comment: “the conormal algebra of an immersion”.

Stacks Project, Tag 09RN. The conormal algebra 𝒞_{Z/X,*} of an immersion i : Z ⟶ X of algebraic spaces: the conormal algebra of the closed immersion of Z into the complement X ∖ ∂Z of the boundary of its image, through which i factors by Stacks 04CE.

Its degree-n piece is the inverse image along that closed immersion of the n-th power of the ideal sheaf of Z in X ∖ ∂Z, which is the 𝒪_Z-module the source describes as 𝓘ⁿ/𝓘ⁿ⁺¹.

noncomputable def conormalAlgebraOfImmersion (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    SheafOfModules.GradedAlgebra.{u, u}
      (structureRingSheaf B S hS (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS))

AlgebraicGeometry.Space.conormalAlgebraPiece, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/ClosedImmersion/ConormalAlgebra.lean, line 205. The attribute's comment: “the homogeneous pieces, as inverse images of the ideal powers, for a closed subspace”. References: EGA IV (16.1.2), “I^n/I^{n+1} pieces”.

The homogeneous pieces of the conormal algebra of a closed subspace. The degree-n piece 𝒞_{Z/X, n} of the conormal algebra of a closed subspace Z of an algebraic space X is the inverse image along the inclusion i : Z ⟶ X of the n-th power of the defining ideal sheaf 𝓘_Z ⊆ 𝒪_X of Stacks 03MB.

noncomputable def conormalAlgebraPiece (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) (n : ℕ) :
    Modules.{u, u} B S hS Z.1.toFunctor Z.2.1

Tag 09RP, an equation

Tag 09RP in the Stacks Project.

AlgebraicGeometry.Space.conormalAlgebraPiecePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraDegreeN.lean, line 480.

Stacks 09RP. For a closed subspace Z of an algebraic space X with inclusion i and defining ideal sheaf 𝓘, the direct image of the degree-n piece of the conormal algebra is the degree-n graded piece of 𝓘:

i_*𝒞_{Z/X, n} = 𝓘ⁿ/𝓘ⁿ⁺¹.

The degree-n piece is AlgebraicGeometry.Space.conormalAlgebraPiece, the inverse image i^*(𝓘ⁿ) of Stacks 09RN; in degree one it is the conormal module of Stacks 04CN, and in degree zero the inverse image of the structure sheaf of X. The identification with 𝓘ⁿ/𝓘ⁿ⁺¹ is the inverse of the unit of Stacks 03LU, transported along AlgebraicGeometry.Space.pullbackConormalGradedPieceIso; AlgebraicGeometry.Space.isoConormalAlgebraPiece records that it determines 𝒞_{Z/X, n} up to isomorphism, which is what makes the equation of the source an identification and not merely the assertion that some module has that direct image.

def conormalAlgebraPiecePushforwardIso (n : ℕ) :
    (modulePushforward B S hS (subspaceInclusion B S hS X Z)).obj
        (conormalAlgebraPiece B S hS X Z n) ≅ conormalGradedPiece B S hS X Z n

AlgebraicGeometry.Space.isoConormalAlgebraPiece, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraDegreeN.lean, line 498. The attribute's comment: “the characterizing property 76.6.1.1 determines 𝒞_{Z/X, n} up to isomorphism”.

The degree-n piece of the conormal algebra is determined by Stacks 09RP. An 𝒪_Z-module whose direct image along the inclusion is 𝓘ⁿ/𝓘ⁿ⁺¹ is isomorphic to 𝒞_{Z/X, n}, because the direct image of modules along a closed immersion is fully faithful (Stacks 04CJ, part (2)). This is the uniqueness clause behind the equality sign of the source.

The source introduces 76.6.1.1 by saying that 𝒞_{Z/X, n} is "characterized by the property" i_*𝒞_{Z/X, n} = 𝓘ⁿ/𝓘ⁿ⁺¹; this is that characterization, and it is what licenses reading AlgebraicGeometry.Space.conormalAlgebraPiecePushforwardIso as the equality sign of the source rather than as the weaker assertion that some module has that direct image.

def isoConormalAlgebraPiece (n : ℕ) (Cc : Modules.{u, u} B S hS Z.1.toFunctor Z.2.1)
    (e : (modulePushforward B S hS (subspaceInclusion B S hS X Z)).obj Cc ≅
      conormalGradedPiece B S hS X Z n) :
    Cc ≅ conormalAlgebraPiece B S hS X Z n

AlgebraicGeometry.Space.conormalAlgebraDegreeZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraDegreeZero.lean, line 157. The attribute's comment: “degree zero”.

For a closed subspace Z of an algebraic space X with inclusion i and defining ideal sheaf 𝓘, the direct image of the structure sheaf of Z is the quotient of the structure sheaf of X by 𝓘:

i_*𝒞_{Z/X, 0} = i_*𝒪_Z = 𝒪_X/𝓘 = 𝓘⁰/𝓘¹.

The isomorphism is induced by the structure projection.

noncomputable def conormalAlgebraDegreeZeroIso :
    cokernel (definingIdealSheaf B S hS X Z).ι ≅ pushforwardStructureSheaf B S hS X Z

Tag 09RQ, an equation

Tag 09RQ in the Stacks Project.

AlgebraicGeometry.Space.symmetricAlgebraToConormalAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSymmetricAlgebra.lean, line 165. The attribute's comment: “the canonical map from the symmetric algebra on the conormal module”.

Stacks Project, Tag 09RQ, Equation 76.6.1.2. Let i : Z ⟶ X be a morphism of algebraic spaces and let A be a sheaf of graded 𝒪_Z-algebras which is the symmetric algebra on the conormal module 𝒞_{Z/X} = (𝒞_{Z/X,*})_1, with degree-one generator ι. Then there is a canonical unital homomorphism of sheaves of graded 𝒪_Z-algebras

Sym^*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*},

the unique one extending the identity of the conormal module.

It exists because the degree-(1,1) multiplication of the conormal algebra is commutative, by AlgebraicGeometry.Space.conormalAlgebra_mul_one_one_comm, which is exactly the condition the universal property of the symmetric algebra tests a degree-one generator against.

noncomputable def symmetricAlgebraToConormalAlgebra (i : Z ⟶ X)
    (A : SheafOfModules.GradedAlgebra.{u, u} (structureRingSheaf B S hS Z))
    (ι : (conormalAlgebra B S hS i).piece 1 ⟶ A.piece 1)
    (hA : SheafOfModules.GradedAlgebra.IsSymmetricAlgebra A ι) :
    SheafOfModules.GradedAlgebra.UnitalHom A (conormalAlgebra B S hS i)

AlgebraicGeometry.Space.symmetricAlgebraToConormalAlgebraOfImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSymmetricAlgebra.lean, line 211. The attribute's comment: “the canonical map from the symmetric algebra, for an immersion”.

Stacks Project, Tag 09RQ for an immersion. The canonical map Sym^*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} of Equation 76.6.1.2 for an immersion i : Z ⟶ X, taken through the closed factorisation of Stacks 04CE which defines AlgebraicGeometry.Space.conormalAlgebraOfImmersion.

noncomputable def symmetricAlgebraToConormalAlgebraOfImmersion
    (hX : IsAlgebraicSpace B S hS X₀) (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀)
    (hi : IsImmersion B S hS i)
    (A : SheafOfModules.GradedAlgebra.{u, u}
      (structureRingSheaf B S hS (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS)))
    (ι : (conormalAlgebraOfImmersion B S hS hX hZ i hi).piece 1 ⟶ A.piece 1)
    (hA : SheafOfModules.GradedAlgebra.IsSymmetricAlgebra A ι) :
    SheafOfModules.GradedAlgebra.UnitalHom A
      (conormalAlgebraOfImmersion B S hS hX hZ i hi)

Tag 09RR, a lemma

Tag 09RR in the Stacks Project.

AlgebraicGeometry.Space.conormalAlgebraEtaleRestrictionPieceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraEtaleRestriction.lean, line 137. The attribute's comment: “the conormal algebra of an etale localisation, in each degree”.

Let i : Z ⟶ X be a morphism of algebraic spaces, let φ : U ⟶ X be étale and let Z_U = U ×_X Z with projections p : Z_U ⟶ Z and i_U : Z_U ⟶ U. Then the inverse image along p of the degree-n piece of the conormal algebra of i is the degree-n piece of the conormal algebra of i_U:

(𝒞_{Z/X,*}|_{Z_U})_n = p^*(𝒞_{Z/X,*})_n ≅ (𝒞_{Z_U/U,*})_n.

The isomorphism is the square comparison p^*i^* ≅ i_U^*φ^* of AlgebraicGeometry.Space.modulePullbackSquareCompIso, then the inverse image along i_U of the identification of φ^* with étale restriction of [Stacks Project, Tag 03LW], then the equality 𝓘ⁿ|_U = 𝓘_Uⁿ of the powers of the kernel ideal sheaves.

noncomputable def conormalAlgebraEtaleRestrictionPieceIso (p : ZU ⟶ Z) (iU : ZU ⟶ U) (i : Z ⟶ X)
    (φ : U ⟶ X) (sq : IsPullback p iU i φ) (hφ : IsEtale B S hS φ.hom) (n : ℤ) :
    (modulePullback B S hS p).obj ((conormalAlgebra B S hS i).piece n) ≅
      (conormalAlgebra B S hS iU).piece n

AlgebraicGeometry.Space.conormalAlgebraEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraEtaleRestrictionGraded.lean, line 331. The attribute's comment: “the conormal algebra of an etale localisation, as graded algebras”.

Stacks 09RR. Let i : Z ⟶ X be a morphism of algebraic spaces, let φ : U ⟶ X be étale and let Z_U = U ×_X Z, with projections p : Z_U ⟶ Z and i_U : Z_U ⟶ U. Then the restriction p^*𝒞_{Z/X,*} of the conormal algebra of i is the conormal algebra of i_U, as sheaves of graded 𝒪_{Z_U}-algebras:

𝒞_{Z/X,*}|_{Z_U} = p^*𝒞_{Z/X,*} ≅ 𝒞_{Z_U/U,*}.

The isomorphism is canonical: it is the multiplicative composition comparison p^*i^* ≅ (i_U ≫ φ)^* ≅ i_U^*φ^* of Stacks 03LU followed by the inverse image along i_U of the identification φ^*(⨁ 𝓘ⁿ) = ⨁ 𝓘_Uⁿ of the graded algebras of the powers of the kernel ideal sheaves, which is Stacks 03LW in each degree.

No hypothesis is imposed on i and U is an arbitrary algebraic space étale over X; for an immersion i and a scheme U this is the statement of Stacks 09RR.

noncomputable def conormalAlgebraEtaleRestrictionIso (p : ZU ⟶ Z) (iU : ZU ⟶ U) (i : Z ⟶ X)
    (φ : U ⟶ X) (sq : IsPullback p iU i φ) (hφ : IsEtale B S hS φ.hom) :
    (gradedPull (X := smallEtaleRingedTopos B S hS ZU) (Y := smallEtaleRingedTopos B S hS Z)
        (smallEtaleRingedToposHom B S hS p)).obj (conormalAlgebra B S hS i) ≅
      conormalAlgebra B S hS iU

AlgebraicGeometry.Space.conormalAlgebraEtaleRestrictionIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraEtaleRestrictionGraded.lean, line 388. The attribute's comment: “functoriality in U of the identification of conormal algebras”.

Stacks 09RR, functoriality in U. Let i : Z ⟶ X be a morphism of algebraic spaces and let φ : U ⟶ X, φ' : U' ⟶ X be étale, with cartesian squares Z_U = U ×_X Z and Z_{U'} = U' ×_X Z. Let ψ : U' ⟶ U be a morphism over X and q : Z_{U'} ⟶ Z_U the induced morphism, so that q ≫ p = p' and q ≫ i_U = i_{U'} ≫ ψ. Then the identification 𝒞_{Z/X,*}|_{Z_{U'}} ≅ 𝒞_{Z_{U'}/U',*} of Stacks 09RR along φ' is the identification along φ, restricted along q, followed by the identification along ψ:

p'^*𝒞_{Z/X,*} ≅ q^*p^*𝒞_{Z/X,*} ≅ q^*𝒞_{Z_U/U,*} ≅ 𝒞_{Z_{U'}/U',*}.

theorem conormalAlgebraEtaleRestrictionIso_comp (p : ZU ⟶ Z) (iU : ZU ⟶ U) (i : Z ⟶ X)
    (φ : U ⟶ X) (sq : IsPullback p iU i φ) (hφ : IsEtale B S hS φ.hom) (p' : ZU' ⟶ Z)
    (iU' : ZU' ⟶ U') (φ' : U' ⟶ X) (sq' : IsPullback p' iU' i φ')
    (hφ' : IsEtale B S hS φ'.hom) (ψ : U' ⟶ U) (hψφ : ψ ≫ φ = φ') (q : ZU' ⟶ ZU)
    (hqp : q ≫ p = p') (hqi : q ≫ iU = iU' ≫ ψ) :
    conormalAlgebraEtaleRestrictionIso B S hS p' iU' i φ' sq' hφ' =
      (gradedAlgebraPullbackCompIsoOfEq B S hS q p p' hqp.symm).app (conormalAlgebra B S hS i) ≪≫
        (gradedPull (X := smallEtaleRingedTopos B S hS ZU') (Y := smallEtaleRingedTopos B S hS ZU)
            (smallEtaleRingedToposHom B S hS q)).mapIso
          (conormalAlgebraEtaleRestrictionIso B S hS p iU i φ sq hφ) ≪≫
        conormalAlgebraEtaleRestrictionIso B S hS q iU' iU ψ
          (isPullback_of_comp_eq B S hS sq sq' ψ hψφ q hqp hqi)
          (isEtale_of_comp_eq B S hS ψ hφ hφ' hψφ)

AlgebraicGeometry.Space.conormalAlgebraOfImmersionEtaleRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraEtaleRestrictionGraded.lean, line 468. The attribute's comment: “the conormal algebra of an immersion, restricted to an etale U, as graded algebras”.

Stacks 09RR, for the conormal algebra of an immersion as defined in Stacks 09RN. Let i : Z ⟶ X be an immersion of algebraic spaces, let φ : U ⟶ X be étale and let Z_U = U ×_X Z, with projections p : Z_U ⟶ Z and i_U : Z_U ⟶ U; then i_U is an immersion and

𝒞_{Z/X,*}|_{Z_U} = p^*𝒞_{Z/X,*} ≅ 𝒞_{Z_U/U,*}

as sheaves of graded 𝒪_{Z_U}-algebras, where both conormal algebras are those of Stacks 09RN, AlgebraicGeometry.Space.conormalAlgebraOfImmersion.

It is AlgebraicGeometry.Space.conormalAlgebraEtaleRestrictionIso read through the identification AlgebraicGeometry.Space.conormalAlgebraIsoConormalAlgebraOfImmersion on both sides.

noncomputable def conormalAlgebraOfImmersionEtaleRestrictionIso (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i)
    {U ZU : AlgebraicSpaces B S hS} (p : ZU ⟶ ⟨Z₀, hZ⟩) (iU : ZU ⟶ U) (φ : U ⟶ ⟨X₀, hX⟩)
    (sq : IsPullback p iU
      (ObjectProperty.homMk i : (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS) ⟶ ⟨X₀, hX⟩) φ)
    (hφ : IsEtale B S hS φ.hom) :
    (gradedPull (X := smallEtaleRingedTopos B S hS ZU)
        (Y := smallEtaleRingedTopos B S hS ⟨Z₀, hZ⟩) (smallEtaleRingedToposHom B S hS p)).obj
        (conormalAlgebraOfImmersion B S hS hX hZ i hi) ≅
      conormalAlgebraOfImmersion B S hS U.2 ZU.2 iU.hom (isImmersion_of_isPullback B S hS sq hi)

AlgebraicGeometry.Space.conormalAlgebraOfImmersionEtaleRestrictionIso_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraEtaleRestrictionGraded.lean, line 494. The attribute's comment: “functoriality in U, for the conormal algebra of an immersion”.

Stacks 09RR, functoriality in U, for the conormal algebra of an immersion as defined in Stacks 09RN. Let i : Z ⟶ X be an immersion and let φ : U ⟶ X, φ' : U' ⟶ X be étale, with cartesian squares Z_U = U ×_X Z and Z_{U'} = U' ×_X Z. Let ψ : U' ⟶ U be a morphism over X and q : Z_{U'} ⟶ Z_U the induced morphism, so that q ≫ p = p' and q ≫ i_U = i_{U'} ≫ ψ. Then the identification 𝒞_{Z/X,*}|_{Z_{U'}} ≅ 𝒞_{Z_{U'}/U',*} along φ' is the identification along φ, restricted along q, followed by the identification along ψ for the immersion i_U.

theorem conormalAlgebraOfImmersionEtaleRestrictionIso_comp (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i)
    {U ZU U' ZU' : AlgebraicSpaces B S hS} (p : ZU ⟶ ⟨Z₀, hZ⟩) (iU : ZU ⟶ U)
    (φ : U ⟶ ⟨X₀, hX⟩)
    (sq : IsPullback p iU
      (ObjectProperty.homMk i : (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS) ⟶ ⟨X₀, hX⟩) φ)
    (hφ : IsEtale B S hS φ.hom) (p' : ZU' ⟶ ⟨Z₀, hZ⟩) (iU' : ZU' ⟶ U') (φ' : U' ⟶ ⟨X₀, hX⟩)
    (sq' : IsPullback p' iU'
      (ObjectProperty.homMk i : (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS) ⟶ ⟨X₀, hX⟩) φ')
    (hφ' : IsEtale B S hS φ'.hom) (ψ : U' ⟶ U) (hψφ : ψ ≫ φ = φ') (q : ZU' ⟶ ZU)
    (hqp : q ≫ p = p') (hqi : q ≫ iU = iU' ≫ ψ) :
    conormalAlgebraOfImmersionEtaleRestrictionIso B S hS hX hZ i hi p' iU' φ' sq' hφ' =
      (gradedAlgebraPullbackCompIsoOfEq B S hS q p p' hqp.symm).app
          (conormalAlgebraOfImmersion B S hS hX hZ i hi) ≪≫
        (gradedPull (X := smallEtaleRingedTopos B S hS ZU') (Y := smallEtaleRingedTopos B S hS ZU)
            (smallEtaleRingedToposHom B S hS q)).mapIso
          (conormalAlgebraOfImmersionEtaleRestrictionIso B S hS hX hZ i hi p iU φ sq hφ) ≪≫
        conormalAlgebraOfImmersionEtaleRestrictionIso B S hS U.2 ZU.2 iU.hom
          (isImmersion_of_isPullback B S hS sq hi) q iU' ψ
          (isPullback_of_comp_eq B S hS sq sq' ψ hψφ q hqp hqi)
          (isEtale_of_comp_eq B S hS ψ hφ hφ' hψφ)

Tag 09RS, a lemma

Tag 09RS in the Stacks Project.

AlgebraicGeometry.Space.conormalAlgebraOfImmersionSquareMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraOfImmersionSquareMap.lean, line 229. The attribute's comment: “the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} for immersions i, i', on the conormal algebras of immersions of Tag 09RN”.

[Stacks Project, Tag 09RS] for a square of immersions, on the conormal algebras of [Stacks Project, Tag 09RN]. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a commutative square of algebraic spaces over S with i and i' immersions. There is a canonical homomorphism of sheaves of graded 𝒪_Z-algebras

f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*},

where 𝒞_{Z/X,*} is the conormal algebra of the immersion i, that is of its closed factorisation i₀ : Z ⟶ X ∖ ∂Z (AlgebraicGeometry.Space.conormalAlgebraOfImmersion), and likewise for i'.

It is the inverse image along f of the inverse of the isomorphism AlgebraicGeometry.Space.conormalAlgebraOfImmersionIso for i', then the composition comparison f^*𝟙^* ≅ f^*, then the canonical map AlgebraicGeometry.Space.conormalAlgebraSquareMap of the commutative square with edges i₀, ι ≫ g, f and i'; the last is built from g^♯ exactly as in the source's proof.

noncomputable def conormalAlgebraOfImmersionSquareMap (i : 𝒵 ⟶ 𝒳) (i' : 𝒵' ⟶ 𝒳')
    (f : 𝒵 ⟶ 𝒵') (g : 𝒳 ⟶ 𝒳') (hsq : i ≫ g = f ≫ i') (hi : IsImmersion B S hS i.hom)
    (hi' : IsImmersion B S hS i'.hom) :
    (gradedPull (X := smallEtaleRingedTopos B S hS 𝒵) (Y := smallEtaleRingedTopos B S hS 𝒵')
        (smallEtaleRingedToposHom B S hS f)).obj
        (conormalAlgebraOfImmersion B S hS hX' hZ' i'.hom hi') ⟶
      conormalAlgebraOfImmersion B S hS hX hZ i.hom hi

AlgebraicGeometry.Space.conormalAlgebraSquareMapOfPullbackHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraSquareMap.lean, line 323. The attribute's comment: “the canonical map, given the ambient homomorphism g^*(⨁ 𝓙ⁿ) ⟶ ⨁ 𝓘ⁿ”.

The canonical map of conormal algebras of [Stacks Project, Tag 09RS], given the ambient graded homomorphism. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a commutative square of algebraic spaces, hsq : i ≫ g = f ≫ i'. Write 𝓘 = Ker(i^♯) ⊆ 𝒪_X and 𝓙 = Ker((f ≫ i')^♯) ⊆ 𝒪_{X'} for the kernel ideal sheaf of the diagonal. Given a homomorphism of sheaves of graded 𝒪_X-algebras

Ψ : g^*(⨁_{n ≥ 0} 𝓙ⁿ) ⟶ ⨁_{n ≥ 0} 𝓘ⁿ

on the ambient space, there is a canonical homomorphism of sheaves of graded 𝒪_Z-algebras

f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*}.

It is the composite of the two factors of the source's proof: the unconditional first factor AlgebraicGeometry.Space.conormalAlgebraPullbackCompMap, which carries f^*𝒞_{Z'/X',*} into the conormal algebra 𝒞_{Z/X',*} of the diagonal and rests on the containment of kernel ideal sheaves AlgebraicGeometry.Space.kernelIdealSheaf_le_comp, followed by the ambient factor AlgebraicGeometry.Space.conormalAlgebraAmbientSquareMapOfPullbackHom, which descends Ψ from X to Z along the Stacks 03LU composition comparison.

Ψ is a hypothesis and not the conclusion: it is a homomorphism upstairs on the ambient space X between the graded algebras of the powers of the two kernel ideal sheaves, whereas the conclusion is a homomorphism downstairs on Z between the conormal algebras of the two vertical arrows. The module documentation of StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraAmbientGradedTransport.lean records that no such Ψ is constructed yet and what its construction is waiting for.

The statement takes i and i' to be arbitrary morphisms, where Stacks 09RS takes them to be immersions; nothing here uses any property of them, so this is strictly more general and specialises to the source's statement.

noncomputable def conormalAlgebraSquareMapOfPullbackHom (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z')
    (g : X ⟶ X') (hsq : i ≫ g = f ≫ i')
    (Ψ : (gradedPull (X := smallEtaleRingedTopos B S hS X)
          (Y := smallEtaleRingedTopos B S hS X') (smallEtaleRingedToposHom B S hS g)).obj
        (kernelIdealGradedAlgebra B S hS (f ≫ i')) ⟶ kernelIdealGradedAlgebra B S hS i) :
    (gradedPull (X := smallEtaleRingedTopos B S hS Z)
        (Y := smallEtaleRingedTopos B S hS Z')
        (smallEtaleRingedToposHom B S hS f)).obj (conormalAlgebra B S hS i') ⟶
      conormalAlgebra B S hS i

AlgebraicGeometry.Space.conormalAlgebraSquareMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/KernelIdealGradedPushforward.lean, line 377. The attribute's comment: “the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} of graded algebras”.

[Stacks Project, Tag 09RS]: the canonical map of conormal algebras of a commutative square. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a commutative square of algebraic spaces over S, hsq : i ≫ g = f ≫ i'. There is a canonical homomorphism of sheaves of graded 𝒪_Z-algebras

f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*}.

It is AlgebraicGeometry.Space.conormalAlgebraSquareMapOfPullbackHom at the ambient homomorphism AlgebraicGeometry.Space.kernelIdealGradedPullbackHom : g^*(⨁ 𝓙ⁿ) ⟶ ⨁ 𝓘ⁿ induced by g^♯, where 𝓘 = Ker(i^♯) and 𝓙 = Ker((f ≫ i')^♯): the first factor f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X',*} comes from the containment Ker((i')^♯) ⊆ 𝓙, and the second factor 𝒞_{Z/X',*} ⟶ 𝒞_{Z/X,*} is the inverse image along i of the ambient homomorphism, read through the Stacks 03LU composition comparison (f ≫ i')^* ≅ i^* g^*. This is the source's proof: g^♯ carries g^{-1}((𝓘')ⁿ) into 𝓘ⁿ, and pulling back to Z, with i^{-1}g^{-1} = f^{-1}(i')^{-1}, gives the map in each degree.

The statement takes i and i' to be arbitrary morphisms, where Stacks 09RS takes them to be immersions; nothing here uses any property of them.

noncomputable def conormalAlgebraSquareMap (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z')
    (g : X ⟶ X') (hsq : i ≫ g = f ≫ i') :
    (gradedPull (X := smallEtaleRingedTopos B S hS Z)
        (Y := smallEtaleRingedTopos B S hS Z')
        (smallEtaleRingedToposHom B S hS f)).obj (conormalAlgebra B S hS i') ⟶
      conormalAlgebra B S hS i

Tag 09RT, a lemma

Tag 09RT in the Stacks Project.

AlgebraicGeometry.Space.epi_conormalAlgebraOfImmersionSquareMap_app_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraOfImmersionSquareMapCartesian.lean, line 159. The attribute's comment: “surjectivity: for a cartesian square with i, i' immersions, the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} of Tag 09RS on the conormal algebras of immersions of Tag 09RN is surjective in every degree”.

[Stacks Project, Tag 09RT], surjectivity, on the conormal algebras of immersions. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a cartesian square of algebraic spaces with i and i' immersions. Then the canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] between the conormal algebras of the immersions of [Stacks Project, Tag 09RN] (AlgebraicGeometry.Space.conormalAlgebraOfImmersionSquareMap) is surjective: it is an epimorphism of 𝒪_Z-modules in every degree.

The map is two isomorphisms followed by the canonical map of the square of the closed factorisation of i, which is cartesian (AlgebraicGeometry.Space.isPullback_immersionClosedFactorization_comp), so that AlgebraicGeometry.Space.epi_conormalAlgebraSquareMap_app_of_isPullback applies.

theorem epi_conormalAlgebraOfImmersionSquareMap_app_of_isPullback {i : 𝒵 ⟶ 𝒳} {i' : 𝒵' ⟶ 𝒳'}
    {f : 𝒵 ⟶ 𝒵'} {g : 𝒳 ⟶ 𝒳'} (sq : IsPullback i f g i') (hi : IsImmersion B S hS i.hom)
    (hi' : IsImmersion B S hS i'.hom) (n : ℤ) :
    Epi ((conormalAlgebraOfImmersionSquareMap B S hS hZ hX hZ' hX' i i' f g sq.w hi hi').app
      n)

AlgebraicGeometry.Space.isIso_conormalAlgebraOfImmersionSquareMap_of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraOfImmersionSquareMapCartesian.lean, line 199. The attribute's comment: “flat case: for a cartesian square with i, i' immersions and g flat, the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} of Tag 09RS on the conormal algebras of immersions of Tag 09RN is an isomorphism of graded algebras”.

[Stacks Project, Tag 09RT], the flat case, on the conormal algebras of immersions. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a cartesian square of algebraic spaces with i and i' immersions. If g is flat, the canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] between the conormal algebras of the immersions of [Stacks Project, Tag 09RN] (AlgebraicGeometry.Space.conormalAlgebraOfImmersionSquareMap) is an isomorphism of sheaves of graded 𝒪_Z-algebras.

The map is two isomorphisms followed by the canonical map of the square of the closed factorisation of i, which is cartesian (AlgebraicGeometry.Space.isPullback_immersionClosedFactorization_comp) with flat right edge ι ≫ g (an open immersion is étale, hence flat, and flatness composes), so that AlgebraicGeometry.Space.isIso_conormalAlgebraSquareMap_of_isPullback_of_isFlat applies.

theorem isIso_conormalAlgebraOfImmersionSquareMap_of_isPullback_of_isFlat {i : 𝒵 ⟶ 𝒳}
    {i' : 𝒵' ⟶ 𝒳'} {f : 𝒵 ⟶ 𝒵'} {g : 𝒳 ⟶ 𝒳'} (sq : IsPullback i f g i')
    (hi : IsImmersion B S hS i.hom) (hi' : IsImmersion B S hS i'.hom)
    (hg : IsFlat B S hS g.hom) :
    IsIso (conormalAlgebraOfImmersionSquareMap B S hS hZ hX hZ' hX' i i' f g sq.w hi hi')

AlgebraicGeometry.Space.epi_conormalAlgebraSquareMap_app_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraSquareMapCartesian.lean, line 245. The attribute's comment: “surjectivity: for a cartesian square with i' (hence i) an immersion, the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} of Tag 09RS is surjective in every degree”.

[Stacks Project, Tag 09RT], surjectivity. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a cartesian square of algebraic spaces with i' (hence i) an immersion. Then the canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] is surjective: it is an epimorphism of 𝒪_Z-modules in every degree.

In degree n ≥ 0 the map is the inverse image along i of the degree-n ambient comparison, preceded by two isomorphisms; that comparison is induced by pullback of regular functions (AlgebraicGeometry.Space.isInducedByPullback_conormalAlgebraSquareAmbientComparison_app), so its inverse image along i is an epimorphism by AlgebraicGeometry.Space.epi_modulePullback_map_of_isPullback. In negative degrees the target vanishes.

theorem epi_conormalAlgebraSquareMap_app_of_isPullback (sq : IsPullback i f g i')
    (hi' : IsImmersion B S hS i'.hom) (n : ℤ) :
    Epi ((conormalAlgebraSquareMap B S hS i i' f g sq.w).app n)

AlgebraicGeometry.Space.isIso_conormalAlgebraSquareMap_of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraSquareMapCartesian.lean, line 310. The attribute's comment: “flat case: for a cartesian square with i' (hence i) an immersion and g flat, the canonical map f^𝒞_{Z'/X',} ⟶ 𝒞_{Z/X,*} of Tag 09RS is an isomorphism of graded algebras”.

[Stacks Project, Tag 09RT], the flat case. Let
Z --i--→ X
|        |
f        g
↓        ↓
Z' -i'-→ X'
be a cartesian square of algebraic spaces with i' (hence i) an immersion. If g is flat, the canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] is an isomorphism of sheaves of graded 𝒪_Z-algebras.

Degreewise this is AlgebraicGeometry.Space.isIso_conormalAlgebraSquareMap_app_of_isPullback_of_isFlat, whose nonnegative degrees are AlgebraicGeometry.Space.isIso_modulePullback_map_of_isPullback_of_isFlat for the ambient comparison; a degreewise isomorphism of sheaves of graded algebras is an isomorphism.

theorem isIso_conormalAlgebraSquareMap_of_isPullback_of_isFlat (sq : IsPullback i f g i')
    (hi' : IsImmersion B S hS i'.hom) (hg : IsFlat B S hS g.hom) :
    IsIso (conormalAlgebraSquareMap B S hS i i' f g sq.w)

AlgebraicGeometry.Space.epi_conormalAlgebraSquareMapOfPullbackHom_app_of_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraSquareMapDegreePropagation.lean, line 223. The attribute's comment: “the surjectivity clause, in every nonnegative degree; the cartesian hypothesis is NOT consumed, three inputs being carried: hunit, h0 and h1, the degree-one one being Tag 04CQ's surjectivity clause in ideal-sheaf form transported to this square; the flat clause is isIso_conormalAlgebraSquareMapOfPullbackHom_app_of_isFlat”.

The surjectivity clause of [Stacks Project, Tag 09RT]. The canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] is surjective in every nonnegative degree.

The ambient comparison is surjective in every nonnegative degree by AlgebraicGeometry.Space.epi_conormalAlgebraSquareAmbientComparison_app_of_nonneg, and the canonical map is in each degree the inverse image along i of the ambient comparison preceded by two isomorphisms.

Three inputs are carried: that the ambient comparison carries the unit, and its surjectivity in the degrees zero and one — the conclusions of AlgebraicGeometry.Space.epi_structureSheafMap and of AlgebraicGeometry.Space.epi_idealSheafMap, the ideal-sheaf form of [Stacks Project, Tag 04CQ]'s surjectivity clause, transported to this square. The square being cartesian is therefore not consumed, and neither is either vertical arrow being an immersion. What is proved is that the three suffice: surjectivity propagates from the degrees zero and one to every degree. The module documentation says why none of the three is available in the library, and why carrying the degree-one one is carrying 04CQ's conclusion and not this tag's.

theorem epi_conormalAlgebraSquareMapOfPullbackHom_app_of_nonneg (i : Z ⟶ X) (i' : Z' ⟶ X')
    (f : Z ⟶ Z') (g : X ⟶ X') (hsq : i ≫ g = f ≫ i')
    (Ψ : (gradedPull (X := smallEtaleRingedTopos B S hS X)
          (Y := smallEtaleRingedTopos B S hS X') (smallEtaleRingedToposHom B S hS g)).obj
        (kernelIdealGradedAlgebra B S hS (f ≫ i')) ⟶ kernelIdealGradedAlgebra B S hS i)
    (hunit : SheafOfModules.sectionsMap
        ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 0)
        ((gradedPull (X := smallEtaleRingedTopos B S hS X)
            (Y := smallEtaleRingedTopos B S hS X')
            (smallEtaleRingedToposHom B S hS g)).obj
          (kernelIdealGradedAlgebra B S hS i')).one =
      (kernelIdealGradedAlgebra B S hS i).one)
    (h0 : Epi ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 0))
    (h1 : Epi ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 1))
    (n : ℤ) (hn : 0 ≤ n) :
    Epi ((conormalAlgebraSquareMapOfPullbackHom B S hS i i' f g hsq Ψ).app n)

AlgebraicGeometry.Space.isIso_conormalAlgebraSquareMapOfPullbackHom_app_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalAlgebraSquareMapFlatClause.lean, line 246. The attribute's comment: “the flat clause: an isomorphism in every nonnegative degree when g is flat, flatness consumed through exactness of the inverse image; the cartesian hypothesis is NOT consumed, four inputs being carried: hunit, h0, h1 (Tag 04CQ's flat half transported) and hiota (the n-th power analogue of idealSheafMap_comp_ι); see the module docs”.

The flat clause of [Stacks Project, Tag 09RT]. If g is flat — that is, if the morphism of small étale ringed topoi it induces is flat in the sense of [Stacks Project, Tag 04JB] — then the canonical map f^*𝒞_{Z'/X',*} ⟶ 𝒞_{Z/X,*} of [Stacks Project, Tag 09RS] is an isomorphism in every nonnegative degree.

Flatness is consumed in the injectivity half, through the exactness of the inverse image along a flat morphism. Four inputs are carried: that the ambient comparison carries the unit, its invertibility in the degrees zero and one — the conclusions of AlgebraicGeometry.Space.isIso_structureSheafMap and of the flat half of [Stacks Project, Tag 04CQ], AlgebraicGeometry.Space.isIso_idealSheafMap_of_isFlat, transported to this square — and the compatibility of the comparison with the embeddings of the powers of the two ideal sheaves into the two structure sheaves, whose degree-one instance is AlgebraicGeometry.Space.idealSheafMap_comp_ι. The square being cartesian is therefore not consumed, and neither is either vertical arrow being an immersion. What is proved is that the four suffice: surjectivity and injectivity propagate from the degrees zero and one to every degree. The module documentation says why none of the four is available in the library.

theorem isIso_conormalAlgebraSquareMapOfPullbackHom_app_of_isFlat (i : Z ⟶ X) (i' : Z' ⟶ X')
    (f : Z ⟶ Z') (g : X ⟶ X') (hsq : i ≫ g = f ≫ i')
    (Ψ : (gradedPull (X := smallEtaleRingedTopos B S hS X)
          (Y := smallEtaleRingedTopos B S hS X') (smallEtaleRingedToposHom B S hS g)).obj
        (kernelIdealGradedAlgebra B S hS (f ≫ i')) ⟶ kernelIdealGradedAlgebra B S hS i)
    (hg : (smallEtaleRingedToposHom B S hS g).IsFlat)
    (hunit : SheafOfModules.sectionsMap
        ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 0)
        ((gradedPull (X := smallEtaleRingedTopos B S hS X)
            (Y := smallEtaleRingedTopos B S hS X')
            (smallEtaleRingedToposHom B S hS g)).obj
          (kernelIdealGradedAlgebra B S hS i')).one =
      (kernelIdealGradedAlgebra B S hS i).one)
    (h0 : IsIso ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 0))
    (h1 : IsIso ((conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app 1))
    (hι : ∀ n : ℤ, 0 ≤ n →
      (conormalAlgebraSquareAmbientComparison B S hS i i' f g Ψ).app n ≫
          (kernelIdealSheafZPow B S hS i n).ι =
        (modulePullback B S hS g).map (kernelIdealSheafZPow B S hS i' n).ι ≫
          structureSheafMap B S hS g)
    (n : ℤ) (hn : 0 ≤ n) :
    IsIso ((conormalAlgebraSquareMapOfPullbackHom B S hS i i' f g hsq Ψ).app n)

Tag 09RU, a definition

Tag 09RU in the Stacks Project.

AlgebraicGeometry.Space.immersionNormalCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalConeRelativeSpectrum.lean, line 155. The attribute's comment: “the normal cone C_ZX = Spec_Z(C_{Z/X,*}) of an immersion, as an algebraic space affine over Z”.

Stacks Project, Tag 09RU. The normal cone C_ZX = \underline{Spec}_Z(𝒞_{Z/X,*}) of an immersion i : Z ⟶ X of algebraic spaces, as an algebraic space affine over Z: the relative spectrum (Stacks 081W) of the conormal algebra of Stacks 09RN. Its structure morphism is affine (this is the AffineOver property) and the direct image of its structure sheaf is 𝒞_{Z/X,*} (AlgebraicGeometry.Space.immersionNormalConePushforwardIso).

def immersionNormalCone (hX : IsAlgebraicSpace B S hS X₀) (hZ : IsAlgebraicSpace B S hS Z₀)
    (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    AffineOver B S hS (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS)

AlgebraicGeometry.Space.immersionNormalConePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalConeRelativeSpectrum.lean, line 167. The attribute's comment: “the direct image of the structure sheaf of the normal cone C_ZX is the conormal algebra C_{Z/X,}, i.e. C_ZX = Spec_Z(C_{Z/X,})”.

Stacks Project, Tag 09RU. C_ZX is the relative spectrum of 𝒞_{Z/X,*}: for its projection π : C_ZX ⟶ Z, π_* 𝒪_{C_ZX} ≅ 𝒞_{Z/X,*} as sheaves of commutative 𝒪_Z-algebras.

def immersionNormalConePushforwardIso (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    pushforwardAlgebra B S hS (immersionNormalCone B S hS hX hZ i hi).obj ≅
      conormalAlgebraSheafOfImmersion B S hS hX hZ i hi

AlgebraicGeometry.Space.immersionNormalBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalConeRelativeSpectrum.lean, line 180. The attribute's comment: “the normal bundle N_ZX = Spec_Z(Sym(C_{Z/X})) of an immersion, as an algebraic space affine over Z”.

Stacks Project, Tag 09RU. The normal bundle N_ZX = \underline{Spec}_Z(Sym(𝒞_{Z/X})) of an immersion i : Z ⟶ X of algebraic spaces, as an algebraic space affine over Z: the relative spectrum (Stacks 081W) of the symmetric algebra on the conormal sheaf 𝒞_{Z/X} of Stacks 04CN. Its structure morphism is affine and the direct image of its structure sheaf is Sym(𝒞_{Z/X}) (AlgebraicGeometry.Space.immersionNormalBundlePushforwardIso).

def immersionNormalBundle (hX : IsAlgebraicSpace B S hS X₀) (hZ : IsAlgebraicSpace B S hS Z₀)
    (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    AffineOver B S hS (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS)

AlgebraicGeometry.Space.immersionNormalBundlePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalConeRelativeSpectrum.lean, line 192. The attribute's comment: “the direct image of the structure sheaf of the normal bundle N_ZX is Sym(C_{Z/X}), i.e. N_ZX = Spec_Z(Sym(C_{Z/X}))”.

Stacks Project, Tag 09RU. N_ZX is the relative spectrum of Sym(𝒞_{Z/X}): for its projection π : N_ZX ⟶ Z, π_* 𝒪_{N_ZX} ≅ Sym(𝒞_{Z/X}) as sheaves of commutative 𝒪_Z-algebras.

def immersionNormalBundlePushforwardIso (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    pushforwardAlgebra B S hS (immersionNormalBundle B S hS hX hZ i hi).obj ≅
      conormalSymmetricAlgebraSheafOfImmersion B S hS hX hZ i hi

Sources

LeanAlgebraicGeometry.Space.conormalAlgebra · AlgebraicGeometry.Space.conormalAlgebraOfImmersion · AlgebraicGeometry.Space.conormalAlgebraPiece · AlgebraicGeometry.Space.conormalAlgebraPiecePushforwardIso · AlgebraicGeometry.Space.isoConormalAlgebraPiece · AlgebraicGeometry.Space.conormalAlgebraDegreeZeroIso · AlgebraicGeometry.Space.symmetricAlgebraToConormalAlgebra · AlgebraicGeometry.Space.symmetricAlgebraToConormalAlgebraOfImmersion

Section76.7 Sheaf of differentials of a morphism #

Section 76.7 of the Stacks Project, Tag 04CR. 16 tags here are carried by 85 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04CS, a lemma

Tag 04CS in the Stacks Project.

AlgebraicGeometry.SmallEtale.differentialsComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentials.lean, line 197. The attribute's comment: “the comparison map c'' : (Ω_{X/Y})^a ⟶ 𝓕 of the source's proof, for a derivation of 𝒪_{X_étale} annihilating the functions pulled back from Y”.

Stacks 04CS, the comparison map. Let D be a derivation of 𝒪_{X_étale} with values in a sheaf of 𝒪_{X_étale}-modules 𝓕 which annihilates every function pulled back from an open of Y. This is the morphism c'' : (Ω_{X/Y})^a ⟶ 𝓕 of 𝒪_{X_étale}-modules adjoint, under the adjunction between the associated-module functor of Stacks 03DU (4) and restriction to the small Zariski site, to the morphism c' : Ω_{X/Y} ⟶ ε_* 𝓕 through which the small Zariski restriction of D factors.

At 𝓕 = Ω_{X_étale/Y_étale} and D its universal derivation this is the map the source's proof calls c''.

public noncomputable def differentialsComparison
    (hD : ∀ (W : Y.Opens) (b : Γ(Y, W)), D.d (pullbackSection B hX f W b) = 0) :
    associatedRelativeDifferentials B hX f ⟶ F

AlgebraicGeometry.SmallEtale.differentialsComparison_adjunct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentials.lean, line 225. The attribute's comment: “compatibility of the comparison map with the universal derivation d_{X/Y} on the small Zariski site”.

Stacks 04CS, compatibility with the universal derivations on the small Zariski site. The adjunct c' : Ω_{X/Y} ⟶ ε_* 𝓕 of the comparison map carries the universal derivation d_{X/Y} of Ω_{X/Y} to the small Zariski restriction of D.

public theorem differentialsComparison_adjunct
    (hD : ∀ (W : Y.Opens) (b : Γ(Y, W)), D.d (pullbackSection B hX f W b) = 0) :
    (f.universalRelativeDerivation).postcomp
        ((((associatedModuleAdjunction B X hX).homEquiv
          (Scheme.Hom.relativeDifferentials f) F)
            (differentialsComparison B hX f D hD))).val =
      zariskiRestriction B hX f D hD

AlgebraicGeometry.SmallEtale.eq_differentialsComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentials.lean, line 239. The attribute's comment: “canonicity: the comparison map is the unique morphism whose adjunct carries d_{X/Y} to the small Zariski restriction of the derivation”.

Stacks 04CS, canonicity of the comparison map. It is the only morphism (Ω_{X/Y})^a ⟶ 𝓕 whose adjunct carries the universal derivation d_{X/Y} to the small Zariski restriction of D.

public theorem eq_differentialsComparison
    (hD : ∀ (W : Y.Opens) (b : Γ(Y, W)), D.d (pullbackSection B hX f W b) = 0)
    (g : associatedRelativeDifferentials B hX f ⟶ F)
    (hg : (f.universalRelativeDerivation).postcomp
        ((((associatedModuleAdjunction B X hX).homEquiv
          (Scheme.Hom.relativeDifferentials f) F) g)).val =
      zariskiRestriction B hX f D hD) :
    g = differentialsComparison B hX f D hD

AlgebraicGeometry.SmallEtale.differentialsComparison_postcomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentials.lean, line 277. The attribute's comment: “naturality of the comparison map in the coefficient sheaf of modules”.

Stacks 04CS, naturality of the comparison map in the coefficient sheaf: the comparison map of a derivation postcomposed with α : 𝓕 ⟶ 𝓖 is the comparison map of the derivation followed by α. So the comparison maps form a natural transformation out of (Ω_{X/Y})^a, and in particular an isomorphism (Ω_{X/Y})^a ≅ 𝓕 exhibited by one of them is canonical.

public theorem differentialsComparison_postcomp
    (hD : ∀ (W : Y.Opens) (b : Γ(Y, W)), D.d (pullbackSection B hX f W b) = 0) (α : F ⟶ G) :
    differentialsComparison B hX f (D.postcomp α.val)
        (postcomp_pullbackSection_eq_zero B hX f D hD α) =
      differentialsComparison B hX f D hD ≫ α

AlgebraicGeometry.SmallEtale.existsUnique_postcomp_associatedRelativeDifferentialsDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentialsCorepresentable.lean, line 699. The attribute's comment: “corepresentability: (Ω_{X/Y})^a with d^a is the module of differentials”.

Stacks 04CS. The associated module (Ω_{X/Y})^a of the relative differentials of f : X ⟶ Y, together with the derivation d^a, is the module of differentials of 𝒪_{X_étale} over Y in the sense of Stacks 04BN: every derivation D of 𝒪_{X_étale} with values in a sheaf of 𝒪_{X_étale}-modules 𝓖 which annihilates the functions pulled back from Y factors as D = d^a ∘ g for exactly one morphism g : (Ω_{X/Y})^a ⟶ 𝓖 of sheaves of modules.

The factorization is the comparison map c'' of AlgebraicGeometry.SmallEtale.differentialsComparison; that it is a factorization, and that it is the only one, both come from the injectivity of restriction to the small Zariski site together with the identity AlgebraicGeometry.SmallEtale.differentialsComparison_associatedRelativeDifferentialsDerivation.

The derivation is taken relative to the constant presheaf of integers, which imposes nothing beyond the Leibniz rule, so that the Y-linearity is carried by the hypothesis hD alone; see the implementation notes of StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentials.lean.

public theorem existsUnique_postcomp_associatedRelativeDifferentialsDerivation
    {G : SheafOfModules.{u} (structureSheaf B X hX)}
    (D : PresheafOfModulesOfCommRing.Derivation' (R := (commRingStructureSheaf B X hX).obj) G.val
      (constIntMap (commRingStructureSheaf B X hX).obj))
    (hD : ∀ (W : Y.Opens) (b : Γ(Y, W)), D.d (pullbackSection B hX f W b) = 0) :
    ∃! g : associatedRelativeDifferentials B hX f ⟶ G,
      (associatedRelativeDifferentialsDerivation B hX f).postcomp g.val = D

AlgebraicGeometry.SmallEtale.associatedRelativeDifferentialsDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentialsDerivation.lean, line 245. The attribute's comment: “the derivation d^a into the associated module of differentials”.

The derivation d^a of the source's proof of Stacks 04CS, on (Ω_{X/Y})^a itself: AlgebraicGeometry.SmallEtale.sectionsDerivation transported along the identification of the associated module with its sections description.

public noncomputable def associatedRelativeDifferentialsDerivation :
    PresheafOfModulesOfCommRing.Derivation' (R := (commRingStructureSheaf B X hX).obj)
      (associatedRelativeDifferentials B hX f).val
      (constIntMap (commRingStructureSheaf B X hX).obj)

AlgebraicGeometry.SmallEtale.differentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentialsIso.lean, line 460. The attribute's comment: “the canonical isomorphism (Ω_{X/Y})^a ≅ Ω_{X_étale/Y_étale}”.

Stacks 04CS. The canonical isomorphism (Ω_{X/Y})^a ≅ Ω_{X_étale/Y_étale}: both sides corepresent the functor of Y_étale-derivations of 𝒪_{X_étale}, the left one by AlgebraicGeometry.SmallEtale.existsUnique_postcomp_etaleAssociatedDerivation and the right one by AlgebraicGeometry.SmallEtale.universalDerivation_isUniversal.

public noncomputable def differentialsIso :
    associatedRelativeDifferentials B X.property (schemeHom B f) ≅ sheafOfDifferentials B f

AlgebraicGeometry.SmallEtale.postcomp_differentialsIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentialsIso.lean, line 468. The attribute's comment: “compatibility of the canonical isomorphism with the universal derivations”.

Stacks 04CS, compatibility with the universal derivations: the canonical isomorphism carries d^a to the universal Y_étale-derivation d_{X_étale/Y_étale}.

public theorem postcomp_differentialsIso_hom :
    (etaleAssociatedDerivation B f).postcomp (differentialsIso B f).hom.val =
      universalDerivation B f

AlgebraicGeometry.SmallEtale.isIso_universalDifferentialsComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleDifferentialsIso.lean, line 518. The attribute's comment: “the comparison map c'' is an isomorphism at 𝓕 = Ω_{X_étale/Y_étale}”.

Stacks 04CS, the invertibility clause. The comparison map c'' : (Ω_{X/Y})^a ⟶ 𝓕 of AlgebraicGeometry.SmallEtale.differentialsComparison is an isomorphism at 𝓕 = Ω_{X_étale/Y_étale} carrying its universal derivation. This is the statement the tag's "canonical isomorphism" amounts to for the map the source's proof produces.

public theorem isIso_universalDifferentialsComparison :
    IsIso (universalDifferentialsComparison B f)

AlgebraicGeometry.Space.sheafOfDifferentialsSchemeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeTransport.lean, line 848. The attribute's comment: “the invertibility clause, for a morphism of schemes of the site read on the small étale site of the represented algebraic space”.

Stacks 04CS, the invertibility clause, for every morphism of schemes of the big fppf site over S. For a morphism α : U ⟶ V of schemes of the site, the sheaf of differentials of α read as a morphism of represented algebraic spaces — the module of differentials on the small étale site of yoneda.obj U — is the small-étale module attached by Stacks 03DU (4) to the Zariski sheaf of relative differentials Ω_{U/V} of Stacks 01US.

This is the hypothesis AlgebraicGeometry.Space.SheafOfDifferentialsSchemeComparison, which the consumers of the final sentence of Stacks 04CU need. It is AlgebraicGeometry.SmallEtale.differentialsIso, the canonical isomorphism (Ω_{U/V})^a ≅ Ω_{U_étale/V_étale} of Stacks 04CS, transported along the identification of the small étale site of yoneda.obj U with the small étale site of the scheme underlying U (AlgebraicGeometry.Space.schemeDifferentialsIso).

theorem sheafOfDifferentialsSchemeComparison :
    SheafOfDifferentialsSchemeComparison B S hS

AlgebraicGeometry.Space.sheafOfDifferentialsSchemeVanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeTransport.lean, line 865. The attribute's comment: “the vanishing comparison for a morphism of schemes of the site”.

Stacks 04CS at zero objects, the vanishing comparison that Stacks 04G9 needs: for a morphism ψ : U ⟶ V of schemes of the site, the spaces-level sheaf of differentials of ψ vanishes exactly when Ω_{U/V} does.

theorem sheafOfDifferentialsSchemeVanishing :
    SheafOfDifferentialsSchemeVanishing B S hS

Tag 04CT, a definition

Tag 04CT in the Stacks Project.

AlgebraicGeometry.Space.sheafOfDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentials.lean, line 142. The attribute's comment: “the sheaf of differentials of a morphism of algebraic spaces”.

Stacks 04CT. The sheaf of differentials Ω_{X/Y} of a morphism f : X ⟶ Y of algebraic spaces: the module of differentials of f♯ : f⁻¹𝒪_Y ⟶ 𝒪_X, realized as the associated sheaf of modules of the presheaf of sectionwise Kähler differentials of f♯.

noncomputable def sheafOfDifferentials (f : X ⟶ Y) : Modules.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.universalDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentials.lean, line 150. The attribute's comment: “the universal Y-derivation d_{X/Y}”.

Stacks 04CT. The universal Y-derivation d_{X/Y} : 𝒪_X ⟶ Ω_{X/Y}: the sectionwise Kähler differential followed by the unit of sheafification.

noncomputable def universalDerivation (f : X ⟶ Y) :
    PresheafOfModulesOfCommRing.Derivation' (sheafOfDifferentials B S hS f).val
      (structureSharpInverseImage B S hS f).hom

Tag 04CU, a lemma

Tag 04CU in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_etaleSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleBaseChange.lean, line 190. The attribute's comment: “the identification Ω_{X/Y}|_{U_étale} ≅ Ω_{U/V} is the canonical one on a full square of étale charts: every comparison map of 04CX for a commutative square whose two vertical arrows are étale is an isomorphism. The already registered clause is the case of a square whose bottom edge is an identity”.

Stacks 04CU, the invertibility clause on a full square of étale charts. Let
U --ψ--> V
|        |
a        b
v        v
X --f--> Y
be a commutative square of algebraic spaces over S whose vertical arrows a and b are étale. Then every comparison map c : a^*Ω_{X/Y} ⟶ Ω_{U/V} of Stacks 04CX for that square is an isomorphism.

AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_etale is this statement for b = 𝟙 Y. The step to an arbitrary étale b is the étale-base comparison Ω_{U/V} ≅ Ω_{U/(ψ ≫ b)} of AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso, built from Stacks 03G8 and the clause b^{-1}𝒪_Y = 𝒪_V of Stacks 03LV: composing c with it produces, by AlgebraicGeometry.Space.isSheafOfDifferentialsMap_comp_sharpIsoHom, a comparison map of the square with left edge ψ ≫ b = a ≫ f, which is invertible by the case already proved.

theorem isIso_of_isSheafOfDifferentialsMap_etaleSquare (f : X ⟶ Y) (a : U ⟶ X) (ψ : U ⟶ V)
    (b : V ⟶ Y) (ha : IsEtale B S hS a.hom) (hb : IsEtale B S hS b.hom)
    (hcomm : a ≫ f = ψ ≫ b)
    {c : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS f) ⟶
      sheafOfDifferentials B S hS ψ}
    (hc : IsSheafOfDifferentialsMap B S hS a f ψ c) : IsIso c

AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleComparison.lean, line 126. The attribute's comment: “the identification Ω_{X/Y}|_{U_étale} ≅ Ω_{U/V} is the canonical one: every comparison map of 04CX along an étale a : U ⟶ X, for a square whose bottom edge is an identity, is an isomorphism”.

The comparison map of Stacks 04CX along an étale morphism is an isomorphism. By uniqueness of the comparison map it is the identification of Stacks 04CU, AlgebraicGeometry.Space.sheafOfDifferentialsEtaleSourceLocalizationIso.

The left edge of the square is taken as a morphism p' : U ⟶ Y together with an equality a ≫ f = p', so that the statement applies at whatever spelling of the composite a caller has.

theorem isIso_of_isSheafOfDifferentialsMap_etale (a : U ⟶ X) (ha : IsEtale B S hS a.hom)
    (f : X ⟶ Y) (p' : U ⟶ Y) (hp' : a ≫ f = p')
    {c : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS f) ⟶
      sheafOfDifferentials B S hS p'}
    (hc : IsSheafOfDifferentialsMap B S hS a f p' c) : IsIso c

AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleLocalization.lean, line 239. The attribute's comment: “the étale-base step: Ω_{X/Y} = Ω_{X/Z} when the two structure maps differ by an isomorphism of their sources, which is what 03G8 and the clause b⁻¹𝒪_Y = 𝒪_V of 03LV supply for an étale b : V ⟶ Y at p = ψ, q = ψ ≫ b”.

Stacks 04CU, the étale-base step. If the structure maps of p : X ⟶ Y and q : X ⟶ Z differ by an isomorphism e of their sources, then the two sheaves of differentials agree: Ω_{X/Y} ≅ Ω_{X/Z}.

Both sheaves corepresent the same functor of derivations — a Y-derivation and a Z-derivation are the same additive map, by PresheafOfModulesOfCommRing.Derivation'.precompBase applied to e and to its inverse — so the identification is the one matching the two universal derivations.

Applied to ψ : U ⟶ V and ψ ≫ b : U ⟶ Y for an étale b : V ⟶ Y this is the equality Ω_{U/V} = Ω_{U/Y} which the final sentence of the source's proof uses.

def sheafOfDifferentialsIsoOfSharpIso
    (he : e.hom ≫ structureSharpInverseImage B S hS p =
      structureSharpInverseImage B S hS q) :
    sheafOfDifferentials B S hS p ≅ sheafOfDifferentials B S hS q

AlgebraicGeometry.Space.universalDerivation_sheafOfDifferentialsIsoOfSharpIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleLocalization.lean, line 283. The attribute's comment: “the étale-base step carries one universal derivation to the other”.

Stacks 04CU, the étale-base step is canonical. The identification of AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso carries the universal Y-derivation d_{X/Y} of a local section to the universal Z-derivation d_{X/Z} of the same section, so it is the comparison the source names and not merely some isomorphism.

lemma universalDerivation_sheafOfDifferentialsIsoOfSharpIso
    (he : e.hom ≫ structureSharpInverseImage B S hS p =
      structureSharpInverseImage B S hS q)
    {W : (SmallEtale B S hS X.1)ᵒᵖ} (x : (structureRingSheaf B S hS X).obj.obj W) :
    (((sharpIsoHom B S hS p q e he).val.app W).hom)
        ((universalDerivation B S hS p).d x) =
      (universalDerivation B S hS q).d x

AlgebraicGeometry.Space.sheafOfDifferentialsEtaleLocalizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleLocalization.lean, line 342. The attribute's comment: “the identification Ω_{X/Y}|_{U_étale} ≅ Ω_{U/V} on a square of étale charts, from the étale-source localization of 03LP, 03LQ and 04BO and the étale-base comparison of 03G8 and 03LV”.

Stacks 04CU. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let a ≫ f = ψ ≫ b be a commutative square with a : U ⟶ X and b : V ⟶ Y étale. Then the restriction of Ω_{X/Y} to the small étale site of U — the pullback of 𝒪_X-modules along a, by the abuse of notation of Stacks' Equation 03LW — is Ω_{U/V}.

The source's proof has two steps and both are carried out here. Its first step is the étale-source localization Ω_{X/Y}|_{U_étale} = Ω_{U/Y} of Stacks 03LP, 03LQ and 04BO, which is AlgebraicGeometry.Space.sheafOfDifferentialsEtaleSourceLocalizationIso at the étale a. Its second step is the identification ψ^{-1}𝒪_V = (ψ ≫ b)^{-1}𝒪_Y under the structure maps, which is AlgebraicGeometry.Space.etaleBaseInverseImageStructureSheafIso and its compatibility, from the composition law of Stacks 03G8 and the clause b^{-1}𝒪_Y = 𝒪_V of Stacks 03LV for the étale b. The square then identifies Ω_{U/Y} with Ω_{U/(ψ ≫ b)}, and AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso identifies that with Ω_{U/V}.

noncomputable def sheafOfDifferentialsEtaleLocalizationIso (f : X ⟶ Y) (a : U ⟶ X) (ψ : U ⟶ V)
    (b : V ⟶ Y) (ha : IsEtale B S hS a.hom) (hb : IsEtale B S hS b.hom)
    (hcomm : a ≫ f = ψ ≫ b) :
    (modulePullback B S hS a).obj (sheafOfDifferentials B S hS f) ≅
      sheafOfDifferentials B S hS ψ

AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceComparison.lean, line 356. The attribute's comment: “the comparison map of an étale triangle over the base is an isomorphism”.

Stacks 04CU: the comparison map of a triangle over Y whose upper edge is étale is an isomorphism. Let a : U ⟶ X be étale, let f : X ⟶ Y, and let q : U ⟶ Y be the composite. Any morphism c : a^*Ω_{X/Y} ⟶ Ω_{U/Y} with the characterizing property of Stacks 04CX is an isomorphism.

By AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap there is at most one such c, and AlgebraicGeometry.Space.isSheafOfDifferentialsMap_etaleSourceLocalizationHom exhibits one which is the forward map of AlgebraicGeometry.Space.sheafOfDifferentialsEtaleSourceLocalizationIso.

theorem isIso_of_isSheafOfDifferentialsMap_of_isEtale (a : U ⟶ X) (ha : IsEtale B S hS a.hom)
    (f : X ⟶ Y) (q : U ⟶ Y) (haq : a ≫ f = q)
    {c : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS f) ⟶
      sheafOfDifferentials B S hS q}
    (hc : IsSheafOfDifferentialsMap B S hS a f q c) : IsIso c

AlgebraicGeometry.Space.pullbackDifferentialsMap_eq_etaleSourceLocalizationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceComparisonMap.lean, line 94. The attribute's comment: “the étale-source localization is the comparison map of Stacks 04CX”.

The comparison map of Stacks 04CX along an étale morphism is the étale-source localization of Stacks 04CU. The two morphisms a^*Ω_{X/Y} ⟶ Ω_{U/Y} both have the characterizing property of Stacks 04CX, and at most one morphism does, by AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap.

theorem pullbackDifferentialsMap_eq_etaleSourceLocalizationHom (a : U ⟶ X)
    (ha : IsEtale B S hS a.hom) (f : X ⟶ Y) :
    pullbackDifferentialsMap B S hS a f = etaleSourceLocalizationHom B S hS a ha f

AlgebraicGeometry.Space.isIso_pullbackDifferentialsMap_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceComparisonMap.lean, line 111. The attribute's comment: “the comparison map a^*Ω_{X/Y} ⟶ Ω_{U/Y} along an étale a is invertible”.

Stacks 04CU, the étale-source localization as an invertibility. For an étale a : U ⟶ X and any f : X ⟶ Y, the comparison map c_a : a^*Ω_{X/Y} ⟶ Ω_{U/Y} of Stacks 04CX — the first map AlgebraicGeometry.Space.pullbackDifferentialsMap of the transitivity sequence of Stacks 05Z8 at the square over the identity of Y — is an isomorphism.

It is the forward map of AlgebraicGeometry.Space.sheafOfDifferentialsEtaleSourceLocalizationIso.

theorem isIso_pullbackDifferentialsMap_of_isEtale (a : U ⟶ X) (ha : IsEtale B S hS a.hom)
    (f : X ⟶ Y) : IsIso (pullbackDifferentialsMap B S hS a f)

AlgebraicGeometry.Space.derivationEtalePullbackEquiv_etaleSourceLocalizationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceLocalization.lean, line 421. The attribute's comment: “the étale-source comparison is the one matching the universal derivations”.

The defining property of the forward comparison. Read as a Y-derivation of 𝒪_U through the four bijections, it is the universal Y-derivation d_{U/Y}.

theorem derivationEtalePullbackEquiv_etaleSourceLocalizationHom (a : U ⟶ X)
    (ha : IsEtale B S hS a.hom) (f : X ⟶ Y) :
    derivationEtalePullbackEquiv B S hS a ha f (sheafOfDifferentials B S hS (a ≫ f))
        (etaleSourceLocalizationHom B S hS a ha f) =
      universalDerivation B S hS (a ≫ f)

AlgebraicGeometry.Space.sheafOfDifferentialsEtaleSourceLocalizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceLocalization.lean, line 459. The attribute's comment: “the étale-source localization a^*Ω_{X/Y} ≅ Ω_{U/Y} along an étale a : U ⟶ X: the first step of the source's proof, Properties of Spaces 03LP and Equation 03LQ together with Modules on Sites 04BO”.

Stacks 04CU, the étale-source localization. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let a : U ⟶ X be étale. The restriction of Ω_{X/Y} to the small étale site of U — the pullback of 𝒪_X-modules along a, by the abuse of notation of Stacks' Equation 03LW — is the sheaf of differentials of the composite:

a^*Ω_{X/Y} ≅ Ω_{U/Y}.

Both sides corepresent the functor of Y-derivations of 𝒪_U, the left-hand side by AlgebraicGeometry.Space.derivationEtalePullbackEquiv and the right-hand side by its own universal property, so they are canonically isomorphic; the two morphisms are the ones through which the two universal derivations factor.

This is the clause of Stacks 04CU that AlgebraicGeometry.Space.sheafOfDifferentialsEtaleLocalizationIso consumes directly. Together with the étale-base step AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso it gives the identification Ω_{X/Y}|_{U_étale} ≅ Ω_{U/V} on a square of étale charts that the source states.

def sheafOfDifferentialsEtaleSourceLocalizationIso (a : U ⟶ X) (ha : IsEtale B S hS a.hom)
    (f : X ⟶ Y) :
    (modulePullback B S hS a).obj (sheafOfDifferentials B S hS f) ≅
      sheafOfDifferentials B S hS (a ≫ f)

AlgebraicGeometry.Space.universalDerivation_etaleSourceLocalizationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceLocalization.lean, line 487. The attribute's comment: “the étale-source localization carries the universal derivation of the restriction to the universal derivation d_{U/Y}, on local sections”.

Stacks 04CU, the étale-source localization on local sections. Reading the forward map of the identification a^*Ω_{X/Y} ≅ Ω_{U/Y} as a Y-derivation of 𝒪_U, by the four bijections of AlgebraicGeometry.Space.derivationEtalePullbackEquiv, returns the universal differential d_{U/Y}(x) of every local section x of 𝒪_U. So the identification is the canonical comparison and not merely some isomorphism.

theorem universalDerivation_etaleSourceLocalizationHom (a : U ⟶ X) (ha : IsEtale B S hS a.hom)
    (f : X ⟶ Y) {W : (SmallEtale B S hS U.1)ᵒᵖ}
    (x : (structureRingSheaf B S hS U).obj.obj W) :
    (derivationEtalePullbackEquiv B S hS a ha f (sheafOfDifferentials B S hS (a ≫ f))
        (sheafOfDifferentialsEtaleSourceLocalizationIso B S hS a ha f).hom).d x =
      (universalDerivation B S hS (a ≫ f)).d x

AlgebraicGeometry.Space.isSheafOfDifferentialsMap_etaleBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsMapTransport.lean, line 249. The attribute's comment: “the étale-base step for the comparison map of 04CX: the comparison map over W read through the identifications Ω_{V/W} ≅ Ω_{V/Z} and Ω_{U/W} ≅ Ω_{U/Z} is the comparison map over Z”.

Stacks 04CU, the étale-base step for the comparison map of Stacks 04CX. Let ψ : U ⟶ V be a morphism of algebraic spaces, q : V ⟶ W a structure morphism and cw : W ⟶ Z étale. The comparison map c_ψ : ψ^*Ω_{V/W} ⟶ Ω_{U/W} of the square over W, read through the étale-base identifications Ω_{V/W} ≅ Ω_{V/Z} of the right edge and Ω_{U/W} ≅ Ω_{U/Z} of the left edge, has the characterizing property of the comparison map of the same square over Z.

AlgebraicGeometry.Space.sheafOfDifferentialsIsoOfSharpIso supplies those identifications as isomorphisms of objects; what makes them compatible with the comparison map is that each carries one universal derivation to the other, so that AlgebraicGeometry.Space.IsSheafOfDifferentialsMap.map_comp and AlgebraicGeometry.Space.IsSheafOfDifferentialsMap.comp_right apply.

theorem isSheafOfDifferentialsMap_etaleBase :
    IsSheafOfDifferentialsMap B S hS ψ (q ≫ cw) ((ψ ≫ q) ≫ cw)
      ((modulePullback B S hS ψ).map (etaleBaseDifferentialsIso B S hS q cw hcw).inv ≫
        pullbackDifferentialsMap B S hS ψ q ≫
          (etaleBaseDifferentialsIso B S hS (ψ ≫ q) cw hcw).hom)

Declarations registered for the tag:

AlgebraicGeometry.Space.isSheafOfDifferentialsMap_etaleSourceLocalizationHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsEtaleSourceComparison.lean, line 343 (StacksFrontier): “the étale-source identification is the comparison map of 04CX”.
AlgebraicGeometry.Space.sheafOfDifferentialsSchemeComparison, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeTransport.lean, line 854 (StacksFrontier): “the 'in particular' clause: for U and V schemes of the site the sheaf of differentials of U ⟶ V read on the small étale site agrees with the usual sheaf of differentials of the morphism of schemes, through the associated module of 03DU (4). The identification Ω_{X/Y}|_{U_étale} = Ω_{U/V} itself is elsewhere, on AlgebraicGeometry.Space.sheafOfDifferentialsEtaleLocalizationIso and its chart form”.

Tag 04CV, a lemma

Tag 04CV in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsQuasicoherent.lean, line 222.

Stacks 04CV. The sheaf of differentials Ω_{X/Y} of a morphism f : X ⟶ Y of algebraic spaces over a scheme S is a quasi-coherent 𝒪_X-module on the small étale site of X.

The proof follows the source. An atlas q : V ⟶ Y of the target lifts, by Stacks 02X1, to a surjective étale chart p : U ⟶ X of the source together with a morphism α : U ⟶ V of schemes making the square commute. The identification of Stacks 04CU then reads the pullback of Ω_{X/Y} along p as the sheaf of differentials of α, which AlgebraicGeometry.Space.sheafOfDifferentialsSchemeComparison identifies with the small-étale module associated to the Zariski sheaf of relative differentials of α; that module is quasi-coherent because Ω_{U/V} is (Stacks 08S2) and because the associated module of a quasi-coherent module is quasi-coherent (AlgebraicGeometry.Space.isQuasicoherentOnSite_representedAssociatedModule). Finally Stacks 03M0, conditions (1) and (2), returns quasi-coherence on X from quasi-coherence of the pullback along one surjective étale chart, the pullback of modules and étale restriction being matched by Equation 03LW.

Nothing is carried: the two clauses of Stacks 04CU proper are used through AlgebraicGeometry.Space.sheafOfDifferentialsEtaleLocalizationIso, and the final sentence, read through Stacks 04CS, through AlgebraicGeometry.Space.sheafOfDifferentialsSchemeComparison; see the implementation notes.

theorem isQuasicoherentOnSite_sheafOfDifferentials
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    (sheafOfDifferentials B S hS f).IsQuasicoherentOnSite

Tag 04CW, a remark

Tag 04CW in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.differentialsDescentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/EtaleDescentDatum.lean, line 149. The attribute's comment: “the descent isomorphism α : s^*Ω_{U/Y} ⟶ Ω_{R/Y} ⟶ t^*Ω_{U/Y}”.

The descent isomorphism α : s^*Ω_{U/Y} ⟶ Ω_{R/Y} ⟶ t^*Ω_{U/Y} attached to two étale morphisms s, t : R ⟶ U of schemes over Y inducing the same morphism to Y. Both comparison maps are isomorphisms because s and t are étale.

noncomputable def differentialsDescentIso (p : U ⟶ Y) (s t : R ⟶ U) (q : R ⟶ Y)
    (hs : s ≫ p = q) (ht : t ≫ p = q) [Etale s] [Etale t] :
    (Scheme.Modules.pullback s).obj (relativeDifferentials p) ≅
      (Scheme.Modules.pullback t).obj (relativeDifferentials p)

AlgebraicGeometry.Scheme.Hom.differentialsDescentIso_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/EtaleDescentDatum.lean, line 240. The attribute's comment: “the cocycle condition satisfied by α”.

Stacks 04CW, the cocycle condition. Let T carry three étale legs a₀, a₁, a₂ : T ⟶ U over Y and three morphisms g₀₁, g₁₂, g₀₂ : T ⟶ R realizing the pairs (a₀, a₁), (a₁, a₂) and (a₀, a₂) through (s, t). Then the pullback of α along g₀₂ is the composite of its pullbacks along g₀₁ and g₁₂, each normalized by the canonical factorization isomorphisms. So α is a descent datum.

theorem differentialsDescentIso_cocycle {T : Scheme.{u}} (p : U ⟶ Y) (s t : R ⟶ U) (q : R ⟶ Y)
    (hs : s ≫ p = q) (ht : t ≫ p = q) [Etale s] [Etale t]
    (g₀₁ g₁₂ g₀₂ : T ⟶ R) {a₀ a₁ a₂ : T ⟶ U} (r : T ⟶ Y) [Etale a₀] [Etale a₁] [Etale a₂]
    (h₀₁s : g₀₁ ≫ s = a₀) (h₀₁t : g₀₁ ≫ t = a₁) (h₁₂s : g₁₂ ≫ s = a₁)
    (h₁₂t : g₁₂ ≫ t = a₂) (h₀₂s : g₀₂ ≫ s = a₀) (h₀₂t : g₀₂ ≫ t = a₂)
    (h₀ : a₀ ≫ p = r) (h₁ : a₁ ≫ p = r) (h₂ : a₂ ≫ p = r) :
    (Scheme.Modules.pullbackFactorIso g₀₂ s h₀₂s (relativeDifferentials p)).inv ≫
        (Scheme.Modules.pullback g₀₂).map (differentialsDescentIso p s t q hs ht).hom ≫
          (Scheme.Modules.pullbackFactorIso g₀₂ t h₀₂t (relativeDifferentials p)).hom =
      ((Scheme.Modules.pullbackFactorIso g₀₁ s h₀₁s (relativeDifferentials p)).inv ≫
          (Scheme.Modules.pullback g₀₁).map (differentialsDescentIso p s t q hs ht).hom ≫
            (Scheme.Modules.pullbackFactorIso g₀₁ t h₀₁t (relativeDifferentials p)).hom) ≫
        ((Scheme.Modules.pullbackFactorIso g₁₂ s h₁₂s (relativeDifferentials p)).inv ≫
          (Scheme.Modules.pullback g₁₂).map (differentialsDescentIso p s t q hs ht).hom ≫
            (Scheme.Modules.pullbackFactorIso g₁₂ t h₁₂t (relativeDifferentials p)).hom)

AlgebraicGeometry.Scheme.Hom.differentialsDescentIso_pullbackDescentIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/EtaleDescentDatum.lean, line 271. The attribute's comment: “for a quotient which is a scheme, α agrees with the canonical descent datum of π^*Ω_{X/Y}”.

For a quotient which is a scheme, α is the canonical descent datum of π^*Ω_{X/Y}. For π : U ⟶ X over Y with s ≫ π = t ≫ π, the canonical map π^*Ω_{X/Y} ⟶ Ω_{U/Y} of Stacks 01UV carries the canonical descent isomorphism of π^*Ω_{X/Y} to α; when π is étale that map is an isomorphism, so the module α descends to is Ω_{X/Y}. The same identification for a quotient which is an algebraic space is AlgebraicGeometry.Space.sheafOfDifferentialsDescentIso_canonicalComparison in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsDescent.lean; here the comparison map is constructed rather than hypothesized, so no input beyond the square is needed.

theorem differentialsDescentIso_pullbackDescentIso {X : Scheme.{u}} (pX : X ⟶ Y) (π : U ⟶ X)
    (p : U ⟶ Y) (hp : π ≫ pX = p) (s t : R ⟶ U) (q : R ⟶ Y) (hs : s ≫ p = q)
    (ht : t ≫ p = q) [Etale s] [Etale t] (hπ : s ≫ π = t ≫ π) :
    (Scheme.Modules.pullbackDescentIso π hπ (relativeDifferentials pX)).hom ≫
        (Scheme.Modules.pullback t).map (triangleDifferentialsMap π pX p hp) =
      (Scheme.Modules.pullback s).map (triangleDifferentialsMap π pX p hp) ≫
        (differentialsDescentIso p s t q hs ht).hom

AlgebraicGeometry.Space.sheafOfDifferentialsDescentIso_canonicalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsDescent.lean, line 162. The attribute's comment: “the module α descends to is Ω_{X/Y}: α is the transition isomorphism of the canonical descent datum of Ω_{X/Y} on a presentation π : U ⟶ X of an algebraic space”.

Stacks 04CW. For a presentation π : U ⟶ X of an algebraic space over Y and s, t : R ⟶ U with s ≫ π = t ≫ π, the descent isomorphism α is the transition isomorphism of the canonical descent datum of Ω_{X/Y}: the comparison map c_π : π^*Ω_{X/Y} ⟶ Ω_{U/Y} carries the canonical comparison of the two inverse images of Ω_{X/Y} to α. So the module α descends to is Ω_{X/Y}.

Invertibility of c_s and c_t is the étale-localization clause of Stacks 04CU; the identity it is divided out of, AlgebraicGeometry.Space.canonicalComparison_comp_sheafOfDifferentialsMap, needs no invertibility.

theorem sheafOfDifferentialsDescentIso_canonicalComparison (pX : X ⟶ Y) (π : U ⟶ X) (p : U ⟶ Y)
    {s t : R ⟶ U} (q : R ⟶ Y) (hπ : s ≫ π = t ≫ π)
    {cπ : (modulePullback B S hS π).obj (sheafOfDifferentials B S hS pX) ⟶
      sheafOfDifferentials B S hS p}
    {cs : (modulePullback B S hS s).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS q}
    {ct : (modulePullback B S hS t).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS q}
    (hcπ : IsSheafOfDifferentialsMap B S hS π pX p cπ)
    (hcs : IsSheafOfDifferentialsMap B S hS s p q cs)
    (hct : IsSheafOfDifferentialsMap B S hS t p q ct) [IsIso cs] [IsIso ct] :
    (QuasiCoherentDescent.canonicalComparison s t π π hπ
          (sheafOfDifferentials B S hS pX)).hom ≫
        (modulePullback B S hS t).map cπ =
      (modulePullback B S hS s).map cπ ≫
        (sheafOfDifferentialsDescentIso B S hS cs ct).hom

AlgebraicGeometry.Space.sheafOfDifferentialsDescentIsoOfEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsDescentOfEtale.lean, line 106. The attribute's comment: “the descent isomorphism itself: alpha : s^*Omega_{U/Y} -> t^*Omega_{U/Y}, built from the two etale projections of the groupoid”.

Stacks 04CW. The descent isomorphism α : s^*Ω_{U/Y} ⟶ Ω_{R/Y} ⟶ t^*Ω_{U/Y} attached to two étale morphisms s, t : R ⟶ U of algebraic spaces inducing the same morphism q : R ⟶ Y.

It is the comparison map c_s of Stacks 04CX for the triangle s ≫ p = q, namely AlgebraicGeometry.Space.sheafOfDifferentialsMap, followed by the inverse of the comparison map c_t of the triangle t ≫ p = q. Both comparison maps are isomorphisms because s and t are étale: that is the étale-localization clause of Stacks 04CU, in the form AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_of_isEtale.

def sheafOfDifferentialsDescentIsoOfEtale (p : U ⟶ Y) {s t : R ⟶ U} {q : R ⟶ Y}
    (hs : IsEtale B S hS s.hom) (ht : IsEtale B S hS t.hom) (hsq : s ≫ p = q)
    (htq : t ≫ p = q) :
    (modulePullback B S hS s).obj (sheafOfDifferentials B S hS p) ≅
      (modulePullback B S hS t).obj (sheafOfDifferentials B S hS p)

AlgebraicGeometry.Space.sheafOfDifferentialsDescentIsoOfEtale_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsDescentOfEtale.lean, line 254. The attribute's comment: “the cocycle condition for that isomorphism, which is what the remark leaves to the reader to verify”.

Stacks 04CW, the cocycle condition. Let the test space T carry three étale legs a₀, a₁, a₂ : T ⟶ U over Y and three morphisms g₀₁, g₁₂, g₀₂ : T ⟶ R realizing the pairs (a₀, a₁), (a₁, a₂) and (a₀, a₂) through (s, t) — the situation of the three projections of a triple fibre product. Then the pullback of α along g₀₂ is the composite of its pullbacks along g₀₁ and g₁₂, each normalized by the comparisons of iterated inverse images. So α is a descent datum, which is the check the source leaves to the reader.

theorem sheafOfDifferentialsDescentIsoOfEtale_cocycle {T : AlgebraicSpaces B S hS} (p : U ⟶ Y)
    {s t : R ⟶ U} (q : R ⟶ Y)
    (hs : IsEtale B S hS s.hom) (ht : IsEtale B S hS t.hom) (hsq : s ≫ p = q)
    (htq : t ≫ p = q) (g₀₁ g₁₂ g₀₂ : T ⟶ R) {a₀ a₁ a₂ : T ⟶ U} (r : T ⟶ Y)
    (h₀ : IsEtale B S hS a₀.hom) (h₁ : IsEtale B S hS a₁.hom) (h₂ : IsEtale B S hS a₂.hom)
    (h₀₁s : g₀₁ ≫ s = a₀) (h₀₁t : g₀₁ ≫ t = a₁) (h₁₂s : g₁₂ ≫ s = a₁)
    (h₁₂t : g₁₂ ≫ t = a₂) (h₀₂s : g₀₂ ≫ s = a₀) (h₀₂t : g₀₂ ≫ t = a₂)
    (hr₀ : a₀ ≫ p = r) (hr₁ : a₁ ≫ p = r) (hr₂ : a₂ ≫ p = r) :
    (QuasiCoherentDescent.pullbackComparison B S hS g₀₂ s a₀ h₀₂s
          (sheafOfDifferentials B S hS p)).hom ≫
        (modulePullback B S hS g₀₂).map
          (sheafOfDifferentialsDescentIsoOfEtale B S hS p hs ht hsq htq).hom ≫
        (QuasiCoherentDescent.pullbackComparison B S hS g₀₂ t a₂ h₀₂t
          (sheafOfDifferentials B S hS p)).inv =
      ((QuasiCoherentDescent.pullbackComparison B S hS g₀₁ s a₀ h₀₁s
            (sheafOfDifferentials B S hS p)).hom ≫
          (modulePullback B S hS g₀₁).map
            (sheafOfDifferentialsDescentIsoOfEtale B S hS p hs ht hsq htq).hom ≫
          (QuasiCoherentDescent.pullbackComparison B S hS g₀₁ t a₁ h₀₁t
            (sheafOfDifferentials B S hS p)).inv) ≫
        ((QuasiCoherentDescent.pullbackComparison B S hS g₁₂ s a₁ h₁₂s
            (sheafOfDifferentials B S hS p)).hom ≫
          (modulePullback B S hS g₁₂).map
            (sheafOfDifferentialsDescentIsoOfEtale B S hS p hs ht hsq htq).hom ≫
          (QuasiCoherentDescent.pullbackComparison B S hS g₁₂ t a₂ h₁₂t
            (sheafOfDifferentials B S hS p)).inv)

AlgebraicGeometry.Space.sheafOfDifferentialsDescentIsoOfEtale_canonicalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsDescentOfEtale.lean, line 314. The attribute's comment: “the module α descends to is Ω_{X/Y}: α is the transition isomorphism of the canonical descent datum of Ω_{X/Y} on a presentation π : U ⟶ X which the two étale projections equalize”.

Stacks 04CW. For a presentation π : U ⟶ X of an algebraic space X over Y, with p = π ≫ pX, and étale s, t : R ⟶ U with s ≫ π = t ≫ π inducing the same morphism q : R ⟶ Y, the descent isomorphism α is the transition isomorphism of the canonical descent datum of Ω_{X/Y}: the comparison map c_π : π^*Ω_{X/Y} ⟶ Ω_{U/Y} of Stacks 04CX, namely AlgebraicGeometry.Space.sheafOfDifferentialsMap, carries the canonical comparison of the two inverse images of Ω_{X/Y} to α. When π is étale c_π is an isomorphism, by AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_of_isEtale, so for a presentation the module α descends to is Ω_{X/Y}; étaleness of π is not needed for the identity itself and is not assumed.

The identity α is divided out of, AlgebraicGeometry.Space.canonicalComparison_comp_sheafOfDifferentialsMap, needs no invertibility; the invertibility of c_s and c_t that forms α is derived from étaleness of s and t by Stacks 04CU.

The cocycle condition is the separate statement AlgebraicGeometry.Space.sheafOfDifferentialsDescentIsoOfEtale_cocycle above, and in the scheme-level vocabulary AlgebraicGeometry.Scheme.Hom.differentialsDescentIso_cocycle in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/EtaleDescentDatum.lean. Together with AlgebraicGeometry.Space.sheafOfDifferentialsDescentIsoOfEtale and that cocycle condition, this is the source's remark in the vocabulary of algebraic spaces: the module obtained by gluing Ω_{U/Y} along α is Ω_{X/Y}.

theorem sheafOfDifferentialsDescentIsoOfEtale_canonicalComparison (pX : X ⟶ Y) (π : U ⟶ X)
    (p : U ⟶ Y) {s t : R ⟶ U} (q : R ⟶ Y) (hπ : s ≫ π = t ≫ π) (hπp : π ≫ pX = p)
    (hs : IsEtale B S hS s.hom) (ht : IsEtale B S hS t.hom) (hsq : s ≫ p = q)
    (htq : t ≫ p = q) :
    (QuasiCoherentDescent.canonicalComparison s t π π hπ
          (sheafOfDifferentials B S hS pX)).hom ≫
        (modulePullback B S hS t).map
          (sheafOfDifferentialsMap B S hS π pX p (𝟙 Y) (by rw [hπp, Category.comp_id])) =
      (modulePullback B S hS s).map
          (sheafOfDifferentialsMap B S hS π pX p (𝟙 Y) (by rw [hπp, Category.comp_id])) ≫
        (sheafOfDifferentialsDescentIsoOfEtale B S hS p hs ht hsq htq).hom

Tag 04CX, a lemma

Tag 04CX in the Stacks Project.

AlgebraicGeometry.Space.pushforwardUniversalDerivationHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentials.lean, line 200. The attribute's comment: “the composite f_*d_{X'/Y'} ∘ f♯”.

Stacks 04CX. For a commutative square with top edge f : X' ⟶ X and left edge p' : X' ⟶ Y', the structure map f♯ : 𝒪_X ⟶ f_*𝒪_{X'} followed by the direct image of the universal Y'-derivation d_{X'/Y'}, on underlying sheaves of sets.

noncomputable def pushforwardUniversalDerivationHom (f : X' ⟶ X) (p' : X' ⟶ Y') :
    CategoryTheory.Sheaf.ringSheaf.{u, u, u + 1} (structureRingSheaf B S hS X) ⟶
      CategoryTheory.Sheaf.moduleSheaf.{u, u, u + 1} (structureRingSheaf B S hS X)
        ((modulePushforward B S hS f).obj (sheafOfDifferentials B S hS p'))

AlgebraicGeometry.Space.IsSheafOfDifferentialsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentials.lean, line 212. The attribute's comment: “the characterizing property of c_f on universal local sections”.

Stacks 04CX, the characterizing property of the comparison map c_f : f^*Ω_{X/Y} ⟶ Ω_{X'/Y'} of a commutative square: its adjoint transpose carries the universal differential d_{X/Y}(t) of a local section t of 𝒪_X to d_{X'/Y'}(f♯ t).

def IsSheafOfDifferentialsMap (f : X' ⟶ X) (p : X ⟶ Y) (p' : X' ⟶ Y')
    (c : (modulePullback B S hS f).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p') : Prop

AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentials.lean, line 225. The attribute's comment: “uniqueness of the comparison map c_f”.

Stacks 04CX, uniqueness: at most one morphism f^*Ω_{X/Y} ⟶ Ω_{X'/Y'} of 𝒪_{X'}-modules carries the pulled-back universal differentials to the universal differentials of the pulled-back local sections.

theorem eq_of_isSheafOfDifferentialsMap (f : X' ⟶ X) (p : X ⟶ Y) (p' : X' ⟶ Y')
    {c₁ c₂ : (modulePullback B S hS f).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p'}
    (h₁ : IsSheafOfDifferentialsMap B S hS f p p' c₁)
    (h₂ : IsSheafOfDifferentialsMap B S hS f p p' c₂) : c₁ = c₂

AlgebraicGeometry.Space.pushforwardUniversalDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsMap.lean, line 501. The attribute's comment: “the composite f_*d_{X'/Y'} ∘ f♯ is a Y-derivation”.

Stacks 04CX. For a commutative square with top edge f : X' ⟶ X, the composite D = f_*d_{X'/Y'} ∘ f♯ : 𝒪_X ⟶ f_*Ω_{X'/Y'} is a Y-derivation of 𝒪_X with values in the direct image of the sheaf of differentials of p'.

noncomputable def pushforwardUniversalDerivation (f : X' ⟶ X) (p : X ⟶ Y) (p' : X' ⟶ Y')
    (q : Y' ⟶ Y) (hcomm : f ≫ p = p' ≫ q) :
    PresheafOfModulesOfCommRing.Derivation'
      ((modulePushforward B S hS f).obj (sheafOfDifferentials B S hS p')).val
      (structureSharpInverseImage B S hS p).hom

AlgebraicGeometry.Space.sheafOfDifferentialsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsMap.lean, line 530. The attribute's comment: “the existence of the canonical map”.

Stacks 04CX. The comparison map c_f : f^*Ω_{X/Y} ⟶ Ω_{X'/Y'} of a commutative square of algebraic spaces: the Y-derivation f_*d_{X'/Y'} ∘ f♯ read through Equation 0619.

noncomputable def sheafOfDifferentialsMap (f : X' ⟶ X) (p : X ⟶ Y) (p' : X' ⟶ Y') (q : Y' ⟶ Y)
    (hcomm : f ≫ p = p' ≫ q) :
    (modulePullback B S hS f).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p'

AlgebraicGeometry.Space.isSheafOfDifferentialsMap_sheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsMap.lean, line 544. The attribute's comment: “the canonical map has the characterizing property”.

Stacks 04CX. The comparison map has the characterizing property of Stacks 04CX: its adjoint transpose carries the universal differential d_{X/Y}(t) of a local section t of 𝒪_X to d_{X'/Y'}(f♯ t).

With AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap this identifies AlgebraicGeometry.Space.sheafOfDifferentialsMap with any morphism having that property.

theorem isSheafOfDifferentialsMap_sheafOfDifferentialsMap (f : X' ⟶ X) (p : X ⟶ Y)
    (p' : X' ⟶ Y') (q : Y' ⟶ Y) (hcomm : f ≫ p = p' ≫ q) :
    IsSheafOfDifferentialsMap B S hS f p p'
      (sheafOfDifferentialsMap B S hS f p p' q hcomm)

Tag 05Z7, a lemma

Tag 05Z7 in the Stacks Project.

AlgebraicGeometry.Space.isSheafOfDifferentialsMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsComp.lean, line 699. The attribute's comment: “the composite satisfies the characterization of c_{g ≫ f}”.

Stacks 05Z7, the characterization: for two stacked commutative squares, the composite c_g ∘ g^*c_f of the comparison maps of the inner squares, read through the comparison (g ≫ f)^* ≅ g^*f^* of inverse images of Stacks 03LU, has the characterizing property of Stacks 04CX for the outer square.

theorem isSheafOfDifferentialsMap_comp (f : X' ⟶ X) (g : X'' ⟶ X') (p : X ⟶ Y) (p' : X' ⟶ Y')
    (p'' : X'' ⟶ Y'')
    {cf : (modulePullback B S hS f).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p'}
    {cg : (modulePullback B S hS g).obj (sheafOfDifferentials B S hS p') ⟶
      sheafOfDifferentials B S hS p''}
    (hf : IsSheafOfDifferentialsMap B S hS f p p' cf)
    (hg : IsSheafOfDifferentialsMap B S hS g p' p'' cg) :
    IsSheafOfDifferentialsMap B S hS (g ≫ f) p p''
      ((modulePullbackCompIso B S hS g f).inv.app (sheafOfDifferentials B S hS p) ≫
        (modulePullback B S hS g).map cf ≫ cg)

AlgebraicGeometry.Space.eq_comp_of_isSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsComp.lean, line 723.

Stacks 05Z7. The comparison maps of Stacks 04CX compose: for two stacked commutative squares with top edges g : X'' ⟶ X' and f : X' ⟶ X, the comparison map of the outer square is the comparison map of the inner right square pulled back along g, followed by the comparison map of the inner left square, the two being composable through the comparison (g ≫ f)^* ≅ g^*f^* of Stacks 03LU. Each of the three comparison maps appears through its characterizing property of Stacks 04CX, which determines it uniquely.

theorem eq_comp_of_isSheafOfDifferentialsMap (f : X' ⟶ X) (g : X'' ⟶ X') (p : X ⟶ Y)
    (p' : X' ⟶ Y') (p'' : X'' ⟶ Y'')
    {c : (modulePullback B S hS (g ≫ f)).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p''}
    {cf : (modulePullback B S hS f).obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p'}
    {cg : (modulePullback B S hS g).obj (sheafOfDifferentials B S hS p') ⟶
      sheafOfDifferentials B S hS p''}
    (hc : IsSheafOfDifferentialsMap B S hS (g ≫ f) p p'' c)
    (hf : IsSheafOfDifferentialsMap B S hS f p p' cf)
    (hg : IsSheafOfDifferentialsMap B S hS g p' p'' cg) :
    c = (modulePullbackCompIso B S hS g f).inv.app (sheafOfDifferentials B S hS p) ≫
      (modulePullback B S hS g).map cf ≫ cg

Tag 05Z8, a lemma

Tag 05Z8 in the Stacks Project.

AlgebraicGeometry.Space.triangleDifferentials_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDifferentialsTriangle.lean, line 302. The attribute's comment: “exactness at the right term: the map to Ω_{X/Y} is an epimorphism”.

Stacks 05Z8, exactness at the right term of the transitivity sequence f^*Ω_{Y/B} ⟶ Ω_{X/B} ⟶ Ω_{X/Y} ⟶ 0: the canonical map Ω_{X/B} ⟶ Ω_{X/Y} is an epimorphism.

Two morphisms out of Ω_{X/Y} agreeing after it agree on every d_{X/Y}(t), because d_{X/B}(t) is carried to d_{X/Y}(t), so they are equal by the uniqueness half of Stacks 04CT.

theorem triangleDifferentials_epi (f : X ⟶ Y) (g : Y ⟶ Z) :
    Epi (toRelativeDifferentials B S hS f g)

AlgebraicGeometry.Space.triangleDifferentials_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDifferentialsTriangle.lean, line 506. The attribute's comment: “the composite of the two maps is zero, and exactness at the middle term Ω_{X/B}”.

Stacks 05Z8, the two clauses of the transitivity sequence f^*Ω_{Y/B} ⟶ Ω_{X/B} ⟶ Ω_{X/Y} ⟶ 0 that concern its left half: the composite of the two maps is zero, and the resulting short complex is exact at Ω_{X/B}. Together with AlgebraicGeometry.Space.triangleDifferentials_epi, which is exactness at Ω_{X/Y}, this is the exactness of the whole sequence.

Both come from AlgebraicGeometry.Space.isColimitCokernelCoforkToRelativeDifferentials: the cokernel cofork carries the vanishing of the composite, and CategoryTheory.ShortComplex.exact_of_g_is_cokernel turns the colimit into exactness in the middle. The homology of the short complex is formed in the abelian category of 𝒪_X-modules; the instance that makes it abelian is HasSheafify for abelian sheaves on the small étale site, which instance search does not find at the projection (AlgebraicGeometry.Space.smallEtaleRingedSite B S hS X.1 X.2).J of the ringed site, exactly as for AlgebraicGeometry.Space.smallEtaleRingedSite_hasWeakSheafify.

theorem triangleDifferentials_exact (f : X ⟶ Y) (g : Y ⟶ Z) :
    ∃ h : pullbackDifferentialsMap B S hS f g ≫ toRelativeDifferentials B S hS f g = 0,
      (ShortComplex.mk _ _ h).Exact

Tag 05Z9, a lemma

Tag 05Z9 in the Stacks Project.

AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsImmersion.lean, line 331. The attribute's comment: “the vanishing Ω_{X/Y} = 0, from local surjectivity of f♯; the gap to the source's hypothesis is that an immersion of algebraic spaces has locally surjective structure map, which is the inverse-image form of the surjectivity clause of 03MB”.

Stacks 05Z9, with local surjectivity of the structure map in place of the hypothesis that f is an immersion. If f♯ : f⁻¹𝒪_Y ⟶ 𝒪_X is locally surjective then Ω_{X/Y} is zero.

Ω_{X/Y} corepresents the functor of Y-derivations, and by AlgebraicGeometry.Space.derivation_eq_of_isLocallySurjective that functor takes at most one value at each sheaf of 𝒪_X-modules; so the identity and the zero endomorphism of Ω_{X/Y} both factor the same derivation and are therefore equal.

An immersion has locally surjective structure map, by AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage_of_isImmersion, which is how AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isImmersion_unconditional reaches the source's statement.

theorem isZero_sheafOfDifferentials_of_isLocallySurjective (f : X ⟶ Y)
    (hsharp : Presheaf.IsLocallySurjective (SmallEtale.topology B S hS X.1)
      (structureSharpInverseImage B S hS f).hom) :
    IsZero (sheafOfDifferentials B S hS f)

AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsImmersion.lean, line 360. The attribute's comment: “the source's statement, carrying local surjectivity of the structure map of an immersion (the inverse-image form of the surjectivity clause of 03MB) as hsharp, quantified over all immersions of algebraic spaces over S”.

Stacks 05Z9. If f : X ⟶ Y is an immersion of algebraic spaces over S then Ω_{X/Y} is zero.

The hypothesis hsharp is the one input not proved in this development: the structure map f♯ : f⁻¹𝒪_Y ⟶ 𝒪_X of an immersion of algebraic spaces is locally surjective. It is the inverse-image form of the surjectivity clause of Stacks 03MB, which AlgebraicGeometry.Space.isLocallySurjective_structureSharp supplies only in the direct-image form 𝒪_Y ⟶ f_*𝒪_X and only for closed immersions, and it is carried here universally quantified over all immersions of algebraic spaces over S.

That input is no longer unproved: it is AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage_of_isImmersion above, so the hypothesis-free form of this statement is AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isImmersion_unconditional.

theorem isZero_sheafOfDifferentials_of_isImmersion
    (hsharp : ∀ (X' Y' : AlgebraicSpaces B S hS) (g : X' ⟶ Y'), IsImmersion B S hS g.hom →
      Presheaf.IsLocallySurjective (SmallEtale.topology B S hS X'.1)
        (structureSharpInverseImage B S hS g).hom)
    (f : X ⟶ Y) (hf : IsImmersion B S hS f.hom) :
    IsZero (sheafOfDifferentials B S hS f)

AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isImmersion_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsImmersion.lean, line 379. The attribute's comment: “the source's statement: the sheaf of differentials of an immersion of algebraic spaces over S is a zero object, with no hypothesis beyond the immersion”.

Stacks 05Z9. If f : X ⟶ Y is an immersion of algebraic spaces over S then Ω_{X/Y} is zero, with no hypothesis beyond the immersion.

The structure map f♯ : f⁻¹𝒪_Y ⟶ 𝒪_X of an immersion is locally surjective (AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage_of_isImmersion), and local surjectivity forces the vanishing (AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isLocallySurjective). This is AlgebraicGeometry.Space.isZero_sheafOfDifferentials_of_isImmersion with its hypothesis hsharp discharged.

theorem isZero_sheafOfDifferentials_of_isImmersion_unconditional (f : X ⟶ Y)
    (hf : IsImmersion B S hS f.hom) :
    IsZero (sheafOfDifferentials B S hS f)

Tag 05ZA, a lemma

Tag 05ZA in the Stacks Project.

AlgebraicGeometry.Space.conormalSequenceFirstMap_comp_pullbackDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceComplex.lean, line 236. The attribute's comment: “the composite of the two arrows is zero, so the sequence 𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} is a complex, for a closed subspace. Unconditional”.

Stacks 05ZA, the composite of the two arrows is zero. For a closed subspace Z of an algebraic space X over Bb, with inclusion i : Z ⟶ X, the sequence
  𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb}
is a complex.

This is AlgebraicGeometry.Space.conormalSequenceIdealPullbackMap_comp_pullbackDifferentialsMap with the source of the first arrow read as the conormal module, which it is by AlgebraicGeometry.Space.conormalModule_eq.

theorem conormalSequenceFirstMap_comp_pullbackDifferentialsMap
    (Z : ClosedSubspaces B S hS X.1) (b : X ⟶ Bb) :
    conormalSequenceFirstMap B S hS Z b ≫
        pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X Z) b = 0

AlgebraicGeometry.Space.conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceCompositeZero.lean, line 316. The attribute's comment: “the composite of the two arrows is zero, at a subspace inclusion, with the first arrow read out of the conormal module 𝒞_{Z/X} of 04CN. The same clause at the first arrow of an arbitrary immersion is conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero”.

Stacks 05ZA, the composite of the two arrows is zero, read at AlgebraicGeometry.Space.conormalSequenceFirstMap, that is with the source of the first arrow written as the conormal module 𝒞_{Z/X} of Stacks 04CN rather than as i^*𝓘. The two readings are the same morphism, by AlgebraicGeometry.Space.conormalModule_eq.

This is the shape in which the clause is consumed: it is the hzero hypothesis carried by AlgebraicGeometry.Space.thickeningConormalSequence_exact of Stacks 060F and by AlgebraicGeometry.Space.epi_thickeningConormalFirstMap of Stacks 060G.

theorem conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero
    (Z : ClosedSubspaces B S hS Y.1) (b : Y ⟶ Bb) :
    conormalSequenceFirstMap B S hS Z b ≫
      pullbackDifferentialsMap B S hS (subspaceInclusion B S hS Y Z) b = 0

AlgebraicGeometry.Space.conormalSequenceIdealDifferential_val_app_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceDifferentials.lean, line 690. The attribute's comment: “the first arrow is induced by d_{X/B}: the transpose of the first arrow across i^* ⊣ i_* carries a section of the defining ideal sheaf to the universal differential of that section, followed by the unit”.

Stacks 05ZA, "the first arrow is induced by d_{X/B}". The first arrow is by definition the transpose across i^* ⊣ i_* of AlgebraicGeometry.Space.conormalSequenceIdealDifferential, and that transpose carries a local section a of the defining ideal sheaf of Z to D(a), where D is d_{X/B} followed by the unit of the adjunction — which is what AlgebraicGeometry.Space.conormalSequenceUnitDerivation is, by its definition. This equation is the whole of the arrow's dependence on d_{X/B}; since the transposition is a bijection, it determines the arrow.

theorem conormalSequenceIdealDifferential_val_app_apply (Z : ClosedSubspaces B S hS X.1)
    (b : X ⟶ Bb) (U : (SmallEtale B S hS X.1)ᵒᵖ)
    (x : (definingIdealSheaf B S hS X Z).toSheafOfModules.val.obj U) :
    ((conormalSequenceIdealDifferential B S hS Z b).val.app U).hom x =
      (conormalSequenceUnitDerivation B S hS Z b).d x.1

AlgebraicGeometry.Space.conormalSequenceFirstMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceDifferentials.lean, line 733. The attribute's comment: “the canonical first arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/B} induced by d_{X/B}, at a subspace inclusion. The same arrow at an arbitrary immersion is conormalSequenceFirstMapOfImmersion”.

Stacks 05ZA, the canonical first arrow. For a subspace Z of an algebraic space X over B, with inclusion i : Z ⟶ X, the arrow
  𝒞_{Z/X} ⟶ i^*Ω_{X/B}
induced by d_{X/B}. It is AlgebraicGeometry.Space.conormalSequenceIdealPullbackMap with its source read as the conormal module, which it is by AlgebraicGeometry.Space.conormalModule_eq.

noncomputable def conormalSequenceFirstMap (Z : ClosedSubspaces B S hS X.1) (b : X ⟶ Bb) :
    conormalModule B S hS X Z ⟶
      (modulePullback B S hS (subspaceInclusion B S hS X Z)).obj
        (sheafOfDifferentials B S hS b)

AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceDifferentialsEpi.lean, line 113. The attribute's comment: “exactness at the right term: the second arrow i^*Ω_{X/B} ⟶ Ω_{Z/B} is an epimorphism, carrying local surjectivity of i♯ : i⁻¹𝒪_X ⟶ 𝒪_Z (the inverse-image form of the surjectivity clause of 03MB) as hsharp”.

Stacks 05ZA, exactness at the right term, under local surjectivity of the structure map i♯ : i⁻¹𝒪_X ⟶ 𝒪_Z. The comparison map c_i : i^*Ω_{X/B} ⟶ Ω_{Z/B} of Stacks 04CX is an epimorphism, so the conormal sequence of i ends in zero.

Left-cancellation is checked directly: given g, g' with equal composites, AlgebraicGeometry.Space.sheafOfDifferentialsMap_comp_eq_iff makes them agree on the universal differentials of the sections in the image of i♯; local surjectivity makes every local section of 𝒪_Z locally of that form, so the two values agree on a covering sieve and hence are equal, the target being a sheaf; and AlgebraicGeometry.Space.sheafOfDifferentials_hom_ext turns that into g = g'.

theorem epi_pullbackDifferentialsMap_of_isLocallySurjective (i : X ⟶ Y) (b : Y ⟶ Bb)
    (hsharp : Presheaf.IsLocallySurjective (SmallEtale.topology B S hS X.1)
      (structureSharpInverseImage B S hS i).hom) :
    Epi (pullbackDifferentialsMap B S hS i b)

AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceEpiImmersion.lean, line 71. The attribute's comment: “exactness at the right term: the second arrow i^*Ω_{X/B} ⟶ Ω_{Z/B} is an epimorphism for an immersion, with no hypothesis beyond the immersion”.

Stacks 05ZA, exactness at the right term, for an immersion. For an immersion i : X ⟶ Y of algebraic spaces over B and a structure morphism b : Y ⟶ B, the second arrow i^*Ω_{Y/B} ⟶ Ω_{X/B} of the conormal sequence — the comparison map of Stacks 04CX for the square over the identity of B — is an epimorphism.

This is AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_of_isLocallySurjective with its hypothesis hsharp discharged by AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage_of_isImmersion.

theorem epi_pullbackDifferentialsMap_of_isImmersion (i : X ⟶ Y) (b : Y ⟶ Bb)
    (hi : IsImmersion B S hS i.hom) :
    Epi (pullbackDifferentialsMap B S hS i b)

AlgebraicGeometry.Space.conormalSequenceFirstMapOfImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionFirstMap.lean, line 165. The attribute's comment: “the canonical first arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/B} induced by d_{X/B}, for an arbitrary immersion”.

Stacks 05ZA, the canonical first arrow, for an arbitrary immersion. For an immersion i : Z ⟶ X of algebraic spaces over B with structure morphism b : X ⟶ B, the arrow
  𝒞_{Z/X} ⟶ i^*Ω_{X/B}
induced by d_{X/B}.

It is AlgebraicGeometry.Space.kernelConormalFirstMap, the arrow built from the kernel ideal sheaf of i by restricting d_{X/B} followed by the unit of i^* ⊣ i_* to it, read out of the conormal module: AlgebraicGeometry.Space.conormalAlgebra_piece_one says the source of that arrow is the degree-one piece of the conormal algebra of i, and AlgebraicGeometry.Space.conormalAlgebraOfImmersionPieceIso identifies that piece with the conormal module of the immersion.

noncomputable def conormalSequenceFirstMapOfImmersion (i : Z ⟶ X)
    (hi : IsImmersion B S hS i.hom) (b : X ⟶ Bb) :
    immersionConormalModule B S hS i hi ⟶
      (modulePullback B S hS i).obj (sheafOfDifferentials B S hS b)

AlgebraicGeometry.Space.conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionFirstMap.lean, line 181. The attribute's comment: “the composite 𝒞_{Z/X} ⟶ i^*Ω_{X/B} ⟶ Ω_{Z/B} of the two arrows is zero, for an arbitrary immersion”.

Stacks 05ZA, the composite of the two arrows is zero, for an arbitrary immersion. The first arrow 𝒞_{Z/X} ⟶ i^*Ω_{X/B} followed by the second arrow i^*Ω_{X/B} ⟶ Ω_{Z/B}, the comparison map of Stacks 04CX for the square over the identity of B, is the zero morphism.

The first arrow factors through AlgebraicGeometry.Space.kernelConormalFirstMap, for which the clause is AlgebraicGeometry.Space.kernelConormalFirstMap_comp_pullbackDifferentialsMap_eq_zero.

theorem conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero (i : Z ⟶ X)
    (hi : IsImmersion B S hS i.hom) (b : X ⟶ Bb) :
    conormalSequenceFirstMapOfImmersion B S hS i hi b ≫
      pullbackDifferentialsMap B S hS i b = 0

AlgebraicGeometry.Space.conormalSequenceOfImmersion_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionKernelExactness.lean, line 307. The attribute's comment: “exactness at the middle term i^*Ω_{X/B}: the second arrow is a cokernel of the first, for an arbitrary immersion i : Z ⟶ X, at the tag's own first arrow conormalSequenceFirstMapOfImmersion. Unconditional: the open-subspace reduction of the tag's own proof is carried out, through the factorisation of 04CE and the comparison of the two first arrows across the étale inclusion of the ambient open”.

Stacks 05ZA, exactness at the middle term, for an arbitrary immersion. For an immersion i : Z ⟶ X of algebraic spaces over B with structure morphism b : X ⟶ B, the sequence
  𝒞_{Z/X} ⟶ i^*Ω_{X/B} ⟶ Ω_{Z/B}
built from the canonical first arrow AlgebraicGeometry.Space.conormalSequenceFirstMapOfImmersion and the second arrow AlgebraicGeometry.Space.pullbackDifferentialsMap is exact at i^*Ω_{X/B}.

No hypothesis beyond the immersion is carried. It is AlgebraicGeometry.Space.conormalSequenceKernel_exact_of_isImmersion fed to AlgebraicGeometry.Space.conormalSequenceOfImmersion_exact_of_kernelConormalFirstMap, which reads the first arrow out of the conormal module 𝒞_{Z/X} of [Stacks Project, Tag 04CN] rather than out of the kernel ideal sheaf; the two differ by the isomorphism AlgebraicGeometry.Space.conormalModuleOfImmersionKernelPullbackIso of the left-hand terms.

theorem conormalSequenceOfImmersion_exact (i : Z ⟶ X) (hi : IsImmersion B S hS i.hom)
    (b : X ⟶ Bb) :
    (ShortComplex.mk _ _
      (conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero
        B S hS i hi b)).Exact

AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_subspaceInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceMiddleExactness.lean, line 335. The attribute's comment: “exactness at the right term: the second arrow i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} is an epimorphism. UNCONDITIONAL for a closed subspace: the local surjectivity of i♯ : i⁻¹𝒪_X ⟶ 𝒪_Z that epi_pullbackDifferentialsMap_of_isLocallySurjective carries as hsharp is isLocallySurjective_structureSharpInverseImage, the inverse-image form of the surjectivity clause of 03MB, applied to the closed immersion Z.2.2”.

Stacks 05ZA, exactness at the right term, unconditionally for a closed subspace. The second arrow i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} of the sequence of Stacks 05ZA is an epimorphism.

AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_of_isLocallySurjective proves this from local surjectivity of i♯ : i⁻¹𝒪_X ⟶ 𝒪_Z, which that module's implementation notes record as carried; it is not carried any more, and for a closed immersion it is proved — AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage of StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionStructureSharpInverseImage.lean, the inverse-image form of the surjectivity clause of Stacks 03MB — and the inclusion of a closed subspace is a closed immersion by Z.2.2.

theorem epi_pullbackDifferentialsMap_subspaceInclusion :
    Epi (pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X Z) b)

AlgebraicGeometry.Space.conormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceMiddleExactnessAt.lean, line 492. The attribute's comment: “exactness at the middle term i^*Ω_{X/B}: the second arrow is a cokernel of the first, at a subspace inclusion Z ⊆ X — the case the tag's own proof reduces the immersion case to. Unconditional: stated at the canonical inclusion and at the registered first arrow conormalSequenceFirstMap, with no hypothesis beyond the tag's own data. The general form with the inclusion an explicit parameter is conormalSequenceAt_exact, whose three hypotheses this discharges — the two halves of mem_definingIdealAt_iff and the closed-immersion clause of 02YU(4); the inclusion is left a parameter there for the reason recorded in ConormalSequenceInclusionParameter.lean. The same clause at the first arrow of an arbitrary immersion, over the ambient open of 04CE, is conormalSequenceOfImmersion_exact”.

Stacks 05ZA, exactness at the middle term, unconditionally. For a subspace Z ⊆ X of an algebraic space over B with structure morphism b : X ⟶ Bb, the short complex
  𝒞_{Z/X} ⟶ i^*Ω_{X/B} ⟶ Ω_{Z/B}
built from the canonical first arrow AlgebraicGeometry.Space.conormalSequenceFirstMap and the second arrow AlgebraicGeometry.Space.pullbackDifferentialsMap is exact at i^*Ω_{X/B}.

No hypothesis is carried. This is AlgebraicGeometry.Space.conormalSequenceAt_exact_subspaceInclusion, read with the source of the first arrow written as the conormal module 𝒞_{Z/X} of Stacks 04CN rather than as i^*𝓘; the two readings are the same morphism, by AlgebraicGeometry.Space.conormalModule_eq.

The transport is through CategoryTheory.ShortComplex.exact_iff_of_iso, with every component of the isomorphism written out, rather than by ascribing the statement directly; the implementation notes of this file record what each of the other routes costs.

theorem conormalSequence_exact (Z : ClosedSubspaces B S hS X.1) (b : X ⟶ Bb) :
    (ShortComplex.mk _ _
      (conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero B S hS Z b)).Exact

AlgebraicGeometry.Space.exact_conormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceThickeningDescent.lean, line 409. The attribute's comment: “exactness at the middle term: the short complex 𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} is exact at i^*Ω_{X/Bb}, for a closed subspace”.

Stacks 05ZA, exactness at the middle term, unconditionally for a closed subspace. The short complex 𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} of [Stacks Project, Tag 05ZA] is exact at i^*Ω_{X/Bb}.

This is AlgebraicGeometry.Space.exact_conormalSequence_of_exists_pushforwardDerivation, whose hypothesis hdesc is AlgebraicGeometry.Space.exists_conormalPushforwardDerivation_eq above. Nothing beyond the inclusion i being a closed immersion is used: the one step that used to carry a thickening hypothesis, the vanishing of the transpose of a derivation on the sections killed by i^♯ in inverse-image form, is proved for an arbitrary closed subspace in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceThickeningKernelVanishing.lean from the fibre-square presentation of the defining ideal sheaf.

Together with AlgebraicGeometry.Space.epi_pullbackDifferentialsMap_subspaceInclusion, which is the clause at the right, this is the whole of 05ZA for the closed immersions this development models — the source asserts exactness at i^*Ω_{X/Bb} and at Ω_{Z/Bb} and nothing on the left.

theorem exact_conormalSequence :
    (ShortComplex.mk _ _
      (conormalSequenceFirstMap_comp_pullbackDifferentialsMap B S hS Z b)).Exact

Declarations registered for the tag:

AlgebraicGeometry.Space.pullbackDifferentialsMap, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSecondMap.lean, line 32 (StacksFrontier): “the canonical second arrow i^*Ω_{X/B} ⟶ Ω_{Z/B}, the comparison map of 04CX for the square over the identity of the base”.

Tag 05ZB, a lemma

Tag 05ZB in the Stacks Project.

AlgebraicGeometry.Space.nonempty_conormalSequenceOfImmersion_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionSplitExact.lean, line 216. The attribute's comment: “the global clause at an arbitrary immersion i : Z ⟶ X having a left inverse over B: the conormal sequence of 05ZA is split exact, that is, it admits a CategoryTheory.ShortComplex.Splitting, so its first arrow is a monomorphism, it is exact at the middle term i^*Ω_{X/B} and its second arrow is a split epimorphism. Stated at the tag's own first arrow conormalSequenceFirstMapOfImmersion out of the conormal module of 04CN, with no hypothesis beyond IsImmersion and the tag's own left inverse over B. The source's open-subspace reduction is carried out: the immersion is factored through the open subspace of 04CE, where it is closed and the restricted left inverse makes nonempty_conormalSequenceKernel_splitting apply, and the splitting is transported back along the comparison of the two sequences across the étale inclusion of that open”.

Stacks 05ZB, the global clause, at an arbitrary immersion. Let i : Z ⟶ X be an immersion of algebraic spaces over Bb with structure morphism b : X ⟶ Bb, and let g : X ⟶ Z be a left inverse of i over Bb. Then the conormal sequence of [Stacks Project, Tag 05ZA]
  0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} ⟶ 0
is split exact: it admits a CategoryTheory.ShortComplex.Splitting, that is a retraction of the first arrow and a section of the second summing to the identity — so in particular the first arrow is a monomorphism, the sequence is exact at its middle term and the second arrow is a split epimorphism.

The sequence is the one the tag states: the first arrow is AlgebraicGeometry.Space.conormalSequenceFirstMapOfImmersion, whose source is the conormal module 𝒞_{Z/X} of [Stacks Project, Tag 04CN]. Nothing is assumed beyond the immersion and the left inverse over Bb, which are the tag's own data: the splitting at the kernel-ideal reading is AlgebraicGeometry.Space.nonempty_conormalSequenceKernel_splitting_of_isImmersion, and the two short complexes differ by the isomorphism AlgebraicGeometry.Space.conormalModuleOfImmersionKernelPullbackIso of their left-hand terms and nothing else.

theorem nonempty_conormalSequenceOfImmersion_splitting (i : Z ⟶ X)
    (hi : IsImmersion B S hS i.hom) (b : X ⟶ Bb) (g : X ⟶ Z) (hg : i ≫ g = 𝟙 Z)
    (hgb : g ≫ i ≫ b = b) :
    Nonempty (ShortComplex.mk _ _
      (conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero
        B S hS i hi b)).Splitting

AlgebraicGeometry.Space.nonempty_conormalSequenceOfImmersion_splitting_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionSplitExact.lean, line 263. The attribute's comment: “the étale-local clause at an arbitrary immersion: for an étale φ : W' ⟶ W, an immersion i' : Zs' ⟶ W' and an étale a : Zs' ⟶ Zs with i' ≫ φ = a ≫ i, the immersion i' having a left inverse over B, the restricted conormal sequence of 05ZA is split exact — it admits a CategoryTheory.ShortComplex.Splitting, so its first arrow is a monomorphism, it is exact at the middle term and its second arrow is a split epimorphism — and the inverse image along a of the second arrow of the unrestricted sequence is a split epimorphism too, which is where the étale-localization clause of 04CU is consumed. Stated at the tag's own first arrow conormalSequenceFirstMapOfImmersion, with IsImmersion of i' and the étale-local data of the tag the only hypotheses; the unrestricted i is an arbitrary morphism”.

Stacks 05ZB, the étale-local clause, at an arbitrary immersion. Let i : Zs ⟶ W be a morphism of algebraic spaces over Bb with structure morphism b : W ⟶ Bb, let φ : W' ⟶ W be étale, let i' : Zs' ⟶ W' be an arbitrary immersion and a : Zs' ⟶ Zs étale with i' ≫ φ = a ≫ i, and let g' : W' ⟶ Zs' be a left inverse of i' over Bb. Then

the restricted conormal sequence, the sequence of [Stacks Project, Tag 05ZA] at i' over φ ≫ b, is split exact;

the inverse image along a of the second arrow of the unrestricted sequence is a split epimorphism.

Étaleness is assumed of φ and of a separately rather than Zs' being assumed to be the preimage of Zs, which is weaker: in the situation of the source a is a base change of φ. The unrestricted morphism i is free: the split epimorphism clause is AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etale, which assumes nothing of i or i', and the restricted sequence's splitting is AlgebraicGeometry.Space.nonempty_conormalSequenceOfImmersion_splitting at i'.

theorem nonempty_conormalSequenceOfImmersion_splitting_of_etale (i : Zs ⟶ W) (b : W ⟶ Bb)
    (φ : W' ⟶ W) (hφ : IsEtale B S hS φ.hom) (i' : Zs' ⟶ W')
    (hi' : IsImmersion B S hS i'.hom) (a : Zs' ⟶ Zs) (ha : IsEtale B S hS a.hom)
    (hsq : i' ≫ φ = a ≫ i) (g' : W' ⟶ Zs') (hg' : i' ≫ g' = 𝟙 Zs')
    (hg'b : g' ≫ i' ≫ φ ≫ b = φ ≫ b) :
    Nonempty (ShortComplex.mk _ _
          (conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero B S hS i'
            hi' (φ ≫ b))).Splitting ∧
      IsSplitEpi ((modulePullback B S hS a).map (pullbackDifferentialsMap B S hS i b))

AlgebraicGeometry.Space.nonempty_map_conormalSequenceOfImmersion_splitting_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceImmersionSplitExactEtaleLocal.lean, line 723. The attribute's comment: “the étale-local clause in full: if i étale locally has a left inverse (on an étale covering {X_k → X} with Z_k = Z ×_X X_k), the restriction to each Z_k of the whole conormal sequence of i is split exact”.

Stacks 05ZB, the étale-local clause in full. Let i : Z ⟶ X be an immersion of algebraic spaces over Bb with structure morphism b : X ⟶ Bb, and assume that i étale locally has a left inverse: there is an étale covering {φ_k : X_k ⟶ X} of X (Stacks 041E: every φ_k étale, the family jointly surjective) such that, for each k, in a cartesian square
Z_k --i_k--→ X_k
 |            |
a_k          φ_k
 ↓            ↓
 Z  ---i---→  X
presenting Z_k as Z ×_X X_k, the immersion i_k has a left inverse g_k over Bb. Then for every k the restriction to Z_k of the conormal sequence of [Stacks Project, Tag 05ZA] of i — the image under a_k^* of the whole short complex
  𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb},
conormal term and first arrow included — admits a CategoryTheory.ShortComplex.Splitting. So the restricted first arrow a_k^*𝒞_{Z/X} ⟶ a_k^*i^*Ω_{X/Bb} is a monomorphism, the restricted sequence is exact at its middle term, and its second arrow is a split epimorphism.

Each member is AlgebraicGeometry.Space.nonempty_map_conormalSequenceOfImmersion_splitting_of_isPullback.

theorem nonempty_map_conormalSequenceOfImmersion_splitting_of_isEtaleCovering (i : Z ⟶ X)
    (hi : IsImmersion B S hS i.hom) (b : X ⟶ Bb) {ι : Type*}
    {Xk Zk : ι → AlgebraicSpaces B S hS} (φ : ∀ k, Xk k ⟶ X)
    (hφ : IsEtaleCovering B S hS (fun k ↦ (Xk k).1) (fun k ↦ (φ k).hom))
    (ik : ∀ k, Zk k ⟶ Xk k) (a : ∀ k, Zk k ⟶ Z) (hpb : ∀ k, IsPullback (ik k) (a k) (φ k) i)
    (g : ∀ k, Xk k ⟶ Zk k) (hg : ∀ k, ik k ≫ g k = 𝟙 (Zk k))
    (hgb : ∀ k, g k ≫ ik k ≫ φ k ≫ b = φ k ≫ b) (k : ι) :
    Nonempty ((ShortComplex.mk _ _
      (conormalSequenceFirstMapOfImmersion_comp_pullbackDifferentialsMap_eq_zero
        B S hS i hi b)).map (modulePullback B S hS (a k))).Splitting

AlgebraicGeometry.Space.conormalSequence_splitExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitExact.lean, line 681. The attribute's comment: “the global clause at the inclusion of a bundled subspace Z ⊆ X having a left inverse over B: the conormal sequence of 05ZA is exact at its middle term i^*Ω_{X/B} and its second arrow is a split epimorphism, hence also an epimorphism, which is exactness at the right term; the vanishing of the composite is the short complex itself. Stated at the canonical inclusion and at the registered first arrow conormalSequenceFirstMap, with no hypothesis beyond the left inverse, which is the tag's own datum. The injectivity clause at the left end of the sequence is the subject of nonempty_conormalSequence_splitting_iff_mono, which shows it equivalent to the full ShortComplex.Splitting. The general form with the inclusion an explicit parameter is conormalSequenceAt_splitExact, and the same clause at an arbitrary closed immersion, with no bundled subspace anywhere, is conormalSequenceKernel_splitExact_of_isClosedImmersion; at the generality the tag is stated at, an arbitrary immersion with a left inverse over B, the sequence is split exact in full by nonempty_conormalSequenceOfImmersion_splitting”.

Stacks 05ZB, the global clause, unconditionally. Let Z ⊆ X be a closed subspace of an algebraic space over Bb with structure morphism b : X ⟶ Bb, and let g : X ⟶ Z be a left inverse over Bb of the inclusion of Z. Then the conormal sequence of Stacks 05ZA
  𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} ⟶ 0
is exact at its middle term and its second arrow is a split epimorphism.

No hypothesis beyond the left inverse is carried, and the sequence is the one Stacks 05ZA states: the first arrow is AlgebraicGeometry.Space.conormalSequenceFirstMap, whose source is the conormal module 𝒞_{Z/X} of Stacks 04CN. The exactness clause is AlgebraicGeometry.Space.conormalSequence_exact, which is AlgebraicGeometry.Space.conormalSequenceAt_splitExact's first component at the canonical inclusion with its three hypotheses discharged — the two halves of AlgebraicGeometry.Space.mem_definingIdealAt_iff and part (4) of Stacks 02YU — and read at conormalSequenceFirstMap; the splitness clause is unchanged by that reading, since AlgebraicGeometry.Space.pullbackDifferentialsMap does not mention the first arrow.

The hypothesis is satisfiable: at the top closed subspace the inclusion is an isomorphism, and its inverse is a left inverse over Bb; the retraction is written out in the proof of AlgebraicGeometry.Space.isZero_conormalModule_top of StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheaf.lean.

theorem conormalSequence_splitExact (Z : ClosedSubspaces B S hS X.1) (b : X ⟶ Bb)
    (g : X ⟶ (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))
    (hg : subspaceInclusion B S hS X Z ≫ g = 𝟙 (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))
    (hgb : g ≫ subspaceInclusion B S hS X Z ≫ b = b) :
    (ShortComplex.mk _ _
          (conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero B S hS Z b)).Exact ∧
      IsSplitEpi (pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X Z) b)

AlgebraicGeometry.Space.conormalSequence_splitExact_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitExact.lean, line 756. The attribute's comment: “the étale-local clause: for closed subspaces Z ⊆ X and Z' ⊆ X' joined by an étale φ : X' ⟶ X and an étale a : Z' ⟶ Z over it, with the inclusion of Z' admitting a left inverse over B, the restricted conormal sequence of 05ZA is exact at its middle term and its second arrow is a split epimorphism, and so is the inverse image along a of the second arrow of the unrestricted sequence — which is where the étale-localization clause of 04CU is consumed. Stated at the two canonical inclusions and at the registered first arrow conormalSequenceFirstMap, with no hypothesis beyond the étale-local data of the tag. As in the global clause, the injectivity clause at the left end of the sequence is the subject of nonempty_conormalSequence_splitting_iff_mono. The general form with both inclusions explicit parameters is conormalSequenceAt_splitExact_of_etale”.

Stacks 05ZB, the étale-local clause, unconditionally. Let Z ⊆ X and Z' ⊆ X' be closed subspaces, let φ : X' ⟶ X be étale, let a : Z' ⟶ Z be étale with i' ≫ φ = a ≫ i for the two inclusions, and let g' : X' ⟶ Z' be a left inverse of the inclusion of Z' over Bb. Then

the restricted conormal sequence, the sequence of Stacks 05ZA at Z' ⊆ X' over φ ≫ b, is exact at its middle term, and its second arrow is a split epimorphism;

the inverse image along a of the second arrow of the unrestricted sequence is a split epimorphism too.

No hypothesis beyond the étale-local data of the tag is carried: φ, a and the square they sit in, and the left inverse g'. The first clause is AlgebraicGeometry.Space.conormalSequence_exact at Z' ⊆ X' over φ ≫ b, so it is stated at the registered first arrow AlgebraicGeometry.Space.conormalSequenceFirstMap with the source read as 𝒞_{Z'/X'}; the other two are the corresponding clauses of AlgebraicGeometry.Space.conormalSequenceAt_splitExact_of_etale, which do not mention the first arrow. As there, étaleness is assumed of φ and of a separately rather than Z' being assumed to be the preimage of Z, which is weaker: in the situation of the source a is a base change of φ.

theorem conormalSequence_splitExact_of_etale (Z : ClosedSubspaces B S hS X.1)
    (Z' : ClosedSubspaces B S hS X'.1) (b : X ⟶ Bb) (φ : X' ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (a : (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))
    (ha : IsEtale B S hS a.hom)
    (hsq : subspaceInclusion B S hS X' Z' ≫ φ = a ≫ subspaceInclusion B S hS X Z)
    (g' : X' ⟶ (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hg' : subspaceInclusion B S hS X' Z' ≫ g' =
      𝟙 (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hg'b : g' ≫ subspaceInclusion B S hS X' Z' ≫ φ ≫ b = φ ≫ b) :
    (ShortComplex.mk _ _
          (conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero B S hS Z'
            (φ ≫ b))).Exact ∧
        IsSplitEpi (pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X' Z')
          (φ ≫ b)) ∧
      IsSplitEpi ((modulePullback B S hS a).map
        (pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X Z) b))

AlgebraicGeometry.Space.nonempty_conormalSequence_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitMono.lean, line 830. The attribute's comment: “the global clause in full at the inclusion of a bundled subspace Z ⊆ X of an algebraic space over B, that inclusion having a left inverse over B: the conormal sequence of 05ZA is split exact, that is, it admits a CategoryTheory.ShortComplex.Splitting: the first arrow conormalSequenceFirstMap is a monomorphism, the sequence is exact at the middle term i^*Ω_{X/B}, and the second arrow is a split epimorphism. Stated at the canonical inclusion and at the registered first arrow, with no hypothesis beyond the tag's own left inverse over B. The same clause at an arbitrary closed immersion, with no bundled subspace anywhere, is nonempty_conormalSequenceKernel_splitting, and at the generality the tag is stated at, an arbitrary immersion with a left inverse over B, it is nonempty_conormalSequenceOfImmersion_splitting”.

Stacks 05ZB, the global clause in full. Let Z ⊆ X be a closed subspace of an algebraic space over Bb with structure morphism b : X ⟶ Bb, and let g : X ⟶ Z be a left inverse over Bb of its inclusion. Then the conormal sequence of Stacks 05ZA
  0 ⟶ 𝒞_{Z/X} ⟶ i^*Ω_{X/Bb} ⟶ Ω_{Z/Bb} ⟶ 0
is split exact: it admits a CategoryTheory.ShortComplex.Splitting, that is a retraction of the first arrow and a section of the second summing to the identity — so in particular the first arrow is a monomorphism, the sequence is exact at its middle term and the second arrow is a split epimorphism.

The exactness and the splitness of the second arrow are AlgebraicGeometry.Space.conormalSequence_splitExact; what completes the tag is the injectivity of the first arrow, AlgebraicGeometry.Space.mono_conormalSequenceFirstMap, which AlgebraicGeometry.Space.nonempty_conormalSequence_splitting_iff_mono turns into the full splitting.

theorem nonempty_conormalSequence_splitting (b : X ⟶ Bb)
    (hgb : g ≫ subspaceInclusion B S hS X Z ≫ b = b) :
    Nonempty (ShortComplex.mk _ _
      (conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero B S hS Z b)).Splitting

AlgebraicGeometry.Space.nonempty_conormalSequence_splitting_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitMono.lean, line 857. The attribute's comment: “the étale-local clause in full: for closed subspaces Z ⊆ X and Z' ⊆ X' joined by an étale φ : X' ⟶ X and an étale a : Z' ⟶ Z over it, with the inclusion of Z' admitting a left inverse over B, the restricted conormal sequence of 05ZA is split exact — it admits a CategoryTheory.ShortComplex.Splitting, so its first arrow is a monomorphism, it is exact at the middle term and its second arrow is a split epimorphism — and the inverse image along a of the second arrow of the unrestricted sequence is a split epimorphism too, which is where the étale-localization clause of 04CU is consumed. Stated at the two canonical inclusions and at the registered first arrow, with no hypothesis beyond the étale-local data of the tag”.

Stacks 05ZB, the étale-local clause in full. Let Z ⊆ X and Z' ⊆ X' be closed subspaces, let φ : X' ⟶ X be étale, let a : Z' ⟶ Z be étale with i' ≫ φ = a ≫ i for the two inclusions, and let g' : X' ⟶ Z' be a left inverse over Bb of the inclusion of Z'. Then

the restricted conormal sequence, the sequence of Stacks 05ZA at Z' ⊆ X' over φ ≫ b, is split exact;

the inverse image along a of the second arrow of the unrestricted sequence is a split epimorphism.

As in AlgebraicGeometry.Space.conormalSequence_splitExact_of_etale, étaleness is assumed of φ and of a separately rather than Z' being assumed to be the preimage of Z, which is weaker: in the situation of the source a is a base change of φ.

theorem nonempty_conormalSequence_splitting_of_etale
    (Z' : ClosedSubspaces B S hS X'.1) (b : X ⟶ Bb) (φ : X' ⟶ X) (hφ : IsEtale B S hS φ.hom)
    (a : (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS) ⟶
      (⟨Z.1.toFunctor, Z.2.1⟩ : AlgebraicSpaces B S hS))
    (ha : IsEtale B S hS a.hom)
    (hsq : subspaceInclusion B S hS X' Z' ≫ φ = a ≫ subspaceInclusion B S hS X Z)
    (g' : X' ⟶ (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hg' : subspaceInclusion B S hS X' Z' ≫ g' =
      𝟙 (⟨Z'.1.toFunctor, Z'.2.1⟩ : AlgebraicSpaces B S hS))
    (hg'b : g' ≫ subspaceInclusion B S hS X' Z' ≫ φ ≫ b = φ ≫ b) :
    Nonempty (ShortComplex.mk _ _
          (conormalSequenceFirstMap_comp_pullbackDifferentialsMap_eq_zero B S hS Z'
            (φ ≫ b))).Splitting ∧
      IsSplitEpi ((modulePullback B S hS a).map
        (pullbackDifferentialsMap B S hS (subspaceInclusion B S hS X Z) b))

AlgebraicGeometry.Space.isSplitEpi_pullbackDifferentialsMap_of_leftInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitting.lean, line 325. The attribute's comment: “the global clause: a left inverse of i over B splits the second arrow of the conormal sequence of 05ZA, so that sequence is split exact”.

Stacks 05ZB, the global clause: a left inverse of i over Bb makes the second arrow of the sequence of Stacks 05ZA a split epimorphism, so that sequence is split exact.

The comparison map of Stacks 04CX at the identity square is carried as the parameters cid, hcid and [IsIso cid]; see the implementation notes.

theorem isSplitEpi_pullbackDifferentialsMap_of_leftInverse (i : Z ⟶ X) (b : X ⟶ Bb) (g : X ⟶ Z)
    (hg : i ≫ g = 𝟙 Z) (hgb : g ≫ i ≫ b = b)
    (cid : (modulePullback B S hS (𝟙 Z)).obj (sheafOfDifferentials B S hS (i ≫ b)) ⟶
      sheafOfDifferentials B S hS (i ≫ b)) [IsIso cid]
    (hcid : IsSheafOfDifferentialsMap B S hS (𝟙 Z) (i ≫ b) (i ≫ b) cid) :
    IsSplitEpi (pullbackDifferentialsMap B S hS i b)

AlgebraicGeometry.Space.isSplitEpi_pullbackDifferentialsMap_of_retraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitting.lean, line 345. The attribute's comment: “the global clause, unconditionally: a left inverse of i over B splits the second arrow of the conormal sequence of 05ZA, so that sequence is split exact”.

Stacks 05ZB, the global clause, unconditionally: a left inverse of i over Bb makes the second arrow of the sequence of Stacks 05ZA a split epimorphism, so that sequence is split exact.

This is AlgebraicGeometry.Space.isSplitEpi_pullbackDifferentialsMap_of_leftInverse with the comparison map of Stacks 04CX at the identity square supplied rather than carried: it is the unit law of Stacks 03LU at Ω_{Z/Bb}, which is a comparison map by AlgebraicGeometry.Space.isSheafOfDifferentialsMap_modulePullbackIdIso, and invertible by AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_id. Nothing is assumed beyond the left inverse.

theorem isSplitEpi_pullbackDifferentialsMap_of_retraction (i : Z ⟶ X) (b : X ⟶ Bb) (g : X ⟶ Z)
    (hg : i ≫ g = 𝟙 Z) (hgb : g ≫ i ≫ b = b) :
    IsSplitEpi (pullbackDifferentialsMap B S hS i b)

AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etaleLeftInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitting.lean, line 400. The attribute's comment: “the étale-local clause: a left inverse of the restriction of i along an étale φ : X' ⟶ X splits the inverse image along the induced a : Z' ⟶ Z of the second arrow of the conormal sequence of 05ZA”.

Stacks 05ZB, the étale-local clause: if the restriction of i along an étale φ : X' ⟶ X has a left inverse over Bb, the inverse image along the induced a : Z' ⟶ Z of the second arrow of the sequence of Stacks 05ZA is a split epimorphism, so the restricted sequence is split exact.

The section is the chosen section of the global clause at i', conjugated by the two invertible comparison maps of Stacks 04CU and the composition comparisons of Stacks 03LU. The comparison map at the identity square and the étale-localization clause of Stacks 04CU are carried as parameters and instances; see the implementation notes.

theorem isSplitEpi_map_pullbackDifferentialsMap_of_etaleLeftInverse (i : Z ⟶ X) (b : X ⟶ Bb)
    (φ : X' ⟶ X) (i' : Z' ⟶ X') (a : Z' ⟶ Z) (hsq : i' ≫ φ = a ≫ i) (g' : X' ⟶ Z')
    (hg' : i' ≫ g' = 𝟙 Z') (hg'b : g' ≫ i' ≫ φ ≫ b = φ ≫ b)
    (cid' : (modulePullback B S hS (𝟙 Z')).obj
        (sheafOfDifferentials B S hS (i' ≫ φ ≫ b)) ⟶
      sheafOfDifferentials B S hS (i' ≫ φ ≫ b)) [IsIso cid']
    (hcid' : IsSheafOfDifferentialsMap B S hS (𝟙 Z') (i' ≫ φ ≫ b) (i' ≫ φ ≫ b) cid')
    (ca : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS (i ≫ b)) ⟶
      sheafOfDifferentials B S hS (i' ≫ φ ≫ b)) [IsIso ca]
    (hca : IsSheafOfDifferentialsMap B S hS a (i ≫ b) (i' ≫ φ ≫ b) ca)
    [IsIso (pullbackDifferentialsMap B S hS φ b)] :
    IsSplitEpi ((modulePullback B S hS a).map (pullbackDifferentialsMap B S hS i b))

AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etaleRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitting.lean, line 445. The attribute's comment: “the étale-local clause, unconditional in 04CX: a left inverse of the restriction of i along an étale φ : X' ⟶ X splits the inverse image along the induced a : Z' ⟶ Z of the second arrow of the conormal sequence of 05ZA”.

Stacks 05ZB, the étale-local clause, with the comparison map at the identity square no longer carried: if the restriction of i along an étale φ : X' ⟶ X has a left inverse over Bb, the inverse image along the induced a : Z' ⟶ Z of the second arrow of the sequence of Stacks 05ZA is a split epimorphism, so the restricted sequence is split exact.

This is AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etaleLeftInverse with the unit law of Stacks 04CX supplied rather than carried, by AlgebraicGeometry.Space.isSheafOfDifferentialsMap_modulePullbackIdIso and AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_id. So this clause is unconditional in Stacks 04CX.

It still takes the invertibility of the two comparison maps as the instances [IsIso ca] and [IsIso (pullbackDifferentialsMap B S hS φ b)], which is the conclusion of the étale-localization clause of Stacks 04CU at a and at φ; étaleness of φ and of a is not assumed, so this applies to any square where those two maps are invertible. AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etale is the form that assumes étaleness and discharges the two instances.

theorem isSplitEpi_map_pullbackDifferentialsMap_of_etaleRetraction (i : Z ⟶ X) (b : X ⟶ Bb)
    (φ : X' ⟶ X) (i' : Z' ⟶ X') (a : Z' ⟶ Z) (hsq : i' ≫ φ = a ≫ i) (g' : X' ⟶ Z')
    (hg' : i' ≫ g' = 𝟙 Z') (hg'b : g' ≫ i' ≫ φ ≫ b = φ ≫ b)
    (ca : (modulePullback B S hS a).obj (sheafOfDifferentials B S hS (i ≫ b)) ⟶
      sheafOfDifferentials B S hS (i' ≫ φ ≫ b)) [IsIso ca]
    (hca : IsSheafOfDifferentialsMap B S hS a (i ≫ b) (i' ≫ φ ≫ b) ca)
    [IsIso (pullbackDifferentialsMap B S hS φ b)] :
    IsSplitEpi ((modulePullback B S hS a).map (pullbackDifferentialsMap B S hS i b))

AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalSequenceSplitting.lean, line 473. The attribute's comment: “the étale-local clause, with nothing carried: for étale φ : X' ⟶ X and a, a left inverse of the restriction of i along φ splits the inverse image along a of the second arrow of the conormal sequence of 05ZA”.

Stacks 05ZB, the étale-local clause, with nothing carried: if φ : X' ⟶ X and the induced a : Z' ⟶ Z are étale and the restriction i' : Z' ⟶ X' of i along φ has a left inverse over Bb, then the inverse image along a of the second arrow of the sequence of Stacks 05ZA is a split epimorphism, so the restricted sequence is split exact.

This is AlgebraicGeometry.Space.isSplitEpi_map_pullbackDifferentialsMap_of_etaleRetraction with the two invertible comparison maps supplied rather than carried: the comparison map of Stacks 04CX along an étale morphism, over a fixed base, is invertible by AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_etale, which is the étale-localization clause of Stacks 04CU. So nothing is assumed here beyond the hypotheses of the source: φ is étale, a — a base change of φ in the situation of the source — is étale, the square i' ≫ φ = a ≫ i commutes, and i' has the left inverse g' over Bb.

theorem isSplitEpi_map_pullbackDifferentialsMap_of_etale (i : Z ⟶ X) (b : X ⟶ Bb)
    (φ : X' ⟶ X) (hφ : IsEtale B S hS φ.hom) (i' : Z' ⟶ X') (a : Z' ⟶ Z)
    (ha : IsEtale B S hS a.hom) (hsq : i' ≫ φ = a ≫ i) (g' : X' ⟶ Z')
    (hg' : i' ≫ g' = 𝟙 Z') (hg'b : g' ≫ i' ≫ φ ≫ b = φ ≫ b) :
    IsSplitEpi ((modulePullback B S hS a).map (pullbackDifferentialsMap B S hS i b))

Tag 05ZC, a lemma

Tag 05ZC in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_isSheafOfDifferentialsMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsBaseChange.lean, line 227. The attribute's comment: “granted, as hetale, the étale localization of 04CU: over each étale chart the comparison map is the canonical map 01UV of a cartesian square of schemes. The scheme case 01V0 is applied, not granted”.

Stacks 05ZC. Let p : X ⟶ Y be a morphism of algebraic spaces over S, let g : Y' ⟶ Y be a morphism and let X', with its projections g' : X' ⟶ X and p' : X' ⟶ Y', be the base change of p by g. Then the comparison map c_{g'} : (g')^*Ω_{X/Y} ⟶ Ω_{X'/Y'} of Stacks 04CX is an isomorphism.

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 the comparison map is the canonical map of a cartesian square of schemes, which is an isomorphism by Morphisms, Lemma 01V0, and an isomorphism on the sections over every chart is an isomorphism.

theorem isIso_of_isSheafOfDifferentialsMap_of_isPullback (g' : X' ⟶ X) (p' : X' ⟶ Y')
    (p : X ⟶ Y) (g : Y' ⟶ Y) (h : IsPullback g' p' p g)
    (c c₀ : (modulePullback B S hS g').obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p')
    (hc : IsSheafOfDifferentialsMap B S hS g' p p' c)
    (hc₀ : IsSheafOfDifferentialsMap B S hS g' p p' c₀)
    (hetale : IsEtaleLocalBaseChangeMap B S hS g' p' p g h c₀) :
    IsIso c

AlgebraicGeometry.Space.isIso_sheafOfDifferentialsMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeSquareBijective.lean, line 459. The attribute's comment: “the map of 04CX for the base change of X along g is an isomorphism, with the base change presented as a cartesian square and the map by the property characterizing it. The étale localization of 04CU and the scheme case 01V0 are both applied as proved”.

Stacks 05ZC. Let X ⟶ Y be a morphism of algebraic spaces over S and let g : Y' ⟶ Y be a morphism of algebraic spaces over S. Let X' = X_{Y'} be the base change of X and let g' : X' ⟶ X be the projection. Then the map (g')^*Ω_{X/Y} ⟶ Ω_{X'/Y'} of Stacks 04CX is an isomorphism.

The base change is presented as a cartesian square IsPullback g' p' p g of algebraic spaces, and the map of Stacks 04CX by the property AlgebraicGeometry.Space.IsSheafOfDifferentialsMap that characterizes it — existence is AlgebraicGeometry.Space.isSheafOfDifferentialsMap_sheafOfDifferentialsMap and uniqueness AlgebraicGeometry.Space.eq_of_isSheafOfDifferentialsMap, so naming the map this way asserts nothing beyond the square.

The proof is the source's own: the case of a square of schemes, Morphisms, Lemma 01V0, together with the étale localization of Stacks 04CU. The scheme case enters as AlgebraicGeometry.Scheme.Hom.bijective_restrictRelativeDerivation_of_isPullback through AlgebraicGeometry.Space.schemeSquareDerivationRestriction.

theorem isIso_sheafOfDifferentialsMap_of_isPullback (g' : X' ⟶ X) (p' : X' ⟶ Y') (p : X ⟶ Y)
    (g : Y' ⟶ Y) (h : IsPullback g' p' p g)
    {c : (modulePullback B S hS g').obj (sheafOfDifferentials B S hS p) ⟶
      sheafOfDifferentials B S hS p'}
    (hc : IsSheafOfDifferentialsMap B S hS g' p p' c) : IsIso c

Tag 05ZD, a lemma

Tag 05ZD in the Stacks Project.

AlgebraicGeometry.Space.isIso_biprodDesc_of_isSheafOfDifferentialsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsBaseChange.lean, line 257. The attribute's comment: “granted, as hetale, the étale localization of 04CU: over each étale chart the map p^*Ω_{X/T} ⊕ q^*Ω_{Y/T} ⟶ Ω_{W/T} is the map 01V1 of a cartesian square of schemes. The scheme case 01V1 is applied, not granted”.

Stacks 05ZD. Let f : X ⟶ T and g : Y ⟶ T be morphisms of algebraic spaces over S with the same target and let p : W ⟶ X, q : W ⟶ Y be the projections of a fibre product of f and g. The two comparison maps of Stacks 04CX exhibit Ω_{W/T} as the direct sum p^*Ω_{X/T} ⊕ q^*Ω_{Y/T}.

Both summands are named by the characterizing property of Stacks 04CX for the square they come from — the one with top edge p and right edge f, and the one with top edge q and right edge g, both with left edge the structure morphism p ≫ f of W — so the conclusion is about the two comparison maps and not about some decomposition of Ω_{W/T}. As for Stacks 05ZC the étale localization of Stacks 04CU is granted and Morphisms, Lemma 01V1 is applied.

theorem isIso_biprodDesc_of_isSheafOfDifferentialsMap {W T : AlgebraicSpaces B S hS}
    (p : W ⟶ X) (q : W ⟶ Y) (f : X ⟶ T) (g : Y ⟶ T) (h : IsPullback p q f g)
    (a a₀ : (modulePullback B S hS p).obj (sheafOfDifferentials B S hS f) ⟶
      sheafOfDifferentials B S hS (p ≫ f))
    (b b₀ : (modulePullback B S hS q).obj (sheafOfDifferentials B S hS g) ⟶
      sheafOfDifferentials B S hS (p ≫ f))
    (ha : IsSheafOfDifferentialsMap B S hS p f (p ≫ f) a)
    (ha₀ : IsSheafOfDifferentialsMap B S hS p f (p ≫ f) a₀)
    (hb : IsSheafOfDifferentialsMap B S hS q g (p ≫ f) b)
    (hb₀ : IsSheafOfDifferentialsMap B S hS q g (p ≫ f) b₀)
    (hetale : IsEtaleLocalFibreProductMap B S hS p q f g h (biprod.desc a₀ b₀)) :
    IsIso (biprod.desc a b)

AlgebraicGeometry.Space.isIso_biprodDesc_sheafOfDifferentialsMap_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSchemeSquareBijective.lean, line 484. The attribute's comment: “the two maps of 04CX out of p^Omega_{X/T} and q^Omega_{Y/T} give an isomorphism onto Omega_{X x_T Y/T}, with the fibre product presented as a cartesian square and each summand by the property characterizing it. The étale localization of 04CU and the scheme case 01V1 are both applied as proved”.

Stacks 05ZD. Let f : X ⟶ T and g : Y ⟶ T be morphisms of algebraic spaces over S with the same target and let p : W ⟶ X, q : W ⟶ Y be the projections of the fibre product W = X ×_T Y. Then the maps of Stacks 04CX give an isomorphism p^*Ω_{X/T} ⊕ q^*Ω_{Y/T} ⟶ Ω_{W/T}.

The fibre product is presented as a cartesian square IsPullback p q f g and the two summands by the property AlgebraicGeometry.Space.IsSheafOfDifferentialsMap that characterizes the map of Stacks 04CX for the square they come from, so the conclusion is about those two maps and not about some decomposition of Ω_{W/T}.

The proof is the source's own: the case of schemes, Morphisms, Lemma 01V1, together with the étale localization of Stacks 04CU, the scheme case entering through AlgebraicGeometry.Space.schemeSquareDerivationRestriction.

theorem isIso_biprodDesc_sheafOfDifferentialsMap_of_isPullback {W T : AlgebraicSpaces B S hS}
    (p : W ⟶ X) (q : W ⟶ Y) (f : X ⟶ T) (g : Y ⟶ T) (h : IsPullback p q f g)
    (a : (modulePullback B S hS p).obj (sheafOfDifferentials B S hS f) ⟶
      sheafOfDifferentials B S hS (p ≫ f))
    (b : (modulePullback B S hS q).obj (sheafOfDifferentials B S hS g) ⟶
      sheafOfDifferentials B S hS (p ≫ f))
    (ha : IsSheafOfDifferentialsMap B S hS p f (p ≫ f) a)
    (hb : IsSheafOfDifferentialsMap B S hS q g (p ≫ f) b) :
    IsIso (biprod.desc a b)

Tag 05ZE, a lemma

Tag 05ZE in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteType.lean, line 652. The attribute's comment: “finite type of Ω_{X/Y}, from étale-local finite generation of 𝒪_X over f⁻¹𝒪_Y and unramifiedness of the transition maps of the small étale site; the gap to the source's hypothesis is the bridge from 03XF(1) to the algebra statement, and 00UU for the sections of an arrow of the small étale site”.

Stacks 05ZE, with the two carried hypotheses in place of "f is locally of finite type". If 𝒪_X is étale-locally generated as an f⁻¹𝒪_Y-algebra by finitely many sections and the transition maps of the small étale site of X are unramified, then Ω_{X/Y} is a finite type 𝒪_X-module.

The covering of each object is the one hft supplies, presented as the family of all its arrows indexed by their sources, and on each member the finitely many generators are AlgebraicGeometry.Space.hasFiniteGlobalGenerators_sheafOfDifferentials_over.

theorem isFiniteTypeOnSite_sheafOfDifferentials (f : X ⟶ Y)
    (hunram : HasUnramifiedChartTransitions B S hS X)
    (hft : HasFiniteTypeChartAlgebras B S hS f) :
    (sheafOfDifferentials B S hS f).IsFiniteTypeOnSite

AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteType.lean, line 676. The attribute's comment: “the source's statement, carrying the bridge from 03XF(1) to étale-local finite generation of 𝒪_X over f⁻¹𝒪_Y as hft and unramifiedness of the transition maps of a small étale site (00UU) as hunram, both quantified over all algebraic spaces over S”.

Stacks 05ZE. If f : X ⟶ Y is a morphism of algebraic spaces over S which is locally of finite type, then Ω_{X/Y} is a finite type 𝒪_X-module.

The two inputs not proved in this development are carried universally quantified: the bridge from AlgebraicGeometry.Space.IsLocallyOfFiniteType (Stacks 03XF(1), defined through étale scheme charts) to the statement that 𝒪_X is étale-locally a finite type f⁻¹𝒪_Y-algebra, and the unramifiedness of the transition maps of a small étale site, which is Algebra, Lemma 00UU for the ring map of sections of an arrow of that site.

theorem isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType
    (hunram : ∀ X' : AlgebraicSpaces B S hS, HasUnramifiedChartTransitions B S hS X')
    (hft : ∀ (X' Y' : AlgebraicSpaces B S hS) (g : X' ⟶ Y'),
      IsLocallyOfFiniteType B S hS g.hom → HasFiniteTypeChartAlgebras B S hS g)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    (sheafOfDifferentials B S hS f).IsFiniteTypeOnSite

AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_affineChartAlgebras, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteType.lean, line 796. The attribute's comment: “finite type of Ω_{X/Y} from étale-local finite generation of 𝒪_X over f⁻¹𝒪_Y on a covering by affine charts, which is what 03XF(1) delivers; unramifiedness of the transition maps of the small étale site (00UU) is proved, not assumed. The source's own hypothesis is taken in isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_unconditional”.

Finite type of Ω_{X/Y} from the étale-local finite generation of 𝒪_X over f⁻¹𝒪_Y. If every object of the small étale site of X has a covering by affine charts over which 𝒪_X is generated as an f⁻¹𝒪_Y-algebra by finitely many sections, then Ω_{X/Y} is a finite type 𝒪_X-module.

The covering of each object is the one hft supplies, and on each of its members the finitely many generators are AlgebraicGeometry.Space.hasFiniteGlobalGenerators_sheafOfDifferentials_over_of_isAffine. Unramifiedness of the transition maps — Algebra, Lemma 00UU — is proved, not assumed: affineness of the members is what makes AlgebraicGeometry.Space.subsingleton_kaehlerDifferential_chartRing_of_affineChart apply.

This is the engine of Stacks 05ZE with no unramifiedness hypothesis; at the source's own hypothesis AlgebraicGeometry.Space.IsLocallyOfFiniteType, and with nothing else assumed, the statement is AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_unconditional, in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteTypeChartBridge.lean.

theorem isFiniteTypeOnSite_sheafOfDifferentials_of_affineChartAlgebras (f : X ⟶ Y)
    (hft : HasFiniteTypeAffineChartAlgebras B S hS f) :
    (sheafOfDifferentials B S hS f).IsFiniteTypeOnSite

AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteTypeChartBridge.lean, line 268. The attribute's comment: “Ω_{X/Y} is a finite type 𝒪_X-module for f locally of finite type, with no further hypothesis”.

Stacks 05ZE. If f : X ⟶ Y is a morphism of algebraic spaces over S which is locally of finite type, then Ω_{X/Y} is a finite type 𝒪_X-module.

The chart-algebra condition of AlgebraicGeometry.Space.hasFiniteTypeAffineChartAlgebras_of_isLocallyOfFiniteType feeds AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_affineChartAlgebras, which generates Ω_{X/Y} over each member of the covering by the universal differentials of the generators. Algebra, Lemma 00UU for the transition maps of the small étale site is proved there, not assumed.

theorem isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_unconditional
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    (sheafOfDifferentials B S hS f).IsFiniteTypeOnSite

AlgebraicGeometry.Space.isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFiniteTypeEtaleChart.lean, line 107.

Stacks 05ZE. If f : X ⟶ Y is a morphism of algebraic spaces over S which is locally of finite type, then the sheaf of differentials Ω_{X/Y} is an 𝒪_X-module of finite type.

The proof is the source's. An atlas q : V ⟶ Y lifts, by Stacks 02X1, to a surjective étale chart p : U ⟶ X and a morphism α : U ⟶ V of schemes over q; α is locally of finite type because f is. The pullback of Ω_{X/Y} to U is the sheaf of differentials of α (Stacks 04CU), which is the small-étale module associated to Ω_{U/V}; that is of finite type by Stacks 01V2 and Stacks 08HD, and finite type descends from the surjective chart.

theorem isFiniteTypeOnSite_sheafOfDifferentials_of_isLocallyOfFiniteType_hom
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    (sheafOfDifferentials B S hS f).IsFiniteTypeOnSite

Tag 05ZF, a lemma

Tag 05ZF in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentationOnSite_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFinitePresentation.lean, line 519. The attribute's comment: “finite presentation of Ω_{X/Y}. ASSUMED, not proved: the relations half of Descent, Proposition 03DX(2), as the last clause of hfp — that the relations among the universal differentials of a finite generating family are étale-locally finitely generated. Also assumed: the bridge from 03XP(1) to étale-local finite generation of 𝒪_X over f⁻¹𝒪_Y (first clause of hfp), and unramifiedness of the transition maps of the small étale site (hunram, 00UU), which hasUnramifiedChartTransitions_of_forall_isAffine discharges when every étale chart is affine. PROVED here: the generators half and the assembly into 03DL(7)”.

Stacks 05ZF, with the two carried hypotheses in place of "f is locally of finite presentation". If 𝒪_X is étale-locally generated as an f⁻¹𝒪_Y-algebra by finitely many sections whose universal differentials have étale-locally finitely generated relations, and the transition maps of the small étale site of X are unramified, then Ω_{X/Y} is an 𝒪_X-module of finite presentation.

The covering of each object is the one hfp supplies, presented as the family of all its arrows indexed by their sources, and on each member the finite presentation is AlgebraicGeometry.Space.hasFiniteGlobalPresentation_sheafOfDifferentials_over.

theorem isFinitePresentationOnSite_sheafOfDifferentials (f : X ⟶ Y)
    (hunram : HasUnramifiedChartTransitions B S hS X)
    (hfp : HasFinitePresentationChartData B S hS f) :
    (sheafOfDifferentials B S hS f).IsFinitePresentationOnSite

AlgebraicGeometry.Space.isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFinitePresentation.lean, line 548. The attribute's comment: “the source's statement. ASSUMED, not proved: the relations half of Descent, Proposition 03DX(2), inside hfp; the bridge from 03XP(1) to étale-local finite presentation data for 𝒪_X over f⁻¹𝒪_Y, also inside hfp; and unramifiedness of the transition maps of a small étale site (hunram, 00UU), discharged by hasUnramifiedChartTransitions_of_forall_isAffine when every étale chart is affine. Both inputs are quantified over all algebraic spaces over S”.

Stacks 05ZF. If f : X ⟶ Y is a morphism of algebraic spaces over S which is locally of finite presentation, then Ω_{X/Y} is an 𝒪_X-module of finite presentation.

The two inputs not proved in this development are carried universally quantified: the bridge from AlgebraicGeometry.Space.IsLocallyOfFinitePresentation (Stacks 03XP(1), defined through étale scheme charts) to the étale-local finite presentation data of AlgebraicGeometry.Space.HasFinitePresentationChartData, and the unramifiedness of the transition maps of a small étale site, which is Algebra, Lemma 00UU for the ring map of sections of an arrow of that site.

theorem isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation
    (hunram : ∀ X' : AlgebraicSpaces B S hS, HasUnramifiedChartTransitions B S hS X')
    (hfp : ∀ (X' Y' : AlgebraicSpaces B S hS) (g : X' ⟶ Y'),
      IsLocallyOfFinitePresentation B S hS g.hom → HasFinitePresentationChartData B S hS g)
    (f : X ⟶ Y) (hf : IsLocallyOfFinitePresentation B S hS f.hom) :
    (sheafOfDifferentials B S hS f).IsFinitePresentationOnSite

AlgebraicGeometry.Space.isFinitePresentationOnSite_sheafOfDifferentials_of_chartData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFinitePresentation.lean, line 736. The attribute's comment: “finite presentation of Ω_{X/Y} from étale-local finite presentation data for 𝒪_X over f⁻¹𝒪_Y; unramifiedness of the transition maps of the small étale site (00UU) is proved, not assumed. The source's own hypothesis is taken in isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation_unconditional”.

Finite presentation of Ω_{X/Y} from étale-local presentation data for 𝒪_X over f⁻¹𝒪_Y. If 𝒪_X is étale-locally generated as an f⁻¹𝒪_Y-algebra by finitely many sections whose universal differentials have étale-locally finitely generated relations, then Ω_{X/Y} is an 𝒪_X-module of finite presentation.

The covering of each object is the one hfp supplies, refined to its members with affine underlying scheme (AlgebraicGeometry.Space.SmallEtale.ofArrows_affineMember_mem_topology), and on each such member the finite presentation is AlgebraicGeometry.Space.hasFiniteGlobalPresentation_sheafOfDifferentials_over. Refining to affine members is what makes Algebra, Lemma 00UU applicable: the only transition maps the proof differentiates are arrows between affine charts.

The tag itself is AlgebraicGeometry.Space.isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation below, which takes the source's hypothesis on f; this is the sectionwise route to the same conclusion, kept because it reads the presentation off the construction of Ω_{X/Y} as a sheafification rather than off the scheme case.

theorem isFinitePresentationOnSite_sheafOfDifferentials_of_chartData (f : X ⟶ Y)
    (hfp : HasFinitePresentationChartData B S hS f) :
    (sheafOfDifferentials B S hS f).IsFinitePresentationOnSite

AlgebraicGeometry.Space.isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsFinitePresentation.lean, line 768. The attribute's comment: “finite presentation of Ω_{X/Y} for a morphism of algebraic spaces locally of finite presentation”. References: SGA 3 III (0.14), “more general”; SGA 7 VI (5.1), “partial”.

Stacks 05ZF. If f : X ⟶ Y is a morphism of algebraic spaces over S which is locally of finite presentation, then Ω_{X/Y} is an 𝒪_X-module of finite presentation.

The proof is the source's, and it is the finite-presentation refinement of the proof of Stacks 04CV in StacksFrontier.AlgebraicGeometry.Spaces.SheafOfDifferentialsQuasicoherent. An atlas q : V ⟶ Y of the target lifts, by Stacks 02X1, to a surjective étale chart p : U ⟶ X of the source together with a morphism α : U ⟶ V of schemes of the site making the square commute. Being locally of finite presentation is a condition on exactly such squares, so α is a morphism of schemes locally of finite presentation and its Zariski sheaf of relative differentials is of finite presentation by Morphisms, Lemma 01V3. The identification of Stacks 04CU reads the pullback of Ω_{X/Y} along p as the sheaf of differentials of α, which the final sentence of Stacks 04CU — Stacks 04CS, in the form AlgebraicGeometry.Space.sheafOfDifferentialsSchemeComparison — identifies with the small-étale module associated to that Zariski sheaf; the associated module of a module of finite presentation is of finite presentation by AlgebraicGeometry.Space.isFinitePresentationOnSite_representedAssociatedModule. Finally finite presentation descends from a surjective étale chart by AlgebraicGeometry.Space.isFinitePresentationOnSite_iff_exists_etale_surjective, the pullback of modules and étale restriction being matched by Equation 03LW.

theorem isFinitePresentationOnSite_sheafOfDifferentials_of_isLocallyOfFinitePresentation_unconditional
    (f : X ⟶ Y) (hf : IsLocallyOfFinitePresentation B S hS f.hom) :
    (sheafOfDifferentials B S hS f).IsFinitePresentationOnSite

Tag 0CK5, a lemma

Tag 0CK5 in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_sheafOfDifferentials_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSiteTransport.lean, line 97. The attribute's comment: “the unconditional form, with the 04CS site transport of finite local freeness discharged by AlgebraicGeometry.Space.sheafOfDifferentialsSchemeSiteComparison; smoothness of f is the only thing this asks”.

Stacks 0CK5, asking nothing beyond smoothness. The sheaf of differentials Ω_{X/Y} of a smooth morphism f : X ⟶ Y of algebraic spaces over a scheme S is finite locally free on the small étale site of X.

This is AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_sheafOfDifferentials, the reduction of Stacks 0CK5 to Stacks 02G1, applied to AlgebraicGeometry.Space.sheafOfDifferentialsSchemeSiteComparison, which proves the comparison of Stacks 04CS that the reduction takes as its argument hsite. The mathematics is that of the reduction; only the argument is supplied.

theorem isFiniteLocallyFreeOnSite_sheafOfDifferentials_of_isSmooth
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsSmooth B S hS f.hom) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (sheafOfDifferentials B S hS f)

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsSmoothFiniteLocallyFree.lean, line 199. The attribute's comment: “granted as hsite the comparison of 04CS transporting finite local freeness of the differentials of a morphism of schemes of the site from its small Zariski site to its small étale site. The identification Ω_{X/Y}|_{U_étale} ≅ Ω_{U/V} of 04CU over a commuting square of étale charts is not granted: it is proved here”.

Stacks 0CK5. The sheaf of differentials Ω_{X/Y} of a smooth morphism f : X ⟶ Y of algebraic spaces over a scheme S is finite locally free on the small étale site of X, granted the comparison AlgebraicGeometry.Space.SheafOfDifferentialsSchemeSiteComparison.

An atlas of the target lifts along f, by Stacks 02X1, to a commuting square of étale charts whose chart of the source is surjective on points. Smoothness of f is the every-chart condition of Stacks 03ZC(1), so the square's scheme morphism ψ is smooth; Stacks 02G1 makes Ω_{U/V} finite locally free in the local-generators form of Stacks 01C6(2), and Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_of_isFiniteLocallyFree rewrites that in the covering-family form of Stacks 03DL(2). The hypothesis carries it to the small étale site, Stacks 04CU — AlgebraicGeometry.Space.sheafOfDifferentialsEtaleChartComparison, which is proved and no longer assumed — to the restriction of Ω_{X/Y} to the chart, and the clause of Stacks 03DN along an étale morphism of algebraic spaces descends it from that surjective chart to X.

theorem isFiniteLocallyFreeOnSite_sheafOfDifferentials {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsSmooth B S hS f.hom)
    (hsite : SheafOfDifferentialsSchemeSiteComparison B S hS) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (sheafOfDifferentials B S hS f)

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

76.3 Radicial morphisms to 76.7 Sheaf of differentials of…

Section76.3 Radicial morphisms#

Tag 0481, a definition

Tag 0482, a lemma

Tag 0483, an example

Tag 0484, a lemma

Tag 049E, a remark

Tag 0AGE, a lemma

Sources

Section76.4 Monomorphisms#

Tag 0B8A, a lemma

Tag 0B8B, a lemma

Tag 0B8C, a lemma

Sources

Section76.5 Conormal sheaf of an immersion#

Tag 04CN, a definition

Tag 04CO, a lemma

Tag 04CP, a lemma

Tag 04G2, a lemma

Tag 04CQ, a lemma

Tag 06BD, a lemma

Sources

Section76.6 The normal cone of an immersion#

Tag 09RN, a definition

Tag 09RP, an equation

Tag 09RQ, an equation

Tag 09RR, a lemma

Tag 09RS, a lemma

Tag 09RT, a lemma

Tag 09RU, a definition

Sources

Section76.7 Sheaf of differentials of a morphism#

Tag 04CS, a lemma

Tag 04CT, a definition

Tag 04CU, a lemma

Tag 04CV, a lemma

Tag 04CW, a remark

Tag 04CX, a lemma

Tag 05Z7, a lemma

Tag 05Z8, a lemma

Tag 05Z9, a lemma

Tag 05ZA, a lemma

Tag 05ZB, a lemma

Tag 05ZC, a lemma

Tag 05ZD, a lemma

Tag 05ZE, a lemma

Tag 05ZF, a lemma

Tag 0CK5, a lemma

Sources

Section76.3 Radicial morphisms #

Section76.4 Monomorphisms #

Section76.5 Conormal sheaf of an immersion #

Section76.6 The normal cone of an immersion #

Section76.7 Sheaf of differentials of a morphism #