English
For a commutative monoid M, the perfection is the projective limit of M under p-th power maps, i.e., the set of functions f: N → M with f(n+1)^p = f(n).
Русский
Для коммутативного моноида M перфекция — предел проективной системы, состоящей из функций f: ℕ → M с условием f(n+1)^p = f(n).
LaTeX
$$Monoid.perfection(M,p) = { f: ℕ → M | ∀ n, f(n+1)^p = f(n) }$$
Lean4
/-- The perfection of a monoid `M`, defined to be the projective limit of `M`
using the `p`-th power maps `M → M` indexed by the natural numbers, implemented as
`{ f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }`. -/
def perfection (M : Type u₁) [CommMonoid M] (p : ℕ) : Submonoid (ℕ → M)
where
carrier := {f | ∀ n, f (n + 1) ^ p = f n}
one_mem' _ := one_pow _
mul_mem' hf hg n := (mul_pow _ _ _).trans <| congr_arg₂ _ (hf n) (hg n)
