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 morphismsp
inC
that satisfy the rlp w.r.t.F i
, for any elementi
ofD
.
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
Any identity has the right lifting property with respect to any map.
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.
The condition of having the rlp with respect to a morphism i
is stable under composition.
The objects of the subcategory right_lifting_subcategory
are the ones in the
underlying category.
Equations
Equations
- category_theory.right_lifting_subcat.inhabited R = {default := default _inst_2}
The objects of the subcategory right_lifting_subcategory
are the ones in the
underlying category.
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' := _}