English
The first and second cochain differentials commute with the corresponding cochain isomorphisms.
Русский
Дифференциалы d12 совместимы с соответствующими изоморфизмами коцепей.
LaTeX
$$$(\\text{cochainsIso}_1 A)^{\\mathrm{hom}} \\circ d_{12} A = d_{12}^{\\mathrm{inhom}}(A) \\circ (\\text{cochainsIso}_2 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 1st differential: that is, the following
square commutes:
```
C¹(G, A) ---d 1 2---> C²(G, A)
| |
| |
| |
v v
Fun(G, A) --d₁₂--> Fun(G × G, A)
```
where the vertical arrows are `cochainsIso₁` and `cochainsIso₂` respectively.
-/
theorem comp_d₁₂_eq : (cochainsIso₁ A).hom ≫ d₁₂ A = (inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom :=
by
ext x y
change A.ρ y.1 (x _) - x _ + x _ = _ + _
rw [Fin.sum_univ_two]
simp only [Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one, Nat.one_add, neg_one_sq, sub_eq_add_neg,
add_assoc]
rcongr i <;> rw [Subsingleton.elim i 0] <;> rfl
