The structure presheaf of the Frobenius orbit space #
Let R be a perfect ring of characteristic p, give the Witt vectors 𝕎 R the (p, [ϖ])-adic
topology, and let 𝒪 be the presentation-limit structure presheaf of Spa(𝕎 R, 𝕎 R) for a pair
of definition P. For R = 𝒪_F this is Spa(A_inf, A_inf). The adic Fargues–Fontaine curve is
the orbit space 𝒳 = 𝒴 / φ^ℤ of the open subset 𝒴 = D(p) ∩ D([ϖ]) under Witt Frobenius, and its
structure presheaf is
𝒪_𝒳(U) = 𝒪_𝒴(q⁻¹U)^{φ=1},
the Frobenius-invariant sections of 𝒪_𝒴 over the preimage of U under the projection
q : 𝒴 → 𝒳. This file constructs it.
𝒪_𝒴is the restriction of𝒪to the open subset𝒴.- Witt Frobenius is an automorphism of the pair
(𝕎 R, 𝕎 R), continuous in both directions, so it acts on𝒪(TauCeti.ValuationSpectrum.presentationLimitPresheafIsoPushforward). Since𝒴is Frobenius-stable this restricts to a morphism𝒪_𝒴 → φ_* 𝒪_𝒴, whose component onV ⊆ 𝒴is𝒪(V) → 𝒪(φ⁻¹V). - Since
q ∘ φ = q, pushing it forward alongqgives an endomorphism ofq_* 𝒪_𝒴, and𝒪_𝒳is its equalizer with the identity, taken in presheaves of complete separated topological rings.
The sections of 𝒪_𝒳 over U form the closed subring of Frobenius-invariant sections of 𝒪_𝒴
over q⁻¹U, with the subspace topology. Equalizers and pushforwards of sheaves are sheaves, so
𝒪_𝒳 is a sheaf as soon as 𝒪_𝒴 is one. Sheafiness of 𝒪_𝒴 is not proved here. In
characteristic p with ϖ not a unit, 𝕎 R is not a Tate ring, so it is not an instance of Tate
acyclicity for Spa(𝕎 R, 𝕎 R); since the sheaf condition is local and the Frobenius windows are
rational subsets covering 𝒴, it suffices to know that 𝒪 is a sheaf on each window. This is how
TauCeti.FarguesFontaine.isSheaf_spaYPresheaf proves it when R is the ring of integers of a
valuation on a field.
Main definitions #
TauCeti.FarguesFontaine.spaYPresheaf: the structure presheaf𝒪_𝒴of𝒴.TauCeti.FarguesFontaine.presentationLimitPresheafFrobeniusIso: the Frobenius action𝒪 ≅ φ_* 𝒪on the structure presheaf ofSpa(𝕎 R, 𝕎 R).TauCeti.FarguesFontaine.presentationLimitPreAdicSpaceFrobeniusIso: Frobenius as an automorphism of the pre-adic spaceSpa(𝕎 R, 𝕎 R), compatible with the stalk valuations.TauCeti.FarguesFontaine.spaYPresheafFrobenius: its restriction𝒪_𝒴 → φ_* 𝒪_𝒴.TauCeti.FarguesFontaine.pushforwardSpaYPresheafFrobenius: the induced endomorphism ofq_* 𝒪_𝒴.TauCeti.FarguesFontaine.spaXPresheaf: the structure presheaf𝒪_𝒳of the orbit space, with its inclusionTauCeti.FarguesFontaine.spaXPresheafιintoq_* 𝒪_𝒴.
Main results #
TauCeti.FarguesFontaine.isIso_spaYPresheafFrobenius_app: each component𝒪_𝒴(V) → 𝒪_𝒴(φ⁻¹V)of Frobenius is an isomorphism, since𝒴is stable under Frobenius in both directions (TauCeti.FarguesFontaine.functor_obj_map_frobeniusTopHom).TauCeti.FarguesFontaine.isLimitSpaXPresheafFork:𝒪_𝒳is the equalizer of the identity and Frobenius onq_* 𝒪_𝒴.TauCeti.FarguesFontaine.isClosedEmbedding_spaXPresheafι_appandTauCeti.FarguesFontaine.range_spaXPresheafι_app: on each openU ⊆ 𝒳, the inclusion𝒪_𝒳(U) → 𝒪_𝒴(q⁻¹U)is a closed embedding onto the Frobenius-invariant sections, andTauCeti.FarguesFontaine.mono_spaXPresheafι_apprecords that it is a monomorphism.TauCeti.FarguesFontaine.isSheaf_spaXPresheaf:𝒪_𝒳is a sheaf when𝒪_𝒴is.
References #
- K. S. Kedlaya, Sheaves, stacks, and shtukas, Arizona Winter School 2017 notes, §3.1.
- P. Scholze and J. Weinstein, Berkeley lectures on p-adic geometry, Lecture 12.
- L. Fargues and J.-M. Fontaine, Courbes et fibrés vectoriels en théorie de Hodge p-adique, Astérisque 406 (2018).
The structure presheaf of 𝒴 #
𝒴 is contained in Spa(𝕎 R, 𝕎 R).
The inclusion of 𝒴 into Spa(𝕎 R, 𝕎 R), as a morphism of topological spaces.
Instances For
The inclusion of 𝒴 into Spa(𝕎 R, 𝕎 R) does not change the underlying valuation.
The inclusion of 𝒴 into Spa(𝕎 R, 𝕎 R) is an open embedding.
The structure presheaf 𝒪_𝒴 of 𝒴: the restriction to the open subset 𝒴 of the
presentation-limit structure presheaf of Spa(𝕎 R, 𝕎 R) for the pair of definition P. Its
sections over an open V ⊆ 𝒴 are those of Spa(𝕎 R, 𝕎 R) over V.
Instances For
The sections of 𝒪_𝒴 over V are the sections of Spa(𝕎 R, 𝕎 R) over V.
Frobenius on 𝒪_𝒴 #
The Frobenius homeomorphism of 𝒴, as a morphism of topological spaces.
Instances For
The projection q : 𝒴 → 𝒳, as a morphism of topological spaces.
Instances For
Frobenius followed by the projection to 𝒳 is the projection.
The image in Spa(𝕎 R, 𝕎 R) of φ⁻¹V lies in the preimage under Frobenius of the image of
V.
The image in Spa(𝕎 R, 𝕎 R) of φ⁻¹V is the preimage under Frobenius of the image of V:
𝒴 is stable under Frobenius in both directions.
Witt Frobenius acting on the structure presheaf of Spa(𝕎 R, 𝕎 R): the isomorphism
𝒪 ≅ φ_* 𝒪 obtained by transporting the presentation-limit presheaf along the automorphism φ of
the pair (𝕎 R, 𝕎 R), where φ acts on points by v ↦ v ∘ φ.
Instances For
Witt Frobenius as an automorphism of the pre-adic space Spa(𝕎 R, 𝕎 R): the isomorphism
in 𝒱^pre induced by the automorphism φ of the pair (𝕎 R, 𝕎 R). On points it is
v ↦ v ∘ φ, on sections it is presentationLimitPresheafFrobeniusIso, and it matches the stalk
valuations: through the Frobenius map of stalks 𝒪_{v ∘ φ} → 𝒪_v, the stalk valuation at v ∘ φ
is the pullback of the stalk valuation at v (TauCeti.PreAdicSpace.Hom.stalkValuation_eq_comap).
No sheaf condition on Spa(𝕎 R, 𝕎 R) is needed.
Instances For
Frobenius acting on 𝒪_𝒴: the morphism 𝒪_𝒴 → φ_* 𝒪_𝒴 whose component on an open
V ⊆ 𝒴 is the map 𝒪(V) → 𝒪(φ⁻¹V) induced by the Witt-vector Frobenius φ, an automorphism of
the pair (𝕎 R, 𝕎 R). Here φ acts on points by v ↦ v ∘ φ.
Instances For
The component of spaYPresheafFrobenius on V ⊆ 𝒴 is that of
presentationLimitPresheafFrobeniusIso on V, followed by restriction from φ⁻¹V computed in
Spa(𝕎 R, 𝕎 R) to φ⁻¹V computed in 𝒴.
Frobenius acts on the sections of 𝒪_𝒴 by isomorphisms: each component 𝒪_𝒴(V) → 𝒪_𝒴(φ⁻¹V)
of spaYPresheafFrobenius is an isomorphism of complete separated topological rings.
Frobenius acting on q_* 𝒪_𝒴: the pushforward along q : 𝒴 → 𝒳 of
spaYPresheafFrobenius, an endomorphism because q ∘ φ = q. Its component on an open U ⊆ 𝒳 is
the map 𝒪_𝒴(q⁻¹U) → 𝒪_𝒴(φ⁻¹q⁻¹U) = 𝒪_𝒴(q⁻¹U) induced by Frobenius.
Instances For
The component of pushforwardSpaYPresheafFrobenius on U ⊆ 𝒳 is the component of
spaYPresheafFrobenius on q⁻¹U, followed by the identification φ⁻¹q⁻¹U = q⁻¹U.
The structure presheaf of 𝒳 #
The structure presheaf 𝒪_𝒳 of the Frobenius orbit space 𝒳 = 𝒴 / φ^ℤ, given on an
open U ⊆ 𝒳 by the Frobenius-invariant sections 𝒪_𝒴(q⁻¹U)^{φ=1}: the equalizer of the identity
and Frobenius on q_* 𝒪_𝒴, in presheaves of complete separated topological rings. The
characterizing API is spaXPresheafι with isLimitSpaXPresheafFork, and on sections
isClosedEmbedding_spaXPresheafι_app with range_spaXPresheafι_app.
Instances For
The inclusion 𝒪_𝒳 → q_* 𝒪_𝒴 of the Frobenius-invariant sections.
Instances For
Sections of 𝒪_𝒳 are Frobenius-invariant.
Sections of 𝒪_𝒳 are Frobenius-invariant.
The universal property of 𝒪_𝒳: with its inclusion into q_* 𝒪_𝒴, it is the equalizer
of the identity and Frobenius.
Instances For
On each open U ⊆ 𝒳, the inclusion 𝒪_𝒳(U) → 𝒪_𝒴(q⁻¹U) is a monomorphism: evaluation at U
preserves the equalizer defining 𝒪_𝒳.
The sections of 𝒪_𝒳 embed in those of 𝒪_𝒴: on each open U ⊆ 𝒳, the inclusion
𝒪_𝒳(U) → 𝒪_𝒴(q⁻¹U) is a closed embedding.
The sections of 𝒪_𝒳 are the Frobenius-invariant sections of 𝒪_𝒴: on each open
U ⊆ 𝒳, the image of 𝒪_𝒳(U) in 𝒪_𝒴(q⁻¹U) consists of the sections fixed by Frobenius.
𝒪_𝒳 is a sheaf when 𝒪_𝒴 is: pushforwards and equalizers of sheaves are sheaves.