The monoidal category structure on R-modules

Mostly this uses existing machinery in LinearAlgebra.TensorProduct. We just need to provide a few small missing pieces to build the MonoidalCategory instance. The SymmetricCategory instance is in Algebra.Category.ModuleCat.Monoidal.Symmetric to reduce imports.

Note the universe level of the modules must be at least the universe level of the ring, so that we have a monoidal unit. For now, we simplify by insisting both universe levels are the same.

We construct the monoidal closed structure on ModuleCat R in Algebra.Category.ModuleCat.Monoidal.Closed.

If you're happy using the bundled ModuleCat R, it may be possible to mostly use this as an interface and not need to interact much with the implementation details.

def SemimoduleCat.MonoidalCategory.tensorObj {R : Type u} [CommSemiring R] (M : SemimoduleCat R) (N : SemimoduleCat R) : SemimoduleCat R

(implementation) tensor product of R-modules

def SemimoduleCat.MonoidalCategory.tensorHom {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} {M' N' : SemimoduleCat R} (f : M ⟶ N) (g : M' ⟶ N') : tensorObj M M' ⟶ tensorObj N N'

(implementation) tensor product of morphisms R-modules

def SemimoduleCat.MonoidalCategory.whiskerLeft {R : Type u} [CommSemiring R] (M : SemimoduleCat R) {N₁ N₂ : SemimoduleCat R} (f : N₁ ⟶ N₂) : tensorObj M N₁ ⟶ tensorObj M N₂

(implementation) left whiskering for R-modules

def SemimoduleCat.MonoidalCategory.whiskerRight {R : Type u} [CommSemiring R] {M₁ M₂ : SemimoduleCat R} (f : M₁ ⟶ M₂) (N : SemimoduleCat R) : tensorObj M₁ N ⟶ tensorObj M₂ N

(implementation) right whiskering for R-modules

theorem SemimoduleCat.MonoidalCategory.id_tensorHom_id {R : Type u} [CommSemiring R] (M : SemimoduleCat R) (N : SemimoduleCat R) : tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (of R (TensorProduct R ↑M ↑N))

theorem SemimoduleCat.MonoidalCategory.tensorHom_comp_tensorHom {R : Type u} [CommSemiring R] {X₁ Y₁ Z₁ : SemimoduleCat R} {X₂ Y₂ Z₂ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryTheory.CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)

def SemimoduleCat.MonoidalCategory.associator {R : Type u} [CommSemiring R] (M : SemimoduleCat R) (N : SemimoduleCat R) (K : SemimoduleCat R) : tensorObj (tensorObj M N) K ≅ tensorObj M (tensorObj N K)

(implementation) the associator for R-modules

def SemimoduleCat.MonoidalCategory.leftUnitor {R : Type u} [CommSemiring R] (M : SemimoduleCat R) : of R (TensorProduct R R ↑M) ≅ M

(implementation) the left unitor for R-modules

def SemimoduleCat.MonoidalCategory.rightUnitor {R : Type u} [CommSemiring R] (M : SemimoduleCat R) : of R (TensorProduct R (↑M) R) ≅ M

(implementation) the right unitor for R-modules

instance SemimoduleCat.MonoidalCategory.instMonoidalCategoryStruct {R : Type u} [CommSemiring R] : CategoryTheory.MonoidalCategoryStruct (SemimoduleCat R)

theorem SemimoduleCat.MonoidalCategory.tensorHom_def {R : Type u} [CommSemiring R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : SemimoduleCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = tensorHom f g

theorem SemimoduleCat.MonoidalCategory.whiskerLeft_def {R : Type u} [CommSemiring R] (M : SemimoduleCat R) {N₁ N₂ : SemimoduleCat R} (f : N₁ ⟶ N₂) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = whiskerLeft M f

theorem SemimoduleCat.MonoidalCategory.whiskerRight_def {R : Type u} [CommSemiring R] {X₁✝ X₂✝ : SemimoduleCat R} (f : X₁✝ ⟶ X₂✝) (N : SemimoduleCat R) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f N = whiskerRight f N

theorem SemimoduleCat.MonoidalCategory.tensorUnit_isAddCommMonoid {R : Type u} [CommSemiring R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R)).isAddCommMonoid = inst✝.toNonAssocSemiring.toAddCommMonoid

theorem SemimoduleCat.MonoidalCategory.rightUnitor_def {R : Type u} [CommSemiring R] (M : SemimoduleCat R) : CategoryTheory.MonoidalCategoryStruct.rightUnitor M = rightUnitor M

theorem SemimoduleCat.MonoidalCategory.associator_def {R : Type u} [CommSemiring R] (M N K : SemimoduleCat R) : CategoryTheory.MonoidalCategoryStruct.associator M N K = associator M N K

theorem SemimoduleCat.MonoidalCategory.tensorUnit_carrier {R : Type u} [CommSemiring R] : ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R)) = R

theorem SemimoduleCat.MonoidalCategory.tensorUnit_isModule {R : Type u} [CommSemiring R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R)).isModule = Semiring.toModule

theorem SemimoduleCat.MonoidalCategory.leftUnitor_def {R : Type u} [CommSemiring R] (M : SemimoduleCat R) : CategoryTheory.MonoidalCategoryStruct.leftUnitor M = leftUnitor M

theorem SemimoduleCat.MonoidalCategory.tensorObj_def {R : Type u} [CommSemiring R] (M N : SemimoduleCat R) : CategoryTheory.MonoidalCategoryStruct.tensorObj M N = tensorObj M N

theorem SemimoduleCat.MonoidalCategory.associator_naturality {R : Type u} [CommSemiring R] {X₁ : SemimoduleCat R} {X₂ : SemimoduleCat R} {X₃ : SemimoduleCat R} {Y₁ : SemimoduleCat R} {Y₂ : SemimoduleCat R} {Y₃ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

theorem SemimoduleCat.MonoidalCategory.pentagon {R : Type u} [CommSemiring R] (W : SemimoduleCat R) (X : SemimoduleCat R) (Y : SemimoduleCat R) (Z : SemimoduleCat R) : CategoryTheory.CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryTheory.CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom

theorem SemimoduleCat.MonoidalCategory.leftUnitor_naturality {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id (of R R)) f) (leftUnitor N).hom = CategoryTheory.CategoryStruct.comp (leftUnitor M).hom f

theorem SemimoduleCat.MonoidalCategory.rightUnitor_naturality {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom f (CategoryTheory.CategoryStruct.id (of R R))) (rightUnitor N).hom = CategoryTheory.CategoryStruct.comp (rightUnitor M).hom f

theorem SemimoduleCat.MonoidalCategory.triangle {R : Type u} [CommSemiring R] (M N : SemimoduleCat R) : CategoryTheory.CategoryStruct.comp (associator M (of R R) N).hom (tensorHom (CategoryTheory.CategoryStruct.id M) (leftUnitor N).hom) = tensorHom (rightUnitor M).hom (CategoryTheory.CategoryStruct.id N)

instance SemimoduleCat.monoidalCategory {R : Type u} [CommSemiring R] : CategoryTheory.MonoidalCategory (SemimoduleCat R)

instance SemimoduleCat.instCommSemiringCarrierTensorUnit {R : Type u} [CommSemiring R] : CommSemiring ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))

Remind ourselves that the monoidal unit, being just R, is still a commutative semiring.

theorem SemimoduleCat.hom_tensorHom {R : Type u} [CommSemiring R] {K L M N : SemimoduleCat R} (f : K ⟶ L) (g : M ⟶ N) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = TensorProduct.map (Hom.hom f) (Hom.hom g)

theorem SemimoduleCat.hom_whiskerLeft {R : Type u} [CommSemiring R] (L : SemimoduleCat R) {M N : SemimoduleCat R} (f : M ⟶ N) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) = LinearMap.lTensor (↑L) (Hom.hom f)

theorem SemimoduleCat.hom_whiskerRight {R : Type u} [CommSemiring R] {L M : SemimoduleCat R} (f : L ⟶ M) (N : SemimoduleCat R) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) = LinearMap.rTensor (↑N) (Hom.hom f)

theorem SemimoduleCat.hom_hom_leftUnitor {R : Type u} [CommSemiring R] {M : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(TensorProduct.lid R ↑M)

theorem SemimoduleCat.hom_inv_leftUnitor {R : Type u} [CommSemiring R] {M : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(TensorProduct.lid R ↑M).symm

theorem SemimoduleCat.hom_hom_rightUnitor {R : Type u} [CommSemiring R] {M : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = ↑(TensorProduct.rid R ↑M)

theorem SemimoduleCat.hom_inv_rightUnitor {R : Type u} [CommSemiring R] {M : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv = ↑(TensorProduct.rid R ↑M).symm

theorem SemimoduleCat.hom_hom_associator {R : Type u} [CommSemiring R] {M N K : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom = ↑(TensorProduct.assoc R ↑M ↑N ↑K)

theorem SemimoduleCat.hom_inv_associator {R : Type u} [CommSemiring R] {M N K : SemimoduleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv = ↑(TensorProduct.assoc R ↑M ↑N ↑K).symm

@[simp]

theorem SemimoduleCat.MonoidalCategory.tensorHom_tmul {R : Type u} [CommSemiring R] {K L M N : SemimoduleCat R} (f : K ⟶ L) (g : M ⟶ N) (k : ↑K) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (k ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom f) k ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m

@[simp]

theorem SemimoduleCat.MonoidalCategory.whiskerLeft_apply {R : Type u} [CommSemiring R] (L : SemimoduleCat R) {M N : SemimoduleCat R} (f : M ⟶ N) (l : ↑L) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f)) (l ⊗ₜ[R] m) = l ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom f) m

@[simp]

theorem SemimoduleCat.MonoidalCategory.whiskerRight_apply {R : Type u} [CommSemiring R] {L M : SemimoduleCat R} (f : L ⟶ M) (N : SemimoduleCat R) (l : ↑L) (n : ↑N) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)) (l ⊗ₜ[R] n) = (CategoryTheory.ConcreteCategory.hom f) l ⊗ₜ[R] n

@[simp]

theorem SemimoduleCat.MonoidalCategory.leftUnitor_hom_apply {R : Type u} [CommSemiring R] {M : SemimoduleCat R} (r : R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m

@[simp]

theorem SemimoduleCat.MonoidalCategory.leftUnitor_inv_apply {R : Type u} [CommSemiring R] {M : SemimoduleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m

@[simp]

theorem SemimoduleCat.MonoidalCategory.rightUnitor_hom_apply {R : Type u} [CommSemiring R] {M : SemimoduleCat R} (m : ↑M) (r : R) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m

@[simp]

theorem SemimoduleCat.MonoidalCategory.rightUnitor_inv_apply {R : Type u} [CommSemiring R] {M : SemimoduleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1

@[simp]

theorem SemimoduleCat.MonoidalCategory.associator_hom_apply {R : Type u} [CommSemiring R] {M N K : SemimoduleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom) (m ⊗ₜ[R] n ⊗ₜ[R] k) = m ⊗ₜ[R] (n ⊗ₜ[R] k)

@[simp]

theorem SemimoduleCat.MonoidalCategory.associator_inv_apply {R : Type u} [CommSemiring R] {M N K : SemimoduleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] k)) = m ⊗ₜ[R] n ⊗ₜ[R] k

def SemimoduleCat.MonoidalCategory.tensorLift {R : Type u} [CommSemiring R] {M₁ M₂ M₃ : SemimoduleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃

Construct for morphisms from the tensor product of two objects in SemimoduleCat.

@[simp]

theorem SemimoduleCat.MonoidalCategory.tensorLift_tmul {R : Type u} [CommSemiring R] {M₁ M₂ M₃ : SemimoduleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) (m : ↑M₁) (n : ↑M₂) : (CategoryTheory.ConcreteCategory.hom (tensorLift f h₁ h₂ h₃ h₄)) (m ⊗ₜ[R] n) = f m n

theorem SemimoduleCat.MonoidalCategory.tensor_ext {R : Type u} [CommSemiring R] {M₁ M₂ M₃ : SemimoduleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃} (h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)) : f = g

theorem SemimoduleCat.MonoidalCategory.tensor_ext₃' {R : Type u} [CommSemiring R] {M₁ M₂ M₃ M₄ : SemimoduleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂) M₃ ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) : f = g

Extensionality lemma for morphisms from a module of the form (M₁ ⊗ M₂) ⊗ M₃.

theorem SemimoduleCat.MonoidalCategory.tensor_ext₃ {R : Type u} [CommSemiring R] {M₁ M₂ M₃ M₄ : SemimoduleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃) ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))) : f = g

Extensionality lemma for morphisms from a module of the form M₁ ⊗ (M₂ ⊗ M₃).

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

theorem ModuleCat.MonoidalCategory.rightUnitor_def {R : Type u} [CommRing R] (M : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.rightUnitor M = (TensorProduct.rid R ↑M).toModuleIso

theorem ModuleCat.MonoidalCategory.tensorUnit_carrier {R : Type u} [CommRing R] : ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)) = R

theorem ModuleCat.MonoidalCategory.associator_def {R : Type u} [CommRing R] (M N K : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.associator M N K = (TensorProduct.assoc R ↑M ↑N ↑K).toModuleIso

theorem ModuleCat.MonoidalCategory.tensorUnit_isModule {R : Type u} [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)).isModule = Semiring.toModule

theorem ModuleCat.MonoidalCategory.tensorObj_isModule {R : Type u} [CommRing R] (M N : ModuleCat R) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).isModule = TensorProduct.instModule

theorem ModuleCat.MonoidalCategory.whiskerRight_def {R : Type u} [CommRing R] {X₁✝ X₂✝ : ModuleCat R} (f : X₁✝ ⟶ X₂✝) (M : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f M = ofHom (LinearMap.rTensor (↑M) (Hom.hom f))

theorem ModuleCat.MonoidalCategory.tensorUnit_isAddCommGroup {R : Type u} [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)).isAddCommGroup = inst✝.toAddCommGroup

theorem ModuleCat.MonoidalCategory.tensorObj_carrier {R : Type u} [CommRing R] (M N : ModuleCat R) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) = TensorProduct R ↑M ↑N

theorem ModuleCat.MonoidalCategory.whiskerLeft_def {R : Type u} [CommRing R] (M x✝ x✝¹ : ModuleCat R) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = ofHom (LinearMap.lTensor (↑M) (Hom.hom f))

theorem ModuleCat.MonoidalCategory.leftUnitor_def {R : Type u} [CommRing R] (M : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.leftUnitor M = (TensorProduct.lid R ↑M).toModuleIso

theorem ModuleCat.MonoidalCategory.tensorObj_isAddCommGroup {R : Type u} [CommRing R] (M N : ModuleCat R) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).isAddCommGroup = TensorProduct.addCommGroup

theorem ModuleCat.MonoidalCategory.tensorHom_def {R : Type u} [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : ModuleCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (TensorProduct.map (Hom.hom f) (Hom.hom g))

instance ModuleCat.monoidalCategory {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategory (ModuleCat R)

instance ModuleCat.instCommRingCarrierTensorUnit {R : Type u} [CommRing R] : CommRing ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

Remind ourselves that the monoidal unit, being just R, is still a commutative ring.

theorem ModuleCat.hom_tensorHom {R : Type u} [CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = TensorProduct.map (Hom.hom f) (Hom.hom g)

theorem ModuleCat.hom_whiskerLeft {R : Type u} [CommRing R] (L : ModuleCat R) {M N : ModuleCat R} (f : M ⟶ N) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) = LinearMap.lTensor (↑L) (Hom.hom f)

theorem ModuleCat.hom_whiskerRight {R : Type u} [CommRing R] {L M : ModuleCat R} (f : L ⟶ M) (N : ModuleCat R) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) = LinearMap.rTensor (↑N) (Hom.hom f)

theorem ModuleCat.hom_hom_leftUnitor {R : Type u} [CommRing R] {M : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(TensorProduct.lid R ↑M)

theorem ModuleCat.hom_inv_leftUnitor {R : Type u} [CommRing R] {M : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(TensorProduct.lid R ↑M).symm

theorem ModuleCat.hom_hom_rightUnitor {R : Type u} [CommRing R] {M : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = ↑(TensorProduct.rid R ↑M)

theorem ModuleCat.hom_inv_rightUnitor {R : Type u} [CommRing R] {M : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv = ↑(TensorProduct.rid R ↑M).symm

theorem ModuleCat.hom_hom_associator {R : Type u} [CommRing R] {M N K : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom = ↑(TensorProduct.assoc R ↑M ↑N ↑K)

theorem ModuleCat.hom_inv_associator {R : Type u} [CommRing R] {M N K : ModuleCat R} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv = ↑(TensorProduct.assoc R ↑M ↑N ↑K).symm

@[deprecated ModuleCat.MonoidalCategory.tensorObj_carrier (since := "2025-10-29")]

theorem ModuleCat.MonoidalCategory.tensorObj {R : Type u} [CommRing R] (M N : ModuleCat R) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) = TensorProduct R ↑M ↑N

Alias of ModuleCat.MonoidalCategory.tensorObj_carrier.

@[deprecated ModuleCat.MonoidalCategory.tensorObj_carrier (since := "2025-10-29")]

theorem ModuleCat.MonoidalCategory.tensorObj_def {R : Type u} [CommRing R] (M N : ModuleCat R) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) = TensorProduct R ↑M ↑N

Alias of ModuleCat.MonoidalCategory.tensorObj_carrier.

@[simp]

theorem ModuleCat.MonoidalCategory.tensorHom_tmul {R : Type u} [CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N) (k : ↑K) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (k ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom f) k ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m

@[simp]

theorem ModuleCat.MonoidalCategory.whiskerLeft_apply {R : Type u} [CommRing R] (L : ModuleCat R) {M N : ModuleCat R} (f : M ⟶ N) (l : ↑L) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f)) (l ⊗ₜ[R] m) = l ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom f) m

@[simp]

theorem ModuleCat.MonoidalCategory.whiskerRight_apply {R : Type u} [CommRing R] {L M : ModuleCat R} (f : L ⟶ M) (N : ModuleCat R) (l : ↑L) (n : ↑N) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)) (l ⊗ₜ[R] n) = (CategoryTheory.ConcreteCategory.hom f) l ⊗ₜ[R] n

@[simp]

theorem ModuleCat.MonoidalCategory.leftUnitor_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (r : R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m

@[simp]

theorem ModuleCat.MonoidalCategory.leftUnitor_inv_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m

@[simp]

theorem ModuleCat.MonoidalCategory.rightUnitor_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) (r : R) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m

@[simp]

theorem ModuleCat.MonoidalCategory.rightUnitor_inv_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1

@[simp]

theorem ModuleCat.MonoidalCategory.associator_hom_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom) (m ⊗ₜ[R] n ⊗ₜ[R] k) = m ⊗ₜ[R] (n ⊗ₜ[R] k)

@[simp]

theorem ModuleCat.MonoidalCategory.associator_inv_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] k)) = m ⊗ₜ[R] n ⊗ₜ[R] k

def ModuleCat.MonoidalCategory.tensorLift {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃

Construct for morphisms from the tensor product of two objects in ModuleCat.

@[simp]

theorem ModuleCat.MonoidalCategory.tensorLift_tmul {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) (m : ↑M₁) (n : ↑M₂) : (CategoryTheory.ConcreteCategory.hom (tensorLift f h₁ h₂ h₃ h₄)) (m ⊗ₜ[R] n) = f m n

theorem ModuleCat.MonoidalCategory.tensor_ext {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃} (h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)) : f = g

theorem ModuleCat.MonoidalCategory.tensor_ext₃' {R : Type u} [CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂) M₃ ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) : f = g

Extensionality lemma for morphisms from a module of the form (M₁ ⊗ M₂) ⊗ M₃.

theorem ModuleCat.MonoidalCategory.tensor_ext₃ {R : Type u} [CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃) ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))) : f = g

Extensionality lemma for morphisms from a module of the form M₁ ⊗ (M₂ ⊗ M₃).

instance ModuleCat.instMonoidalPreadditive {R : Type u} [CommRing R] : CategoryTheory.MonoidalPreadditive (ModuleCat R)

instance ModuleCat.instMonoidalLinear {R : Type u} [CommRing R] : CategoryTheory.MonoidalLinear R (ModuleCat R)

@[simp]

theorem ModuleCat.ofHom₂_compr₂ {R : Type u} [CommRing R] {M N P Q : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (g : ↑P →ₗ[R] ↑Q) : ofHom₂ (f.compr₂ g) = CategoryTheory.CategoryStruct.comp (ofHom₂ f) (ofHom (CategoryTheory.Linear.rightComp R N (ofHom g)))