The monoidal category structure on R-algebras

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

• AlgCat.instMonoidalCategory.tensorObj X Y = AlgCat.of R (TensorProduct R ↑X ↑Y)

@[simp]

theorem AlgCat.instMonoidalCategory.tensorObj_carrier {R : Type u} [CommRing R] (X Y : AlgCat R) : ↑(tensorObj X Y) = TensorProduct R ↑X ↑Y

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

• AlgCat.instMonoidalCategory.tensorHom f g = AlgCat.ofHom (Algebra.TensorProduct.map (AlgCat.Hom.hom f) (AlgCat.Hom.hom g))

instance AlgCat.instMonoidalCategoryStruct {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategoryStruct (AlgCat R)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance AlgCat.instMonoidalCategory {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategory (AlgCat R)

Equations

• One or more equations did not get rendered due to their size.