Commit 2023-06-29 10:11 f3b01c55

View on Github →

feat: port Algebra.Homology.DifferentialObject (#5033)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/DifferentialObject.lean

added theorem CategoryTheory.DifferentialObject.d_squared_apply

added theorem CategoryTheory.DifferentialObject.eqToHom_f'

added theorem CategoryTheory.DifferentialObject.objEqToHom_d

added theorem CategoryTheory.DifferentialObject.objEqToHom_refl

added theorem HomologicalComplex.d_eqToHom

added def HomologicalComplex.dgoEquivHomologicalComplex

added def HomologicalComplex.dgoEquivHomologicalComplexCounitIso

added def HomologicalComplex.dgoEquivHomologicalComplexUnitIso

added def HomologicalComplex.dgoToHomologicalComplex

added def HomologicalComplex.homologicalComplexToDGO

Modified Mathlib/CategoryTheory/DifferentialObject.lean