Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

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.

noncomputable def ModuleCat.MonoidalCategory.tensorObj {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) :

(implementation) tensor product of R-modules

Equations
Instances For

    (implementation) tensor product of morphisms R-modules

    Equations
    Instances For

      (implementation) left whiskering for R-modules

      Equations
      Instances For

        (implementation) right whiskering for R-modules

        Equations
        Instances For
          theorem ModuleCat.MonoidalCategory.tensor_comp {R : Type u} [CommRing R] {X₁ Y₁ Z₁ : ModuleCat R} {X₂ Y₂ Z₂ : ModuleCat R} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
          noncomputable def ModuleCat.MonoidalCategory.leftUnitor {R : Type u} [CommRing R] (M : ModuleCat R) :

          (implementation) the left unitor for R-modules

          Equations
          Instances For
            noncomputable def ModuleCat.MonoidalCategory.rightUnitor {R : Type u} [CommRing R] (M : ModuleCat R) :
            ModuleCat.of R (TensorProduct R (↑M) R) M

            (implementation) the right unitor for R-modules

            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              theorem ModuleCat.MonoidalCategory.instMonoidalCategoryStruct_tensorHom_hom {R : Type u} [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : ModuleCat R} (f : X₁✝ Y₁✝) (g : X₂✝ Y₂✝) :
              theorem ModuleCat.MonoidalCategory.instMonoidalCategoryStruct_tensorUnit_isAddCommGroup {R : Type u} [CommRing R] :
              (𝟙_ (ModuleCat R)).isAddCommGroup = Ring.toAddCommGroup
              Equations
              noncomputable instance ModuleCat.instCommRingCarrierTensorUnit {R : Type u} [CommRing R] :
              CommRing (𝟙_ (ModuleCat R))

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

              Equations
              @[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) :
              @[deprecated ModuleCat.MonoidalCategory.tensorHom_tmul]
              theorem ModuleCat.MonoidalCategory.hom_apply {R : Type u} [CommRing R] {K L M N : ModuleCat R} (f : K L) (g : M N) (k : K) (m : M) :

              Alias of ModuleCat.MonoidalCategory.tensorHom_tmul.

              @[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) :
              @[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) :
              @[simp]
              @[simp]
              theorem ModuleCat.MonoidalCategory.associator_hom_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : M) (n : N) (k : K) :
              @[simp]
              theorem ModuleCat.MonoidalCategory.associator_inv_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : M) (n : N) (k : K) :
              noncomputable 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) :

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

              Equations
              Instances For
                @[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₂) :
                (ModuleCat.MonoidalCategory.tensorLift f h₁ h₂ h₃ h₄).hom (m ⊗ₜ[R] n) = f m n
                theorem ModuleCat.MonoidalCategory.tensor_ext {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} {f g : CategoryTheory.MonoidalCategory.tensorObj M₁ M₂ M₃} (h : ∀ (m : M₁) (n : M₂), f.hom (m ⊗ₜ[R] n) = g.hom (m ⊗ₜ[R] n)) :
                f = g
                theorem ModuleCat.MonoidalCategory.tensor_ext₃' {R : Type u} [CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R} {f g : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj M₁ M₂) M₃ M₄} (h : ∀ (m₁ : M₁) (m₂ : M₂) (m₃ : M₃), f.hom ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₃) = g.hom ((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.MonoidalCategory.tensorObj M₁ (CategoryTheory.MonoidalCategory.tensorObj M₂ M₃) M₄} (h : ∀ (m₁ : M₁) (m₂ : M₂) (m₃ : M₃), f.hom (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = g.hom (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) :
                f = g

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