inv_conjMap_comp_apply — Mathlib

English

Let b = g · a and c = h · b with c = k · a. Then the conjugation map associated to hg has an inverse given by the conjugation map for the inverse smul, and applying them to any element x of the stabilizer of b yields x itself; i.e., the two conjugations cancel.

Русский

Пусть b = g · a, c = h · b и c = k · a. Тогда отображение конъюгирования, соответствующее hg, имеет обратное отображение, заданное конъюгированием для обратного смуля, и применение их к элементу x из стабилизатора b возвращает x; т.е. их композиция даёт тождественность на стабилизаторе b.

LaTeX

$$$\\forall x \\in \\mathrm{Stab}_G(b),\\; \\mathrm{conjMap}_{hg}\\bigl(\\mathrm{conjMap}_{\\mathrm{eq\\_inv\\_smul\\_iff.mpr(hg.symm)}}(x)\\bigr) = x.$$$

Lean4

@[to_additive]
theorem inv_conjMap_comp_apply (x : ofStabilizer G b) : conjMap hg (conjMap (eq_inv_smul_iff.mpr hg.symm) x) = x := by
  simp [← Subtype.coe_inj, conjMap_apply]

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