English
The square involving the isomorphisms between cochains and inhomogeneous cochains commutes with the differential d01.
Русский
Квадрат, связывающий коэффициентные коцепи и инфогомохомые коцепи, совместим с дифференциалом d01.
LaTeX
$$$(\\text{cochainsIso}_0 A)^{\\mathrm{hom}} \\circ d_{01} A = d_{01}^{\\mathrm{inhom}}(A) \\circ (\\text{cochainsIso}_1 A)^{\\mathrm{hom}}$$$
Lean4
/-- The 1st differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `Fun(G, A) → Fun(G × G, A)`. It sends
`(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).` -/
@[simps!]
def d₁₂ : ModuleCat.of k (G → A) ⟶ ModuleCat.of k (G × G → A) :=
ModuleCat.ofHom
{ toFun f g := A.ρ g.1 (f g.2) - f (g.1 * g.2) + f g.1
map_add' x y := funext fun g => by dsimp; rw [map_add, add_add_add_comm, add_sub_add_comm]
map_smul' r x := funext fun g => by dsimp; rw [map_smul, smul_add, smul_sub] }
