English
The horizontal square relating d21 with the isomorphisms commutes up to the inverse identifications; equivalently, the two ways to transport d21 through the chain iso commute.
Русский
Горизонтальный квадрат, связывающий d21 с изоморфизмами, коммугнет через обратные идентификации; иначе говоря, два способа переноса d21 через цепное изоморфизм согласуются.
LaTeX
$$$(\text{chainsIso}_2 A).hom \circ d_{21} A = (\operatorname{inhomogeneousChains} A).d 2 1 \circ (\text{chainsIso}_1 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 1st differential: that is, the following
square commutes:
```
C₂(G, A) --d 2 1--> 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 2 1 ≫ (chainsIso₁ A).hom :=
ModuleCat.hom_ext <|
lhom_ext fun _ _ => by
simp [inhomogeneousChains.d_def, chainsIso₁, add_assoc, chainsIso₂, d₂₁_single (G := G), -Finsupp.domLCongr_apply,
domLCongr_single, sub_eq_add_neg, Fin.contractNth, inhomogeneousChains.d_single (G := G)]
