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 [AddCommGroup M] [Module R M] [Module Sᵐᵒᵖ M] [SMulCommClass R Sᵐᵒᵖ M]
The key fact is:
example : Module (R ⊗[ℕ] Sᵐᵒᵖ) M := TensorProduct.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
Modules. In particular a two-sided Submodule of a bimodule is simply a term of type
Submodule (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] [SMulCommClass R S M] rather than
[Module Sᵐᵒᵖ M] [SMulCommClass 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"