instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux

English

For a small category J and a functor F: J ⥤ ProfiniteGrp, the subtype realizing a subspace of the limit cone ptAux has compact topology.

Русский

Для малой категории J и функторa F: J ⥤ ProfiniteGrp, подсистема, соответствующая подпространству точки предела, имеет компактную топологию.

LaTeX

$$$\text{CompactSpace} (\mathrm{subtype\;of\;limitConePtAux(F)})$$$

Lean4

instance : CompactSpace (limitConePtAux F) :=
  inferInstanceAs (CompactSpace (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt)

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