English
For any cocycles₁ A, the map cocylesMk₁ transported along the isomorphism from cochains yields the corresponding inv component of isoCocycles₁ A. This expresses compatibility between Mk₁-construction and the isomorphism of cocycles.
Русский
Для любых cocycles₁ A отображение cocylesMk₁, переносимое вдоль изоморфизма от коциклинтов, даёт соответствующую компоненту inv у isoCocycles₁ A. Отражает совместимость конструирования Mk₁ и изоморфизма кокозиал.
LaTeX
$$$cocyclesMk\left((cochainsIso_{1}(A))^{-1} x\right) = (isoCocycles_{1}(A))^{-1} x \quad\text{для } x \in cocycles_{1}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 1) using
(AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _
simpa only [HomologicalComplex.i_cyclesMk] using (isoCocycles₁_inv_comp_iCocycles_apply _ x).symm
