English
The Mk construction for cocycles₂ A agrees with the inversion of isoCocycles₂ A after transporting along cochainsIso₂ A. This parallels the Mk₁ equality for cocycles₁.
Русский
Конструкция Mk₂ для кокози₂ A согласуется с инверсией isoCocycles₂ A после переноса через cochainsIso₂ A, аналогично равенству Mk₁ для кокози₁.
LaTeX
$$$cocyclesMk\left((cochainsIso_{2}(A))^{-1} x\right) = (isoCocycles_{2}(A))^{-1} x$, for $x \in cocycles_{2}A$$$
Lean4
theorem cocyclesMk₂_eq (x : cocycles₂ A) :
cocyclesMk ((cochainsIso₂ A).inv x) (by simp [← inhomogeneousCochains.d_def, cocycles₂.d₂₃_apply x]) =
(isoCocycles₂ A).inv x :=
by
apply_fun (forget₂ _ Ab).map ((inhomogeneousCochains A).iCycles 2) using
(AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _
simpa only [HomologicalComplex.i_cyclesMk] using (isoCocycles₂_inv_comp_iCocycles_apply _ x).symm
