(A-A)-Bimodules #

We define (A-A)-bimodules, where A is a commutative semiring, and show basic properties of them.

noncomputable def Bimodule.lsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) (y : TensorProduct R H₁ H₂) :

TensorProduct R H₁ H₂

Left multiplication on the left tensor factor.

Equations

Bimodule.lsmul x y = (TensorProduct.map (LinearMap.mulLeft R x) 1) y

Instances For

source

noncomputable def Bimodule.rsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) (y : H₂) :

TensorProduct R H₁ H₂

Right multiplication on the right tensor factor.

Equations

Bimodule.rsmul x y = (TensorProduct.map 1 (LinearMap.mulRight R y)) x

Instances For

source

def Bimodule.«term_•ₗ_» :

Lean.TrailingParserDescr

Scoped notation for left multiplication on the left tensor factor.

Equations

Bimodule.«term_•ₗ_» = Lean.ParserDescr.trailingNode `Bimodule.«term_•ₗ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " •ₗ ") (Lean.ParserDescr.cat `term 73))

Instances For

source

def Bimodule.«term_•ᵣ_» :

Lean.TrailingParserDescr

Scoped notation for right multiplication on the right tensor factor.

Equations

Bimodule.«term_•ᵣ_» = Lean.ParserDescr.trailingNode `Bimodule.«term_•ᵣ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " •ᵣ ") (Lean.ParserDescr.cat `term 73))

Instances For

source

theorem Bimodule.lsmul_apply {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x a : H₁) (b : H₂) :

lsmul x (a ⊗ₜ[R] b) = (x * a) ⊗ₜ[R] b

source

theorem Bimodule.rsmul_apply {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (a : H₁) (x b : H₂) :

rsmul (a ⊗ₜ[R] b) x = a ⊗ₜ[R] (b * x)

source

theorem Bimodule.lsmul_rsmul_assoc {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) (y : H₂) (a : TensorProduct R H₁ H₂) :

rsmul (lsmul x a) y = lsmul x (rsmul a y)

source

theorem Bimodule.lsmul_zero {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) :

lsmul x 0 = 0

source

theorem Bimodule.zero_lsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

lsmul 0 x = 0

source

theorem Bimodule.zero_rsmul {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₂) :

rsmul 0 x = 0

source

theorem Bimodule.rsmul_zero {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

rsmul x 0 = 0

source

theorem Bimodule.lsmul_add {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) (a b : TensorProduct R H₁ H₂) :

lsmul x (a + b) = lsmul x a + lsmul x b

source

theorem Bimodule.add_rsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₂) (a b : TensorProduct R H₁ H₂) :

rsmul (a + b) x = rsmul a x + rsmul b x

source

theorem Bimodule.lsmul_sum {R : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) {k : Type u_1} {s : Finset k} (a : k → TensorProduct R H₁ H₂) :

lsmul x (∑ i ∈ s, a i) = ∑ i ∈ s, lsmul x (a i)

source

theorem Bimodule.sum_rsmul {R : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₂) {k : Type u_1} {s : Finset k} (a : k → TensorProduct R H₁ H₂) :

rsmul (∑ i ∈ s, a i) x = ∑ i ∈ s, rsmul (a i) x

source

theorem Bimodule.one_lsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

lsmul 1 x = x

source

theorem Bimodule.rsmul_one {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

rsmul x 1 = x

source

theorem Bimodule.lsmul_one {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) :

lsmul x 1 = x ⊗ₜ[R] 1

source

theorem Bimodule.one_rsmul {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₂) :

rsmul 1 x = 1 ⊗ₜ[R] x

source

theorem Bimodule.lsmul_smul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (α : R) (x : H₁) (a : TensorProduct R H₁ H₂) :

lsmul x (α • a) = α • lsmul x a

source

theorem Bimodule.smul_rsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (α : R) (x : H₂) (a : TensorProduct R H₁ H₂) :

rsmul (α • a) x = α • rsmul a x

source

theorem Bimodule.lsmul_lsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x y : H₁) (a : TensorProduct R H₁ H₂) :

lsmul x (lsmul y a) = lsmul (x * y) a

source

theorem Bimodule.rsmul_rsmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x y : H₂) (a : TensorProduct R H₁ H₂) :

rsmul (rsmul a x) y = rsmul a (x * y)

source

def LinearMap.IsBimoduleMap {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (P : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂) :

Prop

A linear map commuting with the left and right tensor-factor actions.

Equations

P.IsBimoduleMap = ∀ (x : H₁) (y : H₂) (a : TensorProduct R H₁ H₂), P (Bimodule.rsmul (Bimodule.lsmul x a) y) = Bimodule.rsmul (Bimodule.lsmul x (P a)) y

Instances For

source

theorem LinearMap.IsBimoduleMap.lsmul {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {P : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} (hP : P.IsBimoduleMap) (x : H₁) (a : TensorProduct R H₁ H₂) :

P (Bimodule.lsmul x a) = Bimodule.lsmul x (P a)

source

theorem LinearMap.IsBimoduleMap.rsmul {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {P : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} (hP : P.IsBimoduleMap) (x : H₂) (a : TensorProduct R H₁ H₂) :

P (Bimodule.rsmul a x) = Bimodule.rsmul (P a) x

source

theorem LinearMap.IsBimoduleMap.add {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {P Q : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} (hP : P.IsBimoduleMap) (hQ : Q.IsBimoduleMap) :

(P + Q).IsBimoduleMap

source

theorem LinearMap.isBimoduleMap.zero {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] :

IsBimoduleMap 0

source

theorem LinearMap.IsBimoduleMap.smul {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {x : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} (hx : x.IsBimoduleMap) (k : R) :

(k • x).IsBimoduleMap

source

theorem LinearMap.IsBimoduleMap.nsmul {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {x : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} (hx : x.IsBimoduleMap) (k : ℕ) :

(k • x).IsBimoduleMap

source

noncomputable def LinearMap.IsBimoduleMaps (R : Type u_1) (H₁ : Type u_2) (H₂ : Type u_3) [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] :

Submodule R (TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂)

The submodule of bimodule endomorphisms of a tensor product.

Equations

LinearMap.IsBimoduleMaps R H₁ H₂ = { carrier := fun (x : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂) => x.IsBimoduleMap, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.IsBimoduleMaps.coe_add {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x y : ↥(IsBimoduleMaps R H₁ H₂)) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem LinearMap.IsBimoduleMaps.coe_smul {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : ↥(IsBimoduleMaps R H₁ H₂)) (r : R) :

↑(r • x) = r • ↑x

source

@[simp]

theorem LinearMap.IsBimoduleMaps.coe_nsmul {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : ↥(IsBimoduleMaps R H₁ H₂)) (r : ℕ) :

↑(r • x) = r • ↑x

source

@[simp]

theorem LinearMap.IsBimoduleMaps.coe_zero {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] :

↑0 = 0

source

theorem LinearMap.IsBimoduleMap.add_smul {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (a b : R) (x : ↥(IsBimoduleMaps R H₁ H₂)) :

(a + b) • x = a • x + b • x

source

theorem LinearMap.isBimoduleMap_iff {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {T : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} :

T.IsBimoduleMap ↔ ∀ (a : H₁) (b : H₂) (x : H₁) (y : H₂), T ((a * x) ⊗ₜ[R] (y * b)) = Bimodule.rsmul (Bimodule.lsmul a (T (x ⊗ₜ[R] y))) b

source

theorem LinearMap.isBimoduleMap_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₂} :

(TensorProduct.map x y).IsBimoduleMap ↔ TensorProduct.map x y = 0 ∨ x = mulRight R (x 1) ∧ y = mulLeft R (y 1)

source

theorem LinearMap.IsBimoduleMap.sum_coe {R : Type u_4} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {p : Type u_1} {s : Finset p} (x : p → ↥(IsBimoduleMaps R H₁ H₂)) :

↑(∑ i ∈ s, x i) = ∑ i ∈ s, ↑(x i)

source

theorem rmulMapLmul_apply_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) (a : H₁) (b : H₂) :

(rmulMapLmul x) (a ⊗ₜ[R] b) = Bimodule.rsmul (Bimodule.lsmul a x) b

source

theorem LinearMap.isBimoduleMap_iff' {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {f : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} :

f.IsBimoduleMap ↔ rmulMapLmul (f 1) = f

source

@[simp]

theorem rmulMapLmul_apply_one {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

(rmulMapLmul x) 1 = x

source

@[simp]

theorem LinearMap.mem_isBimoduleMaps_iff {R : Type u_1} {H₁ : Type u_3} {H₂ : Type u_2} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] {x : TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂} :

x ∈ IsBimoduleMaps R H₁ H₂ ↔ x.IsBimoduleMap

source

theorem rmulMapLmul_mem_isBimoduleMaps {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

rmulMapLmul x ∈ LinearMap.IsBimoduleMaps R H₁ H₂

source

noncomputable def TensorProduct.toIsBimoduleMap {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] :

TensorProduct R H₁ H₂ ≃ₗ[R] ↥(LinearMap.IsBimoduleMaps R H₁ H₂)

The tensor product is linearly equivalent to its bimodule endomorphism submodule.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TensorProduct.toIsBimoduleMap_apply_coe {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : TensorProduct R H₁ H₂) :

↑(toIsBimoduleMap x) = rmulMapLmul x

source

@[simp]

theorem TensorProduct.toIsBimoduleMap_symm_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (x : ↥(LinearMap.IsBimoduleMaps R H₁ H₂)) :

toIsBimoduleMap.symm x = ↑x 1

Documentation

LeanPool.Monlib4.LinearAlgebra.MyBimodule

(A-A)-Bimodules #