Lifting properties and pushout-products / pullback-homs

Various equivalent lifting properties involving pushout-products and pullback-homs. For f : A ⟶ B, g : K ⟶ L, h : X ⟶ Y in a monoidal closed category with pushouts and pullbacks, f □ g lifts against h if and only if g lifts against f ⋔ h.

Special cases are considered when any of A = ∅, K = ∅, or Y = ⋆ are true.

References

• Charles Rezk, Introduction to Quasi-categories, Proposition 21.5

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_iff {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] {X Y Z : Arrow C} : HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty Y.hom (Opposite.op X ⋔ Z).hom

X □ Y lifts against Z if and only if Y lifts against X ⋔ Z.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_iff' {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {X Y Z : Arrow C} : HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

X □ Y lifts against Z if and only if X lifts against Y ⋔ Z.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L} {h : X ⟶ Y} : HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk h).hom

f □ g lifts against h if and only if g lifts against f ⋔ h.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff' {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L} {h : X ⟶ Y} : HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty f (Opposite.op (Arrow.mk g) ⋔ Arrow.mk h).hom

f □ g lifts against h if and only if f lifts against g ⋔ h.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} {h : X ⟶ Y} (i : Limits.IsInitial A) : HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom h ↔ HasLiftingProperty g ((ihom B).map h)

(∅ ⟶ B) □ g lifts against X ⟶ Y if and only if g lifts against B ⟹ X ⟶ B ⟹ Y.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff' {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} {h : X ⟶ Y} (i : Limits.IsInitial K) : HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty f ((ihom L).map h)

f □ (∅ ⟶ L) lifts against X ⟶ Y if and only if f lifts against L ⟹ X ⟶ L ⟹ Y.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isTerminal_iff {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L} (t : Limits.IsTerminal Y) : HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g ((MonoidalClosed.pre f).app X)

f □ g lifts against X ⟶ ⋆ if and only if g lifts against B ⟹ X ⟶ A ⟹ X.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} (i : Limits.IsInitial A) (t : Limits.IsTerminal Y) : HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g (t.from (B ⟹ X))

(∅ ⟶ B) □ g lifts against X ⟶ ⋆ if and only if g lifts against (B ⟹ X) ⟶ ⋆.

theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff' {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasPullbacks C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} (i : Limits.IsInitial K) (t : Limits.IsTerminal Y) : HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔ HasLiftingProperty f (t.from (L ⟹ X))

f □ (∅ ⟶ L) lifts against X ⟶ ⋆ if and only if f lifts against (L ⟹ X) ⟶ ⋆.