Documentation

TauCeti.AlgebraicGeometry.AdicSpace.FarguesFontaine.Quotient

The Frobenius orbit space #

The Witt-vector Frobenius restricts to a homeomorphism of 𝒴 = D(p) ∩ D([Ο–]) when the coefficient ring is perfect of characteristic p and the Witt vectors carry the (p, [Ο–])-adic topology. Its cyclic subgroup acts continuously on 𝒴. The orbit space spaX carries the quotient topology, and its projection is open.

The wandering Frobenius windows embed openly into this orbit space. The images of Uβ‚€ and Vβ‚€ cover it, so it is quasi-compact and T0. These topological charts are the inputs for constructing the quotient sheaf and identifying its affinoid charts.

The adic curve additionally requires a sheaf of complete separated topological rings on this orbit space and identifications of its window charts with affinoid adic spaces.

The construction works over any perfect commutative coefficient ring of characteristic p, with the stated adic topology, and does not require 𝒴 to be nonempty. Nonemptiness for R = π’ͺ_F and a pseudouniformiser Ο– requires a separate construction of a point of 𝒴. The quotient topology and window charts depend only on Frobenius stability and the rational, covering, and wandering properties of the windows.

References #

source
def TauCeti.FarguesFontaine.spaX {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
Type u_1

The topological orbit space 𝒳 = 𝒴 / Ο†^β„€. The acting group is the cyclic subgroup of homeomorphisms generated by Frobenius, so no representative valuation or value group is chosen.

Equations
Instances For
    source
    @[instance_reducible]
    instance TauCeti.FarguesFontaine.topologicalSpaceSpaX {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
    TopologicalSpace (spaX hI)

    The Frobenius orbit space carries the quotient topology from 𝒴.

    Equations
    source
    noncomputable def TauCeti.FarguesFontaine.quotientMap {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
    ↑(spaY p Ο–) β†’ spaX hI

    The projection of 𝒴 to its Frobenius orbit space.

    Equations
    Instances For
      source
      theorem TauCeti.FarguesFontaine.quotientMap_eq_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (v w : ↑(spaY p Ο–)) :
      quotientMap hI v = quotientMap hI w ↔ βˆƒ (n : β„€), (frobeniusHomeomorph hI ^ n) w = v

      Two points have the same image precisely when one is an integer Frobenius translate of the other.

      source
      theorem TauCeti.FarguesFontaine.spaX.inductionOn {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} {hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})} {motive : spaX hI β†’ Prop} (x : spaX hI) (h : βˆ€ (v : ↑(spaY p Ο–)), motive (quotientMap hI v)) :
      motive x

      Prove a proposition on 𝒳 by proving it on the image of every point of 𝒴.

      source
      noncomputable def TauCeti.FarguesFontaine.spaX.lift {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {Ξ± : Sort u_2} (f : ↑(spaY p Ο–) β†’ Ξ±) (hf : βˆ€ (n : β„€) (v : ↑(spaY p Ο–)), f ((frobeniusHomeomorph hI ^ n) v) = f v) :
      spaX hI β†’ Ξ±

      A function on 𝒴 invariant under all integer Frobenius translates descends to 𝒳.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.FarguesFontaine.spaX.lift_quotientMap {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {Ξ± : Sort u_2} (f : ↑(spaY p Ο–) β†’ Ξ±) (hf : βˆ€ (n : β„€) (v : ↑(spaY p Ο–)), f ((frobeniusHomeomorph hI ^ n) v) = f v) (v : ↑(spaY p Ο–)) :
        lift hI f hf (quotientMap hI v) = f v

        The descended function evaluates on a quotient point by evaluating on its representative.

        source
        theorem TauCeti.FarguesFontaine.isOpenQuotientMap_quotientMap {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
        IsOpenQuotientMap (quotientMap hI)

        The Frobenius orbit projection is an open quotient map.

        source
        @[simp]
        theorem TauCeti.FarguesFontaine.quotientMap_zpow {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) (v : ↑(spaY p Ο–)) :
        quotientMap hI ((frobeniusHomeomorph hI ^ n) v) = quotientMap hI v

        Integer Frobenius translates have the same image in the quotient.

        source
        theorem TauCeti.FarguesFontaine.injOn_quotientMap_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
        Set.InjOn (quotientMap hI) (Subtype.val ⁻¹' windowU p Ο– n)

        The orbit projection is injective on every U window.

        source
        theorem TauCeti.FarguesFontaine.injOn_quotientMap_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
        Set.InjOn (quotientMap hI) (Subtype.val ⁻¹' windowV p Ο– n)

        The orbit projection is injective on every V window.

        source
        theorem TauCeti.FarguesFontaine.isOpenEmbedding_quotientMap_windowU {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
        Topology.IsOpenEmbedding fun (v : ↑(Subtype.val ⁻¹' windowU p Ο– n)) => quotientMap hI ↑v

        The restriction of the orbit projection to a U window is an open embedding.

        source
        theorem TauCeti.FarguesFontaine.isOpenEmbedding_quotientMap_windowV {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (n : β„€) :
        Topology.IsOpenEmbedding fun (v : ↑(Subtype.val ⁻¹' windowV p Ο– n)) => quotientMap hI ↑v

        The restriction of the orbit projection to a V window is an open embedding.

        source
        theorem TauCeti.FarguesFontaine.image_windowU_zero_union_image_windowV_zero {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
        quotientMap hI '' Subtype.val ⁻¹' windowU p Ο– 0 βˆͺ quotientMap hI '' Subtype.val ⁻¹' windowV p Ο– 0 = Set.univ

        The images of the two windows of index zero cover the Frobenius orbit space.

        source
        instance TauCeti.FarguesFontaine.compactSpace_spaX {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
        CompactSpace (spaX hI)

        The Frobenius orbit space is quasi-compact: its two charts of index zero are images of quasi-compact rational windows.

        source
        instance TauCeti.FarguesFontaine.t0Space_spaX {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] [PerfectRing R p] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
        T0Space (spaX hI)

        The Frobenius orbit space is T0, since its open window charts are subspaces of the valuation spectrum.