# 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

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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?

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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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.

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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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.

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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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) :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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) :
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

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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