Lifting properties #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the lifting property of two morphisms in a category and
shows basic properties of this notion.
Main results #
has_lifting_property: the definition of the lifting property
- define llp/rlp with respect to a
- retracts, direct/inverse images, (co)products, adjunctions
has_lifting_property i p means that
i has the left lifting
property with respect to
p, or equivalently that
the right lifting property with respect to
Instances of this typeclass