continuousSMul_aut_fiber — Mathlib

English

There is a topological group isomorphism Aut F ≃ Aut (F ⋙ G) for fully faithful G.

Русский

Существует топологическое групповое изоморфизм Aut F ≃ Aut (F ⋙ G) для полностью верного G.

LaTeX

$$$\operatorname{Aut} F \simeq_{top} \operatorname{Aut}(F \circ G)$$$

Lean4

instance continuousSMul_aut_fiber (X : C) : ContinuousSMul (Aut F) (F.obj X) where
  continuous_smul := by
    let g : Aut (F.obj X) × F.obj X → F.obj X := fun ⟨σ, x⟩ ↦ σ.hom x
    let h (q : Aut F × F.obj X) : Aut (F.obj X) × F.obj X := ⟨((fun p ↦ p X) ∘ autEmbedding F) q.1, q.2⟩
    change Continuous (g ∘ h)
    fun_prop

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