instCompactSpaceAutFunctorFintypeCat

English

Let F be a functor from a category C to the finite-type category. Then the automorphism group Aut F, equipped with the natural topology coming from the construction autEmbedding, is a compact space.

Русский

Пусть F — функтор из категории C в категорию конечных типов. Тогда группа автоморфизмов Aut F, снабженная естественной топологией, образованной через встраивание autEmbedding, является компактным пространством.

LaTeX

$$$\operatorname{CompactSpace}\big(\operatorname{Aut} F\big)$$$

Lean4

instance : CompactSpace (Aut F) :=
  (autEmbedding_isClosedEmbedding F).compactSpace

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