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} {S : Type v} [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

Equations

• A.lTensorBot = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (Subalgebra.toSubmodule A).lTensorOne ⋯ ⋯

@[simp]

theorem Subalgebra.lTensorBot_tmul {R : Type u} {S : Type v} [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} {S : Type v} [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} {S : Type v} [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} {S : Type v} [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

Equations

• A.rTensorBot = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (Subalgebra.toSubmodule A).rTensorOne ⋯ ⋯

@[simp]

theorem Subalgebra.rTensorBot_tmul {R : Type u} {S : Type v} [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} {S : Type v} [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} {S : Type v} [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} {S : Type v} [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} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : (Algebra.TensorProduct.comm R ↥⊥ ↥A).trans A.rTensorBot = A.lTensorBot

def Subalgebra.mulMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Subalgebra R S) (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.

Equations

• A.mulMap B = Algebra.TensorProduct.productMap A.val B.val

@[simp]

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

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

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

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

theorem Subalgebra.mulMap_bot_left_eq {R : Type u} {S : Type v} [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} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Subalgebra R S) : A.mulMap ⊥ = A.val.comp ↑A.rTensorBot

def Subalgebra.mulMap' {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Subalgebra R S) (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).

Equations

• A.mulMap' B = (↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯)).comp (A.mulMap B).rangeRestrict

@[simp]

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

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

theorem Subalgebra.rank_sup_le_of_free {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (A : Subalgebra R S) (B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B] : Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

If A and B are subalgebras of a commutative R-algebra S, both of them are free R-algebras, then the rank of A ⊔ B is less than or equal to the product of that of A and B.

theorem Subalgebra.finrank_sup_le_of_free {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (A : Subalgebra R S) (B : Subalgebra R S) [Module.Free R ↥A] [Module.Free R ↥B] : FiniteDimensional.finrank R ↥(A ⊔ B) ≤ FiniteDimensional.finrank R ↥A * FiniteDimensional.finrank R ↥B

If A and B are subalgebras of a commutative R-algebra S, both of them are free R-algebras, then the FiniteDimensional.finrank of A ⊔ B is less than or equal to the product of that of A and B.