Theorems · Theorem · commutative algebra

WittVector.factorPowSucc_comp_fontaineThetaModPPow

∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ),
  (Ideal.Quotient.factorPowSucc (Ideal.span {↑p}) (n + 1)).comp (WittVector.fontaineThetaModPPow R p (n + 1)) =
    WittVector.fontaineThetaModPPow R p n

Defined in

Mathlib.RingTheory.Perfectoid.FontaineTheta

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFactFactIsAdicComplete