mathlib documentation

algebra.category.Module.monoidal

The symmetric monoidal category structure on R-modules #

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 and then the symmetric_category instance.

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 then construct the monoidal closed structure on Module R.

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

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

Module.monoidal_category.tensor_obj M N ≅ Module.monoidal_category.tensor_obj N M

(implementation) the braiding for R-modules

Equations

M.braiding N = (tensor_product.comm R ↥M ↥N).to_Module_iso

@[simp]

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

(f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f)

@[simp]

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

(α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = ((X.braiding Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (X.braiding Z).hom)

@[simp]

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

(α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv = (𝟙 X ⊗ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ 𝟙 Y)

@[protected, instance]

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

category_theory.symmetric_category (Module R)

The symmetric monoidal structure on Module R.

Equations

Module.symmetric_category = {to_braided_category := {braiding := Module.braiding _inst_1, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}

@[simp]

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

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

@[simp]

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

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

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

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

((category_theory.monoidal_category.tensor_left M).obj N ⟶ P) ≃ (N ⟶ ((category_theory.linear_coyoneda R (Module R)).obj (opposite.op M)).obj P)

Auxiliary definition for the monoidal_closed instance on Module R. (This is only a separate definition in order to speed up typechecking. )

Equations

M.monoidal_closed_hom_equiv N P = {to_fun := λ (f : (category_theory.monoidal_category.tensor_left M).obj N ⟶ P), (tensor_product.mk R ↥N ↥M).compr₂ ((β_ N M).hom ≫ f), inv_fun := λ (f : N ⟶ ((category_theory.linear_coyoneda R (Module R)).obj (opposite.op M)).obj P), (β_ M N).hom ≫ tensor_product.lift f, left_inv := _, right_inv := _}

@[simp]

theorem Module.monoidal_closed_hom_equiv_symm_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : N ⟶ ((category_theory.linear_coyoneda R (Module R)).obj (opposite.op M)).obj P) :

⇑((M.monoidal_closed_hom_equiv N P).symm) f = (β_ M N).hom ≫ tensor_product.lift f

@[simp]

theorem Module.monoidal_closed_hom_equiv_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : (category_theory.monoidal_category.tensor_left M).obj N ⟶ P) :

⇑(M.monoidal_closed_hom_equiv N P) f = (tensor_product.mk R ↥N ↥M).compr₂ ((β_ N M).hom ≫ f)

@[protected, instance]

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

category_theory.monoidal_closed (Module R)

Equations

Module.category_theory.monoidal_closed = {closed' := λ (M : Module R), {is_adj := {right := (category_theory.linear_coyoneda R (Module R)).obj (opposite.op M), adj := category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (N P : Module R), M.monoidal_closed_hom_equiv N P, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}}}}

theorem Module.ihom_map_apply {R : Type u} [comm_ring R] {M N P : Module R} (f : N ⟶ P) (g : ↥(Module.of R (M ⟶ N))) :

⇑((category_theory.ihom M).map f) g = g ≫ f

@[simp]

theorem Module.monoidal_closed_curry {R : Type u} [comm_ring R] {M N P : Module R} (f : M ⊗ N ⟶ P) (x : ↥M) (y : ↥N) :

⇑(⇑(category_theory.monoidal_closed.curry f) y) x = ⇑f (x ⊗ₜ[R] y)

@[simp]

theorem Module.monoidal_closed_uncurry {R : Type u} [comm_ring R] {M N P : Module R} (f : N ⟶ (category_theory.ihom M).obj P) (x : ↥M) (y : ↥N) :

⇑(category_theory.monoidal_closed.uncurry f) (x ⊗ₜ[R] y) = ⇑(⇑f y) x

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

(category_theory.ihom.ev M).app N = ⇑(tensor_product.uncurry R ↥M (↥M →ₗ[R] ↥N) ↥N) linear_map.id.flip

Describes the counit of the adjunction M ⊗ - ⊣ Hom(M, -). Given an R-module N this should give a map M ⊗ Hom(M, N) ⟶ N, so we flip the order of the arguments in the identity map Hom(M, N) ⟶ (M ⟶ N) and uncurry the resulting map M ⟶ Hom(M, N) ⟶ N.

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

(category_theory.ihom.coev M).app N = (tensor_product.mk R ↥(opposite.unop (opposite.op M)) ↥((𝟭 (Module R)).obj N)).flip

Describes the unit of the adjunction M ⊗ - ⊣ Hom(M, -). Given an R-module N this should define a map N ⟶ Hom(M, M ⊗ N), which is given by flipping the arguments in the natural R-bilinear map M ⟶ N ⟶ M ⊗ N.

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

(category_theory.monoidal_closed.pre f).app P = linear_map.lcomp R ↥P f