mathlib documentation

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 #

Tags #

lifting property

@[class]

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.

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

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

Equations

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