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
• Fontaine, Le corps des périodes p-adiques
• Scholze, p-adic Hodge theory for rigid-analytic varieties

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.