Commit 2023-07-30 23:31 4707b474

View on Github →

feat: allow differential objects with shifts in an AddMonoidWithOne (#6246) What I was really hoping to do was show that ℕ-graded DGOs were the same as ℕ-graded chain complexes (we have the ℤ version), but this still seems awkward. If anyone would like to help with that, please let me know. I think this might be helpful in constructor tensor products of chain complexes with less suffering.

Estimated changes

Modified Mathlib/Algebra/Homology/DifferentialObject.lean

modified theorem CategoryTheory.DifferentialObject.eqToHom_f'

Modified Mathlib/CategoryTheory/DifferentialObject.lean

modified def CategoryTheory.DifferentialObject.Hom.comp

modified def CategoryTheory.DifferentialObject.Hom.id

modified structure CategoryTheory.DifferentialObject.Hom

modified theorem CategoryTheory.DifferentialObject.comp_f

modified theorem CategoryTheory.DifferentialObject.eqToHom_f

modified theorem CategoryTheory.DifferentialObject.ext

modified def CategoryTheory.DifferentialObject.forget

modified theorem CategoryTheory.DifferentialObject.id_f

modified def CategoryTheory.DifferentialObject.isoApp

modified theorem CategoryTheory.DifferentialObject.isoApp_refl

modified theorem CategoryTheory.DifferentialObject.isoApp_symm

modified theorem CategoryTheory.DifferentialObject.isoApp_trans

modified def CategoryTheory.DifferentialObject.mkIso

modified def CategoryTheory.DifferentialObject.shiftFunctor

modified def CategoryTheory.DifferentialObject.shiftZero

modified theorem CategoryTheory.DifferentialObject.zero_f