continuous_mapAut_whiskeringRight

English

Noncomputable continuous multiplicative equivalence between Aut F and Aut (F ⋙ G).

Русский

Не вычислимое непрерывное умножение-эквивалентность между Aut F и Aut (F ⋙ G).

LaTeX

$$$\text{Aut F} \equiv_{\text{cont}}^* \text{Aut}(F \circ G)$$$

Lean4

/-- If `G` is a functor of categories of finite types, the induced map `Aut F → Aut (F ⋙ G)` is
continuous. -/
theorem continuous_mapAut_whiskeringRight (G : FintypeCat.{w} ⥤ FintypeCat.{v}) :
    Continuous (((whiskeringRight _ _ _).obj G).mapAut F) :=
  by
  rw [Topology.IsInducing.continuous_iff (autEmbedding_isClosedEmbedding _).isInducing, continuous_pi_iff]
  intro X
  change Continuous fun a ↦ G.mapAut (F.obj X) (autEmbedding F a X)
  fun_prop

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