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	18 math math: CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, 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, CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, commMonFunctorCategoryEquivalence_functor, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, commMonFunctorCategoryEquivalence_inverse
functorCategoryMonoidal 📖	CompOp	93 math math: MonFunctorCategoryEquivalence.inverse_obj, CategoryTheory.Functor.instIsLeftAdjointDiscreteTensorLeftCompIncl, CategoryTheory.MonoidalCategory.externalProductCompDiagIso_hom_app_app, Action.leftUnitor_inv_hom, CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, Action.whiskerRight_hom, CategoryTheory.IsSifted.factorization_prodComparison_colim, CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, MonFunctorCategoryEquivalence.functorObjObj_mon_one, Action.FunctorCategoryEquivalence.functor_δ, MonFunctorCategoryEquivalence.functorObjObj_mon_mul, CategoryTheory.GrothendieckTopology.W.transport_isMonoidal, monFunctorCategoryEquivalence_unitIso, CategoryTheory.Functor.ihom_ev_app, monFunctorCategoryEquivalence_functor, CategoryTheory.Mon.limit_mon_mul, 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.instIsMonoidalFunctorCongrLeft, CategoryTheory.Functor.Monoidal.whiskeringLeft_μ_app, CategoryTheory.Limits.lim_ε_π_assoc, ComonFunctorCategoryEquivalence.inverseObj_X, 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, 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.Functor.LaxMonoidal.whiskeringRight_ε_app, ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Limits.lim_μ_π_assoc, CategoryTheory.η_app, CommMonFunctorCategoryEquivalence.inverse_obj_X_map, Action.tensorHom_hom, Action.associator_hom_hom, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, comonFunctorCategoryEquivalence_counitIso, 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, MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, Action.FunctorCategoryEquivalence.functor_μ, CategoryTheory.Functor.closedCounit_app_app, CategoryTheory.Mon.limit_mon_one, 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.Functor.Monoidal.whiskeringLeft_δ_app, Action.rightUnitor_inv_hom, MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, CategoryTheory.Limits.lim_μ_π, CategoryTheory.ε_app, monFunctorCategoryEquivalence_inverse, CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, commMonFunctorCategoryEquivalence_inverse, Action.leftUnitor_hom_hom, Action.FunctorCategoryEquivalence.functor_η, CategoryTheory.μ_app, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, Action.FunctorCategoryEquivalence.functor_ε
functorCategoryMonoidalStruct 📖	CompOp	42 math math: tensorHom_app, CategoryTheory.Enriched.Functor.associator_inv_apply, CategoryTheory.Functor.natTransEquiv_apply_app, CategoryTheory.Functor.homObjEquiv_apply_app, leftUnitor_hom_app, CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_comp, CategoryTheory.Enriched.Functor.whiskerLeft_app_apply, associator_hom_app, CategoryTheory.Functor.homObjEquiv_symm_apply_app, tensorUnit_map, CategoryTheory.Functor.natTransEquiv_symm_apply_app, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, whiskerRight_app, tensorUnit_obj, tensorObj_obj, CategoryTheory.Enriched.Functor.associator_hom_apply, rightUnitor_inv_app, CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp, CategoryTheory.Enriched.Functor.whiskerRight_app_apply, CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply, leftUnitor_inv_app, CategoryTheory.GrothendieckTopology.W.whiskerLeft, CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp_app, CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app, CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, rightUnitor_hom_app, CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp_assoc, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm, associator_inv_app, CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc_assoc, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_id, tensorObj_map, CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three, whiskerLeft_app, CategoryTheory.Enriched.FunctorCategory.functorEnrichedId_app, 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