stabilizer_normal_of_isGalois — Mathlib

English

For a Galois X and x ∈ F.obj X, the stabilizer of x under Aut F is a normal subgroup of Aut F.

Русский

Для галуа-объекта X и элемента x ∈ F.obj X стабилизатор x под действием Aut F образует нормальную подгруппу Aut F.

LaTeX

$$$\operatorname{Subgroup.Normal}\bigl(\operatorname{MulAction.stabilizer}(\mathrm{Aut}\,F)\,x\bigr).$$$

Lean4

theorem stabilizer_normal_of_isGalois (X : C) [IsGalois X] (x : F.obj X) :
    Subgroup.Normal (MulAction.stabilizer (Aut F) x) where
  conj_mem n ninstab
    g := by
    rw [MulAction.mem_stabilizer_iff]
    change g • n • (g⁻¹ • x) = x
    have : ∃ (φ : Aut X), F.map φ.hom x = g⁻¹ • x := MulAction.IsPretransitive.exists_smul_eq x (g⁻¹ • x)
    obtain ⟨φ, h⟩ := this
    rw [← h, mulAction_naturality, ninstab, h]
    simp

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