Documentation

TauCeti.AlgebraicGeometry.AdicSpace.FarguesFontaine.Y

The open subset 𝒴 = D(p) ∩ D([Ο–]) of Spa(A_inf, A_inf) #

Let p be a prime, R a commutative ring and Ο– : R, and give the Witt vectors π•Ž R the (p, [Ο–])-adic topology, where [Ο–] is the TeichmΓΌller representative of Ο–. When R = π’ͺ_F is the ring of integers of a complete perfect nonarchimedean field F of characteristic p and Ο– is a pseudouniformiser, this is the Huber ring A_inf = W(π’ͺ_F). The adic Fargues–Fontaine curve is the quotient 𝒴 / Ο†^β„€ of the open subset

𝒴 = {v ∈ Spa(A_inf, A_inf) : v(p [Ο–]) β‰  0} = D(p) ∩ D([Ο–])

of its adic spectrum by the Witt-vector Frobenius Ο†, which acts on points by v ↦ v ∘ Ο†.

This file defines 𝒴 and proves its first properties.

Main definitions #

Main results #

References #

source
theorem TauCeti.FarguesFontaine.comap_frobenius_teichmuller_pow_vle_natCast_pow_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] {Ο– : R} (v : ValuationSpectrum (WittVector p R)) (a b : β„•) :
(WittVector.teichmuller p) Ο– ^ b ≀α΅₯ ↑p ^ a ↔ (WittVector.teichmuller p) Ο– ^ (p * b) ≀α΅₯ ↑p ^ a

Frobenius multiplies the radius by p, from below. Read ΞΊ(v) β‰₯ a / b as v([Ο–]) ^ b ≀ v(p) ^ a. Then ΞΊ(Ο† v) β‰₯ a / b exactly when ΞΊ(v) β‰₯ a / (p b), since Ο† [Ο–] = [Ο–] ^ p and Ο† p = p.

source
theorem TauCeti.FarguesFontaine.comap_frobenius_natCast_pow_vle_teichmuller_pow_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [CharP R p] {Ο– : R} (v : ValuationSpectrum (WittVector p R)) (a b : β„•) :
↑p ^ a ≀α΅₯ (WittVector.teichmuller p) Ο– ^ b ↔ ↑p ^ a ≀α΅₯ (WittVector.teichmuller p) Ο– ^ (p * b)

Frobenius multiplies the radius by p, from above. Read ΞΊ(v) ≀ a / b as v(p) ^ a ≀ v([Ο–]) ^ b. Then ΞΊ(Ο† v) ≀ a / b exactly when ΞΊ(v) ≀ a / (p b), since Ο† [Ο–] = [Ο–] ^ p and Ο† p = p.

source
def TauCeti.FarguesFontaine.spaY (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) :
Set (ValuationSpectrum (WittVector p R))

The open subset 𝒴 = D(p) ∩ D([Ο–]) of Spa(π•Ž R, π•Ž R): the points of the adic spectrum, with plus ring all of π•Ž R, at which neither p nor the TeichmΓΌller representative [Ο–] vanishes. For A_inf = W(π’ͺ_F) with its (p, [Ο–])-adic topology, this is the space whose quotient by Frobenius is the adic Fargues–Fontaine curve.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FarguesFontaine.mem_spaY_iff (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) (v : ValuationSpectrum (WittVector p R)) :
    v ∈ spaY p Ο– ↔ v ∈ ValuationSpectrum.spa ⊀ ∧ ↑p βˆ‰ v.supp ∧ (WittVector.teichmuller p) Ο– βˆ‰ v.supp

    Membership in 𝒴: a point of Spa(π•Ž R, π•Ž R) at which p and [Ο–] do not vanish.

    source
    theorem TauCeti.FarguesFontaine.spaY_eq_spa_inter_basicOpen (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) :
    spaY p Ο– = ValuationSpectrum.spa ⊀ ∩ ValuationSpectrum.basicOpen (↑p * (WittVector.teichmuller p) Ο–) (↑p * (WittVector.teichmuller p) Ο–)

    𝒴 is the locus of Spa(π•Ž R, π•Ž R) where the single element p [Ο–] does not vanish, the basic open subset Spv(π•Ž R)(p [Ο–] / p [Ο–]), since supports are prime.

    source
    theorem TauCeti.FarguesFontaine.isOpen_val_preimage_spaY (p : β„•) [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] (Ο– : R) :
    IsOpen (Subtype.val ⁻¹' spaY p Ο–)

    𝒴 is open in Spa(π•Ž R, π•Ž R).

    source
    theorem TauCeti.FarguesFontaine.mem_spaAnalytic_iff_of_isAdic {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (Aplus : Subring (WittVector p R)) (v : ValuationSpectrum (WittVector p R)) :
    v ∈ ValuationSpectrum.spaAnalytic Aplus ↔ v ∈ ValuationSpectrum.spa Aplus ∧ (↑p βˆ‰ v.supp ∨ (WittVector.teichmuller p) Ο– βˆ‰ v.supp)

    The analytic locus of Spa(π•Ž R, A⁺) is D(p) βˆͺ D([Ο–]), for the (p, [Ο–])-adic topology and any plus ring A⁺: a point is analytic exactly when p or [Ο–] does not vanish at it.

    source
    theorem TauCeti.FarguesFontaine.spaY_subset_spaAnalytic {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) :
    spaY p Ο– βŠ† ValuationSpectrum.spaAnalytic ⊀

    𝒴 consists of analytic points of Spa(π•Ž R, π•Ž R), for the (p, [Ο–])-adic topology.

    source
    theorem TauCeti.FarguesFontaine.exists_pow_vlt_of_mem_spaY {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ spaY p Ο–) (a : β„•) :
    (βˆƒ (b : β„•), (WittVector.teichmuller p) Ο– ^ b <α΅₯ ↑p ^ a) ∧ βˆƒ (b : β„•), ↑p ^ b <α΅₯ (WittVector.teichmuller p) Ο– ^ a

    Power comparison on 𝒴. At a point v ∈ 𝒴 of the (p, [Ο–])-adic Witt vectors, every power v(p) ^ a strictly dominates some power v([Ο–]) ^ b, and every power v([Ο–]) ^ a strictly dominates some power v(p) ^ b. Both p and [Ο–] are topologically nilpotent, and v is continuous and nonvanishing at both. The exponent b is necessarily positive, since v(p) and v([Ο–]) are at most 1.

    source
    theorem TauCeti.FarguesFontaine.comap_frobenius_mem_spaY {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} [CharP R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) {v : ValuationSpectrum (WittVector p R)} (hv : v ∈ spaY p Ο–) :
    ValuationSpectrum.comap WittVector.frobenius v ∈ spaY p Ο–

    Frobenius preserves 𝒴: pulling a point of 𝒴 back along the Witt-vector Frobenius gives a point of 𝒴, for the (p, [Ο–])-adic topology in characteristic p.

    source
    theorem TauCeti.FarguesFontaine.comap_frobenius_mem_spaY_iff {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (v : ValuationSpectrum (WittVector p R)) :
    ValuationSpectrum.comap WittVector.frobenius v ∈ spaY p Ο– ↔ v ∈ spaY p Ο–

    𝒴 is stable under Frobenius and its inverse. For a perfect ring R of characteristic p and the (p, [Ο–])-adic topology, a point of Spv (π•Ž R) lies in 𝒴 exactly when its pullback along the Witt-vector Frobenius does, so the group Ο†^β„€ acts on 𝒴.

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

    Pullback along Witt Frobenius, as a homeomorphism of 𝒴.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.FarguesFontaine.frobeniusHomeomorph_apply_val {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (v : ↑(spaY p Ο–)) :
      ↑((frobeniusHomeomorph hI) v) = ValuationSpectrum.comap WittVector.frobenius ↑v

      On underlying valuations, the Frobenius homeomorphism is pullback along Frobenius.

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

      The inverse Frobenius homeomorphism is pullback along inverse Witt Frobenius.

      source
      theorem TauCeti.FarguesFontaine.frobeniusHomeomorph_pow_apply_val {p : β„•} [Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] [TopologicalSpace (WittVector p R)] {Ο– : R} [CharP R p] [PerfectRing R p] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (k : β„•) (v : ↑(spaY p Ο–)) :
      ↑((frobeniusHomeomorph hI ^ k) v) = (ValuationSpectrum.comap WittVector.frobenius)^[k] ↑v

      Positive powers of the Frobenius homeomorphism are the usual Frobenius iterates.