Documentation

Mathlib.Algebra.Category.AlgCat.Monoidal

The monoidal category structure on R-algebras #

@[reducible, inline]

noncomputable abbrev AlgCat.instMonoidalCategory.tensorObj {R : Type u} [CommRing R] (X Y : AlgCat R) :

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

Equations

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

Instances For

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

Instances For

@[instance_reducible]

noncomputable 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.

theorem AlgCat.hom_tensorHom {R : Type u} [CommRing R] {K L M N : AlgCat R} (f : K ⟶ L) (g : M ⟶ N) :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = Algebra.TensorProduct.map (Hom.hom f) (Hom.hom g)

theorem AlgCat.hom_whiskerLeft {R : Type u} [CommRing R] (L : AlgCat R) {M N : AlgCat R} (f : M ⟶ N) :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) = Algebra.TensorProduct.map (AlgHom.id R ↑L) (Hom.hom f)

theorem AlgCat.hom_whiskerRight {R : Type u} [CommRing R] {L M : AlgCat R} (f : L ⟶ M) (N : AlgCat R) :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) = Algebra.TensorProduct.map (Hom.hom f) (AlgHom.id R ↑N)

theorem AlgCat.hom_hom_leftUnitor {R : Type u} [CommRing R] {M : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(Algebra.TensorProduct.lid R ↑M)

theorem AlgCat.hom_inv_leftUnitor {R : Type u} [CommRing R] {M : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(Algebra.TensorProduct.lid R ↑M).symm

theorem AlgCat.hom_hom_rightUnitor {R : Type u} [CommRing R] {M : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = ↑(Algebra.TensorProduct.rid (↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))) R ↑M)

theorem AlgCat.hom_inv_rightUnitor {R : Type u} [CommRing R] {M : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv = ↑(Algebra.TensorProduct.rid (↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))) R ↑M).symm

theorem AlgCat.hom_hom_associator {R : Type u} [CommRing R] {M N K : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom = ↑(Algebra.TensorProduct.assoc R R R ↑M ↑N ↑K)

theorem AlgCat.hom_inv_associator {R : Type u} [CommRing R] {M N K : AlgCat R} :

Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv = ↑(Algebra.TensorProduct.assoc R R R ↑M ↑N ↑K).symm

@[instance_reducible]

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.