Structures · Category theory
CategoryTheory.Functor.Monoidal
A functor between monoidal categories is monoidal if it is lax and oplax monoidals, and both data give inverse isomorphisms.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Functor
- Shape
- One type argument · adds ε_η, η_ε, μ_δ, δ_μ
Extends2
Extended by1
Concrete types that are instances28
- CategoryTheory.Functor
- CategoryTheory.Discrete
- ModuleCat
- CategoryTheory.Grp
- Action
- CategoryTheory.Mon
- CategoryTheory.ObjectProperty.FullSubcategory
- TopCat
- CategoryTheory.MonoidalOpposite
- CategoryTheory.Skeleton
- PresheafOfModules
- CategoryTheory.Sheaf
- CategoryTheory.Center
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
- CategoryTheory.Monoidal.Transported
- HopfAlgCat
- CategoryTheory.Comon
- BialgCat
- SSet
- CategoryTheory.FreeMonoidalCategory
- CategoryTheory.EndMonoidal
- LightProfinite
- LightCondSet
- FDRep
- SSet.Truncated
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by390
- CategoryTheory.Equivalence.IsMonoidal
- CategoryTheory.Functor.mapGrp
- CategoryTheory.Functor.mapAddGrp
- CategoryTheory.Functor.Monoidal.μIso
- CategoryTheory.Functor.Monoidal.δ_μ_assoc
- CategoryTheory.Functor.Monoidal.μ_δ
- CategoryTheory.Functor.Monoidal.εIso
- CategoryTheory.Functor.Monoidal.μIso_inv
- CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor
- CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop
- CategoryTheory.Functor.Monoidal.transport
- CategoryTheory.Functor.Monoidal.δ_μ
- CategoryTheory.Functor.Monoidal.μ_δ_assoc
- CategoryTheory.Functor.Monoidal.μ_fst
- CategoryTheory.Functor.Monoidal.μ_snd
- CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
- CategoryTheory.μ_δ_app
- CategoryTheory.Functor.mapAddGrpCompIso
- CategoryTheory.Functor.Monoidal.ε_η
- CategoryTheory.Functor.Monoidal.η_ε
- CategoryTheory.Functor.mapGrpCompIso
- CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp
- CategoryTheory.Functor.grpObjObj
- CategoryTheory.Functor.Monoidal.μIso_hom
- CategoryTheory.Localization.Monoidal.functorMonoidalOfComp
- CategoryTheory.Functor.FullyFaithful.grpObj
- CategoryTheory.Equivalence.mapAddMon
- CategoryTheory.unitOfTensorIsoUnit
- CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost
- CategoryTheory.equivOfTensorIsoUnit
- CategoryTheory.Functor.Monoidal.ε_η_assoc
- CategoryTheory.Functor.Monoidal.commTensorLeft
- CategoryTheory.Functor.addGrpObjObj
- CategoryTheory.Functor.mapGrpNatIso
- CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ
- CategoryTheory.Equivalence.mapAddGrp
- CategoryTheory.Functor.FullyFaithful.addGrpObj
- CategoryTheory.Functor.mapAddGrpNatIso
- CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc
- CategoryTheory.Functor.Monoidal.coreMonoidalTransport
- CategoryTheory.Equivalence.mapGrp
- CategoryTheory.Equivalence.mapMon
- CategoryTheory.Functor.mapGrpNatTrans
- CategoryTheory.Functor.Monoidal.map_ε_η
- CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ
- CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory
- CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app
- CategoryTheory.Functor.Monoidal.map_whiskerLeft
- CategoryTheory.Functor.mapAddGrpNatTrans
- CategoryTheory.Functor.Monoidal.map_associator