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
@[instance_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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_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.

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