English
The perfection of a ring R with characteristic p is the subsemiring of ℕ → R consisting of all functions with the p-th Frobenius relation, closed under addition and multiplication.
Русский
Перфекция кольца R с характеристикой p образует подпол semiring из функций ℕ → R удовлетворяющих отношение Фробениуса p-го порядка; замкнута относительно сложения и умножения.
LaTeX
$$perfectionSubsemiring(R,p) is a Subsemiring of $(\\mathbb{N} \\to R)$ with $\forall n, f(n+1)^p=f(n)$$$
Lean4
/-- The perfection of a ring `R` with characteristic `p`, as a subsemiring,
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 perfectionSubsemiring (R : Type u₁) [CommSemiring R] (p : ℕ) [hp : Fact p.Prime] [CharP R p] :
Subsemiring (ℕ → R) :=
{ Monoid.perfection R p with
zero_mem' := fun _ ↦ zero_pow hp.1.ne_zero
add_mem' := fun hf hg n => (frobenius_add R p _ _).trans <| congr_arg₂ _ (hf n) (hg n) }
