English
The same compatibility as in item 172681, expressed in terms of the other form of the differential.
Русский
Та же совместимость, что в пункте 172681, выраженная через другую форму дифференциала.
LaTeX
$$$(\\text{cochainsIso}_0 A)^{\\mathrm{hom}} \\circ d_{01} A = d_{01}^{\\mathrm{inhom}}(A) \\circ (\\text{cochainsIso}_1 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 0th differential: that is, the following
square commutes:
```
C⁰(G, A) --d 0 1--> C¹(G, A)
| |
| |
| |
v v
A ------d₀₁-----> Fun(G, A)
```
where the vertical arrows are `cochainsIso₀` and `cochainsIso₁` respectively.
-/
theorem comp_d₀₁_eq : (cochainsIso₀ A).hom ≫ d₀₁ A = (inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom :=
by
ext x y
change A.ρ y (x default) - x default = _ + ({0} : Finset _).sum _
simp_rw [Fin.val_eq_zero, zero_add, pow_one, neg_smul, one_smul, Finset.sum_singleton, sub_eq_add_neg]
rcongr i <;> exact Fin.elim0 i
