toAut_continuous — Mathlib

English

Let F be a fiber functor with a continuous G-action on each fiber. The induced map from G to the automorphism group of F is continuous.

Русский

Пусть F — фибр-функтор с непрерывным действием группы G на каждое волокно. Тогда индуцированная карта из G в группу автоморфизмов F непрерывна.

LaTeX

$$$\mathrm{Continuous}(toAut\,F\,G)$$$

Lean4

theorem toAut_continuous [TopologicalSpace G] [IsTopologicalGroup G] [∀ (X : C), ContinuousSMul G (F.obj X)] :
    Continuous (toAut F G) := by
  apply continuous_of_continuousAt_one
  rw [continuousAt_def, map_one]
  intro A hA
  obtain ⟨X, _, hX⟩ := ((nhds_one_has_basis_stabilizers F).mem_iff' A).mp hA
  rw [mem_nhds_iff]
  exact ⟨MulAction.stabilizer G X.pt, Set.preimage_mono (f := toAut F G) hX, stabilizer_isOpen G X.pt, one_mem _⟩

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