mathlibdocumentation

category_theory.lifting_properties

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 property
• iso_has_right_lifting_property: any isomorphism satisfies the right lifting property (rlp)
• id_has_right_lifting_property: any identity has the rlp
• right_lifting_property_initial_iff: spells out the rlp with respect to a map whose source is an initial object
• right_lifting_subcat: given a set of arrows F : D → arrow C, we construct the subcategory of those morphisms p in C that satisfy the rlp w.r.t. F i, for any element i of D.

Tags #

lifting property

@[class]
structure category_theory.has_lifting_property {C : Type u} (i p : category_theory.arrow C) :
Prop
• sq_has_lift : ∀ (sq : i p),

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.

@[protected, instance]
def category_theory.has_lifting_property' {C : Type u} {i p : category_theory.arrow C} (sq : i p) :
theorem category_theory.iso_has_right_lifting_property {C : Type u} {X Y : C} (i : category_theory.arrow C) (p : X Y) :

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.

theorem category_theory.right_lifting_property_initial_iff {C : Type u} (i p : category_theory.arrow C)  :
∀ {e : i.right p.right}, ∃ (l : i.right p.left), l p.hom = e

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.

theorem category_theory.has_right_lifting_property_comp {C : Type u} {X Y Z : C} {i : category_theory.arrow C} {f : X Y} {g : Y Z}  :

The condition of having the rlp with respect to a morphism i is stable under composition.

def category_theory.right_lifting_subcat (R : Type u) :
Type u

The objects of the subcategory right_lifting_subcategory are the ones in the underlying category.

Equations
Instances for category_theory.right_lifting_subcat
@[protected, instance]
Equations

The objects of the subcategory right_lifting_subcategory are the ones in the underlying category.

Equations
theorem category_theory.id_has_right_lifting_property' {C : Type u} {D : Type v₁} {F : D → } (X : C) (i : D) :
theorem category_theory.has_right_lifting_property_comp' {C : Type u} {D : Type v₁} {X Y Z : C} {F : D → } {f : X Y} (hf : ∀ (i : D), ) {g : Y Z} (hg : ∀ (i : D), ) (i : D) :
def category_theory.right_lifting_subcategory {C : Type u} {D : Type v₁} (F : D → ) :

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