stabilizer_image_coe_quotient — Mathlib

English

In the quotient by the stabilizer, the stabilizer of the image of s is the bottom subgroup; i.e., it is trivial.

Русский

В фактор-группе по стабилизатору стабилизатор образа s является тривиальным подгруппой; то есть это нулевой подгрупповой элемент.

LaTeX

$$$\mathrm{Stab}_Q( q''s) = \bot$$$

Lean4

@[to_additive]
theorem stabilizer_image_coe_quotient : stabilizer Q ( q '' s) = ⊥ :=
  by
  ext a
  induction a using QuotientGroup.induction_on with
  | _ a
  simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]
  have : q a • q '' s = q '' (a • s) := (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm
  rw [this]
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h

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