Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-11 10:11 34d3fe1d

View on Github →

chore(category_theory/comma): split into three files (#3358) Just reorganisation.

Estimated changes

Created src/category_theory/arrow.lean

added def category_theory.arrow.hom_mk'

added def category_theory.arrow.hom_mk

added theorem category_theory.arrow.id_left

added theorem category_theory.arrow.id_right

added theorem category_theory.arrow.lift.fac_left

added theorem category_theory.arrow.lift.fac_right

added def category_theory.arrow.lift

added theorem category_theory.arrow.lift_mk'_left

added theorem category_theory.arrow.lift_mk'_right

added def category_theory.arrow.mk

added theorem category_theory.arrow.w

added def category_theory.arrow

Modified src/category_theory/comma.lean

deleted def category_theory.arrow.hom_mk'

deleted def category_theory.arrow.hom_mk

deleted theorem category_theory.arrow.id_left

deleted theorem category_theory.arrow.id_right

deleted theorem category_theory.arrow.lift.fac_left

deleted theorem category_theory.arrow.lift.fac_right

deleted def category_theory.arrow.lift

deleted theorem category_theory.arrow.lift_mk'_left

deleted theorem category_theory.arrow.lift_mk'_right

deleted def category_theory.arrow.mk

deleted theorem category_theory.arrow.w

deleted def category_theory.arrow

deleted theorem category_theory.over.comp_left

deleted def category_theory.over.forget

deleted theorem category_theory.over.forget_map

deleted theorem category_theory.over.forget_obj

deleted def category_theory.over.hom_mk

deleted theorem category_theory.over.id_left

deleted def category_theory.over.iterated_slice_backward

deleted theorem category_theory.over.iterated_slice_backward_forget_forget

deleted def category_theory.over.iterated_slice_equiv

deleted def category_theory.over.iterated_slice_forward

deleted theorem category_theory.over.iterated_slice_forward_forget

deleted def category_theory.over.map

deleted theorem category_theory.over.map_map_left

deleted theorem category_theory.over.map_obj_hom

deleted theorem category_theory.over.map_obj_left

deleted def category_theory.over.mk

deleted theorem category_theory.over.mk_hom

deleted theorem category_theory.over.mk_left

deleted theorem category_theory.over.over_morphism.ext

deleted theorem category_theory.over.over_right

deleted def category_theory.over.post

deleted theorem category_theory.over.w

deleted def category_theory.over

deleted theorem category_theory.under.comp_right

deleted def category_theory.under.forget

deleted theorem category_theory.under.forget_map

deleted theorem category_theory.under.forget_obj

deleted def category_theory.under.hom_mk

deleted theorem category_theory.under.id_right

deleted def category_theory.under.map

deleted theorem category_theory.under.map_map_right

deleted theorem category_theory.under.map_obj_hom

deleted theorem category_theory.under.map_obj_right

deleted def category_theory.under.mk

deleted def category_theory.under.post

deleted theorem category_theory.under.under_left

deleted theorem category_theory.under.under_morphism.ext

deleted theorem category_theory.under.w

deleted def category_theory.under

Modified src/category_theory/elements.lean

Modified src/category_theory/limits/over.lean

Modified src/category_theory/limits/shapes/strong_epi.lean

Created src/category_theory/over.lean

added theorem category_theory.over.comp_left

added def category_theory.over.forget

added theorem category_theory.over.forget_map

added theorem category_theory.over.forget_obj

added def category_theory.over.hom_mk

added theorem category_theory.over.id_left

added def category_theory.over.iterated_slice_backward

added theorem category_theory.over.iterated_slice_backward_forget_forget

added def category_theory.over.iterated_slice_equiv

added def category_theory.over.iterated_slice_forward

added theorem category_theory.over.iterated_slice_forward_forget

added def category_theory.over.map

added theorem category_theory.over.map_map_left

added theorem category_theory.over.map_obj_hom

added theorem category_theory.over.map_obj_left

added def category_theory.over.mk

added theorem category_theory.over.mk_hom

added theorem category_theory.over.mk_left

added theorem category_theory.over.over_morphism.ext

added theorem category_theory.over.over_right

added def category_theory.over.post

added theorem category_theory.over.w

added def category_theory.over

added theorem category_theory.under.comp_right

added def category_theory.under.forget

added theorem category_theory.under.forget_map

added theorem category_theory.under.forget_obj

added def category_theory.under.hom_mk

added theorem category_theory.under.id_right

added def category_theory.under.map

added theorem category_theory.under.map_map_right

added theorem category_theory.under.map_obj_hom

added theorem category_theory.under.map_obj_right

added def category_theory.under.mk

added def category_theory.under.post

added theorem category_theory.under.under_left

added theorem category_theory.under.under_morphism.ext

added theorem category_theory.under.w

added def category_theory.under