instHasForget₂Profinite — Mathlib

English

There is a forgetful functor from ProfiniteGrp to Profinite that sends a profinite group to its underlying profinite space and a morphism to the underlying continuous map.

Русский

Существует функтор забывания из ProfiniteGrp в Profinite, отправляющий профинированную группу на соответствующее ей профинированное пространство, а гомоморфизм — на непрерывный отображение между пространствами.

LaTeX

$$$\mathrm{Forget2}\;\mathrm{ProfiniteGrp}\;\mathrm{Profinite}$$$

Lean4

/-- The functor mapping a profinite group to its underlying profinite space. -/
@[to_additive]
instance : HasForget₂ ProfiniteGrp Profinite where
  forget₂ :=
    { obj G := G.toProfinite
      map f := CompHausLike.ofHom _ ⟨f, by continuity⟩ }

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