FunctorCategory

📁 Source: Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Statistics

Metric	Count
Definitions whiskeringRight, whiskeringLeft, whiskeringRight, tensorHom, tensorObj, whiskerLeft, whiskerRight, functorCategoryBraided, functorCategoryMonoidal, functorCategoryMonoidalStruct, functorCategorySymmetric, instLaxMonoidalFunctorObjWhiskeringRight, instMonoidalFunctorFunctorCongrLeft, instMonoidalFunctorInverseCongrLeft, instMonoidalFunctorObjWhiskeringRight, instOplaxMonoidalFunctorObjWhiskeringRight	16
Theorems whiskeringRight_ε_app, whiskeringRight_μ_app, whiskeringLeft_δ_app, whiskeringLeft_ε_app, whiskeringLeft_η_app, whiskeringLeft_μ_app, whiskeringRight_δ_app, whiskeringRight_η_app, tensorHom_app, tensorObj_map, tensorObj_obj, whiskerLeft_app, whiskerRight_app, associator_hom_app, associator_inv_app, leftUnitor_hom_app, leftUnitor_inv_app, rightUnitor_hom_app, rightUnitor_inv_app, tensorHom_app, tensorObj_map, tensorObj_obj, tensorUnit_map, tensorUnit_obj, whiskerLeft_app, whiskerRight_app, instIsMonoidalFunctorCongrLeft, δ_app, ε_app, η_app, μ_app	31
Total	47

CategoryTheory

Definitions

Name	Category	Theorems
instLaxMonoidalFunctorObjWhiskeringRight 📖	CompOp	—
instMonoidalFunctorFunctorCongrLeft 📖	CompOp	1 math math: instIsMonoidalFunctorCongrLeft
instMonoidalFunctorInverseCongrLeft 📖	CompOp	1 math math: instIsMonoidalFunctorCongrLeft
instMonoidalFunctorObjWhiskeringRight 📖	CompOp	—
instOplaxMonoidalFunctorObjWhiskeringRight 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidalFunctorCongrLeft 📖	mathematical	—	Equivalence.IsMonoidal Functor Functor.category Monoidal.functorCategoryMonoidal Equivalence.congrLeft instMonoidalFunctorFunctorCongrLeft instMonoidalFunctorInverseCongrLeft	—	NatTrans.ext' Equivalence.funInvIdAssoc_inv_app Category.comp_id Equivalence.invFunIdAssoc_hom_app Category.id_comp MonoidalCategory.tensorHom_comp_tensorHom Equivalence.functor_unit_comp Functor.map_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight
δ_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.whiskeringRight MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Monoidal.functorCategoryMonoidal Functor.OplaxMonoidal.δ Functor.OplaxMonoidal.whiskeringRight	—	Functor.OplaxMonoidal.whiskeringRight_δ_app
ε_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorUnit Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct Monoidal.functorCategoryMonoidal Functor.obj Functor.whiskeringRight Functor.LaxMonoidal.ε Functor.LaxMonoidal.whiskeringRight	—	Functor.LaxMonoidal.whiskeringRight_ε_app
η_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.whiskeringRight MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct Monoidal.functorCategoryMonoidal Functor.OplaxMonoidal.η Functor.OplaxMonoidal.whiskeringRight	—	Functor.OplaxMonoidal.whiskeringRight_η_app
μ_app 📖	mathematical	—	NatTrans.app MonoidalCategoryStruct.tensorObj Functor Functor.category MonoidalCategory.toMonoidalCategoryStruct Monoidal.functorCategoryMonoidal Functor.obj Functor.whiskeringRight Functor.LaxMonoidal.μ Functor.LaxMonoidal.whiskeringRight	—	Functor.LaxMonoidal.whiskeringRight_μ_app

CategoryTheory.Functor.LaxMonoidal

Definitions

Name	Category	Theorems
whiskeringRight 📖	CompOp	4 math math: whiskeringRight_μ_app, whiskeringRight_ε_app, CategoryTheory.ε_app, CategoryTheory.μ_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
whiskeringRight_ε_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight ε whiskeringRight	—	—
whiskeringRight_μ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight μ whiskeringRight	—	—

CategoryTheory.Functor.Monoidal

Definitions

Name	Category	Theorems
whiskeringLeft 📖	CompOp	4 math math: whiskeringLeft_ε_app, whiskeringLeft_μ_app, whiskeringLeft_η_app, whiskeringLeft_δ_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
whiskeringLeft_δ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal whiskeringLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskeringLeft_ε_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal whiskeringLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskeringLeft_η_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal whiskeringLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskeringLeft_μ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal whiskeringLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Functor.OplaxMonoidal

Definitions

Name	Category	Theorems
whiskeringRight 📖	CompOp	4 math math: CategoryTheory.δ_app, whiskeringRight_δ_app, CategoryTheory.η_app, whiskeringRight_η_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
whiskeringRight_δ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal δ whiskeringRight	—	—
whiskeringRight_η_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal η whiskeringRight	—	—

CategoryTheory.Monoidal

Definitions

Name	Category	Theorems
functorCategoryBraided 📖	CompOp	24 math math: CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, SSet.Subcomplex.unionProd.image_β_inv, SSet.Subcomplex.unionProd.symmIso_inv, CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, SSet.Subcomplex.unionProd.image_β_hom, SSet.Subcomplex.unionProd.symmIso_hom, CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, commMonFunctorCategoryEquivalence_counitIso, CommMonFunctorCategoryEquivalence.functor_obj_obj_X, CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, commMonFunctorCategoryEquivalence_unitIso, CommMonFunctorCategoryEquivalence.inverse_obj_X_obj, CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, SSet.Subcomplex.unionProd.preimage_β_inv, CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, SSet.Subcomplex.unionProd.preimage_β_hom, commMonFunctorCategoryEquivalence_functor, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, commMonFunctorCategoryEquivalence_inverse
functorCategoryMonoidal 📖	CompOp	128 math math: MonFunctorCategoryEquivalence.inverse_obj, CategoryTheory.Functor.instIsLeftAdjointDiscreteTensorLeftCompIncl, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, CategoryTheory.MonoidalCategory.externalProductCompDiagIso_hom_app_app, Action.leftUnitor_inv_hom, CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W, Action.whiskerRight_hom, SSet.Subcomplex.unionProd.image_β_inv, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.sheafToPresheaf_μ, SSet.Subcomplex.unionProd.symmIso_inv, CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc, CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, MonFunctorCategoryEquivalence.functorObjObj_mon_one, Action.FunctorCategoryEquivalence.functor_δ, SSet.Subcomplex.unionProd.image_β_hom, CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints, MonFunctorCategoryEquivalence.functorObjObj_mon_mul, CategoryTheory.GrothendieckTopology.W.transport_isMonoidal, monFunctorCategoryEquivalence_unitIso, CategoryTheory.Functor.ihom_ev_app, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, SSet.Subcomplex.unionProd.symmIso_hom, monFunctorCategoryEquivalence_functor, SSet.hoFunctor.unitHomEquiv_eq, CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.ihom_map, MonFunctorCategoryEquivalence.functor_obj, CategoryTheory.δ_app, CategoryTheory.Functor.Monoidal.whiskeringLeft_ε_app, ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber, CategoryTheory.instIsMonoidalFunctorCongrLeft, CategoryTheory.Functor.Monoidal.whiskeringLeft_μ_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ, CategoryTheory.sheafToPresheaf_δ, CategoryTheory.Limits.lim_ε_π_assoc, ComonFunctorCategoryEquivalence.inverseObj_X, CategoryTheory.SimplicialThickening.functor_map, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ_assoc, commMonFunctorCategoryEquivalence_counitIso, CommMonFunctorCategoryEquivalence.functor_obj_obj_X, ComonFunctorCategoryEquivalence.functorObjObj_comon_counit, CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app, CategoryTheory.MonoidalCategory.externalProductCompDiagIso_inv_app_app, CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, MonFunctorCategoryEquivalence.functor_map_app_hom, MonFunctorCategoryEquivalence.inverse_map_hom_app, CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, CategoryTheory.GrothendieckTopology.W.monoidal, ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, comonFunctorCategoryEquivalence_unitIso, CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, commMonFunctorCategoryEquivalence_unitIso, CategoryTheory.Limits.lim_ε_π, CommMonFunctorCategoryEquivalence.inverse_obj_X_obj, MonFunctorCategoryEquivalence.inverseObj_X, comonFunctorCategoryEquivalence_functor, CategoryTheory.Functor.Monoidal.whiskeringLeft_η_app, CategoryTheory.Functor.closedUnit_app_app, CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app, ComonFunctorCategoryEquivalence.functor_obj, CategoryTheory.Functor.ihom_coev_app, CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ, CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Limits.lim_μ_π_assoc, CategoryTheory.η_app, SSet.Subcomplex.unionProd.preimage_β_inv, CommMonFunctorCategoryEquivalence.inverse_obj_X_map, Action.tensorHom_hom, Action.associator_hom_hom, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, SSet.Subcomplex.unionProd.preimage_β_hom, CategoryTheory.Functor.Monoidal.instPreservesColimitsOfShapeTensorLeftOfHasColimitsOfShape, ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, comonFunctorCategoryEquivalence_counitIso, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η, CategoryTheory.sheafToPresheaf_η, MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, Action.whiskerLeft_hom, ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, ComonFunctorCategoryEquivalence.functorObjObj_comon_comul, monFunctorCategoryEquivalence_counitIso, MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, commMonFunctorCategoryEquivalence_functor, CategoryTheory.sheafToPresheaf_ε, MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, Action.FunctorCategoryEquivalence.functor_μ, CategoryTheory.Functor.closedCounit_app_app, CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app, Action.rightUnitor_hom_hom, CategoryTheory.Functor.monoidalClosed_closed_adj, Action.associator_inv_hom, MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, MonFunctorCategoryEquivalence.inverseObj_mon_one_app, comonFunctorCategoryEquivalence_inverse, CategoryTheory.GrothendieckTopology.Point.instIsIsoηFunctorOppositePresheafFiber, CategoryTheory.Functor.Monoidal.whiskeringLeft_δ_app, CategoryTheory.SimplicialThickening.functor_id, Action.rightUnitor_inv_hom, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.SimplicialThickening.functor_obj_as, MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, CategoryTheory.Limits.lim_μ_π, CategoryTheory.ε_app, CategoryTheory.SimplicialThickening.functor_comp, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, monFunctorCategoryEquivalence_inverse, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, commMonFunctorCategoryEquivalence_inverse, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η_assoc, Action.leftUnitor_hom_hom, Action.FunctorCategoryEquivalence.functor_η, CategoryTheory.Sheaf.instIsMonoidalFunctorOppositeIsSheaf, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc, CategoryTheory.μ_app, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, Action.FunctorCategoryEquivalence.functor_ε
functorCategoryMonoidalStruct 📖	CompOp	211 math math: tensorHom_app, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, CategoryTheory.Enriched.Functor.associator_inv_apply, CategoryTheory.Functor.natTransEquiv_apply_app, CategoryTheory.Functor.homObjEquiv_apply_app, SSet.Truncated.tensor_map_apply_snd, SSet.Subcomplex.prod_top_le_unionProd, CategoryTheory.Functor.Monoidal.rightUnitor_inv_app, SSet.Subcomplex.prodIso_hom, leftUnitor_hom_app, SSet.ι₀_snd_assoc, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app, SSet.Subcomplex.mem_unionProd_iff, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_comp, CategoryTheory.Enriched.Functor.whiskerLeft_app_apply, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, SSet.Subcomplex.unionProd.isPushout, SSet.iSup_subcomplexOfSimplex_prod_eq_top, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, SSet.instHasDimensionLETensorUnitOfNatNat, SSet.tensorHom_app_apply, SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SSet.Truncated.Edge.map_fst, associator_hom_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, CategoryTheory.Functor.Monoidal.tensorObj_map, CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app, SSet.prodStdSimplex.nonDegenerateEquiv₁_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, SSet.hasDimensionLT_prod, SSet.RelativeMorphism.Homotopy.h₀_assoc, SSet.Subcomplex.unionProd.image_β_inv, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.Homotopy.h₁_assoc, SSet.Subcomplex.unionProd.symmIso_inv, SSet.instFiniteTensorUnit, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, SSet.prod_δ_snd, SSet.Subcomplex.ofSimplexProd_eq_range, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, CategoryTheory.Functor.homObjEquiv_symm_apply_app, SSet.prod_σ_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, SSet.prodStdSimplex.objEquiv_δ_apply, SSet.Truncated.Edge.id_tensor_id, SSet.Subcomplex.unionProd.image_β_hom, CategoryTheory.Limits.Cocone.tensor_ι_app, SSet.prodStdSimplex.objEquiv_naturality, CategoryTheory.Sheaf.tensorProd_isSheaf, SSet.prod_δ_fst, tensorUnit_map, SSet.instFiniteTensorObj, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, CategoryTheory.Functor.natTransEquiv_symm_apply_app, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, whiskerRight_app, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.Subcomplex.unionProd.symmIso_hom, SSet.hoFunctor.unitHomEquiv_eq, tensorUnit_obj, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, SSet.ι₁_app_snd_apply, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, SSet.prod_map_fst, SSet.whiskerRight_app_apply, SSet.Subcomplex.unionProd.ι₂_ι, SSet.rightUnitor_inv_app_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, tensorObj_obj, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, CategoryTheory.Enriched.Functor.associator_hom_apply, CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ, SSet.ι₀_snd, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, SSet.Homotopy.h₀, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, SSet.Truncated.Edge.map_associator_hom, rightUnitor_inv_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ_assoc, SSet.Subcomplex.unionProd.ι₁_ι, CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp, CategoryTheory.Enriched.Functor.whiskerRight_app_apply, SSet.ι₁_snd_assoc, CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst, SSet.instHasDimensionLETensorObjHAddNat, SSet.ι₁_app_fst, SSet.ι₁_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, SSet.whiskerLeft_app_apply, SSet.Subcomplex.prod_obj, CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app, SSet.Truncated.Edge.map_whiskerLeft, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, SSet.Truncated.Edge.map_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply, SSet.Subcomplex.prod_le_unionProd, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, SSet.Subcomplex.unionProd.ι₁_ι_assoc, SSet.instHasDimensionLTTensorObjHAddNat, leftUnitor_inv_app, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, SSet.prodStdSimplex.objEquiv_map_apply, CategoryTheory.GrothendieckTopology.W.whiskerLeft, CategoryTheory.Functor.Monoidal.tensorHom_app_fst, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd, CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp_app, CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ, SSet.Subcomplex.unionProd.ι₂_ι_assoc, SSet.prodStdSimplex.nonDegenerateEquiv₁_fst, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, SSet.Subcomplex.prod_monotone, SSet.ι₀_comp_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_snd, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, SSet.ι₀_comp, SSet.Homotopy.h₀_assoc, SSet.Homotopy.h₁, SSet.prodStdSimplex.le_orderHomOfSimplex, SSet.RelativeMorphism.Homotopy.h₁_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst, SSet.Subcomplex.prodIso_inv, SSet.Subcomplex.unionProd.preimage_β_inv, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, SSet.RelativeMorphism.Homotopy.ofEq_h, CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, SSet.rightUnitor_hom_app_apply, rightUnitor_hom_app, SSet.Truncated.tensor_map_apply_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, SSet.ι₁_fst, CategoryTheory.Functor.Monoidal.tensorObj_obj, SSet.Truncated.Edge.tensor_edge, SSet.ι₀_app_snd_apply, CategoryTheory.Functor.Monoidal.associator_inv_app, SSet.Subcomplex.unionProd.preimage_β_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.square, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η, CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, SSet.prodStdSimplex.nonDegenerate_max_dim_iff, SSet.Subcomplex.prod_le_top_prod, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm, SSet.RelativeMorphism.Homotopy.h₀, associator_inv_app, SSet.RelativeMorphism.Homotopy.precomp_h, SSet.ι₀_fst, SSet.associator_hom_app_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, SSet.Subcomplex.unionProd.bicartSq, SSet.prod_σ_snd, SSet.RelativeMorphism.Homotopy.h₁, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd, SSet.Subcomplex.range_tensorHom, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, SSet.RelativeMorphism.Homotopy.postcomp_h, SSet.prodStdSimplex.strictMono_orderHomOfSimplex, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, CategoryTheory.Functor.Monoidal.associator_hom_app, SSet.RelativeMorphism.Homotopy.rel, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc_assoc, SSet.Truncated.Edge.map_whiskerRight, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app, SSet.RelativeMorphism.Homotopy.refl_h, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_id, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, SSet.Subcomplex.top_prod_le_unionProd, CategoryTheory.Functor.Monoidal.leftUnitor_hom_app, tensorObj_map, CategoryTheory.Functor.Monoidal.leftUnitor_inv_app, SSet.hasDimensionLE_prod, SSet.ι₁_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, CategoryTheory.Functor.Monoidal.rightUnitor_hom_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε, SSet.leftUnitor_hom_app_apply, SSet.prod_map_snd, SSet.associator_inv_app_apply, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, SSet.Subcomplex.prod_le_prod_top, CategoryTheory.Limits.Cocone.tensor_pt, CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id, CategoryTheory.Sheaf.tensorUnit_isSheaf, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, SSet.ι₀_app_fst, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η_assoc, whiskerLeft_app, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc, SSet.ι₁_comp_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnrichedId_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, SSet.RelativeMorphism.Homotopy.rel_assoc, CategoryTheory.GrothendieckTopology.W.whiskerRight
functorCategorySymmetric 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
associator_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
leftUnitor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
leftUnitor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
rightUnitor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
rightUnitor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
tensorHom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
tensorObj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
tensorObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorUnit_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorUnit_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
whiskerLeft_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
whiskerRight_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—

CategoryTheory.Monoidal.FunctorCategory

Definitions

Name	Category	Theorems
tensorHom 📖	CompOp	1 math math: tensorHom_app
tensorObj 📖	CompOp	5 math math: whiskerLeft_app, tensorObj_map, tensorHom_app, whiskerRight_app, tensorObj_obj
whiskerLeft 📖	CompOp	1 math math: whiskerLeft_app
whiskerRight 📖	CompOp	1 math math: whiskerRight_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorHom_app 📖	mathematical	—	CategoryTheory.NatTrans.app tensorObj tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
tensorObj_map 📖	mathematical	—	CategoryTheory.Functor.map tensorObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
tensorObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj tensorObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
whiskerLeft_app 📖	mathematical	—	CategoryTheory.NatTrans.app tensorObj whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
whiskerRight_app 📖	mathematical	—	CategoryTheory.NatTrans.app tensorObj whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—

---

← Back to Index