d₃₂_single_one_snd — Mathlib

English

When the middle component is one, d32 maps to a boundary that isolates the last component via the representation action.

Русский

Когда средняя компонента равна единице, d32 отображает границу, выделяющую последнюю компоненту через действие представления.

LaTeX

$$$d_{32}A(\mathrm{single}(g,1,h)\otimes a) = \mathrm{single}(1,h)\big(A.ρ(g^{-1})a\big) - \mathrm{single}(g,1)\;a$$$

Lean4

theorem d₃₂_single_one_snd (g h : G) (a : A) :
    d₃₂ A (single (g, 1, h) a) = single (1, h) (A.ρ g⁻¹ a) - single (g, 1) a := by simp [d₃₂]

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