Theorems · Definition · category theory

SemimoduleCat.MonoidalCategory.tensorHom

{R : Type u} →
  [inst : CommSemiring R] →
    {M N : SemimoduleCat R} →
      {M' N' : SemimoduleCat R} →
        (M ⟶ N) →
          (M' ⟶ N') → (SemimoduleCat.MonoidalCategory.tensorObj M M' ⟶ SemimoduleCat.MonoidalCategory.tensorObj N N')

(implementation) tensor product of morphisms R-modules

Defined in

Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Cited by

7 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Quot.sound

Assumes

CommSemiring