60.13 Two universal thickenings to 60.23 Applications

Section60.13 Two universal thickenings #

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

Tag 07J2, a remark

Tag 07J2 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.firstOrderThickeningHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalConnectionNaturality.lean, line 82. The attribute's comment: “the functoriality datum of the first-order thickening, in the shape in which the naturality clause of 07J6 consumes it”.

The functoriality datum of the first-order universal thickening of [Stacks, Tag 07J2]. For a morphism g : (U, T, δ) ⟶ (U₁, T₁, δ₁) of CRIS(X/S), the induced morphism (U, T', δ') ⟶ (U₁, T₁', δ₁') of the site together with its two commutation relations, which StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean constructs as Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap, Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap_comp_P₀ and Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap_comp_P₁.

This is the input [Stacks, Tag 07J6] uses to turn its family of connections into a morphism of abelian sheaves on the site.

def firstOrderThickeningHom {A B : Thickening S} (g : A ⟶ B) : FirstOrderThickeningHom g

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 367. The attribute's comment: “the morphism T' ⟶ T₁' of schemes”.

The morphism of schemes T_A' ⟶ T_B' between the first-order universal thickenings.

public def firstOrderThickeningSchemeMap (g : A ⟶ B) :
    firstOrderThickeningScheme A.thickening.target S.S.scheme A.toBase.hom ⟶
      firstOrderThickeningScheme B.thickening.target S.S.scheme B.toBase.hom

Crystalline.GlobalCrystallineSituation.firstOrderThickeningMapApp_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 387. The attribute's comment: “the map T' ⟶ T₁' is compatible with the divided powers δ'”.

The map on sections of the first-order thickenings is a homomorphism of divided power rings. It carries J'_B = J_B ⊕ Ω_B into J'_A = J_A ⊕ Ω_A because the ambient morphism does so on the first summand, and it commutes with δ' because the ambient morphism commutes with δ and the map on differentials is semilinear.

public theorem firstOrderThickeningMapApp_isDPMorphism (g : A ⟶ B)
    (U : B.thickening.target.scheme.Opens) :
    DividedPowers.IsDPMorphism
      (firstOrderThickeningDividedPowers B.thickening.target S.S.scheme B.toBase.hom (op U))
      (firstOrderThickeningDividedPowers A.thickening.target S.S.scheme A.toBase.hom
        (op (ambientHom g ⁻¹ᵁ U)))
      (firstOrderThickeningMapApp g (op U)).hom

Crystalline.GlobalCrystallineSituation.firstOrderThickeningDPMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 424. The attribute's comment: “the morphism T' ⟶ T₁' of divided power schemes”.

The morphism of divided power schemes (T_A', J_A', δ_A') ⟶ (T_B', J_B', δ_B') between the first-order universal thickenings.

public def firstOrderThickeningDPMap (g : A ⟶ B) :
    firstOrderThickeningDPScheme S A ⟶ firstOrderThickeningDPScheme S B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap_comp_projHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 442. The attribute's comment: “the map T' ⟶ T₁' commutes with p₀, for schemes”.

The map of first-order thickenings commutes with the first projection, both sides carrying (b, ω) to gh^# b.

public theorem firstOrderThickeningSchemeMap_comp_projHom (g : A ⟶ B) :
    firstOrderThickeningSchemeMap g ≫
        firstOrderThickeningProjHom B.thickening.target S.S.scheme B.toBase.hom =
      firstOrderThickeningProjHom A.thickening.target S.S.scheme A.toBase.hom ≫ ambientHom g

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap_comp_P₁Hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 454. The attribute's comment: “the map T' ⟶ T₁' commutes with p₁, for schemes”.

The map of first-order thickenings commutes with the second projection. This is the computation dg ∘ d_B = d_A ∘ gh^#: one side carries b to (gh^# b, dg (d_B b)) and the other to (gh^# b, d_A (gh^# b)).

public theorem firstOrderThickeningSchemeMap_comp_P₁Hom (g : A ⟶ B) :
    firstOrderThickeningSchemeMap g ≫
        firstOrderThickeningP₁Hom B.thickening.target S.S.scheme B.toBase.hom =
      firstOrderThickeningP₁Hom A.thickening.target S.S.scheme A.toBase.hom ≫ ambientHom g

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 464. The attribute's comment: “the functoriality (U, T, δ) ↦ (U, T', δ') of the first-order thickening”.

The morphism of CRIS(X/S) between the first-order universal thickenings induced by a morphism g of CRIS(X/S): the functoriality datum of [Stacks, Tag 07J2].

public def firstOrderThickeningSiteMap (g : A ⟶ B) :
    firstOrderThickeningObject S A ⟶ firstOrderThickeningObject S B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 488. The attribute's comment: “the functoriality datum commutes with p₀, in CRIS(X/S)”.

The functoriality datum commutes with the first projection, the left relation of [Stacks, Tag 07J2].

public theorem firstOrderThickeningSiteMap_comp_P₀ (g : A ⟶ B) :
    firstOrderThickeningSiteMap g ≫ firstOrderThickeningSiteP₀ S B =
      firstOrderThickeningSiteP₀ S A ≫ g

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningFunctorial.lean, line 497. The attribute's comment: “the functoriality datum commutes with p₁, in CRIS(X/S)”.

The functoriality datum commutes with the second projection, the right relation of [Stacks, Tag 07J2].

public theorem firstOrderThickeningSiteMap_comp_P₁ (g : A ⟶ B) :
    firstOrderThickeningSiteMap g ≫ firstOrderThickeningSiteP₁ S B =
      firstOrderThickeningSiteP₁ S A ≫ g

Crystalline.firstOrderThickeningSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 117. The attribute's comment: “the structure sheaf of the first-order thickening”.

The structure sheaf of the first-order universal thickening T' of a divided power scheme T over Y: the square-zero extension 𝒪_T ⊕ Ω_{T/Y,δ} of the structure sheaf of T by its sheaf of divided power differentials.

public def firstOrderThickeningSheaf : TopCat.Sheaf CommRingCat.{u} ↑T.scheme

Crystalline.firstOrderThickeningIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 141. The attribute's comment: “the extended ideal J' = J ⊕ Ω”.

The ideal J' = J ⊕ Ω_{T/Y,δ} of the sections of 𝒪_{T'} over an open: the sections whose component in 𝒪_T lies in the divided power ideal of T.

public def firstOrderThickeningIdeal (W : (Opens ↑T.scheme)ᵒᵖ) :
    Ideal ↑((firstOrderThickeningPresheaf T Y f).obj W)

Crystalline.firstOrderThickeningDividedPowers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 171. The attribute's comment: “the divided power structure on J'”.

The divided power structure δ' on the ideal J' = J ⊕ Ω_{T/Y,δ}, given in degree k + 1 by (g, ω) ↦ (δ_{k+1} g, δ_k g · ω) and in degree zero by 1.

public def firstOrderThickeningDividedPowers (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers (firstOrderThickeningIdeal T Y f W)

Crystalline.firstOrderThickening_mul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 200. The attribute's comment: “the differentials are an ideal of square zero”.

The sheaf of divided power differentials is an ideal of square zero in 𝒪_{T'}.

public theorem firstOrderThickening_mul_eq_zero (W : (Opens ↑T.scheme)ᵒᵖ)
    {x y : ↑((firstOrderThickeningPresheaf T Y f).obj W)}
    (hx : sqZeroExtFst x = 0) (hy : sqZeroExtFst y = 0) : x * y = 0

Crystalline.firstOrderThickening_restriction_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 225. The attribute's comment: “the divided powers on J' are compatible with restriction”.

Every restriction map of 𝒪_{T'} is compatible with the divided powers of J', so the rings of sections of 𝒪_{T'} with the ideals J' and the structures δ' form a presheaf of divided power rings.

public theorem firstOrderThickening_restriction_isDPMorphism
    {W W' : (Opens ↑T.scheme)ᵒᵖ} (i : W ⟶ W') :
    DividedPowers.IsDPMorphism (firstOrderThickeningDividedPowers T Y f W)
      (firstOrderThickeningDividedPowers T Y f W')
      (((firstOrderThickeningPresheaf T Y f).map i).hom)

Crystalline.firstOrderThickeningP₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 285. The attribute's comment: “the map p₀”.

The first of the two maps 𝒪_T → 𝒪_{T'}, the inclusion g ↦ (g, 0).

public def firstOrderThickeningP₀ : T.scheme.sheaf.obj ⟶ firstOrderThickeningPresheaf T Y f

Crystalline.firstOrderThickeningP₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 291. The attribute's comment: “the map p₁”.

The second of the two maps 𝒪_T → 𝒪_{T'}, the inclusion shifted by the universal divided power derivation: g ↦ (g, d_{T/Y,δ} g).

public def firstOrderThickeningP₁ : T.scheme.sheaf.obj ⟶ firstOrderThickeningPresheaf T Y f

Crystalline.firstOrderThickeningProj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 300. The attribute's comment: “the quotient map”.

The projection 𝒪_{T'} → 𝒪_T, forgetting the differential component.

public def firstOrderThickeningProj : firstOrderThickeningPresheaf T Y f ⟶ T.scheme.sheaf.obj

Crystalline.firstOrderThickeningP₀_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 335. The attribute's comment: “p₀ is compatible with the divided powers”.

p₀ is compatible with the divided power structures on J and J'.

public theorem firstOrderThickeningP₀_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (T.dividedPowers.dividedPowers W)
      (firstOrderThickeningDividedPowers T Y f W)
      (((firstOrderThickeningP₀ T Y f).app W).hom)

Crystalline.firstOrderThickeningP₁_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 349. The attribute's comment: “p₁ is compatible with the divided powers”.

p₁ is compatible with the divided power structures on J and J', because the universal divided power derivation obeys the divided power chain rule.

public theorem firstOrderThickeningP₁_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (T.dividedPowers.dividedPowers W)
      (firstOrderThickeningDividedPowers T Y f W)
      (((firstOrderThickeningP₁ T Y f).app W).hom)

Crystalline.firstOrderThickeningProj_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 364. The attribute's comment: “the quotient map is compatible with the divided powers”.

The projection 𝒪_{T'} → 𝒪_T is compatible with the divided power structures on J' and J.

public theorem firstOrderThickeningProj_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (firstOrderThickeningDividedPowers T Y f W)
      (T.dividedPowers.dividedPowers W) (((firstOrderThickeningProj T Y f).app W).hom)

Crystalline.firstOrderThickeningP₁_sub_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 386. The attribute's comment: “p₁ - p₀ is the universal derivation”.

The difference of the two maps 𝒪_T → 𝒪_{T'} is the universal divided power derivation, followed by the inclusion of Ω_{T/Y,δ} as the square-zero summand.

public theorem firstOrderThickeningP₁_sub_P₀ (W : (Opens ↑T.scheme)ᵒᵖ)
    (a : ↑(T.scheme.sheaf.obj.obj W)) :
    ((firstOrderThickeningP₁ T Y f).app W).hom a - ((firstOrderThickeningP₀ T Y f).app W).hom a =
      sqZeroExtMk 0 (sheafApp T Y f W.unop a)

Crystalline.firstOrderThickeningKernelEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 401. The attribute's comment: “the ideal of the thickening is the differentials”.

The ideal of the first-order thickening T → T' is the sheaf of divided power differentials: the kernel of 𝒪_{T'} → 𝒪_T over an open is canonically Ω_{T/Y,δ}.

public def firstOrderThickeningKernelEquiv (W : (Opens ↑T.scheme)ᵒᵖ) :
    ↑((dpDifferentialsModules T Y f).obj W) ≃+
      RingHom.ker (((firstOrderThickeningProj T Y f).app W).hom)

Crystalline.firstOrderThickening_ker_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickenings.lean, line 421. The attribute's comment: “T → T' is a first-order thickening”.

T → T' is a first-order thickening: the ideal of the projection 𝒪_{T'} → 𝒪_T has square zero on every open.

public theorem firstOrderThickening_ker_sq (W : (Opens ↑T.scheme)ᵒᵖ) :
    RingHom.ker (((firstOrderThickeningProj T Y f).app W).hom) ^ 2 = ⊥

Crystalline.firstOrderThickeningScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 213. The attribute's comment: “the first-order thickening T' as a scheme”.

The first-order universal thickening T' as a scheme. The topological space of T equipped with the structure sheaf 𝒪_{T'} = 𝒪_T ⊕ Ω_{T/Y,δ}; it is a scheme because it is isomorphic, as a locally ringed space, to the realization of the square-zero extension.

public def firstOrderThickeningScheme : Scheme.{u}

Crystalline.firstOrderThickeningι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 247. The attribute's comment: “the immersion i : T ⟶ T' of schemes”.

The immersion i : T ⟶ T', whose map on sections is the projection 𝒪_{T'} ⟶ 𝒪_T.

public def firstOrderThickeningι : T.scheme ⟶ firstOrderThickeningScheme T Y f

Crystalline.firstOrderThickeningProjHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 310. The attribute's comment: “the morphism p₀ : T' ⟶ T of schemes”.

The morphism p₀ : T' ⟶ T, induced by the inclusion g ↦ (g, 0) of structure sheaves.

public def firstOrderThickeningProjHom : firstOrderThickeningScheme T Y f ⟶ T.scheme

Crystalline.firstOrderThickeningP₁Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 318. The attribute's comment: “the morphism p₁ : T' ⟶ T of schemes”.

The morphism p₁ : T' ⟶ T, induced by the derivation-shifted inclusion g ↦ (g, d_{T/Y,δ} g) of structure sheaves.

public def firstOrderThickeningP₁Hom : firstOrderThickeningScheme T Y f ⟶ T.scheme

Crystalline.firstOrderThickeningι_comp_projHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 347. The attribute's comment: “the diagram relation p₀ ∘ i = id, for schemes”.

p₀ retracts the immersion i.

public theorem firstOrderThickeningι_comp_projHom :
    firstOrderThickeningι T Y f ≫ firstOrderThickeningProjHom T Y f = 𝟙 T.scheme

Crystalline.firstOrderThickeningι_comp_P₁Hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 354. The attribute's comment: “the diagram relation p₁ ∘ i = id, for schemes”.

p₁ retracts the immersion i.

public theorem firstOrderThickeningι_comp_P₁Hom :
    firstOrderThickeningι T Y f ≫ firstOrderThickeningP₁Hom T Y f = 𝟙 T.scheme

Crystalline.firstOrderThickeningι_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 377. The attribute's comment: “i : T ⟶ T' is a first-order thickening of schemes”.

The immersion T ⟶ T' is a first-order thickening of schemes: its ideal sheaf has square zero, because the kernel of 𝒪_{T'} ⟶ 𝒪_T over every open is the square-zero summand Ω_{T/Y,δ}.

public theorem firstOrderThickeningι_isFirstOrderThickening :
    Stacks.Thickenings.IsFirstOrderThickening (firstOrderThickeningι T Y f)

Crystalline.firstOrderThickeningιKernelEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 394. The attribute's comment: “the ideal sheaf of i is the sheaf of divided power differentials”.

The ideal sheaf of i : T ⟶ T' is Ω_{T/Y,δ}: over every open, the kernel of the map on sections of i is canonically the module of divided power differentials.

public def firstOrderThickeningιKernelEquiv
    (W : (Opens ↑(firstOrderThickeningScheme T Y f))ᵒᵖ) :
    ↑((dpDifferentialsModules T Y f).obj (firstOrderThickeningOpen T Y f W)) ≃+
      RingHom.ker (((firstOrderThickeningι T Y f).c.app W).hom)

Crystalline.firstOrderThickeningP₁Hom_comp_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 428. The attribute's comment: “p₀ and p₁ agree over the base”.

p₀ and p₁ are morphisms over the base Y, and they agree there: their difference is the universal divided power derivation, which kills every section pulled back from Y.

public theorem firstOrderThickeningP₁Hom_comp_base :
    firstOrderThickeningP₁Hom T Y f ≫ f = firstOrderThickeningProjHom T Y f ≫ f

Crystalline.GlobalCrystallineSituation.firstOrderThickeningIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 511. The attribute's comment: “the ideal J' as a sheaf of ideals on T'”.

The extended ideal J' = J ⊕ Ω_{T/S,δ} as a sheaf of ideals on T'.

public def firstOrderThickeningIdealSheaf :
    (SheafOfModules.unit (firstOrderThickeningScheme A.thickening.target S.S.scheme
      A.toBase.hom).ringCatSheaf).Submodule

Crystalline.GlobalCrystallineSituation.firstOrderThickeningIdealSheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 572. The attribute's comment: “the ideal J' is quasi-coherent”.

The extended ideal J' is quasi-coherent, being the ideal sheaf of the closed immersion U ⟶ T'.

public theorem firstOrderThickeningIdealSheaf_isQuasicoherent :
    (firstOrderThickeningIdealSheaf S A).toSheafOfModules.IsQuasicoherent

Crystalline.GlobalCrystallineSituation.firstOrderThickeningDPScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 584. The attribute's comment: “T' with the ideal J' and the divided powers δ' is a divided power scheme”.

The divided power scheme (T', J', δ'). The scheme T', the quasi-coherent ideal J' = J ⊕ Ω_{T/S,δ} and the divided power structure δ' of [Stacks, Tag 07J2].

public abbrev firstOrderThickeningDPScheme : DividedPowerScheme.{u}

Crystalline.GlobalCrystallineSituation.firstOrderThickeningProjDP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 598. The attribute's comment: “p₀ is a morphism of divided power schemes”.

p₀ : T' ⟶ T is a morphism of divided power schemes.

public def firstOrderThickeningProjDP :
    firstOrderThickeningDPScheme S A ⟶ A.thickening.target

Crystalline.GlobalCrystallineSituation.firstOrderThickeningP₁DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 606. The attribute's comment: “p₁ is a morphism of divided power schemes”.

p₁ : T' ⟶ T is a morphism of divided power schemes.

public def firstOrderThickeningP₁DP :
    firstOrderThickeningDPScheme S A ⟶ A.thickening.target

Crystalline.GlobalCrystallineSituation.firstOrderThickeningιDP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 614. The attribute's comment: “i is a morphism of divided power schemes”.

i : T ⟶ T' is a morphism of divided power schemes.

public def firstOrderThickeningιDP :
    A.thickening.target ⟶ firstOrderThickeningDPScheme S A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 623. The attribute's comment: “U ⟶ T' is a divided power thickening”.

The divided power thickening U ⟶ T': a thickening of schemes whose defining ideal is the divided power ideal J'.

public abbrev firstOrderThickeningSchemeThickening : SchemeThickening.{u}

Crystalline.GlobalCrystallineSituation.firstOrderThickeningObject, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 641. The attribute's comment: “(U, T', δ') is an object of CRIS(X/S)”.

(U, T', δ') is an object of CRIS(X/S). This is the assertion of [Stacks, Tag 07J2] that the first-order universal thickening of an object of the crystalline category is again an object of it: T' with the ideal J' = J ⊕ Ω_{T/S,δ} and the divided powers δ' is a divided power scheme, U ⟶ T' is a divided power thickening, and T' ⟶ S is p₀ followed by the structure morphism of T.

public abbrev firstOrderThickeningObject : Thickening S

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 659. The attribute's comment: “the morphism i of CRIS(X/S)”.

The morphism i : (U, T, δ) ⟶ (U, T', δ') of CRIS(X/S).

public def firstOrderThickeningSiteι : A ⟶ firstOrderThickeningObject S A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteP₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 677. The attribute's comment: “the morphism p₀ of CRIS(X/S)”.

The morphism p₀ : (U, T', δ') ⟶ (U, T, δ) of CRIS(X/S).

public def firstOrderThickeningSiteP₀ : firstOrderThickeningObject S A ⟶ A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteP₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 695. The attribute's comment: “the morphism p₁ of CRIS(X/S)”.

The morphism p₁ : (U, T', δ') ⟶ (U, T, δ) of CRIS(X/S). It is a morphism over the divided power base because p₁ and p₀ agree after composing with the structure morphism of T, the universal divided power derivation killing every section pulled back from S.

public def firstOrderThickeningSiteP₁ : firstOrderThickeningObject S A ⟶ A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteι_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 720. The attribute's comment: “the diagram relation p₀ ∘ i = id in CRIS(X/S)”.

p₀ ∘ i = id in CRIS(X/S), the left relation of the diagram of [Stacks, Tag 07J2].

public theorem firstOrderThickeningSiteι_comp_P₀ :
    firstOrderThickeningSiteι S A ≫ firstOrderThickeningSiteP₀ S A = 𝟙 A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteι_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 730. The attribute's comment: “the diagram relation p₁ ∘ i = id in CRIS(X/S)”.

p₁ ∘ i = id in CRIS(X/S), the right relation of the diagram of [Stacks, Tag 07J2].

public theorem firstOrderThickeningSiteι_comp_P₁ :
    firstOrderThickeningSiteι S A ≫ firstOrderThickeningSiteP₁ S A = 𝟙 A

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteι_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 741. The attribute's comment: “i is a first-order thickening with ideal sheaf Ω_{T/S,δ}”.

i : (U, T, δ) ⟶ (U, T', δ') is a first-order thickening whose ideal sheaf is Ω_{T/S,δ}, which is the restriction (Ω_{X/S})_T of the crystalline differentials by [Stacks, Tag 07IZ].

public theorem firstOrderThickeningSiteι_isFirstOrderThickening :
    Stacks.Thickenings.IsFirstOrderThickening
      (firstOrderThickeningSiteι S A).targetHom.hom

Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteKernelEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 752. The attribute's comment: “the ideal sheaf of i is the restriction of Ω_{X/S} to T”.

The ideal sheaf of i : T ⟶ T' is (Ω_{X/S})_T, the restriction of the crystalline differentials to the ambient scheme of the object — which is the spelling in which [Stacks, Tag 07J2] states it. Over every open the kernel of the map on sections of i is the sheaf Ω_{T/S,δ} of divided power differentials, and [Stacks, Tag 07IZ] identifies that sheaf with (Ω_{X/S})_T.

public def firstOrderThickeningSiteKernelEquiv
    (W : (Opens ↑(firstOrderThickeningScheme A.thickening.target S.S.scheme
      A.toBase.hom))ᵒᵖ) :
    ↑((restrictedCrysDifferentialsSheaf S A).val.obj
        (firstOrderThickeningOpen A.thickening.target S.S.scheme A.toBase.hom W)) ≃+
      RingHom.ker (((firstOrderThickeningι A.thickening.target S.S.scheme
        A.toBase.hom).c.app W).hom)

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 773. The attribute's comment: “(U, T', δ') is an object of Cris(X/S)”.

(U, T', δ') is an object of the small crystalline category Cris(X/S) whenever (U, T, δ) is. The construction leaves the map U ⟶ X untouched, so it is still an open immersion; this is the assertion of [Stacks, Tag 07J2] in the category in which the remark states it.

public def firstOrderThickeningCrysObject : CrystallineThickening S

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 778. The attribute's comment: “the morphism i of the diagram in Cris(X/S)”.

The morphism i : (U, T, δ) ⟶ (U, T', δ') of Cris(X/S).

public def firstOrderThickeningCrysι : B ⟶ firstOrderThickeningCrysObject S B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysP₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 783. The attribute's comment: “the morphism p₀ of the diagram in Cris(X/S)”.

The morphism p₀ : (U, T', δ') ⟶ (U, T, δ) of Cris(X/S).

public def firstOrderThickeningCrysP₀ : firstOrderThickeningCrysObject S B ⟶ B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysP₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 788. The attribute's comment: “the morphism p₁ of the diagram in Cris(X/S)”.

The morphism p₁ : (U, T', δ') ⟶ (U, T, δ) of Cris(X/S).

public def firstOrderThickeningCrysP₁ : firstOrderThickeningCrysObject S B ⟶ B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysι_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 794. The attribute's comment: “the diagram relation p₀ ∘ i = id in Cris(X/S)”.

p₀ ∘ i = id in Cris(X/S), the left relation of the diagram of [Stacks, Tag 07J2].

public theorem firstOrderThickeningCrysι_comp_P₀ :
    firstOrderThickeningCrysι S B ≫ firstOrderThickeningCrysP₀ S B = 𝟙 B

Crystalline.GlobalCrystallineSituation.firstOrderThickeningCrysι_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/UniversalThickeningScheme.lean, line 802. The attribute's comment: “the diagram relation p₁ ∘ i = id in Cris(X/S)”.

p₁ ∘ i = id in Cris(X/S), the right relation of the diagram of [Stacks, Tag 07J2].

public theorem firstOrderThickeningCrysι_comp_P₁ :
    firstOrderThickeningCrysι S B ≫ firstOrderThickeningCrysP₁ S B = 𝟙 B

Tag 07J3, a remark

Tag 07J3 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalConnectionSecondOrder.lean, line 82. The attribute's comment: “the second-order thickening as an object of CRIS(X/S) together with q₁₂ and the two relations q₁ = q₁₂ ∘ p₀, q₂ = q₁₂ ∘ p₁, in the shape in which the integrability argument of 07J6 consumes them”.

The second-order universal thickening of [Stacks, Tag 07J3] as an object of CRIS(X/S), with the morphism q₁₂ and the two relations the integrability argument consumes. Every field is a declaration of StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean: the object is Crystalline.GlobalCrystallineSituation.secondOrderThickeningObject, the morphisms are Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂, Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁ and Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₂, and the two relations are Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂_comp_P₀ and Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂_comp_P₁.

def secondOrderThickeningSiteData (A : Thickening S) : SecondOrderThickeningSiteData A

Crystalline.secondOrderThickeningPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1230. The attribute's comment: “the structure sheaf of the second-order thickening”.

The structure sheaf of the second-order universal thickening T'' of a divided power scheme T over Y: the presheaf of commutative rings 𝒪_T ⊕ Ω_{T/Y,δ} ⊕ Ω_{T/Y,δ} ⊕ Ω²_{T/Y,δ} whose multiplication is corrected in the last coordinate by the exterior product of the two middle coordinates. All four summands are sheaves.

public def secondOrderThickeningPresheaf : (Opens ↑T.scheme)ᵒᵖ ⥤ CommRingCat.{u}

Crystalline.secondOrderThickeningSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1237. The attribute's comment: “the structure sheaf of the second-order thickening is a sheaf”.

The structure sheaf of the second-order universal thickening, as a sheaf: all four summands 𝒪_T, Ω_{T/Y,δ}, Ω_{T/Y,δ} and Ω²_{T/Y,δ} are sheaves, so the second-order extension satisfies the sheaf condition.

public def secondOrderThickeningSheaf : TopCat.Sheaf CommRingCat.{u} ↑T.scheme

Crystalline.secondOrderThickening_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1251. The attribute's comment: “the multiplication of the second-order thickening”.

The multiplication of 𝒪_{T''} in coordinates.

public theorem secondOrderThickening_mul (W : (Opens ↑T.scheme)ᵒᵖ)
    (x y : SecondOrderExt (dpWedge T Y f) W) :
    (secondOrderExtFst (x * y) = secondOrderExtFst x * secondOrderExtFst y ∧
      secondOrderExtLeft (x * y) =
        secondOrderExtFst x • secondOrderExtLeft y +
          secondOrderExtFst y • secondOrderExtLeft x) ∧
    secondOrderExtRight (x * y) =
        secondOrderExtFst x • secondOrderExtRight y +
          secondOrderExtFst y • secondOrderExtRight x ∧
      secondOrderExtTop (x * y) =
        secondOrderExtFst x • secondOrderExtTop y + secondOrderExtFst y • secondOrderExtTop x +
          (dpWedge T Y f).app W (secondOrderExtLeft x) (secondOrderExtRight y) +
          (dpWedge T Y f).app W (secondOrderExtLeft y) (secondOrderExtRight x)

Crystalline.secondOrderThickeningIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1269. The attribute's comment: “the ideal J'' of the second-order thickening”.

The ideal J'' of the second-order universal thickening: the inverse image of the divided power ideal of T under the projection 𝒪_{T''} → 𝒪_T.

public def secondOrderThickeningIdeal (W : (Opens ↑T.scheme)ᵒᵖ) :
    Ideal (SecondOrderExt (dpWedge T Y f) W)

Crystalline.secondOrderThickeningDividedPowers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1276. The attribute's comment: “the divided power structure on J''”.

The divided power structure δ'' on the ideal J'' of the second-order universal thickening.

public def secondOrderThickeningDividedPowers (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers (secondOrderThickeningIdeal T Y f W)

Crystalline.secondOrderThickeningDividedPowers_dpow_add_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1284. The attribute's comment: “the divided power formula on J''”.

The displayed formula for δ'': δ''\_\{k+2}(f, ω₁, ω₂, η) = (δ\_\{k+2} f, δ\_\{k+1} f · ω₁, δ\_\{k+1} f · ω₂, δ\_\{k+1} f · η + δ\_k f · ω₁ ∧ ω₂).

public theorem secondOrderThickeningDividedPowers_dpow_add_two (W : (Opens ↑T.scheme)ᵒᵖ) (k : ℕ)
    {x : SecondOrderExt (dpWedge T Y f) W} (hx : x ∈ secondOrderThickeningIdeal T Y f W) :
    (secondOrderThickeningDividedPowers T Y f W).dpow (k + 2) x =
      secondOrderExtMk
        ((T.dividedPowers.dividedPowers W).dpow (k + 2) (secondOrderExtFst x))
        ((T.dividedPowers.dividedPowers W).dpow (k + 1) (secondOrderExtFst x) •
          secondOrderExtLeft x)
        ((T.dividedPowers.dividedPowers W).dpow (k + 1) (secondOrderExtFst x) •
          secondOrderExtRight x)
        ((T.dividedPowers.dividedPowers W).dpow (k + 1) (secondOrderExtFst x) •
            secondOrderExtTop x +
          (T.dividedPowers.dividedPowers W).dpow k (secondOrderExtFst x) •
            (dpWedge T Y f).app W (secondOrderExtLeft x) (secondOrderExtRight x))

Crystalline.secondOrderThickening_restriction_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1303. The attribute's comment: “the divided powers on J'' are compatible with restriction”.

Every restriction map of 𝒪_{T''} is compatible with the divided powers of J'', so the rings of sections of 𝒪_{T''} with the ideals J'' and the structures δ'' form a presheaf of divided power rings.

public theorem secondOrderThickening_restriction_isDPMorphism
    {W W' : (Opens ↑T.scheme)ᵒᵖ} (i : W ⟶ W') :
    DividedPowers.IsDPMorphism (secondOrderThickeningDividedPowers T Y f W)
      (secondOrderThickeningDividedPowers T Y f W')
      (secondOrderExtRingHom (dpWedge T Y f) i)

Crystalline.secondOrderThickeningQ₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1340. The attribute's comment: “the map q₀”.

The first of the three maps 𝒪_T → 𝒪_{T''}, f ↦ (f, 0, 0, 0).

public def secondOrderThickeningQ₀ :
    T.scheme.sheaf.obj ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1348. The attribute's comment: “the map q₁”.

The second of the three maps 𝒪_T → 𝒪_{T''}, f ↦ (f, d f, 0, 0).

public def secondOrderThickeningQ₁ :
    T.scheme.sheaf.obj ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1359. The attribute's comment: “the map q₂”.

The third of the three maps 𝒪_T → 𝒪_{T''}, f ↦ (f, d f, d f, 0). It is multiplicative because the exterior product is antisymmetric.

public def secondOrderThickeningQ₂ :
    T.scheme.sheaf.obj ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₀₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1384. The attribute's comment: “the map q₀₁”.

The map q₀₁ : 𝒪_{T'} → 𝒪_{T''}, (f, ω) ↦ (f, ω, 0, 0).

public def secondOrderThickeningQ₀₁ :
    firstOrderThickeningPresheaf T Y f ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₀₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1394. The attribute's comment: “the map q₀₂”.

The map q₀₂ : 𝒪_{T'} → 𝒪_{T''}, (f, ω) ↦ (f, ω, ω, 0). It is multiplicative because the exterior product is antisymmetric.

public def secondOrderThickeningQ₀₂ :
    firstOrderThickeningPresheaf T Y f ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₀_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1406. The attribute's comment: “q₀ is compatible with the divided powers”.

q₀ is compatible with the divided power structures on J and J''.

public theorem secondOrderThickeningQ₀_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (T.dividedPowers.dividedPowers W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₀ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₁_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1420. The attribute's comment: “q₁ is compatible with the divided powers”.

q₁ is compatible with the divided power structures on J and J'', because the universal divided power derivation obeys the divided power chain rule and the exterior product of a differential with zero vanishes.

public theorem secondOrderThickeningQ₁_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (T.dividedPowers.dividedPowers W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₁ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₂_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1434. The attribute's comment: “q₂ is compatible with the divided powers”.

q₂ is compatible with the divided power structures on J and J'', because the universal divided power derivation obeys the divided power chain rule and the exterior product of a differential with itself vanishes.

public theorem secondOrderThickeningQ₂_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (T.dividedPowers.dividedPowers W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₂ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₀₁_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1447. The attribute's comment: “q₀₁ is compatible with the divided powers”.

q₀₁ is compatible with the divided power structures on J' and J''.

public theorem secondOrderThickeningQ₀₁_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (firstOrderThickeningDividedPowers T Y f W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₀₁ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₀₂_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1461. The attribute's comment: “q₀₂ is compatible with the divided powers”.

q₀₂ is compatible with the divided power structures on J' and J'', because the exterior product of a differential with itself vanishes.

public theorem secondOrderThickeningQ₀₂_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (firstOrderThickeningDividedPowers T Y f W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₀₂ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₀_eq_Q₀₁_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1478. The attribute's comment: “q₀ = q₀₁ ∘ p₀”.

q₀ = q₀₁ ∘ p₀.

public theorem secondOrderThickeningQ₀_eq_Q₀₁_comp_P₀ :
    firstOrderThickeningP₀ T Y f ≫ secondOrderThickeningQ₀₁ T Y f =
      secondOrderThickeningQ₀ T Y f

Crystalline.secondOrderThickeningQ₁_eq_Q₀₁_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1485. The attribute's comment: “q₁ = q₀₁ ∘ p₁”.

q₁ = q₀₁ ∘ p₁.

public theorem secondOrderThickeningQ₁_eq_Q₀₁_comp_P₁ :
    firstOrderThickeningP₁ T Y f ≫ secondOrderThickeningQ₀₁ T Y f =
      secondOrderThickeningQ₁ T Y f

Crystalline.secondOrderThickeningQ₀_eq_Q₀₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1492. The attribute's comment: “q₀ = q₀₂ ∘ p₀”.

q₀ = q₀₂ ∘ p₀.

public theorem secondOrderThickeningQ₀_eq_Q₀₂_comp_P₀ :
    firstOrderThickeningP₀ T Y f ≫ secondOrderThickeningQ₀₂ T Y f =
      secondOrderThickeningQ₀ T Y f

Crystalline.secondOrderThickeningQ₂_eq_Q₀₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickening.lean, line 1499. The attribute's comment: “q₂ = q₀₂ ∘ p₁”.

q₂ = q₀₂ ∘ p₁.

public theorem secondOrderThickeningQ₂_eq_Q₀₂_comp_P₁ :
    firstOrderThickeningP₁ T Y f ≫ secondOrderThickeningQ₀₂ T Y f =
      secondOrderThickeningQ₂ T Y f

Crystalline.secondOrderThickeningQ₁₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningDeRham.lean, line 595. The attribute's comment: “the map q₁₂”.

The map q₁₂ : 𝒪_{T'} → 𝒪_{T''}, (f, ω) ↦ (f, d f, ω, d ω). It is multiplicative because the de Rham differential obeys the Leibniz rule d (f η + g ω) = f (d η) + g (d ω) + (d f) ∧ η + (d g) ∧ ω, which is exactly the correction term of the second-order multiplication.

public def secondOrderThickeningQ₁₂ :
    firstOrderThickeningPresheaf T Y f ⟶ secondOrderThickeningPresheaf T Y f

Crystalline.secondOrderThickeningQ₁₂_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningDeRham.lean, line 649. The attribute's comment: “q₁₂ is compatible with the divided powers”.

q₁₂ is compatible with the divided power structures on J' and J'', because the universal divided power derivation obeys the divided power chain rule and the de Rham differential obeys its divided power Leibniz rule d (δ_{k+1}(f) ω) = δ_{k+1}(f) (d ω) + δ_k(f) ((d f) ∧ ω).

public theorem secondOrderThickeningQ₁₂_isDPMorphism (W : (Opens ↑T.scheme)ᵒᵖ) :
    DividedPowers.IsDPMorphism (firstOrderThickeningDividedPowers T Y f W)
      (secondOrderThickeningDividedPowers T Y f W)
      (((secondOrderThickeningQ₁₂ T Y f).app W).hom)

Crystalline.secondOrderThickeningQ₁_eq_Q₁₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningDeRham.lean, line 676. The attribute's comment: “q₁ = q₁₂ ∘ p₀”.

q₁ = q₁₂ ∘ p₀, the two-form coordinate because the de Rham differential of the zero differential vanishes.

public theorem secondOrderThickeningQ₁_eq_Q₁₂_comp_P₀ :
    firstOrderThickeningP₀ T Y f ≫ secondOrderThickeningQ₁₂ T Y f =
      secondOrderThickeningQ₁ T Y f

Crystalline.secondOrderThickeningQ₂_eq_Q₁₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningDeRham.lean, line 685. The attribute's comment: “q₂ = q₁₂ ∘ p₁”.

q₂ = q₁₂ ∘ p₁, the two-form coordinate because the de Rham differential kills every exact differential.

public theorem secondOrderThickeningQ₂_eq_Q₁₂_comp_P₁ :
    firstOrderThickeningP₁ T Y f ≫ secondOrderThickeningQ₁₂ T Y f =
      secondOrderThickeningQ₂ T Y f

Crystalline.secondOrderThickening_ker_cube, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningOrder.lean, line 301. The attribute's comment: “T → T'' is a second-order thickening of sheaves of rings”.

T → T'' is a second-order thickening: the ideal of the projection 𝒪_{T''} → 𝒪_T has vanishing cube on every open. Its square lies in the top summand, and the top summand annihilates it.

public theorem secondOrderThickening_ker_cube (W : (Opens ↑T.scheme)ᵒᵖ) :
    RingHom.ker (secondOrderExtFstHom (dpWedge T Y f) W) ^ 3 = ⊥

Crystalline.secondOrderThickeningScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 256. The attribute's comment: “the second-order thickening T'' as a scheme”.

The second-order universal thickening T'' as a scheme. The topological space of T equipped with the structure sheaf 𝒪_{T''} = 𝒪_T ⊕ Ω_{T/Y,δ} ⊕ Ω_{T/Y,δ} ⊕ Ω²_{T/Y,δ}; it is a scheme because it is isomorphic, as a locally ringed space, to the realization of the square-zero extension of 𝒪_{T'} by K.

public def secondOrderThickeningScheme : Scheme.{u}

Crystalline.secondOrderThickeningι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 291. The attribute's comment: “the immersion T' ⟶ T'' of schemes”.

The immersion j : T' ⟶ T'', whose map on sections is the projection 𝒪_{T''} ⟶ 𝒪_{T'}.

public def secondOrderThickeningι :
    firstOrderThickeningScheme T Y f ⟶ secondOrderThickeningScheme T Y f

Crystalline.secondOrderThickeningιT, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 306. The attribute's comment: “the immersion T ⟶ T'' of schemes”.

The immersion T ⟶ T'': the immersion T ⟶ T' followed by T' ⟶ T''. Its map on sections is Crystalline.secondOrderThickeningFstProj, the projection 𝒪_{T''} ⟶ 𝒪_T.

public def secondOrderThickeningιT : T.scheme ⟶ secondOrderThickeningScheme T Y f

Crystalline.secondOrderThickeningQ₀₁Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 367. The attribute's comment: “the morphism q₀₁ : T'' ⟶ T' of schemes”.

The morphism q₀₁ : T'' ⟶ T', induced by the map (g, ω) ↦ (g, ω, 0, 0) of structure sheaves.

public def secondOrderThickeningQ₀₁Hom :
    secondOrderThickeningScheme T Y f ⟶ firstOrderThickeningScheme T Y f

Crystalline.secondOrderThickeningQ₀₂Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 381. The attribute's comment: “the morphism q₀₂ : T'' ⟶ T' of schemes”.

The morphism q₀₂ : T'' ⟶ T', induced by the map (g, ω) ↦ (g, ω, ω, 0) of structure sheaves.

public def secondOrderThickeningQ₀₂Hom :
    secondOrderThickeningScheme T Y f ⟶ firstOrderThickeningScheme T Y f

Crystalline.secondOrderThickeningQ₁₂Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 395. The attribute's comment: “the morphism q₁₂ : T'' ⟶ T' of schemes”.

The morphism q₁₂ : T'' ⟶ T', induced by the map (g, ω) ↦ (g, d g, ω, d ω) of structure sheaves.

public def secondOrderThickeningQ₁₂Hom :
    secondOrderThickeningScheme T Y f ⟶ firstOrderThickeningScheme T Y f

Crystalline.secondOrderThickeningQ₀Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 410. The attribute's comment: “the morphism q₀ : T'' ⟶ T of schemes”.

The morphism q₀ : T'' ⟶ T, the composite of q₀₁ with p₀; on sections this is the relation q₀ = q₀₁ ∘ p₀ of [Stacks, Tag 07J3].

public def secondOrderThickeningQ₀Hom : secondOrderThickeningScheme T Y f ⟶ T.scheme

Crystalline.secondOrderThickeningQ₁Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 416. The attribute's comment: “the morphism q₁ : T'' ⟶ T of schemes”.

The morphism q₁ : T'' ⟶ T, the composite of q₀₁ with p₁; on sections this is the relation q₁ = q₀₁ ∘ p₁.

public def secondOrderThickeningQ₁Hom : secondOrderThickeningScheme T Y f ⟶ T.scheme

Crystalline.secondOrderThickeningQ₂Hom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 422. The attribute's comment: “the morphism q₂ : T'' ⟶ T of schemes”.

The morphism q₂ : T'' ⟶ T, the composite of q₁₂ with p₁; on sections this is the relation q₂ = q₁₂ ∘ p₁.

public def secondOrderThickeningQ₂Hom : secondOrderThickeningScheme T Y f ⟶ T.scheme

Crystalline.secondOrderThickeningQ₀Hom_eq_Q₀₁_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 496. The attribute's comment: “the relation q₀ = q₀₁ ∘ p₀, for schemes”.

q₀ = q₀₁ ∘ p₀ for schemes, the first relation of [Stacks, Tag 07J3]; it holds by the definition of q₀.

public theorem secondOrderThickeningQ₀Hom_eq_Q₀₁_comp_P₀ :
    secondOrderThickeningQ₀₁Hom T Y f ≫ firstOrderThickeningProjHom T Y f =
      secondOrderThickeningQ₀Hom T Y f

Crystalline.secondOrderThickeningQ₁Hom_eq_Q₀₁_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 502. The attribute's comment: “the relation q₁ = q₀₁ ∘ p₁, for schemes”.

q₁ = q₀₁ ∘ p₁ for schemes; it holds by the definition of q₁.

public theorem secondOrderThickeningQ₁Hom_eq_Q₀₁_comp_P₁ :
    secondOrderThickeningQ₀₁Hom T Y f ≫ firstOrderThickeningP₁Hom T Y f =
      secondOrderThickeningQ₁Hom T Y f

Crystalline.secondOrderThickeningQ₂Hom_eq_Q₁₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 508. The attribute's comment: “the relation q₂ = q₁₂ ∘ p₁, for schemes”.

q₂ = q₁₂ ∘ p₁ for schemes; it holds by the definition of q₂.

public theorem secondOrderThickeningQ₂Hom_eq_Q₁₂_comp_P₁ :
    secondOrderThickeningQ₁₂Hom T Y f ≫ firstOrderThickeningP₁Hom T Y f =
      secondOrderThickeningQ₂Hom T Y f

Crystalline.secondOrderThickeningQ₁Hom_eq_Q₁₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 515. The attribute's comment: “the relation q₁ = q₁₂ ∘ p₀, for schemes”.

q₁ = q₁₂ ∘ p₀ for schemes, which on sections is Crystalline.secondOrderThickeningQ₁_eq_Q₁₂_comp_P₀.

public theorem secondOrderThickeningQ₁Hom_eq_Q₁₂_comp_P₀ :
    secondOrderThickeningQ₁₂Hom T Y f ≫ firstOrderThickeningProjHom T Y f =
      secondOrderThickeningQ₁Hom T Y f

Crystalline.secondOrderThickeningQ₀Hom_eq_Q₀₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 527. The attribute's comment: “the relation q₀ = q₀₂ ∘ p₀, for schemes”.

q₀ = q₀₂ ∘ p₀ for schemes, which on sections is Crystalline.secondOrderThickeningQ₀_eq_Q₀₂_comp_P₀.

public theorem secondOrderThickeningQ₀Hom_eq_Q₀₂_comp_P₀ :
    secondOrderThickeningQ₀₂Hom T Y f ≫ firstOrderThickeningProjHom T Y f =
      secondOrderThickeningQ₀Hom T Y f

Crystalline.secondOrderThickeningQ₂Hom_eq_Q₀₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 539. The attribute's comment: “the relation q₂ = q₀₂ ∘ p₁, for schemes”.

q₂ = q₀₂ ∘ p₁ for schemes, which on sections is Crystalline.secondOrderThickeningQ₂_eq_Q₀₂_comp_P₁.

public theorem secondOrderThickeningQ₂Hom_eq_Q₀₂_comp_P₁ :
    secondOrderThickeningQ₀₂Hom T Y f ≫ firstOrderThickeningP₁Hom T Y f =
      secondOrderThickeningQ₂Hom T Y f

Crystalline.secondOrderThickeningι_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 570. The attribute's comment: “T' ⟶ T'' is a first-order thickening of schemes”.

T' ⟶ T'' is a first-order thickening of schemes: its ideal sheaf has square zero, because the kernel of 𝒪_{T''} ⟶ 𝒪_{T'} over every open is the square-zero ideal K = 0 ⊕ 0 ⊕ Ω_{T/Y,δ} ⊕ Ω²_{T/Y,δ}.

public theorem secondOrderThickeningι_isFirstOrderThickening :
    Stacks.Thickenings.IsFirstOrderThickening (secondOrderThickeningι T Y f)

Crystalline.secondOrderThickeningιT_isNthOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 596. The attribute's comment: “T → T'' is a second-order thickening of schemes”.

T → T'' is a second-order thickening of schemes, which is the description of T'' in [Stacks, Tag 07J3]. The ideal sheaf of T ⟶ T'' is the kernel of 𝒪_{T''} ⟶ 𝒪_T, whose cube vanishes on every open by Crystalline.secondOrderThickening_ker_cube.

The order is not obtained by composing the two first-order thickenings T ⟶ T' and T' ⟶ T'': a composite of two first-order thickenings is in general only of order three — for Z = Spec k[x]/(x⁴), the closed subschemes cut out by (x²) and by (x) give first-order thickenings whose composite has (x)³ ≠ 0 — and what makes the order here two is the explicit vanishing of the cube in the sheaf-level computation.

public theorem secondOrderThickeningιT_isNthOrderThickening :
    Stacks.Thickenings.IsNthOrderThickening 2 (secondOrderThickeningιT T Y f)

Crystalline.secondOrderThickeningιT_comp_Q₀Hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 688. The attribute's comment: “the relation q₀ ∘ (T ⟶ T'') = id”.

q₀ retracts the immersion T ⟶ T''.

public theorem secondOrderThickeningιT_comp_Q₀Hom :
    secondOrderThickeningιT T Y f ≫ secondOrderThickeningQ₀Hom T Y f = 𝟙 T.scheme

Crystalline.secondOrderThickeningιT_comp_Q₁Hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 697. The attribute's comment: “the relation q₁ ∘ (T ⟶ T'') = id”.

q₁ retracts the immersion T ⟶ T''.

public theorem secondOrderThickeningιT_comp_Q₁Hom :
    secondOrderThickeningιT T Y f ≫ secondOrderThickeningQ₁Hom T Y f = 𝟙 T.scheme

Crystalline.secondOrderThickeningιT_comp_Q₂Hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 706. The attribute's comment: “the relation q₂ ∘ (T ⟶ T'') = id”.

q₂ retracts the immersion T ⟶ T''.

public theorem secondOrderThickeningιT_comp_Q₂Hom :
    secondOrderThickeningιT T Y f ≫ secondOrderThickeningQ₂Hom T Y f = 𝟙 T.scheme

Crystalline.GlobalCrystallineSituation.secondOrderThickeningIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 739. The attribute's comment: “the ideal J'' as a sheaf of ideals on T''”.

The extended ideal J'' as a sheaf of ideals on T'': the sections of 𝒪_{T''} whose component in 𝒪_T lies in the divided power ideal J of T.

public def secondOrderThickeningIdealSheaf :
    (SheafOfModules.unit (secondOrderThickeningScheme A.thickening.target S.S.scheme
      A.toBase.hom).ringCatSheaf).Submodule

Crystalline.GlobalCrystallineSituation.secondOrderThickeningIdealSheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 799. The attribute's comment: “the ideal J'' is quasi-coherent”.

The extended ideal J'' is quasi-coherent, being the ideal sheaf of the closed immersion U ⟶ T''.

public theorem secondOrderThickeningIdealSheaf_isQuasicoherent :
    (secondOrderThickeningIdealSheaf S A).toSheafOfModules.IsQuasicoherent

Crystalline.GlobalCrystallineSituation.secondOrderThickeningDPScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 809. The attribute's comment: “T'' with the ideal J'' and the divided powers δ'' is a divided power scheme”.

The divided power scheme (T'', J'', δ''). The scheme T'', the quasi-coherent ideal J'' and the divided power structure δ'' of [Stacks, Tag 07J3].

public abbrev secondOrderThickeningDPScheme : DividedPowerScheme.{u}

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₀DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 825. The attribute's comment: “q₀ is a morphism of divided power schemes”.

q₀ : T'' ⟶ T is a morphism of divided power schemes.

public def secondOrderThickeningQ₀DP :
    secondOrderThickeningDPScheme S A ⟶ A.thickening.target

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₁DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 833. The attribute's comment: “q₁ is a morphism of divided power schemes”.

q₁ : T'' ⟶ T is a morphism of divided power schemes.

public def secondOrderThickeningQ₁DP :
    secondOrderThickeningDPScheme S A ⟶ A.thickening.target

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₂DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 841. The attribute's comment: “q₂ is a morphism of divided power schemes”.

q₂ : T'' ⟶ T is a morphism of divided power schemes.

public def secondOrderThickeningQ₂DP :
    secondOrderThickeningDPScheme S A ⟶ A.thickening.target

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₀₁DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 851. The attribute's comment: “q₀₁ is a morphism of divided power schemes”.

q₀₁ : T'' ⟶ T' is a morphism of divided power schemes.

public def secondOrderThickeningQ₀₁DP :
    secondOrderThickeningDPScheme S A ⟶ firstOrderThickeningDPScheme S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₀₂DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 859. The attribute's comment: “q₀₂ is a morphism of divided power schemes”.

q₀₂ : T'' ⟶ T' is a morphism of divided power schemes.

public def secondOrderThickeningQ₀₂DP :
    secondOrderThickeningDPScheme S A ⟶ firstOrderThickeningDPScheme S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningQ₁₂DP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 867. The attribute's comment: “q₁₂ is a morphism of divided power schemes”.

q₁₂ : T'' ⟶ T' is a morphism of divided power schemes.

public def secondOrderThickeningQ₁₂DP :
    secondOrderThickeningDPScheme S A ⟶ firstOrderThickeningDPScheme S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSchemeThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 878. The attribute's comment: “U ⟶ T'' is a divided power thickening”.

The divided power thickening U ⟶ T'': a thickening of schemes whose defining ideal is the divided power ideal J''.

public abbrev secondOrderThickeningSchemeThickening : SchemeThickening.{u}

Crystalline.GlobalCrystallineSituation.secondOrderThickeningObject, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 897. The attribute's comment: “(U, T'', δ'') is an object of CRIS(X/S)”.

(U, T'', δ'') is an object of CRIS(X/S). This is the final assertion of [Stacks, Tag 07J3]: the second-order universal thickening of an object of the crystalline category is again an object of it. T'' with the ideal J'' = J ⊕ Ω_{T/S,δ} ⊕ Ω_{T/S,δ} ⊕ Ω²_{T/S,δ} and the divided powers δ'' of the remark is a divided power scheme, U ⟶ T'' is a divided power thickening, and T'' ⟶ S is q₀ followed by the structure morphism of T.

public abbrev secondOrderThickeningObject : Thickening S

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 917. The attribute's comment: “the morphism q₀ of CRIS(X/S)”.

The morphism q₀ : (U, T'', δ'') ⟶ (U, T, δ) of CRIS(X/S).

public def secondOrderThickeningSiteQ₀ : secondOrderThickeningObject S A ⟶ A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 935. The attribute's comment: “the morphism q₁ of CRIS(X/S)”.

The morphism q₁ : (U, T'', δ'') ⟶ (U, T, δ) of CRIS(X/S). It is a morphism over the divided power base because q₁ and q₀ agree after composing with the structure morphism of T.

public def secondOrderThickeningSiteQ₁ : secondOrderThickeningObject S A ⟶ A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 958. The attribute's comment: “the morphism q₂ of CRIS(X/S)”.

The morphism q₂ : (U, T'', δ'') ⟶ (U, T, δ) of CRIS(X/S).

public def secondOrderThickeningSiteQ₂ : secondOrderThickeningObject S A ⟶ A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 981. The attribute's comment: “the morphism q₀₁ of CRIS(X/S)”.

The morphism q₀₁ : (U, T'', δ'') ⟶ (U, T', δ') of CRIS(X/S).

public def secondOrderThickeningSiteQ₀₁ :
    secondOrderThickeningObject S A ⟶ firstOrderThickeningObject S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1011. The attribute's comment: “the morphism q₀₂ of CRIS(X/S)”.

The morphism q₀₂ : (U, T'', δ'') ⟶ (U, T', δ') of CRIS(X/S).

public def secondOrderThickeningSiteQ₀₂ :
    secondOrderThickeningObject S A ⟶ firstOrderThickeningObject S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1041. The attribute's comment: “the morphism q₁₂ of CRIS(X/S)”.

The morphism q₁₂ : (U, T'', δ'') ⟶ (U, T', δ') of CRIS(X/S).

public def secondOrderThickeningSiteQ₁₂ :
    secondOrderThickeningObject S A ⟶ firstOrderThickeningObject S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₁_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1073. The attribute's comment: “the relation q₀ = q₀₁ ∘ p₀ in CRIS(X/S)”.

q₀ = q₀₁ ∘ p₀ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₀₁_comp_P₀ :
    secondOrderThickeningSiteQ₀₁ S A ≫ firstOrderThickeningSiteP₀ S A =
      secondOrderThickeningSiteQ₀ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₁_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1081. The attribute's comment: “the relation q₁ = q₀₁ ∘ p₁ in CRIS(X/S)”.

q₁ = q₀₁ ∘ p₁ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₀₁_comp_P₁ :
    secondOrderThickeningSiteQ₀₁ S A ≫ firstOrderThickeningSiteP₁ S A =
      secondOrderThickeningSiteQ₁ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1089. The attribute's comment: “the relation q₁ = q₁₂ ∘ p₀ in CRIS(X/S)”.

q₁ = q₁₂ ∘ p₀ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₁₂_comp_P₀ :
    secondOrderThickeningSiteQ₁₂ S A ≫ firstOrderThickeningSiteP₀ S A =
      secondOrderThickeningSiteQ₁ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₁₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1097. The attribute's comment: “the relation q₂ = q₁₂ ∘ p₁ in CRIS(X/S)”.

q₂ = q₁₂ ∘ p₁ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₁₂_comp_P₁ :
    secondOrderThickeningSiteQ₁₂ S A ≫ firstOrderThickeningSiteP₁ S A =
      secondOrderThickeningSiteQ₂ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1105. The attribute's comment: “the relation q₀ = q₀₂ ∘ p₀ in CRIS(X/S)”.

q₀ = q₀₂ ∘ p₀ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₀₂_comp_P₀ :
    secondOrderThickeningSiteQ₀₂ S A ≫ firstOrderThickeningSiteP₀ S A =
      secondOrderThickeningSiteQ₀ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningSiteQ₀₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1113. The attribute's comment: “the relation q₂ = q₀₂ ∘ p₁ in CRIS(X/S)”.

q₂ = q₀₂ ∘ p₁ in CRIS(X/S), one of the six relations of [Stacks, Tag 07J3].

public theorem secondOrderThickeningSiteQ₀₂_comp_P₁ :
    secondOrderThickeningSiteQ₀₂ S A ≫ firstOrderThickeningSiteP₁ S A =
      secondOrderThickeningSiteQ₂ S A

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1128. The attribute's comment: “(U, T'', δ'') is an object of Cris(X/S)”.

(U, T'', δ'') is an object of the small crystalline category Cris(X/S) whenever (U, T, δ) is. The construction leaves the map U ⟶ X untouched, so it is still an open immersion; this is the assertion of [Stacks, Tag 07J3] in the category in which the remark states it.

public def secondOrderThickeningCrysObject : CrystallineThickening S

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1133. The attribute's comment: “the morphism q₀ of the diagram in Cris(X/S)”.

The morphism q₀ : (U, T'', δ'') ⟶ (U, T, δ) of Cris(X/S).

public def secondOrderThickeningCrysQ₀ : secondOrderThickeningCrysObject S B ⟶ B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1138. The attribute's comment: “the morphism q₁ of the diagram in Cris(X/S)”.

The morphism q₁ : (U, T'', δ'') ⟶ (U, T, δ) of Cris(X/S).

public def secondOrderThickeningCrysQ₁ : secondOrderThickeningCrysObject S B ⟶ B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1143. The attribute's comment: “the morphism q₂ of the diagram in Cris(X/S)”.

The morphism q₂ : (U, T'', δ'') ⟶ (U, T, δ) of Cris(X/S).

public def secondOrderThickeningCrysQ₂ : secondOrderThickeningCrysObject S B ⟶ B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1148. The attribute's comment: “the morphism q₀₁ of the diagram in Cris(X/S)”.

The morphism q₀₁ : (U, T'', δ'') ⟶ (U, T', δ') of Cris(X/S).

public def secondOrderThickeningCrysQ₀₁ :
    secondOrderThickeningCrysObject S B ⟶ firstOrderThickeningCrysObject S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1154. The attribute's comment: “the morphism q₀₂ of the diagram in Cris(X/S)”.

The morphism q₀₂ : (U, T'', δ'') ⟶ (U, T', δ') of Cris(X/S).

public def secondOrderThickeningCrysQ₀₂ :
    secondOrderThickeningCrysObject S B ⟶ firstOrderThickeningCrysObject S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₁₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1160. The attribute's comment: “the morphism q₁₂ of the diagram in Cris(X/S)”.

The morphism q₁₂ : (U, T'', δ'') ⟶ (U, T', δ') of Cris(X/S).

public def secondOrderThickeningCrysQ₁₂ :
    secondOrderThickeningCrysObject S B ⟶ firstOrderThickeningCrysObject S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₁_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1166. The attribute's comment: “the relation q₀ = q₀₁ ∘ p₀ in Cris(X/S)”.

q₀ = q₀₁ ∘ p₀ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₀₁_comp_P₀ :
    secondOrderThickeningCrysQ₀₁ S B ≫ firstOrderThickeningCrysP₀ S B =
      secondOrderThickeningCrysQ₀ S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₁_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1173. The attribute's comment: “the relation q₁ = q₀₁ ∘ p₁ in Cris(X/S)”.

q₁ = q₀₁ ∘ p₁ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₀₁_comp_P₁ :
    secondOrderThickeningCrysQ₀₁ S B ≫ firstOrderThickeningCrysP₁ S B =
      secondOrderThickeningCrysQ₁ S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₁₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1180. The attribute's comment: “the relation q₁ = q₁₂ ∘ p₀ in Cris(X/S)”.

q₁ = q₁₂ ∘ p₀ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₁₂_comp_P₀ :
    secondOrderThickeningCrysQ₁₂ S B ≫ firstOrderThickeningCrysP₀ S B =
      secondOrderThickeningCrysQ₁ S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₁₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1187. The attribute's comment: “the relation q₂ = q₁₂ ∘ p₁ in Cris(X/S)”.

q₂ = q₁₂ ∘ p₁ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₁₂_comp_P₁ :
    secondOrderThickeningCrysQ₁₂ S B ≫ firstOrderThickeningCrysP₁ S B =
      secondOrderThickeningCrysQ₂ S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₂_comp_P₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1194. The attribute's comment: “the relation q₀ = q₀₂ ∘ p₀ in Cris(X/S)”.

q₀ = q₀₂ ∘ p₀ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₀₂_comp_P₀ :
    secondOrderThickeningCrysQ₀₂ S B ≫ firstOrderThickeningCrysP₀ S B =
      secondOrderThickeningCrysQ₀ S B

Crystalline.GlobalCrystallineSituation.secondOrderThickeningCrysQ₀₂_comp_P₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningScheme.lean, line 1201. The attribute's comment: “the relation q₂ = q₀₂ ∘ p₁ in Cris(X/S)”.

q₂ = q₀₂ ∘ p₁ in Cris(X/S).

public theorem secondOrderThickeningCrysQ₀₂_comp_P₁ :
    secondOrderThickeningCrysQ₀₂ S B ≫ firstOrderThickeningCrysP₁ S B =
      secondOrderThickeningCrysQ₂ S B

Crystalline.GlobalCrystallineSituation.crysSheafRingMap_q₀₁_add_q₁₂_diffSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningSections.lean, line 367. The attribute's comment: “the first formula of the remark on the sections over an object: on a section of the square-zero summand of 𝒪_{T'}, q₀₁ + q₁₂ = q₀₂ + d, the two-form d ω being read through the top summand Ω² of 𝒪_{T''}”.

The first formula of [Stacks, Remark 60.14.5, Tag 07J3] on sections over an object. On a section ω of the square-zero summand Ω_{T/S,δ} of 𝒪_{T'} the three maps out of 𝒪_{T'} of the remark satisfy

q₀₁^* ω + q₁₂^* ω = q₀₂^* ω + d ω,

the two-form d ω being read in 𝒪_{T''} through the top summand. Indeed q₀₁ (0, ω) = (0, ω, 0, 0), q₁₂ (0, ω) = (0, 0, ω, d ω) and q₀₂ (0, ω) = (0, ω, ω, 0). This is the identity q₀₁^* ω + q₁₂^* ω - q₀₂^* ω = d ω that the proof of [Stacks, Tag 07J6] reads off the remark.

theorem crysSheafRingMap_q₀₁_add_q₁₂_diffSection (A : Thickening S)
    (ω : crysDiffSections A) :
    crysSheafRingMap (secondOrderThickeningSiteQ₀₁ S A)
          (firstOrderThickeningDiffSection A ω) +
        crysSheafRingMap (secondOrderThickeningSiteQ₁₂ S A)
          (firstOrderThickeningDiffSection A ω) =
      crysSheafRingMap (secondOrderThickeningSiteQ₀₂ S A)
          (firstOrderThickeningDiffSection A ω) +
        secondOrderTopSection A (crysDeRham A ω)

Crystalline.GlobalCrystallineSituation.crysSheafRingMap_q₁₂_mul_q₀₁_diffSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SecondOrderThickeningSections.lean, line 388. The attribute's comment: “the second formula of the remark on the sections over an object: the product in 𝒪_{T''} of a differential read through q₁₂ with one read through q₀₁ is their exterior product in the other order, read through the top summand Ω²”.

The second formula of [Stacks, Remark 60.14.5, Tag 07J3] on sections over an object. The product in 𝒪_{T''} of a section of the square-zero summand of 𝒪_{T'} read through q₁₂ with one read through q₀₁ is their exterior product, in the other order:

q₁₂^* ω · q₀₁^* ω' = ω' ∧ ω.

theorem crysSheafRingMap_q₁₂_mul_q₀₁_diffSection (A : Thickening S)
    (ω ω' : crysDiffSections A) :
    crysSheafRingMap (secondOrderThickeningSiteQ₁₂ S A)
          (firstOrderThickeningDiffSection A ω) *
        crysSheafRingMap (secondOrderThickeningSiteQ₀₁ S A)
          (firstOrderThickeningDiffSection A ω') =
      secondOrderTopSection A (crysWedgeSections A ω' ω)

Sources

LeanCrystalline.GlobalCrystallineSituation.firstOrderThickeningHom · Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap · Crystalline.GlobalCrystallineSituation.firstOrderThickeningMapApp_isDPMorphism · Crystalline.GlobalCrystallineSituation.firstOrderThickeningDPMap · Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap_comp_projHom · Crystalline.GlobalCrystallineSituation.firstOrderThickeningSchemeMap_comp_P₁Hom · Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap · Crystalline.GlobalCrystallineSituation.firstOrderThickeningSiteMap_comp_P₀

Section60.14 The de Rham complex #

Section 60.14 of the Stacks Project, Tag 07J4. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07J4, the section

Tag 07J4 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.crysDifferentialForms, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DeRhamComplex.lean, line 406. The attribute's comment: “Ω^i_{X/S} = ∧^i Ω_{X/S}, on the big crystalline category CRIS(X/S)”.

The presheaf Ω^i_{X/S} of crystalline differential forms of degree i on the big crystalline category. Its sections over an object (U, T, δ) are the i-th exterior power over Γ(T, 𝒪_T) of the sections of Ω_{X/S} there, and its transition maps are the exterior powers of those of Ω_{X/S}.

abbrev crysDifferentialForms (i : ℕ) : PresheafOfModules.{u} (structureRingCatPresheaf S)

Crystalline.GlobalCrystallineSituation.crysDeRhamComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DeRhamComplex.lean, line 739. The attribute's comment: “the de Rham complex 𝒪_{X/S} → Ω¹ → Ω² → ⋯, on CRIS(X/S)”.

The canonical de Rham complex on the crystalline site, the complex 𝒪_{X/S} → Ω¹_{X/S} → Ω²_{X/S} → ⋯ that the universal S-derivation d_{X/S} gives rise to.

def crysDeRhamComplex : CrysDeRhamComplex S

Crystalline.GlobalCrystallineSituation.SmallSite.crysDifferentialForms, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DeRhamComplex.lean, line 785. The attribute's comment: “Ω^i_{X/S} = ∧^i_{𝒪_{X/S}} Ω_{X/S} on the small crystalline site Cris(X/S)”.

The presheaf Ω^i_{X/S} of crystalline differential forms of degree i on the small crystalline site Cris(X/S), the i-th exterior power of Ω_{X/S} over 𝒪_{X/S}.

abbrev crysDifferentialForms (i : ℕ) :
    PresheafOfModules.{u} (structurePresheaf S ⋙ forget₂ CommRingCat RingCat)

Crystalline.GlobalCrystallineSituation.SmallSite.crysDeRhamDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DeRhamComplex.lean, line 876. The attribute's comment: “the de Rham complex 𝒪_{X/S} → Ω¹ → Ω² → ⋯ on Cris(X/S)”.

The de Rham complex 𝒪_{X/S} → Ω¹_{X/S} → Ω²_{X/S} → ⋯ on the small crystalline site Cris(X/S): the differential of the canonical complex on CRIS(X/S) at an object of the full subcategory Cris(X/S).

def crysDeRhamDifferential (i : ℕ) (A : CrystallineThickening S) :
    ⋀[crysFormRing S A]^i ((crysDifferentials S).obj (op A)) →+
      ⋀[crysFormRing S A]^(i + 1) ((crysDifferentials S).obj (op A))

Sources

LeanCrystalline.GlobalCrystallineSituation.crysDifferentialForms · Crystalline.GlobalCrystallineSituation.crysDeRhamComplex · Crystalline.GlobalCrystallineSituation.SmallSite.crysDifferentialForms · Crystalline.GlobalCrystallineSituation.SmallSite.crysDeRhamDifferential

Section60.15 Connections #

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

Tag 07J6, a lemma

Tag 07J6 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crystalConnectionCris, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalConnectionCris.lean, line 347. The attribute's comment: “the canonical connection ∇ : F ⟶ F ⊗_{𝒪_{X/S}} Ω_{X/S} of a crystal F on Cris(X/S), a morphism of abelian sheaves: on every T it is p₁^ s - p₀^ s on the first-order thickening T' of 07J2, read through (F ⊗ Ω_{X/S})_T = F_T ⊗ Ω_{T/S,δ}”.

The canonical connection of a crystal, as a morphism of abelian sheaves ∇ : F ⟶ F ⊗_{𝒪_{X/S}} Ω_{X/S} on Cris(X/S). On the ambient scheme T of every object it is the connection p₁^* s - p₀^* s, read through (F ⊗ Ω_{X/S})_T = F_T ⊗ Ω_{T/S,δ} (crystalConnectionCrisApp_restrict).

def crystalConnectionCris : abelianSheaf F ⟶ tensorDifferentialFormsSheaf F 1

Crystalline.GlobalCrystallineSituation.SmallSite.crystalConnectionCris_isIntegrableConnection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalIntegrableConnectionCris.lean, line 153. The attribute's comment: “a crystal F on Cris(X/S) has a canonical integrable connection: ∇ = crystalConnectionCris : F ⟶ F ⊗ Ω_{X/S}, a morphism of abelian sheaves, satisfies the Leibniz rule, is p₁^ s - p₀^ s on every T, its extension F ⊗ Ω ⟶ F ⊗ Ω² obeys ∇(s ⊗ ω) = ∇(s) ∧ ω + s ⊗ d ω, and ∇ ∘ ∇ = 0”.

A crystal F in 𝒪_{X/S}-modules on Cris(X/S) comes equipped with a canonical integrable connection. The connection is ∇ = crystalConnectionCris : F ⟶ F ⊗_{𝒪_{X/S}} Ω_{X/S}, a morphism of abelian sheaves on Cris(X/S), and

(it is a connection) ∇(f s) = f ∇(s) + s ⊗ d f for every object A and all sections f of 𝒪_{X/S} and s of F over A;

(it is the canonical one) on the ambient scheme T of every object, ∇(s) is p₁^* s - p₀^* s on the first-order thickening T' of [Stacks, Tag 07J2], read in F_T ⊗ Ω_{T/S,δ} ⊂ F_{T'};

the exterior product by a one-form is (x ⊗ η) ∧ ω = x ⊗ (η ∧ ω) on local pure tensors, and the extension crystalExtensionCris : F ⊗ Ω_{X/S} ⟶ F ⊗ Ω²_{X/S} is given by the rule ∇(s ⊗ ω) = ∇(s) ∧ ω + s ⊗ d ω of [Stacks, Tag 07I0] and [Stacks, Section 60.15, Tag 07J5];

(it is integrable) ∇ ∘ ∇ = 0 : F ⟶ F ⊗ Ω²_{X/S}.

theorem crystalConnectionCris_isIntegrableConnection (hF : IsSheafCrystal F) :
    ((∀ (A : CrystallineThickening S) (f : crysFormRing S A) (s : F.val.obj (op A)),
        (show tensorFormsModSec F 1 A from
          (crystalConnectionCris hF).hom.app (op A) (ULift.up (f • s))) =
          f • (show tensorFormsModSec F 1 A from
            (crystalConnectionCris hF).hom.app (op A) (ULift.up s)) +
          (show tensorFormsModSec F 1 A from
            (CategoryTheory.toSheafify (smallTopology S) (tensorDifferentialFormsPresheaf F 1)).app
              (op A) (ULift.up (formsTmul F s (formsD A f))))) ∧
      ∀ (A : CrystallineThickening S) (s : (abelianSheaf F).obj.obj (op A)),
        (firstOrderTensorInclusion F A).val.app (op ⊤)
            ((tensorFormsAmbientIsoOne A).hom.app (op ⊤)
              ((tensorDifferentialFormsSheaf F 1).obj.map (A.restrictOpenHom ⊤).op
                ((crystalConnectionCris hF).hom.app (op A) s))).down =
          crystalConnectionRaw F A ⊤ (F.val.map (A.restrictOpenHom ⊤).op s.down)) ∧
    ((∀ (A : CrystallineThickening S) (ω : (crysDifferentialForms S 1).obj (op A))
          (x : F.val.obj (op A)) (η : (crysDifferentialForms S 1).obj (op A)),
        crystalWedgeCrisApp F A ω
            ((CategoryTheory.toSheafify (smallTopology S) (tensorDifferentialFormsPresheaf F 1)).app
              (op A) (ULift.up (formsTmul F x η))) =
          (CategoryTheory.toSheafify (smallTopology S) (tensorDifferentialFormsPresheaf F 2)).app
            (op A) (ULift.up (formsTmul F x (formsWedgeOne η ω)))) ∧
      (∀ (A : CrystallineThickening S) (s : F.val.obj (op A))
          (ω : (crysDifferentialForms S 1).obj (op A)),
        (crystalExtensionCris hF).hom.app (op A)
            ((CategoryTheory.toSheafify (smallTopology S) (tensorDifferentialFormsPresheaf F 1)).app
              (op A) (ULift.up (formsTmul F s ω))) =
          crystalWedgeCrisApp F A ω ((crystalConnectionCris hF).hom.app (op A) (ULift.up s)) +
            (show (tensorDifferentialFormsSheaf F 2).obj.obj (op A) from
              (CategoryTheory.toSheafify (smallTopology S)
                (tensorDifferentialFormsPresheaf F 2)).app
                  (op A) (ULift.up (formsTmul F s (formsDeRham A ω))))) ∧
      crystalConnectionCris hF ≫ crystalExtensionCris hF = 0)

Sources

LeanCrystalline.GlobalCrystallineSituation.SmallSite.crystalConnectionCris · Crystalline.GlobalCrystallineSituation.SmallSite.crystalConnectionCris_isIntegrableConnection

Section60.16 Cosimplicial algebra #

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

Tag 07KQ, a lemma

Tag 07KQ in the Stacks Project.

Crystalline.homotopic_tensor_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial.lean, line 155. The attribute's comment: “tensor”.

Stacks Lemma 07KQ (tensor). Tensoring homotopic morphisms of cosimplicial modules with the identity morphism of another cosimplicial module preserves homotopy.

public theorem homotopic_tensor_id {φ ψ : K ⟶ M} (h : Homotopic φ ψ)
    (L : CosimplicialModule A) :
    Homotopic (φ ⊗ₘ 𝟙 L) (ψ ⊗ₘ 𝟙 L)

Crystalline.homotopic_exteriorPower_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial.lean, line 406. The attribute's comment: “exterior_power”.

Stacks 07KQ, exterior power. Homotopic homomorphisms of cosimplicial modules induce homotopic homomorphisms on every exterior power.

public theorem homotopic_exteriorPower_map
    {A : CosimplicialObject CommRingCat.{u}}
    {K M : CosimplicialModule A} {φ ψ : K ⟶ M} (i : ℕ)
    (h : Homotopic φ ψ) :
    Homotopic ((exteriorPowerFunctor A i).functor.map φ)
      ((exteriorPowerFunctor A i).functor.map ψ)

Crystalline.homotopic_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial.lean, line 748. The attribute's comment: “base change”.

Stacks 07KQ, base change. If two homomorphisms of cosimplicial A-modules are homotopic and f : A ⟶ B is a homomorphism of cosimplicial rings, then the induced homomorphisms of cosimplicial B-modules between the base changes are homotopic. The homotopy is h ⊗ 1, and in particular each of its components is B_n-linear, because Homotopy for cosimplicial B-modules demands exactly that.

public theorem homotopic_baseChange (f : A ⟶ B) {K M : CosimplicialModule A} {φ ψ : K ⟶ M}
    (h : Homotopic φ ψ) :
    Homotopic ((baseChange f).map φ) ((baseChange f).map ψ)

Crystalline.homotopic_adicCompletionMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial.lean, line 1124. The attribute's comment: “completion”.

Stacks 07KQ, completion. Homotopic homomorphisms of modules over a cosimplicial ring induce homotopic homomorphisms on their completions with respect to a cosimplicial ideal.

public lemma homotopic_adicCompletionMap
    {A : CosimplicialObject CommRingCat.{u}} (I : CosimplicialIdeal A)
    {K M : SemilinearCosimplicialModule.{u, v} A} (φ ψ : SemilinearCosimplicialModule.Hom K M)
    (h : Relation.EqvGen (fun a b => Nonempty (SemilinearCosimplicialModule.Homotopy a b)) φ ψ)
    (Khat : SemilinearCosimplicialModule.Completion I K)
    (Mhat : SemilinearCosimplicialModule.Completion I M)
    (φhat ψhat : SemilinearCosimplicialModule.Completion.Hom Khat Mhat)
    (hφ : ∀ n x, Mhat.iso n (φhat.hom.app n x) =
      AdicCompletion.map (I.obj n) (φ.app n) (Khat.iso n x))
    (hψ : ∀ n x, Mhat.iso n (ψhat.hom.app n x) =
      AdicCompletion.map (I.obj n) (ψ.app n) (Khat.iso n x)) :
    Relation.EqvGen (fun a b =>
      Nonempty (SemilinearCosimplicialModule.Completion.Homotopy a b)) φhat ψhat

Tag 07KT, an item

Tag 07KT in the Stacks Project.

Crystalline.homotopic_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial.lean, line 748. The attribute's comment: “homotopy is preserved by base change along a homomorphism of cosimplicial rings”.

Stacks 07KQ, base change. If two homomorphisms of cosimplicial A-modules are homotopic and f : A ⟶ B is a homomorphism of cosimplicial rings, then the induced homomorphisms of cosimplicial B-modules between the base changes are homotopic. The homotopy is h ⊗ 1, and in particular each of its components is B_n-linear, because Homotopy for cosimplicial B-modules demands exactly that.

public theorem homotopic_baseChange (f : A ⟶ B) {K M : CosimplicialModule A} {φ ψ : K ⟶ M}
    (h : Homotopic φ ψ) :
    Homotopic ((baseChange f).map φ) ((baseChange f).map ψ)

Sources

LeanCrystalline.homotopic_tensor_id · Crystalline.homotopic_exteriorPower_map · Crystalline.homotopic_baseChange · Crystalline.homotopic_adicCompletionMap

Section60.17 Crystals in quasi-coherent modules #

Section 60.17 of the Stacks Project, Tag 07J7. 17 tags here are carried by 24 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07J8, an equation

Tag 07J8 in the Stacks Project.

Crystalline.pAdicCompletedDividedPowerEnvelope, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Crystal.lean, line 85.

The p-adically completed divided power envelope of the kernel of a surjective polynomial presentation of C over A.

public noncomputable abbrev pAdicCompletedDividedPowerEnvelope
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) (_hf : Function.Surjective f) : Type (max u w)

Tag 07J9, an equation

Tag 07J9 in the Stacks Project.

Crystalline.pAdicCompletedDividedPowerDifferentials, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalsQuasiCoherent/Basic.lean, line 307.

The module Ω_D: the p-adic completion of the module of divided power differentials of the divided power envelope of a polynomial presentation of C over A.

public noncomputable abbrev pAdicCompletedDividedPowerDifferentials
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) : Type (max u w)

Crystalline.pAdicCompletedDividedPowerDifferentialsEquivLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalsQuasiCoherent/Basic.lean, line 328. The attribute's comment: “the inverse limit over the finite levels”.

Stacks 07J9, the first identification. Ω_D = lim_e Ω_{D_e/A, γ̄}: the completed module of divided power differentials is the inverse limit of the modules of divided power differentials of the finite levels D_e.

public noncomputable def pAdicCompletedDividedPowerDifferentialsEquivLimit
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) :
    pAdicCompletedDividedPowerDifferentials s f ≃+
      ((limit (QuotientDifferentialsSystem.functor (A := s.A)
          (polynomialDividedPowerEnvelopeRing s f).ideal
          (polynomialDividedPowerEnvelopeRing s f).dividedPowers s.p
          (presentationDifferentialsCompletionComparison s f).quotientSystem) :
        AddCommGrpCat) : Type (max u w))

Crystalline.pAdicCompletedDividedPowerDifferentialsEquivCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalsQuasiCoherent/Basic.lean, line 343. The attribute's comment: “the p-adic completion of the differentials of the completed envelope”.

Stacks 07J9, the second identification. Ω_D = lim_e Ω_{D/A, γ̄}/p^eΩ_{D/A, γ̄}: the completed module of divided power differentials is also the p-adic completion of the module of divided power differentials of the completed envelope D itself.

public noncomputable def pAdicCompletedDividedPowerDifferentialsEquivCompletion
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) :
    pAdicCompletedDividedPowerDifferentials s f ≃+
      AdicCompletion
        (DividedPowers.pAdicIdeal
          (A := AdicCompletion
            (DividedPowers.pAdicIdeal (A := polynomialDividedPowerEnvelopeRing s f) s.p)
            (polynomialDividedPowerEnvelopeRing s f)) s.p)
        (dividedPowerDifferentials (A := s.A)
          (DividedPowers.completedDividedPowers (polynomialDividedPowerEnvelopeRing s f).ideal
            (polynomialDividedPowerEnvelopeRing s f).dividedPowers s.p
            (polynomialDividedPowerEnvelope_prime_nilpotent s f)).1)

Crystalline.exists_dividedPowerDifferentialsCompletionEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/ModuleDifferentials/Completion.lean, line 722. The attribute's comment: “the identification of the inverse limits that defines Ω_D, the case B = D”.

Let A → B be a ring map, let (J, δ) be a divided power structure on B, let p be prime, let A be a ℤ_(p)-algebra and let p be nilpotent in B / J. Then lim\_e Ω\_\{B\_e/A, δ̄} = lim\_e Ω\_\{B/A, δ} / pᵉ Ω\_\{B/A, δ} = lim\_e Ω\_\{B^∧/A, δ^∧} / pᵉ Ω\_\{B^∧/A, δ^∧}.

The conclusion is written out here, with no reference to Crystalline.DifferentialsCompletionComparison. Beyond a level N, each pᵉ B lies in J and is stable under the divided powers of δ (level), so B_e = B / pᵉ B carries divided powers δ̄ and the modules Ω_{B_e/A, δ̄} = Crystalline.quotientDifferentials .. form an inverse system whose transition maps are those induced on universal differentials (transition, and the first conjunct). The second and third limits are Mathlib's AdicCompletions of Ω_{B/A, δ} and of Ω_{B^∧/A, δ^∧}; fromOriginal and fromCompletion identify every level of their towers of quotients with that system, compatibly with all three families of transition maps, which is the first equality in the strong form of an isomorphism of inverse systems. limitEquiv is the isomorphism of the second limit with the third that results, and the last conjunct says its component at each level N + e is fromOriginal followed by the inverse of fromCompletion.

public theorem exists_dividedPowerDifferentialsCompletionEquiv
    [Fact p.Prime] [Algebra (DividedPowers.IntegersAtPrime p) A]
    (hp : IsNilpotent (Ideal.Quotient.mk J (p : B))) :
    ∃ (N : ℕ)
      (level : ∀ e, N ≤ e → (DividedPowers.pAdicIdeal (A := B) p ^ e ≤ J) ∧
        delta.IsSubDPIdeal (DividedPowers.pAdicIdeal (A := B) p ^ e))
      (transition : ∀ e e' : ℕ, e ≤ e' →
        quotientDifferentials (A := A) J delta p (N + e')
            (level _ (Nat.le_add_right N e')).1 (level _ (Nat.le_add_right N e')).2 →+
          quotientDifferentials (A := A) J delta p (N + e)
            (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (fromOriginal : ∀ e : ℕ, differentialsModPow (A := A) J delta p (N + e) ≃ₗ[B]
        quotientDifferentials (A := A) J delta p (N + e)
          (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (fromCompletion : ∀ e : ℕ,
        completedDifferentialsModPow (A := A) J delta p hp (N + e) ≃+
          quotientDifferentials (A := A) J delta p (N + e)
            (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (limitEquiv : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p)
            (dividedPowerDifferentials (A := A) delta) ≃+
          AdicCompletion
            (DividedPowers.pAdicIdeal
              (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
            (dividedPowerDifferentials (A := A)
              (DividedPowers.completedDividedPowers J delta p hp).1)),
      (∀ (e e' : ℕ) (h : e ≤ e') (b : B),
          transition e e' h
              (dividedPowerDifferential (A := A)
                (DividedPowers.quotientDividedPowers J delta p (N + e')
                  (level _ (Nat.le_add_right N e')).1 (level _ (Nat.le_add_right N e')).2)
                (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e')) b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e)) b)) ∧
      (∀ (e : ℕ) (b : B),
          fromOriginal e
              (Submodule.Quotient.mk (dividedPowerDifferential (A := A) delta b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e)) b)) ∧
      (∀ (e e' : ℕ) (h : e ≤ e')
          (omega : differentialsModPow (A := A) J delta p (N + e')),
          transition e e' h (fromOriginal e' omega) =
            fromOriginal e
              (AdicCompletion.transitionMap (DividedPowers.pAdicIdeal (A := B) p)
                (dividedPowerDifferentials (A := A) delta)
                (Nat.add_le_add_left h N) omega)) ∧
      (∀ (e : ℕ) (b : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B),
          fromCompletion e
              (Submodule.Quotient.mk
                (dividedPowerDifferential (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1 b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (AdicCompletion.evalₐ (DividedPowers.pAdicIdeal (A := B) p) (N + e) b)) ∧
      (∀ (e : ℕ) (b : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B)
          (omega : completedDifferentialsModPow (A := A) J delta p hp (N + e)),
          fromCompletion e (b • omega) =
            AdicCompletion.evalₐ (DividedPowers.pAdicIdeal (A := B) p) (N + e) b •
              fromCompletion e omega) ∧
      (∀ (e e' : ℕ) (h : e ≤ e')
          (omega : completedDifferentialsModPow (A := A) J delta p hp (N + e')),
          transition e e' h (fromCompletion e' omega) =
            fromCompletion e
              (AdicCompletion.transitionMap
                (DividedPowers.pAdicIdeal
                  (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
                (dividedPowerDifferentials (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1)
                (Nat.add_le_add_left h N) omega)) ∧
      (∀ (e : ℕ) (omega : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p)
            (dividedPowerDifferentials (A := A) delta)),
          fromCompletion e
              (AdicCompletion.eval
                (DividedPowers.pAdicIdeal
                  (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
                (dividedPowerDifferentials (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1)
                (N + e) (limitEquiv omega)) =
            fromOriginal e
              (AdicCompletion.eval (DividedPowers.pAdicIdeal (A := B) p)
                (dividedPowerDifferentials (A := A) delta) (N + e) omega))

Tag 07JA, an equation

Tag 07JA in the Stacks Project.

Crystalline.completedDividedPowerDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalsQuasiCoherent/Basic.lean, line 175.

The universal divided power derivation of the completed envelope, characterized on the dense image of the original envelope.

public noncomputable def completedDividedPowerDifferential
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) (hf : Function.Surjective f) :
    let env := polynomialDividedPowerEnvelope s f
    let E := env.object
    letI : Algebra s.A E := env.structureMap.toRingHom.toAlgebra
    let P := DividedPowers.pAdicIdeal (A := E) s.p
    let Ω := AdicCompletion P (dividedPowerDifferentials (A := s.A) E.dividedPowers)
    Σ' hp : IsNilpotent (Ideal.Quotient.mk E.ideal (s.p : E)),
      let D := DividedPowerRing.of
        (pAdicCompletedDividedPowerEnvelope s f hf)
        (DividedPowers.completionIdeal E.ideal s.p hp)
        (DividedPowers.completedDividedPowers E.ideal E.dividedPowers s.p hp).1
      letI : Algebra s.A D :=
        ((algebraMap E D).comp env.structureMap.toRingHom).toAlgebra
      { d : DividedPowerDerivation s.A D (algebraMap s.A D) Ω //
        ∀ b : E, d (algebraMap E D b) =
          AdicCompletion.of P (dividedPowerDifferentials (A := s.A) E.dividedPowers)
            (dividedPowerDifferential (A := s.A) E.dividedPowers b) }

Tag 07JF, an equation

Tag 07JF in the Stacks Project.

Crystalline.pAdicCompletedTensorPowerEnvelope, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Crystal.lean, line 150.

The ring D(n): the p-adically completed divided power envelope of the kernel J(n) of the surjection P ⊗_A … ⊗_A P → C on the (n + 1)-fold tensor power of a surjective polynomial presentation of C over A.

public noncomputable abbrev pAdicCompletedTensorPowerEnvelope
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) (hf : Function.Surjective f) (n : ℕ) :
    Type (max u w)

Tag 07L0, an equation

Tag 07L0 in the Stacks Project.

Crystalline.exists_dividedPowerDifferentialsCompletionEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/ModuleDifferentials/Completion.lean, line 722. The attribute's comment: “the same identification of the limits, read at the divided power envelope D(n)”.

Let A → B be a ring map, let (J, δ) be a divided power structure on B, let p be prime, let A be a ℤ_(p)-algebra and let p be nilpotent in B / J. Then lim\_e Ω\_\{B\_e/A, δ̄} = lim\_e Ω\_\{B/A, δ} / pᵉ Ω\_\{B/A, δ} = lim\_e Ω\_\{B^∧/A, δ^∧} / pᵉ Ω\_\{B^∧/A, δ^∧}.

The conclusion is written out here, with no reference to Crystalline.DifferentialsCompletionComparison. Beyond a level N, each pᵉ B lies in J and is stable under the divided powers of δ (level), so B_e = B / pᵉ B carries divided powers δ̄ and the modules Ω_{B_e/A, δ̄} = Crystalline.quotientDifferentials .. form an inverse system whose transition maps are those induced on universal differentials (transition, and the first conjunct). The second and third limits are Mathlib's AdicCompletions of Ω_{B/A, δ} and of Ω_{B^∧/A, δ^∧}; fromOriginal and fromCompletion identify every level of their towers of quotients with that system, compatibly with all three families of transition maps, which is the first equality in the strong form of an isomorphism of inverse systems. limitEquiv is the isomorphism of the second limit with the third that results, and the last conjunct says its component at each level N + e is fromOriginal followed by the inverse of fromCompletion.

public theorem exists_dividedPowerDifferentialsCompletionEquiv
    [Fact p.Prime] [Algebra (DividedPowers.IntegersAtPrime p) A]
    (hp : IsNilpotent (Ideal.Quotient.mk J (p : B))) :
    ∃ (N : ℕ)
      (level : ∀ e, N ≤ e → (DividedPowers.pAdicIdeal (A := B) p ^ e ≤ J) ∧
        delta.IsSubDPIdeal (DividedPowers.pAdicIdeal (A := B) p ^ e))
      (transition : ∀ e e' : ℕ, e ≤ e' →
        quotientDifferentials (A := A) J delta p (N + e')
            (level _ (Nat.le_add_right N e')).1 (level _ (Nat.le_add_right N e')).2 →+
          quotientDifferentials (A := A) J delta p (N + e)
            (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (fromOriginal : ∀ e : ℕ, differentialsModPow (A := A) J delta p (N + e) ≃ₗ[B]
        quotientDifferentials (A := A) J delta p (N + e)
          (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (fromCompletion : ∀ e : ℕ,
        completedDifferentialsModPow (A := A) J delta p hp (N + e) ≃+
          quotientDifferentials (A := A) J delta p (N + e)
            (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
      (limitEquiv : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p)
            (dividedPowerDifferentials (A := A) delta) ≃+
          AdicCompletion
            (DividedPowers.pAdicIdeal
              (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
            (dividedPowerDifferentials (A := A)
              (DividedPowers.completedDividedPowers J delta p hp).1)),
      (∀ (e e' : ℕ) (h : e ≤ e') (b : B),
          transition e e' h
              (dividedPowerDifferential (A := A)
                (DividedPowers.quotientDividedPowers J delta p (N + e')
                  (level _ (Nat.le_add_right N e')).1 (level _ (Nat.le_add_right N e')).2)
                (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e')) b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e)) b)) ∧
      (∀ (e : ℕ) (b : B),
          fromOriginal e
              (Submodule.Quotient.mk (dividedPowerDifferential (A := A) delta b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (Ideal.Quotient.mk (DividedPowers.pAdicIdeal (A := B) p ^ (N + e)) b)) ∧
      (∀ (e e' : ℕ) (h : e ≤ e')
          (omega : differentialsModPow (A := A) J delta p (N + e')),
          transition e e' h (fromOriginal e' omega) =
            fromOriginal e
              (AdicCompletion.transitionMap (DividedPowers.pAdicIdeal (A := B) p)
                (dividedPowerDifferentials (A := A) delta)
                (Nat.add_le_add_left h N) omega)) ∧
      (∀ (e : ℕ) (b : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B),
          fromCompletion e
              (Submodule.Quotient.mk
                (dividedPowerDifferential (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1 b)) =
            dividedPowerDifferential (A := A)
              (DividedPowers.quotientDividedPowers J delta p (N + e)
                (level _ (Nat.le_add_right N e)).1 (level _ (Nat.le_add_right N e)).2)
              (AdicCompletion.evalₐ (DividedPowers.pAdicIdeal (A := B) p) (N + e) b)) ∧
      (∀ (e : ℕ) (b : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B)
          (omega : completedDifferentialsModPow (A := A) J delta p hp (N + e)),
          fromCompletion e (b • omega) =
            AdicCompletion.evalₐ (DividedPowers.pAdicIdeal (A := B) p) (N + e) b •
              fromCompletion e omega) ∧
      (∀ (e e' : ℕ) (h : e ≤ e')
          (omega : completedDifferentialsModPow (A := A) J delta p hp (N + e')),
          transition e e' h (fromCompletion e' omega) =
            fromCompletion e
              (AdicCompletion.transitionMap
                (DividedPowers.pAdicIdeal
                  (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
                (dividedPowerDifferentials (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1)
                (Nat.add_le_add_left h N) omega)) ∧
      (∀ (e : ℕ) (omega : AdicCompletion (DividedPowers.pAdicIdeal (A := B) p)
            (dividedPowerDifferentials (A := A) delta)),
          fromCompletion e
              (AdicCompletion.eval
                (DividedPowers.pAdicIdeal
                  (A := AdicCompletion (DividedPowers.pAdicIdeal (A := B) p) B) p)
                (dividedPowerDifferentials (A := A)
                  (DividedPowers.completedDividedPowers J delta p hp).1)
                (N + e) (limitEquiv omega)) =
            fromOriginal e
              (AdicCompletion.eval (DividedPowers.pAdicIdeal (A := B) p)
                (dividedPowerDifferentials (A := A) delta) (N + e) omega))

Tag 07L1, an equation

Tag 07L1 in the Stacks Project.

Crystalline.completedDividedPowerDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CrystalsQuasiCoherent/Basic.lean, line 175. The attribute's comment: “the same derivation for the (n+1)-fold tensor-product presentation”.

The universal divided power derivation of the completed envelope, characterized on the dense image of the original envelope.

public noncomputable def completedDividedPowerDifferential
    (s : AffineCrystallineSituation.{u, v}) {ι : Type w}
    (f : MvPolynomial ι s.A →ₐ[s.A] s.C) (hf : Function.Surjective f) :
    let env := polynomialDividedPowerEnvelope s f
    let E := env.object
    letI : Algebra s.A E := env.structureMap.toRingHom.toAlgebra
    let P := DividedPowers.pAdicIdeal (A := E) s.p
    let Ω := AdicCompletion P (dividedPowerDifferentials (A := s.A) E.dividedPowers)
    Σ' hp : IsNilpotent (Ideal.Quotient.mk E.ideal (s.p : E)),
      let D := DividedPowerRing.of
        (pAdicCompletedDividedPowerEnvelope s f hf)
        (DividedPowers.completionIdeal E.ideal s.p hp)
        (DividedPowers.completedDividedPowers E.ideal E.dividedPowers s.p hp).1
      letI : Algebra s.A D :=
        ((algebraMap E D).comp env.structureMap.toRingHom).toAlgebra
      { d : DividedPowerDerivation s.A D (algebraMap s.A D) Ω //
        ∀ b : E, d (algebraMap E D b) =
          AdicCompletion.of P (dividedPowerDifferentials (A := s.A) E.dividedPowers)
            (dividedPowerDifferential (A := s.A) E.dividedPowers b) }

Tag 07L2, a lemma

Tag 07L2 in the Stacks Project.

Crystalline.exists_ringEquiv_pAdicCompletedDividedPowerPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/TensorPowerEnvelope.lean, line 1347.

Stacks Project, Lemma 60.17.5, Tag 07L2. Let D and D(n) be as in (07J8) and (07JF). The coprojection P → P ⊗_A … ⊗_A P, h ↦ h ⊗ 1 ⊗ … ⊗ 1 induces an isomorphism

D(n) = lim_e D⟨ξ_i(j)⟩/p^e D⟨ξ_i(j)⟩

of algebras over D, with ξ_i(j) = x_i ⊗ 1 ⊗ … ⊗ 1 - 1 ⊗ … ⊗ 1 ⊗ x_i ⊗ 1 ⊗ … ⊗ 1 for j = 1, …, n, where the second x_i is placed in the (j + 1)-st slot.

The map φ induced by the coprojection is the algebra structure of D(n) over D: it agrees with the coprojection on the image of P. The isomorphism e is an isomorphism over φ, and it carries the image of ξ_i(j) in D(n) to the divided power variable ξ_i(j).

public theorem exists_ringEquiv_pAdicCompletedDividedPowerPolynomial (n : ℕ) :
    ∃ (φ : pAdicCompletedDividedPowerEnvelope s f hf →+*
        pAdicCompletedTensorPowerEnvelope s f hf n)
      (e : pAdicCompletedTensorPowerEnvelope s f hf n ≃+*
        pAdicCompletedDividedPowerPolynomialOverEnvelope s f hf n),
      (∀ x : MvPolynomial ι s.A,
          φ (toPAdicCompletedDividedPowerEnvelope s f hf x) =
            toPAdicCompletedDividedPowerEnvelope s (tensorPowerPresentation s f n)
              (tensorPowerPresentation_surjective s f hf n)
              (mvPolynomialCoprojection s.A (0 : Fin (n + 1)) x)) ∧
      (∀ y : pAdicCompletedDividedPowerEnvelope s f hf,
          e (φ y) = toPAdicCompletedDividedPowerPolynomial s f hf n y) ∧
      (∀ q : ι × Fin n,
          e (toPAdicCompletedDividedPowerEnvelope s (tensorPowerPresentation s f n)
            (tensorPowerPresentation_surjective s f hf n) (coprojectionDifference s n q)) =
            coprojectionDifferenceVariable s f hf n q)

Tag 07L3, an equation

Tag 07L3 in the Stacks Project.

Declarations registered for the tag:

Crystalline.exists_ringEquiv_pAdicCompletedDividedPowerPolynomial, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Crystalline/TensorPowerEnvelope.lean, line 1536 (StacksFrontier): “equation 60.17.1.1, the display of this lemma: the isomorphism e produced here is D(n) = lim_e D⟨ξ_i(j)⟩/p^e D⟨ξ_i(j)⟩, over the algebra structure φ of D(n) over D and carrying the image of each ξ_i(j) to the divided power variable of the same name”.

Tag 07L4, a lemma

Tag 07L4 in the Stacks Project.

Crystalline.completedEnvelopeThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineSite/Coproduct.lean, line 140. The attribute's comment: “the completed envelopes are objects of the site”.

Stacks Project, Tag 07L4, first assertion. The divided power ring (D, J̄, γ̄) of a surjective polynomial presentation of C over A is an object of Cris^∧(C/A). Applied to the tensor power presentation this is (D(n), J̄(n), γ̄(n)), see Crystalline.tensorPowerEnvelopeThickening.

public noncomputable def completedEnvelopeThickening
    (g : MvPolynomial ι s.A →ₐ[s.A] s.C) (hg : Function.Surjective g) :
    CompletedEnvelopeThickening s g hg

Crystalline.completedEnvelope_isCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineSite/Coproduct.lean, line 691. The attribute's comment: “the canonical coproduct”.

Stacks Project, Tag 07L4, second assertion. The canonical coprojections exhibit D(n) as the coproduct ∐_{j = 0, …, n} D of n + 1 copies of D in Cris^∧(C/A).

public theorem completedEnvelope_isCoproduct
    (g : MvPolynomial ι s.A →ₐ[s.A] s.C) (hg : Function.Surjective g) (n : ℕ) :
    Nonempty (IsColimit (Cofan.mk (tensorPowerEnvelopeThickening s g hg n).thickening
      (completedEnvelopeCoprojection s g hg n)))

Tag 07JB, an item

Tag 07JB in the Stacks Project.

Crystalline.IsPAdicallyComplete, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CompletedConnection.lean, line 123.

A D-module is p-adically complete when it is complete and separated for the p-adic filtration, that is for the ideal p D.

public def IsPAdicallyComplete (M : Type w) [AddCommGroup M] [Module D M] : Prop

Crystalline.instIsAdicCompleteCompletedDividedPowerRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CompletedRingPAdicComplete.lean, line 63. The attribute's comment: “item (07JB) for the module M = D over the completed divided power ring itself”.

The p-adic completion D of B is p-adically complete for its own ideal (p) ⊆ D.

This is item (07JB) of [Stacks, Lemma 60.17.3, Tag 07JG] for the module M = D over itself, the case of the coefficient sheaf 𝒪_{X/S}. Mathlib's AdicCompletion.isAdicComplete_self proves it for the extension along algebraMap B D of the ideal (p) ⊆ B, and Crystalline.pAdicIdeal_map_ringHom identifies that extension with the ideal (p) ⊆ D; the finite generation it asks of (p) ⊆ B is Submodule.fg_span_singleton.

public instance instIsAdicCompleteCompletedDividedPowerRing :
    IsAdicComplete (pAdicIdeal (A := completedDividedPowerRing p (B := B)) p)
      (completedDividedPowerRing p (B := B))

Tag 07JC, an item

Tag 07JC in the Stacks Project.

Crystalline.CompletedConnection, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CompletedConnection.lean, line 131.

A connection ∇ : M → M ⊗̂_D Ω relative to a map d : D → Ω: an additive map satisfying the Leibniz rule ∇ (f m) = f • ∇ m + m ⊗ d f.

public structure CompletedConnection (d : D → Omega) (M : Type w) [AddCommGroup M]
    [Module D M]

Tag 07JD, an item

Tag 07JD in the Stacks Project.

Crystalline.IsIntegrable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CompletedConnection.lean, line 196. The attribute's comment: “integrability in the coordinates x_i: the coordinate operators commute”.

A completed connection is integrable when its coordinate operators commute.

public def IsIntegrable (dx : ι → Omega) {d : D → Omega} {M : Type w} [AddCommGroup M]
    [Module D M] (nabla : CompletedConnection p D Omega d M) : Prop

Tag 07JE, an item

Tag 07JE in the Stacks Project.

Crystalline.IsTopologicallyQuasiNilpotent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/CompletedConnection.lean, line 205. The attribute's comment: “corrected to k ≥ 1: admitting k = 0 would force M = p M”.

A completed connection is topologically quasi-nilpotent when, writing ∇ m = ∑ θ_i m ⬝ d x_i, for every m only finitely many pairs (i, k) with k ≥ 1 satisfy θ_i^k m ∉ p M.

public def IsTopologicallyQuasiNilpotent (dx : ι → Omega) {d : D → Omega} {M : Type w}
    [AddCommGroup M] [Module D M] (nabla : CompletedConnection p D Omega d M) : Prop

Tag 07JG, a lemma

Tag 07JG in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.pairTensorLevel_crystalPairFunctor_nabla, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalPairConnection07J6.lean, line 65. The attribute's comment: “for any surjective polynomial presentation g : A[x_i : i ∈ ι] → C, supplied as the WholeSpacePresentation instance (the default instance is the tautological one): the connection of the pair attached to a crystal is the canonical connection of 07J6 evaluated on the finite thickenings (X, T_e, δ̄): its image at each level e is the 07J6 connection of the crystal over T_e applied to the image of m”.

The connection ∇ of the pair attached to a crystal is obtained by evaluating the canonical connection of [Stacks, Tag 07J6] on the finite thickenings. For a crystal ℱ in quasi-coherent 𝒪_{X/S}-modules on Cris(X/S), an element m of M = lim_e Γ((X, T_e, δ̄), ℱ) and a level e, the image of ∇(m) ∈ M ⊗̂_D Ω_D in Γ(T_e, Ω_{T_e/S,δ̄}) ⊗_{Γ(T_e, 𝒪)} Γ(T_e, ℱ) is the canonical connection of ℱ on the sections over (X, T_e, δ̄), applied to the image of m.

theorem pairTensorLevel_crystalPairFunctor_nabla (Fc : QuasiCoherentCrystal S) (e : ℕ)
    (m : wholeSpaceSections hp Fc ⦋0⦌) :
    pairTensorLevel hp Fc e (((crystalPairFunctor hp).obj Fc).nabla m) =
      AffineConnection.connection (bijective_crysExtensionSectionsMap_levelObj hp Fc e)
        (pairComponent hp Fc e m)

Crystalline.GlobalCrystallineSituation.SmallSite.firstOrderTensorInclusion_crystalConnection_crystalPairFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalPairConnection07J6.lean, line 90. The attribute's comment: “for any surjective polynomial presentation g : A[x_i : i ∈ ι] → C, supplied as the WholeSpacePresentation instance (the default instance is the tautological one): the connection of the pair attached to a crystal is the sheaf-level canonical connection of 07J6 evaluated on the finite thickenings (X, T_e, δ̄), level by level”.

The connection ∇ of the pair attached to a crystal is obtained by evaluating the sheaf-level canonical connection of [Stacks, Tag 07J6] on the finite thickenings. For a crystal ℱ in quasi-coherent 𝒪_{X/S}-modules on Cris(X/S), an element m of M = lim_e Γ((X, T_e, δ̄), ℱ) and a level e, the canonical connection ∇ : ℱ_{T_e} ⟶ ℱ_{T_e} ⊗ Ω_{T_e/S,δ̄} of ...SmallSite.crystalConnection, applied to the image of m over the whole of T_e and read in the sections of ℱ over the first-order thickening T'_e through the canonical morphism ℱ_{T_e} ⊗ Ω ⟶ p₀_* ℱ_{T'_e}, is the image of ∇(m) at the level e read there through the canonical map ω ⊗ s ↦ ω · p₀^* s.

theorem firstOrderTensorInclusion_crystalConnection_crystalPairFunctor
    (Fc : QuasiCoherentCrystal S) (e : ℕ) (m : wholeSpaceSections hp Fc ⦋0⦌) :
    (firstOrderTensorInclusion Fc.obj (levelObj hp 0 e)).val.app (op ⊤)
        ((crystalConnection (levelObj hp 0 e) Fc.property.2).hom.app (op ⊤)
          (crysSiteRestrict Fc.obj ((levelObj hp 0 e).restrictOpenHom ⊤)
            (show Fc.obj.val.obj (op (levelObj hp 0 e)) from pairComponent hp Fc e m))) =
      crysSiteRestrict Fc.obj
        ((firstOrderThickeningCrysObject S (levelObj hp 0 e)).restrictOpenHom ⊤)
        (AffineConnection.diffAction Fc.obj (levelObj hp 0 e)
          (pairTensorLevel hp Fc e (((crystalPairFunctor hp).obj Fc).nabla m)))

Crystalline.GlobalCrystallineSituation.SmallSite.crystalPairFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalPairFunctor07JG.lean, line 697. The attribute's comment: “the functor from the crystals in quasi-coherent O_{X/S}-modules on Cris(X/S) to the pairs (M, ∇) satisfying (07JB), (07JC), (07JD) and (07JE), for any surjective polynomial presentation g : P = A[x_i : i ∈ ι] → C, supplied as the WholeSpacePresentation instance (the default instance is the tautological one): M = lim_e Γ(T_e, F), ∇ read off the Taylor expansion of the crystal over D(1); that ∇ is the 07J6 connection evaluated on the T_e is pairTensorLevel_crystalPairFunctor_nabla”.

[Stacks, Lemma 60.17.3, Tag 07JG]: the functor

\{crystals in quasi-coherent 𝒪\_\{X/S}-modules on Cris(X/S)} ⟶ \{pairs (M, ∇) satisfying (07JB), (07JC), (07JD) and (07JE)},

in the situation of [Stacks, Section 60.17, Tag 07J7]: X = Spec(C), S = Spec(A) affine with p nilpotent on C, P = A[x_i : i ∈ ι] → C any surjective polynomial presentation (the instance ...SmallSite.WholeSpacePresentation S hp the system of thickenings is built from; by default A[x_c : c ∈ C] → C), D the p-adically completed divided power envelope (07J8), Ω_D its completed module of divided power differentials (07J9) and d : D → Ω_D (07JA). It sends a crystal ℱ to M = lim_e Γ((X, T_e, δ̄), ℱ) with the connection read off the crystal's Taylor expansion over D(1), and a morphism of crystals to the induced map of the limits. That this connection is the canonical connection of [Stacks, Tag 07J6] evaluated on the finite thickenings (X, T_e, δ̄) is ...SmallSite.pairTensorLevel_crystalPairFunctor_nabla and ...SmallSite.firstOrderTensorInclusion_crystalConnection_crystalPairFunctor.

def crystalPairFunctor :
    QuasiCoherentCrystal S ⥤ Pair.{u, u, u, u} S.p (pairRing hp) (pairForms hp) (pairDx hp)
      (derivationFun ((affineSituation S hp).A : Type u) (pairRing hp) _ (pairForms hp)
        (pairDerivation hp))

Tag 07JH, a proposition

Tag 07JH in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crystalPairFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalPairEquivalence.lean, line 633. The attribute's comment: “for any surjective polynomial presentation g : P = A[x_i : i ∈ ι] → C, supplied as the WholeSpacePresentation instance (the default instance is the tautological one): the functor of 07JG, from the crystals in quasi-coherent O_{X/S}-modules on Cris(X/S) to the pairs (M, ∇) over D satisfying (07JB), (07JC), (07JD) and (07JE), with its connection the canonical connection of 07J6 evaluated on the finite thickenings (pairTensorLevel_crystalPairFunctor_nabla), is an equivalence of categories”.

[Stacks, Proposition 60.17.4, Tag 07JH]: the functor of [Stacks, Lemma 60.17.3, Tag 07JG]

\{crystals in quasi-coherent 𝒪\_\{X/S}-modules on Cris(X/S)} ⟶ \{pairs (M, ∇) satisfying (07JB), (07JC), (07JD) and (07JE)}

is an equivalence of categories. This is the functor ...SmallSite.crystalPairFunctor of the tag 07JG, in the situation of [Stacks, Section 60.17, Tag 07J7]: X = Spec(C), S = Spec(A) affine with p nilpotent on C, any surjective polynomial presentation P = A[x_i : i ∈ ι] → C (the instance ...SmallSite.WholeSpacePresentation S hp the system of thickenings is built from; by default the tautological A[x_c : c ∈ C] → C), D the p-adically completed divided power envelope and Ω_D its completed module of divided power differentials. It sends ℱ to M = lim_e Γ((X, T_e, δ̄), ℱ) with its specified canonical crystalline connection: the canonical connection of [Stacks, Tag 07J6] evaluated on the finite thickenings (X, T_e, δ̄), which is ...SmallSite.pairTensorLevel_crystalPairFunctor_nabla.

theorem crystalPairFunctor_isEquivalence : (crystalPairFunctor hp).IsEquivalence

Tag 07L5, a lemma

Tag 07L5 in the Stacks Project.

Crystalline.exists_presentation_retract_pairEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/EnvelopeRetractEquivalence.lean, line 245. The attribute's comment: “both assertions, under exactly the source's hypotheses: for A -> P' smooth and P' -> C surjective, there are a polynomial presentation q : A[x_i] ->> P' with finitely many variables and divided power A-algebra maps a : D -> D', b : D' -> D between the p-adically completed envelopes, compatible with the augmentations to C, with a . b = id; and an equivalence of categories between the pairs (M, nabla) over D satisfying 07JB-07JE (Crystalline.Pair over the completed one-forms of D in the coordinates d x_i) and the pairs (M', nabla') over D' satisfying 07JB-07JE (Crystalline.RetractPair: p-adically complete, a completed connection over the completed forms of D' whose curvature vanishes, and 07JE read on the base change G(M', nabla') along b, as the proof defines it), whose functor is the base change along a and whose inverse is the base change along b; and, for the last sentence, a functor towards the pairs over D is an equivalence exactly when its composite with the base change towards D' is”.

[Stacks, Lemma 60.17.5, Tag 07L5]. In Situation [Stacks, Tag 07MD], let A → P' → C be ring maps with A → P' smooth and P' → C surjective with kernel J', and let D' be the p-adic completion of D_{P', γ}(J') (Crystalline.completedEnvelopeOfPresentation). Then

(first assertion) there are a choice of the data A → P → C — a polynomial algebra P = A[x_i] in finitely many variables with a surjection q : P ↠ P', P → C being the composite — and homomorphisms of divided power A-algebras a : D → D', b : D' → D between the p-adic completions of the divided power envelopes, compatible with the augmentations D → C and D' → C, with a ∘ b = id_{D'};

(second assertion) these maps induce an equivalence of categories between the pairs (M, ∇) over D satisfying (07JB)–(07JE) — Crystalline.Pair for the completed one-forms Ω_D with the coordinates d x_i — and the pairs (M', ∇') over D' satisfying them — Crystalline.RetractPair for the completed forms Ω^*_{D'}: p-adically complete, with a completed connection whose curvature vanishes, and topologically quasi-nilpotent in the sense the proof gives that condition over D', on G(M', ∇'). The functor is the base change F along a and its quasi-inverse the base change G along b;

(last sentence) consequently a functor towards the pairs over D — in particular the functor of [Stacks, Proposition 60.17.4, Tag 07JH] — is an equivalence exactly when its composite with F, towards the pairs over D', is one. For the functor of [Stacks, Tag 07JG] on crystals this is ...SmallSite.exists_presentation_retract_crystalPairEquivalence.

The proof of the second assertion is the source's: F ∘ G ≅ 𝟭 because a ∘ b = id, and G ∘ F ≅ 𝟭 by the Taylor comparison c_{id_D, b ∘ a}, whose horizontality — which the source omits — is Crystalline.coordOp_taylorRoundTrip.

theorem exists_presentation_retract_pairEquivalence :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (q : MvPolynomial ι s.A →ₐ[s.A] P')
      (hq : Function.Surjective q)
      (a : DPMorphism (envelopeCompletion (presentationEnvelope s (f'.comp q)) s.p
          (presentationEnvelope_prime_nilpotent s (f'.comp q) (hf'.comp hq))).dividedPowers
        (completedEnvelopeOfPresentation s f' hf').dividedPowers)
      (b : DPMorphism (completedEnvelopeOfPresentation s f' hf').dividedPowers
        (envelopeCompletion (presentationEnvelope s (f'.comp q)) s.p
          (presentationEnvelope_prime_nilpotent s (f'.comp q) (hf'.comp hq))).dividedPowers)
      (ha : ∀ c : (s.A : Type u), a (algebraMap (s.A : Type u)
          (envelopeCompletion (presentationEnvelope s (f'.comp q)) s.p
            (presentationEnvelope_prime_nilpotent s (f'.comp q) (hf'.comp hq)) : Type u) c) =
          algebraMap (s.A : Type u) (completedEnvelopeOfPresentation s f' hf' : Type u) c)
      (hb : ∀ c : (s.A : Type u), b (algebraMap (s.A : Type u)
          (completedEnvelopeOfPresentation s f' hf' : Type u) c) =
          algebraMap (s.A : Type u) (envelopeCompletion (presentationEnvelope s (f'.comp q)) s.p
            (presentationEnvelope_prime_nilpotent s (f'.comp q) (hf'.comp hq)) : Type u) c)
      (hab : ∀ x, a (b x) = x)
      (hρ : ∀ y, b (a y) - y ∈ (envelopeCompletion (presentationEnvelope s (f'.comp q)) s.p
          (presentationEnvelope_prime_nilpotent s (f'.comp q) (hf'.comp hq))).ideal),
      a.comp b = DPMorphism.id _ ∧
        (completedEnvelopeAugmentation s f' hf').comp a.toRingHom =
          completedEnvelopeAugmentation s (f'.comp q) (hf'.comp hq) ∧
        (completedEnvelopeAugmentation s (f'.comp q) (hf'.comp hq)).comp b.toRingHom =
          completedEnvelopeAugmentation s f' hf' ∧
        ∃ e : Pair.{u, u, u, u} s.p _
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).forms
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).dx
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).diff ≌
          RetractPair (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq))
            (envelopeRetractData _ s.p _ (completedEnvelopeOfPresentation s f' hf') a b ha hb
              hab hρ),
          e.functor = retractForwardFunctor _ (envelopeRetractData _ s.p _
            (completedEnvelopeOfPresentation s f' hf') a b ha hb hab hρ) ∧
          e.inverse = retractBackFunctor _ (envelopeRetractData _ s.p _
            (completedEnvelopeOfPresentation s f' hf') a b ha hb hab hρ) ∧
          ∀ {𝒞 : Type w} [Category.{w'} 𝒞] (Φ : 𝒞 ⥤ Pair.{u, u, u, u} s.p _
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).forms
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).dx
            (polynomialEnvelopeCoordinates s (f'.comp q) (hf'.comp hq)).diff),
            Φ.IsEquivalence ↔ (Φ ⋙ e.functor).IsEquivalence

Crystalline.GlobalCrystallineSituation.SmallSite.exists_presentation_retract_crystalPairEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalRetractPairs07L5.lean, line 208. The attribute's comment: “all three parts in the situation of 07J7 (X = Spec C, S = Spec A affine, p nilpotent on C), for A -> P' smooth and P' -> C surjective: a polynomial presentation q : A[x_i] ->> P' in finitely many variables, the system of 07JN being presented by A[x_(0,i)] -> P' -> C (WholeSpacePresentation S hp), and divided power A-algebra maps a : D -> D', b : D' -> D compatible with the augmentations, with a . b = id; an equivalence between the pairs over D and the pairs over D' satisfying 07JB-07JE whose functor is the base change along a and whose inverse is the base change along b; and the last sentence: the functor of 07JG for that presentation, from the crystals in quasi-coherent O_{X/S}-modules on Cris(X/S), followed by the base change along a towards the pairs over D' (crystalRetractPairFunctor), is an equivalence”.

[Stacks, Lemma 60.17.5, Tag 07L5], for the crystals of [Stacks, Tag 07JH]. In the situation of [Stacks, Section 60.17, Tag 07J7], X = Spec(C) and S = Spec(A) affine with p nilpotent on C, let A → P' → C be ring maps with A → P' smooth and P' → C surjective, and let D' be the p-adic completion of D_{P', γ}(J'). Then

(first assertion) there are a choice of the data A → P → C — a polynomial algebra P = A[x_i] in finitely many variables with a surjection q : P ↠ P', the presentation of the system of [Stacks, Tag 07JN] being the composite P → P' → C — and homomorphisms of divided power A-algebras a : D → D', b : D' → D compatible with the augmentations to C, with a ∘ b = id_{D'};

(second assertion) these maps induce an equivalence of categories e between the pairs over D and the pairs over D' satisfying (07JB)–(07JE), with functor the base change F along a and quasi-inverse the base change G along b;

(last sentence) the equivalence of [Stacks, Proposition 60.17.4, Tag 07JH] also holds for the corresponding functor towards the pairs over D': the functor ...SmallSite.crystalRetractPairFunctor from the crystals in quasi-coherent 𝒪_{X/S}-modules on Cris(X/S), which is the functor of [Stacks, Tag 07JG] (...SmallSite.crystalPairFunctor, for the presentation P → C) followed by F, is an equivalence of categories.

theorem exists_presentation_retract_crystalPairEquivalence (P' : Type u) [CommRing P']
    [Algebra ((affineSituation S hp).A : Type u) P']
    [Algebra.Smooth ((affineSituation S hp).A : Type u) P']
    (f' : P' →ₐ[(affineSituation S hp).A] (affineSituation S hp).C)
    (hf' : Function.Surjective f') :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι)
      (q : MvPolynomial ι (affineSituation S hp).A →ₐ[(affineSituation S hp).A] P')
      (hq : Function.Surjective q),
      letI : WholeSpacePresentation S hp := ⟨ι, f'.comp q, hf'.comp hq⟩
      ∃ (a : DPMorphism (systemEnvelopeCompletion hp).dividedPowers
          (completedEnvelopeOfPresentation (affineSituation S hp) f' hf').dividedPowers)
        (b : DPMorphism
          (completedEnvelopeOfPresentation (affineSituation S hp) f' hf').dividedPowers
          (systemEnvelopeCompletion hp).dividedPowers)
        (ha : ∀ c : ((affineSituation S hp).A : Type u),
          a (algebraMap ((affineSituation S hp).A : Type u) (systemEnvelopeCompletion hp) c) =
            algebraMap ((affineSituation S hp).A : Type u)
              (completedEnvelopeOfPresentation (affineSituation S hp) f' hf' : Type u) c)
        (hb : ∀ c : ((affineSituation S hp).A : Type u),
          b (algebraMap ((affineSituation S hp).A : Type u)
              (completedEnvelopeOfPresentation (affineSituation S hp) f' hf' : Type u) c) =
            algebraMap ((affineSituation S hp).A : Type u) (systemEnvelopeCompletion hp) c)
        (hab : ∀ x, a (b x) = x)
        (hρ : ∀ y, b (a y) - y ∈ (systemEnvelopeCompletion hp).ideal),
        a.comp b = DPMorphism.id _ ∧
        (completedEnvelopeAugmentation (affineSituation S hp) f' hf').comp a.toRingHom =
          completedEnvelopeAugmentation (affineSituation S hp)
            (tensorPowerPresentation (affineSituation S hp) (wholeSpacePresentation S hp) 0)
            (tensorPowerPresentation_surjective (affineSituation S hp)
              (wholeSpacePresentation S hp) (wholeSpacePresentation_surjective S hp) 0) ∧
        (completedEnvelopeAugmentation (affineSituation S hp)
            (tensorPowerPresentation (affineSituation S hp) (wholeSpacePresentation S hp) 0)
            (tensorPowerPresentation_surjective (affineSituation S hp)
              (wholeSpacePresentation S hp) (wholeSpacePresentation_surjective S hp) 0)).comp
            b.toRingHom =
          completedEnvelopeAugmentation (affineSituation S hp) f' hf' ∧
        ∃ e : Pair.{u, u, u, u} (affineSituation S hp).p _ (systemEnvelopeCoordinates hp).forms
            (systemEnvelopeCoordinates hp).dx (systemEnvelopeCoordinates hp).diff ≌
          RetractPair (systemEnvelopeCoordinates hp)
            (envelopeRetractData _ (affineSituation S hp).p _
              (completedEnvelopeOfPresentation (affineSituation S hp) f' hf') a b ha hb hab hρ),
          e.functor = retractForwardFunctor _ (envelopeRetractData _ (affineSituation S hp).p _
            (completedEnvelopeOfPresentation (affineSituation S hp) f' hf') a b ha hb hab hρ) ∧
          e.inverse = retractBackFunctor _ (envelopeRetractData _ (affineSituation S hp).p _
            (completedEnvelopeOfPresentation (affineSituation S hp) f' hf') a b ha hb hab hρ) ∧
          crystalRetractPairFunctor hp _ a b ha hb hab hρ =
            crystalPairFunctor hp ⋙ pairCatToTensorPowerPairs hp ⋙
              (tensorPowerPairFormsEquivalence (affineSituation S hp)
                (wholeSpacePresentation S hp) (wholeSpacePresentation_surjective S hp)).functor ⋙
              e.functor ∧
          (crystalRetractPairFunctor hp _ a b ha hb hab hρ).IsEquivalence

Tag 07L6, a remark

Tag 07L6 in the Stacks Project.

Crystalline.exists_dpMorphism_envelope_of_hasStrongLiftingProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/StrongLiftingEnvelope.lean, line 248. The attribute's comment: “the hypothesis-generalisation of the lifting step in the proof of 07L5: smoothness of P'/A is used only through the strong lifting property of 07K4, which is here a hypothesis. The equivalence of categories asserted by 07L6 is NOT proved: the source defers its own proof of it”.

The lifting step of the construction in the proof of [Stacks, Tag 07L5], with smoothness replaced by the strong lifting property of [Stacks, Tag 07K4].

Let (A, I, γ) be a divided power ring, let P' be an A-algebra with the strong lifting property, let π : P' → C be a ring map whose kernel contains the image of I, and let D be the divided power envelope of ker π. Let (B, K, δ) be a divided power ring, aB : A → B a divided power morphism, and suppose p is nilpotent in B for a prime p. Given an ideal L ⊆ K and a ring map g : P' → B ⧸ L which restricts to aB on A and whose further reduction to B ⧸ K is induced by π, there is a divided power morphism b : D → (B, K, δ) over A whose restriction along P' → D, read modulo L, is g, and which is compatible with the maps to C: its restriction read modulo K is induced by π.

Taking B = D_e and L = ker(D_e → D'_e) this is the step of the source's proof which produces β_e : P' → D_e lifting P' → D'_e and then the map D_{P', γ}(J') → D_e.

theorem exists_dpMorphism_envelope_of_hasStrongLiftingProperty {p : ℕ} (hp : p.Prime)
    (A : DividedPowerRing.{u}) {P' : Type u} [CommRing P'] [Algebra A P']
    {C : Type v} [CommRing C] (π : P' →+* C)
    {hJ : A.ideal.map (algebraMap A P') ≤ RingHom.ker π}
    (D : DividedPowerEnvelope A (algebraMap A P') (RingHom.ker π) hJ)
    (hlift : Algebra.HasStrongLiftingProperty A P')
    (B : DividedPowerRing.{u}) (hpB : IsNilpotent (p : B))
    (aB : DividedPowers.DPMorphism A.dividedPowers B.dividedPowers)
    {L : Ideal B} (hL : L ≤ B.ideal) (c : C →+* B ⧸ B.ideal) (g : P' →+* B ⧸ L)
    (hgA : g.comp (algebraMap A P') = (Ideal.Quotient.mk L).comp aB.toRingHom)
    (hgC : (Ideal.Quotient.factor hL).comp g = c.comp π) :
    ∃ b : DividedPowers.DPMorphism D.object.dividedPowers B.dividedPowers,
      b.comp D.structureMap = aB ∧
        (Ideal.Quotient.mk L).comp (b.toRingHom.comp D.algebraMap.toRingHom) = g ∧
        (Ideal.Quotient.mk B.ideal).comp (b.toRingHom.comp D.algebraMap.toRingHom) =
          c.comp π

Sources

LeanCrystalline.pAdicCompletedDividedPowerEnvelope · Crystalline.pAdicCompletedDividedPowerDifferentials · Crystalline.pAdicCompletedDividedPowerDifferentialsEquivLimit · Crystalline.pAdicCompletedDividedPowerDifferentialsEquivCompletion · Crystalline.exists_dividedPowerDifferentialsCompletionEquiv · Crystalline.completedDividedPowerDifferential · Crystalline.pAdicCompletedTensorPowerEnvelope · Crystalline.exists_ringEquiv_pAdicCompletedDividedPowerPolynomial

Section60.18 General remarks on cohomology #

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

Tag 07JJ, a lemma

Tag 07JJ in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.vanishing07JJ_abelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/StandardCoverAcyclicity.lean, line 302. The attribute's comment: “the case of the objects (U, T, δ) whose ambient divided power scheme T is affine, in the packaged form SmallSite.Vanishing07JJ that the consumers of the tag in this library use, and for the abelian sheaf SmallSite.abelianSheaf F of the coefficient universe u + 1 attached to a locally quasi-coherent module F. The source's remaining case of U affine is reduced to this one in isZero_overCohomology_abelianSheaf_of_isAffine, which states both”.

Let F be a locally quasi-coherent sheaf of 𝒪_{X/S}-modules on the small crystalline site Cris(X/S) of a global crystalline situation. Then for every object (U, T, δ) of Cris(X/S) whose ambient divided power scheme T is affine, and every p > 0, the cohomology of the localized site vanishes:

H^p(Cris(X/S)/(U, T, δ), F) = 0.

The statement is about the abelian sheaf SmallSite.abelianSheaf F of the coefficient universe u + 1, which is the universe in which the cohomology of Cris(X/S) and of its localizations exists; the modules of F itself live in Type u.

theorem vanishing07JJ_abelianSheaf (F : SheafOfModules.{u} (structureSheaf S))
    (hF : IsLocallyQuasiCoherent F) : Vanishing07JJ S (abelianSheaf F)

Crystalline.GlobalCrystallineSituation.SmallSite.isZero_overCohomology_abelianSheaf_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/StandardCoverAcyclicity.lean, line 323. The attribute's comment: “both cases of the hypothesis: the objects (U, T, δ) with T or U affine, for the abelian sheaf SmallSite.abelianSheaf F of the coefficient universe u + 1 attached to a locally quasi-coherent module F”.

Let F be a locally quasi-coherent sheaf of 𝒪_{X/S}-modules on the small crystalline site Cris(X/S) of a global crystalline situation. Then for every object (U, T, δ) of Cris(X/S) with T or U affine, and every p > 0, the cohomology of the localized site vanishes:

H^p(Cris(X/S)/(U, T, δ), F) = 0.

theorem isZero_overCohomology_abelianSheaf_of_isAffine
    (F : SheafOfModules.{u} (structureSheaf S)) (hF : IsLocallyQuasiCoherent F)
    (A : CrystallineThickening S)
    (hA : IsAffine A.obj.thickening.target.scheme ∨ IsAffine A.obj.thickening.source)
    (p : ℕ) (hp : 0 < p) :
    IsZero ((overCohomologyFunctor S A p).obj ((restrictToOver S A).obj (abelianSheaf F)))

Tag 07JK, a lemma

Tag 07JK in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.chaoticCohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/ChaoticComparison.lean, line 113. The attribute's comment: “for the abelian sheaf SmallSite.abelianSheaf F of the coefficient universe u + 1 attached to a locally quasi-coherent sheaf F of 𝒪_{X/S}-modules, which is the generality in which the input [Stacks, Tag 07JJ] holds”.

In Situation [Stacks, Tag 07MF] with X and S affine, let 𝒞 ⊆ Cris(X/S) be the full subcategory of divided power thickenings (X, T, δ) of the whole of X with the chaotic topology of [Stacks, Tag 07GE]. Then for every locally quasi-coherent sheaf F of 𝒪_{X/S}-modules on Cris(X/S) and every degree j,

H^j(𝒞, F|_𝒞) ≅ H^j(Cris(X/S), F).

Both sides are read on the abelian sheaf SmallSite.abelianSheaf F of the coefficient universe u + 1.

def chaoticCohomologyComparisonIso (F : SheafOfModules.{u} (structureSheaf S))
    (hF : IsLocallyQuasiCoherent F) (j : ℕ) :
    (chaoticCohomologyFunctor S j).obj ((restrictToWhole S).obj (abelianSheaf F)) ≅
      (cohomologyFunctor S j).obj (abelianSheaf F)

Tag 07JL, a lemma

Tag 07JL in the Stacks Project.

Crystalline.completedCrystallineToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineCrystallineSite/CompletedToposMorphism.lean, line 170. The attribute's comment: “the morphism of topoi”.

The morphism of topoi induced by the canonical functor from crystalline thickenings to completed crystalline thickenings.

public def completedCrystallineToposMorphism
    (S : AffineCrystallineSituation.{u, v}) :
    MorphismOfTopoi
      (Sheaf (⊥ : GrothendieckTopology (CrystallineThickening.{u, v, w} S)ᵒᵖ)
        (Type (max u v (w + 1))))
      (Sheaf (⊥ : GrothendieckTopology (CompletedCrystallineThickening.{u, v, w} S)ᵒᵖ)
        (Type (max u v (w + 1))))

Crystalline.abelianSheafPushforwardIsoDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineCrystallineSite/CompletedToposMorphism.lean, line 209. The attribute's comment: “identification of the abelian direct image”.

The natural isomorphism identifying the abelian-sheaf pushforward induced by the crystalline site functor with the right Kan extension used to compute its derived functors. It comes from the uniqueness of right adjoints, and is an isomorphism of functors, not merely an objectwise comparison.

public noncomputable def abelianSheafPushforwardIsoDirectImage
    (S : AffineCrystallineSituation.{u, v}) :
    abelianSheafPushforward S ⋙
        (completedAbelianSheafEquivalence.{u, v, w} S).functor ≅
      (abelianSheafEquivalence.{u, v, w} S).functor ⋙ abelianDirectImage S

Crystalline.abelianSheafPushforwardForgetIsoPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineCrystallineSite/CompletedToposMorphism.lean, line 244. The attribute's comment: “compatibility with the geometric morphism”.

The natural isomorphism exhibiting the abelian-sheaf direct image, on underlying sets, as the direct image of the same morphism of topoi. It comes from the uniqueness of right adjoints, and is natural in the sheaf.

public noncomputable def abelianSheafPushforwardForgetIsoPushforward
    (S : AffineCrystallineSituation.{u, v}) :
    abelianSheafPushforward S ⋙
        sheafForget
          (⊥ : GrothendieckTopology (CompletedCrystallineThickening.{u, v, w} S)ᵒᵖ) ≅
      sheafForget
          (⊥ : GrothendieckTopology (CrystallineThickening.{u, v, w} S)ᵒᵖ) ⋙
        (completedCrystallineToposMorphism S).pushforward

Crystalline.abelianDirectImageObjObjIsoLimitFiniteLevelSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineCrystallineSite/CompletedToposMorphism.lean, line 320. The attribute's comment: “the direct image computed as the limit over the finite levels”.

The direct image of [Stacks, Tag 07JL], computed. For an abelian presheaf F on the ordinary affine crystalline category and a finite-level system T for a completed thickening X, the value at X of the direct image of F is the inverse limit of the sections of F on the finite-level quotients of X: g_*(F)(X) ≅ lim_e F(X/(p)^(N + e)).

The direct image is the right Kan extension along crystallineToCompleted, whose value at X is the limit over the structured-arrow category, and the finite-level diagram is initial there by Crystalline.finiteLevel_initial.

public noncomputable def abelianDirectImageObjObjIsoLimitFiniteLevelSections
    {S : AffineCrystallineSituation.{u, v}}
    (F : CrystallineThickening.{u, v, w} S ⥤ Ab.{max u v (w + 1)})
    {X : CompletedCrystallineThickening.{u, v, w} S} (T : FiniteLevelSystem X) :
    ((abelianDirectImage S).obj F).obj X ≅ limit (finiteLevelSections T F)

Crystalline.abelianSheafPushforwardObjObjIsoLimitFiniteLevelSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/AffineCrystallineSite/CompletedToposMorphism.lean, line 340. The attribute's comment: “the sections of the direct image as the limit over the finite levels”.

The sections of the direct image of [Stacks, Tag 07JL]. The value at a completed thickening X of the direct image of an abelian sheaf F on the ordinary affine crystalline site is the inverse limit of the sections of F on the finite-level quotients of X.

This is Crystalline.abelianDirectImageObjObjIsoLimitFiniteLevelSections transported along Crystalline.abelianSheafPushforwardIsoDirectImage, so that it speaks about the site-theoretic pushforward rather than the right Kan extension.

public noncomputable def abelianSheafPushforwardObjObjIsoLimitFiniteLevelSections
    (S : AffineCrystallineSituation.{u, v})
    (F : Sheaf (⊥ : GrothendieckTopology (CrystallineThickening.{u, v, w} S)ᵒᵖ)
      Ab.{max u v (w + 1)})
    {X : CompletedCrystallineThickening.{u, v, w} S} (T : FiniteLevelSystem X) :
    ((completedAbelianSheafEquivalence.{u, v, w} S).functor.obj
        ((abelianSheafPushforward S).obj F)).obj X ≅
      limit (finiteLevelSections T
        ((abelianSheafEquivalence.{u, v, w} S).functor.obj F))

Crystalline.rightDerivedPushforwardSectionsIsoRightDerivedLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CompletedHigherDirectImages.lean, line 53. The attribute's comment: “the higher direct images as the derived limits over the finite levels”.

For an abelian sheaf 𝓖 on 𝒞 = (Cris(C/A))ᵒᵖ, a completed thickening B and every degree p, the sections over B of the p-th higher direct image of 𝓖 along the morphism of topoi g : Sh(𝒞) ⟶ Sh(𝒞^∧) are the p-th derived inverse limit of the sections of 𝓖 on the finite levels of B:

R ᵖ g_* 𝓖 (B) ≅ R ᵖ lim_e 𝓖(B/(p)^{N + e}).

def rightDerivedPushforwardSectionsIsoRightDerivedLimit
    (𝓖 : Sheaf (littleChaoticTopology.{u, v, w} s) Ab.{max u v (w + 1)})
    (B : CompletedCrystallineThickening.{u, v, w} s) (p : ℕ) :
    ((completedAbelianSheafEquivalence.{u, v, w} s).functor.obj
        (((abelianSheafPushforward.{u, v, w} s).rightDerived p).obj 𝓖)).obj B ≅
      ((lim : Rlim.InvSystemAb.{max u v (w + 1)} ⥤ Ab.{max u v (w + 1)}).rightDerived p).obj
        (finiteLevelSections (uniformLevelSystem B)
          ((abelianSheafEquivalence.{u, v, w} s).functor.obj 𝓖))

Crystalline.rightDerivedOnePushforwardSectionsIsoRightDerivedOneLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CompletedHigherDirectImages.lean, line 71. The attribute's comment: “the first higher direct image as the first derived limit over the finite levels”.

R ¹ g_* 𝓖 (B) ≅ R ¹ lim_e 𝓖(B_e): for an abelian sheaf 𝓖 on 𝒞 = (Cris(C/A))ᵒᵖ and a completed thickening B, the sections over B of the first higher direct image of 𝓖 along the morphism of topoi g : Sh(𝒞) ⟶ Sh(𝒞^∧) are the first derived inverse limit of the inverse system e ↦ 𝓖(B/(p)^{N + e}) of sections on the finite levels of B.

def rightDerivedOnePushforwardSectionsIsoRightDerivedOneLimit
    (𝓖 : Sheaf (littleChaoticTopology.{u, v, w} s) Ab.{max u v (w + 1)})
    (B : CompletedCrystallineThickening.{u, v, w} s) :
    ((completedAbelianSheafEquivalence.{u, v, w} s).functor.obj
        (((abelianSheafPushforward.{u, v, w} s).rightDerived 1).obj 𝓖)).obj B ≅
      ((lim : Rlim.InvSystemAb.{max u v (w + 1)} ⥤ Ab.{max u v (w + 1)}).rightDerived 1).obj
        (finiteLevelSections (uniformLevelSystem B)
          ((abelianSheafEquivalence.{u, v, w} s).functor.obj 𝓖))

Crystalline.isZero_rightDerived_abelianSheafPushforward_of_two_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CompletedHigherDirectImages.lean, line 85. The attribute's comment: “the vanishing of the higher direct images in degrees at least two”.

R ᵖ g_* 𝓖 = 0 for every p ≥ 2 and every abelian sheaf 𝓖 on 𝒞 = (Cris(C/A))ᵒᵖ, where g_* is the direct image Crystalline.abelianSheafPushforward of the morphism of topoi g : Sh(𝒞) ⟶ Sh(𝒞^∧).

theorem isZero_rightDerived_abelianSheafPushforward_of_two_le
    (𝓖 : Sheaf (littleChaoticTopology.{u, v, w} s) Ab.{max u v (w + 1)})
    (p : ℕ) (hp : 2 ≤ p) :
    IsZero (((abelianSheafPushforward.{u, v, w} s).rightDerived p).obj 𝓖)

Tag 07JM, a lemma

Tag 07JM in the Stacks Project.

Stacks.Cohomology.derivedGlobalSectionsIsoPowerCechComplexExtend, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Acyclicity/ChaoticSiteCoveringObject.lean, line 584.

Stacks Project, Tag 07JM. Let 𝒞 carry the chaotic topology, let X be an object of 𝒞 to which every object of 𝒞 admits a morphism, and let 𝒞 have products of pairs. For every abelian sheaf 𝓕 on 𝒞 the total cohomology RΓ(𝒞, 𝓕) is represented by the complex 𝓕(X) → 𝓕(X × X) → 𝓕(X × X × X) → ⋯ associated to the cosimplicial abelian group [n] ↦ 𝓕(X^{n + 1}).

This is the comparison itself, an isomorphism of complexes of abelian groups between RΓ(𝒞, 𝓕) and that complex placed in the nonnegative degrees. An isomorphism of complexes is sent to an isomorphism of D(Ab) by the localisation functor, which is Stacks.Cohomology.derivedGlobalSectionsQIsoPowerCechComplexExtend, and to the isomorphism of cohomology groups in each degree, which is Stacks.Cohomology.sheafHAddEquivPowerCechComplexHomology.

def derivedGlobalSectionsIsoPowerCechComplexExtend :
    chaoticDerivedGlobalSections X hX F ≅
      (powerCechComplex F.obj X).extend ComplexShape.embeddingUpNat

Stacks.Cohomology.derivedGlobalSectionsQIsoPowerCechComplexExtend, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Acyclicity/ChaoticSiteCoveringObject.lean, line 600.

Stacks Project, Tag 07JM, in the derived category of abelian groups: on the chaotic site with a covering object X and products of pairs, RΓ(𝒞, 𝓕) and the complex 𝓕(X) → 𝓕(X × X) → 𝓕(X × X × X) → ⋯ become isomorphic in D(Ab).

This is Stacks.Cohomology.derivedGlobalSectionsIsoPowerCechComplexExtend read through the localisation functor CategoryTheory.DerivedCategory.Q. The instance HasDerivedCategory.{w} AddCommGrpCat.{u} only chooses a model of D(Ab) with morphisms in a given universe; one always exists, by CategoryTheory.HasDerivedCategory.standard.

def derivedGlobalSectionsQIsoPowerCechComplexExtend
    [HasDerivedCategory.{w} AddCommGrpCat.{u}] :
    DerivedCategory.Q.obj (chaoticDerivedGlobalSections X hX F) ≅
      DerivedCategory.Q.obj ((powerCechComplex F.obj X).extend ComplexShape.embeddingUpNat)

Stacks.Cohomology.sheafHAddEquivPowerCechComplexHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Acyclicity/ChaoticSiteCoveringObject.lean, line 614.

Stacks Project, Tag 07JM in degree n: the cohomology H^n(𝒞, 𝓕) of the chaotic site is the degree-n cohomology of the complex 𝓕(X) → 𝓕(X × X) → 𝓕(X × X × X) → ⋯.

This is H^n of Stacks.Cohomology.derivedGlobalSectionsIsoPowerCechComplexExtend, the cohomology of RΓ(𝒞, 𝓕) being CategoryTheory.Sheaf.H by CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass. It is the map whose existence Stacks.Cohomology.nonempty_addEquiv_sheafH_homology_powerCechComplex asserts.

def sheafHAddEquivPowerCechComplexHomology
    [HasExt.{u} (Sheaf (⊥ : GrothendieckTopology C) AddCommGrpCat.{u})] (n : ℕ) :
    Sheaf.H F n ≃+ (powerCechComplex F.obj X).homology n

Stacks.Cohomology.functorHObjIsoPowerCechComplexHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Acyclicity/ChaoticSiteCoveringObject.lean, line 634.

Stacks Project, Tag 07JM in degree n, as an isomorphism of objects of AddCommGrpCat: the value at 𝓕 of Mathlib's cohomology functor CategoryTheory.Sheaf.functorH of the chaotic site is the degree-n cohomology of the complex 𝓕(X) → 𝓕(X × X) → 𝓕(X × X × X) → ⋯.

This is Stacks.Cohomology.sheafHAddEquivPowerCechComplexHomology read as a morphism of the category AddCommGrpCat, which is the form in which an isomorphism of cohomology groups is stated elsewhere in the library.

def functorHObjIsoPowerCechComplexHomology
    [HasExt.{u} (Sheaf (⊥ : GrothendieckTopology C) AddCommGrpCat.{u})] (n : ℕ) :
    (Sheaf.functorH (⊥ : GrothendieckTopology C) n).obj F ≅
      (powerCechComplex F.obj X).homology n

Stacks.Cohomology.nonempty_addEquiv_sheafH_homology_powerCechComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Acyclicity/ChaoticSiteCoveringObject.lean, line 682.

Stacks Project, Tag 07JM. Let 𝒞 carry the chaotic topology, let X be an object of 𝒞 to which every object of 𝒞 admits a morphism, and let the nonempty finite powers X^{n + 1} of X exist in 𝒞. For every abelian sheaf 𝓕 on 𝒞 the total cohomology RΓ(𝒞, 𝓕) is represented by the complex 𝓕(X) → 𝓕(X × X) → 𝓕(X × X × X) → ⋯ associated to the cosimplicial abelian group [n] ↦ 𝓕(X^{n + 1}): in every degree the cohomology of the site agrees with the cohomology of that complex.

The source asks 𝒞 to have products of pairs; the hypothesis here is the weaker one that the proof uses, and the source's implies it by Stacks.Cohomology.hasProduct_fin_succ.

The comparison itself is Stacks.Cohomology.addEquivSheafHHomologyPowerCechComplex; this is that def read as an existence statement.

theorem nonempty_addEquiv_sheafH_homology_powerCechComplex
    [HasExt.{u} (Sheaf (⊥ : GrothendieckTopology C) AddCommGrpCat.{u})] (n : ℕ) :
    Nonempty (Sheaf.H F n ≃+ (powerCechComplex F.obj X).homology n)

Sources

LeanCrystalline.GlobalCrystallineSituation.SmallSite.vanishing07JJ_abelianSheaf · Crystalline.GlobalCrystallineSituation.SmallSite.isZero_overCohomology_abelianSheaf_of_isAffine · Crystalline.GlobalCrystallineSituation.SmallSite.chaoticCohomologyComparisonIso · Crystalline.completedCrystallineToposMorphism · Crystalline.abelianSheafPushforwardIsoDirectImage · Crystalline.abelianSheafPushforwardForgetIsoPushforward · Crystalline.abelianDirectImageObjObjIsoLimitFiniteLevelSections · Crystalline.abelianSheafPushforwardObjObjIsoLimitFiniteLevelSections

Section60.19 Cosimplicial preparations #

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

Tag 07L7, an example

Tag 07L7 in the Stacks Project.

Crystalline.simplexVertexModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial/Preparation.lean, line 64. The attribute's comment: “the cosimplicial module”.

Stacks 07L7, the module. For a cosimplicial ring A, the cosimplicial A-module which in degree n is free on the vertices 0, ..., n; a map f : [n] ⟶ [m] sends the free generator at i to the free generator at f(i).

public noncomputable def simplexVertexModule (A : CosimplicialObject CommRingCat.{u}) :
    CosimplicialModule A

Crystalline.simplexVertexModuleContractingHomotopy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial/Preparation.lean, line 97. The attribute's comment: “the contracting homotopy”.

Stacks 07L7, the contraction. The specified homotopy from the identity endomorphism of the cosimplicial module freely generated by the vertices to its zero endomorphism.

public noncomputable def simplexVertexModuleContractingHomotopy
    (A : CosimplicialObject CommRingCat.{u}) :
    Homotopy (𝟙 (simplexVertexModule A))
      (0 : simplexVertexModule A ⟶ simplexVertexModule A)

Crystalline.simplexVertexModuleContractingHomotopy_apply_freeMk_objMk₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial/Preparation.lean, line 167. The attribute's comment: “the formula on generators”.

Stacks 07L7, the formula for the contraction. On the generator e_i, at the simplex αʲ : [n] → [1] which is zero precisely before j, the contraction is e_i if i < j and zero otherwise.

public theorem simplexVertexModuleContractingHomotopy_apply_freeMk_objMk₁
    (A : CosimplicialObject CommRingCat.{u}) (n : SimplexCategory)
    (i : Fin (n.len + 1)) (j : Fin (n.len + 2)) :
    (simplexVertexModuleContractingHomotopy A).app n (SSet.stdSimplex.objMk₁ j)
        (ModuleCat.freeMk (ULift.up i)) =
      if i.castSucc < j then ModuleCat.freeMk (ULift.up i) else 0

Tag 07L9, a lemma

Tag 07L9 in the Stacks Project.

Crystalline.id_cosimplicialEnvelopeDifferentials_homotopic_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial/CompletedDifferentials.lean, line 1041.

Stacks Project, Tag 07L9. With the notation of equation (07L0), the complex

Ω_{D(0)} → Ω_{D(1)} → Ω_{D(2)} → ⋯

of p-adically completed modules of divided power differentials is homotopic to zero as a D(*)-cosimplicial module: the identity endomorphism of the cosimplicial module Ω_{D(*)} over the cosimplicial ring D(*) is homotopic to its zero endomorphism.

public theorem id_cosimplicialEnvelopeDifferentials_homotopic_zero
    (E : CosimplicialEnvelope s f hf) :
    Homotopic (𝟙 E.differentials) 0

Tag 07LA, a lemma

Tag 07LA in the Stacks Project.

Crystalline.id_completedTensorCompletedForms_homotopic_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Cosimplicial/CompletedForms.lean, line 534.

Stacks Project, Tag 07LA. With the notation of the equations (07JF) for D(n) and (07L0) for Ω_{D(n)}, given any cosimplicial module M_* over D(*) and any i > 0, the cosimplicial module

M_0 ⊗̂_{D(0)} Ω^i_{D(0)} → M_1 ⊗̂_{D(1)} Ω^i_{D(1)} → M_2 ⊗̂_{D(2)} Ω^i_{D(2)} → ⋯

is homotopic to zero, where Ω^i_{D(n)} is the p-adic completion of the i-th exterior power of Ω_{D(n)} and ⊗̂ is the p-adic completion of the tensor product.

By Tag 07L9 the identity and the zero endomorphism of Ω_{D(*)} are homotopic. Applying the functor ∧^i keeps them homotopic, and for i > 0 turns the zero endomorphism into the zero endomorphism, so the identity of ∧^i Ω_{D(*)} is homotopic to zero; the p-adic completion functor then gives the same for Ω^i_{D(*)}, tensoring with M_* gives it for M_* ⊗_{D(*)} Ω^i_{D(*)}, and a final p-adic completion finishes the proof.

public theorem id_completedTensorCompletedForms_homotopic_zero
    (E : CosimplicialEnvelope s f hf) (M : CosimplicialModule E.ring) {i : ℕ} (hi : 0 < i) :
    Homotopic (𝟙 ((pAdicCosimplicialIdeal E.ring s.p).completion
      (M ⊗ (pAdicCosimplicialIdeal E.ring s.p).completion
        ((exteriorPowerFunctor E.ring i).functor.obj E.differentials)))) 0

Sources

LeanCrystalline.simplexVertexModule · Crystalline.simplexVertexModuleContractingHomotopy · Crystalline.simplexVertexModuleContractingHomotopy_apply_freeMk_objMk₁ · Crystalline.id_cosimplicialEnvelopeDifferentials_homotopic_zero · Crystalline.id_completedTensorCompletedForms_homotopic_zero

Section60.20 Divided power Poincaré lemma #

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

Tag 07LC, a lemma

Tag 07LC in the Stacks Project.

Crystalline.CompletedPoincare.completedDeRham_tensor_augmentation_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedExactness.lean, line 802. The attribute's comment: “completed_exactness”.

Stacks Project, Tag 07LC, completed case. The first map M → M ⊗̂_A D of the completed divided power de Rham complex of P = A⟨x_w⟩ with coefficients in a p-adically complete A-module M is injective.

public theorem completedDeRham_tensor_augmentation_injective
    (hM : IsAdicComplete (pAdicIdeal (A := A) p) M) :
    Function.Injective (augmentation p A W (canonicalCompletedDividedPowers p A W) M)

Crystalline.CompletedPoincare.completedDeRham_tensor_exact_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedExactness.lean, line 817. The attribute's comment: “completed_exactness”.

Stacks Project, Tag 07LC, completed case. The completed divided power de Rham complex of P = A⟨x_w⟩ with coefficients in a p-adically complete A-module M is exact at M ⊗̂_A D.

public theorem completedDeRham_tensor_exact_augmentation
    (hM : IsAdicComplete (pAdicIdeal (A := A) p) M) :
    Function.Exact (augmentation p A W (canonicalCompletedDividedPowers p A W) M)
      (differential p A W (canonicalCompletedDividedPowers p A W) M 0)

Crystalline.CompletedPoincare.completedDeRham_tensor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedExactness.lean, line 828. The attribute's comment: “completed_exactness”.

Stacks Project, Tag 07LC, completed case. The completed divided power de Rham complex of P = A⟨x_w⟩ with coefficients in a p-adically complete A-module M is exact at M ⊗̂_A Ω^{i+1}_D for every i.

public theorem completedDeRham_tensor_exact
    (_hM : IsAdicComplete (pAdicIdeal (A := A) p) M) (i : ℕ) :
    Function.Exact (differential p A W (canonicalCompletedDividedPowers p A W) M i)
      (differential p A W (canonicalCompletedDividedPowers p A W) M (i + 1))

Crystalline.dividedPowerPolynomialDeRham_tensor_augmentation_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedRing.lean, line 71. The attribute's comment: “ordinary_exactness”.

The divided power Poincaré lemma, exactness at the coefficient module. For a ring A, a family of variables W and the divided power polynomial algebra P = A⟨x_w : w ∈ W⟩ with its canonical divided powers, the first map M → M ⊗[A] P of the complex

0 → M → M ⊗[A] P → M ⊗[A] Ω¹_{P/A,δ} → M ⊗[A] Ω²_{P/A,δ} → ⋯

is injective for every A-module M; the degree-zero term of the complex is identified with M by Crystalline.coefficientLinearEquiv.

public theorem dividedPowerPolynomialDeRham_tensor_augmentation_injective
    (A : Type u) [CommRing A] (W : Type w)
    (M : Type v) [AddCommGroup M] [Module A M] :
    Function.Injective
      ((augmentedDividedPowerDeRhamDifferential A W 0).hom.lTensor M)

Crystalline.dividedPowerPolynomialDeRham_tensor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedRing.lean, line 106. The attribute's comment: “ordinary_exactness”.

The divided power Poincaré lemma. For a ring A, a family of variables W and the divided power polynomial algebra P = A⟨x_w : w ∈ W⟩ with its canonical divided powers, the complex

0 → M → M ⊗[A] P → M ⊗[A] Ω¹_{P/A,δ} → M ⊗[A] Ω²_{P/A,δ} → ⋯

is exact at every term after the first, for every A-module M. Injectivity of the first map is Crystalline.dividedPowerPolynomialDeRham_tensor_augmentation_injective.

public theorem dividedPowerPolynomialDeRham_tensor_exact
    (A : Type u) [CommRing A] (W : Type w)
    (M : Type v) [AddCommGroup M] [Module A M] (n : ℕ) :
    Function.Exact
      ((augmentedDividedPowerDeRhamDifferential A W n).hom.lTensor M)
      ((augmentedDividedPowerDeRhamDifferential A W (n + 1)).hom.lTensor M)

Crystalline.CompletedPoincare.exists_continuousDividedPowers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedRing.lean, line 698. The attribute's comment: “completed_exactness”.

The canonical divided powers of P admit a continuous extension to the closure of its augmentation ideal in D.

public theorem exists_continuousDividedPowers :
    Nonempty (ContinuousDividedPowers p A W)

Crystalline.CompletedPoincare.continuousDividedPowers_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/DividedPowerPoincare/CompletedRing.lean, line 739. The attribute's comment: “completed_exactness”.

The continuous extension of the canonical divided powers is unique.

public theorem continuousDividedPowers_unique
    (δ ε : ContinuousDividedPowers p A W) : δ = ε

Tag 07LD, a lemma

Tag 07LD in the Stacks Project.

Crystalline.DividedPowerPolynomial.stacks07LD, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/RelativePoincareModuleQuasiIso.lean, line 710. The attribute's comment: “both clauses: the comparison of de Rham complexes for P = B⟨x_w⟩ on any family of variables is a quasi-isomorphism, for a B-module with integrable connection and, over the p-adic completions D and D', for a D-module with integrable connection”.

[Stacks, Lemma 60.19.2, Tag 07LD].

Let A be a ring, let (B, I, δ) be a divided power ring which is an A-algebra, and let P = B⟨x_w : w ∈ W⟩ be the divided power polynomial ring over B on an arbitrary family W of variables, with divided power ideal J = IP + B⟨x_w⟩₊.

For every B-module M with an integrable connection ∇ : M → M ⊗_B Ω¹_{B/A,δ}, the map of de Rham complexes M ⊗_B Ω^*_{B/A,δ} ⟶ M ⊗_P Ω^*_{P/A,δ} is a quasi-isomorphism (Crystalline.DividedPowerPolynomial.quasiIso_polyDeRhamComparison).

Let D, resp. D', be the p-adic completion of B, resp. P, and Ω̂^i_D, resp. Ω̂^i_{D'}, the p-adic completion of Ω^i_{B/A,δ}, resp. Ω^i_{P/A,δ}. For every D-module M with an integrable connection ∇ : M → M ⊗̂_D Ω̂¹_D (the composite M → M ⊗̂_D Ω̂¹_D → M ⊗̂_D Ω̂²_D vanishes), the map of de Rham complexes M ⊗̂_D Ω̂^*_D ⟶ M ⊗̂_D Ω̂^*_{D'} is a quasi-isomorphism (Crystalline.DividedPowerPolynomial.quasiIso_completedDeRhamComparison).

The second clause holds without the source's hypothesis that M is p-adically complete, so it is not made. The variables, and the ring A, live in the universe of B.

public theorem stacks07LD (A : Type u) [CommRing A] (B : DividedPowerRing.{u}) [Algebra A B]
    (W : Type u) :
    (∀ (M : Type w) [AddCommGroup M] [Module (B : Type u) M]
        (nabla : Connection A (B : Type u) (oneVariableBaseProjection A B) M)
        (hint : Connection.IsIntegrable (oneVariableBaseSource A B)
          (oneVariableBaseProjection A B) (Submodule.mkQ_surjective _)
          (oneVariableBaseGenerationHypothesis A B) nabla),
        QuasiIso (polyDeRhamComparison A B W nabla hint)) ∧
      ∀ (p : ℕ) (M : Type w) [AddCommGroup M]
        [Module (completedDividedPowerRing p (B := (B : Type u))) M]
        (nabla : CompletedConnection p (completedDividedPowerRing p (B := (B : Type u)))
          (completedDividedPowerForms p A B.dividedPowers 1)
          (completedFormsDifferential p A B.dividedPowers) M)
        (hint : CompletedDeRham.HasIntegrableConnection p
          (completedDividedPowerRing p (B := (B : Type u)))
          (completedDividedPowerForms p A B.dividedPowers)
          (completedDividedPowerWedge p A B.dividedPowers)
          (completedDividedPowerDeRham p A B.dividedPowers) M nabla
          (isGradedLeibniz_completedDividedPower p A B.dividedPowers)),
        QuasiIso (completedDeRhamComparison A B W p M nabla hint)

Sources

LeanCrystalline.CompletedPoincare.completedDeRham_tensor_augmentation_injective · Crystalline.CompletedPoincare.completedDeRham_tensor_exact_augmentation · Crystalline.CompletedPoincare.completedDeRham_tensor_exact · Crystalline.dividedPowerPolynomialDeRham_tensor_augmentation_injective · Crystalline.dividedPowerPolynomialDeRham_tensor_exact · Crystalline.CompletedPoincare.exists_continuousDividedPowers · Crystalline.CompletedPoincare.continuousDividedPowers_unique · Crystalline.DividedPowerPolynomial.stacks07LD

Section60.21 Cohomology in the affine case #

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

Tag 07JN, a proposition

Tag 07JN in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.wholeSpaceSystemDerivedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/WholeSpaceSystemDerived.lean, line 226. The attribute's comment: “the complex M(0) → M(1) → M(2) → ⋯ of the system (X, T(n)_e, δ(n)) computes RΓ(Cris(X/S), F): an isomorphism M(•) ≅ RΓ(Cris(X/S), F) in D⁺(Ab), the Čech comparison through an injective resolution, for F locally quasi-coherent with c_f locally surjective along closed immersions, X and S affine”.

[Stacks, Proposition 60.20.1, Tag 07JN]: the complex M(0) → M(1) → M(2) → ⋯ computes RΓ(Cris(X/S), F), as an isomorphism in the bounded below derived category D⁺(Ab):

M(•) ≅ RΓ(Cris(X/S), F),

for a sheaf F of 𝒪_{X/S}-modules on Cris(X/S), over an affine situation (X and S affine, p nilpotent on Γ(X, ⊤)), satisfying the two hypotheses of the tag:

F is locally quasi-coherent, and

for every morphism of Cris(X/S) whose map of ambient schemes is a closed immersion, the comparison map c_f is locally surjective.

Here M(n) = lim_e Γ((X, T(n)_e, δ(n)), F) for the system (X, T(n)_e, δ(n)) of the proof (...SmallSite.wholeSpaceSystem, built from the presentation of the ...SmallSite.WholeSpacePresentation instance), the complex being extended by zero to ℤ, and RΓ(Cris(X/S), -) is ...SmallSite.derivedGlobalSections, the right derived functor of global sections. The isomorphism is the canonical comparison of the proof: the Čech zigzag M(•) ⟶ Tot(lim_e I^•(T(•)_e)) ⟵ Γ(Cris(X/S), I^•) through the Čech double complex of an injective resolution I^• of F (...SmallSite.wholeSpaceSystemDerivedIsoOfAbelian_hom). Hypothesis (1) gives the vanishing of [Stacks, Tag 07JJ] at the objects of the system, and (1) and (2) the surjectivity of the restrictions along its towers; these are what make both arrows of the zigzag quasi-isomorphisms.

def wholeSpaceSystemDerivedIso :
    DerivedCategory.Plus.Q.obj
        (Stacks.Cohomology.extendPlusObj
          (sectionsComplex (wholeSpaceSystem S hp) (abelianSheaf F).obj)) ≅
      (derivedGlobalSections S).obj (abelianSheaf F)

Tag 07LF, a lemma

Tag 07LF in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.vanishing07LF, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/LevelFormsCosimplicialIso.lean, line 390. The attribute's comment: “the vanishing of the cohomology of F ⊗ Ω^i for i > 0, X and S affine”.

[Stacks, Lemma 60.19.3, Tag 07LF]. Let (p, (S, I, γ), X) be a global crystalline situation with X and S affine, and let F be a sheaf of 𝒪_{X/S}-modules on the small crystalline site which is locally quasi-coherent and whose comparison morphisms along closed immersions are surjective — the two hypotheses of [Stacks, Tag 07JN]. Then

H^j(Cris(X/S), F ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0 for every i > 0 and every j ≥ 0.

The proof is the source's own. ...SmallSite.vanishing07LF_of_levelCosimplicialSectionsIso reduces the statement to the existence, at every p-adic level e, of a cosimplicial D(*)-module L_* and an isomorphism M(•)_e ≅ L_* ⊗_{D(*)} ⋀^i Ω_{D(*)} of cosimplicial abelian groups with the tensor product uncompleted; L_* is ...SmallSite.levelSectionsCosimplicialModule and the isomorphism is ...SmallSite.levelCosimplicialSectionsFormsIso.

theorem vanishing07LF (S : GlobalCrystallineSituation.{u}) : Vanishing07LF S

Tag 07LG, a proposition

Tag 07LG in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crystalPairDeRhamComplex_computesCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalDeRhamComputesCohomology.lean, line 90. The attribute's comment: “for any surjective polynomial presentation g : A[x_i : i ∈ ι] → C, supplied as the WholeSpacePresentation instance (the default instance is the tautological one): the complex M ⊗^∧_D Ω*_D of the pair (M, ∇) of a crystal in quasi-coherent modules computes RΓ(Cris(X/S), F): its cohomology in every degree j is H^j(Cris(X/S), F)”.

[Stacks, Proposition 60.21.3, Tag 07LG]: in the situation of [Stacks, Proposition 60.20.1, Tag 07JN] (X and S affine, p nilpotent on X, and D the completed envelope of any surjective polynomial presentation A[x_i : i ∈ ι] → C, supplied as the instance ...SmallSite.WholeSpacePresentation S hp, by default the tautological one), let ℱ be a crystal in quasi-coherent 𝒪_{X/S}-modules and (M, ∇) the module with connection over D corresponding to it under [Stacks, Lemma 60.17.3, Tag 07JG] (...SmallSite.crystalPairFunctor). Then the complex M ⊗^∧_D Ω^*_D (...SmallSite.crystalPairDeRhamComplex) computes RΓ(Cris(X/S), ℱ): for every j, H^j(M ⊗^∧_D Ω^*_D) ≅ H^j(Cris(X/S), ℱ) (...SmallSite.crystalPairDeRhamCohomologyIso).

theorem crystalPairDeRhamComplex_computesCohomology :
    ∀ j : ℕ, Nonempty (AddCommGrpCat.uliftFunctor.{u + 1, u}.obj
        ((crystalPairDeRhamComplex hp Fc).homology j) ≅
      (cohomologyFunctor S j).obj (abelianSheaf Fc.obj))

Tag 07LH, a lemma

Tag 07LH in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crystalRetractPair_computesCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrystalRetractPairCohomology07LH.lean, line 456. The attribute's comment: “in 07L5's reading: for A -> P' smooth and P' -> C surjective, D' the p-adically completed divided power envelope, the data A[x_i] ->> P' -> C of 07L5 presenting the system, a retract a : D -> D', b : D' -> D of 07L5 compatible with the augmentations, and (M', nabla') the pair over D' of 07L5 corresponding to F (crystalRetractPairFunctor), the complex M' ⊗^∧_{D'} Ω*_{D'} (crystalRetractConnModule: module M', connection nabla' read in the completed one-forms of the envelope of P') computes RΓ(Cris(X/S), F): its cohomology in every degree j is H^j(Cris(X/S), F)”.

[Stacks, Lemma 60.21.4, Tag 07LH], for the pair of [Stacks, Lemma 60.17.5, Tag 07L5]: in the situation of [Stacks, Proposition 60.21.3, Tag 07LG] (X and S affine, p nilpotent on X), let ℱ be a crystal in quasi-coherent 𝒪_{X/S}-modules, A → P' → C ring maps with A → P' smooth and P' → C surjective, D' the p-adic completion of D_{P', γ}(J'), P = A[x_i] → P' → C the data of [Stacks, Tag 07L5] (q : P ↠ P', the composite being the presentation of the system), a : D → D', b : D' → D a retract of [Stacks, Tag 07L5] compatible with the augmentations, and (M', ∇') = (crystalRetractPairFunctor hp D' a b ha hb hab hρ).obj ℱ the pair over D' corresponding to ℱ (the base change along a of the pair of [Stacks, Tag 07JG]). Then the complex M' ⊗^∧_{D'} Ω^*_{D'} computes RΓ(Cris(X/S), ℱ): the module with connection ...SmallSite.crystalRetractConnModule has module M' (...SmallSite.crystalRetractConnModule_carrier) and connection ∇' read in the completed one-forms Ω̂¹_{E'/A,δ} (...SmallSite.crystalRetractConnModule_nabla), and the cohomology of its de Rham complex in every degree j is H^j(Cris(X/S), ℱ). Here D is the completed envelope of the presentation of the system (...SmallSite.WholeSpacePresentation S hp), as in ...SmallSite.exists_presentation_retract_crystalPairEquivalence.

theorem crystalRetractPair_computesCohomology
    [Algebra.Smooth ((affineSituation S hp).A : Type u) P']
    (q : MvPolynomial (wholeSpaceIndex S hp) (affineSituation S hp).A →ₐ[(affineSituation S hp).A]
      P') (hq : Function.Surjective q) (hgq : f'.comp q = wholeSpacePresentation S hp)
    (haug : (completedEnvelopeAugmentation (affineSituation S hp) f' hf').comp a.toRingHom =
      completedEnvelopeAugmentation (affineSituation S hp)
        (tensorPowerPresentation (affineSituation S hp) (wholeSpacePresentation S hp) 0)
        (tensorPowerPresentation_surjective (affineSituation S hp) _
          (wholeSpacePresentation_surjective S hp) 0)) :
    ((crystalRetractConnModule hp Fc f' hf' a ha).carrier =
        ((crystalRetractPairFunctor hp _ a b ha hb hab hρ).obj Fc).carrier) ∧
      (∀ x : (crystalRetractConnModule hp Fc f' hf' a ha).carrier,
        (crystalRetractConnModule hp Fc f' hf' a ha).nabla x =
          AdicCompletion.map (pAdicIdeal (A := (presentationFormsData (affineSituation S hp)
              f').ring) (affineSituation S hp).p)
            (LinearMap.lTensor (crystalRetractConnModule hp Fc f' hf' a ha).carrier
              (retractTargetFormsEquiv hp f' hf').toLinearMap)
            (((crystalRetractPairFunctor hp _ a b ha hb hab hρ).obj Fc).nabla x)) ∧
      ∀ j : ℕ, Nonempty (AddCommGrpCat.uliftFunctor.{u + 1, u}.obj
          ((crystalRetractConnModule hp Fc f' hf' a ha).complex.homology j) ≅
        (cohomologyFunctor S j).obj (abelianSheaf Fc.obj))

Crystalline.GlobalCrystallineSituation.SmallSite.smoothPresentationPair_computesCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/SmoothPresentationCohomology07LH.lean, line 650. The attribute's comment: “for A -> P' smooth and P' -> C surjective, D' the p-adically completed divided power envelope and (M', nabla') the pair over D' corresponding to F (the base change of the pair of 07JG, for any polynomial presentation A[x_i] -> C of the system with a variable (WholeSpacePresentation S hp, by default the tautological one), along any augmentation-compatible divided power map D -> D'), the complex M' ⊗^∧_{D'} Ω*_{D'} computes RΓ(Cris(X/S), F): its cohomology in every degree j is H^j(Cris(X/S), F)”.

[Stacks, Lemma 60.21.4, Tag 07LH]: in the situation of [Stacks, Proposition 60.21.3, Tag 07LG] (X and S affine, p nilpotent on X), let ℱ be a crystal in quasi-coherent 𝒪_{X/S}-modules, A → P' → C ring maps with A → P' smooth and P' → C surjective with kernel J', D' the p-adic completion of D_{P', γ}(J') and (M', ∇') the pair over D' corresponding to ℱ: the base change of the pair (M, ∇) of ℱ along any divided power A-algebra map a : D → D' compatible with the augmentations to C (one exists, Crystalline.exists_smoothPresentationMap). Here D is the completed envelope of the presentation A[x_i : i ∈ ι] → C of the system, any one with a variable (the instance ...SmallSite.WholeSpacePresentation S hp, by default the tautological A[x_c : c ∈ C] → C). Then the complex M' ⊗^∧_{D'} Ω^*_{D'} computes RΓ(Cris(X/S), ℱ): its cohomology in every degree j is H^j(Cris(X/S), ℱ), in the graded sense in which [Stacks, Tag 07LG] is stated (...SmallSite.crystalPairDeRhamComplex_computesCohomology).

theorem smoothPresentationPair_computesCohomology [Nonempty (wholeSpaceIndex S hp)]
    [Algebra.Smooth ((affineSituation S hp).A : Type u) P']
    (haug : (completedEnvelopeAugmentation (affineSituation S hp) f' hf').comp a.toRingHom =
      completedEnvelopeAugmentation (affineSituation S hp)
        (tensorPowerPresentation (affineSituation S hp)
          (wholeSpacePresentation S hp) 0)
        (tensorPowerPresentation_surjective (affineSituation S hp) _
          (wholeSpacePresentation_surjective S hp) 0)) :
    ∀ j : ℕ, Nonempty (AddCommGrpCat.uliftFunctor.{u + 1, u}.obj
        ((smoothPresentationPair hp Fc f' hf' a ha).complex.homology j) ≅
      (cohomologyFunctor S j).obj (abelianSheaf Fc.obj))

Sources

LeanCrystalline.GlobalCrystallineSituation.SmallSite.wholeSpaceSystemDerivedIso · Crystalline.GlobalCrystallineSituation.SmallSite.vanishing07LF · Crystalline.GlobalCrystallineSituation.SmallSite.crystalPairDeRhamComplex_computesCohomology · Crystalline.GlobalCrystallineSituation.SmallSite.crystalRetractPair_computesCohomology · Crystalline.GlobalCrystallineSituation.SmallSite.smoothPresentationPair_computesCohomology

Section60.22 Two counter examples #

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

Tag 07LJ, an example

Tag 07LJ in the Stacks Project.

Crystalline.TorsionExample.completedDifferential_tauForm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCompletedDeRham.lean, line 286. The attribute's comment: “dτ = 0 in Ω_D, the p-adic completion of the divided power differentials of D = D_{P,γ}(J)^∧ over ZZ_p: τ lies in the kernel of the degree zero differential of D → Ω¹_D → Ω²_D → ⋯”.

τ lies in the kernel of the degree zero differential of the complex of [Stacks, Tag 07LG], which is the example's identity dτ = 0 read through Ω^0_D = D.

theorem completedDifferential_tauForm : completedDifferential p 0 (tauForm p) = 0

Crystalline.TorsionExample.frobeniusPullback_tauClass_eq_envelopeMapOfLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCrystallineCohomology.lean, line 583. The attribute's comment: “F^*(τ) = σ(τ): for every lift φ of Frobenius on P = ZZ_p[x, y] over ZZ_p, with σ the map it induces on the divided power envelope, the Frobenius pullback of the class of τ in H^0(Cris(X/S), O_{X/S}) is the class defined by σ(τ)”.

F^*(τ) = σ(τ): for every lift φ of Frobenius on P and the map σ it induces on the divided power envelope, the class F^*(τ) ∈ H⁰(Cris(X/S), 𝒪_{X/S}) is the class defined by σ(τ): on every object (U, T, δ) of Cris(X/S) its value is the image of σ(τ) under a lift E → Γ(T, 𝒪_T) of the coordinates.

theorem frobeniusPullback_tauClass_eq_envelopeMapOfLift
    (φ : polynomial p →ₐ[ℤ_[p]] polynomial p)
    (hφ : ∀ f, φ f - f ^ p ∈ Ideal.span {(p : polynomial p)})
    (A : GlobalCrystallineSituation.CrystallineThickening (situation p)) :
    (cohomologyZeroEquiv p (frobeniusPullback p (tauClass p))).val (op A) =
      toSections (envelopeLift A.obj) (envelopeMapOfLift p φ hφ (envelopeTau p))

Crystalline.TorsionExample.frobeniusPullback_tauClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCrystallineCohomology.lean, line 604. The attribute's comment: “for the lift of Frobenius x ↦ x^p, y ↦ y^p one has F^*(τ) = 0 in H^0(Cris(X/S), O_{X/S})”.

F^*(τ) = 0 for the lift of Frobenius x ↦ x^p, y ↦ y^p: the class F^*(τ) = σ(τ) vanishes, as σ(τ) = γ_p(x^{2p}) γ_p(y^{2p}) − γ_p(x^p y^p)² = 0.

theorem frobeniusPullback_tauClass : frobeniusPullback p (tauClass p) = 0

Crystalline.TorsionExample.tauClass_ne_zero_and_prime_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCrystallineCohomology.lean, line 627. The attribute's comment: “τ defines a nonzero element of H^0(Cris(X/S), O_{X/S}) killed by p, for X = Spec(F_p[x, y]/(x^2, xy, y^2)) and S = Spec(ZZ_p) with the divided power ideal (p)”.

τ defines a nonzero p-torsion element of H⁰(Cris(X/S), 𝒪_{X/S}).

theorem tauClass_ne_zero_and_prime_smul_eq_zero : tauClass p ≠ 0 ∧ p • tauClass p = 0

Crystalline.TorsionExample.exists_ne_zero_prime_smul_eq_zero_cohomologyZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCrystallineCohomology.lean, line 634. The attribute's comment: “conclusion (1): H^0(Cris(X/S), O_{X/S}) has p-torsion, for X = Spec(F_p[x, y]/(x^2, xy, y^2)) and S = Spec(ZZ_p) with the divided power ideal (p)”.

H⁰(Cris(X/S), 𝒪_{X/S}) has p-torsion, for X = Spec(𝐅_p[x, y]/(x², xy, y²)) and S = Spec(ℤ_p) with the divided power ideal (p) and its divided powers.

theorem exists_ne_zero_prime_smul_eq_zero_cohomologyZero :
    ∃ a : cohomologyZero p, a ≠ 0 ∧ p • a = 0

Crystalline.TorsionExample.not_injective_frobeniusPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionCrystallineCohomology.lean, line 644. The attribute's comment: “conclusion (2): pulling back by Frobenius F^* : H^0(Cris(X/S), O_{X/S}) → H^0(Cris(X/S), O_{X/S}) is not injective, for X = Spec(F_p[x, y]/(x^2, xy, y^2)) and S = Spec(ZZ_p) with the divided power ideal (p)”.

Pulling back by Frobenius F^* : H⁰(Cris(X/S), 𝒪_{X/S}) → H⁰(Cris(X/S), 𝒪_{X/S}) is not injective, for X = Spec(𝐅_p[x, y]/(x², xy, y²)) and S = Spec(ℤ_p) with the divided power ideal (p).

theorem not_injective_frobeniusPullback : ¬ Function.Injective (frobeniusPullback p)

Crystalline.TorsionExample.quotientRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionDegreeZero.lean, line 297. The attribute's comment: “the example's presentation C = P/J: reduction of coefficients ZZ_p[x, y] -> F_p[x, y] induces a ring isomorphism ZZ_p[x, y]/(p, x^2, xy, y^2) = F_p[x, y]/(x^2, xy, y^2), carrying the class of each variable to that variable”.

The presentation of [Stacks, Tag 07LJ]. Coefficient reduction induces a ring isomorphism

P/J = ℤ_[p][x, y]/(p, x², xy, y²) ≅ 𝐅_p[x, y]/(x², xy, y²) = C

carrying the class of x to x and the class of y to y, which is the identification the example writes as C = P/J. Its effect on classes is quotientRingEquiv_mk.

noncomputable def quotientRingEquiv : quotientRing p ≃+* residueQuotient p

Crystalline.TorsionExample.base_dividedPowers_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionDegreeZero.lean, line 331. The attribute's comment: “the example's base: the ideal (p) of ZZ_p has exactly one divided power structure, so gamma is determined”.

The base of [Stacks, Tag 07LJ] is uniquely divided. The divided powers γ on the ideal (p) ⊆ ℤ_[p] are the only ones: ℤ_[p] is torsion free as a ℤ-module, so n! γ_n(a) = aⁿ determines γ_n(a), which is the uniqueness half of [Stacks, Tag 07GM].

theorem base_dividedPowers_unique (γ : DividedPowers (Ideal.span {(p : ℤ_[p])})) :
    γ = PadicInt.dividedPowers p

Crystalline.TorsionExample.prime_mul_tau_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionDegreeZero.lean, line 537. The attribute's comment: “the example's identity p τ = 0 in D, for τ = gammabar_p(x^2) gammabar_p(y^2) - gammabar_p(xy)^2, by the example's own display p! gammabar_p(x^2) gammabar_p(y^2) = x^{2p} gammabar_p(y^2) = gammabar_p(x^2 y^2) = x^p y^p gammabar_p(xy) = p! gammabar_p(xy)^2 together with the invertibility of (p-1)! in D”.

p τ = 0. Multiplying τ by p! gives γ̄_p(x²y²) − γ̄_p((xy)(xy)) = 0, and p! = p (p − 1)! with (p − 1)! invertible.

theorem prime_mul_tau_eq_zero : (p : completedEnvelope p) * tau p = 0

Crystalline.TorsionExample.toWitnessRing_envelopeTau, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionNonvanishing.lean, line 201. The attribute's comment: “the example's computation inside its witness thickening: the divided power morphism D_{P, γ}(J) -> B out of the universal property of the envelope sends γ_p(x^2) γ_p(y^2) - γ_p(xy)^2 to uv, which is nonzero in B (u_mul_v_ne_zero of RingTheory.DividedPowers.TorsionWitnessRing), at every prime p”.

The computation of [Stacks, Tag 07LJ]. The element γ_p(x²) γ_p(y²) − γ_p(xy)² of the divided power envelope has image u v in the witness thickening B.

theorem toWitnessRing_envelopeTau :
    (toWitnessRing p).toRingHom (envelopeTau p) = u p * v p

Crystalline.TorsionExample.tau_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/TorsionNonvanishing.lean, line 225. The attribute's comment: “the example's claim that τ ≠ 0 in D, at every prime p, by the source's own witness thickening B = F_p[x, y, u, v]/(x^3, x^2 y, x y^2, y^3, xu, yu, xv, yv, u^2, v^2) with the divided powers of DividedPowers.TorsionWitness on K = ker(B -> C), which send x^2 to u and y^2 to v, in which τ maps to uv ≠ 0, so that the first level of the p-adic completion already sees τ”.

τ ≠ 0 in D, the last claim of [Stacks, Tag 07LJ] about τ.

Were τ zero, its first level in the p-adic completion would vanish, so the envelope-level element envelopeTau would be a multiple of p. Its image in the witness thickening B would then be zero, p being zero in B; but that image is u v ≠ 0.

theorem tau_ne_zero : tau p ≠ 0

Tag 07LK, an example

Tag 07LK in the Stacks Project.

Crystalline.AffineSpaceCrystallineSetup.crisCohomologyIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 121. The attribute's comment: “RΓ(Cris(X/S), O_{X/S}) is represented by the complex D -> Omega^1_D -> ... -> Omega^r_D, D = Z_p[x_1, ..., x_r]^wedge, degreewise: H^j(Cris(X/S), O_{X/S}) is the j-th cohomology of that complex for every j, by 07LG/07LH for the presentation C = P/pP”.

RΓ(Cris(X/S), 𝒪_{X/S}) is represented by the complex D → Ω¹_D → Ω²_D → ⋯ → Ω^r_D, for X = Spec(𝐅_p[x_1, …, x_r]) over S = Spec(𝐙_p, (p), γ) and D = P^∧, P = 𝐙_p[x_1, …, x_r]: in every degree j, H^j(Cris(X/S), 𝒪_{X/S}) is the j-th cohomology of the completed divided power de Rham complex of D (Crystalline.AffineSpaceCrystallineSetup.deRhamComplexNat, whose terms vanish above r).

This is [Stacks, Lemma 60.21.4, Tag 07LH] (...SmallSite.smoothPresentationPair_computesCohomology) for the crystal 𝒪_{X/S} and the example's presentation P → Γ(X, 𝒪_X), which is smooth with kernel pP (Crystalline.AffineSpaceCrystallineSetup.presentation), through any divided power map of envelopes compatible with the augmentations (Crystalline.exists_smoothPresentationMap): the pair of 𝒪_{X/S} is (D, d) (structureModulePairHom), its base change to the completed envelope of P → P/pP is the structure module of that envelope (Crystalline.FormsData.baseChangeUnitHom), and the envelope of P → P/pP is P, pP having divided powers by [Stacks, Tag 07H1] (Crystalline.AffineSpaceCrystallineSetup.envelopeEquiv), so that the complex is the example's (Crystalline.AffineSpaceCrystallineSetup.unitBaseChangeComplexIso).

theorem crisCohomologyIso (j : ℕ) :
    Nonempty (T.crisCohomology j ≅
      AddCommGrpCat.uliftFunctor.{1, 0}.obj (T.deRhamComplexNat.homology j))

Crystalline.AffineSpaceCrystallineSetup.isZero_crisCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 173. The attribute's comment: “conclusion (1): H^j(Cris(X/S), O_{X/S}) = 0 for j > r, X = A^r_{F_p}, S = Spec(Z_p)”.

Conclusion (1) of [Stacks, Tag 07LK]: the crystalline cohomology of the crystalline structure sheaf of X = 𝐀^r_{𝐅_p} over S = Spec(𝐙_p) is zero except in degrees 0, …, r. Cohomology is indexed by ℕ, so this is the vanishing above r; it holds for every r (the source states its conclusions under r > 0). The term Ω^i_D of the complex itself vanishes for i > r.

theorem isZero_crisCohomology {j : ℕ} (hj : T.r < j) : IsZero (T.crisCohomology j)

Crystalline.AffineSpaceCrystallineSetup.crisCohomologyZeroIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 185. The attribute's comment: “conclusion (2): H^0(Cris(X/S), O_{X/S}) = Z_p”.

Conclusion (2) of [Stacks, Tag 07LK]: H⁰(Cris(X/S), 𝒪_{X/S}) = 𝐙_p, for every r (the source states its conclusions under r > 0): the kernel of d : D → Ω¹_D consists of the constants, an element of 𝐙_p[x_1, …, x_r]^∧ all of whose partial derivatives vanish being a constant. The universe lift is the one H^j(Cris(X/S), -) is valued in.

theorem crisCohomologyZeroIso :
    Nonempty (T.crisCohomology 0 ≅ AddCommGrpCat.of (ULift.{1, 0} T.A))

Crystalline.AffineSpaceCrystallineSetup.infinite_and_not_isAddTorsion_crisCohomology_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 199. The attribute's comment: “conclusion (3): for r > 0, H^r(Cris(X/S), O_{X/S}) is infinite and is not a torsion abelian group”.

Conclusion (3) of [Stacks, Tag 07LK]: for r > 0 the cohomology group H^r(Cris(X/S), 𝒪_{X/S}) is infinite and is not a torsion abelian group.

theorem infinite_and_not_isAddTorsion_crisCohomology_top (hr : 0 < T.r) :
    Infinite (T.crisCohomology T.r) ∧ ¬ IsAddTorsion (T.crisCohomology T.r)

Crystalline.AffineSpaceCrystallineSetup.not_isHausdorff_crisCohomology_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 214. The attribute's comment: “conclusion (4): for r > 0, H^r(Cris(X/S), O_{X/S}) is not separated for the p-adic topology”.

Conclusion (4) of [Stacks, Tag 07LK]: for r > 0 the cohomology group H^r(Cris(X/S), 𝒪_{X/S}) is not separated for the p-adic topology.

theorem not_isHausdorff_crisCohomology_top (hr : 0 < T.r) :
    ¬ IsHausdorff (Ideal.span {(T.p : ℤ)}) (T.crisCohomology T.r)

Crystalline.AffineSpaceCrystallineSetup.exists_padicInt_crisCohomology_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Examples/AffineSpaceCrystallineCohomology.lean, line 236. The attribute's comment: “closing remark on eta, the quoted 'generates a copy of Q_p' in the sense its argument shows: for r > 0 an injective Z_p -> H^r(Cris(X/S), O_{X/S}) through the class of eta, with [eta] in p^t H^r for every t, and no additive Q_p -> H^r extending it”.

The closing remark of [Stacks, Tag 07LK] on η, in the sense its argument shows. For r > 0 the class of η = ∑_{e > 0} p^e x_1^{p^e - 1} ⋯ x_r^{p^e - 1} dx_1 ∧ ⋯ ∧ dx_r in H^r(Cris(X/S), 𝒪_{X/S}) generates a copy of 𝐙_p (no nonzero 𝐙_p-multiple of η, in particular no p^N η, is exact), and it is divisible by every power of p; but no additive map 𝐐_p → H^r(Cris(X/S), 𝒪_{X/S}) sends 1 to it. The source says that η "generates" a copy of 𝐐_p, in quotation marks, and this theorem formalizes that remark in the sense its argument shows: an injective 𝐙_p → H^r through [η], with [η] ∈ ⋂_t p^t H^r. The third clause records that the quotation marks are needed: there is no additive 𝐐_p → H^r extending it, because the elements x with p x = [η] cannot themselves be divisible by every power of p (Crystalline.AffineSpaceCrystallineSetup.not_exists_pow_smul_eq_etaTop).

theorem exists_padicInt_crisCohomology_top (hr : 0 < T.r) :
    ∃ f : ℤ_[T.p] →+ T.crisCohomology T.r, Function.Injective f ∧
      (∀ t : ℕ, ∃ y, f 1 = (T.p ^ t) • y) ∧
      ¬ ∃ g : ℚ_[T.p] →+ T.crisCohomology T.r, g 1 = f 1

Sources

Section60.23 Applications #

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

Tag 07LM, a proposition

Tag 07LM in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.stacks07LM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Proposition07LM.lean, line 99. The attribute's comment: “the whole proposition: for F a crystal in quasi-coherent O_{X/S}-modules on Cris(X/S), Ru_{X/S,} carries the truncation map (F → F ⊗ Ω¹ → F ⊗ Ω² → ⋯) ⟶ F[0] to an isomorphism of D⁺(Ab(X_Zar)), the differentials of the complex being the extensions of the canonical connection of F of 07J6; and Ru_{X/S,}(F ⊗_{O_{X/S}} Ω^i_{X/S}) = 0 for every i > 0”.

Let F be a crystal in quasi-coherent 𝒪_{X/S}-modules on Cris(X/S). The truncation map of complexes

(F → F ⊗_{𝒪_{X/S}} Ω¹_{X/S} → F ⊗_{𝒪_{X/S}} Ω²_{X/S} → ⋯) ⟶ F[0]

becomes a quasi-isomorphism after applying Ru_{X/S, *} — it is carried to an isomorphism of D⁺(Ab(X_{Zar})) — and in fact Ru_{X/S, *}(F ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0 for every i > 0.

The complex is (crystalDeRhamSheafData hF).complex: its terms are the sheaves F ⊗_{𝒪_{X/S}} Ω^i_{X/S} and its differentials crystalDeRhamDifferential hF i are the extensions m ⊗ ω ↦ ∇(m) ∧ ω + m ⊗ d ω of the canonical connection ∇(m) = p₁^* m - p₀^* m of [Stacks, Tag 07J6].

theorem stacks07LM (F : SheafOfModules.{u} (structureSheaf S)) (hF : F.IsQuasicoherentOnSite) :
    IsIso ((derivedZariskiDirectImageFunctor S).map
        (DerivedCategory.Plus.Qh.map
          ((HomotopyCategory.Plus.quotient _).map
            (sheafPlusTruncation S (crystalDeRhamSheafData hF).complex
              (CrystalDeRhamSheafData.singleComplex (F := F))
              (crystalDeRhamSheafData hF).truncation)))) ∧
      ∀ i : ℕ, 0 < i →
        IsZero ((derivedZariskiDirectImage S).obj (tensorDifferentialFormsSheaf F i))

Tag 07LN, a remark

Tag 07LN in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crysFormsSheaf_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Remark07LN.lean, line 99. The attribute's comment: “the sheaves Ω^j_{X/S}, every j: Ω^j_{X/S} satisfies conditions (1) and (2) of 07JN, hence Ru_{X/S,*}(Ω^j_{X/S} ⊗ Ω^i_{X/S}) = 0 for every i > 0”.

Stacks Project, Remark 60.23.2, Tag 07LN, for the sheaves Ω^j_{X/S}. For every j, the sheaf of 𝒪_{X/S}-modules Ω^j_{X/S} on Cris(X/S) — crysFormsSheaf S j, the sheaf associated with the presheaf Ω^j_{X/S} = ⋀^j Ω_{X/S} (toCrysFormsSheaf is locally bijective, isLocallyInjective_toCrysFormsSheaf and isLocallySurjective_toCrysFormsSheaf) — satisfies conditions (1) and (2) of [Stacks, Tag 07JN], and therefore, for every i > 0,

Ru_{X/S, *}(Ω^j_{X/S} ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0.

Condition (1) is isLocallyQuasiCoherent_crysFormsSheaf: the restriction of Ω^j_{X/S} to the ambient scheme T of an object is the sheaf associated with the restriction of the presheaf, that is Ω^j_{T/S, δ} ([Stacks, Tag 07IZ]), which is quasi-coherent ([Stacks, Tag 07IY]). Condition (2) is isSurjectiveComparison_crysFormsSheaf: the comparison maps of the presheaf Ω^j_{X/S} are locally surjective ([Stacks, Tag 07KM]), and so are those of its sheaf. The vanishing is then isZero_derivedZariskiDirectImage_of_vanishingHypotheses.

theorem crysFormsSheaf_vanishing (j : ℕ) :
    IsLocallyQuasiCoherent (crysFormsSheaf S j) ∧
      CohomologyRestriction.IsSurjectiveComparison (crysFormsSheaf S j).val ∧
      ∀ i : ℕ, 0 < i →
        IsZero ((derivedZariskiDirectImage S).obj
          (tensorDifferentialFormsSheaf (crysFormsSheaf S j) i))

Crystalline.GlobalCrystallineSituation.SmallSite.underlineModules_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Remark07LN.lean, line 126. The attribute's comment: “the sheaves F-underline: for F a quasi-coherent O_X-module, F-underline satisfies conditions (1) and (2) of 07JN, hence Ru_{X/S,*}(F-underline ⊗ Ω^i_{X/S}) = 0 for every i > 0”.

Stacks Project, Remark 60.23.2, Tag 07LN, for the sheaves F̲. Let F be a quasi-coherent 𝒪_X-module and F̲ the sheaf of 𝒪_{X/S}-modules on Cris(X/S) with F̲(U, T, δ) = F(U). Then F̲ satisfies conditions (1) and (2) of [Stacks, Tag 07JN] — it is locally quasi-coherent, and its comparison morphisms c_f along the morphisms of Cris(X/S) whose map on ambient schemes is a closed immersion are surjective — and therefore, for every i > 0,

Ru_{X/S, *}(F̲ ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0.

Condition (1) is isLocallyQuasiCoherent_underlineModules: the restriction of F̲ to the ambient scheme T of (U, T, δ) is the direct image of F|_U along the closed immersion U ↪ T. Condition (2) is isSurjectiveComparison_underlineModules. The vanishing is then isZero_derivedZariskiDirectImage_of_vanishingHypotheses.

theorem underlineModules_vanishing (F : S.X.Modules) [F.IsQuasicoherent] :
    IsLocallyQuasiCoherent (underlineModules S F) ∧
      CohomologyRestriction.IsSurjectiveComparison (underlineModules S F).val ∧
      ∀ i : ℕ, 0 < i →
        IsZero ((derivedZariskiDirectImage S).obj
          (tensorDifferentialFormsSheaf (underlineModules S F) i))

Crystalline.GlobalCrystallineSituation.SmallSite.underlineStructure_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Remark07LN.lean, line 158. The attribute's comment: “the sheaf O_X-underline = G_a-underline: it satisfies conditions (1) and (2) of 07JN, hence Ru_{X/S,*}(O_X-underline ⊗ Ω^i_{X/S}) = 0 for every i > 0”.

Stacks Project, Remark 60.23.2, Tag 07LN, for 𝒪_X̲ = G_a̲. The sheaf 𝒪_X̲ of 𝒪_{X/S}-modules on Cris(X/S), whose sections over (U, T, δ) are Γ(U, 𝒪_U) — the sheaf G_a̲, underlineModules_unit_presheaf — satisfies conditions (1) and (2) of [Stacks, Tag 07JN], and for every i > 0

Ru_{X/S, *}(𝒪_X̲ ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0.

This is underlineModules_vanishing at the quasi-coherent module 𝒪_X.

theorem underlineStructure_vanishing :
    IsLocallyQuasiCoherent (underlineModules S (SheafOfModules.unit S.X.ringCatSheaf)) ∧
      CohomologyRestriction.IsSurjectiveComparison
        (underlineModules S (SheafOfModules.unit S.X.ringCatSheaf)).val ∧
      ∀ i : ℕ, 0 < i →
        IsZero ((derivedZariskiDirectImage S).obj
          (tensorDifferentialFormsSheaf (underlineModules S (SheafOfModules.unit S.X.ringCatSheaf))
            i))

Crystalline.GlobalCrystallineSituation.SmallSite.isZero_derivedZariskiDirectImage_of_vanishingHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Vanishing07LMProof.lean, line 152. The attribute's comment: “the remark's conclusion itself: Ru_{X/S,*}(F ⊗ Ω^i_{X/S}) = 0 for every i > 0 and EVERY sheaf of O_{X/S}-modules F satisfying conditions (1) local quasi-coherence and (2) local surjectivity of the comparison map c_f along a closed immersion, of 07JN -- which is the generality the remark gives the vanishing clause of 07LM, weaker than being a crystal. The proof is the source's: 072W for u_{X/S} reduces to an affine open of X over an affine open of S, 07KL identifies the sections functors there with the cohomology of Cris(V/S|_W), the coefficients transport along that restriction together with the two conditions, and 07LF kills the cohomology”.

Stacks Project, Remark 60.23.2, Tag 07LN. For any sheaf of 𝒪_{X/S}-modules F on the small crystalline site satisfying conditions (1) and (2) of [Stacks, Proposition 60.19.1, Tag 07JN] — F is locally quasi-coherent, and for every morphism of Cris(X/S) whose map on ambient schemes is a closed immersion the comparison morphism c_f : f^*F_{T'} ⟶ F_T is surjective — and for every i > 0,

Ru_{X/S, *}(F ⊗_{𝒪_{X/S}} Ω^i_{X/S}) = 0.

This is the conclusion the remark observes holds at that generality rather than only for a crystal, the proof of [Stacks, Proposition 60.23.1, Tag 07LM] using nothing else about F. It is the source's own argument: the local-to-global criterion [Stacks, Tag 072W] for u_{X/S} reduces it to an affine open V of X mapping into an affine open W of S, over such an open the right derived functors of ℋ ↦ Γ(V, u_{X/S, *}ℋ) are the cohomology of Cris(V/S|_W) by [Stacks, Tag 07KL], the coefficient sheaf transports to the restricted situation together with conditions (1) and (2), and [Stacks, Tag 07LF] kills that cohomology in every degree.

theorem isZero_derivedZariskiDirectImage_of_vanishingHypotheses
    (F : SheafOfModules.{u} (structureSheaf S)) (hqc : IsLocallyQuasiCoherent F)
    (hsurj : CohomologyRestriction.IsSurjectiveComparison F.val) (i : ℕ) (hi : 0 < i) :
    IsZero ((derivedZariskiDirectImage S).obj (tensorDifferentialFormsSheaf F i))

Tag 07LP, an equation

Tag 07LP in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crystallineToAmbientDeRham, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Equation07LP.lean, line 429. The attribute's comment: “the canonical map RΓ(Cris(X/S), F) ⟶ RΓ(T, F_T ⊗ Ω*_{T/S,δ}) for a crystal in quasi-coherent modules F and an object (U, T, δ), built from 07LM, restriction to T and 07IZ”.

Stacks Project, Equation 07LP. In Situation 07MF, let F be a crystal in quasi-coherent modules on Cris(X/S) and let (U, T, δ) be an object of Cris(X/S). The canonical map

RΓ(Cris(X/S), F) ⟶ RΓ(T, F_T ⊗_{𝒪_T} Ω^*_{T/S,δ})

in D⁺(Ab), constructed as in the source: RΓ(Cris(X/S), F) = RΓ(Cris(X/S), F ⊗ Ω^*_{X/S}) by [Stacks, Tag 07LM] (CrystalDeRhamSheafData.derivedGlobalSectionsIsoDeRham, the inverse of the image of the truncation map, invertible after Ru_{X/S, *} and hence after RΓ(Cris(X/S), -)); then the restriction of global cohomology classes to T (...CrystallineThickening.derivedGlobalSectionsToAmbient); then the identification of the restriction of F ⊗ Ω^*_{X/S} to T with F_T ⊗_{𝒪_T} Ω^*_{T/S,δ} by [Stacks, Tag 07IZ] (restrictCrystalDeRhamComplexIso). truncation_comp_crystallineToAmbientDeRham records that it is this composite. The target is RΓ(T, -) of ambientDeRhamComplex hF A, read as a bounded below complex (CrystalDeRhamSheafData.ambientComplexPlus).

def crystallineToAmbientDeRham :
    (derivedGlobalSections S).obj (abelianSheaf F) ⟶
      (CrystallineThickening.derivedAmbientGlobalSectionsFunctor A).obj
        (DerivedCategory.Plus.Qh.obj ((HomotopyCategory.Plus.quotient _).obj
          ((crystalDeRhamSheafData hF).ambientComplexPlus A)))

Crystalline.GlobalCrystallineSituation.SmallSite.truncation_comp_crystallineToAmbientDeRham, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Equation07LP.lean, line 445. The attribute's comment: “the canonical map is the composite of the source: 07LM, restriction of global cohomology classes to T, and 07IZ”.

The map of [Stacks, Equation 07LP] is the composite of the source. Precomposed with the image under RΓ(Cris(X/S), -) of the truncation map F ⊗ Ω^*_{X/S} ⟶ F[0] of [Stacks, Tag 07LM] — an isomorphism — it is the restriction to T of the global cohomology classes of F ⊗ Ω^*_{X/S}, followed by RΓ(T, -) of the identification (F ⊗ Ω^*_{X/S})_T ≅ F_T ⊗_{𝒪_T} Ω^*_{T/S,δ} of [Stacks, Tag 07IZ].

theorem truncation_comp_crystallineToAmbientDeRham :
    (derivedGlobalSectionsFunctor S).map
        (DerivedCategory.Plus.Qh.map
          ((HomotopyCategory.Plus.quotient _).map
            (sheafPlusTruncation S (crystalDeRhamSheafData hF).complex
              (CrystalDeRhamSheafData.singleComplex (F := F))
              (crystalDeRhamSheafData hF).truncation))) ≫
      (derivedGlobalSectionsFunctor S).map
          (CrystalDeRhamSheafData.singleFunctorIsoSingleComplex (F := F)).inv ≫
        crystallineToAmbientDeRham hF A =
      (CrystallineThickening.derivedGlobalSectionsToAmbient A).app _ ≫
        (CrystallineThickening.derivedAmbientGlobalSectionsFunctor A).map
          ((crystalDeRhamSheafData hF).derivedRestrictComplexIso A).hom

Sources

LeanCrystalline.GlobalCrystallineSituation.SmallSite.stacks07LM · Crystalline.GlobalCrystallineSituation.SmallSite.crysFormsSheaf_vanishing · Crystalline.GlobalCrystallineSituation.SmallSite.underlineModules_vanishing · Crystalline.GlobalCrystallineSituation.SmallSite.underlineStructure_vanishing · Crystalline.GlobalCrystallineSituation.SmallSite.isZero_derivedZariskiDirectImage_of_vanishingHypotheses · Crystalline.GlobalCrystallineSituation.SmallSite.crystallineToAmbientDeRham · Crystalline.GlobalCrystallineSituation.SmallSite.truncation_comp_crystallineToAmbientDeRham

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

60.13 Two universal thickenings to 60.23 Applications

Section60.13 Two universal thickenings#

Tag 07J2, a remark

Tag 07J3, a remark

Sources

Section60.14 The de Rham complex#

Tag 07J4, the section

Sources

Section60.15 Connections#

Tag 07J6, a lemma

Sources

Section60.16 Cosimplicial algebra#

Tag 07KQ, a lemma

Tag 07KT, an item

Sources

Section60.17 Crystals in quasi-coherent modules#

Tag 07J8, an equation

Tag 07J9, an equation

Tag 07JA, an equation

Tag 07JF, an equation

Tag 07L0, an equation

Tag 07L1, an equation

Tag 07L2, a lemma

Tag 07L3, an equation

Tag 07L4, a lemma

Tag 07JB, an item

Tag 07JC, an item

Tag 07JD, an item

Tag 07JE, an item

Tag 07JG, a lemma

Tag 07JH, a proposition

Tag 07L5, a lemma

Tag 07L6, a remark

Sources

Section60.18 General remarks on cohomology#

Tag 07JJ, a lemma

Tag 07JK, a lemma

Tag 07JL, a lemma

Tag 07JM, a lemma

Sources

Section60.19 Cosimplicial preparations#

Tag 07L7, an example

Tag 07L9, a lemma

Tag 07LA, a lemma

Sources

Section60.20 Divided power Poincaré lemma#

Tag 07LC, a lemma

Tag 07LD, a lemma

Sources

Section60.21 Cohomology in the affine case#

Tag 07JN, a proposition

Tag 07LF, a lemma

Tag 07LG, a proposition

Tag 07LH, a lemma

Sources

Section60.22 Two counter examples#

Tag 07LJ, an example

Tag 07LK, an example

Sources

Section60.23 Applications#

Tag 07LM, a proposition

Tag 07LN, a remark

Tag 07LP, an equation

Sources

Section60.13 Two universal thickenings #

Section60.14 The de Rham complex #

Section60.15 Connections #

Section60.16 Cosimplicial algebra #

Section60.17 Crystals in quasi-coherent modules #

Section60.18 General remarks on cohomology #

Section60.19 Cosimplicial preparations #

Section60.20 Divided power Poincaré lemma #

Section60.21 Cohomology in the affine case #

Section60.22 Two counter examples #

Section60.23 Applications #