Functor

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

Statistics

Metric	Count
Definitions IsMonoidal, rightAdjointLaxMonoidal, IsMonoidal, instMonoidalFunctorRefl, instMonoidalFunctorSymmOfInverse, instMonoidalFunctorTrans, instMonoidalInverseRefl, instMonoidalInverseSymmOfFunctor, instMonoidalInverseTrans, inverseMonoidal, monoidalOfPostcompFunctor, monoidalOfPostcompInverse, monoidalOfPrecompFunctor, monoidalOfPrecompInverse, CoreMonoidal, ofLaxMonoidal, ofOplaxMonoidal, toLaxMonoidal, toMonoidal, toOplaxMonoidal, εIso, μIso, LaxMonoidal, comp, id, ofTensorHom, prod', ε, μ, commTensorLeft, commTensorRight, coreMonoidalTransport, instComp, instId, ofLaxMonoidal, ofOplaxMonoidal, prod', toLaxMonoidal, toOplaxMonoidal, transport, εIso, μIso, μNatIso, OplaxMonoidal, comp, id, prod', δ, η, instLaxMonoidalProdProd, instMonoidalProdDiag, instMonoidalProdProd, instOplaxMonoidalProdProd, LaxMonoidalFunctor, laxMonoidal, of, toFunctor	57
Theorems leftAdjoint_ε, leftAdjoint_μ, instIsMonoidal, instIsMonoidalId, isMonoidal_comp, map_ε_comp_counit_app_unit, map_ε_comp_counit_app_unit_assoc, map_η_comp_η, map_η_comp_η_assoc, map_μ_comp_counit_app_tensor, map_μ_comp_counit_app_tensor_assoc, rightAdjointLaxMonoidal_ε, rightAdjointLaxMonoidal_μ, unit_app_tensor_comp_map_δ, unit_app_tensor_comp_map_δ_assoc, unit_app_unit_comp_map_η, unit_app_unit_comp_map_η_assoc, ε_comp_map_ε, ε_comp_map_ε_assoc, counitInv_app_comp_functor_map_η_inverse, counitInv_app_comp_functor_map_η_inverse_assoc, counitInv_app_tensor_comp_functor_map_δ_inverse, counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, counitIso_inv_app_comp_functor_map_η_inverse, counitIso_inv_app_comp_functor_map_η_inverse_assoc, counitIso_inv_app_tensor_comp_functor_map_δ_inverse, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, functor_map_ε_inverse_comp_counitIso_hom_app, functor_map_ε_inverse_comp_counitIso_hom_app_assoc, functor_map_ε_inverse_comp_counit_app, functor_map_ε_inverse_comp_counit_app_assoc, functor_map_μ_inverse_comp_counitIso_hom_app_tensor, functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, functor_map_μ_inverse_comp_counit_app_tensor, functor_map_μ_inverse_comp_counit_app_tensor_assoc, isMonoidal_refl, isMonoidal_symm, isMonoidal_trans, map_η_comp_η, map_η_comp_η_assoc, unitIso_hom_app_comp_inverse_map_η_functor, unitIso_hom_app_comp_inverse_map_η_functor_assoc, unitIso_hom_app_tensor_comp_inverse_map_δ_functor, unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, unit_app_comp_inverse_map_η_functor, unit_app_comp_inverse_map_η_functor_assoc, unit_app_tensor_comp_inverse_map_δ_functor, unit_app_tensor_comp_inverse_map_δ_functor_assoc, ε_comp_map_ε, ε_comp_map_ε_assoc, associativity, associativity_assoc, left_unitality, left_unitality_assoc, ofOplaxMonoidal_εIso, ofOplaxMonoidal_μIso, right_unitality, right_unitality_assoc, toLaxMonoidal_ε, toLaxMonoidal_μ, toMonoidal_toLaxMonoidal, toMonoidal_toOplaxMonoidal, toOplaxMonoidal_δ, toOplaxMonoidal_η, μIso_hom_natural_left, μIso_hom_natural_left_assoc, μIso_hom_natural_right, μIso_hom_natural_right_assoc, associativity, associativity_assoc, associativity_inv, associativity_inv_assoc, comp_ε, comp_μ, ext, ext_iff, id_ε, id_μ, left_unitality, left_unitality_assoc, left_unitality_inv, left_unitality_inv_assoc, right_unitality, right_unitality_assoc, right_unitality_inv, right_unitality_inv_assoc, tensorHom_ε_comp_μ, tensorHom_ε_comp_μ_assoc, tensorUnit_whiskerLeft_comp_leftUnitor_hom, tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc, whiskerLeft_μ_comp_μ, whiskerLeft_μ_comp_μ_assoc, whiskerRight_tensorUnit_comp_rightUnitor_hom, whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc, ε_tensorHom_comp_μ, ε_tensorHom_comp_μ_assoc, μ_natural, μ_natural_assoc, μ_natural_left, μ_natural_left_assoc, μ_natural_right, μ_natural_right_assoc, μ_whiskerRight_comp_μ, μ_whiskerRight_comp_μ_assoc, commTensorLeft_hom_app, commTensorLeft_inv_app, commTensorRight_hom_app, commTensorRight_inv_app, coreMonoidalTransport_εIso_hom, coreMonoidalTransport_εIso_inv, coreMonoidalTransport_μIso_hom, coreMonoidalTransport_μIso_inv, ext, ext_iff, instIsIsoδ, instIsIsoε, instIsIsoη, instIsIsoμ, inv_δ, inv_ε, inv_η, inv_μ, map_associator, map_associator', map_associator'_assoc, map_associator_assoc, map_associator_inv, map_associator_inv', map_associator_inv'_assoc, map_associator_inv_assoc, map_leftUnitor, map_leftUnitor_assoc, map_leftUnitor_inv, map_leftUnitor_inv_assoc, map_rightUnitor, map_rightUnitor_assoc, map_rightUnitor_inv, map_rightUnitor_inv_assoc, map_tensor, map_tensor_assoc, map_whiskerLeft, map_whiskerLeft_assoc, map_whiskerRight, map_whiskerRight_assoc, map_δ_μ, map_δ_μ_assoc, map_ε_η, map_ε_η_assoc, map_η_ε, map_η_ε_assoc, map_μ_δ, map_μ_δ_assoc, toLaxMonoidal_injective, toOplaxMonoidal_injective, transport_δ, transport_δ_assoc, transport_ε, transport_ε_assoc, transport_η, transport_η_assoc, transport_μ, transport_μ_assoc, whiskerLeft_δ_μ, whiskerLeft_δ_μ_assoc, whiskerLeft_ε_η, whiskerLeft_ε_η_assoc, whiskerLeft_η_ε, whiskerLeft_η_ε_assoc, whiskerLeft_μ_δ, whiskerLeft_μ_δ_assoc, whiskerRight_δ_μ, whiskerRight_δ_μ_assoc, whiskerRight_ε_η, whiskerRight_ε_η_assoc, whiskerRight_η_ε, whiskerRight_η_ε_assoc, whiskerRight_μ_δ, whiskerRight_μ_δ_assoc, δ_μ, δ_μ_assoc, εIso_hom, εIso_inv, ε_η, ε_η_assoc, η_ε, η_ε_assoc, μIso_hom, μIso_inv, μNatIso_hom_app, μNatIso_inv_app, μ_δ, μ_δ_assoc, associativity, associativity_assoc, associativity_inv, associativity_inv_assoc, comp_δ, comp_η, ext, ext_iff, id_δ, id_η, left_unitality, left_unitality_assoc, left_unitality_hom, left_unitality_hom_assoc, oplax_associativity, oplax_left_unitality, oplax_right_unitality, right_unitality, right_unitality_assoc, right_unitality_hom, right_unitality_hom_assoc, δ_comp_tensorHom_η, δ_comp_tensorHom_η_assoc, δ_comp_whiskerLeft_δ, δ_comp_whiskerLeft_δ_assoc, δ_comp_δ_whiskerRight, δ_comp_δ_whiskerRight_assoc, δ_comp_η_tensorHom, δ_comp_η_tensorHom_assoc, δ_natural, δ_natural_assoc, δ_natural_left, δ_natural_left_assoc, δ_natural_right, δ_natural_right_assoc, diag_δ, diag_ε, diag_η, diag_μ, prod'_δ_fst, prod'_δ_snd, prod'_ε_fst, prod'_ε_snd, prod'_η_fst, prod'_η_snd, prod'_μ_fst, prod'_μ_snd, prod_δ_fst, prod_δ_snd, prod_ε_fst, prod_ε_snd, prod_η_fst, prod_η_snd, prod_μ_fst, prod_μ_snd, of_toFunctor	248
Total	305

CategoryTheory

Definitions

Name	Category	Theorems
LaxMonoidalFunctor 📖	CompData	47 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, Mon.equivLaxMonoidalFunctorPUnit_inverse, LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app, CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, LaxBraidedFunctor.comp_hom, LaxBraidedFunctor.isoOfComponents_hom_hom_app, LaxMonoidalFunctor.isoOfComponents_inv_hom_app, LaxBraidedFunctor.forget_map, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, LaxMonoidalFunctor.isoMk_inv, LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app, CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, Functor.mapCommMonFunctor_map_app, LaxBraidedFunctor.comp_hom_assoc, Functor.mapMonFunctor_obj, LaxMonoidalFunctor.isoOfComponents_hom_hom_app, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, Functor.mapMonFunctor_map_app_hom, Mon.equivLaxMonoidalFunctorPUnit_counitIso, Mon.equivLaxMonoidalFunctorPUnit_unitIso, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj, Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app, Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, LaxBraidedFunctor.homMk_hom_hom, LaxBraidedFunctor.forget_obj, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, Mon.equivLaxMonoidalFunctorPUnit_functor, LaxBraidedFunctor.isoOfComponents_inv_hom_app, LaxMonoidalFunctor.comp_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map, LaxMonoidalFunctor.isoMk_hom, CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, LaxMonoidalFunctor.comp_hom_assoc, LaxBraidedFunctor.id_hom, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, LaxBraidedFunctor.hom_ext_iff, Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, LaxMonoidalFunctor.id_hom, Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app, TannakaDuality.FiniteGroup.equivHom_apply

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
IsMonoidal 📖	CompData	3 math math: isMonoidal_comp, instIsMonoidalId, instIsMonoidal
rightAdjointLaxMonoidal 📖	CompOp	3 math math: rightAdjointLaxMonoidal_μ, instIsMonoidal, rightAdjointLaxMonoidal_ε

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidal 📖	mathematical	—	IsMonoidal rightAdjointLaxMonoidal	—	—
instIsMonoidalId 📖	mathematical	—	IsMonoidal CategoryTheory.Functor.id id CategoryTheory.Functor.OplaxMonoidal.id CategoryTheory.Functor.LaxMonoidal.id	—	CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight
isMonoidal_comp 📖	mathematical	—	IsMonoidal CategoryTheory.Functor.comp comp CategoryTheory.Functor.OplaxMonoidal.comp CategoryTheory.Functor.LaxMonoidal.comp	—	IsMonoidal.leftAdjoint_ε CategoryTheory.Category.assoc unit_naturality_assoc comp_unit_app IsMonoidal.leftAdjoint_μ comp_counit_app CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc CategoryTheory.Functor.map_comp
map_ε_comp_counit_app_unit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit CategoryTheory.Functor.OplaxMonoidal.η	—	IsMonoidal.leftAdjoint_ε CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality left_triangle_components_assoc
map_ε_comp_counit_app_unit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ε_comp_counit_app_unit
map_η_comp_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	map_ε_comp_counit_app_unit CategoryTheory.Functor.Monoidal.map_η_ε_assoc
map_η_comp_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_η_comp_η
map_μ_comp_counit_app_tensor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	IsMonoidal.leftAdjoint_μ CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality counit_naturality_assoc left_triangle_components_assoc
map_μ_comp_counit_app_tensor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_μ_comp_counit_app_tensor
rightAdjointLaxMonoidal_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε rightAdjointLaxMonoidal DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Functor.OplaxMonoidal.η	—	—
rightAdjointLaxMonoidal_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ rightAdjointLaxMonoidal DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	—
unit_app_tensor_comp_map_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.LaxMonoidal.μ	—	IsMonoidal.leftAdjoint_μ unit_naturality_assoc CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom left_triangle_components CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id
unit_app_tensor_comp_map_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.LaxMonoidal.μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_tensor_comp_map_δ
unit_app_unit_comp_map_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.LaxMonoidal.ε	—	IsMonoidal.leftAdjoint_ε
unit_app_unit_comp_map_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.LaxMonoidal.ε	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_unit_comp_map_η
ε_comp_map_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	unit_app_unit_comp_map_η CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.map_η_ε CategoryTheory.Category.comp_id
ε_comp_map_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ε_comp_map_ε

CategoryTheory.Adjunction.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftAdjoint_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η	—	—
leftAdjoint_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Adjunction.counit	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
IsMonoidal 📖	MathDef	7 math math: isMonoidal_trans, CategoryTheory.instIsMonoidalFunctorCongrLeft, CategoryTheory.Monoidal.instIsMonoidalTransportedSymmEquivalenceTransported, isMonoidal_symm, CategoryTheory.instIsMonoidalOppositeOpOpEquivalence, isMonoidal_refl, CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence
instMonoidalFunctorRefl 📖	CompOp	1 math math: isMonoidal_refl
instMonoidalFunctorSymmOfInverse 📖	CompOp	1 math math: isMonoidal_symm
instMonoidalFunctorTrans 📖	CompOp	1 math math: isMonoidal_trans
instMonoidalInverseRefl 📖	CompOp	1 math math: isMonoidal_refl
instMonoidalInverseSymmOfFunctor 📖	CompOp	1 math math: isMonoidal_symm
instMonoidalInverseTrans 📖	CompOp	1 math math: isMonoidal_trans
inverseMonoidal 📖	CompOp	—
monoidalOfPostcompFunctor 📖	CompOp	—
monoidalOfPostcompInverse 📖	CompOp	—
monoidalOfPrecompFunctor 📖	CompOp	—
monoidalOfPrecompInverse 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitInv_app_comp_functor_map_η_inverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app counitInv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Functor.Monoidal.instIsIsoη CategoryTheory.Functor.Monoidal.η_ε functor_map_ε_inverse_comp_counitIso_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.Functor.Monoidal.map_ε_η
counitInv_app_comp_functor_map_η_inverse_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counitInv_app_comp_functor_map_η_inverse
counitInv_app_tensor_comp_functor_map_δ_inverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct functor CategoryTheory.Functor.comp inverse CategoryTheory.NatTrans.app counitInv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso	—	counitIso_inv_app_tensor_comp_functor_map_δ_inverse
counitInv_app_tensor_comp_functor_map_δ_inverse_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counitInv_app_tensor_comp_functor_map_δ_inverse
counitIso_inv_app_comp_functor_map_η_inverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Functor.Monoidal.instIsIsoη CategoryTheory.Functor.Monoidal.η_ε functor_map_ε_inverse_comp_counitIso_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.Functor.Monoidal.map_ε_η
counitIso_inv_app_comp_functor_map_η_inverse_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counitIso_inv_app_comp_functor_map_η_inverse
counitIso_inv_app_tensor_comp_functor_map_δ_inverse 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct functor CategoryTheory.Functor.comp inverse CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom unitIso	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Functor.Monoidal.instIsIsoδ CategoryTheory.Functor.Monoidal.δ_μ_assoc CategoryTheory.Functor.map_injective faithful_inverse CategoryTheory.Functor.map_comp inv_fun_map inverse_counitInv_comp_assoc CategoryTheory.NatIso.hom_app_isIso unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc CategoryTheory.Functor.Monoidal.μ_δ_assoc CategoryTheory.Iso.hom_inv_id_app_assoc
counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom unitIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counitIso_inv_app_tensor_comp_functor_map_δ_inverse
functor_map_ε_inverse_comp_counitIso_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
functor_map_ε_inverse_comp_counitIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functor_map_ε_inverse_comp_counitIso_hom_app
functor_map_ε_inverse_comp_counit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
functor_map_ε_inverse_comp_counit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functor_map_ε_inverse_comp_counit_app
functor_map_μ_inverse_comp_counitIso_hom_app_tensor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functor_map_μ_inverse_comp_counitIso_hom_app_tensor
functor_map_μ_inverse_comp_counit_app_tensor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
functor_map_μ_inverse_comp_counit_app_tensor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct inverse CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functor_map_μ_inverse_comp_counit_app_tensor
isMonoidal_refl 📖	mathematical	—	IsMonoidal refl instMonoidalFunctorRefl instMonoidalInverseRefl	—	CategoryTheory.Adjunction.instIsMonoidalId
isMonoidal_symm 📖	mathematical	—	IsMonoidal symm instMonoidalFunctorSymmOfInverse instMonoidalInverseSymmOfFunctor	—	counitIso_inv_app_comp_functor_map_η_inverse CategoryTheory.Functor.map_comp counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.Iso.hom_inv_id_app CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
isMonoidal_trans 📖	mathematical	—	IsMonoidal trans instMonoidalFunctorTrans instMonoidalInverseTrans	—	trans_toAdjunction CategoryTheory.Adjunction.isMonoidal_comp
map_η_comp_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Adjunction.map_η_comp_η
map_η_comp_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_η_comp_η
unitIso_hom_app_comp_inverse_map_η_functor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Adjunction.unit_app_unit_comp_map_η
unitIso_hom_app_comp_inverse_map_η_functor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unitIso_hom_app_comp_inverse_map_η_functor
unitIso_hom_app_tensor_comp_inverse_map_δ_functor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unitIso_hom_app_tensor_comp_inverse_map_δ_functor
unit_app_comp_inverse_map_η_functor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Adjunction.unit_app_unit_comp_map_η
unit_app_comp_inverse_map_η_functor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_comp_inverse_map_η_functor
unit_app_tensor_comp_inverse_map_δ_functor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
unit_app_tensor_comp_inverse_map_δ_functor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_tensor_comp_inverse_map_δ_functor
ε_comp_map_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	CategoryTheory.Adjunction.ε_comp_map_ε
ε_comp_map_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj inverse CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal functor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ε_comp_map_ε

CategoryTheory.Functor

Definitions

Name	Category	Theorems
CoreMonoidal 📖	CompData	—
LaxMonoidal 📖	CompData	1 math math: Monoidal.toLaxMonoidal_injective
OplaxMonoidal 📖	CompData	2 math math: OplaxMonoidal.instSubsingleton, Monoidal.toOplaxMonoidal_injective
instLaxMonoidalProdProd 📖	CompOp	4 math math: prod_ε_snd, prod_ε_fst, prod_μ_fst, prod_μ_snd
instMonoidalProdDiag 📖	CompOp	4 math math: diag_δ, diag_μ, diag_η, diag_ε
instMonoidalProdProd 📖	CompOp	—
instOplaxMonoidalProdProd 📖	CompOp	4 math math: prod_η_snd, prod_δ_snd, prod_η_fst, prod_δ_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diag_δ 📖	mathematical	—	OplaxMonoidal.δ CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.prodMonoidal diag Monoidal.toOplaxMonoidal instMonoidalProdDiag CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
diag_ε 📖	mathematical	—	LaxMonoidal.ε CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.prodMonoidal diag Monoidal.toLaxMonoidal instMonoidalProdDiag CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
diag_η 📖	mathematical	—	OplaxMonoidal.η CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.prodMonoidal diag Monoidal.toOplaxMonoidal instMonoidalProdDiag CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
diag_μ 📖	mathematical	—	LaxMonoidal.μ CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.prodMonoidal diag Monoidal.toLaxMonoidal instMonoidalProdDiag CategoryTheory.CategoryStruct.id CategoryTheory.prod CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct obj	—	—
prod'_δ_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.δ OplaxMonoidal.prod'	—	map_id CategoryTheory.Category.id_comp
prod'_δ_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.δ OplaxMonoidal.prod'	—	map_id CategoryTheory.Category.id_comp
prod'_ε_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod' LaxMonoidal.ε LaxMonoidal.prod'	—	map_id CategoryTheory.Category.comp_id
prod'_ε_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod' LaxMonoidal.ε LaxMonoidal.prod'	—	map_id CategoryTheory.Category.comp_id
prod'_η_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod' CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.η OplaxMonoidal.prod'	—	map_id CategoryTheory.Category.id_comp
prod'_η_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod' CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.η OplaxMonoidal.prod'	—	map_id CategoryTheory.Category.id_comp
prod'_μ_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod' LaxMonoidal.μ LaxMonoidal.prod'	—	map_id CategoryTheory.Category.comp_id
prod'_μ_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod' LaxMonoidal.μ LaxMonoidal.prod'	—	map_id CategoryTheory.Category.comp_id
prod_δ_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.δ instOplaxMonoidalProdProd	—	—
prod_δ_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.δ instOplaxMonoidalProdProd	—	—
prod_ε_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod LaxMonoidal.ε instLaxMonoidalProdProd	—	—
prod_ε_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod LaxMonoidal.ε instLaxMonoidalProdProd	—	—
prod_η_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.η instOplaxMonoidalProdProd	—	—
prod_η_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.prod' prod CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal OplaxMonoidal.η instOplaxMonoidalProdProd	—	—
prod_μ_fst 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod LaxMonoidal.μ instLaxMonoidalProdProd	—	—
prod_μ_snd 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.prod' CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.prodMonoidal obj prod LaxMonoidal.μ instLaxMonoidalProdProd	—	—

CategoryTheory.Functor.CoreMonoidal

Definitions

Name	Category	Theorems
ofLaxMonoidal 📖	CompOp	—
ofOplaxMonoidal 📖	CompOp	4 math math: CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.Over.grpObjMkPullbackSnd_mul, ofOplaxMonoidal_εIso, ofOplaxMonoidal_μIso
toLaxMonoidal 📖	CompOp	5 math math: CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.Over.grpObjMkPullbackSnd_mul, toMonoidal_toLaxMonoidal, toLaxMonoidal_ε, toLaxMonoidal_μ
toMonoidal 📖	CompOp	2 math math: toMonoidal_toLaxMonoidal, toMonoidal_toOplaxMonoidal
toOplaxMonoidal 📖	CompOp	3 math math: toOplaxMonoidal_δ, toOplaxMonoidal_η, toMonoidal_toOplaxMonoidal
εIso 📖	CompOp	11 math math: CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_inv, left_unitality, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_hom, right_unitality_assoc, ofOplaxMonoidal_εIso, right_unitality, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, toLaxMonoidal_ε, left_unitality_assoc, toOplaxMonoidal_η, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
μIso 📖	CompOp	17 math math: left_unitality, μIso_hom_natural_left, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_hom, associativity_assoc, right_unitality_assoc, toOplaxMonoidal_δ, μIso_hom_natural_left_assoc, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_inv, associativity, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom, μIso_hom_natural_right, right_unitality, μIso_hom_natural_right_assoc, toLaxMonoidal_μ, left_unitality_assoc, ofOplaxMonoidal_μIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associativity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom μIso CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
associativity_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom μIso CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity
left_unitality 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight εIso μIso CategoryTheory.Functor.map	—	—
left_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight εIso μIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_unitality
ofOplaxMonoidal_εIso 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ	εIso ofOplaxMonoidal CategoryTheory.Iso.symm CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.asIso CategoryTheory.Functor.OplaxMonoidal.η	—	—
ofOplaxMonoidal_μIso 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ	μIso ofOplaxMonoidal CategoryTheory.Iso.symm CategoryTheory.asIso	—	—
right_unitality 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft εIso μIso CategoryTheory.Functor.map	—	—
right_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft εIso μIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_unitality
toLaxMonoidal_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj εIso	—	—
toLaxMonoidal_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj μIso	—	—
toMonoidal_toLaxMonoidal 📖	mathematical	—	CategoryTheory.Functor.Monoidal.toLaxMonoidal toMonoidal toLaxMonoidal	—	—
toMonoidal_toOplaxMonoidal 📖	mathematical	—	CategoryTheory.Functor.Monoidal.toOplaxMonoidal toMonoidal toOplaxMonoidal	—	—
toOplaxMonoidal_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj μIso	—	—
toOplaxMonoidal_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj εIso	—	—
μIso_hom_natural_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom μIso	—	—
μIso_hom_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom μIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μIso_hom_natural_left
μIso_hom_natural_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.hom μIso	—	—
μIso_hom_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.hom μIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μIso_hom_natural_right

CategoryTheory.Functor.LaxMonoidal

Definitions

Name	Category	Theorems
comp 📖	CompOp	32 math math: CategoryTheory.Adjunction.isMonoidal_comp, CategoryTheory.NatTrans.IsMonoidal.instHomFunctorAssociator, CategoryTheory.Adjunction.mapMon_unit, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal, CategoryTheory.Functor.mapMonCompIso_hom_app_hom, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, CategoryTheory.Localization.Monoidal.lifting_isMonoidal, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, CategoryTheory.Equivalence.mapMon_unitIso, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, CategoryTheory.Adjunction.mapMon_counit, CategoryTheory.NatTrans.IsMonoidal.hcomp, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.Functor.comp_mapCommMon_mul, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit, CategoryTheory.Functor.comp_mapCommGrp_mul, CategoryTheory.NatTrans.IsMonoidal.whiskerRight, CategoryTheory.NatTrans.IsMonoidal.instHomFunctorRightUnitor, CategoryTheory.Equivalence.mapMon_counitIso, CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor, comp_ε, CategoryTheory.Functor.mapMonCompIso_inv_app_hom, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal, comp_μ, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit, CategoryTheory.Functor.comp_mapMon_one, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Functor.comp_mapGrp_one, CategoryTheory.NatTrans.IsMonoidal.whiskerLeft
id 📖	CompOp	19 math math: CategoryTheory.Adjunction.mapMon_unit, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, CategoryTheory.Equivalence.mapMon_unitIso, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, CategoryTheory.Adjunction.instIsMonoidalId, CategoryTheory.Adjunction.mapMon_counit, id_ε, CategoryTheory.Functor.mapMonIdIso_hom_app_hom, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit, id_μ, CategoryTheory.NatTrans.IsMonoidal.instHomFunctorRightUnitor, CategoryTheory.Functor.mapMonIdIso_inv_app_hom, CategoryTheory.Equivalence.mapMon_counitIso, CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor, CategoryTheory.Functor.id_mapMon_mul, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit, CategoryTheory.Functor.id_mapMon_one
ofTensorHom 📖	CompOp	—
prod' 📖	CompOp	5 math math: CategoryTheory.Functor.prod'_μ_fst, CategoryTheory.NatTrans.instIsMonoidalProdProd', CategoryTheory.Functor.prod'_ε_fst, CategoryTheory.Functor.prod'_μ_snd, CategoryTheory.Functor.prod'_ε_snd
ε 📖	CompOp	158 math math: CategoryTheory.Functor.Braided.ext_iff, CategoryTheory.obj_ε_app_assoc, CategoryTheory.Functor.Monoidal.ext_iff, right_unitality, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.Functor.Monoidal.εIso_hom, CategoryTheory.TransportEnrichment.eId_eq, CategoryTheory.Mon.forget_ε, CategoryTheory.MonoidalOpposite.mopFunctor_ε, CategoryTheory.Functor.Monoidal.η_ε_assoc, CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.η_ε_app_assoc, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, CategoryTheory.Functor.Monoidal.whiskerRight_η_ε, left_unitality_assoc, CategoryTheory.Functor.Monoidal.map_rightUnitor_inv, CategoryTheory.Grp.ε_def, CategoryTheory.Functor.Monoidal.map_leftUnitor_inv, CategoryTheory.ε_η_app_assoc, CategoryTheory.ε_naturality_assoc, CategoryTheory.Functor.prod'_ε_fst, CategoryTheory.Adjunction.ε_comp_map_ε_assoc, CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.ObjectProperty.ι_η, CategoryTheory.Pi.laxMonoidalPi'_ε, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.Monoidal.map_ε_η_assoc, CategoryTheory.left_unitality_app_assoc, CategoryTheory.Functor.prod_ε_snd, CategoryTheory.NatTrans.IsMonoidal.unit, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_hom, CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc, CategoryTheory.Functor.Monoidal.transport_ε, CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc, CategoryTheory.Adjunction.unit_app_unit_comp_map_η, CategoryTheory.ObjectProperty.ι_ε, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε, CategoryTheory.Center.ofBraided_ε_f, left_unitality, CategoryTheory.right_unitality_app_assoc, CategoryTheory.Functor.obj.η_def_assoc, CategoryTheory.Center.forget_ε, CategoryTheory.Functor.obj.η_def, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε, CategoryTheory.Functor.Monoidal.whiskeringLeft_ε_app, CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc, CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc, CategoryTheory.Limits.lim_ε_π_assoc, CategoryTheory.monoidalUnopUnop_ε, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc, id_ε, CategoryTheory.Functor.Monoidal.inv_η, right_unitality_inv, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc, ModuleCat.free_ε_one, CategoryTheory.Functor.mapAction_ε_hom, CategoryTheory.Functor.Monoidal.toUnit_ε, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε, CategoryTheory.Functor.mapMon_obj_mon_one, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.Discrete.monoidalFunctor_ε, tensorHom_ε_comp_μ_assoc, CategoryTheory.ε_naturality, ε_tensorHom_comp_μ_assoc, CategoryTheory.Adjunction.ε_comp_map_ε, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse, CategoryTheory.Limits.lim_ε_π, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app, tensorUnit_whiskerLeft_comp_leftUnitor_hom, CategoryTheory.Functor.prod_ε_fst, CategoryTheory.Over.monObjMkPullbackSnd_one, CategoryTheory.unitOfTensorIsoUnit_inv_app, CategoryTheory.MonoidalCategory.tensoringRight_ε, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc, CategoryTheory.Functor.Monoidal.inv_ε, tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc, CategoryTheory.ε_app_obj, CategoryTheory.Functor.mapCommMon_obj_mon_one, CategoryTheory.monoidalOpOp_ε, whiskeringRight_ε_app, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.Functor.instIsMonHomε, CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.ε_def, Action.forget_ε, CategoryTheory.left_unitality_app, CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app, CategoryTheory.Equivalence.ε_comp_map_ε, CategoryTheory.ε_η_app, CategoryTheory.Functor.prod'_ε_snd, right_unitality_assoc, CategoryTheory.Functor.Monoidal.map_ε_η, ext_iff, comp_ε, CategoryTheory.Functor.Monoidal.instIsIsoε, CategoryTheory.Pi.monoidalPi_ε, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, CategoryTheory.NatTrans.IsMonoidal.unit_assoc, CategoryTheory.Discrete.addMonoidalFunctor_ε, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Functor.Monoidal.whiskerRight_ε_η, CategoryTheory.Functor.Monoidal.map_η_ε_assoc, whiskerRight_tensorUnit_comp_rightUnitor_hom, CategoryTheory.sheafToPresheaf_ε, CategoryTheory.Functor.Monoidal.map_η_ε, CategoryTheory.Pi.monoidalPi'_ε, CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_ε, CategoryTheory.Pi.laxMonoidalPi_ε, CategoryTheory.ObjectProperty.ιOfLE_ε, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc, ε_tensorHom_comp_μ, CategoryTheory.Mon.limit_mon_one, right_unitality_inv_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, tensorHom_ε_comp_μ, whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc, CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε, CategoryTheory.MonoidalOpposite.unmopFunctor_ε, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.Equivalence.ε_comp_map_ε_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, CategoryTheory.obj_ε_app, CategoryTheory.Functor.Monoidal.transport_ε_assoc, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit, CategoryTheory.Over.ε_pullback_left, CategoryTheory.Comon.forget_ε, CategoryTheory.Functor.Monoidal.ε_η_assoc, CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc, left_unitality_inv, CategoryTheory.Functor.diag_ε, left_unitality_inv_assoc, Rep.linearization_ε_hom, CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc, CategoryTheory.Pi.ε_def, CategoryTheory.MonoidalCategory.tensor_ε, CategoryTheory.ε_app, CategoryTheory.right_unitality_app, CategoryTheory.η_ε_app, CategoryTheory.Functor.comp_mapMon_one, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε, CategoryTheory.Functor.comp_mapGrp_one, Action.FunctorCategoryEquivalence.functor_ε, CategoryTheory.Functor.Monoidal.η_ε, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
μ 📖	CompOp	230 math math: CategoryTheory.Functor.Braided.ext_iff, CategoryTheory.Over.μ_pullback_left_snd', associativity_assoc, whiskerLeft_μ_comp_μ_assoc, CategoryTheory.Functor.Monoidal.ext_iff, CategoryTheory.Functor.Monoidal.commTensorLeft_hom_app, μ_natural_right, right_unitality, CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Functor.mapCommMon_obj_mon_mul, CategoryTheory.Mon.forget_μ, CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc, CategoryTheory.μ_def, CategoryTheory.Functor.prod'_μ_fst, CategoryTheory.Functor.mapMon_obj_mon_mul, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ, CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ, CategoryTheory.Functor.Monoidal.inv_μ, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.Functor.Monoidal.map_associator_inv_assoc, CategoryTheory.μ_δ_app_assoc, CategoryTheory.Functor.Monoidal.map_associator_assoc, CategoryTheory.Functor.Monoidal.transport_μ, CategoryTheory.Functor.Monoidal.map_μ_δ_assoc, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.Functor.LaxBraided.braided, left_unitality_assoc, CategoryTheory.μ_naturality₂_assoc, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ, CategoryTheory.Functor.Monoidal.map_rightUnitor_inv, CategoryTheory.sheafToPresheaf_μ, CategoryTheory.Functor.Monoidal.map_leftUnitor_inv, CategoryTheory.Functor.Monoidal.map_associator, CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ_assoc, CategoryTheory.obj_zero_map_μ_app_assoc, CategoryTheory.Functor.Monoidal.map_whiskerRight, CategoryTheory.μ_naturalityᵣ_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', CommGrpCat.μ_forget_apply, CategoryTheory.obj_μ_app, CategoryTheory.μ_naturalityₗ, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv, CategoryTheory.Functor.Monoidal.μ_comp_assoc, CategoryTheory.left_unitality_app_assoc, CategoryTheory.μ_naturality₂, CategoryTheory.Functor.instIsMonHomμ, CategoryTheory.μ_naturalityᵣ, CategoryTheory.Functor.Monoidal.map_associator'_assoc, CategoryTheory.Functor.Monoidal.μ_fst_assoc, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_hom, CategoryTheory.Functor.Monoidal.map_δ_μ_assoc, CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, CategoryTheory.δ_μ_app, CategoryTheory.Mon.limit_mon_mul, CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ, CategoryTheory.Functor.Monoidal.transport_μ_assoc, left_unitality, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor, μ_natural_right_assoc, CategoryTheory.right_unitality_app_assoc, CategoryTheory.η_app_obj, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ, CategoryTheory.Grp.μ_def, CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc, CategoryTheory.NatTrans.IsMonoidal.tensor, CategoryTheory.μ_naturality, CategoryTheory.obj_zero_map_μ_app, CategoryTheory.Functor.Monoidal.whiskeringLeft_μ_app, CategoryTheory.Over.μ_pullback_left_fst_snd', CategoryTheory.Functor.Monoidal.map_associator_inv, CategoryTheory.associator_inv, CategoryTheory.Pi.laxMonoidalPi'_μ, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.Functor.Monoidal.map_associator_inv', right_unitality_inv, CategoryTheory.Functor.diag_μ, CategoryTheory.Functor.comp_mapCommMon_mul, CategoryTheory.Functor.Monoidal.instIsIsoμ, CategoryTheory.Functor.Monoidal.map_associator_inv'_assoc, CategoryTheory.Functor.Braided.braided, CategoryTheory.monoidalOpOp_μ, CategoryTheory.Functor.prod'_μ_snd, CategoryTheory.Functor.comp_mapCommGrp_mul, AddCommGrpCat.μ_forget_apply, tensorHom_ε_comp_μ_assoc, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Functor.mapAction_μ_hom, ε_tensorHom_comp_μ_assoc, associativity_inv, tensorUnit_whiskerLeft_comp_leftUnitor_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ, id_μ, CategoryTheory.Over.μ_pullback_left_fst_fst', μ_natural_left_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd, associativity_inv_assoc, CategoryTheory.Functor.Monoidal.map_associator', CategoryTheory.obj_η_app_assoc, CategoryTheory.Functor.map_braiding_assoc, ModuleCat.free_μ_freeMk_tmul_freeMk, CategoryTheory.Functor.prod_μ_fst, AddGrpCat.μ_forget_apply, whiskeringRight_μ_app, CategoryTheory.Functor.obj.μ_def, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, CategoryTheory.TransportEnrichment.eComp_eq, CategoryTheory.Functor.Monoidal.μ_comp, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc, CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ, tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc, CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.obj_μ_inv_app, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, μ_whiskerRight_comp_μ_assoc, CategoryTheory.ObjectProperty.ι_μ, CategoryTheory.associativity_app_assoc, CategoryTheory.Limits.lim_μ_π_assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app, CategoryTheory.Functor.Monoidal.map_μ_δ, CategoryTheory.Functor.Monoidal.map_tensor_assoc, CategoryTheory.MonoidalOpposite.mopFunctor_μ, CategoryTheory.μ_δ_app, CategoryTheory.Functor.Monoidal.inv_δ, CategoryTheory.left_unitality_app, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ, CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor, CategoryTheory.Center.ofBraided_μ_f, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.Functor.obj.μ_def_assoc, right_unitality_assoc, CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc, ext_iff, CategoryTheory.Discrete.addMonoidalFunctor_μ, CategoryTheory.MonoidalOpposite.unmopFunctor_μ, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc, CategoryTheory.Functor.Monoidal.map_whiskerLeft, μ_natural_left, CategoryTheory.Functor.Monoidal.map_δ_μ, CategoryTheory.monoidalUnopUnop_μ, associativity, CategoryTheory.Over.μ_pullback_left_snd, CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ, CategoryTheory.Functor.Monoidal.μ_snd, whiskerRight_tensorUnit_comp_rightUnitor_hom, CategoryTheory.Localization.Monoidal.β_hom_app, Action.FunctorCategoryEquivalence.functor_μ, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor, CategoryTheory.Functor.Monoidal.μ_snd_assoc, CategoryTheory.Functor.Monoidal.map_tensor, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.obj_μ_app_assoc, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left, CategoryTheory.Functor.Monoidal.μNatIso_hom_app, CategoryTheory.Over.μ_pullback_left_fst_fst, ε_tensorHom_comp_μ, whiskerLeft_μ_comp_μ, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor, right_unitality_inv_assoc, Action.forget_μ, CategoryTheory.Discrete.monoidalFunctor_μ, CategoryTheory.Functor.prod_μ_snd, CategoryTheory.obj_μ_zero_app, tensorHom_ε_comp_μ, comp_μ, whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc, CategoryTheory.Pi.monoidalPi_μ, CategoryTheory.associativity_app, μ_whiskerRight_comp_μ, CategoryTheory.NatTrans.IsMonoidal.tensor_assoc, CategoryTheory.obj_μ_inv_app_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.μ_naturality_assoc, CategoryTheory.Comon.forget_μ, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ, CategoryTheory.unitOfTensorIsoUnit_hom_app, μ_natural_assoc, CategoryTheory.Functor.Monoidal.lift_μ, CategoryTheory.Functor.LaxBraided.braided_assoc, CategoryTheory.Functor.Monoidal.commTensorRight_hom_app, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc, CategoryTheory.δ_μ_app_assoc, CategoryTheory.Functor.Monoidal.δ_μ_assoc, μ_natural, CategoryTheory.obj_η_app, GrpCat.μ_forget_apply, CategoryTheory.ObjectProperty.ιOfLE_μ, CategoryTheory.Pi.μ_def, CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, left_unitality_inv, CategoryTheory.Center.forget_μ, CategoryTheory.Limits.lim_μ_π, CategoryTheory.Functor.map_braiding, left_unitality_inv_assoc, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, CategoryTheory.right_unitality_app, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.Functor.Monoidal.μ_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc, CategoryTheory.μ_naturalityₗ_assoc, CategoryTheory.MonoidalCategory.tensor_μ, CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc, CategoryTheory.Pi.laxMonoidalPi_μ, CategoryTheory.μ_app, CategoryTheory.Pi.monoidalPi'_μ, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.Functor.Monoidal.μ_δ_assoc, Rep.linearization_μ_hom, CategoryTheory.associator_hom, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc, CategoryTheory.MonoidalCategory.tensoringRight_μ, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associativity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight μ CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
associativity_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight μ CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity
associativity_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft μ CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Iso.eq_inv_comp associativity_assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
associativity_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft μ CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity_inv
comp_ε 📖	mathematical	—	ε CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
comp_μ 📖	mathematical	—	μ CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
ext 📖	—	ε μ	—	—	—
ext_iff 📖	mathematical	—	ε μ	—	ext
id_ε 📖	mathematical	—	ε CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
id_μ 📖	mathematical	—	μ CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
left_unitality 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight ε μ CategoryTheory.Functor.map	—	—
left_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_unitality
left_unitality_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight ε μ CategoryTheory.Functor.map	—	CategoryTheory.Iso.inv_comp_eq left_unitality CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
left_unitality_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_unitality_inv
right_unitality 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft ε μ CategoryTheory.Functor.map	—	—
right_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_unitality
right_unitality_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft ε μ CategoryTheory.Functor.map	—	CategoryTheory.Iso.inv_comp_eq right_unitality CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
right_unitality_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_unitality_inv
tensorHom_ε_comp_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.assoc right_unitality_inv right_unitality CategoryTheory.Iso.map_hom_inv_id CategoryTheory.Category.comp_id
tensorHom_ε_comp_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_ε_comp_μ
tensorUnit_whiskerLeft_comp_leftUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.Functor.map	—	CategoryTheory.MonoidalCategory.id_whiskerLeft left_unitality CategoryTheory.Category.assoc left_unitality_inv_assoc CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_def'
tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorUnit_whiskerLeft_comp_leftUnitor_hom
whiskerLeft_μ_comp_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft μ CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	associativity CategoryTheory.Iso.inv_hom_id_assoc
whiskerLeft_μ_comp_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft μ CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_μ_comp_μ
whiskerRight_tensorUnit_comp_rightUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.Functor.map	—	CategoryTheory.MonoidalCategory.whiskerRight_id right_unitality CategoryTheory.Category.assoc right_unitality_inv_assoc CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_def
whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_tensorUnit_comp_rightUnitor_hom
ε_tensorHom_comp_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Category.assoc left_unitality_inv left_unitality CategoryTheory.Iso.map_hom_inv_id CategoryTheory.Category.comp_id
ε_tensorHom_comp_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom ε μ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ε_tensorHom_comp_μ
μ_natural 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map μ	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc μ_natural_right μ_natural_left_assoc CategoryTheory.Functor.map_comp
μ_natural_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_natural
μ_natural_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map μ	—	—
μ_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_natural_left
μ_natural_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map μ	—	—
μ_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_natural_right
μ_whiskerRight_comp_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight μ CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	associativity_assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
μ_whiskerRight_comp_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight μ CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_whiskerRight_comp_μ

CategoryTheory.Functor.Monoidal

Definitions

Name	Category	Theorems
commTensorLeft 📖	CompOp	4 math math: commTensorLeft_hom_app, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, commTensorLeft_inv_app, CategoryTheory.MonoidalClosed.ofEquiv_curry_def
commTensorRight 📖	CompOp	2 math math: commTensorRight_inv_app, commTensorRight_hom_app
coreMonoidalTransport 📖	CompOp	4 math math: coreMonoidalTransport_εIso_inv, coreMonoidalTransport_μIso_hom, coreMonoidalTransport_εIso_hom, coreMonoidalTransport_μIso_inv
instComp 📖	CompOp	8 math math: CategoryTheory.Equivalence.mapGrp_counitIso, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Adjunction.mapGrp_unit, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapGrp_unitIso, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.Adjunction.mapGrp_counit, CategoryTheory.Functor.comp_mapGrp_one
instId 📖	CompOp	10 math math: CategoryTheory.Equivalence.mapGrp_counitIso, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso, CategoryTheory.Functor.mapGrp_id_one, CategoryTheory.Adjunction.mapGrp_unit, CategoryTheory.Equivalence.mapGrp_unitIso, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso, CategoryTheory.Adjunction.mapGrp_counit
ofLaxMonoidal 📖	CompOp	—
ofOplaxMonoidal 📖	CompOp	—
prod' 📖	CompOp	—
toLaxMonoidal 📖	CompOp	258 math math: CategoryTheory.Functor.Braided.ext_iff, CategoryTheory.obj_ε_app_assoc, ext_iff, CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom, commTensorLeft_hom_app, CategoryTheory.Equivalence.mapMon_inverse, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc, whiskerLeft_η_ε, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Functor.map_mul, CategoryTheory.Mon.forget_μ, natTransIsMonoidal_of_transport, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse, CategoryTheory.Functor.mapCommGrp_obj_grp_one, εIso_hom, CategoryTheory.Adjunction.mapMon_unit, whiskerLeft_μ_δ_assoc, CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.Mon.forget_ε, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.MonoidalOpposite.mopFunctor_ε, η_ε_assoc, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, inv_μ, map_associator_inv_assoc, CategoryTheory.μ_δ_app_assoc, toUnit_ε_assoc, CategoryTheory.η_ε_app_assoc, map_associator_assoc, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, transport_μ, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, map_μ_δ_assoc, lift_μ_assoc, whiskerRight_η_ε, δ_μ, whiskerLeft_μ_δ, map_rightUnitor_inv, CategoryTheory.Grp.ε_def, CategoryTheory.sheafToPresheaf_μ, map_leftUnitor_inv, CategoryTheory.ε_η_app_assoc, map_associator, CategoryTheory.Adjunction.ε_comp_map_ε_assoc, CategoryTheory.obj_zero_map_μ_app_assoc, ε_η, CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal, CategoryTheory.ObjectProperty.ι_η, map_whiskerRight, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, whiskerRight_μ_δ_assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv, CategoryTheory.Localization.Monoidal.lifting_isMonoidal, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', CategoryTheory.Functor.mapGrp_obj_grp_one, map_ε_η_assoc, CategoryTheory.NatTrans.IsMonoidal.of_cartesianMonoidalCategory, CategoryTheory.obj_μ_app, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv, μ_comp_assoc, map_associator'_assoc, μ_fst_assoc, coreMonoidalTransport_μIso_hom, coreMonoidalTransport_εIso_hom, map_δ_μ_assoc, map_whiskerLeft_assoc, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, whiskerLeft_ε_η_assoc, transport_ε, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, whiskerRight_η_ε_assoc, CategoryTheory.δ_μ_app, CategoryTheory.ObjectProperty.ι_ε, CategoryTheory.Equivalence.mapMon_unitIso, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.Center.ofBraided_ε_f, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ, transport_μ_assoc, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.right_unitality_app_assoc, CategoryTheory.η_app_obj, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, toLaxMonoidal_injective, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ, CategoryTheory.Grp.μ_def, CategoryTheory.Center.forget_ε, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε, whiskeringLeft_ε_app, map_leftUnitor_inv_assoc, whiskerRight_ε_η_assoc, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, CategoryTheory.obj_zero_map_μ_app, whiskeringLeft_μ_app, CategoryTheory.monoidalUnopUnop_ε, map_associator_inv, CategoryTheory.associator_inv, CategoryTheory.Adjunction.mapMon_counit, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc, μ_of_cartesianMonoidalCategory, map_associator_inv', inv_η, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc, CategoryTheory.Functor.diag_μ, ModuleCat.free_ε_one, instIsIsoμ, toUnit_ε, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit, map_associator_inv'_assoc, CategoryTheory.Functor.Braided.braided, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.monoidalOpOp_μ, CategoryTheory.Discrete.monoidalFunctor_ε, μIso_hom, CategoryTheory.Adjunction.ε_comp_map_ε, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app, CategoryTheory.unitOfTensorIsoUnit_inv_app, map_associator', CategoryTheory.obj_η_app_assoc, ModuleCat.free_μ_freeMk_tmul_freeMk, CategoryTheory.MonoidalCategory.tensoringRight_ε, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage, inv_ε, CategoryTheory.Functor.mapGrp_map_hom_hom, μ_comp, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_assoc, whiskerRight_μ_δ, CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.ε_app_obj, CategoryTheory.Equivalence.mapMon_counitIso, CategoryTheory.obj_μ_inv_app, μ_fst, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Functor.Full.mapMon, CategoryTheory.monoidalOpOp_ε, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.ObjectProperty.ι_μ, ε_of_cartesianMonoidalCategory, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app, map_μ_δ, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc, Action.forget_ε, map_tensor_assoc, CategoryTheory.MonoidalOpposite.mopFunctor_μ, CategoryTheory.μ_δ_app, inv_δ, whiskerLeft_δ_μ, whiskerLeft_ε_η, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app, CategoryTheory.Equivalence.ε_comp_map_ε, CategoryTheory.Center.ofBraided_μ_f, CategoryTheory.ε_η_app, whiskerRight_δ_μ, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc, map_whiskerRight_assoc, map_ε_η, CategoryTheory.Discrete.addMonoidalFunctor_μ, CategoryTheory.MonoidalOpposite.unmopFunctor_μ, instIsIsoε, CategoryTheory.Equivalence.mapMon_functor, CategoryTheory.Pi.monoidalPi_ε, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc, map_whiskerLeft, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, map_δ_μ, CategoryTheory.Discrete.addMonoidalFunctor_ε, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, CategoryTheory.monoidalUnopUnop_μ, whiskerRight_ε_η, CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal, CategoryTheory.Functor.essImage_mapMon, μ_snd, map_η_ε_assoc, CategoryTheory.sheafToPresheaf_ε, CategoryTheory.Localization.Monoidal.β_hom_app, Action.FunctorCategoryEquivalence.functor_μ, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor, μ_snd_assoc, map_η_ε, CategoryTheory.Pi.monoidalPi'_ε, map_tensor, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.obj_μ_app_assoc, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left, μNatIso_hom_app, CategoryTheory.Functor.homMonoidHom_apply, CategoryTheory.ObjectProperty.ιOfLE_ε, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor, Action.forget_μ, CategoryTheory.Discrete.monoidalFunctor_μ, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, CategoryTheory.obj_μ_zero_app, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Pi.monoidalPi_μ, CategoryTheory.obj_μ_inv_app_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Comon.forget_μ, CategoryTheory.MonoidalOpposite.unmopFunctor_ε, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit, CategoryTheory.unitOfTensorIsoUnit_hom_app, lift_μ, CategoryTheory.Equivalence.ε_comp_map_ε_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, CategoryTheory.obj_ε_app, commTensorRight_hom_app, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, whiskerRight_δ_μ_assoc, CategoryTheory.δ_μ_app_assoc, δ_μ_assoc, transport_ε_assoc, CategoryTheory.obj_η_app, CategoryTheory.Comon.forget_ε, ε_η_assoc, CategoryTheory.ObjectProperty.ιOfLE_μ, CategoryTheory.Pi.μ_def, map_rightUnitor_inv_assoc, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Center.forget_μ, CategoryTheory.Functor.diag_ε, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, Rep.linearization_ε_hom, whiskerLeft_η_ε_assoc, CategoryTheory.Pi.ε_def, CategoryTheory.MonoidalCategory.tensor_ε, CategoryTheory.right_unitality_app, CategoryTheory.Functor.map_one, CategoryTheory.η_ε_app, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor, μ_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc, CategoryTheory.MonoidalCategory.tensor_μ, CategoryTheory.Pi.monoidalPi'_μ, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right, CategoryTheory.Functor.comp_mapGrp_one, μ_δ_assoc, Action.FunctorCategoryEquivalence.functor_ε, Rep.linearization_μ_hom, CategoryTheory.associator_hom, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc, η_ε, CategoryTheory.MonoidalCategory.tensoringRight_μ, whiskerLeft_δ_μ_assoc, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
toOplaxMonoidal 📖	CompOp	203 math math: Action.forget_η, CategoryTheory.Pi.monoidalPi'_η, CategoryTheory.Functor.Braided.ext_iff, CategoryTheory.obj_ε_app_assoc, CategoryTheory.Pi.monoidalPi_δ, μNatIso_inv_app, ext_iff, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, CategoryTheory.MonoidalOpposite.unmopFunctor_δ, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc, whiskerLeft_η_ε, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse, whiskerLeft_μ_δ_assoc, commTensorRight_inv_app, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, instIsIsoδ, η_ε_assoc, coreMonoidalTransport_εIso_inv, inv_μ, map_associator_inv_assoc, CategoryTheory.μ_δ_app_assoc, CategoryTheory.Center.forget_η, CategoryTheory.η_ε_app_assoc, map_associator_assoc, map_μ_δ_assoc, instIsIsoη, whiskerRight_η_ε, δ_μ, whiskerLeft_μ_δ, CategoryTheory.monoidalOpOp_δ, CategoryTheory.Bimon.toComon_map_hom, CategoryTheory.ε_η_app_assoc, map_associator, CategoryTheory.obj_zero_map_μ_app_assoc, ε_η, map_whiskerRight, whiskerRight_μ_δ_assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom, map_ε_η_assoc, CategoryTheory.obj_μ_app, CategoryTheory.Functor.diag_δ, Action.FunctorCategoryEquivalence.functor_δ, map_associator'_assoc, CategoryTheory.Equivalence.map_η_comp_η, map_δ_μ_assoc, CategoryTheory.Comon.forget_η, map_whiskerLeft_assoc, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, whiskerLeft_ε_η_assoc, CategoryTheory.Comon.forget_δ, whiskerRight_η_ε_assoc, CategoryTheory.δ_μ_app, CategoryTheory.MonoidalOpposite.mopFunctor_η, transport_δ, CategoryTheory.MonoidalCategory.tensoringRight_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.η_app_obj, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, map_rightUnitor_assoc, whiskerRight_ε_η_assoc, CategoryTheory.obj_zero_map_μ_app, CategoryTheory.sheafToPresheaf_δ, map_associator_inv, CategoryTheory.associator_inv, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Pi.η_def, map_associator_inv', inv_η, Action.forget_δ, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.Center.ofBraided_δ_f, CategoryTheory.monoidalUnopUnop_δ, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc, coreMonoidalTransport_μIso_inv, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε, map_associator_inv'_assoc, Rep.linearization_η_hom_apply, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.ObjectProperty.ι_δ, CategoryTheory.Grp.δ_def, CategoryTheory.monoidalOpOp_η, ModuleCat.free_η_freeMk, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse, whiskeringLeft_η_app, CategoryTheory.unitOfTensorIsoUnit_inv_app, map_associator', CategoryTheory.obj_η_app_assoc, CategoryTheory.Functor.map_braiding_assoc, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc, transport_η_assoc, inv_ε, CategoryTheory.Adjunction.map_η_comp_η_assoc, whiskerRight_μ_δ, commTensorLeft_inv_app, CategoryTheory.ε_app_obj, CategoryTheory.obj_μ_inv_app, CategoryTheory.MonoidalCategory.tensor_η, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.Equivalence.map_η_comp_η_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, map_μ_δ, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Discrete.addMonoidalFunctor_δ, CategoryTheory.Over.η_pullback_left, μIso_inv, map_tensor_assoc, CategoryTheory.μ_δ_app, inv_δ, whiskerLeft_δ_μ, whiskerLeft_ε_η, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app, transport_η, CategoryTheory.ε_η_app, whiskerRight_δ_μ, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc, ModuleCat.free_δ_freeMk, map_whiskerRight_assoc, map_leftUnitor, map_ε_η, toOplaxMonoidal_injective, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor, CategoryTheory.sheafToPresheaf_η, Rep.linearization_δ_hom, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc, map_whiskerLeft, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, CategoryTheory.MonoidalCategory.tensor_δ, map_δ_μ, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η, whiskerRight_ε_η, CategoryTheory.Functor.diag_η, CategoryTheory.Pi.δ_def, CategoryTheory.Pi.monoidalPi'_δ, CategoryTheory.Functor.FullyFaithful.grpObj_mul, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app, CategoryTheory.Mon.forget_η, map_η_ε_assoc, CategoryTheory.Discrete.addMonoidalFunctor_η, CategoryTheory.Localization.Monoidal.β_hom_app, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor, map_η_ε, map_tensor, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.obj_μ_app_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc, CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_inv_app_app, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor, CategoryTheory.obj_μ_zero_app, CategoryTheory.Mon.forget_δ, CategoryTheory.Grp.η_def, map_leftUnitor_assoc, CategoryTheory.Functor.FullyFaithful.grpObj_one, CategoryTheory.obj_μ_inv_app_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse, whiskeringLeft_δ_app, CategoryTheory.MonoidalOpposite.unmopFunctor_η, CategoryTheory.Pi.monoidalPi_η, CategoryTheory.unitOfTensorIsoUnit_hom_app, εIso_inv, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, CategoryTheory.Discrete.monoidalFunctor_η, CategoryTheory.obj_ε_app, CategoryTheory.Center.forget_δ, map_rightUnitor, whiskerRight_δ_μ_assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom, CategoryTheory.δ_μ_app_assoc, CategoryTheory.MonoidalOpposite.mopFunctor_δ, δ_μ_assoc, CategoryTheory.Adjunction.map_η_comp_η, transport_δ_assoc, CategoryTheory.ObjectProperty.ιOfLE_η, CategoryTheory.obj_η_app, ε_η_assoc, CategoryTheory.monoidalUnopUnop_η, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Center.ofBraided_η_f, CategoryTheory.Functor.map_braiding, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop, whiskerLeft_η_ε_assoc, CategoryTheory.Discrete.monoidalFunctor_δ, CategoryTheory.η_ε_app, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.ObjectProperty.ιOfLE_δ, μ_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc, CategoryTheory.MonoidalCategory.tensoringRight_η, Action.FunctorCategoryEquivalence.functor_η, μ_δ_assoc, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, CategoryTheory.associator_hom, η_ε, whiskerLeft_δ_μ_assoc, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom
transport 📖	CompOp	9 math math: natTransIsMonoidal_of_transport, transport_μ, transport_ε, transport_δ, transport_μ_assoc, transport_η_assoc, transport_η, transport_ε_assoc, transport_δ_assoc
εIso 📖	CompOp	3 math math: εIso_hom, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso, εIso_inv
μIso 📖	CompOp	3 math math: μIso_hom, μIso_inv, CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso
μNatIso 📖	CompOp	2 math math: μNatIso_inv_app, μNatIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commTensorLeft_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category commTensorLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	—
commTensorLeft_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category commTensorLeft CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	—
commTensorRight_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category commTensorRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	—
commTensorRight_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category commTensorRight CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	—
coreMonoidalTransport_εIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.εIso coreMonoidalTransport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	—	—
coreMonoidalTransport_εIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.εIso coreMonoidalTransport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	—
coreMonoidalTransport_μIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.μIso coreMonoidalTransport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	—
coreMonoidalTransport_μIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.μIso coreMonoidalTransport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc
ext 📖	—	CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ	—	—	—
ext_iff 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ	—	ext
instIsIsoδ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	CategoryTheory.Iso.isIso_inv
instIsIsoε 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	CategoryTheory.Iso.isIso_hom
instIsIsoη 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	CategoryTheory.Iso.isIso_inv
instIsIsoμ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Iso.isIso_hom
inv_δ 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal instIsIsoδ CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	instIsIsoδ instIsIsoμ CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_inv
inv_ε 📖	mathematical	—	CategoryTheory.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal instIsIsoε CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	instIsIsoε instIsIsoη CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_inv
inv_η 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal instIsIsoη CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	instIsIsoη εIso_hom CategoryTheory.Iso.comp_inv_eq_id εIso_inv CategoryTheory.IsIso.inv_hom_id
inv_μ 📖	mathematical	—	CategoryTheory.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal instIsIsoμ CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	instIsIsoμ μIso_inv CategoryTheory.IsIso.inv_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.inv_eq_inv CategoryTheory.IsIso.inv_inv CategoryTheory.IsIso.Iso.inv_inv
map_associator 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Functor.LaxMonoidal.associativity whiskerRight_δ_μ_assoc δ_μ_assoc
map_associator' 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Functor.LaxMonoidal.associativity_assoc μ_δ_assoc whiskerLeft_μ_δ CategoryTheory.Category.comp_id
map_associator'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_associator'
map_associator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_associator
map_associator_inv 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.instIsSplitEpiMap CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.map_hom_inv_id map_associator CategoryTheory.Category.assoc CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc whiskerRight_δ_μ_assoc δ_μ CategoryTheory.Category.comp_id CategoryTheory.Functor.LaxMonoidal.associativity_inv CategoryTheory.Iso.hom_inv_id_assoc
map_associator_inv' 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom map_associator' CategoryTheory.Functor.LaxMonoidal.associativity_assoc μ_δ_assoc whiskerLeft_μ_δ CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc whiskerRight_μ_δ
map_associator_inv'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_associator_inv'
map_associator_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_associator_inv
map_leftUnitor 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Functor.LaxMonoidal.left_unitality whiskerRight_η_ε_assoc δ_μ_assoc
map_leftUnitor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_leftUnitor
map_leftUnitor_inv 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ	—	CategoryTheory.Functor.OplaxMonoidal.left_unitality CategoryTheory.Category.assoc whiskerRight_η_ε_assoc δ_μ CategoryTheory.Category.comp_id
map_leftUnitor_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_leftUnitor_inv
map_rightUnitor 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Functor.LaxMonoidal.right_unitality whiskerLeft_η_ε_assoc δ_μ_assoc
map_rightUnitor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_rightUnitor
map_rightUnitor_inv 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ	—	CategoryTheory.Functor.OplaxMonoidal.right_unitality CategoryTheory.Category.assoc whiskerLeft_η_ε_assoc δ_μ CategoryTheory.Category.comp_id
map_rightUnitor_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_rightUnitor_inv
map_tensor 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Functor.LaxMonoidal.μ_natural δ_μ_assoc
map_tensor_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_tensor
map_whiskerLeft 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Functor.LaxMonoidal.μ_natural_right δ_μ_assoc
map_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_whiskerLeft
map_whiskerRight 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Functor.LaxMonoidal.μ_natural_left δ_μ_assoc
map_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_whiskerRight
map_δ_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.map_inv_hom_id
map_δ_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_δ_μ
map_ε_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.map_hom_inv_id
map_ε_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_ε_η
map_η_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.map_inv_hom_id
map_η_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_η_ε
map_μ_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.map_hom_inv_id
map_μ_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_μ_δ
toLaxMonoidal_injective 📖	mathematical	—	CategoryTheory.Functor.Monoidal CategoryTheory.Functor.LaxMonoidal toLaxMonoidal	—	ext CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom εIso_hom ε_η μIso_hom μ_δ
toOplaxMonoidal_injective 📖	mathematical	—	CategoryTheory.Functor.Monoidal CategoryTheory.Functor.OplaxMonoidal toOplaxMonoidal	—	ext CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv εIso_inv ε_η μIso_inv μ_δ
transport_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal transport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom	—	coreMonoidalTransport_μIso_inv
transport_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal transport CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' transport_δ
transport_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal transport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
transport_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal transport CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' transport_ε
transport_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal transport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
transport_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal transport CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' transport_η
transport_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal transport CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom	—	—
transport_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal transport CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' transport_μ
whiskerLeft_δ_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp δ_μ CategoryTheory.MonoidalCategory.whiskerLeft_id
whiskerLeft_δ_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_δ_μ
whiskerLeft_ε_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp ε_η CategoryTheory.MonoidalCategory.whiskerLeft_id
whiskerLeft_ε_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_ε_η
whiskerLeft_η_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp η_ε CategoryTheory.MonoidalCategory.whiskerLeft_id
whiskerLeft_η_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_η_ε
whiskerLeft_μ_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp μ_δ CategoryTheory.MonoidalCategory.whiskerLeft_id
whiskerLeft_μ_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_μ_δ
whiskerRight_δ_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.comp_whiskerRight δ_μ CategoryTheory.MonoidalCategory.id_whiskerRight
whiskerRight_δ_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_δ_μ
whiskerRight_ε_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.comp_whiskerRight ε_η CategoryTheory.MonoidalCategory.id_whiskerRight
whiskerRight_ε_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_ε_η
whiskerRight_η_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.comp_whiskerRight η_ε CategoryTheory.MonoidalCategory.id_whiskerRight
whiskerRight_η_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_η_ε
whiskerRight_μ_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.comp_whiskerRight μ_δ CategoryTheory.MonoidalCategory.id_whiskerRight
whiskerRight_μ_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_μ_δ
δ_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.CategoryStruct.id	—	—
δ_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_μ
εIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj εIso CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	—
εIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj εIso CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	—
ε_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	—
ε_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ε_η
η_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.CategoryStruct.id	—	—
η_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η toOplaxMonoidal CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' η_ε
μIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj μIso CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	—
μIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj μIso CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	—
μNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.Functor.prod CategoryTheory.MonoidalCategory.tensor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category μNatIso CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	—
μNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.Functor.prod CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category μNatIso CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	—
μ_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal CategoryTheory.CategoryStruct.id	—	—
μ_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.OplaxMonoidal.δ toOplaxMonoidal	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' μ_δ

CategoryTheory.Functor.OplaxMonoidal

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: CategoryTheory.Adjunction.isMonoidal_comp, comp_η, comp_δ
id 📖	CompOp	3 math math: id_δ, CategoryTheory.Adjunction.instIsMonoidalId, id_η
prod' 📖	CompOp	4 math math: CategoryTheory.Functor.prod'_δ_snd, CategoryTheory.Functor.prod'_δ_fst, CategoryTheory.Functor.prod'_η_snd, CategoryTheory.Functor.prod'_η_fst
δ 📖	CompOp	183 math math: CategoryTheory.Functor.Braided.ext_iff, δ_comp_tensorHom_η, associativity, CategoryTheory.obj_ε_app_assoc, δ_natural_left_assoc, CategoryTheory.Pi.monoidalPi_δ, CategoryTheory.Functor.Monoidal.μNatIso_inv_app, CategoryTheory.Functor.Monoidal.ext_iff, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, CategoryTheory.MonoidalOpposite.unmopFunctor_δ, δ_comp_η_tensorHom_assoc, CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse, left_unitality, CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc, δ_snd_assoc, CategoryTheory.Functor.Monoidal.commTensorRight_inv_app, associativity_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.Functor.mapAction_δ_hom, CategoryTheory.Functor.Monoidal.instIsIsoδ, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ, CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ, CategoryTheory.δ_naturalityₗ_assoc, CategoryTheory.Functor.Monoidal.inv_μ, CategoryTheory.Functor.Monoidal.map_associator_inv_assoc, CategoryTheory.μ_δ_app_assoc, CategoryTheory.Functor.Monoidal.map_associator_assoc, CategoryTheory.Functor.FullyFaithful.monObj_mul, CategoryTheory.Functor.Monoidal.map_μ_δ_assoc, δ_of_cartesianMonoidalCategory, CategoryTheory.Functor.prod'_δ_snd, δ_snd, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.monoidalOfHasFiniteProducts.δ_eq, CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ, CategoryTheory.monoidalOpOp_δ, CategoryTheory.Functor.Monoidal.map_associator, δ_fst_assoc, CategoryTheory.Functor.Monoidal.map_whiskerRight, CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', CategoryTheory.obj_μ_app, CategoryTheory.δ_naturalityᵣ_assoc, id_δ, CategoryTheory.Functor.diag_δ, Action.FunctorCategoryEquivalence.functor_δ, CategoryTheory.Functor.Monoidal.map_associator'_assoc, CategoryTheory.Functor.Monoidal.map_δ_μ_assoc, oplax_right_unitality, CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, δ_comp_whiskerLeft_δ_assoc, CategoryTheory.Comon.forget_δ, CategoryTheory.δ_μ_app, CategoryTheory.Functor.obj.Δ_def_assoc, CategoryTheory.Functor.Monoidal.transport_δ, CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_δ, CategoryTheory.MonoidalCategory.tensoringRight_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor, δ_comp_δ_whiskerRight_assoc, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc, lift_δ, CategoryTheory.δ_app, oplax_associativity, CategoryTheory.sheafToPresheaf_δ, CategoryTheory.Functor.Monoidal.map_associator_inv, CategoryTheory.associator_inv, CategoryTheory.Functor.Monoidal.map_associator_inv', Action.forget_δ, CategoryTheory.Center.ofBraided_δ_f, CategoryTheory.monoidalUnopUnop_δ, whiskeringRight_δ_app, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_inv, δ_natural_left, CategoryTheory.Functor.mapComon_obj_comon_comul, right_unitality_hom, CategoryTheory.Functor.Monoidal.map_associator_inv'_assoc, CategoryTheory.ObjectProperty.ι_δ, CategoryTheory.Functor.prod'_δ_fst, CategoryTheory.Grp.δ_def, CategoryTheory.unitOfTensorIsoUnit_inv_app, CategoryTheory.Functor.Monoidal.map_associator', CategoryTheory.Functor.map_braiding_assoc, δ_comp_whiskerLeft_δ, δ_comp_η_tensorHom, left_unitality_hom, CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ, CategoryTheory.Functor.Monoidal.commTensorLeft_inv_app, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ, CategoryTheory.ε_app_obj, CategoryTheory.obj_μ_inv_app, associativity_inv, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Functor.prod_δ_snd, δ_fst, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, CategoryTheory.Functor.Monoidal.map_μ_δ, CategoryTheory.Discrete.addMonoidalFunctor_δ, CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.Functor.Monoidal.map_tensor_assoc, oplax_left_unitality, CategoryTheory.μ_δ_app, CategoryTheory.Functor.Monoidal.inv_δ, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ, CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ, CategoryTheory.Pi.opLaxMonoidalPi_δ, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc, ModuleCat.free_δ_freeMk, CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc, CategoryTheory.Functor.Monoidal.map_leftUnitor, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ, Rep.linearization_δ_hom, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc, CategoryTheory.Functor.Monoidal.map_whiskerLeft, CategoryTheory.δ_naturality_assoc, CategoryTheory.MonoidalCategory.tensor_δ, CategoryTheory.Functor.Monoidal.map_δ_μ, CategoryTheory.δ_naturality, CategoryTheory.Pi.δ_def, CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ, CategoryTheory.Pi.monoidalPi'_δ, δ_comp_tensorHom_η_assoc, CategoryTheory.Functor.FullyFaithful.grpObj_mul, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app, CategoryTheory.Localization.Monoidal.β_hom_app, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor, CategoryTheory.Functor.Monoidal.map_tensor, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.obj_μ_app_assoc, ext_iff, δ_natural, δ_natural_right, CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost_inv_app_app, CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor, δ_natural_assoc, left_unitality_assoc, CategoryTheory.obj_μ_zero_app, CategoryTheory.Mon.forget_δ, CategoryTheory.Functor.Monoidal.map_leftUnitor_assoc, right_unitality_assoc, δ_comp_δ_whiskerRight, CategoryTheory.obj_μ_inv_app_assoc, CategoryTheory.δ_naturalityₗ, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc, CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Functor.Monoidal.whiskeringLeft_δ_app, CategoryTheory.δ_naturalityᵣ, CategoryTheory.obj_ε_app, CategoryTheory.Center.forget_δ, comp_δ, CategoryTheory.Functor.Monoidal.map_rightUnitor, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom, lift_δ_assoc, CategoryTheory.δ_μ_app_assoc, CategoryTheory.MonoidalOpposite.mopFunctor_δ, CategoryTheory.Functor.Monoidal.δ_μ_assoc, right_unitality, CategoryTheory.Functor.Monoidal.transport_δ_assoc, δ_natural_right_assoc, CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Functor.map_braiding, left_unitality_hom_assoc, CategoryTheory.Discrete.monoidalFunctor_δ, CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.ObjectProperty.ιOfLE_δ, CategoryTheory.Functor.Monoidal.μ_δ, CategoryTheory.Pi.opLaxMonoidalPi'_δ, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ_assoc, CategoryTheory.Functor.obj.Δ_def, CategoryTheory.Functor.prod_δ_fst, right_unitality_hom_assoc, associativity_inv_assoc, CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc, instIsIsoδ, CategoryTheory.Functor.Monoidal.μ_δ_assoc, CategoryTheory.associator_hom, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc
η 📖	CompOp	135 math math: Action.forget_η, CategoryTheory.Pi.monoidalPi'_η, CategoryTheory.Functor.Braided.ext_iff, δ_comp_tensorHom_η, CategoryTheory.Functor.Monoidal.ext_iff, δ_comp_η_tensorHom_assoc, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc, left_unitality, CategoryTheory.Functor.Monoidal.η_ε_assoc, CategoryTheory.Pi.opLaxMonoidalPi_η, CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_inv, CategoryTheory.η_naturality_assoc, η_of_cartesianMonoidalCategory, CategoryTheory.Center.forget_η, CategoryTheory.η_ε_app_assoc, CategoryTheory.Functor.Monoidal.instIsIsoη, CategoryTheory.Functor.Monoidal.whiskerRight_η_ε, CategoryTheory.ε_η_app_assoc, CategoryTheory.obj_zero_map_μ_app_assoc, CategoryTheory.Functor.obj.ε_def_assoc, CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom, CategoryTheory.Functor.Monoidal.map_ε_η_assoc, CategoryTheory.Equivalence.map_η_comp_η, CategoryTheory.Comon.forget_η, CategoryTheory.Functor.prod_η_snd, oplax_right_unitality, CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc, CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc, CategoryTheory.Adjunction.unit_app_unit_comp_map_η, CategoryTheory.MonoidalOpposite.mopFunctor_η, CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε, CategoryTheory.η_app_obj, CategoryTheory.Functor.mapAction_η_hom, CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc, CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc, CategoryTheory.obj_zero_map_μ_app, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Pi.η_def, CategoryTheory.Functor.Monoidal.inv_η, CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor, instIsIsoη, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε, right_unitality_hom, Rep.linearization_η_hom_apply, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.η_naturality, CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_εIso, CategoryTheory.monoidalOpOp_η, ModuleCat.free_η_freeMk, CategoryTheory.Functor.obj.ε_def, CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse, CategoryTheory.Functor.FullyFaithful.monObj_one, CategoryTheory.Functor.Monoidal.whiskeringLeft_η_app, CategoryTheory.obj_η_app_assoc, CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc, CategoryTheory.Functor.Monoidal.transport_η_assoc, comp_η, δ_comp_η_tensorHom, left_unitality_hom, CategoryTheory.Functor.Monoidal.inv_ε, CategoryTheory.Adjunction.map_η_comp_η_assoc, CategoryTheory.Functor.prod'_η_snd, CategoryTheory.MonoidalCategory.tensor_η, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.Pi.opLaxMonoidalPi'_η, CategoryTheory.Equivalence.map_η_comp_η_assoc, CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.η_app, CategoryTheory.Over.η_pullback_left, oplax_left_unitality, CategoryTheory.Functor.mapComon_obj_comon_counit, CategoryTheory.Functor.prod_η_fst, CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app, CategoryTheory.Functor.Monoidal.transport_η, CategoryTheory.ε_η_app, CategoryTheory.Functor.Monoidal.map_leftUnitor, CategoryTheory.Functor.Monoidal.map_ε_η, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor, CategoryTheory.sheafToPresheaf_η, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_inv, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η, CategoryTheory.Functor.Monoidal.whiskerRight_ε_η, CategoryTheory.Functor.diag_η, δ_comp_tensorHom_η_assoc, CategoryTheory.Mon.forget_η, id_η, CategoryTheory.Functor.Monoidal.map_η_ε_assoc, CategoryTheory.Discrete.addMonoidalFunctor_η, CategoryTheory.Functor.prod'_η_fst, CategoryTheory.Functor.Monoidal.map_η_ε, ext_iff, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc, whiskeringRight_η_app, left_unitality_assoc, CategoryTheory.monoidalOfHasFiniteProducts.η_eq, CategoryTheory.Grp.η_def, CategoryTheory.Functor.Monoidal.map_leftUnitor_assoc, right_unitality_assoc, CategoryTheory.Functor.FullyFaithful.grpObj_one, CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc, CategoryTheory.MonoidalOpposite.unmopFunctor_η, CategoryTheory.Pi.monoidalPi_η, CategoryTheory.unitOfTensorIsoUnit_hom_app, CategoryTheory.Functor.Monoidal.εIso_inv, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, CategoryTheory.Discrete.monoidalFunctor_η, CategoryTheory.Functor.Monoidal.map_rightUnitor, CategoryTheory.Adjunction.map_η_comp_η, right_unitality, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit, CategoryTheory.ObjectProperty.ιOfLE_η, CategoryTheory.obj_η_app, CategoryTheory.Functor.Monoidal.ε_η_assoc, CategoryTheory.monoidalUnopUnop_η, CategoryTheory.Center.ofBraided_η_f, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop, CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc, left_unitality_hom_assoc, CategoryTheory.η_ε_app, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη, right_unitality_hom_assoc, CategoryTheory.MonoidalCategory.tensoringRight_η, Action.FunctorCategoryEquivalence.functor_η, CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_η, CategoryTheory.Functor.Monoidal.η_ε, CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associativity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	oplax_associativity
associativity_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity
associativity_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc CategoryTheory.Iso.comp_inv_eq associativity CategoryTheory.Functor.map_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
associativity_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associativity_inv
comp_δ 📖	mathematical	—	δ CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map	—	—
comp_η 📖	mathematical	—	η CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map	—	—
ext 📖	—	η δ	—	—	—
ext_iff 📖	mathematical	—	η δ	—	ext
id_δ 📖	mathematical	—	δ CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
id_η 📖	mathematical	—	η CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
left_unitality 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerRight η	—	oplax_left_unitality
left_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerRight η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_unitality
left_unitality_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.whiskerRight η CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv left_unitality CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
left_unitality_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.whiskerRight η CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_unitality_hom
oplax_associativity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
oplax_left_unitality 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerRight η	—	—
oplax_right_unitality 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft η	—	—
right_unitality 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft η	—	oplax_right_unitality
right_unitality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_unitality
right_unitality_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft η CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv right_unitality CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
right_unitality_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft η CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_unitality_hom
δ_comp_tensorHom_η 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.tensorHom η CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.whiskerRight_id right_unitality_hom_assoc right_unitality CategoryTheory.Category.assoc CategoryTheory.Iso.map_inv_hom_id_assoc
δ_comp_tensorHom_η_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.tensorHom η CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_tensorHom_η
δ_comp_whiskerLeft_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	associativity CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
δ_comp_whiskerLeft_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_whiskerLeft_δ
δ_comp_δ_whiskerRight 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	associativity_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
δ_comp_δ_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ_whiskerRight
δ_comp_η_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.tensorHom η CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.id_whiskerLeft left_unitality_hom_assoc left_unitality CategoryTheory.Category.assoc CategoryTheory.Iso.map_inv_hom_id_assoc
δ_comp_η_tensorHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit δ CategoryTheory.MonoidalCategoryStruct.tensorHom η CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_η_tensorHom
δ_natural 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map	—	CategoryTheory.MonoidalCategory.tensorHom_def δ_natural_left_assoc δ_natural_right CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
δ_natural_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_natural
δ_natural_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map	—	—
δ_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_natural_left
δ_natural_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map	—	—
δ_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct δ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_natural_right

CategoryTheory.LaxMonoidalFunctor

Definitions

Name	Category	Theorems
laxMonoidal 📖	CompOp	4 math math: CategoryTheory.Functor.mapMonFunctor_obj, CategoryTheory.Functor.mapMonFunctor_map_app_hom, Hom.isMonoidal, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj
of 📖	CompOp	3 math math: CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj, of_toFunctor
toFunctor 📖	CompOp	27 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, TannakaDuality.FiniteGroup.forget_obj, CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_app, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, isoMk_inv, CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.Functor.mapCommMonFunctor_map_app, CategoryTheory.Functor.mapMonFunctor_obj, TannakaDuality.FiniteGroup.forget_map, CategoryTheory.Functor.mapMonFunctor_map_app_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app, CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor, CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_app, comp_hom, isoMk_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, Hom.isMonoidal, comp_hom_assoc, CategoryTheory.LaxBraidedFunctor.id_hom, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, id_hom, of_toFunctor, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_toFunctor 📖	mathematical	—	toFunctor of	—	—

---

← Back to Index