Theorems · Definition · commutative algebra

Perfection.teichmuller

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommRing R] →
        (I : Ideal R) → [inst_2 : CharP (R ⧸ I) p] → [IsAdicComplete I R] → Perfection (R ⧸ I) p →* R

Given an I-adically complete ring R, and a prime number p with p ∈ I, this is the multiplicative map from Perfection (R ⧸ I) p to R itself. Specifically, it is defined as the limit of p^n-th powers of arbitrary lifts in R of the n-th component from the perfection of R ⧸ I. The simp NF is teichmuller₀.

Defined in

Mathlib.RingTheory.Teichmuller

Cited by

10 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPIsAdicComplete