Theorems · Definition · category theory
CategoryTheory.CartesianMonoidalCategory.lift
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
{T X Y : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)Constructs a morphism to the product given its two components.
- Cited by
- 160 results in Mathlib
- Foundations
- Depth 26 from the axioms, rests on 151 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
- CategoryTheory.CartesianMonoidalCategorystatement and proof · cited by 947
- CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProductproof · cited by 6
- CategoryTheory.Limits.BinaryFan.IsLimit.lift'proof · cited by 5
Cited by191
Results whose statement or proof uses this declaration.
- CategoryTheory.CartesianMonoidalCategory.prodComparisonproof · cited by 41
- CategoryTheory.CartesianMonoidalCategory.lift_sndstatement · cited by 37
- CategoryTheory.CartesianMonoidalCategory.lift_fststatement · cited by 36
- SSet.ι₀proof · cited by 18
- SSet.ι₁proof · cited by 18
- CategoryTheory.CartesianMonoidalCategory.comp_liftstatement and proof · cited by 13
- TopCat.ι₀proof · cited by 11
- TopCat.ι₁proof · cited by 11
- CategoryTheory.CartesianMonoidalCategory.lift_fst_sndstatement and proof · cited by 10
- CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assocstatement and proof · cited by 9
- CategoryTheory.ModObj.leftSMulproof · cited by 8
- CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assocstatement and proof · cited by 7