Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice

The preorder category of a meet-semilattice with a greatest element is Cartesian monoidal #

The preorder category of a meet-semilattice C with a greatest element is Cartesian monoidal.

A symmetric monoidal structure on the preorder category is automatically provided by the instance and CartesianMonoidalCategory.toSymmetricCategory.

source
🔸 coverage
@[implicit_reducible]
noncomputable def CategoryTheory.SemilatticeInf.cartesianMonoidalCategory (C : Type u) [SemilatticeInf C] [OrderTop C] :
CartesianMonoidalCategory C

Cartesian monoidal structure for the preorder category of a meet-semilattice with a greatest element.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    noncomputable def CategoryTheory.SemilatticeInf.braidedCategory (C : Type u) [SemilatticeInf C] [OrderTop C] :
    BraidedCategory C

    Braided structure for the preorder category of a meet-semilattice with a greatest element.

    Instances For
      source
      📐 coverage
      theorem CategoryTheory.SemilatticeInf.tensorObj {C : Type u} [SemilatticeInf C] [OrderTop C] {X Y : C} :
      MonoidalCategoryStruct.tensorObj X Y = X ⊓ Y
      source
      📐 coverage
      theorem CategoryTheory.SemilatticeInf.tensorUnit {C : Type u} [SemilatticeInf C] [OrderTop C] :
      MonoidalCategoryStruct.tensorUnit C = ⊤