Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 58cef51

Browse files
ocfnashocfnash
committed
feat(algebra/module/bimodule): basic definitions for subbimodules (#14465)
1 parent 26e3eea commit 58cef51

File tree

3 files changed

+250
-0
lines changed

3 files changed

+250
-0
lines changed

‎src/algebra/module/bimodule.lean

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
/-
2+
Copyright (c) 2022 Oliver Nash. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Oliver Nash
5+
-/
6+
import ring_theory.tensor_product
7+
8+
/-!
9+
# Bimodules
10+
11+
One frequently encounters situations in which several sets of scalars act on a single space, subject
12+
to compatibility condition(s). A distinguished instance of this is the theory of bimodules: one has
13+
two rings `R`, `S` acting on an additive group `M`, with `R` acting covariantly ("on the left")
14+
and `S` acting contravariantly ("on the right"). The compatibility condition is just:
15+
`(r • m) • s = r • (m • s)` for all `r : R`, `s : S`, `m : M`.
16+
17+
This situation can be set up in Mathlib as:
18+
```lean
19+
variables (R S M : Type*) [ring R] [ring S]
20+
variables [add_comm_group M] [module R M] [module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]
21+
```
22+
The key fact is:
23+
```lean
24+
example : module (R ⊗[ℕ] Sᵐᵒᵖ) M := tensor_product.algebra.module
25+
```
26+
Note that the corresponding result holds for the canonically isomorphic ring `R ⊗[ℤ] Sᵐᵒᵖ` but it is
27+
preferable to use the `R ⊗[ℕ] Sᵐᵒᵖ` instance since it works without additive inverses.
28+
29+
Bimodules are thus just a special case of `module`s and most of their properties follow from the
30+
theory of `module`s`. In particular a two-sided submodule of a bimodule is simply a term of type
31+
`submodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.
32+
33+
This file is a place to collect results which are specific to bimodules.
34+
35+
## Main definitions
36+
37+
* `subbimodule.mk`
38+
* `subbimodule.smul_mem`
39+
* `subbimodule.smul_mem'`
40+
* `subbimodule.to_submodule`
41+
* `subbimodule.to_submodule'`
42+
43+
## Implementation details
44+
45+
For many definitions and lemmas it is preferable to set things up without opposites, i.e., as:
46+
`[module S M] [smul_comm_class R S M]` rather than `[module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]`.
47+
The corresponding results for opposites then follow automatically and do not require taking
48+
advantage of the fact that `(Sᵐᵒᵖ)ᵐᵒᵖ` is defeq to `S`.
49+
50+
## TODO
51+
52+
Develop the theory of two-sided ideals, which have type `submodule (R ⊗[ℕ] Rᵐᵒᵖ) R`.
53+
54+
-/
55+
56+
open_locale tensor_product
57+
58+
local attribute [instance] tensor_product.algebra.module
59+
60+
namespace subbimodule
61+
62+
section algebra
63+
64+
variables {R A B M : Type*}
65+
variables [comm_semiring R] [add_comm_monoid M] [module R M]
66+
variables [semiring A] [semiring B] [module A M] [module B M]
67+
variables [algebra R A] [algebra R B]
68+
variables [is_scalar_tower R A M] [is_scalar_tower R B M]
69+
variables [smul_comm_class A B M]
70+
71+
/-- A constructor for a subbimodule which demands closure under the two sets of scalars
72+
individually, rather than jointly via their tensor product.
73+
74+
Note that `R` plays no role but it is convenient to make this generalisation to support the cases
75+
`R = ℕ` and `R = ℤ` which both show up naturally. See also `base_change`. -/
76+
@[simps] def mk (p : add_submonoid M)
77+
(hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p)
78+
(hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p) : submodule (A ⊗[R] B) M :=
79+
{ carrier := p,
80+
smul_mem' := λ ab m, tensor_product.induction_on ab
81+
(λ hm, by simpa only [zero_smul] using p.zero_mem)
82+
(λ a b hm, by simpa only [tensor_product.algebra.smul_def] using hA a (hB b hm))
83+
(λ z w hz hw hm, by simpa only [add_smul] using p.add_mem (hz hm) (hw hm)),
84+
.. p }
85+
86+
lemma smul_mem (p : submodule (A ⊗[R] B) M) (a : A) {m : M} (hm : m ∈ p) : a • m ∈ p :=
87+
begin
88+
suffices : a • m = a ⊗ₜ[R] (1 : B) • m, { exact this.symm ▸ p.smul_mem _ hm, },
89+
simp [tensor_product.algebra.smul_def],
90+
end
91+
92+
lemma smul_mem' (p : submodule (A ⊗[R] B) M) (b : B) {m : M} (hm : m ∈ p) : b • m ∈ p :=
93+
begin
94+
suffices : b • m = (1 : A) ⊗ₜ[R] b • m, { exact this.symm ▸ p.smul_mem _ hm, },
95+
simp [tensor_product.algebra.smul_def],
96+
end
97+
98+
/-- If `A` and `B` are also `algebra`s over yet another set of scalars `S` then we may "base change"
99+
from `R` to `S`. -/
100+
@[simps] def base_change (S : Type*) [comm_semiring S] [module S M] [algebra S A] [algebra S B]
101+
[is_scalar_tower S A M] [is_scalar_tower S B M] (p : submodule (A ⊗[R] B) M) :
102+
submodule (A ⊗[S] B) M :=
103+
mk p.to_add_submonoid (smul_mem p) (smul_mem' p)
104+
105+
/-- Forgetting the `B` action, a `submodule` over `A ⊗[R] B` is just a `submodule` over `A`. -/
106+
@[simps] def to_submodule (p : submodule (A ⊗[R] B) M) : submodule A M :=
107+
{ carrier := p,
108+
smul_mem' := smul_mem p,
109+
.. p }
110+
111+
/-- Forgetting the `A` action, a `submodule` over `A ⊗[R] B` is just a `submodule` over `B`. -/
112+
@[simps] def to_submodule' (p : submodule (A ⊗[R] B) M) : submodule B M :=
113+
{ carrier := p,
114+
smul_mem' := smul_mem' p,
115+
.. p }
116+
117+
end algebra
118+
119+
section ring
120+
121+
variables (R S M : Type*) [ring R] [ring S]
122+
variables [add_comm_group M] [module R M] [module S M] [smul_comm_class R S M]
123+
124+
/-- A `submodule` over `R ⊗[ℕ] S` is naturally also a `submodule` over the canonically-isomorphic
125+
ring `R ⊗[ℤ] S`. -/
126+
@[simps] def to_subbimodule_int (p : submodule (R ⊗[ℕ] S) M) : submodule (R ⊗[ℤ] S) M :=
127+
base_change ℤ p
128+
129+
/-- A `submodule` over `R ⊗[ℤ] S` is naturally also a `submodule` over the canonically-isomorphic
130+
ring `R ⊗[ℕ] S`. -/
131+
@[simps] def to_subbimodule_nat (p : submodule (R ⊗[ℤ] S) M) : submodule (R ⊗[ℕ] S) M :=
132+
base_change ℕ p
133+
134+
end ring
135+
136+
end subbimodule

‎src/ring_theory/tensor_product.lean

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -893,3 +893,75 @@ begin
893893
rw [←E1.range_val, ←E2.range_val, ←algebra.tensor_product.product_map_range],
894894
exact (algebra.tensor_product.product_map E1.val E2.val).to_linear_map.finite_dimensional_range,
895895
end
896+
897+
namespace tensor_product.algebra
898+
899+
variables {R A B M : Type*}
900+
variables [comm_semiring R] [add_comm_monoid M] [module R M]
901+
variables [semiring A] [semiring B] [module A M] [module B M]
902+
variables [algebra R A] [algebra R B]
903+
variables [is_scalar_tower R A M] [is_scalar_tower R B M]
904+
905+
/-- An auxiliary definition, used for constructing the `module (A ⊗[R] B) M` in
906+
`tensor_product.algebra.module` below. -/
907+
def module_aux : A ⊗[R] B →ₗ[R] M →ₗ[R] M :=
908+
tensor_product.lift
909+
{ to_fun := λ a, a • (algebra.lsmul R M : B →ₐ[R] module.End R M).to_linear_map,
910+
map_add' := λ r t, by { ext, simp only [add_smul, linear_map.add_apply] },
911+
map_smul' := λ n r, by { ext, simp only [ring_hom.id_apply, linear_map.smul_apply, smul_assoc] } }
912+
913+
lemma module_aux_apply (a : A) (b : B) (m : M) :
914+
module_aux (a ⊗ₜ[R] b) m = a • b • m :=
915+
by simp [module_aux]
916+
917+
variables [smul_comm_class A B M]
918+
919+
/-- If `M` is a representation of two different `R`-algebras `A` and `B` whose actions commute,
920+
then it is a representation the `R`-algebra `A ⊗[R] B`.
921+
922+
An important example arises from a semiring `S`; allowing `S` to act on itself via left and right
923+
multiplication, the roles of `R`, `A`, `B`, `M` are played by `ℕ`, `S`, `Sᵐᵒᵖ`, `S`. This example
924+
is important because a submodule of `S` as a `module` over `S ⊗[ℕ] Sᵐᵒᵖ` is a two-sided ideal.
925+
926+
NB: This is not an instance because in the case `B = A` and `M = A ⊗[R] A` we would have a diamond
927+
of `smul` actions. Furthermore, this would not be a mere definitional diamond but a true
928+
mathematical diamond in which `A ⊗[R] A` had two distinct scalar actions on itself: one from its
929+
multiplication, and one from this would-be instance. Arguably we could live with this but in any
930+
case the real fix is to address the ambiguity in notation, probably along the lines outlined here:
931+
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258
932+
-/
933+
protected def module : module (A ⊗[R] B) M :=
934+
{ smul := λ x m, module_aux x m,
935+
zero_smul := λ m, by simp only [map_zero, linear_map.zero_apply],
936+
smul_zero := λ x, by simp only [map_zero],
937+
smul_add := λ x m₁ m₂, by simp only [map_add],
938+
add_smul := λ x y m, by simp only [map_add, linear_map.add_apply],
939+
one_smul := λ m, by simp only [module_aux_apply, algebra.tensor_product.one_def, one_smul],
940+
mul_smul := λ x y m,
941+
begin
942+
apply tensor_product.induction_on x;
943+
apply tensor_product.induction_on y,
944+
{ simp only [mul_zero, map_zero, linear_map.zero_apply], },
945+
{ intros a b, simp only [zero_mul, map_zero, linear_map.zero_apply], },
946+
{ intros z w hz hw, simp only [zero_mul, map_zero, linear_map.zero_apply], },
947+
{ intros a b, simp only [mul_zero, map_zero, linear_map.zero_apply], },
948+
{ intros a₁ b₁ a₂ b₂,
949+
simp only [module_aux_apply, mul_smul, smul_comm a₁ b₂, algebra.tensor_product.tmul_mul_tmul,
950+
linear_map.mul_apply], },
951+
{ intros z w hz hw a b,
952+
simp only at hz hw,
953+
simp only [mul_add, hz, hw, map_add, linear_map.add_apply], },
954+
{ intros z w hz hw, simp only [mul_zero, map_zero, linear_map.zero_apply], },
955+
{ intros a b z w hz hw,
956+
simp only at hz hw,
957+
simp only [map_add, add_mul, linear_map.add_apply, hz, hw], },
958+
{ intros u v hu hv z w hz hw,
959+
simp only at hz hw,
960+
simp only [add_mul, hz, hw, map_add, linear_map.add_apply], },
961+
end }
962+
963+
local attribute [instance] tensor_product.algebra.module
964+
965+
lemma smul_def (a : A) (b : B) (m : M) : (a ⊗ₜ[R] b) • m = a • b • m := module_aux_apply a b m
966+
967+
end tensor_product.algebra

‎test/instance_diamonds.lean

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ import group_theory.group_action.units
1111
import data.complex.module
1212
import ring_theory.algebraic
1313
import data.zmod.basic
14+
import ring_theory.tensor_product
1415

1516
/-! # Tests that instances do not form diamonds -/
1617

@@ -37,6 +38,47 @@ example (α : Type*) (β : α → Type*) [Π a, add_monoid (β a)] :
3738
example (α : Type*) (β : α → Type*) [Π a, sub_neg_monoid (β a)] :
3839
(pi.has_smul : has_smul ℤ (Π a, β a)) = sub_neg_monoid.has_smul_int := rfl
3940

41+
namespace tensor_product
42+
43+
open_locale tensor_product
44+
open complex
45+
46+
/-! The `example` below times out. TODO Fix it!
47+
48+
/- `tensor_product.algebra.module` forms a diamond with `has_mul.to_has_smul` and
49+
`algebra.tensor_product.tensor_product.semiring`. Given a commutative semiring `A` over a
50+
commutative semiring `R`, we get two mathematically different scalar actions of `A ⊗[R] A` on
51+
itself. -/
52+
def f : ℂ ⊗[ℝ] ℂ →ₗ[ℝ] ℝ :=
53+
tensor_product.lift
54+
{ to_fun := λ z, z.re • re_lm,
55+
map_add' := λ z w, by simp [add_smul],
56+
map_smul' := λ r z, by simp [mul_smul], }
57+
58+
@[simp] lemma f_apply (z w : ℂ) : f (z ⊗ₜ[ℝ] w) = z.re * w.re := by simp [f]
59+
60+
/- `tensor_product.algebra.module` forms a diamond with `has_mul.to_has_smul` and
61+
`algebra.tensor_product.tensor_product.semiring`. Given a commutative semiring `A` over a
62+
commutative semiring `R`, we get two mathematically different scalar actions of `A ⊗[R] A` on
63+
itself. -/
64+
example :
65+
has_mul.to_has_smul (ℂ ⊗[ℝ] ℂ) ≠
66+
(@tensor_product.algebra.module ℝ ℂ ℂ (ℂ ⊗[ℝ] ℂ) _ _ _ _ _ _ _ _ _ _ _ _).to_has_smul :=
67+
begin
68+
have contra : I ⊗ₜ[ℝ] I ≠ (-1) ⊗ₜ[ℝ] 1 := λ c, by simpa using congr_arg f c,
69+
contrapose! contra,
70+
rw has_smul.ext_iff at contra,
71+
replace contra := congr_fun (congr_fun contra (1 ⊗ₜ I)) (I ⊗ₜ 1),
72+
rw @tensor_product.algebra.smul_def ℝ ℂ ℂ (ℂ ⊗[ℝ] ℂ) _ _ _ _ _ _ _ _ _ _ _ _
73+
(1 : ℂ) I (I ⊗ₜ[ℝ] (1 : ℂ)) at contra,
74+
simpa only [algebra.id.smul_eq_mul, algebra.tensor_product.tmul_mul_tmul, one_mul, mul_one,
75+
one_smul, tensor_product.smul_tmul', I_mul_I] using contra,
76+
end
77+
78+
-/
79+
80+
end tensor_product
81+
4082
section units
4183

4284
example (α : Type*) [monoid α] :

0 commit comments

Comments
 (0)