Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_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] {X Y Z : CategoryTheory.Arrow C},
  CategoryTheory.HasLiftingProperty (X □ Y).hom Z.hom ↔ CategoryTheory.HasLiftingProperty Y.hom (Opposite.op X ⋔ Z).hom

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

Defined in

Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

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