Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-11 16:07 796f2675

View on Github →

refactor(category_theory/lifting_properties): refactor lifting properties using comm_sq (#15765)

Estimated changes

Modified src/category_theory/arrow.lean

deleted theorem category_theory.arrow.has_lift.mk

deleted theorem category_theory.arrow.lift.fac_left

deleted theorem category_theory.arrow.lift.fac_left_of_from_mk

deleted theorem category_theory.arrow.lift.fac_right

deleted theorem category_theory.arrow.lift.fac_right_of_to_mk

deleted theorem category_theory.arrow.lift_mk'_left

deleted theorem category_theory.arrow.lift_mk'_right

deleted structure category_theory.arrow.lift_struct

Modified src/category_theory/comm_sq.lean

added theorem category_theory.comm_sq.fac_left

added theorem category_theory.comm_sq.fac_right

added theorem category_theory.comm_sq.has_lift.iff

added theorem category_theory.comm_sq.has_lift.iff_op

added theorem category_theory.comm_sq.has_lift.iff_unop

added theorem category_theory.comm_sq.has_lift.mk'

added def category_theory.comm_sq.lift

added def category_theory.comm_sq.lift_struct.op

added def category_theory.comm_sq.lift_struct.op_equiv

added def category_theory.comm_sq.lift_struct.unop

added def category_theory.comm_sq.lift_struct.unop_equiv

added structure category_theory.comm_sq.lift_struct

Deleted src/category_theory/lifting_properties.lean

deleted theorem category_theory.has_right_lifting_property_comp'

deleted theorem category_theory.has_right_lifting_property_comp

deleted theorem category_theory.id_has_right_lifting_property'

deleted theorem category_theory.id_has_right_lifting_property

deleted theorem category_theory.iso_has_right_lifting_property

deleted theorem category_theory.right_lifting_property_initial_iff

deleted def category_theory.right_lifting_subcat.X

deleted def category_theory.right_lifting_subcat

deleted def category_theory.right_lifting_subcategory

Created src/category_theory/lifting_properties/basic.lean

added theorem category_theory.has_lifting_property.iff_op

added theorem category_theory.has_lifting_property.iff_unop

added theorem category_theory.has_lifting_property.op

added theorem category_theory.has_lifting_property.unop

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

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

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

added theorem category_theory.strong_epi.mk'

added theorem category_theory.strong_mono.mk'