Documentation

Mathlib.RingTheory.Perfectoid.FontaineTheta

Fontaine's θ map #

In this file, we define Fontaine's θ map, which is a ring homomorphism from the Witt vector 𝕎 R♭ of the tilt of a perfectoid ring R to R itself. Our definition of θ does not require that R is perfectoid in the first place. We only need R to be p-adically complete.

Main Definitions #

Main Theorems #

TODO #

Establish that our definition (explicit construction of θ mod p ^ n) agrees with the deformation-theoretic approach via the cotangent complex, as in Bhatt, Lecture notes for a class on perfectoid spaces. Remark 6.1.7.

Tags #

Fontaine's theta map, perfectoid theory, p-adic Hodge theory

Reference #

θ as a ring homomorphism #

Let 𝔭 denote the ideal of R generated by the prime number p. In this section, we first define the ring homomorphism fontaineThetaModPPow : 𝕎 R♭ →+* R ⧸ 𝔭 ^ (n + 1). Then we show they are compatible with each other and lift to a ring homomorphism fontaineTheta : 𝕎 R♭ →+* R.

To prove this, we define fontaineThetaModPPow as a composition of the following ring homomorphisms.

𝕎 R♭ --𝕎(Frob^-n)-> 𝕎 R♭ --𝕎(coeff 0)-> 𝕎(R/𝔭) --gh_n-> R/𝔭^(n+1)

Here, the ring map gh_n fits in the following diagram.

𝕎(R)  --ghost_n->   R
|                   |
v                   v
𝕎(R/𝔭) --gh_n-> R/𝔭^(n+1)
source
theorem WittVector.ker_map_le_ker_mk_comp_ghostComponent {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) :
RingHom.ker (map (Ideal.Quotient.mk (Ideal.span {↑p}))) ≤ RingHom.ker ((Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))).comp (ghostComponent n))
source
def WittVector.ghostComponentModPPow {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) :
WittVector p (R ⧸ Ideal.span {↑p}) →+* R ⧸ Ideal.span {↑p} ^ (n + 1)

The lift ring map gh_n : 𝕎(R/𝔭) →+* R/𝔭^(n+1) of the n-th ghost component 𝕎(R) →+* R along the surjective ring map 𝕎(R) →+* 𝕎(R/𝔭).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WittVector.ghostComponentModPPow_map_mk {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (x : WittVector p R) :
    (ghostComponentModPPow n) ((map (Ideal.Quotient.mk (Ideal.span {↑p}))) x) = (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) ((ghostComponent n) x)
    source
    @[simp]
    theorem WittVector.quotEquivOfEq_ghostComponentModPPow {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] (x : WittVector p (R ⧸ Ideal.span {↑p})) (h : Ideal.span {↑p} ^ (0 + 1) = Ideal.span {↑p}) :
    (Ideal.quotEquivOfEq h) ((ghostComponentModPPow 0) x) = (ghostComponent 0) x
    source
    @[simp]
    theorem WittVector.ghostComponentModPPow_teichmuller_coeff {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : PreTilt R p) :
    (ghostComponentModPPow n) ((teichmuller p) ((PreTilt.coeff n) x)) = (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) (PreTilt.untilt x)
    source
    def WittVector.fontaineThetaModPPow (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (n : ℕ) :
    WittVector p (PreTilt R p) →+* R ⧸ Ideal.span {↑p} ^ (n + 1)

    The Fontaine's theta map modulo p^(n+1). It is the composition of the following ring homomorphisms. 𝕎 R♭ --𝕎(Frob^-n)-> 𝕎 R♭ --𝕎(coeff 0)-> 𝕎(R/p) --gh_n-> R/p^(n+1)

    Equations
    Instances For
      source
      @[simp]
      theorem WittVector.fontaineThetaModPPow_teichmuller {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : PreTilt R p) :
      (fontaineThetaModPPow R p n) ((teichmuller p) x) = (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) (PreTilt.untilt x)
      source
      theorem WittVector.factorPowSucc_comp_fontaineThetaModPPow {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) :
      (Ideal.Quotient.factorPowSucc (Ideal.span {↑p}) (n + 1)).comp (fontaineThetaModPPow R p (n + 1)) = fontaineThetaModPPow R p n
      source
      theorem WittVector.factorPowSucc_fontaineThetaModPPow_eq {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : WittVector p (PreTilt R p)) :
      (Ideal.Quotient.factorPowSucc (Ideal.span {↑p}) (n + 1)) ((fontaineThetaModPPow R p (n + 1)) x) = (fontaineThetaModPPow R p n) x
      source
      def WittVector.fontaineTheta (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] :
      WittVector p (PreTilt R p) →+* R

      The Fontaine's θ map from 𝕎 R♭ to R. It is the limit of the ring maps fontaineThetaModPPow n from 𝕎 R♭ to R/p^(n+1).

      Equations
      Instances For
        source
        theorem WittVector.mk_pow_fontaineTheta {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : WittVector p (PreTilt R p)) :
        (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) ((fontaineTheta R p) x) = (fontaineThetaModPPow R p n) x
        source
        theorem WittVector.mk_fontaineTheta {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (x : WittVector p (PreTilt R p)) :
        (Ideal.Quotient.mk (Ideal.span {↑p})) ((fontaineTheta R p) x) = (PreTilt.coeff 0) (x.coeff 0)
        source
        @[simp]
        theorem WittVector.fontaineTheta_teichmuller {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (x : PreTilt R p) :
        (fontaineTheta R p) ((teichmuller p) x) = PreTilt.untilt x
        source
        theorem surjective_fontaineTheta {R : Type u} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] (hF : Function.Surjective ⇑(frobenius (ModP R p) p)) :
        Function.Surjective ⇑(WittVector.fontaineTheta R p)

        If the Frobenius map is surjective on R/pR, then the Fontaine's θ map is surjective.