English
The natural square formed by the chains and isomorphisms commutes: going along the top then right is the same as going down then along the side.
Русский
Естественный квадрат, образованный цепями и изоморфизмами, коммугент: путь сверху вправо равен пути слева вниз.
LaTeX
$$$(\text{chainsIso}_1 A)^{\mathrm{hom}} \circ d_{10} A = d_{1 0}^{\mathrm{inhom}} \circ (\text{chainsIso}_0 A)^{\mathrm{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 0th differential: that is, the following
square commutes:
```
C₁(G, A) --d 1 0--> C₀(G, A)
| |
| |
| |
v v
(G →₀ A) ----d₁₀----> A
```
where the vertical arrows are `chainsIso₁` and `chainsIso₀` respectively.
-/
theorem comp_d₁₀_eq : (chainsIso₁ A).hom ≫ d₁₀ A = (inhomogeneousChains A).d 1 0 ≫ (chainsIso₀ A).hom :=
ModuleCat.hom_ext <|
lhom_ext fun _ _ => by
simp [inhomogeneousChains.d_def, chainsIso₀, chainsIso₁, d₁₀_single (G := G), Unique.eq_default (α := Fin 0 → G),
sub_eq_add_neg, inhomogeneousChains.d_single (G := G)]
