Theorems · Definition · commutative algebra

Perfection

(α : Type u₁) → [Pow α ℕ] → ℕ → Type u₁

The perfection of a monoid α, defined to be the projective limit of α using the p-th power maps α → α indexed by the natural numbers, implemented as { f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }. If α is a ring with characteristic p and p is prime, Perfection α p is also a ring.

Defined in

Mathlib.RingTheory.Perfection

Cited by

84 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Pow