Lifting properties and (co)limits #
In this file, we show some consequences of lifting properties in the presence of certain (co)limits.
theorem
CategoryTheory.IsPushout.hasLiftingProperty
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X Y Z W : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
{g : Z ⟶ W}
{t : Y ⟶ W}
(h : CategoryTheory.IsPushout s f g t)
{Z' W' : C}
(g' : Z' ⟶ W')
[CategoryTheory.HasLiftingProperty f g']
:
theorem
CategoryTheory.IsPullback.hasLiftingProperty
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X Y Z W : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
{g : Z ⟶ W}
{t : Y ⟶ W}
(h : CategoryTheory.IsPullback s f g t)
{X' Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.HasLiftingProperty f' g]
:
instance
CategoryTheory.instHasLiftingPropertyInl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X Y Z : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
[CategoryTheory.Limits.HasPushout s f]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[CategoryTheory.HasLiftingProperty f p]
:
instance
CategoryTheory.instHasLiftingPropertyInr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X Y Z : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
[CategoryTheory.Limits.HasPushout s f]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[CategoryTheory.HasLiftingProperty s p]
:
instance
CategoryTheory.instHasLiftingPropertySnd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Y Z W : C}
{g : Z ⟶ W}
{t : Y ⟶ W}
[CategoryTheory.Limits.HasPullback g t]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[CategoryTheory.HasLiftingProperty p g]
:
instance
CategoryTheory.instHasLiftingPropertyFst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Y Z W : C}
{g : Z ⟶ W}
{t : Y ⟶ W}
[CategoryTheory.Limits.HasPullback g t]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[CategoryTheory.HasLiftingProperty p t]
:
instance
CategoryTheory.instHasLiftingPropertyMap
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{J : Type u_2}
{A B : J → C}
[CategoryTheory.Limits.HasProduct A]
[CategoryTheory.Limits.HasProduct B]
(f : (j : J) → A j ⟶ B j)
{X Y : C}
(p : X ⟶ Y)
[∀ (j : J), CategoryTheory.HasLiftingProperty p (f j)]
:
instance
CategoryTheory.instHasLiftingPropertyMap_1
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{J : Type u_2}
{A B : J → C}
[CategoryTheory.Limits.HasCoproduct A]
[CategoryTheory.Limits.HasCoproduct B]
(f : (j : J) → A j ⟶ B j)
{X Y : C}
(p : X ⟶ Y)
[∀ (j : J), CategoryTheory.HasLiftingProperty (f j) p]
: