Theorems · Definition · category theory
AugmentedSimplexCategory.inl
(x y : AugmentedSimplexCategory) → x ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y
Thanks to tensorUnit being initial in AugmentedSimplexCategory, we get
a morphism Δ ⟶ Δ ⊗ Δ' for every pair of objects Δ, Δ'.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Iso.invproof · cited by 6,514
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
- SimplexCategorystatement · cited by 2,204
- CategoryTheory.MonoidalCategoryStruct.whiskerLeftproof · cited by 915
- CategoryTheory.MonoidalCategoryStruct.rightUnitorproof · cited by 397
- CategoryTheory.Limits.IsInitial.toproof · cited by 119
- AugmentedSimplexCategorystatement and proof · cited by 66
- CategoryTheory.WithInitial.starInitialproof · cited by 23
Cited by10
Results whose statement or proof uses this declaration.
- AugmentedSimplexCategory.inl'proof · cited by 5
- AugmentedSimplexCategory.tensorObj_hom_extstatement and proof · cited by 3
- AugmentedSimplexCategory.inl_comp_tensorHomstatement and proof · cited by 2
- AugmentedSimplexCategory.inl_comp_inl_comp_associatorstatement and proof · cited by 1
- AugmentedSimplexCategory.inl_comp_tensorHom_assocstatement and proof · cited by 1
- AugmentedSimplexCategory.inr_comp_inl_comp_associatorstatement and proof · cited by 1
- AugmentedSimplexCategory.tensorHom_comp_tensorHomproof · cited by 1
- AugmentedSimplexCategory.tensorObj_hom_ext_iffstatement and proof · cited by 0
- AugmentedSimplexCategory.inl_comp_inl_comp_associator_assocstatement and proof · cited by 0
- AugmentedSimplexCategory.inr_comp_inl_comp_associator_assocstatement and proof · cited by 0