End — Mathlib

English

The collection of coalgebra endomorphisms of A, with multiplication given by composition and identity map, forms a monoid.

Русский

Множество коалгоморфизмов A → A образует моноид под операцией композиции, с единицей — тождественное отображение.

LaTeX

$$$\mathrm{End}_R(A) \\text{is a monoid with } (f \cdot g)(a) = f(g(a)) \\text{and } \mathrm{id}_A(a) = a$$$

Lean4

@[simps -isSimp toSemigroup_toMul_mul toOne_one]
instance End : Monoid (A →ₗc[R] A) where
  mul := comp
  mul_assoc _ _ _ := rfl
  one := CoalgHom.id R A
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl

Похожие утверждения