Commit 2023-04-11 12:30 ce0c89b8

View on Github →

feat: port CategoryTheory.GradedObject (#3342)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/GradedObject.lean

added def CategoryTheory.GradedObject.comapEq

added theorem CategoryTheory.GradedObject.comapEq_symm

added theorem CategoryTheory.GradedObject.comapEq_trans

added def CategoryTheory.GradedObject.comapEquiv

added theorem CategoryTheory.GradedObject.eqToHom_apply

added theorem CategoryTheory.GradedObject.eqToHom_proj

added def CategoryTheory.GradedObject.eval

added theorem CategoryTheory.GradedObject.hom_ext

added theorem CategoryTheory.GradedObject.shiftFunctor_map_apply

added theorem CategoryTheory.GradedObject.shiftFunctor_obj_apply

added theorem CategoryTheory.GradedObject.zero_apply

added def CategoryTheory.GradedObject

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean