The de Rham Period Ring $\mathbb{B}_{dR}^+$ and $\mathbb{B}_{dR}$

In this file, we define the de Rham period ring $\mathbb{B}_{dR}^+$ and the de Rham ring $\mathbb{B}_{dR}$. We define a generalized version of these period rings following Scholze. When R is the ring of integers of ℂₚ (PadicComplexInt), they coincide with the classical de Rham period rings.

Main definitions

• BDeRhamPlus : The period ring $\mathbb{B}_{dR}^+$.
• BDeRham : The period ring $\mathbb{B}_{dR}$.

TODO

1. Extend the θ map to $\mathbb{B}_{dR}^+$
2. Show that $\mathbb{B}_{dR}^+$ is a discrete valuation ring.
3. Show that ker θ is principal when the base ring is integral perfectoid.

Currently, the period ring BDeRhamPlus takes the ring of integers R as the input. After the perfectoid theory is developed, we can modify it to take a perfectoid field as the input.

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]
• [Scholze, p-adic Hodge theory for rigid-analytic varieties][scholze2013adic]

Tags

Period rings, p-adic Hodge theory

def fontaineThetaInvertP (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] : Localization.Away ↑p →+* Localization.Away ↑p

The Fontaine's θ map inverting p. Note that if p = 0 in R, then this is the zero map.

Equations

• fontaineThetaInvertP R p = Localization.awayLift ((algebraMap R (Localization.Away ↑p)).comp (WittVector.fontaineTheta R p)) ↑p ⋯

def BDeRhamPlus (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] : Type u

The de Rham period ring $\mathbb{B}_{dR}^+$ for general perfectoid ring. It is the completion of 𝕎 R♭ inverting p with respect to the kernel of the Fontaine's θ map. When $R = \mathcal{O}_{\mathbb{C}_p}$, it coincides with the classical de Rham period ring. Note that if p = 0 in R, then this definition is the zero ring.

Equations

• BDeRhamPlus R p = AdicCompletion (RingHom.ker (fontaineThetaInvertP R p)) (Localization.Away ↑p)

instance instCommRingBDeRhamPlus (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] : CommRing (BDeRhamPlus R p)

Equations

• instCommRingBDeRhamPlus R p = AdicCompletion.instCommRing (RingHom.ker (fontaineThetaInvertP R p))

def BDeRham (R : Type u) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) R] : Type u

The de Rham period ring $\mathbb{B}_{dR}$ for general perfectoid ring. It is defined as $\mathbb{B}_{dR}^+$ inverting the generators of the ideal ker θ. Mathematically, this is equivalent to inverting a generator of the ideal ker θ after we show that it is principal. When $R = \mathcal{O}_{\mathbb{C}_p}$, it coincides with the classical de Rham period ring. Note that if p = 0 in R, then this definition is the zero ring.

Equations

• One or more equations did not get rendered due to their size.