Documentation

Mathlib.Algebra.Category.AlgebraCat.Monoidal

The monoidal category structure on R-algebras #

source
@[reducible, inline]
noncomputable abbrev AlgebraCat.instMonoidalCategory.tensorObj {R : Type u} [CommRing R] (X Y : AlgebraCat R) :
AlgebraCat R

Auxiliary definition used to fight a timeout when building AlgebraCat.instMonoidalCategory.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraCat.instMonoidalCategory.tensorObj_carrier {R : Type u} [CommRing R] (X Y : AlgebraCat R) :
    ↑(AlgebraCat.instMonoidalCategory.tensorObj X Y) = TensorProduct R ↑X ↑Y
    source
    @[reducible, inline]
    noncomputable abbrev AlgebraCat.instMonoidalCategory.tensorHom {R : Type u} [CommRing R] {W X Y Z : AlgebraCat R} (f : W ⟶ X) (g : Y ⟶ Z) :
    AlgebraCat.instMonoidalCategory.tensorObj W Y ⟶ AlgebraCat.instMonoidalCategory.tensorObj X Z

    Auxiliary definition used to fight a timeout when building AlgebraCat.instMonoidalCategory.

    Equations
    Instances For
      source
      instance AlgebraCat.instMonoidalCategoryStruct {R : Type u} [CommRing R] :
      CategoryTheory.MonoidalCategoryStruct (AlgebraCat R)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      noncomputable instance AlgebraCat.instMonoidalCategory {R : Type u} [CommRing R] :
      CategoryTheory.MonoidalCategory (AlgebraCat R)
      Equations
      • One or more equations did not get rendered due to their size.