d₂₁_single_ρ_add_single_inv_mul

English

The differential d21 is additive on two basis elements: it maps a sum of two basis elements to the sum of their images under the prescribed rules, one of which uses the action by ρ and the other a shift by multiplication.

Русский

Дифференциал d21 сохраняет аддитивность по отношению к сумме двух базисных элементов: он переводит сумму в сумму изображений по заданным правилам, одна из которых использует действие ρ, другая — сдвиг по умножению.

LaTeX

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

Lean4

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

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