60.24 Some further results to 60.26 Frobenius action on…

Section60.24 Some further results#

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

Tag 07MJ, a remark

Tag 07MJ in the Stacks Project.

Crystalline.GlobalCrystallineSituation.pullbackToClosedFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 187. The attribute's comment: “the induced morphism U ⟶ T₀, for T = S ×_{S'} T' and U = X ×_{X'} U'”.

Stacks Project, Tag 07MJ. The induced morphism U ⟶ T₀ of the remark: the closed fibre of T = S ×_{S'} T' is S₀ ×_{S'₀} T'₀ by [Stacks, Tag 07ME], and U = X ×_{X'} U' maps to S₀ through X and to T'₀ = U' through U'.

def pullbackToClosedFiber : pullbackSource S S' fX A' ⟶ closedFiber (pullbackBase S S' fS A')

Crystalline.GlobalCrystallineSituation.pullbackSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 219. The attribute's comment: “the crystalline situation U/T attached to an object (U', T', δ') of Cris(X'/S')”.

Stacks Project, Tag 07MJ. The crystalline situation U/T of the remark attached to an object (U', T', δ') of Cris(X'/S'): the divided power base is the fibre product T = S ×_{S'} T' of [Stacks, Tag 07ME], the scheme is U = X ×_{X'} U', and the structure morphism to T₀ is pullbackToClosedFiber. The prime p is locally nilpotent on U because it is on X and U ⟶ X induces maps on local rings.

def pullbackSituation : GlobalCrystallineSituation.{u}

Crystalline.GlobalCrystallineSituation.isOpenImmersion_pullbackSituationToX, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 262. The attribute's comment: “U = X ×_{X'} U' is an open subscheme of X”.

Stacks Project, Tag 07MJ. U = X ×_{X'} U' is an open subscheme of X, the morphism U' ⟶ X' of an object of the small crystalline site being an open immersion.

theorem isOpenImmersion_pullbackSituationToX :
    IsOpenImmersion (pullback.fst fX A'.obj.toX)

Crystalline.GlobalCrystallineSituation.range_pullbackSituationToX, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 270. The attribute's comment: “U = X ×_{X'} U' is f⁻¹(U')”.

Stacks Project, Tag 07MJ. The open subscheme U = X ×_{X'} U' of X is f⁻¹(U'): its image in X is the preimage under f of the image of U' in X'.

theorem range_pullbackSituationToX :
    Set.range (pullback.fst fX A'.obj.toX) = fX ⁻¹' Set.range A'.obj.toX

Crystalline.GlobalCrystallineSituation.pullbackCrisMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 287. The attribute's comment: “the morphism (U/T)_cris ⟶ (X/S)_cris”.

The morphism of small crystalline topoi (U/T)_cris ⟶ (X/S)_cris induced by U ⟶ X over T ⟶ S, [Stacks, Tag 07IK]. It is unconditional, left exactness of i_! for X/S being Crystalline.GlobalCrystallineSituation.CrystallineThickening.preservesFiniteLimits_lowerShriek.

def pullbackCrisMorphism :
    MorphismOfTopoi (smallTopos (pullbackSituation S S' fS fX hf A')) (smallTopos S)

Crystalline.GlobalCrystallineSituation.pullbackStructureToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 308. The attribute's comment: “the structure morphism τ_{U/T} : (U/T)_cris ⟶ Sh(T_Zar)”.

Stacks Project, Tag 07MJ. The structure morphism τ_{U/T} : (U/T)_cris ⟶ Sh(T_Zar) of the remark.

def pullbackStructureToposMorphism :
    MorphismOfTopoi (smallTopos (pullbackSituation S S' fS fX hf A'))
      (Sheaf (Opens.grothendieckTopology (pullbackBase S S' fS A').scheme.carrier)
        (Type (u + 1)))

Crystalline.GlobalCrystallineSituation.pullbackSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/HigherDirectImage.lean, line 320. The attribute's comment: “the pullback F_U of a sheaf on Cris(X/S) to Cris(U/T), completing the data of the remark's recipe. NOT covered, here or elsewhere: the displayed equation 07MK (Rf_{cris,}F)_{T'} = R(T → T')_(R τ_{U/T,*} F_U), which the source states without proof, and the hint that Cris(U/T) is the localization of Cris(X/S) at f_cris^{-1} h_{(U',T',δ')}”.

Stacks Project, Tag 07MJ. The pullback F_U to Cris(U/T) of a sheaf F on Cris(X/S).

def pullbackSheaf (F : smallTopos S) : smallTopos (pullbackSituation S S' fS fX hf A')
Tag 07ML, a remark

Tag 07ML in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.isPullback_sections_openCoverSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisCover.lean, line 324. The attribute's comment: “the Mayer-Vietoris square of the covering on Cris(X/S), the fact the remark's triangle is a formal consequence of. The triangle at a fixed object of the site is openCoverTriangle_distinguished of SmallSite/MayerVietorisTriangle.lean; the remark's own statement, about the derived global sections of the four crystalline sites, is not stated”.

Stacks Project, Tag 07ML. Mayer--Vietoris for an open covering X = X' ∪ X'' on the small crystalline site: for every sheaf F on Cris(X/S) and every object (U, T, δ), the sections of F over (U, T, δ) and over its restrictions to X', X'' and X''' = X' ∩ X'' form a cartesian square. For a sheaf of abelian groups this is exactness of 0 ⟶ F(U, T, δ) ⟶ F' ⊕ F'' ⟶ F'''.

This is the geometric input the remark reduces its distinguished triangle to. The short exact form of this square at an injective abelian sheaf is CrystallineThickening.openCoverShortComplex_shortExact of StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisShortExact.lean, and the triangle it yields, at a fixed object of the site, is CrystallineThickening.openCoverTriangle_distinguished of StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisTriangle.lean. What the remark's own statement still wants is the same sequence for the derived global sections of the four crystalline sites; see the module documentation.

theorem isPullback_sections_openCoverSquare {𝒜 : Type v} [Category.{w} 𝒜]
    (A : CrystallineThickening S) {V₁ V₂ : S.X.Opens} (hV : V₁ ⊔ V₂ = ⊤)
    (F : Sheaf (smallTopology S) 𝒜) :
    ((openCoverSquare A V₁ V₂).op.map F.obj).IsPullback

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.openCoverShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisShortExact.lean, line 87. The attribute's comment: “the Mayer-Vietoris sequence of the covering on Cris(X/S), short exact at an injective sheaf, which is the form a derived functor consumes. NOT the remark's triangle: that is openCoverTriangle_distinguished of SmallSite/MayerVietorisTriangle.lean, at a fixed object of the site, and identifying its terms with RGamma of the four sites is still open”.

The Mayer--Vietoris sequence of an injective abelian sheaf on Cris(X/S) for an open covering X = X' ∪ X'' is short exact:

0 ⟶ I(U, T, δ) ⟶ I' ⊕ I'' ⟶ I''' ⟶ 0.

theorem openCoverShortComplex_shortExact (A : CrystallineThickening S) {V₁ V₂ : S.X.Opens}
    (hV : V₁ ⊔ V₂ = ⊤) (I : Sheaf (smallTopology S) AddCommGrpCat.{u + 1}) [Injective I] :
    (openCoverShortComplex A V₁ V₂ I).ShortExact

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.longExact_openCoverFunctorComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisTriangle.lean, line 265. The attribute's comment: “the long exact sequence of the same Mayer-Vietoris short complex of section functors, at a fixed object of Cris(X/S). NOT the identification of its terms with RGamma of the four crystalline sites: that needs the same sequence for GLOBAL sections, see the module docstring”.

Stacks Project, Tag 07ML. The long exact sequence of the Mayer--Vietoris short complex of section functors of an open covering X = X' ∪ X'', at a fixed object (U, T, δ) of Cris(X/S): the right derived functors of sections over (U, T, δ), of the sum of sections over the X'- and X''-parts, and of sections over the X'''-part fit into a long exact sequence, natural in the abelian sheaf.

The same scope caveat as for openCoverTriangle_distinguished applies: this is the sequence at a fixed object of the site, and identifying its terms with the derived global sections of the four crystalline sites of the remark needs clause (d) of [Stacks, Tag 07KL].

theorem longExact_openCoverFunctorComplex (A : CrystallineThickening S) {V₁ V₂ : S.X.Opens}
    (hV : V₁ ⊔ V₂ = ⊤) :
    ∃ delta : ∀ n : ℕ, (openCoverFunctorComplex A V₁ V₂).X₃.rightDerived n ⟶
        (openCoverFunctorComplex A V₁ V₂).X₁.rightDerived (n + 1),
      (∀ F : Sheaf (smallTopology S) AddCommGrpCat.{u + 1},
          Mono ((NatTrans.rightDerived (openCoverFunctorComplex A V₁ V₂).f 0).app F)) ∧
        ∀ (n : ℕ) (F : Sheaf (smallTopology S) AddCommGrpCat.{u + 1}),
          (ComposableArrows.mk₅
            ((NatTrans.rightDerived (openCoverFunctorComplex A V₁ V₂).f n).app F)
            ((NatTrans.rightDerived (openCoverFunctorComplex A V₁ V₂).g n).app F)
            ((delta n).app F)
            ((NatTrans.rightDerived (openCoverFunctorComplex A V₁ V₂).f (n + 1)).app F)
            ((NatTrans.rightDerived (openCoverFunctorComplex A V₁ V₂).g (n + 1)).app F)).Exact

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.openCoverTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/MayerVietorisTriangle.lean, line 347. The attribute's comment: “the remark's distinguished triangle, at a fixed object (U, T, delta) of Cris(X/S) and a fixed pair of opens of X, for a cochain complex of injective abelian sheaves. NOT the identification of the three terms with RGamma(Cris(X'/S), F) etc., which needs the same short exact sequence for GLOBAL sections of the four sites; see the module docstring”.

Stacks Project, Tag 07ML. The Mayer--Vietoris triangle of an open covering X = X' ∪ X'' on the small crystalline site is distinguished: for every object (U, T, δ) of Cris(X/S) and every cochain complex K of injective abelian sheaves on Cris(X/S),

Γ((U, T, δ), K) ⟶ Γ(X'-part, K) ⊕ Γ(X''-part, K) ⟶ Γ(X'''-part, K) ⟶ [1]

is a distinguished triangle of D(Ab).

This is the remark's triangle at a fixed object of the site and a fixed pair of opens of X. Identifying its three terms with RΓ(Cris(X/S), F), RΓ(Cris(X'/S), F), RΓ(Cris(X''/S), F) and RΓ(Cris(X'''/S), F) is a further step, which the module docstring describes; it is not claimed here.

theorem openCoverTriangle_distinguished (A : CrystallineThickening S) {V₁ V₂ : S.X.Opens}
    (hV : V₁ ⊔ V₂ = ⊤) (K : CochainComplex (Sheaf (smallTopology S) AddCommGrpCat.{u + 1}) ℤ)
    (hK : ∀ n, Injective (K.X n)) :
    openCoverTriangle A hV K hK ∈ distTriang (DerivedCategory AddCommGrpCat.{u + 1})
Tag 07MS, a remark

Tag 07MS in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.crisGlobalBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/BaseChangeMapGlobal07MS.lean, line 72. The attribute's comment: “the base change map RΓ(Cris(X'/S'), F') ⊗^L_{A'} A ⟶ RΓ(Cris(X/S), F) of (07MT) in D(A), the sheaf-level base change map read on global sections, for an arbitrary g : X ⟶ X'”.

The base change map (07MT) on global sections

RΓ(Cris(X'/S'), F') ⊗^L_{A'} A ⟶ RΓ(Cris(X/S), F) in D(A),

A = Γ(S, 𝒪_S), A' = Γ(S', 𝒪_{S'}), for an 𝒪_{X'/S'}-module F', its pullback F = f_cris^*F' (crisModuleInverseImage) and an arbitrary morphism g : X ⟶ X' over a morphism of divided power bases f. It is RΓ(S, -) of the sheaf-level base change map crisSheafBaseChangeMap, preceded by the canonical map RΓ(S', K) ⊗^L_{A'} A ⟶ RΓ(S, L(S ⟶ S')^*K) at K = Rτ_{X'/S', *}F' and read through RΓ(S, Rτ_*-) = RΓ(Cris, -) at both ends.

def crisGlobalBaseChangeMap (F' : ModuleSheaf S') :
    (derivedBaseChangeTensor f).obj
        (DerivedCategory.Plus.ι.obj ((derivedModuleGlobalSections S').obj F')) ⟶
      DerivedCategory.Plus.ι.obj
        ((derivedModuleGlobalSections S).obj ((crisModuleInverseImage f g h).obj F'))

Crystalline.GlobalCrystallineSituation.SmallSite.crisSheafBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/BaseChangeMapSheaf07MS.lean, line 109. The attribute's comment: “the canonical base change map L(S ⟶ S')^ Rτ_{X'/S',} F' ⟶ Rτ_{X/S,} F in D(O_S), F = f_cris^ F', for an arbitrary morphism g : X ⟶ X', built as the hint prescribes”.

Stacks Project, Tag 07MS: the canonical base change map

L(S ⟶ S')^* Rτ_{X'/S', *}F' ⟶ Rτ_{X/S, *}F in D(𝒪_S),

for an 𝒪_{X'/S'}-module F', its pullback F = f_cris^*F' (crisModuleInverseImage), and an arbitrary morphism g : X ⟶ X' over a morphism of divided power bases f — the situation of [Stacks, Tag 07MJ]. As the source's hint prescribes, it is the base change map of [Stacks, Tag 07A7] for the square structureSquareTwoIso, followed by Rτ_{X/S, *} of the canonical map Lf_cris^*F' ⟶ f_cris^*F' = F.

def crisSheafBaseChangeMap (F' : ModuleSheaf S') :
    (derivedPullback (X := zariskiRingedTopos S.S.scheme) (Y := zariskiRingedTopos S'.S.scheme)
        (zariskiRingedHom f.hom)).obj (tauDerivedDirectImage S' F') ⟶
      tauDerivedDirectImage S ((crisModuleInverseImage f g h).obj F')

Crystalline.GlobalCrystallineSituation.SmallSite.crisModuleInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/LowerShriekModules.lean, line 357. The attribute's comment: “the pullback F = f_cris^* F' of an O_{X'/S'}-module F', for an arbitrary morphism g : X ⟶ X'”.

f_cris^{-1} on sheaves of modules, in the generality of [Stacks, Tag 07MJ]: no hypothesis whatever on g : X ⟶ X', in particular not that it is an open immersion, so this covers the hypothesis X = X' ×_{S'₀} S₀ of [Stacks, Tag 07MU](4).

It is the composite of the two legs of [Stacks, Tag 07IK]'s f_cris = π_{X'} ∘ f_CRIS ∘ i_X: the module-level i_{X', !} of [Stacks, Tag 07IJ] carries a sheaf of 𝒪_{X'/S'}-modules on Cris(X'/S') to the big site CRIS(X'/S'), and ...SmallSite.crisModulePullback restricts it along Cris(X/S) ⥤ CRIS(X/S) ⥤ CRIS(X'/S'), a functor of sites that exists for every g.

Where ...SmallSite.smallChangeBaseModulePullback applies — that is, for g an open immersion, the generality of [Stacks, Tag 07KL] — the two agree, by crisModuleInverseImageIsoSmallChangeBase.

This is the pullback F = f_cris^*F' of [Stacks, Tag 07MS]; the base change map of that tag, L(S ⟶ S')^*Rτ_{X'/S', *}F' ⟶ Rτ_{X/S, *}F, is ...SmallSite.crisSheafBaseChangeMap, and on global sections ...SmallSite.crisGlobalBaseChangeMap.

def crisModuleInverseImage (f : S.S ⟶ S'.S) (g : S.X ⟶ S'.X)
    (h : S.toClosedFiber ≫ DividedPowerScheme.closedFiberMap f = g ≫ S'.toClosedFiber) :
    ModuleSheaf S' ⥤ ModuleSheaf S
Tag 07MV, a remark

Tag 07MV in the Stacks Project.

Crystalline.exists_forall_isPAdicLevel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelBase.lean, line 72. The attribute's comment: “for e ≫ 0 the ideal (p^e) ⊆ I is preserved by γ”.

Stacks Project, Tag 07MV. For a divided power ring (A, I, γ) with A an algebra over ℤ_(p) and p nilpotent in A/I, every sufficiently large exponent e has (p^e) ⊆ I preserved by γ.

theorem exists_forall_isPAdicLevel [Fact p.Prime]
    [Algebra (DividedPowers.IntegersAtPrime p) A]
    (hp : IsNilpotent (Ideal.Quotient.mk I (p : A))) :
    ∃ N, ∀ e, N ≤ e → IsPAdicLevel I γ p e

Crystalline.pAdicLevelRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelBase.lean, line 138. The attribute's comment: “the divided power ring A/p^eA whose spectrum is the base S_e = Spec(A/p^eA)”.

Stacks Project, Tag 07MV. The divided power ring (A/p^eA, I/p^eA, γ̄) at a finite divided power level e, of which the base S_e = Spec(A/p^eA) of the remark is the spectrum.

noncomputable def pAdicLevelRing {e : ℕ} (he : IsPAdicLevel I γ p e) : DividedPowerRing.{u}

Crystalline.preservesInjectiveObjects_pAdicLevelSheafRestriction, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelRestrictionInjectives.lean, line 159. The attribute's comment: “restriction of abelian sheaves to a finite level carries injectives to injectives, the first half of the remark's hint”.

Stacks Project, Tag 07MV. Restriction of abelian sheaves from Cris(X/S) to a finite divided power level Cris(X/S_e) carries injective abelian sheaves to injective abelian sheaves.

This is the first half of the hint of the remark. The functor of levels is change of divided power base at the pair (S_e ⟶ S, 𝟙 X), so this is ...SmallSite.preservesInjectiveObjects_smallChangeBaseAbelianRestriction: the left adjoint of restriction is the abelian lower shriek, which is exact by [Stacks, Tag 00X4] because Cris(X/S_e) has fibre products and equalizers and change of base preserves them, hence preserves monomorphisms, and a right adjoint of a monomorphism-preserving functor preserves injective objects, [Stacks, Tag 015Z].

instance preservesInjectiveObjects_pAdicLevelSheafRestriction {e : ℕ}
    (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    (pAdicLevelSheafRestriction I γ p he X toCF hX).PreservesInjectiveObjects

Crystalline.preservesInjectiveObjects_pAdicLevelStepSheafRestriction, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelRestrictionInjectives.lean, line 176. The attribute's comment: “restriction of abelian sheaves between two finite levels carries injectives to injectives”.

Stacks Project, Tag 07MV. Restriction of abelian sheaves between two finite divided power levels Cris(X/S_e) ⟶ Cris(X/S_m), for m ≤ e, carries injective abelian sheaves to injective abelian sheaves. This is the same argument as Crystalline.preservesInjectiveObjects_pAdicLevelSheafRestriction at the pair (S_m ⟶ S_e, 𝟙 X).

instance preservesInjectiveObjects_pAdicLevelStepSheafRestriction {m e : ℕ}
    (hm : IsPAdicLevel I γ p m) (he : IsPAdicLevel I γ p e) (hme : m ≤ e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    (pAdicLevelStepSheafRestriction I γ p hm he hme X toCF hX).PreservesInjectiveObjects

Crystalline.rightAcyclic_globalSections_pAdicLevelSheafRestriction_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelRestrictionInjectives.lean, line 234. The attribute's comment: “restriction to a finite level carries an injective abelian sheaf to one with acyclic global sections, the acyclicity hypothesis of (015M); NOT the tower and NOT the remark's conclusion”.

Stacks Project, Tag 07MV. Restriction to a finite divided power level carries an injective abelian sheaf to one with acyclic global sections: this is Crystalline.preservesInjectiveObjects_pAdicLevelSheafRestriction followed by CategoryTheory.Functor.rightAcyclic_of_injective, an injective object being right acyclic for every additive functor whose bounded below right derived functor exists.

This is verbatim the hypothesis hg of Crystalline.GlobalCrystallineSituation.SmallSite.derivedGlobalSectionsCompIso, and so the first half of the hint of the remark.

theorem rightAcyclic_globalSections_pAdicLevelSheafRestriction_of_injective {e : ℕ}
    (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w'} (Sheaf (smallTopology (pAdicLevelSituation I γ p he X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w''} AddCommGrpCat.{u + 1}] :
    ∀ F : Sheaf (smallTopology (specSituation I γ p X toCF hX)) AddCommGrpCat.{u + 1},
      Injective F → (globalSections (pAdicLevelSituation I γ p he X toCF hX)).rightAcyclic
        ((pAdicLevelSheafRestriction I γ p he X toCF hX).obj F)

Crystalline.rightAcyclic_globalSections_pAdicLevelStepSheafRestriction_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelRestrictionInjectives.lean, line 253. The attribute's comment: “restriction between two finite levels carries an injective abelian sheaf to one with acyclic global sections, the acyclicity hypothesis of (015M) for the tower's arrows”.

Stacks Project, Tag 07MV. The transition-functor form of Crystalline.rightAcyclic_globalSections_pAdicLevelSheafRestriction_of_injective: restriction from Cris(X/S_e) to Cris(X/S_m), m ≤ e, carries an injective abelian sheaf to one with acyclic global sections.

theorem rightAcyclic_globalSections_pAdicLevelStepSheafRestriction_of_injective {m e : ℕ}
    (hm : IsPAdicLevel I γ p m) (he : IsPAdicLevel I γ p e) (hme : m ≤ e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w'} (Sheaf (smallTopology (pAdicLevelSituation I γ p hm X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w''} AddCommGrpCat.{u + 1}] :
    ∀ F : Sheaf (smallTopology (pAdicLevelSituation I γ p he X toCF hX)) AddCommGrpCat.{u + 1},
      Injective F → (globalSections (pAdicLevelSituation I γ p hm X toCF hX)).rightAcyclic
        ((pAdicLevelStepSheafRestriction I γ p hm he hme X toCF hX).obj F)

Crystalline.pAdicLevelScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 174. The attribute's comment: “S_e = Spec(A/p^eA) is a divided power base, for e a finite divided power level”.

The divided power base S_e = Spec(A/p^eA) at a finite divided power level e: the spectrum of the divided power ring Crystalline.pAdicLevelRing.

def pAdicLevelScheme {e : ℕ} (he : IsPAdicLevel I γ p e) : DividedPowerScheme.{u}

Crystalline.pAdicLevelClosedFiberIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 243. The attribute's comment: “S_e has the same closed fibre S₀ = Spec(A/I) as S, since (p^e) ⊆ I”.

The closed fibre of S_e = Spec(A/p^eA) is the closed fibre S_0 = Spec(A/I) of S. Both are the spectrum of a double quotient of A, and the two double quotients agree because (p^e) ⊆ I.

def pAdicLevelClosedFiberIso {e : ℕ} (he : IsPAdicLevel I γ p e) :
    closedFiber (pAdicLevelScheme I γ p he) ≅ closedFiber (specBase I γ)

Crystalline.pAdicLevelSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 323. The attribute's comment: “X/S_e is a global crystalline situation on the same X, so Cris(X/S_e) is defined”.

The global crystalline situation X/S_e at a finite divided power level e, on the same scheme X: the structure morphism X ⟶ S_0 of the situation X/S is read in the closed fibre of S_e through the identification Crystalline.pAdicLevelClosedFiberIso of the two closed fibres.

def pAdicLevelSituation {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    GlobalCrystallineSituation.{u}

Crystalline.pAdicLevelExtend, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 390. The attribute's comment: “the functor Cris(X/S_e) ⥤ Cris(X/S)”.

The functor Cris(X/S_e) ⥤ Cris(X/S): change of divided power base along the projection S_e ⟶ S and the identity of X. An object of Cris(X/S_e) is a divided power thickening of X relative to S_e, which composed with S_e ⟶ S is one relative to S.

def pAdicLevelExtend {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    GlobalCrystallineSituation.CrystallineThickening
        (pAdicLevelSituation I γ p he X toCF hX) ⥤
      GlobalCrystallineSituation.CrystallineThickening (specSituation I γ p X toCF hX)

Crystalline.pAdicLevelExtendFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 403. The attribute's comment: “Cris(X/S_e) is a full subcategory of Cris(X/S)”.

Cris(X/S_e) is a full subcategory of Cris(X/S): change of divided power base along S_e ⟶ S and 𝟙 X is fully faithful, the projection S_e ⟶ S being a closed immersion and hence a monomorphism.

def pAdicLevelExtendFullyFaithful {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    (pAdicLevelExtend I γ p he X toCF hX).FullyFaithful

Crystalline.pAdicLevelModuleRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelSite.lean, line 446. The attribute's comment: “F_e, the restriction of an 𝒪_{X/S}-module F to Cris(X/S_e), as a presheaf of modules”.

The restriction F_e of a presheaf of 𝒪_{X/S}-modules on Cris(X/S) to a presheaf of 𝒪_{X/S_e}-modules on Cris(X/S_e). No comparison of structure presheaves is needed: the restriction of 𝒪_{X/S} along the functor is 𝒪_{X/S_e} itself, by Crystalline.pAdicLevelExtend_op_comp_crisRing.

def pAdicLevelModuleRestriction {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    (F : PresheafOfModules.{u}
      (GlobalCrystallineSituation.SmallSite.crisRing (specSituation I γ p X toCF hX))) :
    PresheafOfModules.{u}
      (GlobalCrystallineSituation.SmallSite.crisRing
        (pAdicLevelSituation I γ p he X toCF hX))

Crystalline.pAdicLevelStepExtend, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTower.lean, line 419. The attribute's comment: “the transition functor Cris(X/S_m) ⥤ Cris(X/S_e) of the tower of finite levels”.

Stacks Project, Tag 07MV. The transition functor Cris(X/S_m) ⥤ Cris(X/S_e) of the tower of finite divided power levels, for m ≤ e: change of divided power base along the closed immersion S_m ⟶ S_e and the identity of X. This is the arrow of the tower whose inverse limit the remark takes; Crystalline.pAdicLevelExtend is its colimit end, the functor to Cris(X/S) itself.

def pAdicLevelStepExtend {m e : ℕ} (hm : IsPAdicLevel I γ p m) (he : IsPAdicLevel I γ p e)
    (hme : m ≤ e) (X : Scheme.{u}) (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    GlobalCrystallineSituation.CrystallineThickening
        (pAdicLevelSituation I γ p hm X toCF hX) ⥤
      GlobalCrystallineSituation.CrystallineThickening
        (pAdicLevelSituation I γ p he X toCF hX)

Crystalline.pAdicLevelStepExtendFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTower.lean, line 433. The attribute's comment: “Cris(X/S_m) is a full subcategory of Cris(X/S_e) for m ≤ e”.

Stacks Project, Tag 07MV. Cris(X/S_m) is a full subcategory of Cris(X/S_e) for m ≤ e: the transition S_m ⟶ S_e is a closed immersion, hence a monomorphism.

def pAdicLevelStepExtendFullyFaithful {m e : ℕ} (hm : IsPAdicLevel I γ p m)
    (he : IsPAdicLevel I γ p e) (hme : m ≤ e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    (pAdicLevelStepExtend I γ p hm he hme X toCF hX).FullyFaithful

Crystalline.pAdicLevelSmallModuleRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTower.lean, line 504. The attribute's comment: “F_e as a sheaf of 𝒪_{X/S_e}-modules on the small site Cris(X/S_e), by restriction”.

Stacks Project, Tag 07MV. F_e, the restriction of a sheaf of 𝒪_{X/S}-modules on the small crystalline site Cris(X/S) to a sheaf of 𝒪_{X/S_e}-modules on Cris(X/S_e).

This is the F_e of the remark. It is the restriction itself, not a sheafification of it: that rests on the continuity of Crystalline.pAdicLevelExtend, and no comparison of structure sheaves is needed because the restriction of 𝒪_{X/S} along the functor is 𝒪_{X/S_e}.

def pAdicLevelSmallModuleRestriction {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x)) :
    SheafOfModules.{u} (GlobalCrystallineSituation.SmallSite.structureSheaf
        (specSituation I γ p X toCF hX)) ⥤
      SheafOfModules.{u} (GlobalCrystallineSituation.SmallSite.structureSheaf
        (pAdicLevelSituation I γ p he X toCF hX))

Crystalline.pAdicLevelDerivedGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTower.lean, line 539. The attribute's comment: “the individual terms RΓ(Cris(X/S_e), F_e) of the remark's R lim, for F an abelian sheaf; NOT the tower (its arrows are missing) and NOT the conclusion”.

Stacks Project, Tag 07MV. RΓ(Cris(X/S_e), F_e), the term at level e of the tower whose derived inverse limit the remark takes: derived global sections on the small crystalline site of X/S_e applied to the restriction F_e of an abelian sheaf F on Cris(X/S).

This is an object of D⁺(Ab), and it is the restriction F_e itself — not a sheafification of it — that is being evaluated, by the continuity of Crystalline.pAdicLevelExtend.

def pAdicLevelDerivedGlobalSections {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w} (Sheaf (GlobalCrystallineSituation.smallTopology
      (pAdicLevelSituation I γ p he X toCF hX)) AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} AddCommGrpCat.{u + 1}]
    (F : Sheaf (GlobalCrystallineSituation.smallTopology (specSituation I γ p X toCF hX))
      AddCommGrpCat.{u + 1}) :
    DerivedCategory.Plus AddCommGrpCat.{u + 1}

Crystalline.pAdicLevelStepDerivedGlobalSectionsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTowerArrows.lean, line 296. The attribute's comment: “the arrow RΓ(Cris(X/S_e), F_e) ⟶ RΓ(Cris(X/S_m), F_m) of the remark's tower, for m ≤ e”.

Stacks Project, Tag 07MV. The arrow RΓ(Cris(X/S_e), F_e) ⟶ RΓ(Cris(X/S_m), F_m) of the tower of finite divided power levels, for m ≤ e.

Four inputs from the library and no hypothesis. The underived comparison Crystalline.pAdicLevelStepGlobalSectionsTrans is derived by Stacks.DerivedIndexing.rightDerivedFunctorPlusNatTrans; its target, the derived functor of the composite ρ ⋙ Γ(Cris(X/S_m), -), is split by Crystalline.pAdicLevelStepDerivedGlobalSectionsCompIso, which is [Stacks, Tag 015M] and is unconditional because restriction to a level preserves injectives; CategoryTheory.Functor.rightDerivedFunctorPlusObjSingleIso replaces Rρ(F_e[0]) by ρ(F_e)[0], restriction to a level being exact; and Crystalline.pAdicLevelStepSheafRestrictionCompIso identifies ρ(F_e) with F_m.

def pAdicLevelStepDerivedGlobalSectionsMap {m e : ℕ} (hm : IsPAdicLevel I γ p m)
    (he : IsPAdicLevel I γ p e) (hme : m ≤ e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w} (Sheaf (smallTopology (pAdicLevelSituation I γ p he X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} (Sheaf (smallTopology (pAdicLevelSituation I γ p hm X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w''} AddCommGrpCat.{u + 1}]
    (F : Sheaf (smallTopology (specSituation I γ p X toCF hX)) AddCommGrpCat.{u + 1}) :
    pAdicLevelDerivedGlobalSections I γ p he X toCF hX F ⟶
      pAdicLevelDerivedGlobalSections I γ p hm X toCF hX F

Crystalline.pAdicLevelDerivedGlobalSectionsTower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTowerArrows.lean, line 337. The attribute's comment: “the tower e ↦ RΓ(Cris(X/S_e), F_e) of the remark, as a functor ℕᵒᵖ ⥤ D⁺(Ab); NOT the remark's conclusion, that RΓ(Cris(X/S), F) is its derived limit”.

Stacks Project, Tag 07MV. The tower n ↦ RΓ(Cris(X/S_{N+n}), F_{N+n}) of the remark, as a functor ℕᵒᵖ ⥤ D⁺(Ab).

The terms are Crystalline.pAdicLevelDerivedGlobalSections and the arrows are Crystalline.pAdicLevelStepDerivedGlobalSectionsMap at the successive pairs N + n ≤ N + n + 1. CategoryTheory.Functor.ofOpSequence asks for no more than those successive steps, which is why no coherence between three levels is needed. The threshold N is the one of Crystalline.exists_forall_isPAdicLevel: the remark's exponents are the levels, and e ≫ 0 is the hypothesis hN.

This is the tower whose derived limit the remark asserts is RΓ(Cris(X/S), F). That assertion is not proved: nothing below compares the tower with RΓ(Cris(X/S), F).

def pAdicLevelDerivedGlobalSectionsTower {N : ℕ}
    (hN : ∀ e, N ≤ e → IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w''} AddCommGrpCat.{u + 1}]
    (F : Sheaf (smallTopology (specSituation I γ p X toCF hX)) AddCommGrpCat.{u + 1}) :
    ℕᵒᵖ ⥤ DerivedCategory.Plus AddCommGrpCat.{u + 1}

Crystalline.pAdicLevelDerivedGlobalSectionsConeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FiniteLevelTowerCone.lean, line 197. The attribute's comment: “the arrow RΓ(Cris(X/S), F) ⟶ RΓ(Cris(X/S_e), F_e) comparing derived global sections with the remark's tower; NOT the remark's conclusion, that RΓ(Cris(X/S), F) is the derived limit”.

Stacks Project, Tag 07MV. The arrow RΓ(Cris(X/S), F) ⟶ RΓ(Cris(X/S_e), F_e) from derived global sections on Cris(X/S) to the term of the remark's tower at the finite divided power level e.

It is assembled exactly as Crystalline.pAdicLevelStepDerivedGlobalSectionsMap is, from four proved inputs and no hypothesis. The underived restriction Crystalline.pAdicLevelGlobalSectionsTrans is derived by Stacks.DerivedIndexing.rightDerivedFunctorPlusNatTrans; its target, the derived functor of the composite ρ_e ⋙ Γ(Cris(X/S_e), -), is split by Crystalline.pAdicLevelDerivedGlobalSectionsCompIso, which is [Stacks, Tag 015M] and is unconditional because restriction to a level preserves injectives; and CategoryTheory.Functor.rightDerivedFunctorPlusObjSingleIso replaces Rρ_e(F[0]) by F_e[0], restriction to a level being exact. Unlike the step map no further identification is needed: the sheaf being restricted is F itself.

This is the comparison whose being a derived limit presentation is the conclusion of the remark; that it is one is not proved.

def pAdicLevelDerivedGlobalSectionsConeMap {e : ℕ} (he : IsPAdicLevel I γ p e) (X : Scheme.{u})
    (toCF : X ⟶ DividedPowerScheme.closedFiber (specBase I γ))
    (hX : ∀ x : X, IsNilpotent (p : X.presheaf.stalk x))
    [HasDerivedCategory.{w} (Sheaf (smallTopology (specSituation I γ p X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} (Sheaf (smallTopology (pAdicLevelSituation I γ p he X toCF hX))
      AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w''} AddCommGrpCat.{u + 1}]
    (F : Sheaf (smallTopology (specSituation I γ p X toCF hX)) AddCommGrpCat.{u + 1}) :
    (derivedGlobalSections (specSituation I γ p X toCF hX)).obj F ⟶
      pAdicLevelDerivedGlobalSections I γ p he X toCF hX F
Tag 07MW, a remark

Tag 07MW in the Stacks Project.

Crystalline.GlobalCrystallineSituation.smoothLiftingCrystallineThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmoothLifting.lean, line 343. The attribute's comment: “part (1): γ extends to the ideal of X in Y, and (X, Y, γ) is an object of Cris(X/S)”.

The object (X, Y, γ) of the small crystalline site Cris(X/S) given by a smooth lifting Y of the closed fibre: the object smoothLiftingThickening of CRIS(X/S), whose map to X is the identity.

noncomputable def smoothLiftingCrystallineThickening : CrystallineThickening base
Sources
LeanCrystalline.GlobalCrystallineSituation.pullbackToClosedFiber · Crystalline.GlobalCrystallineSituation.pullbackSituation · Crystalline.GlobalCrystallineSituation.isOpenImmersion_pullbackSituationToX · Crystalline.GlobalCrystallineSituation.range_pullbackSituationToX · Crystalline.GlobalCrystallineSituation.pullbackCrisMorphism · Crystalline.GlobalCrystallineSituation.pullbackStructureToposMorphism · Crystalline.GlobalCrystallineSituation.pullbackSheaf · Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.isPullback_sections_openCoverSquare

Section60.25 Pulling back along purely inseparable maps#

Section 60.25 of the Stacks Project, Tag 07PZ. 7 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07Q1, an item

Tag 07Q1 in the Stacks Project.

Declarations registered for the tag:

Tag 07Q7, a lemma

Tag 07Q7 in the Stacks Project.

Crystalline.exists_homotopyInverse_baseChangeDeRhamMap_baseLinear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/BaseChangeHomotopyInverse/Existence.lean, line 139. The attribute's comment: “with the B-linearity of the reverse map e and of the homotopy h, which the p-adically completed form of Tag 07N1 needs”.

Stacks 07Q7 (Lemma 60.25.1). In the situation of Section 60.25 — a commutative square B → B' over A → A', quotients Ω_{B/A} → Ω and Ω_{B'/A'} → Ω' to which the de Rham differential descends, a compatible ψ : Ω → Ω', a B-module M with integrable connection ∇, the canonical map of complexes c_M^• of equation 07PY, and data a ∈ B, z ∈ B', θ : B' → B' satisfying assumptions (1)–(7) — there exists a map of complexes

e_M^• : M ⊗_B (Ω')^• ⟶ M ⊗_B Ω^•

such that c_M^• ∘ e_M^• and e_M^• ∘ c_M^• are homotopic to multiplication by a.

public theorem exists_homotopyInverse_baseChangeDeRhamMap_baseLinear
    (S : SourceDeRham A B) (S' : SourceDeRham A' B')
    (pi : Ω[B⁄A] →ₗ[B] Omega) (pi' : Ω[B'⁄A'] →ₗ[B'] Omega')
    (hpi : Function.Surjective pi) (hgen : S.GenerationHypothesis pi)
    (hpi' : Function.Surjective pi') (hgen' : S'.GenerationHypothesis pi')
    (psi : Omega →ₛₗ[algebraMap B B'] Omega')
    (hpsi : ∀ b : B, psi (pi (KaehlerDifferential.D A B b)) =
      pi' (KaehlerDifferential.D A' B' (algebraMap B B' b)))
    (nabla : Connection A B pi M)
    (hintegrable : Connection.IsIntegrable S pi hpi hgen nabla)
    (c : ∀ p : ℕ,
      RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)) →ₗ[A]
        RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')))
    (hc_wedge : ∀ (p : ℕ) (m : M) (omega : Fin p → Omega),
      c p (m ⊗ₜ[B] exteriorPower.ιMulti B p omega) =
        (1 ⊗ₜ[B] m) ⊗ₜ[B'] exteriorPower.ιMulti B' p (psi ∘ omega))
    (hc_comm : ∀ (p : ℕ) (x : M ⊗[B] (⋀[B]^p Omega)),
      c (p + 1)
          ((extendedConnection S pi hpi hgen nabla).toLinearMap p x) =
        (extendedConnection S' pi' hpi' hgen'
          (Connection.baseChange psi nabla hpsi)).toLinearMap p (c p x))
    (a : B) (z : B') (theta : B' →ₗ[B] B')
    (dec : DzDecomposition pi' psi z)
    (hd_a_eq_zero : SourceDeRham.targetD pi a = 0)
    (hpartialZ_theta : ∀ f : B', dec.partialZ (theta f) = a • f)
    (huniv :
      Stacks.UniversalInjectivity.LocalizationCriteria.UniversallyInjective.{max u w}
        (Algebra.linearMap B B'))
    (hepsilon : ∀ f : B',
      a • f - theta (dec.partialZ f) ∈ Set.range (algebraMap B B'))
    (hepsilonPrime : ∀ f : B',
      TensorProduct.map theta (LinearMap.id (R := B) (M := Omega)) (dec.dOne f) -
          dec.dOne (theta f) ∈
        LinearMap.range (TensorProduct.mk B B' Omega 1)) :
    ∃ e : ∀ p : ℕ,
      RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')) →ₗ[A]
        RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)),
      (∀ (p : ℕ) (x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega'))),
          e (p + 1)
              ((extendedConnection S' pi' hpi' hgen'
                (Connection.baseChange psi nabla hpsi)).toLinearMap
                p x) =
            (extendedConnection S pi hpi hgen nabla).toLinearMap
              p (e p x)) ∧
        (∀ (p : ℕ) (b : B) (y : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega'))),
            e p (RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega'))
                (algebraMap B B' b) y) =
              RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^p Omega)) b (e p y)) ∧
        (∃ h : ∀ p : ℕ,
            RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega')) →ₗ[A]
              RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')),
          (∀ x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^0 Omega')),
              h 0 ((extendedConnection S' pi' hpi' hgen'
                (Connection.baseChange psi nabla hpsi)).toLinearMap
                0 x) =
                RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^0 Omega'))
                    (algebraMap B B' a) x -
                  c 0 (e 0 x)) ∧
            (∀ (p : ℕ)
                (x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))),
              (show RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega')) from
                (extendedConnection S' pi' hpi' hgen'
                  (Connection.baseChange psi nabla hpsi)).toLinearMap
                    p (h p x)) +
                  h (p + 1)
                    ((extendedConnection S' pi' hpi' hgen'
                      (Connection.baseChange psi nabla hpsi)).toLinearMap
                      (p + 1) x) =
                RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))
                    (algebraMap B B' a) x -
                  c (p + 1) (e (p + 1) x)) ∧
            (∀ (p : ℕ) (b : B)
                (y : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))),
              h p (RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))
                  (algebraMap B B' b) y) =
                RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega'))
                  (algebraMap B B' b) (h p y))) ∧
        (∃ k : ∀ p : ℕ,
            RestrictScalars A B (M ⊗[B] (⋀[B]^(p + 1) Omega)) →ₗ[A]
              RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)),
          (∀ x : RestrictScalars A B (M ⊗[B] (⋀[B]^0 Omega)),
              k 0 ((extendedConnection S pi hpi hgen nabla).toLinearMap
                0 x) =
                RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^0 Omega)) a x - e 0 (c 0 x)) ∧
            (∀ (p : ℕ) (x : RestrictScalars A B (M ⊗[B] (⋀[B]^(p + 1) Omega))),
              (extendedConnection S pi hpi hgen nabla).toLinearMap
                  p (k p x) +
                k (p + 1)
                  ((extendedConnection S pi hpi hgen nabla).toLinearMap
                    (p + 1) x) =
                RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^(p + 1) Omega)) a x -
                  e (p + 1) (c (p + 1) x)) ∧
            (∀ (p : ℕ) (b : B) (x : RestrictScalars A B (M ⊗[B] (⋀[B]^(p + 1) Omega))),
              k p (RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^(p + 1) Omega)) b x) =
                RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^p Omega)) b (k p x)))

Crystalline.exists_homotopyInverse_baseChangeDeRhamMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/BaseChangeHomotopyInverse/Existence.lean, line 368.

Let c_M^• : M ⊗_B Ω^• ⟶ (M ⊗_B B') ⊗_{B'} (Ω')^• be the base change map of de Rham complexes of a B-module M with integrable connection ∇. Given a ∈ B with d(a) = 0, a decomposition Ω' = (B' ⊗_B Ω) ⊕ B' dz, and a B-linear θ : B' → B' with ∂_z ∘ θ = a, a f - θ(∂_z(f)) ∈ B and (θ ⊗ 1)(d₁(f)) - d₁(θ(f)) ∈ Ω for all f ∈ B', and with B → B' universally injective, there is a map of complexes e_M^• : (M ⊗_B B') ⊗_{B'} (Ω')^• ⟶ M ⊗_B Ω^• such that c_M^• ∘ e_M^• and e_M^• ∘ c_M^• are both homotopic to multiplication by a.

public theorem exists_homotopyInverse_baseChangeDeRhamMap
    (S : SourceDeRham A B) (S' : SourceDeRham A' B')
    (pi : Ω[B⁄A] →ₗ[B] Omega) (pi' : Ω[B'⁄A'] →ₗ[B'] Omega')
    (hpi : Function.Surjective pi) (hgen : S.GenerationHypothesis pi)
    (hpi' : Function.Surjective pi') (hgen' : S'.GenerationHypothesis pi')
    (psi : Omega →ₛₗ[algebraMap B B'] Omega')
    (hpsi : ∀ b : B, psi (pi (KaehlerDifferential.D A B b)) =
      pi' (KaehlerDifferential.D A' B' (algebraMap B B' b)))
    (nabla : Connection A B pi M)
    (hintegrable : Connection.IsIntegrable S pi hpi hgen nabla)
    (c : ∀ p : ℕ,
      RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)) →ₗ[A]
        RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')))
    (hc_wedge : ∀ (p : ℕ) (m : M) (omega : Fin p → Omega),
      c p (m ⊗ₜ[B] exteriorPower.ιMulti B p omega) =
        (1 ⊗ₜ[B] m) ⊗ₜ[B'] exteriorPower.ιMulti B' p (psi ∘ omega))
    (hc_comm : ∀ (p : ℕ) (x : M ⊗[B] (⋀[B]^p Omega)),
      c (p + 1)
          ((extendedConnection S pi hpi hgen nabla).toLinearMap p x) =
        (extendedConnection S' pi' hpi' hgen'
          (Connection.baseChange psi nabla hpsi)).toLinearMap p (c p x))
    (a : B) (z : B') (theta : B' →ₗ[B] B')
    (dec : DzDecomposition pi' psi z)
    (hd_a_eq_zero : SourceDeRham.targetD pi a = 0)
    (hpartialZ_theta : ∀ f : B', dec.partialZ (theta f) = a • f)
    (huniv :
      Stacks.UniversalInjectivity.LocalizationCriteria.UniversallyInjective.{max u w}
        (Algebra.linearMap B B'))
    (hepsilon : ∀ f : B',
      a • f - theta (dec.partialZ f) ∈ Set.range (algebraMap B B'))
    (hepsilonPrime : ∀ f : B',
      TensorProduct.map theta (LinearMap.id (R := B) (M := Omega)) (dec.dOne f) -
          dec.dOne (theta f) ∈
        LinearMap.range (TensorProduct.mk B B' Omega 1)) :
    ∃ e : ∀ p : ℕ,
      RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')) →ₗ[A]
        RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)),
      (∀ (p : ℕ) (x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega'))),
          e (p + 1)
              ((extendedConnection S' pi' hpi' hgen'
                (Connection.baseChange psi nabla hpsi)).toLinearMap
                p x) =
            (extendedConnection S pi hpi hgen nabla).toLinearMap
              p (e p x)) ∧
        (∃ h : ∀ p : ℕ,
            RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega')) →ₗ[A]
              RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^p Omega')),
          (∀ x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^0 Omega')),
              h 0 ((extendedConnection S' pi' hpi' hgen'
                (Connection.baseChange psi nabla hpsi)).toLinearMap
                0 x) =
                RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^0 Omega'))
                    (algebraMap B B' a) x -
                  c 0 (e 0 x)) ∧
            ∀ (p : ℕ)
                (x : RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))),
              (show RestrictScalars A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega')) from
                (extendedConnection S' pi' hpi' hgen'
                  (Connection.baseChange psi nabla hpsi)).toLinearMap
                    p (h p x)) +
                  h (p + 1)
                    ((extendedConnection S' pi' hpi' hgen'
                      (Connection.baseChange psi nabla hpsi)).toLinearMap
                      (p + 1) x) =
                RestrictScalars.lsmul A B' ((B' ⊗[B] M) ⊗[B'] (⋀[B']^(p + 1) Omega'))
                    (algebraMap B B' a) x -
                  c (p + 1) (e (p + 1) x)) ∧
        (∃ k : ∀ p : ℕ,
            RestrictScalars A B (M ⊗[B] (⋀[B]^(p + 1) Omega)) →ₗ[A]
              RestrictScalars A B (M ⊗[B] (⋀[B]^p Omega)),
          (∀ x : RestrictScalars A B (M ⊗[B] (⋀[B]^0 Omega)),
              k 0 ((extendedConnection S pi hpi hgen nabla).toLinearMap
                0 x) =
                RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^0 Omega)) a x - e 0 (c 0 x)) ∧
            ∀ (p : ℕ) (x : RestrictScalars A B (M ⊗[B] (⋀[B]^(p + 1) Omega))),
              (extendedConnection S pi hpi hgen nabla).toLinearMap
                  p (k p x) +
                k (p + 1)
                  ((extendedConnection S pi hpi hgen nabla).toLinearMap
                    (p + 1) x) =
                RestrictScalars.lsmul A B (M ⊗[B] (⋀[B]^(p + 1) Omega)) a x -
                  e (p + 1) (c (p + 1) x))
Tag 07Q8, an example

Tag 07Q8 in the Stacks Project.

Crystalline.oneVariableTheta_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/RelativePoincare.lean, line 1030. The attribute's comment: “the operator θ”.

The operator θ of Example 07Q8. It raises the divided power degree of the variable by one in every term of the divided power monomial expansion: θ(∑ bₘ z^[m]) = ∑ bₘ z^[m+1].

public theorem oneVariableTheta_apply (f : oneVariableDividedPowerPolynomial B) :
    oneVariableTheta B f =
      ((oneVariableMonomialBasis B).repr f).sum fun m b =>
        b • (oneVariableDividedPowers B).dpow (m + 1) (oneVariableVariable B)

Crystalline.oneVariable_sub_theta_partialZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/RelativePoincare.lean, line 1058. The attribute's comment: “f - θ(∂_z f) = f(0)”.

Assumption (6) of Section 60.25 at a = 1, in sharp form. The difference f - θ(∂_z(f)) is the constant term f(0) of f, the image under B → B⟨z⟩ of the augmentation of f.

public theorem oneVariable_sub_theta_partialZ (f : oneVariableDividedPowerPolynomial B) :
    f - oneVariableTheta B (oneVariablePartialZ A B f) =
      algebraMap (B : Type u) (oneVariableDividedPowerPolynomial B)
        (dividedPowerPolynomialAugmentation (B : Type u) Unit f)

Crystalline.oneVariableDividedPowerPolynomial_standingAssumptions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/RelativePoincare.lean, line 1087. The attribute's comment: “the seven standing assumptions for B⟨z⟩ at a = 1”.

Example 07Q8, the verification of the standing assumptions. For a divided power ring (B, J, δ) over A, the divided power polynomial ring B' = B⟨z⟩ with its divided powers on J' = B'₊ + JB', the quotients Ω = Ω¹_{B/A,δ} and Ω' = Ω¹_{B'/A,δ'}, the element a = 1 and the operator θ of Crystalline.oneVariableTheta satisfy the seven standing assumptions of Section 60.25: d(1) = 0, the decomposition Ω' = (B' ⊗_B Ω) ⊕ B' dz, B-linearity of θ, ∂_z ∘ θ = 1, universal injectivity of B → B', f - θ(∂_z(f)) ∈ B, and (θ ⊗ 1)(d₁(f)) - d₁(θ(f)) ∈ Ω.

public theorem oneVariableDividedPowerPolynomial_standingAssumptions :
    ∃ dec : DzDecomposition (oneVariablePolyProjection A B)
      (dividedPowerPolynomialOneFormComparison A B) (oneVariableVariable B),
      SourceDeRham.targetD (oneVariableBaseProjection A B) (1 : (B : Type u)) = 0 ∧
      (∀ f : oneVariableDividedPowerPolynomial B,
        dec.partialZ (oneVariableTheta B f) = (1 : (B : Type u)) • f) ∧
      Stacks.UniversalInjectivity.LocalizationCriteria.UniversallyInjective.{v}
        (Algebra.linearMap (B : Type u) (oneVariableDividedPowerPolynomial B)) ∧
      (∀ f : oneVariableDividedPowerPolynomial B,
        (1 : (B : Type u)) • f - oneVariableTheta B (dec.partialZ f) ∈
          Set.range (algebraMap (B : Type u) (oneVariableDividedPowerPolynomial B))) ∧
      (∀ f : oneVariableDividedPowerPolynomial B,
        TensorProduct.map (oneVariableTheta B)
            (LinearMap.id (R := (B : Type u))
              (M := dividedPowerDifferentials (A := A) B.dividedPowers)) (dec.dOne f) -
            dec.dOne (oneVariableTheta B f) ∈
          LinearMap.range (TensorProduct.mk (B : Type u)
            (oneVariableDividedPowerPolynomial B)
            (dividedPowerDifferentials (A := A) B.dividedPowers) 1))

Crystalline.exists_homotopyEquiv_oneVariableDeRhamComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/RelativePoincare.lean, line 1131. The attribute's comment: “Lemma 07Q7 at a = 1 for B⟨z⟩”.

Example 07Q8, the conclusion. Let (B, J, δ) be a divided power ring which is an A-algebra, let B⟨z⟩ be the divided power polynomial ring on one divided power variable, and let M carry an integrable connection ∇ : M → M ⊗_B Ω¹_{B/A,δ}. Then the canonical map of de Rham complexes c_M^• : M ⊗_B Ω^*_{B/A,δ} ⟶ M ⊗_B Ω^*_{B⟨z⟩/A,δ'} is a homotopy equivalence.

public theorem exists_homotopyEquiv_oneVariableDeRhamComparison
    (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)
    (c : ∀ p : ℕ, oneVariableSourceTerm A B M p →ₗ[A] oneVariableTargetTerm A B M p)
    (hc_wedge : ∀ (p : ℕ) (m : M)
        (omega : Fin p → dividedPowerDifferentials (A := A) B.dividedPowers),
      c p (m ⊗ₜ[(B : Type u)] exteriorPower.ιMulti (B : Type u) p omega) =
        ((1 : oneVariableDividedPowerPolynomial B) ⊗ₜ[(B : Type u)] m) ⊗ₜ[
          oneVariableDividedPowerPolynomial B]
          exteriorPower.ιMulti (oneVariableDividedPowerPolynomial B) p
            (dividedPowerPolynomialOneFormComparison A B ∘ omega))
    (hc : ∀ (p : ℕ) (x : oneVariableSourceTerm A B M p),
      c (p + 1) ((extendedConnection (oneVariableBaseSource A B)
            (oneVariableBaseProjection A B) (Submodule.mkQ_surjective _)
            (oneVariableBaseGenerationHypothesis A B) nabla).toLinearMap p x) =
        (extendedConnection (oneVariablePolySource A B) (oneVariablePolyProjection A B)
          (Submodule.mkQ_surjective _) (oneVariablePolyGenerationHypothesis A B)
          (oneVariableBaseChangeConnection A B nabla)).toLinearMap p (c p x)) :
    ∃ E : HomotopyEquiv (oneVariableSourceDeRhamComplex A B nabla hint)
        (oneVariableTargetDeRhamComplex A B nabla hint),
      E.hom = oneVariableDeRhamComparison A B nabla hint c hc
Tag 07N1, a lemma

Tag 07N1 in the Stacks Project.

Crystalline.PthRootExtension.exists_homotopyInverse_completedPthRootExtension_situation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/Differentials/PthRootCompletedSituation.lean, line 74. The attribute's comment: “in Situation 07MD with D the completed divided power envelope of 07J8 and the completed forms of 07J9; for every completed connection integrable in the sense of 07I0”.

[Stacks, Lemma 60.25.3, Tag 07N1].

In Situation 07MD (s), let P = A[x_i] → C be a surjective polynomial presentation (f, hf), let D be the p-adic completion of the divided power envelope D_{P,γ}(ker f) with its divided powers γ̄ (07J8, [Stacks, Tag 07KG]), and let Ω^q_D be the p-adic completion of the divided power forms of D over A (07J9, in its second form Ω_D = lim_e Ω_{D/A,γ̄}/p^e). Let λ ∈ D, let D' be the p-adic completion of D[z]⟨ξ⟩/(ξ - (z^p - λ)) with the divided powers of [Stacks, Tag 07KD], and let Ω^q_{D'} be the p-adic completion of the divided power forms of D' over A. Let M be a D-module with a connection ∇ : M → M ⊗̂_D Ω_D (07JC), integrable (07JD) in the sense of [Stacks, Remark 60.6.1, Tag 07I0]: the composite M → M ⊗̂ Ω¹ → M ⊗̂ Ω² vanishes. Then:

  • M ⊗^∧_D Ω^•_D and M ⊗^∧_D Ω^•_{D'} are complexes;
  • the canonical map c_M^• : M ⊗^∧_D Ω^•_D → M ⊗^∧_D Ω^•_{D'} of (07PY) is a map of complexes;
  • there is a map of complexes e_M^• in the opposite direction with e_M^• ∘ c_M^• = p, so that e_M^• ∘ c_M^• is homotopic to p (by the zero homotopy), and a homotopy h with h d = p - c_M^• ∘ e_M^• in degree 0 and d h + h d = p - c_M^• ∘ e_M^• in positive degrees, so that c_M^• ∘ e_M^• is homotopic to p; moreover h ∘ c_M^• = 0.

The hypotheses (07JB), completeness of M, and (07JE), quasi-nilpotence of ∇, are not needed and are not assumed.

theorem exists_homotopyInverse_completedPthRootExtension_situation
    (lam : (𝒟 : Type u)) (M : Type u) [AddCommGroup M] [Module (𝒟 : Type u) M]
    (nabla : CompletedConnection s.p (𝒟 : Type u)
      (completedDividedPowerForms s.p (s.A : Type u) (𝒟).dividedPowers 1)
      (completedDividedPowerDifferentialOnRing s.p (s.A : Type u) (𝒟).dividedPowers) M)
    (hint : IsCompletedIntegrable s.p (s.A : Type u) (𝒟 : Type u) (𝒟).dividedPowers M nabla) :
    CompletedDeRham.IsSquareZero s.p (𝒟 : Type u) (completedDividedPowerForms s.p (s.A : Type u)
        (𝒟).dividedPowers)
        (completedDividedPowerWedgeOnRing s.p (s.A : Type u) (𝒟).dividedPowers)
        (completedDividedPowerDeRham s.p (s.A : Type u) (𝒟).dividedPowers) M nabla
        (isGradedLeibniz_completedDividedPowerOnRing s.p (s.A : Type u) (𝒟).dividedPowers) ∧
      CompletedDeRham.IsSquareZero s.p (completedPrimeRingSelf 𝒟 s.p lam)
        (completedDividedPowerForms s.p (s.A : Type u)
          (completedPrimeDividedPowers 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf)))
        (completedDividedPowerWedgeOnRing s.p (s.A : Type u)
          (completedPrimeDividedPowers 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf)))
        (completedDividedPowerDeRham s.p (s.A : Type u)
          (completedPrimeDividedPowers 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf)))
        (genuineCarrier 𝒟 s.p lam M)
        (genuineCompletedConnection (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M nabla)
        (isGradedLeibniz_completedDividedPowerOnRing s.p (s.A : Type u) _) ∧
      (∀ q : ℕ, (genuineCompletedDifferential (s.A : Type u) 𝒟 s.p lam (Fact.out :
          s.p.Prime).ne_zero
          (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M nabla
          q).comp (genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out :
              s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M q) =
        (genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M (q + 1)).comp
          (baseCompletedDifferential (s.A : Type u) 𝒟 s.p M nabla q)) ∧
      ∃ (e : ∀ q : ℕ, genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
          (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M q →+
          baseCompletedTerm (s.A : Type u) 𝒟 s.p M q)
        (h : ∀ q : ℕ, genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M (q + 1) →+
          genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M q),
        (∀ (q : ℕ) (y : genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M q),
          e (q + 1) (genuineCompletedDifferential (s.A : Type u) 𝒟 s.p lam (Fact.out :
              s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M
            nabla q y) = baseCompletedDifferential (s.A : Type u) 𝒟 s.p M nabla q (e q y)) ∧
        (∀ (q : ℕ) (x : baseCompletedTerm (s.A : Type u) 𝒟 s.p M q),
          e q (genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M q x) =
            s.p • x) ∧
        (∀ y : genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M 0,
          h 0 (genuineCompletedDifferential (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M nabla 0
            y) = s.p • y - genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out :
                s.p.Prime).ne_zero
                (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M 0
              (e 0 y)) ∧
        (∀ (q : ℕ) (y : genuineCompletedTerm (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
            (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M
            (q + 1)),
          genuineCompletedDifferential (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M nabla q
              (h q y) +
            h (q + 1) (genuineCompletedDifferential (s.A : Type u) 𝒟 s.p lam (Fact.out :
                s.p.Prime).ne_zero
                (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M
              nabla (q + 1) y) =
            s.p • y - genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out :
                s.p.Prime).ne_zero
                (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M
              (q + 1) (e (q + 1) y)) ∧
        (∀ (q : ℕ) (x : baseCompletedTerm (s.A : Type u) 𝒟 s.p M (q + 1)),
          h q (genuineCompletedComparison (s.A : Type u) 𝒟 s.p lam (Fact.out : s.p.Prime).ne_zero
              (completedEnvelopeOfPresentation_prime_nilpotent s f hf) M (q + 1)
            x) = 0)
Tag 07Q9, a lemma

Tag 07Q9 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.annihilation07Q9_of_isIteratedAlphaPCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/AlphaPCover07Q9Main.lean, line 114. The attribute's comment: “for an iterated α_p-cover f : X' → X over S_0 of constant degree q and a crystal in quasi-coherent modules F on Cris(X/S), with F' = f_cris^ F, the cone E of Ru_{X/S,}F → f_ Ru_{X'/S,}F' has all cohomology sheaves annihilated by q”.

Stacks Project, Lemma 60.26.3, Tag 07Q9. Let p = T.p be the prime of the global crystalline situation T, whose divided power scheme (S, 𝓘, γ) lies over ℤ_(p), and assume p ∈ 𝓘 (hpI). Let f : X' ⟶ X be an iterated α_p-cover (hf) of schemes over S₀ = V(𝓘) — X' lies over S₀ through f, which is the situation overSituation T f — of constant degree q (hq). Let ℱ be a crystal in quasi-coherent sheaves on Cris(X/S) (hF) and ℱ' = f_cris^*ℱ (crisModuleInverseImage of ℱ). Then in every distinguished triangle

Ru_{X/S, *}ℱ ⟶ f_*Ru_{X'/S, *}ℱ' ⟶ E ⟶ Ru_{X/S, *}ℱ[1]

on the canonical map moduleComparison07Q9 (in the derived category of abelian sheaves on X; f_* is the derived direct image of the Zariski topoi, which is f_* since f is a homeomorphism), the object E has every cohomology sheaf annihilated by q (Annihilation07Q9).

The hypothesis p ∈ 𝓘 of the source is stated; the argument only uses that p is nilpotent on X, which every global crystalline situation carries.

theorem annihilation07Q9_of_isIteratedAlphaPCover
    (hpI : (T.p : Γ(T.S.scheme, ⊤)) ∈ T.S.ideal.obj (op ⊤)) {q : ℕ}
    (hf : IsIteratedAlphaPCover T.p f) (hq : HasConstantDegree f q)
    (F : SheafOfModules.{u} (structureSheaf T)) (hF : IsQuasiCoherentCrystal T F) :
    Annihilation07Q9 T q
      (moduleComparison07Q9 (overSituation T f) T (𝟙 T.S) f (overSituation_compat T f)
        ((moduleULift T).obj F))
Tag 07QA, a lemma

Tag 07QA in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.annihilated_ker_coker_crisModuleCohomologyMap_of_isIteratedAlphaPCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/CrisCohomologyBound07QAMain.lean, line 84. The attribute's comment: “f^* : H^i(Cris(X/S), F) → H^i(Cris(X'/S), F') has kernel and cokernel annihilated by q^(i+1)”.

Let p be a prime and (S, I, γ) a divided power scheme over ℤ_(p) with p ∈ I (the prime, the ℤ_(p)-structure of the base and the local nilpotence of p on X are part of the situation T; p ∈ I is hpI), S₀ = V(I). Let f : X' ⟶ X be an iterated α_p-cover of schemes over S₀ of constant degree q, ℱ a crystal in quasi-coherent modules on Cris(X/S) and ℱ' = f_cris^*ℱ. Then the kernel and the cokernel of

f^* : H^i(Cris(X/S), ℱ) ⟶ H^i(Cris(X'/S), ℱ')

are annihilated by q^{i + 1}: every class killed by f^* is killed by q^{i + 1}, and q^{i + 1} times every class of H^i(Cris(X'/S), ℱ') lies in the image of f^*.

theorem annihilated_ker_coker_crisModuleCohomologyMap_of_isIteratedAlphaPCover
    (hpI : (T.p : Γ(T.S.scheme, ⊤)) ∈ T.S.ideal.obj (op ⊤)) (q : ℕ)
    (hf : IsIteratedAlphaPCover T.p f) (hq : HasConstantDegree f q)
    (F : SheafOfModules.{u} (structureSheaf T)) (hF : IsQuasiCoherentCrystal T F)
    [HasDerivedCategory.{w} (Sheaf (smallTopology (overSituation T f)) AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w} (Sheaf (smallTopology T) AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} (Sheaf (opensTopology (overSituation T f)) AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} (Sheaf (opensTopology T) AddCommGrpCat.{u + 1})]
    [HasDerivedCategory.{w'} AddCommGrpCat.{u + 1}] (i : ℕ) :
    (∀ x, crisModuleCohomologyMap (overSituation T f) T (𝟙 T.S) f (overSituation_compat T f)
        ((moduleULift T).obj F) i x = 0 → ((q : ℤ) ^ (i + 1)) • x = 0) ∧
      ∀ y, ∃ x, ((q : ℤ) ^ (i + 1)) • y =
        crisModuleCohomologyMap (overSituation T f) T (𝟙 T.S) f (overSituation_compat T f)
          ((moduleULift T).obj F) i x
Tag 07QB, a lemma

Tag 07QB in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.relativeFrobeniusToTwist_isIteratedAlphaPCover_cohomologyBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/AlphaPCoverRelativeFrobenius07QB.lean, line 204. The attribute's comment: “for the global crystalline situation with p in I and X -> S_0 smooth of relative dimension d: F_{X/S_0} : X -> X^{(1)} is an iterated alpha_p-cover of degree p ^ d, and for every crystal in quasi-coherent modules G on Cris(X^{(1)}/S) and every i the map F_{X/S_0}^ : H^i(Cris(X^{(1)}/S), G) -> H^i(Cris(X/S), F_{X/S_0,cris}^ G) has kernel and cokernel annihilated by p^{d(i+1)}”.

[Stacks, Lemma 60.26.5, Tag 07QB]. In the global crystalline situation X/S of [Stacks, Tag 07MF] with p in the divided power ideal I, let S₀ = V(I), X^{(1)} = X ×_{S₀, F_{S₀}} S₀ and F_{X/S₀} : X ⟶ X^{(1)} the relative Frobenius, and assume that X ⟶ S₀ is smooth of relative dimension d. Then

  • F_{X/S₀} is an iterated α_p-cover of degree p ^ d, and
  • for every crystal in quasi-coherent modules 𝒢 on Cris(X^{(1)}/S) and every i, the map F_{X/S₀}^* : H^i(Cris(X^{(1)}/S), 𝒢) ⟶ H^i(Cris(X/S), F_{X/S₀, cris}^*𝒢) has kernel and cokernel annihilated by p^{d(i + 1)}.

The first assertion is Crystalline.GlobalCrystallineSituation.isIteratedAlphaPCoverOfDegree_relativeFrobeniusToTwist. The second is [Stacks, Lemma 60.26.4, Tag 07QA] (...SmallSite.annihilated_ker_coker_crisModuleCohomologyMap_of_isIteratedAlphaPCover) applied to f = F_{X/S₀} and q = p ^ d, whose two hypotheses on f are the first assertion, read on X/S by zsmul_id_kernel_cokernel_crisModuleCohomologyMap_relativeFrobeniusToTwist_of. The map is ...SmallSite.crisModuleCohomologyMap for the morphism F_{X/S₀} of situations over the identity of S, and F_{X/S₀, cris}^* is the pullback ...SmallSite.crisModuleInverseImage of 𝒪-modules; 𝒢 enters through ...SmallSite.moduleULift, at the module universe of the cohomology of Cris(X^{(1)}/S).

theorem relativeFrobeniusToTwist_isIteratedAlphaPCover_cohomologyBound (d : ℕ)
    [SmoothOfRelativeDimension d T.toClosedFiber] :
    (IsIteratedAlphaPCover T.p (T.relativeFrobeniusToTwist hp) ∧
        HasConstantDegree (T.relativeFrobeniusToTwist hp) (T.p ^ d)) ∧
      ∀ (G : SheafOfModules.{u} (structureSheaf (T.frobeniusTwistSituation hp))),
        IsQuasiCoherentCrystal (T.frobeniusTwistSituation hp) G → ∀ i : ℕ,
          ((T.p : ℤ) ^ (d * (i + 1))) • 𝟙 (kernel (crisModuleCohomologyMap T
              (T.frobeniusTwistSituation hp) (𝟙 T.S) (T.relativeFrobeniusToTwist hp)
              (T.toClosedFiber_comp_closedFiberMap_id hp)
              ((moduleULift (T.frobeniusTwistSituation hp)).obj G) i)) = 0 ∧
            ((T.p : ℤ) ^ (d * (i + 1))) • 𝟙 (cokernel (crisModuleCohomologyMap T
              (T.frobeniusTwistSituation hp) (𝟙 T.S) (T.relativeFrobeniusToTwist hp)
              (T.toClosedFiber_comp_closedFiberMap_id hp)
              ((moduleULift (T.frobeniusTwistSituation hp)).obj G) i)) = 0
Sources
LeanCrystalline.DzDecomposition · Crystalline.DzDecomposition.dOne · Crystalline.DzDecomposition.partialZ · Crystalline.DzDecomposition.dOne_add_partialZ_smul · Crystalline.exists_homotopyInverse_baseChangeDeRhamMap_baseLinear · Crystalline.exists_homotopyInverse_baseChangeDeRhamMap · Crystalline.oneVariableTheta_apply · Crystalline.oneVariable_sub_theta_partialZ

Section60.26 Frobenius action on crystalline cohomology#

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

Tag 07N2, a situation

Tag 07N2 in the Stacks Project.

Crystalline.FCrystalSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FrobeniusCrystalSituation.lean, line 44.

A global crystalline situation over an affine divided power base, with the distinguished prime in its divided power ideal and a divided power endomorphism of the base ring lifting the absolute Frobenius modulo that prime.

See Stacks Project, Tag 07N2.

public structure FCrystalSituation
Tag 07N3, a definition

Tag 07N3 in the Stacks Project.

Crystalline.FCrystal, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FCrystal.lean, line 446. The attribute's comment: “F-crystal”.

Stacks Project, Tag 07N3. An F-crystal on X/S relative to σ: a crystal in finite locally free 𝒪_{X/S}-modules E together with a map F_E : (F_X)_cris^* E ⟶ E.

The crystal in finite locally free modules is the notion of [Stacks, Tag 07IU], Crystalline.GlobalCrystallineSituation.IsFiniteLocallyFreeQuasicoherentCrystal: quasi-coherence — condition (1) of [Stacks, Tag 07IT], the form in which this library reads the source's "crystal in quasi-coherent modules" — together with finite local freeness. It is not the stronger Crystalline.GlobalCrystallineSituation.IsFiniteLocallyFreeCrystal, which reads the crystal condition with the comparison maps of presheaves of modules; see the module documentation.

structure FCrystal (T : FCrystalSituation.{u})

Crystalline.FCrystal.Nondegenerate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FCrystal.lean, line 459. The attribute's comment: “nondegenerate”.

Stacks Project, Tag 07N3. An F-crystal is nondegenerate when there are an integer i ≥ 0 and a map V : E ⟶ (F_X)_cris^* E with V ∘ F_E = p ^ i, the composite being taken diagrammatically as F_E ≫ V, an endomorphism of (F_X)_cris^* E, and the scalar p ^ i acting through the ℕ-action on morphisms.

def FCrystal.Nondegenerate {T : FCrystalSituation.{u}} (E : FCrystal T) : Prop
Tag 07N4, a remark

Tag 07N4 in the Stacks Project.

Matrix.det_mul_det_and_two_sided_of_mul_eq_pow_smul_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FrobeniusNondegeneracy.lean, line 202. The attribute's comment: “the matrix computation: for r × r matrices K, L over a ring R with K L = p ^ i 1, det(K) det(L) = p ^ (r i), the adjugate L' of L satisfies L' L = L L' = det(L) 1, and K' = p ^ (r i) K satisfies K' L = p ^ j 1 and L K' = p ^ j 1 for j = r i + i”.

The matrix computation of [Stacks, Tag 07N4]. Let R be a commutative ring, r an integer and K, L two r × r matrices over R with K L = pⁱ 1. Then:

  • det(K) det(L) = p ^ (r i);
  • the adjugate L' of L satisfies L' L = L L' = det(L) 1;
  • K' = p ^ (r i) K satisfies K' L = p ^ j 1 and L K' = p ^ j 1, where j = r i + i.

The second-sided identity L K' = p ^ j 1 is the content: it is obtained, as in the source, from the adjugate and the determinant identity. The element p is arbitrary, and r ≥ 1 is not needed.

theorem det_mul_det_and_two_sided_of_mul_eq_pow_smul_one {r : ℕ}
    {K L : Matrix (Fin r) (Fin r) R} {p : R} {i : ℕ}
    (h : K * L = p ^ i • (1 : Matrix (Fin r) (Fin r) R)) :
    K.det * L.det = p ^ (r * i) ∧
      (L.adjugate * L = L.det • (1 : Matrix (Fin r) (Fin r) R) ∧
        L * L.adjugate = L.det • (1 : Matrix (Fin r) (Fin r) R)) ∧
      (p ^ (r * i) • K) * L = p ^ (r * i + i) • (1 : Matrix (Fin r) (Fin r) R) ∧
      L * (p ^ (r * i) • K) = p ^ (r * i + i) • (1 : Matrix (Fin r) (Fin r) R)

Crystalline.FCrystal.nsmul_two_sided_of_rankLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FrobeniusNondegeneracyBoundedRank.lean, line 97. The attribute's comment: “for an F-crystal (E, F) whose rank is bounded by rmax and V as in Definition 07N3 with V ∘ F = p ^ i id, the map V' = p ^ N V with N ≥ rmax * i satisfies V' ∘ F = p ^ (N + i) id and F ∘ V' = p ^ (N + i) id”.

The last sentence of [Stacks, Tag 07N4]. Let (E, F_E) be an F-crystal whose rank is bounded by rmax, and let V be as in [Stacks, Tag 07N3], F_E ≫ V = p ^ i • 𝟙, that is V ∘ F_E = p ^ i • id. Setting V' = p ^ N • V with N ≥ rmax * i gives both V' ∘ F_E = p ^ (N + i) • id and F_E ∘ V' = p ^ (N + i) • id; in diagrammatic order these are F_E ≫ V' = p ^ (N + i) • 𝟙 and V' ≫ F_E = p ^ (N + i) • 𝟙.

theorem FCrystal.nsmul_two_sided_of_rankLE
    (hE : AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRankLE
      (crystallineRingedSite T.global) E.crystal rmax)
    {V : E.crystal ⟶ T.frobeniusModulePullback.obj E.crystal}
    (hV : E.frobenius ≫ V = (T.global.p ^ i) • 𝟙 (T.frobeniusModulePullback.obj E.crystal))
    (hN : rmax * i ≤ N) :
    E.frobenius ≫ ((T.global.p ^ N) • V) =
        (T.global.p ^ (N + i)) • 𝟙 (T.frobeniusModulePullback.obj E.crystal) ∧
      ((T.global.p ^ N) • V) ≫ E.frobenius = (T.global.p ^ (N + i)) • 𝟙 E.crystal

Crystalline.FCrystal.nondegenerate_conditions_of_rankLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FrobeniusNondegeneracyBoundedRank.lean, line 170. The attribute's comment: “if the rank of E is bounded, both conditions follow from the nondegeneracy condition of Definition 07N3: there is V' with V' ∘ F = p ^ n id and F ∘ V' = p ^ n id, and there is j ≥ 0 such that Ker(F) and Coker(F) are killed by p ^ j”.

[Stacks, Tag 07N4]: for an F-crystal of bounded rank, both conditions follow from nondegeneracy. Let (E, F) be an F-crystal as in [Stacks, Tag 07N3] whose rank is bounded by rmax. If E is nondegenerate, that is V ∘ F = p ^ i • id for some i ≥ 0 and some V : E ⟶ (F_X)_cris^* E, then

  • there are n and V' with V' ∘ F = p ^ n • id and F ∘ V' = p ^ n • id, the condition often assumed in the literature, and
  • there is an integer j ≥ 0 such that Ker(F) and Coker(F) are killed by p ^ j, the condition needed for [Stacks, Tag 07N5].

The kernel and the cokernel are described by their universal properties: every map into (F_X)_cris^* E which F sends to zero, and every map out of E which kills the image of F, is killed by p ^ j.

theorem FCrystal.nondegenerate_conditions_of_rankLE
    (hE : AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRankLE
      (crystallineRingedSite T.global) E.crystal rmax) (hnd : E.Nondegenerate) :
    (∃ (n : ℕ) (V' : E.crystal ⟶ T.frobeniusModulePullback.obj E.crystal),
        E.frobenius ≫ V' = (T.global.p ^ n) • 𝟙 (T.frobeniusModulePullback.obj E.crystal) ∧
          V' ≫ E.frobenius = (T.global.p ^ n) • 𝟙 E.crystal) ∧
      ∃ j : ℕ,
        (∀ (Q : SheafOfModules.{u} (crystallineStructureSheaf T.global))
          (q : Q ⟶ T.frobeniusModulePullback.obj E.crystal),
          q ≫ E.frobenius = 0 → (T.global.p ^ j) • q = 0) ∧
        (∀ (Q : SheafOfModules.{u} (crystallineStructureSheaf T.global))
          (q : E.crystal ⟶ Q), E.frobenius ≫ q = 0 → (T.global.p ^ j) • q = 0)

Crystalline.FCrystal.exists_isFiniteLocallyFreeOfRankLE_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/FrobeniusNondegeneracyBoundedRank.lean, line 314. The attribute's comment: “the rank of E is bounded if X is quasi-compact”.

If X is quasi-compact, there is an integer rmax such that every object of CRIS(X/S) has a covering on each member of which E is a direct sum of at most rmax copies of 𝒪_{X/S}.

theorem FCrystal.exists_isFiniteLocallyFreeOfRankLE_of_compactSpace [CompactSpace T.global.X] :
    ∃ rmax : ℕ, AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRankLE
      (crystallineRingedSite T.global) E.crystal rmax
Tag 07N5, a theorem

Tag 07N5 in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.statement07N5, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/Frobenius07N5Theorem.lean, line 271. The attribute's comment: “the theorem: for a nondegenerate F-crystal over a p-adically complete Noetherian A with X -> S_0 proper smooth, the canonical map F_E o (F_X)_cris^* on RGamma(Cris(X/S), E) becomes an isomorphism after inverting p”.

[Stacks, Tag 07N5]. In Situation [Stacks, Tag 07N2] let (E, F_E) be a nondegenerate F-crystal. Assume A is a p-adically complete Noetherian ring and that X → S₀ is proper smooth. Then the canonical map

F_E ∘ (F_X)^*_cris : RΓ(Cris(X/S), E) ⊗^L_{A, σ} A ⟶ RΓ(Cris(X/S), E)

becomes an isomorphism after inverting p.

The conclusion is ...SmallSite.Statement07N5 at ...SmallSite.frobeniusMap07N5Canonical, the canonical F_E ∘ (F_X)^*_cris, and its standing hypotheses — A Noetherian, A p-adically complete, X ⟶ S₀ proper, X ⟶ S₀ smooth, E an F-crystal, E nondegenerate — are the tag's own.

The proof is the source's. The map of the theorem is the composite of the three arrows (frobeniusMap07N5Canonical_eq_comp). Arrow 1 is an isomorphism (...SmallSite.isIso_baseChangeArrow07QC, from [Stacks, Tag 07MU] and [Stacks, Tag 07MY]); arrow 2 is an isogeny (becomesIsoAfterInvertingPrime_relativeFrobeniusArrow07N6, from [Stacks, Tag 07QB]), so arrows 1 and 2 together are an isogeny (becomesIsoAfterInvertingPrime_baseChangeArrow07QC_comp); arrow 3 is an isogeny by nondegeneracy (...SmallSite.becomesIsoAfterInvertingPrime_frobeniusCohomologyMap, [Stacks, Tag 07N4], with the rank bound exists_hasBoundedCommonLocalRank_of_isProper); and the three combine by ...SmallSite.becomesIsoAfterInvertingPrime_iff_of_factors.

theorem statement07N5 : Statement07N5 T (frobeniusMap07N5Canonical T)
Sources
LeanCrystalline.FCrystalSituation · Crystalline.FCrystal · Crystalline.FCrystal.Nondegenerate · Matrix.det_mul_det_and_two_sided_of_mul_eq_pow_smul_one · Crystalline.FCrystal.nsmul_two_sided_of_rankLE · Crystalline.FCrystal.nondegenerate_conditions_of_rankLE · Crystalline.FCrystal.exists_isFiniteLocallyFreeOfRankLE_of_compactSpace · Crystalline.GlobalCrystallineSituation.SmallSite.statement07N5

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.