mathlib documentation

algebra.module.bimodule

Bimodules #

One frequently encounters situations in which several sets of scalars act on a single space, subject to compatibility condition(s). A distinguished instance of this is the theory of bimodules: one has two rings R, S acting on an additive group M, with R acting covariantly ("on the left") and S acting contravariantly ("on the right"). The compatibility condition is just: (r • m) • s = r • (m • s) for all r : R, s : S, m : M.

This situation can be set up in Mathlib as:

variables (R S M : Type*) [ring R] [ring S]
variables [add_comm_group M] [module R M] [module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]

The key fact is:

example : module (R ⊗[ℕ] Sᵐᵒᵖ) M := tensor_product.algebra.module

Note that the corresponding result holds for the canonically isomorphic ring R ⊗[ℤ] Sᵐᵒᵖ but it is preferable to use the R ⊗[ℕ] Sᵐᵒᵖ instance since it works without additive inverses.

Bimodules are thus just a special case of modules and most of their properties follow from the theory of modules. In particular a two-sided submodule of a bimodule is simply a term of typesubmodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.

This file is a place to collect results which are specific to bimodules.

Main definitions #

Implementation details #

For many definitions and lemmas it is preferable to set things up without opposites, i.e., as: [module S M] [smul_comm_class R S M] rather than [module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]. The corresponding results for opposites then follow automatically and do not require taking advantage of the fact that (Sᵐᵒᵖ)ᵐᵒᵖ is defeq to S.

TODO #

Develop the theory of two-sided ideals, which have type submodule (R ⊗[ℕ] Rᵐᵒᵖ) R.

source
def subbimodule.mk {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : add_submonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p) (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) :
submodule (tensor_product R A B) M

A constructor for a subbimodule which demands closure under the two sets of scalars individually, rather than jointly via their tensor product.

Note that R plays no role but it is convenient to make this generalisation to support the cases R = ℕ and R = ℤ which both show up naturally. See also base_change.

Equations
source
@[simp]
theorem subbimodule.mk_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : add_submonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p) (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) :
(subbimodule.mk p hA hB).carrier = ↑p
source
theorem subbimodule.smul_mem {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) (a : A) {m : M} (hm : m ∈ p) :
a • m ∈ p
source
theorem subbimodule.smul_mem' {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) (b : B) {m : M} (hm : m ∈ p) :
b • m ∈ p
source
@[simp]
theorem subbimodule.base_change_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (S : Type u_5) [comm_semiring S] [module S M] [algebra S A] [algebra S B] [is_scalar_tower S A M] [is_scalar_tower S B M] (p : submodule (tensor_product R A B) M) :
(subbimodule.base_change S p).carrier = ↑p
source
def subbimodule.base_change {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (S : Type u_5) [comm_semiring S] [module S M] [algebra S A] [algebra S B] [is_scalar_tower S A M] [is_scalar_tower S B M] (p : submodule (tensor_product R A B) M) :
submodule (tensor_product S A B) M

If A and B are also algebras over yet another set of scalars S then we may "base change" from R to S.

Equations
source
@[simp]
theorem subbimodule.to_submodule_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) :
(subbimodule.to_submodule p).carrier = ↑p
source
def subbimodule.to_submodule {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) :
submodule A M

Forgetting the B action, a submodule over A ⊗[R] B is just a submodule over A.

Equations
source
def subbimodule.to_submodule' {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) :
submodule B M

Forgetting the A action, a submodule over A ⊗[R] B is just a submodule over B.

Equations
source
@[simp]
theorem subbimodule.to_submodule'_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (p : submodule (tensor_product R A B) M) :
(subbimodule.to_submodule' p).carrier = ↑p
source
def subbimodule.to_subbimodule_int (R : Type u_1) (S : Type u_2) (M : Type u_3) [ring R] [ring S] [add_comm_group M] [module R M] [module S M] [smul_comm_class R S M] (p : submodule (tensor_product ℕ R S) M) :
submodule (tensor_product ℤ R S) M

A submodule over R ⊗[ℕ] S is naturally also a submodule over the canonically-isomorphic ring R ⊗[ℤ] S.

Equations
source
@[simp]
theorem subbimodule.to_subbimodule_int_carrier (R : Type u_1) (S : Type u_2) (M : Type u_3) [ring R] [ring S] [add_comm_group M] [module R M] [module S M] [smul_comm_class R S M] (p : submodule (tensor_product ℕ R S) M) :
(subbimodule.to_subbimodule_int R S M p).carrier = ↑p
source
@[simp]
theorem subbimodule.to_subbimodule_nat_carrier (R : Type u_1) (S : Type u_2) (M : Type u_3) [ring R] [ring S] [add_comm_group M] [module R M] [module S M] [smul_comm_class R S M] (p : submodule (tensor_product ℤ R S) M) :
(subbimodule.to_subbimodule_nat R S M p).carrier = ↑p
source
def subbimodule.to_subbimodule_nat (R : Type u_1) (S : Type u_2) (M : Type u_3) [ring R] [ring S] [add_comm_group M] [module R M] [module S M] [smul_comm_class R S M] (p : submodule (tensor_product ℤ R S) M) :
submodule (tensor_product ℕ R S) M

A submodule over R ⊗[ℤ] S is naturally also a submodule over the canonically-isomorphic ring R ⊗[ℕ] S.

Equations