English
The D32 differential commutes with the D21 differential after passing through the corresponding chain isomorphisms, yielding a commutative diagram for the 3- and 2-skeleta.
Русский
Дифференциал D32 commuting с D21 после применения соответствующих цепных изоморфизмов, образуя коммутативную диаграмму для 3- и 2-скелетов.
LaTeX
$$$(\text{chainsIso}_3 A).hom \circ d_{32} A = (\operatorname{inhomogeneousChains} A).d 3 2 \circ (\text{chainsIso}_2 A).hom$$$
Lean4
/-- Let `C(G, A)` denote the complex of inhomogeneous chains of `A : Rep k G`. This lemma
says `d₃₂` gives a simpler expression for the 2nd differential: that is, the following
square commutes:
```
C₃(G, A) --d 3 2--> C₂(G, A)
| |
| |
| |
v v
(G³ →₀ A) --d₃₂--> (G² →₀ A)
```
where the vertical arrows are `chainsIso₃` and `chainsIso₂` respectively.
-/
theorem comp_d₃₂_eq : (chainsIso₃ A).hom ≫ d₃₂ A = (inhomogeneousChains A).d 3 2 ≫ (chainsIso₂ A).hom :=
ModuleCat.hom_ext <|
lhom_ext fun _ _ => by
simp [inhomogeneousChains.d_def, chainsIso₂, pow_succ, chainsIso₃, -domLCongr_apply, domLCongr_single, d₃₂,
Fin.sum_univ_three, Fin.contractNth, Fin.tail_def, sub_eq_add_neg, add_assoc,
inhomogeneousChains.d_single (G := G), add_rotate' (-(single (_ * _, _) _)),
add_left_comm (single (_, _ * _) _)]
