Basic

📁 Source: Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean

Statistics

Metric	Count
Definitions associator, instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorLeftObjFunctorTensorBifunctor, instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorRightObjFunctorFlipTensorBifunctor, instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorCurriedTensorObjWhiskeringRightTensorBifunctor, instMonoidalCategoryLocalizedMonoidal, leftUnitor, monoidalCategoryStruct, rightUnitor, tensorBifunctor, tensorBifunctorIso, toMonoidalCategory, ε', μ, instCategoryLocalizedMonoidal, LocalizedMonoidal, IsMonoidal, instMonoidalLocalizedMonoidalToMonoidalCategory	17
Theorems associator_hom_app, associator_naturality, associator_naturality_assoc, associator_naturality₁, associator_naturality₁_assoc, associator_naturality₂, associator_naturality₂_assoc, associator_naturality₃, associator_naturality₃_assoc, id_tensorHom, id_tensorHom_id, instEssSurjLocalizedMonoidalToMonoidalCategory, instIsLocalizationLocalizedMonoidalToMonoidalCategory, isInvertedBy₂, leftUnitor_hom_app, leftUnitor_naturality, pentagon, pentagon_aux₁, pentagon_aux₂, pentagon_aux₃, rightUnitor_hom_app, rightUnitor_naturality, tensorHom_id, tensor_comp, tensor_comp_assoc, triangle, triangle_aux₁, triangle_aux₁_assoc, triangle_aux₂, triangle_aux₃, whiskerLeft_comp, whiskerLeft_comp_assoc, whiskerLeft_id, whiskerRight_comp, whiskerRight_comp_assoc, whiskerRight_id, whisker_exchange, whisker_exchange_assoc, μ_inv_natural_left, μ_inv_natural_left_assoc, μ_inv_natural_right, μ_inv_natural_right_assoc, μ_natural_left, μ_natural_left_assoc, μ_natural_right, μ_natural_right_assoc, mk', toIsMultiplicative, whiskerLeft, whiskerRight, instIsMonoidalInverseImageOfMonoidalOfRespectsIso, tensorHom_mem, whiskerLeft_mem, whiskerRight_mem, associator_hom, associator_inv	56
Total	73

CategoryTheory

Definitions

Name	Category	Theorems
LocalizedMonoidal 📖	CompOp	58 math math: Localization.Monoidal.leftUnitor_hom_app, Localization.Monoidal.whiskerLeft_comp, Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1, Localization.Monoidal.associator_hom_app, Localization.Monoidal.pentagon_aux₁, Localization.Monoidal.μ_inv_natural_right, Localization.Monoidal.pentagon_aux₂, Localization.Monoidal.whiskerRight_comp, Localization.Monoidal.triangle_aux₃, Localization.Monoidal.id_tensorHom, Localization.Monoidal.μ_natural_right, Localization.Monoidal.triangle_aux₁_assoc, Localization.Monoidal.associator_naturality₃, Localization.Monoidal.map_hexagon_forward, Localization.Monoidal.μ_natural_left_assoc, Localization.Monoidal.map_hexagon_reverse, Localization.Monoidal.tensorHom_id, Localization.Monoidal.triangle_aux₁, associator_inv, Localization.Monoidal.map_hexagon_reverse_assoc, Localization.Monoidal.μ_natural_left, Localization.Monoidal.rightUnitor_naturality, Localization.Monoidal.whiskerRight_id, Localization.Monoidal.whisker_exchange, Localization.Monoidal.whisker_exchange_assoc, Localization.Monoidal.μ_inv_natural_left_assoc, Localization.Monoidal.associator_naturality₂, Localization.Monoidal.μ_inv_natural_right_assoc, Localization.Monoidal.associator_naturality₁_assoc, Localization.Monoidal.associator_naturality_assoc, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc, Localization.Monoidal.whiskerRight_comp_assoc, Localization.Monoidal.associator_naturality₂_assoc, Localization.Monoidal.tensor_comp_assoc, Localization.Monoidal.pentagon_aux₃, Localization.Monoidal.leftUnitor_naturality, Localization.Monoidal.triangle, Localization.Monoidal.associator_naturality, Localization.Monoidal.id_tensorHom_id, Localization.Monoidal.triangle_aux₂, Localization.Monoidal.β_hom_app, Localization.Monoidal.whiskerLeft_id, Localization.Monoidal.braidingNatIso_hom_app, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left, Localization.Monoidal.μ_natural_right_assoc, Localization.Monoidal.whiskerLeft_comp_assoc, Localization.Monoidal.pentagon, Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory, Localization.Monoidal.μ_inv_natural_left, Localization.Monoidal.associator_naturality₃_assoc, Localization.Monoidal.rightUnitor_hom_app, Localization.Monoidal.tensor_comp, Localization.Monoidal.associator_naturality₁, Localization.Monoidal.instEssSurjLocalizedMonoidalToMonoidalCategory, Localization.Monoidal.map_hexagon_forward_assoc, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right, associator_hom, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc
instMonoidalLocalizedMonoidalToMonoidalCategory 📖	CompOp	8 math math: associator_inv, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc, Localization.Monoidal.β_hom_app, Localization.Monoidal.braidingNatIso_hom_app, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right, associator_hom, Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom 📖	mathematical	—	Iso.hom LocalizedMonoidal Localization.instCategoryLocalizedMonoidal MonoidalCategoryStruct.tensorObj Localization.Monoidal.monoidalCategoryStruct Functor.obj Localization.Monoidal.toMonoidalCategory MonoidalCategoryStruct.associator CategoryStruct.comp Category.toCategoryStruct MonoidalCategory.toMonoidalCategoryStruct Localization.Monoidal.instMonoidalCategoryLocalizedMonoidal MonoidalCategoryStruct.whiskerRight Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal instMonoidalLocalizedMonoidalToMonoidalCategory Functor.map Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal MonoidalCategoryStruct.whiskerLeft	—	Localization.Monoidal.leftUnitor_hom_app Localization.Monoidal.rightUnitor_hom_app Functor.LaxMonoidal.associativity_assoc Functor.Monoidal.μ_δ_assoc Functor.Monoidal.whiskerLeft_μ_δ Category.comp_id
associator_inv 📖	mathematical	—	Iso.inv LocalizedMonoidal Localization.instCategoryLocalizedMonoidal MonoidalCategoryStruct.tensorObj Localization.Monoidal.monoidalCategoryStruct Functor.obj Localization.Monoidal.toMonoidalCategory MonoidalCategoryStruct.associator CategoryStruct.comp Category.toCategoryStruct MonoidalCategory.toMonoidalCategoryStruct Localization.Monoidal.instMonoidalCategoryLocalizedMonoidal MonoidalCategoryStruct.whiskerLeft Functor.LaxMonoidal.μ Functor.Monoidal.toLaxMonoidal instMonoidalLocalizedMonoidalToMonoidalCategory Functor.map Functor.OplaxMonoidal.δ Functor.Monoidal.toOplaxMonoidal MonoidalCategoryStruct.whiskerRight	—	Localization.Monoidal.leftUnitor_hom_app Localization.Monoidal.rightUnitor_hom_app Functor.LaxMonoidal.associativity_inv_assoc Functor.Monoidal.μ_δ_assoc Functor.Monoidal.whiskerRight_μ_δ Category.comp_id

CategoryTheory.Localization

Definitions

Name	Category	Theorems
instCategoryLocalizedMonoidal 📖	CompOp	58 math math: Monoidal.leftUnitor_hom_app, Monoidal.whiskerLeft_comp, Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1, Monoidal.associator_hom_app, Monoidal.pentagon_aux₁, Monoidal.μ_inv_natural_right, Monoidal.pentagon_aux₂, Monoidal.whiskerRight_comp, Monoidal.triangle_aux₃, Monoidal.id_tensorHom, Monoidal.μ_natural_right, Monoidal.triangle_aux₁_assoc, Monoidal.associator_naturality₃, Monoidal.map_hexagon_forward, Monoidal.μ_natural_left_assoc, Monoidal.map_hexagon_reverse, Monoidal.tensorHom_id, Monoidal.triangle_aux₁, CategoryTheory.associator_inv, Monoidal.map_hexagon_reverse_assoc, Monoidal.μ_natural_left, Monoidal.rightUnitor_naturality, Monoidal.whiskerRight_id, Monoidal.whisker_exchange, Monoidal.whisker_exchange_assoc, Monoidal.μ_inv_natural_left_assoc, Monoidal.associator_naturality₂, Monoidal.μ_inv_natural_right_assoc, Monoidal.associator_naturality₁_assoc, Monoidal.associator_naturality_assoc, Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc, Monoidal.whiskerRight_comp_assoc, Monoidal.associator_naturality₂_assoc, Monoidal.tensor_comp_assoc, Monoidal.pentagon_aux₃, Monoidal.leftUnitor_naturality, Monoidal.triangle, Monoidal.associator_naturality, Monoidal.id_tensorHom_id, Monoidal.triangle_aux₂, Monoidal.β_hom_app, Monoidal.whiskerLeft_id, Monoidal.braidingNatIso_hom_app, Monoidal.braidingNatIso_hom_app_naturality_μ_left, Monoidal.μ_natural_right_assoc, Monoidal.whiskerLeft_comp_assoc, Monoidal.pentagon, Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory, Monoidal.μ_inv_natural_left, Monoidal.associator_naturality₃_assoc, Monoidal.rightUnitor_hom_app, Monoidal.tensor_comp, Monoidal.associator_naturality₁, Monoidal.instEssSurjLocalizedMonoidalToMonoidalCategory, Monoidal.map_hexagon_forward_assoc, Monoidal.braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.associator_hom, Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc

CategoryTheory.Localization.Monoidal

Definitions

Name	Category	Theorems
associator 📖	CompOp	—
instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorLeftObjFunctorTensorBifunctor 📖	CompOp	—
instLiftingLocalizedMonoidalToMonoidalCategoryCompTensorRightObjFunctorFlipTensorBifunctor 📖	CompOp	—
instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorCurriedTensorObjWhiskeringRightTensorBifunctor 📖	CompOp	—
instMonoidalCategoryLocalizedMonoidal 📖	CompOp	8 math math: CategoryTheory.associator_inv, braidingNatIso_hom_app_naturality_μ_left_assoc, β_hom_app, braidingNatIso_hom_app, braidingNatIso_hom_app_naturality_μ_left, braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.associator_hom, braidingNatIso_hom_app_naturality_μ_right_assoc
leftUnitor 📖	CompOp	—
monoidalCategoryStruct 📖	CompOp	53 math math: leftUnitor_hom_app, whiskerLeft_comp, associator_hom_app, pentagon_aux₁, μ_inv_natural_right, pentagon_aux₂, whiskerRight_comp, triangle_aux₃, id_tensorHom, μ_natural_right, triangle_aux₁_assoc, associator_naturality₃, map_hexagon_forward, μ_natural_left_assoc, map_hexagon_reverse, tensorHom_id, triangle_aux₁, CategoryTheory.associator_inv, map_hexagon_reverse_assoc, μ_natural_left, rightUnitor_naturality, whiskerRight_id, whisker_exchange, whisker_exchange_assoc, μ_inv_natural_left_assoc, associator_naturality₂, μ_inv_natural_right_assoc, associator_naturality₁_assoc, associator_naturality_assoc, braidingNatIso_hom_app_naturality_μ_left_assoc, whiskerRight_comp_assoc, associator_naturality₂_assoc, tensor_comp_assoc, pentagon_aux₃, leftUnitor_naturality, triangle, associator_naturality, id_tensorHom_id, triangle_aux₂, whiskerLeft_id, braidingNatIso_hom_app_naturality_μ_left, μ_natural_right_assoc, whiskerLeft_comp_assoc, pentagon, μ_inv_natural_left, associator_naturality₃_assoc, rightUnitor_hom_app, tensor_comp, associator_naturality₁, map_hexagon_forward_assoc, braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.associator_hom, braidingNatIso_hom_app_naturality_μ_right_assoc
rightUnitor 📖	CompOp	—
tensorBifunctor 📖	CompOp	9 math math: map_hexagon_forward, map_hexagon_reverse, map_hexagon_reverse_assoc, braidingNatIso_hom_app_naturality_μ_left_assoc, braidingNatIso_hom_app, braidingNatIso_hom_app_naturality_μ_left, map_hexagon_forward_assoc, braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app_naturality_μ_right_assoc
tensorBifunctorIso 📖	CompOp	—
toMonoidalCategory 📖	CompOp	29 math math: leftUnitor_hom_app, instIsLocalizationLocalizedMonoidalToMonoidalCategory_1, associator_hom_app, μ_inv_natural_right, triangle_aux₃, μ_natural_right, map_hexagon_forward, μ_natural_left_assoc, map_hexagon_reverse, CategoryTheory.associator_inv, map_hexagon_reverse_assoc, μ_natural_left, μ_inv_natural_left_assoc, μ_inv_natural_right_assoc, isInvertedBy₂, braidingNatIso_hom_app_naturality_μ_left_assoc, triangle_aux₂, β_hom_app, braidingNatIso_hom_app, braidingNatIso_hom_app_naturality_μ_left, μ_natural_right_assoc, instIsLocalizationLocalizedMonoidalToMonoidalCategory, μ_inv_natural_left, rightUnitor_hom_app, instEssSurjLocalizedMonoidalToMonoidalCategory, map_hexagon_forward_assoc, braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.associator_hom, braidingNatIso_hom_app_naturality_μ_right_assoc
ε' 📖	CompOp	3 math math: leftUnitor_hom_app, triangle_aux₂, rightUnitor_hom_app
μ 📖	CompOp	12 math math: leftUnitor_hom_app, associator_hom_app, μ_inv_natural_right, triangle_aux₃, μ_natural_right, μ_natural_left_assoc, μ_natural_left, μ_inv_natural_left_assoc, μ_inv_natural_right_assoc, μ_natural_right_assoc, μ_inv_natural_left, rightUnitor_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_app 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom μ CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	instIsLocalizationLocalizedMonoidalToMonoidalCategory CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Localization.associator_hom_app_app_app
associator_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.NatTrans.naturality CategoryTheory.NatTrans.congr_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
associator_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_naturality
associator_naturality₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	associator_naturality id_tensorHom_id
associator_naturality₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_naturality₁
associator_naturality₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	associator_naturality
associator_naturality₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_naturality₂
associator_naturality₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	associator_naturality
associator_naturality₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_naturality₃
id_tensorHom 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
id_tensorHom_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
instEssSurjLocalizedMonoidalToMonoidalCategory 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal toMonoidalCategory	—	CategoryTheory.Localization.essSurj instIsLocalizationLocalizedMonoidalToMonoidalCategory
instIsLocalizationLocalizedMonoidalToMonoidalCategory 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal toMonoidalCategory	—	—
isInvertedBy₂ 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy₂ CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight toMonoidalCategory	—	CategoryTheory.Localization.inverts instIsLocalizationLocalizedMonoidalToMonoidalCategory CategoryTheory.MorphismProperty.whiskerRight_mem CategoryTheory.MorphismProperty.whiskerLeft_mem CategoryTheory.IsIso.comp_isIso
leftUnitor_hom_app 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv ε' μ CategoryTheory.Functor.map	—	instIsLocalizationLocalizedMonoidalToMonoidalCategory CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
leftUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.NatTrans.naturality
pentagon 📖	mathematical	—	CategoryTheory.MonoidalCategory.Pentagon CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct	—	instEssSurjLocalizedMonoidalToMonoidalCategory pentagon_aux₂ associator_hom_app tensorHom_id id_tensorHom whiskerLeft_comp whiskerRight_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pentagon_aux₁ pentagon_aux₃ CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id μ_natural_left_assoc CategoryTheory.Functor.map_comp_assoc μ_inv_natural_right_assoc CategoryTheory.MonoidalCategory.pentagon CategoryTheory.Functor.map_comp whiskerRight_comp_assoc whisker_exchange_assoc whiskerLeft_id CategoryTheory.Category.id_comp whiskerRight_id CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv tensor_comp associator_naturality associator_naturality_assoc tensor_comp_assoc id_tensorHom_id CategoryTheory.whisker_eq CategoryTheory.eq_whisker
pentagon_aux₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	associator_naturality₁_assoc CategoryTheory.Iso.hom_inv_id whiskerRight_id CategoryTheory.Category.comp_id
pentagon_aux₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	associator_naturality₂_assoc CategoryTheory.Iso.hom_inv_id whiskerRight_id whiskerLeft_id CategoryTheory.Category.comp_id
pentagon_aux₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	associator_naturality₃_assoc CategoryTheory.Iso.hom_inv_id whiskerLeft_id CategoryTheory.Category.comp_id
rightUnitor_hom_app 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv ε' μ CategoryTheory.Functor.map	—	instIsLocalizationLocalizedMonoidalToMonoidalCategory CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
rightUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.NatTrans.naturality
tensorHom_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
tensor_comp 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc
tensor_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensor_comp
triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	instEssSurjLocalizedMonoidalToMonoidalCategory CategoryTheory.eq_whisker associator_hom_app CategoryTheory.whisker_eq leftUnitor_hom_app CategoryTheory.Functor.congr_map CategoryTheory.MonoidalCategory.triangle CategoryTheory.Iso.hom_inv_id whiskerRight_id CategoryTheory.Category.id_comp whiskerLeft_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Iso.comp_inv_eq μ_natural_right whiskerRight_comp_assoc tensorHom_id μ_natural_left CategoryTheory.Functor.map_comp Mathlib.Tactic.Reassoc.eq_whisker' id_tensorHom CategoryTheory.Iso.inv_hom_id whiskerLeft_id CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom triangle_aux₁ triangle_aux₂ triangle_aux₃
triangle_aux₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	associator_naturality_assoc CategoryTheory.Iso.hom_inv_id id_tensorHom whiskerLeft_id CategoryTheory.Category.comp_id
triangle_aux₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' triangle_aux₁
triangle_aux₂ 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight ε'	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
triangle_aux₃ 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerLeft μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.hom_inv_id rightUnitor_naturality rightUnitor_hom_app tensorHom_id id_tensorHom tensor_comp_assoc
whiskerLeft_comp 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Category.comp_id
whiskerLeft_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_comp
whiskerLeft_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Functor.map_id
whiskerRight_comp 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Category.comp_id
whiskerRight_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_comp
whiskerRight_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.LocalizedMonoidal CategoryTheory.Localization.instCategoryLocalizedMonoidal monoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.Functor.map_id
whisker_exchange 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
whisker_exchange_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whisker_exchange
μ_inv_natural_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryStruct CategoryTheory.Iso.inv μ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc μ_natural_left CategoryTheory.Iso.inv_hom_id_assoc
μ_inv_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryStruct CategoryTheory.Iso.inv μ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_inv_natural_left
μ_inv_natural_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryStruct CategoryTheory.Iso.inv μ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc μ_natural_right CategoryTheory.Iso.inv_hom_id_assoc
μ_inv_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryStruct CategoryTheory.Iso.inv μ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_inv_natural_right
μ_natural_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom μ	—	CategoryTheory.NatTrans.naturality_app
μ_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_natural_left
μ_natural_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.hom μ	—	CategoryTheory.NatTrans.naturality
μ_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.LocalizedMonoidal CategoryTheory.Category.toCategoryStruct CategoryTheory.Localization.instCategoryLocalizedMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.Functor.obj toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_natural_right

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
IsMonoidal 📖	CompData	5 math math: instIsMonoidalInverseImageOfMonoidalOfRespectsIso, IsMonoidal.mk', CategoryTheory.GrothendieckTopology.W.transport_isMonoidal, CategoryTheory.GrothendieckTopology.W.monoidal, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidalInverseImageOfMonoidalOfRespectsIso 📖	mathematical	—	IsMonoidal inverseImage	—	IsMonoidal.mk' IsMultiplicative.instInverseImage IsMonoidal.toIsMultiplicative CategoryTheory.Functor.Monoidal.map_tensor RespectsIso.precomp CategoryTheory.Functor.Monoidal.instIsIsoδ RespectsIso.postcomp CategoryTheory.Functor.Monoidal.instIsIsoμ tensorHom_mem
tensorHom_mem 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.tensorHom_def comp_mem IsMultiplicative.toIsStableUnderComposition IsMonoidal.toIsMultiplicative whiskerRight_mem whiskerLeft_mem
whiskerLeft_mem 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	IsMonoidal.whiskerLeft
whiskerRight_mem 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	IsMonoidal.whiskerRight

CategoryTheory.MorphismProperty.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.MorphismProperty.IsMonoidal	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MorphismProperty.id_mem CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.MonoidalCategory.tensorHom_id
toIsMultiplicative 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative	—	—
whiskerLeft 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
whiskerRight 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—

---

← Back to Index