English
The second and third cochain differentials commute with the corresponding cochain isomorphisms.
Русский
Дифференциалы d23 совместимы с соответствующими изоморфизмами коцепей.
LaTeX
$$$(\\text{cochainsIso}_2 A)^{\\mathrm{hom}} \\circ d_{23} A = d_{23}^{\\mathrm{inhom}}(A) \\circ (\\text{cochainsIso}_3 A)^{\\mathrm{hom}}$$$
Lean4
/-- Let `C(G, A)` denote the complex of inhomogeneous cochains 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 2 3----> C³(G, A)
| |
| |
| |
v v
Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)
```
where the vertical arrows are `cochainsIso₂` and `cochainsIso₃` respectively.
-/
theorem comp_d₂₃_eq : (cochainsIso₂ A).hom ≫ d₂₃ A = (inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom :=
by
ext x y
change A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
dsimp
rw [Fin.sum_univ_three]
simp only [sub_eq_add_neg, add_assoc, Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one, Fin.val_two,
pow_succ' (-1 : k) 2, neg_sq, Nat.one_add, one_pow, mul_one]
rcongr i <;> fin_cases i <;> rfl
