Documentation

TauCeti.AlgebraicGeometry.AdicSpace.FarguesFontaine.WindowSections

Sections of π’ͺ_𝒳 over the image of a wandering open #

Let q : 𝒴 β†’ 𝒳 = 𝒴 / Ο†^β„€ be the projection onto the Frobenius orbit space, and let π’ͺ_𝒳 be its structure presheaf, whose sections over U βŠ† 𝒳 are the Frobenius-invariant sections of π’ͺ_𝒴 over q⁻¹U (TauCeti.FarguesFontaine.spaXPresheaf). An open V βŠ† 𝒴 wanders when it meets none of its nontrivial integer Frobenius translates φ⁻ᡏ V; the Frobenius windows U_n and V_n, and hence all their open subsets, wander. This file shows that over the image of a wandering open, π’ͺ_𝒳 is computed by π’ͺ_𝒴:

π’ͺ_𝒳(q V) β‰… π’ͺ_𝒴(V),

as complete separated topological rings, by restriction, provided π’ͺ_𝒴 is a sheaf. The preimage q⁻¹(q V) is the disjoint union of the translates φ⁻ᡏ V (TauCeti.FarguesFontaine.quotientMap_preimage_image and TauCeti.FarguesFontaine.pairwise_disjoint_preimage_zpow), and Frobenius carries the sections over one translate isomorphically onto those over the next. So a Frobenius-invariant section over q⁻¹(q V) is determined by its restriction to V, and every section over V is such a restriction, glued from its Frobenius transports to the translates. The topologies agree because the topology of a sheaf of topological rings is induced from the product over a cover (TauCeti.TopCommRingCat.isInducing_restrictionMap_of_isSheafFor).

Together with the open embeddings of the windows into 𝒳, this identifies the restriction of π’ͺ_𝒳 to the image of a window with the restriction of π’ͺ_𝒴 to the window, on sections.

Main definitions #

Main results #

References #

Frobenius translates #

Sections over a wandering open #

source
noncomputable def TauCeti.FarguesFontaine.spaXPresheafRestrict {p : β„•} [Fact (Nat.Prime p)] {R : Type v} [CommRing R] [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] {Ο– : R} [IsTopologicalRing (WittVector p R)] (P : Huber.PairOfDefinition (WittVector p R)) (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (V : TopologicalSpace.Opens ↑(spaY p Ο–)) :
(spaXPresheaf P hI).obj (Opposite.op (β‹―.functor.obj V)) ⟢ (spaYPresheaf P Ο–).obj (Opposite.op V)

Restriction from π’ͺ_𝒳(q V) to π’ͺ_𝒴(V) for an open V βŠ† 𝒴: a section of π’ͺ_𝒳 over the open image q V is a Frobenius-invariant section of π’ͺ_𝒴 over q⁻¹(q V) βŠ‡ V, and this map restricts it to V.

Instances For
    source
    theorem TauCeti.FarguesFontaine.spaXPresheafRestrict_def {p : β„•} [Fact (Nat.Prime p)] {R : Type v} [CommRing R] [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] {Ο– : R} [IsTopologicalRing (WittVector p R)] (P : Huber.PairOfDefinition (WittVector p R)) (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (V : TopologicalSpace.Opens ↑(spaY p Ο–)) :
    spaXPresheafRestrict P hI V = CategoryTheory.CategoryStruct.comp ((spaXPresheafΞΉ P hI).app (Opposite.op (β‹―.functor.1 V))) ((spaYPresheaf P Ο–).map (β‹―.adjunction.unit.app V).op)

    spaXPresheafRestrict is the inclusion π’ͺ_𝒳(q V) β†’ π’ͺ_𝒴(q⁻¹(q V)) followed by restriction to V.

    source
    theorem TauCeti.FarguesFontaine.isIso_spaXPresheafRestrict {p : β„•} [Fact (Nat.Prime p)] {R : Type v} [CommRing R] [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] {Ο– : R} [IsTopologicalRing (WittVector p R)] (P : Huber.PairOfDefinition (WittVector p R)) (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (h : (spaYPresheaf P Ο–).IsSheaf) {V : TopologicalSpace.Opens ↑(spaY p Ο–)} (hV : βˆ€ (k : β„€), k β‰  0 β†’ Disjoint (⇑(frobeniusHomeomorph hI ^ k) ⁻¹' ↑V) ↑V) :
    CategoryTheory.IsIso (spaXPresheafRestrict P hI V)

    Sections of π’ͺ_𝒳 over the image of a wandering open. Let V βŠ† 𝒴 be an open set meeting none of its nontrivial integer Frobenius translates, and suppose that π’ͺ_𝒴 is a sheaf. Then restriction π’ͺ_𝒳(q V) β†’ π’ͺ_𝒴(V) is an isomorphism of complete separated topological rings.

    Indeed q⁻¹(q V) is the disjoint union of the translates φ⁻ᡏ V, and a Frobenius-invariant section over it is the same as a section over V, transported to each translate by Frobenius.

    source
    theorem TauCeti.FarguesFontaine.isIso_spaXPresheafRestrict_of_subset_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type v} [CommRing R] [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] {Ο– : R} [IsTopologicalRing (WittVector p R)] (P : Huber.PairOfDefinition (WittVector p R)) (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (h : (spaYPresheaf P Ο–).IsSheaf) (n : β„€) {V : TopologicalSpace.Opens ↑(spaY p Ο–)} (hV : ↑V βŠ† Subtype.val ⁻¹' windowU p Ο– n) :
    CategoryTheory.IsIso (spaXPresheafRestrict P hI V)

    Sections of π’ͺ_𝒳 over the image of an open inside a U window. If π’ͺ_𝒴 is a sheaf and V βŠ† U_n is open, restriction π’ͺ_𝒳(q V) β†’ π’ͺ_𝒴(V) is an isomorphism of complete separated topological rings.

    source
    theorem TauCeti.FarguesFontaine.isIso_spaXPresheafRestrict_of_subset_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type v} [CommRing R] [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p] {Ο– : R} [IsTopologicalRing (WittVector p R)] (P : Huber.PairOfDefinition (WittVector p R)) (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (h : (spaYPresheaf P Ο–).IsSheaf) (n : β„€) {V : TopologicalSpace.Opens ↑(spaY p Ο–)} (hV : ↑V βŠ† Subtype.val ⁻¹' windowV p Ο– n) :
    CategoryTheory.IsIso (spaXPresheafRestrict P hI V)

    Sections of π’ͺ_𝒳 over the image of an open inside a V window. If π’ͺ_𝒴 is a sheaf and V βŠ† V_n is open, restriction π’ͺ_𝒳(q V) β†’ π’ͺ_𝒴(V) is an isomorphism of complete separated topological rings.