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 #

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] (https://www.math.ias.edu/~bhatt/teaching/mat679w17/lectures.pdf).

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/p) --gh_n-> R/p^(n+1)

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

𝕎(A)  --ghost_n->   A
|                   |
v                   v
𝕎(A/p) --gh_n-> A/p^(n+1)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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
    • One or more equations did not get rendered due to their size.
    Instances For

      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