Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice

Chosen finite products for the preorder category of a meet-semilattice with a greatest element #

The preorder category of a meet-semilattice C with a greatest element has chosen finite products.

A symmetric monoidal structure on the preorder category is automatically provided by the instances monoidalOfChosenFiniteProducts and ChosenFiniteProducts.instSymmetricCategory.

source
noncomputable def CategoryTheory.SemilatticeInf.chosenFiniteProducts (C : Type u) [SemilatticeInf C] [OrderTop C] :
ChosenFiniteProducts C

Chosen finite products 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
    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] :
    𝟙_ C = ⊤