English
The perfection of a ring R with characteristic p yields a subring of ℕ → R, compatible with Frobenius maps.
Русский
Перфекция кольца R с характеристикой p образует подполь кольца из функций ℕ → R, совместимая с отображениями Фробениуса.
LaTeX
$$perfectionSubring(R,p) is a Subring of ℕ → R$$
Lean4
/-- The perfection of a ring `R` with characteristic `p`, as a subring,
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 perfectionSubring (R : Type u₁) [CommRing R] (p : ℕ) [hp : Fact p.Prime] [CharP R p] : Subring (ℕ → R) :=
(Ring.perfectionSubsemiring R p).toSubring fun n => by
simp_rw [← frobenius_def, Pi.neg_apply, Pi.one_apply, RingHom.map_neg, RingHom.map_one]
