stabilizerEquivStabilizer_inv — Mathlib

English

Let G act on α. If b equals g^{-1} acting on a, then the stabilizer equivalence between a and b is the inverse of the stabilizer equivalence obtained from the action of inv(g) on a.

Русский

Пусть G действует на α. Если b = g^{-1} · a, то эквивалентность стабилизаторов между a и b равна обратной эквивалентности стабилизаторов, полученной от действия на a элементом inv(g).

LaTeX

$$$\\text{If } b = g^{-1} \\cdot a, \\quad \\mathrm{stabilizer}_G(a) \\xrightarrow{\\sim} \\mathrm{stabilizer}_G(b) = \\bigl( \\mathrm{stabilizer}_G(b) \\xrightarrow{\\sim} \\mathrm{stabilizer}_G(a) \\bigr)^{-1}.\\,$$$

Lean4

theorem stabilizerEquivStabilizer_inv (hg : b = g⁻¹ • a) :
    stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer (inv_smul_eq_iff.mp hg.symm)).symm := by ext;
  simp [stabilizerEquivStabilizer]

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