leftHomologyπ_comp_leftHomologyIso_hom

English

Let S be a ShortComplex with LeftHomologyData h, then the leftHomology map relation satisfies S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π.

Русский

Пусть S — краткий комплекс с данными левой гомологии h. Тогда тождество связывающее leftHomology maps выполняется как S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π.

LaTeX

$$$S.leftHomologyπ \circ h.leftHomologyIso.hom = h.cyclesIso.hom \circ h.\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem leftHomologyπ_comp_leftHomologyIso_hom : S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π :=
  by
  dsimp only [leftHomologyπ, leftHomologyIso, cyclesIso, leftHomologyMapIso', cyclesMapIso', Iso.refl]
  rw [← leftHomologyπ_naturality']

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