d₂₁_single_inv_self_ρ_sub_self_inv

English

A certain linear combination of two basis elements maps under d21 to a simple difference of two unit elements: a - ρ(g⁻¹)a, reflecting the compatibility of the action with inverses.

Русский

Определённая линейная комбинация двух базисных элементов под действием d21 маппируется в простую разность единичных элементов: a - ρ(g⁻¹)a, что отражает совместимость действия с инверсиями.

LaTeX

$$$d_{21}A(\mathrm{single}(g^{-1},g)(\!A.\rho(g^{-1})a) - \mathrm{single}(g,g^{-1})a) = \mathrm{single}(1)a - \mathrm{single}(1)(A.\rho(g^{-1})a)$$$

Lean4

theorem d₂₁_single_inv_self_ρ_sub_self_inv (g : G) (a : A) :
    d₂₁ A (single (g⁻¹, g) (A.ρ g⁻¹ a) - single (g, g⁻¹) a) = single 1 a - single 1 (A.ρ g⁻¹ a) :=
  by
  simp only [map_sub, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel, mul_inv_cancel]
  abel

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