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}
[Category.{u_2, u_1} C]
{X Y Z W : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
{g : Z ⟶ W}
{t : Y ⟶ W}
(h : IsPushout s f g t)
{Z' W' : C}
(g' : Z' ⟶ W')
[HasLiftingProperty f g']
:
HasLiftingProperty g g'
theorem
CategoryTheory.IsPullback.hasLiftingProperty
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y Z W : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
{g : Z ⟶ W}
{t : Y ⟶ W}
(h : IsPullback s f g t)
{X' Y' : C}
(f' : X' ⟶ Y')
[HasLiftingProperty f' g]
:
HasLiftingProperty f' f
instance
CategoryTheory.instHasLiftingPropertyInl
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y Z : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
[Limits.HasPushout s f]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[HasLiftingProperty f p]
:
HasLiftingProperty (Limits.pushout.inl s f) p
instance
CategoryTheory.instHasLiftingPropertyInr
{C : Type u_1}
[Category.{u_2, u_1} C]
{X Y Z : C}
{f : X ⟶ Y}
{s : X ⟶ Z}
[Limits.HasPushout s f]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[HasLiftingProperty s p]
:
HasLiftingProperty (Limits.pushout.inr s f) p
instance
CategoryTheory.instHasLiftingPropertySnd
{C : Type u_1}
[Category.{u_2, u_1} C]
{Y Z W : C}
{g : Z ⟶ W}
{t : Y ⟶ W}
[Limits.HasPullback g t]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[HasLiftingProperty p g]
:
instance
CategoryTheory.instHasLiftingPropertyFst
{C : Type u_1}
[Category.{u_2, u_1} C]
{Y Z W : C}
{g : Z ⟶ W}
{t : Y ⟶ W}
[Limits.HasPullback g t]
{T₁ T₂ : C}
(p : T₁ ⟶ T₂)
[HasLiftingProperty p t]
:
instance
CategoryTheory.instHasLiftingPropertyMap
{C : Type u_1}
[Category.{u_3, u_1} C]
{J : Type u_2}
{A B : J → C}
[Limits.HasProduct A]
[Limits.HasProduct B]
(f : (j : J) → A j ⟶ B j)
{X Y : C}
(p : X ⟶ Y)
[∀ (j : J), HasLiftingProperty p (f j)]
:
instance
CategoryTheory.instHasLiftingPropertyMap_1
{C : Type u_1}
[Category.{u_3, u_1} C]
{J : Type u_2}
{A B : J → C}
[Limits.HasCoproduct A]
[Limits.HasCoproduct B]
(f : (j : J) → A j ⟶ B j)
{X Y : C}
(p : X ⟶ Y)
[∀ (j : J), HasLiftingProperty (f j) p]
: