Lifting properties #
This file defines the lifting property of two arrows in a category and shows basic properties of this notion. We also construct the subcategory consisting of those morphisms which have the right lifting property with respect to arrows in a given diagram.
Main results #
has_lifting_property: the definition of the lifting propertyiso_has_right_lifting_property: any isomorphism satisfies the right lifting property (rlp)id_has_right_lifting_property: any identity has the rlpright_lifting_property_initial_iff: spells out the rlp with respect to a map whose source is an initial objectright_lifting_subcat: given a set of arrowsF : D → arrow C, we construct the subcategory of those morphismspinCthat satisfy the rlp w.r.t.F i, for any elementiofD.
Tags #
lifting property
- sq_has_lift : ∀ (sq : i ⟶ p), category_theory.arrow.has_lift sq
The lifting property of a morphism i with respect to a morphism p.
This can be interpreted as the right lifting property of i with respect to p,
or the left lifting property of p with respect to i.
Any isomorphism has the right lifting property with respect to any map. A → X ↓i ↓p≅ B → Y
Informal translation
Let $C$ be a category and let $X, Y$ be objects of $C$. Let $i:X\to Y$ be an arrow of $C$. If $X$ and $Y$ are isomorphic, then $i$ has the right lifting property with respect to $X$.
Any identity has the right lifting property with respect to any map.
Informal translation
The identity morphism has the right lifting property with respect to any morphism.
An equivalent characterization for right lifting with respect to a map i whose source is
initial.
∅ → X
↓ ↓
B → Y has a lifting iff there is a map B → X making the right part commute.
Informal translation
Let $C$ be a category and let $i, p:C\to D$ be functors. If $i$ is initial, then $i$ has the right lifting property with respect to $p$ if and only if for every morphism $e:i\to p$ there is a morphism $l:i\to p$ such that $l\circ p=e$.
The condition of having the rlp with respect to a morphism i is stable under composition.
Informal translation
Let $C$ be a category. Let $X, Y, Z$ be objects of $C$ and let $i:X\to Y$ be an arrow. Let $f:X\to Y$ and $g:Y\to Z$ be arrows. If $f$ and $g$ have the right lifting property with respect to $i$, then $g\circ f$ has the right lifting property with respect to $i$.
The objects of the subcategory right_lifting_subcategory are the ones in the
underlying category.
Equations
Instances for category_theory.right_lifting_subcat
Equations
The objects of the subcategory right_lifting_subcategory are the ones in the
underlying category.
Informal translation
Let $C$ be a category and let $F:D\to C$ be a functor. Then the identity functor on $C$ has the right lifting property with respect to $F$.
Informal translation
Let $C$ be a category and let $F:D\to C$ be a functor. Suppose that for each $i\in D$ and each morphism $f:X\to Y$ in $C$, there is a morphism $F(i)(f):F(i)(X)\to F(i)(Y)$ in $C$ such that the following diagram commutes:
$$\require{AMScd}
\begin{CD}
F(i)(X) @>{F(i)(f)}>> F(i)(Y)\
@VVV @VVV\
X @>{f}>> Y
\end{CD
Given a set of arrows in C, indexed by F : D → arrow C,
we construct the (non-full) subcategory of C
spanned by those morphisms that have the right lifting property relative to all maps
of the form F i, where i is any element in D.
Equations
- category_theory.right_lifting_subcategory F = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.right_lifting_subcat C), {p // ∀ {i : D}, category_theory.has_lifting_property (F i) (category_theory.arrow.mk p)}}, id := λ (X : category_theory.right_lifting_subcat C), ⟨𝟙 X, _⟩, comp := λ (X Y Z : category_theory.right_lifting_subcat C) (f : X ⟶ Y) (g : Y ⟶ Z), ⟨f.val ≫ g.val, _⟩}, id_comp' := _, comp_id' := _, assoc' := _}