English
Let A be a monoid with a topology and E a topological commutative group. Then the set of continuous monoid homomorphisms from A to E forms a commutative group under pointwise multiplication.
Русский
Пусть A — моноид топологического типа, E — топологическая коммутативная группа. Тогда множество непрерывных моноид-гомоморфизмов A в E образует коммутативную группу под покоординатной операцией умножения: (f · g)(a) = f(a) g(a).
LaTeX
$$$C = \mathrm{CMonoidHom}(A,E),\qquad (f\cdot g)(a)=f(a)g(a),\qquad e(a)=e_E,\qquad f^{-1}(a)=f(a)^{-1},$$$
Lean4
@[to_additive]
instance : CommGroup (ContinuousMonoidHom A E)
where
__ : CommMonoid (ContinuousMonoidHom A E) := inferInstance
inv f := (inv E).comp f
inv_mul_cancel f := ext fun x => inv_mul_cancel (f x)
div f g := .comp ⟨divMonoidHom, continuous_div'⟩ (f.prod g)
div_eq_mul_inv f g := ext fun x => div_eq_mul_inv (f x) (g x)
