Documentation

Mathlib.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:

variable (R S M : Type*) [Ring R] [Ring S]
variable [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 theory of 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 S.

TODO #

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

source
@[simp]
theorem Subbimodule.mk_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : AddSubmonoid 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) = ↑p
source
def Subbimodule.mk {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : AddSubmonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p) (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) :
Submodule (TensorProduct 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 Subbimodule.baseChange.

Equations
  • Subbimodule.mk p hA hB = { toAddSubmonoid := { toAddSubsemigroup := { carrier := ↑p, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }
Instances For
    source
    theorem Subbimodule.smul_mem {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) (b : B) {m : M} (hm : m ∈ p) :
    b • m ∈ p
    source
    @[simp]
    theorem Subbimodule.baseChange_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (S : Type u_5) [CommSemiring S] [Module S M] [Algebra S A] [Algebra S B] [IsScalarTower S A M] [IsScalarTower S B M] (p : Submodule (TensorProduct R A B) M) :
    ↑(Subbimodule.baseChange S p) = ↑p
    source
    def Subbimodule.baseChange {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (S : Type u_5) [CommSemiring S] [Module S M] [Algebra S A] [Algebra S B] [IsScalarTower S A M] [IsScalarTower S B M] (p : Submodule (TensorProduct R A B) M) :
    Submodule (TensorProduct 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
    Instances For
      source
      @[simp]
      theorem Subbimodule.toSubmodule_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) :
      ↑(Subbimodule.toSubmodule p) = ↑p
      source
      def Subbimodule.toSubmodule {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) :
      Submodule A M

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

      Equations
      • Subbimodule.toSubmodule p = { toAddSubmonoid := { toAddSubsemigroup := { carrier := ↑p, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }
      Instances For
        source
        @[simp]
        theorem Subbimodule.toSubmodule'_carrier {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) :
        ↑(Subbimodule.toSubmodule' p) = ↑p
        source
        def Subbimodule.toSubmodule' {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) :
        Submodule B M

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

        Equations
        • Subbimodule.toSubmodule' p = { toAddSubmonoid := { toAddSubsemigroup := { carrier := ↑p, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }
        Instances For
          source
          @[simp]
          theorem Subbimodule.toSubbimoduleInt_carrier (R : Type u_1) (S : Type u_2) (M : Type u_3) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] (p : Submodule (TensorProduct ℕ R S) M) :
          ↑(Subbimodule.toSubbimoduleInt R S M p) = ↑p
          source
          def Subbimodule.toSubbimoduleInt (R : Type u_1) (S : Type u_2) (M : Type u_3) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] (p : Submodule (TensorProduct ℕ R S) M) :
          Submodule (TensorProduct ℤ R S) M

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

          Equations
          Instances For
            source
            @[simp]
            theorem Subbimodule.toSubbimoduleNat_carrier (R : Type u_1) (S : Type u_2) (M : Type u_3) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] (p : Submodule (TensorProduct ℤ R S) M) :
            ↑(Subbimodule.toSubbimoduleNat R S M p) = ↑p
            source
            def Subbimodule.toSubbimoduleNat (R : Type u_1) (S : Type u_2) (M : Type u_3) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] (p : Submodule (TensorProduct ℤ R S) M) :
            Submodule (TensorProduct ℕ R S) M

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

            Equations
            Instances For