d₂₁_single_inv_mul_ρ_add_single

English

Another variation of the d21 formula shows how a mixed pair (g⁻¹,gh) interacts with the action ρ(g⁻¹) on a and the addition with (g,h).

Русский

Ещё одно вариационное выражение формулы d21, показывающее взаимодействие пары (g⁻¹,gh) с действием ρ(g⁻¹) на a и сложение с (g,h).

LaTeX

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

Lean4

theorem d₂₁_single_inv_mul_ρ_add_single (g h : G) (a : A) :
    d₂₁ A (single (g⁻¹, g * h) (A.ρ g⁻¹ a) + single (g, h) a) = single g⁻¹ (A.ρ g⁻¹ a) + single g a :=
  by
  simp only [map_add, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel_left]
  abel

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