mathlib3 documentation

algebra.category.Module.monoidal.basic

The monoidal category structure on R-modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Mostly this uses existing machinery in linear_algebra.tensor_product. We just need to provide a few small missing pieces to build the monoidal_category instance. The symmetric_category instance is in algebra.category.Module.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 Module R in algebra.category.Module.monoidal.closed.

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

def Module.monoidal_category.tensor_obj {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :

(implementation) tensor product of R-modules

Equations

Module.monoidal_category.tensor_obj M N = Module.of R (tensor_product R ↥M ↥N)

def Module.monoidal_category.tensor_hom {R : Type u} [comm_ring R] {M N : Module R} {M' N' : Module R} (f : M ⟶ N) (g : M' ⟶ N') :

Module.monoidal_category.tensor_obj M M' ⟶ Module.monoidal_category.tensor_obj N N'

(implementation) tensor product of morphisms R-modules

Equations

Module.monoidal_category.tensor_hom f g = tensor_product.map f g

theorem Module.monoidal_category.tensor_id {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :

Module.monoidal_category.tensor_hom (𝟙 M) (𝟙 N) = 𝟙 (Module.of R (tensor_product R ↥M ↥N))

theorem Module.monoidal_category.tensor_comp {R : Type u} [comm_ring R] {X₁ Y₁ Z₁ : Module R} {X₂ Y₂ Z₂ : Module R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :

Module.monoidal_category.tensor_hom (f₁ ≫ g₁) (f₂ ≫ g₂) = Module.monoidal_category.tensor_hom f₁ f₂ ≫ Module.monoidal_category.tensor_hom g₁ g₂

def Module.monoidal_category.associator {R : Type u} [comm_ring R] (M : Module R) (N : Module R) (K : Module R) :

Module.monoidal_category.tensor_obj (Module.monoidal_category.tensor_obj M N) K ≅ Module.monoidal_category.tensor_obj M (Module.monoidal_category.tensor_obj N K)

(implementation) the associator for R-modules

Equations

Module.monoidal_category.associator M N K = (tensor_product.assoc R ↥M ↥N ↥K).to_Module_iso

The associator_naturality and pentagon lemmas below are very slow to elaborate.

We give them some help by expressing the lemmas first non-categorically, then using convert _aux using 1 to have the elaborator work as little as possible.

theorem Module.monoidal_category.associator_naturality {R : Type u} [comm_ring R] {X₁ : Module R} {X₂ : Module R} {X₃ : Module R} {Y₁ : Module R} {Y₂ : Module R} {Y₃ : Module R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :

Module.monoidal_category.tensor_hom (Module.monoidal_category.tensor_hom f₁ f₂) f₃ ≫ (Module.monoidal_category.associator Y₁ Y₂ Y₃).hom = (Module.monoidal_category.associator X₁ X₂ X₃).hom ≫ Module.monoidal_category.tensor_hom f₁ (Module.monoidal_category.tensor_hom f₂ f₃)

theorem Module.monoidal_category.pentagon {R : Type u} [comm_ring R] (W : Module R) (X : Module R) (Y : Module R) (Z : Module R) :

def Module.monoidal_category.left_unitor {R : Type u} [comm_ring R] (M : Module R) :

Module.of R (tensor_product R R ↥M) ≅ M

(implementation) the left unitor for R-modules

Equations

Module.monoidal_category.left_unitor M = (tensor_product.lid R ↥M).to_Module_iso ≪≫ M.of_self_iso

theorem Module.monoidal_category.left_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M ⟶ N) :

Module.monoidal_category.tensor_hom (𝟙 (Module.of R R)) f ≫ (Module.monoidal_category.left_unitor N).hom = (Module.monoidal_category.left_unitor M).hom ≫ f

def Module.monoidal_category.right_unitor {R : Type u} [comm_ring R] (M : Module R) :

Module.of R (tensor_product R ↥M R) ≅ M

(implementation) the right unitor for R-modules

Equations

Module.monoidal_category.right_unitor M = (tensor_product.rid R ↥M).to_Module_iso ≪≫ M.of_self_iso

theorem Module.monoidal_category.right_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M ⟶ N) :

Module.monoidal_category.tensor_hom f (𝟙 (Module.of R R)) ≫ (Module.monoidal_category.right_unitor N).hom = (Module.monoidal_category.right_unitor M).hom ≫ f

theorem Module.monoidal_category.triangle {R : Type u} [comm_ring R] (M N : Module R) :

(Module.monoidal_category.associator M (Module.of R R) N).hom ≫ Module.monoidal_category.tensor_hom (𝟙 M) (Module.monoidal_category.left_unitor N).hom = Module.monoidal_category.tensor_hom (Module.monoidal_category.right_unitor M).hom (𝟙 N)

@[protected, instance]

def Module.monoidal_category {R : Type u} [comm_ring R] :

category_theory.monoidal_category (Module R)

Equations

Module.monoidal_category = {tensor_obj := Module.monoidal_category.tensor_obj _inst_1, tensor_hom := Module.monoidal_category.tensor_hom _inst_1, tensor_id' := _, tensor_comp' := _, tensor_unit := Module.of R R semiring.to_module, associator := Module.monoidal_category.associator _inst_1, associator_naturality' := _, left_unitor := Module.monoidal_category.left_unitor _inst_1, left_unitor_naturality' := _, right_unitor := Module.monoidal_category.right_unitor _inst_1, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

@[protected, instance]

def Module.category_theory.monoidal_category.tensor_unit.comm_ring {R : Type u} [comm_ring R] :

comm_ring ↥(𝟙_ (Module R))

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

Equations

Module.category_theory.monoidal_category.tensor_unit.comm_ring = _inst_1

@[simp]

theorem Module.monoidal_category.hom_apply {R : Type u} [comm_ring R] {K L M N : Module R} (f : K ⟶ L) (g : M ⟶ N) (k : ↥K) (m : ↥M) :

⇑(f ⊗ g) (k ⊗ₜ[R] m) = ⇑f k ⊗ₜ[R] ⇑g m

@[simp]

theorem Module.monoidal_category.left_unitor_hom_apply {R : Type u} [comm_ring R] {M : Module R} (r : R) (m : ↥M) :

⇑((λ_ M).hom) (r ⊗ₜ[R] m) = r • m

@[simp]

theorem Module.monoidal_category.left_unitor_inv_apply {R : Type u} [comm_ring R] {M : Module R} (m : ↥M) :

⇑((λ_ M).inv) m = 1 ⊗ₜ[R] m

@[simp]

theorem Module.monoidal_category.right_unitor_hom_apply {R : Type u} [comm_ring R] {M : Module R} (m : ↥M) (r : R) :

⇑((ρ_ M).hom) (m ⊗ₜ[R] r) = r • m

@[simp]

theorem Module.monoidal_category.right_unitor_inv_apply {R : Type u} [comm_ring R] {M : Module R} (m : ↥M) :

⇑((ρ_ M).inv) m = m ⊗ₜ[R] 1

@[simp]

theorem Module.monoidal_category.associator_hom_apply {R : Type u} [comm_ring R] {M N K : Module R} (m : ↥M) (n : ↥N) (k : ↥K) :

⇑((α_ M N K).hom) (m ⊗ₜ[R] n ⊗ₜ[R] k) = m ⊗ₜ[R] (n ⊗ₜ[R] k)

@[simp]

theorem Module.monoidal_category.associator_inv_apply {R : Type u} [comm_ring R] {M N K : Module R} (m : ↥M) (n : ↥N) (k : ↥K) :

⇑((α_ M N K).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] k)) = m ⊗ₜ[R] n ⊗ₜ[R] k

@[protected, instance]

def Module.category_theory.monoidal_preadditive {R : Type u} [comm_ring R] :

category_theory.monoidal_preadditive (Module R)

@[protected, instance]

def Module.category_theory.monoidal_linear {R : Type u} [comm_ring R] :

category_theory.monoidal_linear R (Module R)