Monoidal

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

Statistics

Metric	Count
Definitions functorMonoidal, inverseMonoidal, diagonalSuccIsoTensorDiagonal, diagonalSuccIsoTensorTrivial, functorCategoryEquivalenceFunctorMonoidal, functorCategoryEquivalenceInverseMonoidal, instBraidedCategory, instBraidedForget, instLeftRigidCategory, instLeftRigidCategoryFunctorSingleObj, instMonoidalCategory, instMonoidalForget, instRightRigidCategory, instRightRigidCategoryFunctorSingleObj, instRigidCategory, instRigidCategoryFunctorSingleObj, instSymmetricCategory, leftRegularTensorIso, tensorUnitIso, instLaxMonoidalActionMapAction, instMonoidalActionMapAction, instOplaxMonoidalActionMapAction	22
Theorems functor_δ, functor_ε, functor_η, functor_μ, associator_hom_hom, associator_inv_hom, diagonalSuccIsoTensorDiagonal_hom_hom, diagonalSuccIsoTensorDiagonal_inv_hom, diagonalSuccIsoTensorTrivial_hom_hom_apply, diagonalSuccIsoTensorTrivial_inv_hom_apply, forget_δ, forget_ε, forget_η, forget_μ, instMonoidalLinear, instMonoidalPreadditive, leftDual_v, leftDual_ρ, leftRegularTensorIso_hom_hom, leftRegularTensorIso_inv_hom, leftUnitor_hom_hom, leftUnitor_inv_hom, rightDual_v, rightDual_ρ, rightUnitor_hom_hom, rightUnitor_inv_hom, tensorHom_hom, tensorObj_V, tensorUnit_V, tensorUnit_ρ, tensor_ρ, whiskerLeft_hom, whiskerRight_hom, β_hom_hom, β_inv_hom, mapAction_δ_hom, mapAction_ε_hom, mapAction_η_hom, mapAction_μ_hom	39
Total	61

Action

Definitions

Name	Category	Theorems
diagonalSuccIsoTensorDiagonal 📖	CompOp	2 math math: diagonalSuccIsoTensorDiagonal_inv_hom, diagonalSuccIsoTensorDiagonal_hom_hom
diagonalSuccIsoTensorTrivial 📖	CompOp	2 math math: diagonalSuccIsoTensorTrivial_inv_hom_apply, diagonalSuccIsoTensorTrivial_hom_hom_apply
functorCategoryEquivalenceFunctorMonoidal 📖	CompOp	—
functorCategoryEquivalenceInverseMonoidal 📖	CompOp	—
instBraidedCategory 📖	CompOp	2 math math: β_inv_hom, β_hom_hom
instBraidedForget 📖	CompOp	—
instLeftRigidCategory 📖	CompOp	2 math math: leftDual_v, leftDual_ρ
instLeftRigidCategoryFunctorSingleObj 📖	CompOp	—
instMonoidalCategory 📖	CompOp	81 math math: forget_η, Representation.repOfTprodIso_inv_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, leftRegularTensorIso_inv_hom, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, FDRep.char_tensor, Representation.repOfTprodIso_apply, diagonalSuccIsoTensorDiagonal_inv_hom, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, CategoryTheory.Functor.mapAction_δ_hom, tensorObj_V, TannakaDuality.FiniteGroup.forget_obj, leftUnitor_inv_hom, rightDual_ρ, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, whiskerRight_hom, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, Rep.homEquiv_apply_hom, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, FunctorCategoryEquivalence.functor_δ, Rep.homEquiv_def, Rep.coinvariantsTensorFreeLEquiv_apply, tensorUnit_ρ, CategoryTheory.Functor.mapAction_η_hom, diagonalSuccIsoTensorTrivial_inv_hom_apply, forget_δ, Rep.finsuppTensorRight_hom_hom, CategoryTheory.Functor.mapAction_ε_hom, TannakaDuality.FiniteGroup.forget_map, Rep.tensor_ρ, Rep.linearization_η_hom_apply, rightDual_v, leftRegularTensorIso_hom_hom, CategoryTheory.Functor.mapAction_μ_hom, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, Rep.finsuppTensorRight_inv_hom, forget_ε, tensorHom_hom, Rep.finsuppTensorLeft_inv_hom, associator_hom_hom, Rep.leftRegularTensorTrivialIsoFree_inv_hom, Rep.linearization_δ_hom, whiskerLeft_hom, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.finsuppTensorLeft_hom_hom, Rep.coinvariantsTensorMk_apply, tensorUnit_V, Rep.homEquiv_symm_apply_hom, instMonoidalPreadditive, FunctorCategoryEquivalence.functor_μ, tensor_ρ, Rep.ihom_coev_app_hom, β_inv_hom, diagonalSuccIsoTensorDiagonal_hom_hom, rightUnitor_hom_hom, forget_μ, diagonalSuccIsoTensorTrivial_hom_hom_apply, leftDual_v, associator_inv_hom, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, leftDual_ρ, groupHomology.inhomogeneousChains.d_eq, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, rightUnitor_inv_hom, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, instMonoidalLinear, Rep.ihom_obj_ρ_def, TannakaDuality.FiniteGroup.equivHom_surjective, Rep.leftRegularTensorTrivialIsoFree_hom_hom, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.dualTensorIsoLinHom_hom_hom, Rep.linearization_ε_hom, β_hom_hom, TannakaDuality.FiniteGroup.equivHom_apply, leftUnitor_hom_hom, FunctorCategoryEquivalence.functor_η, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, FunctorCategoryEquivalence.functor_ε, Rep.linearization_μ_hom
instMonoidalForget 📖	CompOp	4 math math: forget_η, forget_δ, forget_ε, forget_μ
instRightRigidCategory 📖	CompOp	2 math math: rightDual_ρ, rightDual_v
instRightRigidCategoryFunctorSingleObj 📖	CompOp	—
instRigidCategory 📖	CompOp	—
instRigidCategoryFunctorSingleObj 📖	CompOp	—
instSymmetricCategory 📖	CompOp	—
leftRegularTensorIso 📖	CompOp	2 math math: leftRegularTensorIso_inv_hom, leftRegularTensorIso_hom_hom
tensorUnitIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
associator_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id
diagonalSuccIsoTensorDiagonal_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.types diagonal CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular CategoryTheory.Iso.hom diagonalSuccIsoTensorDiagonal DFunLike.coe Equiv V EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Fin.consEquiv	—	—
diagonalSuccIsoTensorDiagonal_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular diagonal CategoryTheory.Iso.inv diagonalSuccIsoTensorDiagonal DFunLike.coe Equiv V EquivLike.toFunLike Equiv.instEquivLike Fin.consEquiv	—	—
diagonalSuccIsoTensorTrivial_hom_hom_apply 📖	mathematical	—	Hom.hom CategoryTheory.types DivInvMonoid.toMonoid Group.toDivInvMonoid diagonal CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular trivial CategoryTheory.Iso.hom diagonalSuccIsoTensorTrivial MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	CategoryTheory.MonoidalCategory.id_tensorHom Fin.insertNthEquiv_zero mkIso.congr_simp Fin.cons_zero Fin.cons_succ
diagonalSuccIsoTensorTrivial_inv_hom_apply 📖	mathematical	—	Hom.hom CategoryTheory.types DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular trivial diagonal CategoryTheory.Iso.inv diagonalSuccIsoTensorTrivial CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm functorCategoryEquivalence Function.hasSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Fin.partialProd	—	Fin.isEmpty' CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.Category.assoc rightUnitor_hom_hom Fin.partialProd_zero mul_one Fin.insertNthEquiv_zero mkIso.congr_simp Fin.cons_zero Fin.cons_succ mul_assoc Fin.partialProd_succ'
forget_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ Action instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε Action instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η Action instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ Action instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
instMonoidalLinear 📖	mathematical	—	CategoryTheory.MonoidalLinear Action instCategory instPreadditive instLinear instMonoidalCategory instMonoidalPreadditive	—	instMonoidalPreadditive hom_ext CategoryTheory.MonoidalLinear.whiskerLeft_smul CategoryTheory.MonoidalLinear.smul_whiskerRight
instMonoidalPreadditive 📖	mathematical	—	CategoryTheory.MonoidalPreadditive Action instCategory instPreadditive instMonoidalCategory	—	hom_ext CategoryTheory.MonoidalPreadditive.whiskerLeft_zero CategoryTheory.MonoidalPreadditive.zero_whiskerRight CategoryTheory.MonoidalPreadditive.whiskerLeft_add CategoryTheory.MonoidalPreadditive.add_whiskerRight
leftDual_v 📖	mathematical	—	V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.HasLeftDual.leftDual Action instCategory instMonoidalCategory CategoryTheory.LeftRigidCategory.leftDual instLeftRigidCategory	—	—
leftDual_ρ 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.HasLeftDual.leftDual Action instCategory instMonoidalCategory CategoryTheory.LeftRigidCategory.leftDual instLeftRigidCategory MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ CategoryTheory.leftAdjointMate InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid CategoryTheory.SingleObj.inv_as_inv
leftRegularTensorIso_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.types DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular trivial V CategoryTheory.Iso.hom leftRegularTensorIso DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
leftRegularTensorIso_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.types DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory leftRegular trivial V CategoryTheory.Iso.inv leftRegularTensorIso DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ	—	—
leftUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
leftUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
rightDual_v 📖	mathematical	—	V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.HasRightDual.rightDual Action instCategory instMonoidalCategory CategoryTheory.RightRigidCategory.rightDual instRightRigidCategory	—	—
rightDual_ρ 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.HasRightDual.rightDual Action instCategory instMonoidalCategory CategoryTheory.RightRigidCategory.rightDual instRightRigidCategory MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ CategoryTheory.rightAdjointMate InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid CategoryTheory.SingleObj.inv_as_inv
rightUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
rightUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor instMonoidalCategory V	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
tensorHom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorHom instMonoidalCategory V	—	—
tensorObj_V 📖	mathematical	—	V CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
tensorUnit_V 📖	mathematical	—	V CategoryTheory.MonoidalCategoryStruct.tensorUnit Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
tensorUnit_ρ 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ Action instCategory instMonoidalCategory CategoryTheory.CategoryStruct.id	—	—
tensor_ρ 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ Action instCategory instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
whiskerLeft_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.whiskerLeft instMonoidalCategory V	—	—
whiskerRight_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm functorCategoryEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.whiskerRight instMonoidalCategory V	—	—
β_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory V	—	—
β_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj Action instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instBraidedCategory V	—	—

Action.FunctorCategoryEquivalence

Definitions

Name	Category	Theorems
functorMonoidal 📖	CompOp	4 math math: functor_δ, functor_μ, functor_η, functor_ε
inverseMonoidal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ Action Action.instCategory Action.instMonoidalCategory CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal functor CategoryTheory.Functor.Monoidal.toOplaxMonoidal functorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε Action Action.instCategory Action.instMonoidalCategory CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal functor CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η Action Action.instCategory Action.instMonoidalCategory CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal functor CategoryTheory.Functor.Monoidal.toOplaxMonoidal functorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ Action Action.instCategory Action.instMonoidalCategory CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidal functor CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
instLaxMonoidalActionMapAction 📖	CompOp	2 math math: mapAction_ε_hom, mapAction_μ_hom
instMonoidalActionMapAction 📖	CompOp	—
instOplaxMonoidalActionMapAction 📖	CompOp	2 math math: mapAction_δ_hom, mapAction_η_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapAction_δ_hom 📖	mathematical	—	Action.Hom.hom obj Action Action.instCategory mapAction CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory OplaxMonoidal.δ instOplaxMonoidalActionMapAction Action.V	—	—
mapAction_ε_hom 📖	mathematical	—	Action.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit Action Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory obj mapAction LaxMonoidal.ε instLaxMonoidalActionMapAction	—	—
mapAction_η_hom 📖	mathematical	—	Action.Hom.hom obj Action Action.instCategory mapAction CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory OplaxMonoidal.η instOplaxMonoidalActionMapAction	—	—
mapAction_μ_hom 📖	mathematical	—	Action.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj Action Action.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory obj mapAction LaxMonoidal.μ instLaxMonoidalActionMapAction Action.V	—	—

---

← Back to Index