The monoidal category structure on R-algebras #
@[simp]
theorem
AlgebraCat.instMonoidalCategory.tensorObj_carrier
{R : Type u}
[CommRing R]
(X : AlgebraCat R)
(Y : AlgebraCat R)
:
↑(AlgebraCat.instMonoidalCategory.tensorObj X Y) = TensorProduct R ↑X ↑Y
@[reducible, inline]
noncomputable abbrev
AlgebraCat.instMonoidalCategory.tensorObj
{R : Type u}
[CommRing R]
(X : AlgebraCat R)
(Y : AlgebraCat R)
:
Auxiliary definition used to fight a timeout when building
AlgebraCat.instMonoidalCategory
.
Equations
- AlgebraCat.instMonoidalCategory.tensorObj X Y = AlgebraCat.of R (TensorProduct R ↑X ↑Y)
Instances For
@[reducible, inline]
noncomputable abbrev
AlgebraCat.instMonoidalCategory.tensorHom
{R : Type u}
[CommRing R]
{W : AlgebraCat R}
{X : AlgebraCat R}
{Y : AlgebraCat R}
{Z : AlgebraCat R}
(f : W ⟶ X)
(g : Y ⟶ Z)
:
Auxiliary definition used to fight a timeout when building
AlgebraCat.instMonoidalCategory
.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
forget₂ (AlgebraCat R) (ModuleCat R)
as a monoidal functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
AlgebraCat.instFaithfulModuleCatToModuleCatMonoidalFunctor
{R : Type u}
[CommRing R]
:
(AlgebraCat.toModuleCatMonoidalFunctor R).Faithful
Equations
- ⋯ = ⋯