(A-A)-Bimodules #
We define (A-A)-bimodules, where A is a commutative semiring, and show basic properties of them.
def
bimodule.lsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁)
(y : tensor_product R H₁ H₂) :
tensor_product R H₁ H₂
Equations
- bimodule.lsmul x y = ⇑(tensor_product.map (linear_map.mul_left R x) 1) y
def
bimodule.rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂)
(y : H₂) :
tensor_product R H₁ H₂
Equations
- bimodule.rsmul x y = ⇑(tensor_product.map 1 (linear_map.mul_right R y)) x
theorem
bimodule.lsmul_rsmul_assoc
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁)
(y : H₂)
(a : tensor_product R H₁ H₂) :
bimodule.rsmul (bimodule.lsmul x a) y = bimodule.lsmul x (bimodule.rsmul a y)
theorem
bimodule.lsmul_zero
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁) :
bimodule.lsmul x 0 = 0
theorem
bimodule.zero_lsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂) :
bimodule.lsmul 0 x = 0
theorem
bimodule.zero_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₂) :
bimodule.rsmul 0 x = 0
theorem
bimodule.rsmul_zero
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂) :
bimodule.rsmul x 0 = 0
theorem
bimodule.lsmul_add
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁)
(a b : tensor_product R H₁ H₂) :
bimodule.lsmul x (a + b) = bimodule.lsmul x a + bimodule.lsmul x b
theorem
bimodule.add_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₂)
(a b : tensor_product R H₁ H₂) :
bimodule.rsmul (a + b) x = bimodule.rsmul a x + bimodule.rsmul b x
theorem
bimodule.lsmul_sum
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁)
{k : Type u_4}
[fintype k]
(a : k → tensor_product R H₁ H₂) :
bimodule.lsmul x (finset.univ.sum (λ (i : k), a i)) = finset.univ.sum (λ (i : k), bimodule.lsmul x (a i))
theorem
bimodule.sum_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₂)
{k : Type u_4}
[fintype k]
(a : k → tensor_product R H₁ H₂) :
bimodule.rsmul (finset.univ.sum (λ (i : k), a i)) x = finset.univ.sum (λ (i : k), bimodule.rsmul (a i) x)
theorem
bimodule.one_lsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂) :
bimodule.lsmul 1 x = x
theorem
bimodule.rsmul_one
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂) :
bimodule.rsmul x 1 = x
theorem
bimodule.lsmul_one
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₁) :
bimodule.lsmul x 1 = x ⊗ₜ[R] 1
theorem
bimodule.one_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : H₂) :
bimodule.rsmul 1 x = 1 ⊗ₜ[R] x
theorem
bimodule.lsmul_smul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(α : R)
(x : H₁)
(a : tensor_product R H₁ H₂) :
bimodule.lsmul x (α • a) = α • bimodule.lsmul x a
theorem
bimodule.smul_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(α : R)
(x : H₂)
(a : tensor_product R H₁ H₂) :
bimodule.rsmul (α • a) x = α • bimodule.rsmul a x
theorem
bimodule.lsmul_lsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x y : H₁)
(a : tensor_product R H₁ H₂) :
bimodule.lsmul x (bimodule.lsmul y a) = bimodule.lsmul (x * y) a
theorem
bimodule.rsmul_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x y : H₂)
(a : tensor_product R H₁ H₂) :
bimodule.rsmul (bimodule.rsmul a x) y = bimodule.rsmul a (x * y)
def
linear_map.is_bimodule_map
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(P : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂) :
Prop
Equations
- P.is_bimodule_map = ∀ (x : H₁) (y : H₂) (a : tensor_product R H₁ H₂), ⇑P (bimodule.rsmul (bimodule.lsmul x a) y) = bimodule.rsmul (bimodule.lsmul x (⇑P a)) y
theorem
linear_map.is_bimodule_map.lsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{P : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂}
(hP : P.is_bimodule_map)
(x : H₁)
(a : tensor_product R H₁ H₂) :
⇑P (bimodule.lsmul x a) = bimodule.lsmul x (⇑P a)
theorem
linear_map.is_bimodule_map.rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{P : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂}
(hP : P.is_bimodule_map)
(x : H₂)
(a : tensor_product R H₁ H₂) :
⇑P (bimodule.rsmul a x) = bimodule.rsmul (⇑P a) x
theorem
linear_map.is_bimodule_map.add
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{P Q : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂}
(hP : P.is_bimodule_map)
(hQ : Q.is_bimodule_map) :
(P + Q).is_bimodule_map
theorem
linear_map.is_bimodule_map_zero
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
theorem
linear_map.is_bimodule_map.smul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{x : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂}
(hx : x.is_bimodule_map)
(k : R) :
(k • x).is_bimodule_map
theorem
linear_map.is_bimodule_map.nsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{x : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂}
(hx : x.is_bimodule_map)
(k : ℕ) :
(k • x).is_bimodule_map
@[instance]
def
is_bimodule_map.add_comm_monoid
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
add_comm_monoid {x // x.is_bimodule_map}
Equations
- is_bimodule_map.add_comm_monoid = {add := λ (x y : {x // x.is_bimodule_map}), ⟨↑x + ↑y, _⟩, add_assoc := _, zero := ⟨0, _⟩, zero_add := _, add_zero := _, nsmul := λ (k : ℕ) (x : {x // x.is_bimodule_map}), ⟨k • ↑x, _⟩, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[instance]
def
is_bimodule_map.has_smul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
has_smul R {x // x.is_bimodule_map}
Equations
- is_bimodule_map.has_smul = {smul := λ (a : R) (x : {x // x.is_bimodule_map}), ⟨a • ↑x, _⟩}
@[protected, instance]
def
subtype.mul_action
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
mul_action R {x // x.is_bimodule_map}
Equations
- subtype.mul_action = {to_has_smul := is_bimodule_map.has_smul _inst_5, one_smul := _, mul_smul := _}
@[protected, instance]
def
subtype.distrib_mul_action
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
distrib_mul_action R {x // x.is_bimodule_map}
Equations
- subtype.distrib_mul_action = {to_mul_action := subtype.mul_action _inst_5, smul_zero := _, smul_add := _}
@[protected, instance]
def
is_bimodule_map.module
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
module R {x // x.is_bimodule_map}
Equations
- is_bimodule_map.module = {to_distrib_mul_action := subtype.distrib_mul_action _inst_5, add_smul := _, zero_smul := _}
def
is_bimodule_map.submodule
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂] :
submodule R (tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂)
Equations
- is_bimodule_map.submodule = {carrier := λ (x : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂), x.is_bimodule_map, add_mem' := _, zero_mem' := _, smul_mem' := _}
theorem
is_bimodule_map_iff
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{T : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂} :
T.is_bimodule_map ↔ ∀ (a : H₁) (b : H₂) (x : H₁) (y : H₂), ⇑T ((a * x) ⊗ₜ[R] (y * b)) = bimodule.rsmul (bimodule.lsmul a (⇑T (x ⊗ₜ[R] y))) b
theorem
is_bimodule_map_iff_ltensor_lsmul_rtensor_rsmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[field R]
[ring H₁]
[ring H₂]
[algebra R H₁]
[algebra R H₂]
{x : H₁ →ₗ[R] H₁}
{y : H₂ →ₗ[R] H₂} :
(tensor_product.map x y).is_bimodule_map ↔ tensor_product.map x y = 0 ∨ x = linear_map.mul_right R (⇑x 1) ∧ y = linear_map.mul_left R (⇑y 1)
def
is_bimodule_map.sum
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{p : Type u_4}
[fintype p]
(x : p → {x // x.is_bimodule_map}) :
{x // x.is_bimodule_map}
Equations
- is_bimodule_map.sum x = ⟨finset.univ.sum (λ (i : p), ↑(x i)), _⟩
theorem
rmul_map_lmul_apply_apply
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
(x : tensor_product R H₁ H₂)
(a : H₁)
(b : H₂) :
⇑(⇑rmul_map_lmul x) (a ⊗ₜ[R] b) = bimodule.rsmul (bimodule.lsmul a x) b
theorem
linear_map.is_bimodule_map_iff'
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[semiring H₁]
[semiring H₂]
[algebra R H₁]
[algebra R H₂]
{f : tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂} :
f.is_bimodule_map ↔ ⇑rmul_map_lmul (⇑f 1) = f