Documentation

Mathlib.Algebra.Category.AlgCat.Monoidal

The monoidal category structure on R-algebras #

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

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

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

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

      Equations
        Instances For
          source
          instance AlgCat.instMonoidalCategoryStruct {R : Type u} [CommRing R] :
          CategoryTheory.MonoidalCategoryStruct (AlgCat R)
          Equations
            source
            noncomputable instance AlgCat.instMonoidalCategory {R : Type u} [CommRing R] :
            CategoryTheory.MonoidalCategory (AlgCat R)
            Equations