Structures · Category theory
CategoryTheory.CartesianMonoidalCategory
An instance of CartesianMonoidalCategory C bundles an explicit choice of a binary
product of two objects of C, and a terminal object in C.
Users should use the monoidal notation: X ⊗ Y for the product and 𝟙_ C for
the terminal object.
- Shape
- One type argument · adds tensorProductIsBinaryProduct
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances15
- CategoryTheory.Functor
- CategoryTheory.Over
- CategoryTheory.Grp
- CategoryTheory.Mon
- AlgebraicGeometry.Scheme
- CategoryTheory.ObjectProperty.FullSubcategory
- TopCat
- CommGrpCat
- GrpCat
- AddGrpCat
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
- CategoryTheory.Cat
- LightProfinite
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by1,285
- CategoryTheory.CartesianMonoidalCategory.lift
- CategoryTheory.Grp.X
- CategoryTheory.Grp.toMon
- CategoryTheory.AddGrp.X
- CategoryTheory.Hom.monoid
- CategoryTheory.AddGrp.toAddMon
- CategoryTheory.CartesianMonoidalCategory.hom_ext
- CategoryTheory.Hom.addMonoid
- CategoryTheory.CartesianMonoidalCategory.prodComparison
- CategoryTheory.CommGrp.X
- CategoryTheory.CartesianMonoidalCategory.lift_snd
- CategoryTheory.CartesianMonoidalCategory.lift_fst
- CategoryTheory.CommGrp.toGrp
- CategoryTheory.Functor.mapGrp
- CategoryTheory.Grp.forget₂Mon
- CategoryTheory.Functor.mapAddGrp
- CategoryTheory.Functor.mapCommGrp
- CategoryTheory.Hom.group
- CategoryTheory.Hom.addGroup
- CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst
- CategoryTheory.AddGrp.forget₂Mon
- CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd
- CategoryTheory.CommGrp.forget₂Grp
- CategoryTheory.RingObjCat.X
- CategoryTheory.toOver
- CategoryTheory.CommRingObjCat.X
- CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd
- CategoryTheory.CartesianMonoidalCategory.prodComparisonIso
- CategoryTheory.CartesianMonoidalCategory.comp_lift
- CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst
- CategoryTheory.zeroMul
- CategoryTheory.yonedaMonObj
- CategoryTheory.yonedaAddMonObj
- CategoryTheory.CartesianMonoidalCategory.tensorHom_fst
- CategoryTheory.CartesianMonoidalCategory.tensorHom_snd
- CategoryTheory.Preadditive.commGrpEquivalence
- CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans
- CategoryTheory.MonObj.comp_mul
- CategoryTheory.yonedaMon
- CategoryTheory.toOverUnit
- CategoryTheory.GrpObj.comp_inv
- CategoryTheory.CartesianMonoidalCategory.lift_fst_snd
- CategoryTheory.IsMonHom.monoidHom
- CategoryTheory.RingObjCat.Hom.hom
- CategoryTheory.AddGrpObj.comp_neg
- CategoryTheory.yonedaAddGrpObj
- CategoryTheory.yonedaGrpObj
- CategoryTheory.GrpObj.commutator
- CategoryTheory.AddMonObj.comp_add
- CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc