Commit 2026-04-27 21:20 95b575de
View on Github →feat(CategoryTheory/Monoidal/PushoutProduct): isomorphisms and lifting properties of pushout-products (#37198)
Defines various isomorphisms of pushout-products.
Defines an isomorphism in the arrow category of SSet between the canonical inclusion (S.unionProd T).toSSet ⟶ X ⊗ Y and the pushout-product S.ι □ T.ι.
Proves various equivalent lifting properties involving pushout-products
Estimated changes
added theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'
added theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff
added theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff'