Theorems · Definition · commutative algebra

WittVector.fontaineTheta

(R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : 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).

Defined in

Mathlib.RingTheory.Perfectoid.FontaineTheta

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingFactFactIsAdicComplete