singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom

English

The composition of the two canonical isomorphisms, one from cycles to homology and another connecting to opcycles, equals the product of the iCycles and pOpcycles maps in the single-object construction.

Русский

Состав двух канонических изоморфизмов, переходящих от циклов к гомологии и соединяющих с opcycles, равен произведению iCycles и pOpcycles в конструкции с одиночным объектом.

LaTeX

$$$(\\mathrm{singleObjCyclesSelfIso} \\, c \\, j \, A).hom \\circ (\\mathrm{singleObjOpcyclesSelfIso} \\, c \\, j \, A).hom = ((\\mathrm{single} \\, C \\, c \\, j).\\mathrm{obj} A).iCycles \\, j \\circ ((\\mathrm{single} \\, C \\, c \\, j).\\mathrm{obj} A).pOpcycles \\, j$$$

Lean4

@[reassoc (attr := simp)]
theorem singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom :
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom =
      ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j :=
  by simp [singleObjCyclesSelfIso, singleObjOpcyclesSelfIso]

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