fixingSubgroup_map_conj_eq — Mathlib

English

Conjugation induces an equivalence preserving the fixingSubgroup under a left action.

Русский

Конъюгация сохраняет фиксацию подгрупп под левым действием.

LaTeX

$$$fixingSubgroup\ M( g\cdot s) = (fixingSubgroup\ M s).map (MulAut.conj g)$$$

Lean4

@[to_additive]
theorem fixingSubgroup_map_conj_eq (hg : g • t = s) :
    (fixingSubgroup M t).map (MulAut.conj g).toMonoidHom = fixingSubgroup M s :=
  by
  ext k
  simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.coe_coe]
  constructor
  · rintro ⟨n, hn, rfl⟩
    exact Set.conj_mem_fixingSubgroup hg hn
  · intro hk
    use MulAut.conj g⁻¹ k
    constructor
    · apply Set.conj_mem_fixingSubgroup _ hk
      rw [inv_smul_eq_iff, hg]
    · simp [MulAut.conj]; group

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