English
If G is a functor of finite-type categories, the induced Aut-map under whiskering is continuous.
Русский
Если G — функтор между категориями конечных типов, сопряженное отображение Aut через обвязку непрерывно.
LaTeX
$$$\text{Continuous}(\mathrm{mapAut} F ( (\mathrm{whiskeringRight} C) .\mathrm{obj} G ))$$$
Lean4
/-- If `G` is a fully faithful functor of categories finite types, this is the automorphism of
topological groups `Aut F ≃ Aut (F ⋙ G)`. -/
noncomputable def autEquivAutWhiskerRight {G : FintypeCat.{w} ⥤ FintypeCat.{v}} (h : G.FullyFaithful) :
Aut F ≃ₜ* Aut (F ⋙ G) where
__ := (h.whiskeringRight C).autMulEquivOfFullyFaithful F
continuous_toFun := continuous_mapAut_whiskeringRight F G
continuous_invFun :=
Continuous.continuous_symm_of_equiv_compact_to_t2 (f :=
((h.whiskeringRight C).autMulEquivOfFullyFaithful F).toEquiv) (continuous_mapAut_whiskeringRight F G)
