d_eqToHom — Mathlib

English

There is a natural isomorphism between the identity functor on differential objects and the composition of dgoToHomologicalComplex and homologicalComplexToDGO, i.e., the unit of the equivalence dgoEquivHomologicalComplex.

Русский

Существует естественный изоморфизм между тождественным функтором на дифференциальные обеъекты и композицией dgoToHomologicalComplex и homologicalComplexToDGO — это единица эквивалентности dgoEquivHomologicalComplex.

LaTeX

$$$\mathrm{Id} \cong (dgoToHomologicalComplex \circ homologicalComplexToDGO)$ on the appropriate category$$

Lean4

@[reassoc]
theorem d_eqToHom (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) :
    X.d x y ≫ eqToHom (congr_arg X.X h) = X.d x z := by cases h; simp

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