Theorems · Definition · number theory

BDeRhamPlus

(R : Type u) →
  [inst : 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.

Defined in

Mathlib.RingTheory.Perfectoid.BDeRham

Cited by

0 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFactFactIsAdicComplete