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

@[inline, reducible]

noncomputable abbrev AlgebraCat.instMonoidalCategory.tensorObj {R : Type u} [CommRing R] (X : AlgebraCat R) (Y : AlgebraCat R) : 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)

@[inline, reducible]

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) : AlgebraCat.instMonoidalCategory.tensorObj W Y ⟶ AlgebraCat.instMonoidalCategory.tensorObj X Z

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

Equations

• AlgebraCat.instMonoidalCategory.tensorHom f g = Algebra.TensorProduct.map f g

instance AlgebraCat.instMonoidalCategoryStructAlgebraCatInstCategoryAlgebraCat {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategoryStruct (AlgebraCat R)

Equations

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

theorem AlgebraCat.forget₂_map_associator_hom {R : Type u} [CommRing R] (X : AlgebraCat R) (Y : AlgebraCat R) (Z : AlgebraCat R) : (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj X) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj Y) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj Z)).hom

theorem AlgebraCat.forget₂_map_associator_inv {R : Type u} [CommRing R] (X : AlgebraCat R) (Y : AlgebraCat R) (Z : AlgebraCat R) : (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj X) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj Y) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).toPrefunctor.obj Z)).inv

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.

def AlgebraCat.toModuleCatMonoidalFunctor (R : Type u) [CommRing R] : CategoryTheory.MonoidalFunctor (AlgebraCat R) (ModuleCat R)

forget₂ (AlgebraCat R) (ModuleCat R) as a monoidal functor.

Equations

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

instance AlgebraCat.instFaithfulAlgebraCatInstCategoryAlgebraCatModuleCatToRingModuleCategoryToFunctorInstMonoidalCategoryMonoidalCategoryToLaxMonoidalFunctorToModuleCatMonoidalFunctor {R : Type u} [CommRing R] : CategoryTheory.Faithful (AlgebraCat.toModuleCatMonoidalFunctor R).toLaxMonoidalFunctor.toFunctor

Equations

• (_ : CategoryTheory.Faithful (AlgebraCat.toModuleCatMonoidalFunctor R).toLaxMonoidalFunctor.toFunctor) = (_ : CategoryTheory.Faithful (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)))