isoCocycles₁_inv_comp_iCocycles

English

Equality of morphisms: (isoCocycles₁ A).inv ≫ iCocycles A 1 = (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv.

Русский

Равенство отображений: (isoCocycles₁ A).inv ≫ iCocycles A 1 = (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv.

LaTeX

$$$(isoCocycles_1(A)).inv \\circ iCocycles(A,1) = (shortComplexH1(A)).moduleCatLeftHomologyData.i \\circ (cochainsIso_1(A)).inv$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem isoCocycles₁_inv_comp_iCocycles :
    (isoCocycles₁ A).inv ≫ iCocycles A 1 = (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₁ A).inv :=
  (CommSq.horiz_inv ⟨isoCocycles₁_hom_comp_i A⟩).w

Похожие утверждения