English
From a continuous monoid homomorphism f : X →ₜ* Y one obtains a morphism in ProfiniteGrp between ProfiniteGrp.of X and ProfiniteGrp.of Y.
Русский
Из непрерывного моноид-гомоморфизма f: X →ₜ* Y строится морфизм в ProfiniteGrp между ProfiniteGrp.of X и ProfiniteGrp.of Y.
LaTeX
$$ofHom (f : X →ₜ* Y) : ProfiniteGrp.of X ⟶ ProfiniteGrp.of Y$$
Lean4
/-- Typecheck a `ContinuousMonoidHom` as a morphism in `ProfiniteGrp`. -/
@[to_additive /-- Typecheck a `ContinuousAddMonoidHom` as a morphism in `ProfiniteAddGrp`. -/
]
abbrev ofHom {X Y : Type u} [Group X] [TopologicalSpace X] [IsTopologicalGroup X] [CompactSpace X]
[TotallyDisconnectedSpace X] [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y] [CompactSpace Y]
[TotallyDisconnectedSpace Y] (f : X →ₜ* Y) : ProfiniteGrp.of X ⟶ ProfiniteGrp.of Y :=
ConcreteCategory.ofHom f
