THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
S acting on an additive group
R acting covariantly ("on the left")
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:
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
. 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
Develop the theory of two-sided ideals, which have type
submodule (R ⊗[ℕ] Rᵐᵒᵖ) R.
A constructor for a subbimodule which demands closure under the two sets of scalars individually, rather than jointly via their tensor product.
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
B are also
algebras over yet another set of scalars
S then we may "base change"