Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff

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

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

Defined in

Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Cited by

2 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.Limits.HasPullbacksCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed