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

• fontaineTheta : Fontaine's θ map, which is a ring homomorphism from 𝕎 R♭ to R.

Main Theorems

• fontaineTheta_teichmuller : θ([x]) is the untilt of x.
• fontaineTheta_surjective : Fontaine's θ map is surjective.

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

• [Fontaine, Sur Certains Types de Représentations p-Adiques du Groupe de Galois d'un Corps Local; Construction d'un Anneau de Barsotti-Tate][fontaine1982certains]
• [Fontaine, Le corps des périodes p-adiques][fontaine1994corps]

θ 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)

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))

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.

@[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)

@[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

@[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)

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

• WittVector.fontaineThetaModPPow R p n = (WittVector.ghostComponentModPPow n).comp ((WittVector.map (PreTilt.coeff 0)).comp (WittVector.map (↑(frobeniusEquiv (PreTilt R p) p).symm ^ n)))

@[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)

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

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

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

• WittVector.fontaineTheta R p = IsAdicComplete.StrictMono.liftRingHom (Ideal.span {↑p}) ⋯ (WittVector.fontaineThetaModPPow R p) ⋯

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

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)

@[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

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.