English
The perfection of a ring R is a type of functions from ℕ to R satisfying the Frobenius relation, endowed with ring operations componentwise.
Русский
Перфекция кольца R — это множество функций ℕ → R, удовлетворяющих отношение Фробениуса, с операциями сложения и умножения по компонентам.
LaTeX
$$Ring.Perfection(R,p) = { f: ℕ → R | ∀ n, f(n+1)^p = f(n) }$$
Lean4
/-- The perfection of a ring `R` with characteristic `p`,
defined to be the projective limit of `R` using the Frobenius maps `R → R`
indexed by the natural numbers, implemented as `{f : ℕ → R // ∀ n, f (n + 1) ^ p = f n}`. -/
def Perfection (R : Type u₁) [CommSemiring R] (p : ℕ) : Type u₁ :=
{ f // ∀ n : ℕ, (f : ℕ → R) (n + 1) ^ p = f n }
