Mathlib Changelog
Changelog
About
Github
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'