instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite

English

The category ProfiniteGrp is equipped with a concrete category instance whose morphisms are continuous monoid homomorphisms.

Русский

Категория ProfiniteGrp снабжена структурой конкретной категории: морфизмы — непрерывные гомоморфизмы моноида.

LaTeX

$$instance : ConcreteCategory ProfiniteGrp (fun X Y => X →ₜ* Y)$$

Lean4

@[to_additive]
instance : ConcreteCategory ProfiniteGrp (fun X Y => X →ₜ* Y)
    where
  hom f := f.hom'
  ofHom f := ⟨f⟩

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