Some results on tensor product of subalgebras

Linear maps induced by multiplication for subalgebras

Let R be a commutative ring, S be a commutative R-algebra. Let A and B be R-subalgebras in S (Subalgebra R S). We define some linear maps induced by the multiplication in S, which are mainly used in the definition of linearly disjointness.

• Subalgebra.mulMap: the natural R-algebra homomorphism A ⊗[R] B →ₐ[R] S induced by the multiplication in S, whose image is A ⊔ B (Subalgebra.mulMap_range).

• Subalgebra.mulMap': the natural R-algebra homomorphism A ⊗[R] B →ₗ[R] A ⊔ B induced by multiplication in S, which is surjective (Subalgebra.mulMap'_surjective).

• Subalgebra.lTensorBot, Subalgebra.rTensorBot: the natural isomorphism of R-algebras between i(R) ⊗[R] A and A, resp. A ⊗[R] i(R) and A, induced by multiplication in S, here i : R → S is the structure map. They generalize Algebra.TensorProduct.lid and Algebra.TensorProduct.rid, as i(R) is not necessarily isomorphic to R.

  They are Subalgebra versions of Submodule.lTensorOne and Submodule.rTensorOne.

def Subalgebra.lTensorBot {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : TensorProduct R ↥⊥ ↥A ≃ₐ[R] ↥A

If A is a subalgebra of S/R, there is the natural R-algebra isomorphism between i(R) ⊗[R] A and A induced by multiplication in S, here i : R → S is the structure map. This generalizes Algebra.TensorProduct.lid as i(R) is not necessarily isomorphic to R.

This is the Subalgebra version of Submodule.lTensorOne

@[simp]

theorem Subalgebra.lTensorBot_tmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (x : R) (a : ↥A) : A.lTensorBot ((algebraMap R ↥⊥) x ⊗ₜ[R] a) = x • a

@[simp]

theorem Subalgebra.lTensorBot_one_tmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (a : ↥A) : A.lTensorBot (1 ⊗ₜ[R] a) = a

@[simp]

theorem Subalgebra.lTensorBot_symm_apply {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (a : ↥A) : A.lTensorBot.symm a = 1 ⊗ₜ[R] a

def Subalgebra.rTensorBot {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : TensorProduct R ↥A ↥⊥ ≃ₐ[R] ↥A

If A is a subalgebra of S/R, there is the natural R-algebra isomorphism between A ⊗[R] i(R) and A induced by multiplication in S, here i : R → S is the structure map. This generalizes Algebra.TensorProduct.rid as i(R) is not necessarily isomorphic to R.

This is the Subalgebra version of Submodule.rTensorOne

@[simp]

theorem Subalgebra.rTensorBot_tmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (x : R) (a : ↥A) : A.rTensorBot (a ⊗ₜ[R] (algebraMap R ↥⊥) x) = x • a

@[simp]

theorem Subalgebra.rTensorBot_tmul_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (a : ↥A) : A.rTensorBot (a ⊗ₜ[R] 1) = a

@[simp]

theorem Subalgebra.rTensorBot_symm_apply {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {A : Subalgebra R S} (a : ↥A) : A.rTensorBot.symm a = a ⊗ₜ[R] 1

@[simp]

theorem Subalgebra.comm_trans_lTensorBot {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : (Algebra.TensorProduct.comm R ↥A ↥⊥).trans A.lTensorBot = A.rTensorBot

@[simp]

theorem Subalgebra.comm_trans_rTensorBot {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : (Algebra.TensorProduct.comm R ↥⊥ ↥A).trans A.rTensorBot = A.lTensorBot

def Algebra.TensorProduct.linearEquivIncludeRange (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : TensorProduct R S T ≃ₗ[R] TensorProduct R ↥includeLeft.range ↥includeRight.range

Given R-algebras S,T, there is a natural R-linear isomorphism from S ⊗[R] T to S' ⊗[R] T' where S',T' are the images of S,T in S ⊗[R] T respectively. This is promoted to an R-algebra isomorphism Algebra.TensorProduct.algEquivIncludeRange.

theorem Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : ↑(linearEquivIncludeRange R S T) = _root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict

theorem Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : ↑(linearEquivIncludeRange R S T).symm = (LinearMap.range includeLeft).mulMap (LinearMap.range includeRight)

@[simp]

theorem Algebra.TensorProduct.linearEquivIncludeRange_tmul (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] (x : S) (y : T) : (linearEquivIncludeRange R S T) (x ⊗ₜ[R] y) = includeLeft.rangeRestrict x ⊗ₜ[R] includeRight.rangeRestrict y

@[simp]

theorem Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] (x : ↥includeLeft.range) (y : ↥includeRight.range) : (linearEquivIncludeRange R S T).symm (x ⊗ₜ[R] y) = ↑x * ↑y

def Algebra.TensorProduct.algEquivIncludeRange (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : TensorProduct R S T ≃ₐ[R] TensorProduct R ↥includeLeft.range ↥includeRight.range

Given R-algebras S,T, there is a natural R-algebra isomorphism from S ⊗[R] T to S' ⊗[R] T' where S',T' are the images of S,T in S ⊗[R] T respectively.

theorem Algebra.TensorProduct.algEquivIncludeRange_toAlgHom (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : ↑(algEquivIncludeRange R S T) = map includeLeft.rangeRestrict includeRight.rangeRestrict

@[simp]

theorem Algebra.TensorProduct.algEquivIncludeRange_tmul (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] (x : S) (y : T) : (algEquivIncludeRange R S T) (x ⊗ₜ[R] y) = includeLeft.rangeRestrict x ⊗ₜ[R] includeRight.rangeRestrict y

@[simp]

theorem Algebra.TensorProduct.algEquivIncludeRange_symm_tmul (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] (x : ↥includeLeft.range) (y : ↥includeRight.range) : (algEquivIncludeRange R S T).symm (x ⊗ₜ[R] y) = ↑x * ↑y

def Subalgebra.mulMap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : TensorProduct R ↥A ↥B →ₐ[R] S

If A and B are subalgebras in a commutative algebra S over R, there is the natural R-algebra homomorphism A ⊗[R] B →ₐ[R] S induced by multiplication in S.

theorem Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] : ↑(algEquivIncludeRange R S T).symm = includeLeft.range.mulMap includeRight.range

@[simp]

theorem Subalgebra.mulMap_tmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) (a : ↥A) (b : ↥B) : (A.mulMap B) (a ⊗ₜ[R] b) = ↑a * ↑b

theorem Subalgebra.mulMap_map_comp_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] (A B : Subalgebra R S) (f : S →ₐ[R] T) : ((map f A).mulMap (map f B)).comp (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) = f.comp (A.mulMap B)

theorem Subalgebra.mulMap_toLinearMap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : (A.mulMap B).toLinearMap = (toSubmodule A).mulMap (toSubmodule B)

theorem Subalgebra.mulMap_comm {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)

theorem Subalgebra.mulMap_range {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : (A.mulMap B).range = A ⊔ B

theorem Subalgebra.mulMap_bot_left_eq {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Subalgebra R S) : ⊥.mulMap A = A.val.comp ↑A.lTensorBot

theorem Subalgebra.mulMap_bot_right_eq {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Subalgebra R S) : A.mulMap ⊥ = A.val.comp ↑A.rTensorBot

def Subalgebra.mulMap' {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : TensorProduct R ↥A ↥B →ₐ[R] ↥(A ⊔ B)

If A and B are subalgebras in a commutative algebra S over R, there is the natural R-algebra homomorphism A ⊗[R] B →ₐ[R] A ⊔ B induced by multiplication in S, which is surjective (Subalgebra.mulMap'_surjective).

@[simp]

theorem Subalgebra.val_mulMap'_tmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (a : ↥A) (b : ↥B) : ↑((A.mulMap' B) (a ⊗ₜ[R] b)) = ↑a * ↑b

theorem Subalgebra.mulMap'_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (A B : Subalgebra R S) : Function.Surjective ⇑(A.mulMap' B)