Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-20 14:35
585294d7
View on Github →
feat(CategoryTheory): covariant functoriality of graded objects on the index set (
#7425
)
Estimated changes
Modified
Mathlib/CategoryTheory/GradedObject.lean
added
theorem
CategoryTheory.GradedObject.CofanMapObjFun.hasMap
added
theorem
CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom
added
def
CategoryTheory.GradedObject.CofanMapObjFun.mk
added
theorem
CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv
added
theorem
CategoryTheory.GradedObject.congr_mapMap
added
theorem
CategoryTheory.GradedObject.isIso_of_isIso_apply
added
def
CategoryTheory.GradedObject.isoMk
added
theorem
CategoryTheory.GradedObject.iso_hom_inv_id_apply
added
theorem
CategoryTheory.GradedObject.iso_inv_hom_id_apply
added
theorem
CategoryTheory.GradedObject.mapMap_comp
added
theorem
CategoryTheory.GradedObject.mapMap_id
added
theorem
CategoryTheory.GradedObject.mapObj_ext
added
theorem
CategoryTheory.GradedObject.ι_descMapObj
added
theorem
CategoryTheory.GradedObject.ι_mapMap
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
added
def
CategoryTheory.Limits.Cofan.IsColimit.desc
added
theorem
CategoryTheory.Limits.Cofan.IsColimit.fac
added
theorem
CategoryTheory.Limits.Cofan.IsColimit.hom_ext
added
def
CategoryTheory.Limits.Fan.IsLimit.desc
added
theorem
CategoryTheory.Limits.Fan.IsLimit.fac
added
theorem
CategoryTheory.Limits.Fan.IsLimit.hom_ext