d₂₁_single — Mathlib

English

The differential d21 acts on a pure tensor of the form single(g1,g2) times a, producing the k-linear combination given by the formula above.

Русский

Дифференциал d21 действует на элемент вида single(g1,g2) ⊗ a, получая линейную комбинацию по формуле выше.

LaTeX

$$$d_{21}A(\mathrm{single}(g1,g2)\otimes a) = \mathrm{single}(g2) \otimes (A.\rho(g1^{-1})a) - \mathrm{single}(g1g2) \otimes a + \mathrm{single}(g1) \otimes a$$$

Lean4

@[simp]
theorem d₂₁_single (g : G × G) (a : A) :
    d₂₁ A (single g a) = single g.2 (A.ρ g.1⁻¹ a) - single (g.1 * g.2) a + single g.1 a := by simp [d₂₁]

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