Monoidal

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

Statistics

Metric	Count
Definitions prod, instCartesianMonoidalCategory, instMonoidalClosed, instMonoidalTruncation, instCartesianMonoidalCategory, instMonoidalClosed, isTerminalObj₀, unitHomEquiv, ι₀, ι₁	10
Theorems prod_monotone, prod_obj, range_tensorHom, tensor_map_apply_fst, tensor_map_apply_snd, associator_hom_app_apply, associator_inv_app_apply, instFiniteObjOppositeSimplexCategoryTensorObj, instFiniteTensorUnit, instHasDimensionLETensorUnitOfNatNat, leftUnitor_hom_app_apply, leftUnitor_inv_app_apply, rightUnitor_hom_app_apply, rightUnitor_inv_app_apply, ext₀, ext₀_iff, tensorHom_app_apply, whiskerLeft_app_apply, whiskerRight_app_apply, ι₀_app_fst, ι₀_comp, ι₀_comp_assoc, ι₀_fst, ι₀_fst_assoc, ι₀_snd, ι₀_snd_assoc, ι₁_app_fst, ι₁_comp, ι₁_comp_assoc, ι₁_fst, ι₁_fst_assoc, ι₁_snd, ι₁_snd_assoc	33
Total	43

SSet

Definitions

Name	Category	Theorems
instCartesianMonoidalCategory 📖	CompOp	68 math math: ι₀_snd_assoc, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, iSup_subcomplexOfSimplex_prod_eq_top, instHasDimensionLETensorUnitOfNatNat, tensorHom_app_apply, prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, hasDimensionLT_prod, RelativeMorphism.Homotopy.h₀_assoc, prodStdSimplex.objEquiv_apply_fst, instFiniteTensorUnit, prodStdSimplex.strictMono_orderHomOfSimplex_iff, Subcomplex.ofSimplexProd_eq_range, prodStdSimplex.objEquiv_δ_apply, prodStdSimplex.objEquiv_naturality, instFiniteTensorObj, prodStdSimplex.objEquiv_apply_snd, hoFunctor.unitHomEquiv_eq, instFiniteObjOppositeSimplexCategoryTensorObj, leftUnitor_inv_app_apply, ι₀_fst_assoc, ι₁_comp, whiskerRight_app_apply, rightUnitor_inv_app_apply, ι₀_snd, CategoryTheory.SimplicialThickening.functor_map, ι₁_snd_assoc, instHasDimensionLETensorObjHAddNat, ι₁_app_fst, ι₁_snd, whiskerLeft_app_apply, Subcomplex.prod_obj, instHasDimensionLTTensorObjHAddNat, prodStdSimplex.objEquiv_map_apply, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, Subcomplex.prod_monotone, ι₀_comp_assoc, ι₀_comp, RelativeMorphism.Homotopy.h₁_assoc, RelativeMorphism.Homotopy.ofEq_h, rightUnitor_hom_app_apply, ι₁_fst, prodStdSimplex.nonDegenerate_iff_injective_objEquiv, RelativeMorphism.Homotopy.h₀, RelativeMorphism.Homotopy.precomp_h, ι₀_fst, associator_hom_app_apply, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, RelativeMorphism.Homotopy.h₁, Subcomplex.range_tensorHom, RelativeMorphism.Homotopy.postcomp_h, prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, RelativeMorphism.Homotopy.rel, RelativeMorphism.Homotopy.refl_h, CategoryTheory.SimplicialThickening.functor_id, hasDimensionLE_prod, ι₁_fst_assoc, leftUnitor_hom_app_apply, associator_inv_app_apply, CategoryTheory.hoFunctor.isIso_prodComparison, CategoryTheory.SimplicialThickening.functor_obj_as, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, CategoryTheory.SimplicialThickening.functor_comp, ι₀_app_fst, ι₁_comp_assoc, RelativeMorphism.Homotopy.rel_assoc
instMonoidalClosed 📖	CompOp	—
unitHomEquiv 📖	CompOp	—
ι₀ 📖	CompOp	9 math math: ι₀_snd_assoc, RelativeMorphism.Homotopy.h₀_assoc, ι₀_fst_assoc, ι₀_snd, ι₀_comp_assoc, ι₀_comp, RelativeMorphism.Homotopy.h₀, ι₀_fst, ι₀_app_fst
ι₁ 📖	CompOp	9 math math: ι₁_comp, ι₁_snd_assoc, ι₁_app_fst, ι₁_snd, RelativeMorphism.Homotopy.h₁_assoc, ι₁_fst, RelativeMorphism.Homotopy.h₁, ι₁_fst_assoc, ι₁_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.obj	—	—
associator_inv_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.obj	—	—
instFiniteObjOppositeSimplexCategoryTensorObj 📖	mathematical	—	Finite CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	Finite.instProd
instFiniteTensorUnit 📖	mathematical	—	Finite CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	finite_of_iso stdSimplex.instFiniteObjSimplexCategory
instHasDimensionLETensorUnitOfNatNat 📖	mathematical	—	HasDimensionLE CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	hasDimensionLT_iff_of_iso stdSimplex.instHasDimensionLEObjSimplexCategoryMk
leftUnitor_hom_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.obj	—	—
leftUnitor_inv_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.obj	—	—
rightUnitor_hom_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.obj	—	—
rightUnitor_inv_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.obj	—	—
tensorHom_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.obj	—	—
whiskerLeft_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.obj	—	—
whiskerRight_app_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj SSet largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.obj	—	—
ι₀_app_fst 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet largeCategory stdSimplex CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory ι₀	—	—
ι₀_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι₀_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_comp
ι₀_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	—
ι₀_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₀_fst
ι₀_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.SemiCartesianMonoidalCategory.snd const DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm stdSimplex.obj₀Equiv	—	—
ι₀_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₀ CategoryTheory.SemiCartesianMonoidalCategory.snd const DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm stdSimplex.obj₀Equiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_snd
ι₁_app_fst 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet largeCategory stdSimplex CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory ι₁	—	—
ι₁_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι₁_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_comp
ι₁_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	—
ι₁_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₁_fst
ι₁_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.SemiCartesianMonoidalCategory.snd const DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm stdSimplex.obj₀Equiv	—	—
ι₁_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory stdSimplex ι₁ CategoryTheory.SemiCartesianMonoidalCategory.snd const DFunLike.coe Equiv Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm stdSimplex.obj₀Equiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_snd

SSet.Subcomplex

Definitions

Name	Category	Theorems
prod 📖	CompOp	5 math math: SSet.iSup_subcomplexOfSimplex_prod_eq_top, ofSimplexProd_eq_range, prod_obj, prod_monotone, range_tensorHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_monotone 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.MonoidalCategoryStruct.tensorObj SSet SSet.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory prod	—	—
prod_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj SSet SSet.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory prod Set.prod CategoryTheory.Functor.obj CategoryTheory.types	—	—
range_tensorHom 📖	mathematical	—	range CategoryTheory.MonoidalCategoryStruct.tensorObj SSet SSet.largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom prod	—	CategoryTheory.Subfunctor.ext Set.ext Prod.eq_iff_fst_eq_snd_eq

SSet.Truncated

Definitions

Name	Category	Theorems
instCartesianMonoidalCategory 📖	CompOp	36 math math: HomotopyCategory.BinaryProduct.iso_inv_toFunctor, tensor_map_apply_snd, HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, Edge.map_fst, HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, Edge.CompStruct.tensor_simplex_snd, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, Edge.id_tensor_id, HomotopyCategory.BinaryProduct.left_unitality, Edge.CompStruct.tensor_simplex_fst, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, Edge.map_associator_hom, HomotopyCategory.BinaryProduct.iso_hom_toFunctor, Edge.map_whiskerLeft, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, Edge.map_snd, HomotopyCategory.BinaryProduct.functor_comp_inverse, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, HomotopyCategory.BinaryProduct.inverse_comp_functor, Edge.map_tensorHom, HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, tensor_map_apply_fst, HomotopyCategory.BinaryProduct.functor_obj, Edge.tensor_edge, HomotopyCategory.BinaryProduct.square, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, HomotopyCategory.BinaryProduct.associativity, HomotopyCategory.BinaryProduct.right_unitality, HomotopyCategory.BinaryProduct.associativityIso_hom_app, Edge.map_whiskerRight, HomotopyCategory.BinaryProduct.functor_map, HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, HomotopyCategory.BinaryProduct.inverse_obj
instMonoidalClosed 📖	CompOp	—
instMonoidalTruncation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_map_apply_fst 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	—
tensor_map_apply_snd 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj SSet.Truncated largeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory	—	—

SSet.stdSimplex

Definitions

Name	Category	Theorems
isTerminalObj₀ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext₀ 📖	—	—	—	—	CategoryTheory.Limits.IsTerminal.hom_ext
ext₀_iff 📖	—	—	—	—	ext₀

---

← Back to Index