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