[Merged by Bors] - feat(category_theory/lifting_properties): create a new file about lifting properties

[JakobScholbach]

This file introduces lifting properties, establishes a few basic properties, and constructs a subcategory spanned by morphisms having a right lifting property.

---

[semorrison]

I wonder if we should just add

instance {X Y : T} : has_coe (X ⟶ Y) (arrow T) := ⟨mk⟩

back in category_theory.arrow.

[JakobScholbach]

I wonder if we should just add

instance {X Y : T} : has_coe (X ⟶ Y) (arrow T) := ⟨mk⟩

back in category_theory.arrow.

I am very new to all these of optimisation thoughts, so I am certainly the wrong person to ask.

[TwoFX]

Given that both has_lift and strong_epi (which is in many ways similar to has_lifting_property) are classes, I think that there's a case to be made for also making has_lifting_property a class and providing an instance [has_lifting_property i p] (sq : i ⟶ p) : has_lift sq. This would also make working with lifting properties more smooth because you don't have to write haveI := ... for every lift that you want to take.

@semorrison, @JakobScholbach, what do you think?

[JakobScholbach]

Given that both has_lift and strong_epi (which is in many ways similar to has_lifting_property) are classes, I think that there's a case to be made for also making has_lifting_property a class and providing an instance [has_lifting_property i p] (sq : i ⟶ p) : has_lift sq. This would also make working with lifting properties more smooth because you don't have to write haveI := ... for every lift that you want to take.

@semorrison, @JakobScholbach, what do you think?

I have tried my hand with this. This does nicely simplify has_right_lifting_property_comp. I also feel that some turns in the proof of right_lifting_property_initial_iff should be unnecessary, but I don't quite see how.

[jcommelin]

Minor comments. Looking good! Thanks a lot

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests