Commit 2023-03-03 08:09 2e3a7258

View on Github →

feat: port CategoryTheory.Over (#2496)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Over.lean

added theorem CategoryTheory.Over.OverMorphism.ext

added def CategoryTheory.Over.coeFromHom

added theorem CategoryTheory.Over.coe_hom

added theorem CategoryTheory.Over.comp_left

added theorem CategoryTheory.Over.epi_of_epi_left

added def CategoryTheory.Over.forget

added def CategoryTheory.Over.forgetCocone

added theorem CategoryTheory.Over.forget_map

added theorem CategoryTheory.Over.forget_obj

added def CategoryTheory.Over.homMk

added theorem CategoryTheory.Over.id_left

added def CategoryTheory.Over.isoMk

added def CategoryTheory.Over.iteratedSliceBackward

added theorem CategoryTheory.Over.iteratedSliceBackward_forget_forget

added def CategoryTheory.Over.iteratedSliceEquiv

added def CategoryTheory.Over.iteratedSliceForward

added theorem CategoryTheory.Over.iteratedSliceForward_forget

added def CategoryTheory.Over.map

added def CategoryTheory.Over.mapComp

added def CategoryTheory.Over.mapId

added theorem CategoryTheory.Over.map_map_left

added theorem CategoryTheory.Over.map_obj_hom

added theorem CategoryTheory.Over.map_obj_left

added def CategoryTheory.Over.mk

added theorem CategoryTheory.Over.mono_of_mono_left

added theorem CategoryTheory.Over.over_right

added def CategoryTheory.Over.post

added theorem CategoryTheory.Over.w

added def CategoryTheory.Over

added theorem CategoryTheory.Under.UnderMorphism.ext

added theorem CategoryTheory.Under.comp_right

added theorem CategoryTheory.Under.epi_of_epi_right

added def CategoryTheory.Under.forget

added def CategoryTheory.Under.forgetCone

added theorem CategoryTheory.Under.forget_map

added theorem CategoryTheory.Under.forget_obj

added def CategoryTheory.Under.homMk

added theorem CategoryTheory.Under.id_right

added def CategoryTheory.Under.isoMk

added theorem CategoryTheory.Under.isoMk_hom_right

added theorem CategoryTheory.Under.isoMk_inv_right

added def CategoryTheory.Under.map

added def CategoryTheory.Under.mapComp

added def CategoryTheory.Under.mapId

added theorem CategoryTheory.Under.map_map_right

added theorem CategoryTheory.Under.map_obj_hom

added theorem CategoryTheory.Under.map_obj_right

added def CategoryTheory.Under.mk

added theorem CategoryTheory.Under.mono_of_mono_right

added def CategoryTheory.Under.post

added theorem CategoryTheory.Under.under_left

added theorem CategoryTheory.Under.w

added def CategoryTheory.Under