Linearly disjoint subalgebras

This file contains basics about linearly disjoint subalgebras. We adapt the definitions in https://en.wikipedia.org/wiki/Linearly_disjoint. See the file Mathlib/LinearAlgebra/LinearDisjoint.lean for details.

Main definitions

• Subalgebra.LinearDisjoint: two subalgebras are linearly disjoint, if they are linearly disjoint as submodules (Submodule.LinearDisjoint).

• Subalgebra.LinearDisjoint.mulMap: if two subalgebras A and B of S / R are linearly disjoint, then there is A ⊗[R] B ≃ₐ[R] A ⊔ B induced by multiplication in S.

Main results

Equivalent characterization of linear disjointness

• Subalgebra.LinearDisjoint.linearIndependent_left_of_flat: if A and B are linearly disjoint, and if B is a flat R-module, then for any family of R-linearly independent elements of A, they are also B-linearly independent.

• Subalgebra.LinearDisjoint.of_basis_left_op: conversely, if a basis of A is also B-linearly independent, then A and B are linearly disjoint.

• Subalgebra.LinearDisjoint.linearIndependent_right_of_flat: if A and B are linearly disjoint, and if A is a flat R-module, then for any family of R-linearly independent elements of B, they are also A-linearly independent.

• Subalgebra.LinearDisjoint.of_basis_right: conversely, if a basis of B is also A-linearly independent, then A and B are linearly disjoint.

• Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat: if A and B are linearly disjoint, and if one of A and B is flat, then for any family of R-linearly independent elements { a_i } of A, and any family of R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is also R-linearly independent.

• Subalgebra.LinearDisjoint.of_basis_mul: conversely, if { a_i } is an R-basis of A, if { b_j } is an R-basis of B, such that the family { a_i * b_j } in S is R-linearly independent, then A and B are linearly disjoint.

Equivalent characterization by IsDomain or IsField of tensor product

The following results are related to the equivalent characterizations in https://mathoverflow.net/questions/8324.

• Subalgebra.LinearDisjoint.isDomain_of_injective, Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective: under some flatness and injectivity conditions, if A and B are R-algebras, then A ⊗[R] B is a domain if and only if there exists an R-algebra which is a field that A and B embed into with linearly disjoint images.

• Subalgebra.LinearDisjoint.of_isField, Subalgebra.LinearDisjoint.of_isField': if A ⊗[R] B is a field, then A and B are linearly disjoint, moreover, for any R-algebra S and injections of A and B into S, their images are linearly disjoint.

• Algebra.TensorProduct.not_isField_of_transcendental, Algebra.TensorProduct.isAlgebraic_of_isField: if A and B are flat R-algebras, both of them are transcendental, then A ⊗[R] B cannot be a field, equivalently, if A ⊗[R] B is a field, then one of them is algebraic.

Other main results

• Subalgebra.LinearDisjoint.symm_of_commute, Subalgebra.linearDisjoint_comm_of_commute: linear disjointness is symmetric under some commutative conditions.

• Subalgebra.LinearDisjoint.map: linear disjointness is preserved by injective algebra homomorphisms.

• Subalgebra.LinearDisjoint.bot_left, Subalgebra.LinearDisjoint.bot_right: the image of R in S is linearly disjoint with any other subalgebras.

• Subalgebra.LinearDisjoint.sup_free_of_free: the compositum of two linearly disjoint subalgebras is a free module, if two subalgebras are also free modules.

• Subalgebra.LinearDisjoint.rank_sup_of_free, Subalgebra.LinearDisjoint.finrank_sup_of_free: if subalgebras A and B are linearly disjoint and they are free modules, then the rank of A ⊔ B is equal to the product of the rank of A and B.

• Subalgebra.LinearDisjoint.of_finrank_sup_of_free: conversely, if A and B are subalgebras which are free modules of finite rank, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.

• Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left: Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right: if A and B are linearly disjoint, if A is free and B is flat (resp. B is free and A is flat), then [B[A] : B] = [A : R] (resp. [A[B] : A] = [B : R]). See also Subalgebra.adjoin_rank_le.

• Subalgebra.LinearDisjoint.of_finrank_coprime_of_free: if the rank of A and B are coprime, and they satisfy some freeness condition, then A and B are linearly disjoint.

• Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, Subalgebra.LinearDisjoint.inf_eq_bot: if A and B are linearly disjoint, under suitable technical conditions, they are disjoint.

The results with name containing "of_commute" also have corresponding specialized versions assuming S is commutative.

Tags

linearly disjoint, linearly independent, tensor product

@[reducible, inline]

abbrev Subalgebra.LinearDisjoint {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (A B : Subalgebra R S) : Prop

If A and B are subalgebras of S / R, then A and B are linearly disjoint, if they are linearly disjoint as submodules of S.

Equations

• A.LinearDisjoint B = (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B)

theorem Subalgebra.linearDisjoint_iff {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (A B : Subalgebra R S) : A.LinearDisjoint B ↔ (toSubmodule A).LinearDisjoint (toSubmodule B)

theorem Subalgebra.LinearDisjoint.of_subsingleton {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {A B : Subalgebra R S} [Subsingleton R] : A.LinearDisjoint B

theorem Subalgebra.LinearDisjoint.of_subsingleton_top {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {A B : Subalgebra R S} [Subsingleton S] : A.LinearDisjoint B

theorem Subalgebra.LinearDisjoint.symm_of_commute {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (hc : ∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) : B.LinearDisjoint A

Linear disjointness is symmetric if elements in the module commute.

theorem Subalgebra.linearDisjoint_comm_of_commute {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {A B : Subalgebra R S} (hc : ∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) : A.LinearDisjoint B ↔ B.LinearDisjoint A

Linear disjointness is symmetric if elements in the module commute.

theorem Subalgebra.LinearDisjoint.map {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ[R] T) (hf : Function.Injective ⇑f) : (Subalgebra.map f A).LinearDisjoint (Subalgebra.map f B)

Linear disjointness is preserved by injective algebra homomorphisms.

theorem Subalgebra.LinearDisjoint.bot_left {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (B : Subalgebra R S) : ⊥.LinearDisjoint B

The image of R in S is linearly disjoint with any other subalgebras.

theorem Subalgebra.LinearDisjoint.bot_right {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (A : Subalgebra R S) : A.LinearDisjoint ⊥

The image of R in S is linearly disjoint with any other subalgebras.

theorem Subalgebra.LinearDisjoint.include_range (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] (B : Type w) [Semiring B] [Algebra R A] [Algebra R B] : Algebra.TensorProduct.includeLeft.range.LinearDisjoint Algebra.TensorProduct.includeRight.range

Images of two R-algebras A and B in A ⊗[R] B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.symm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) : B.LinearDisjoint A

Linear disjointness is symmetric in a commutative ring.

theorem Subalgebra.linearDisjoint_comm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} : A.LinearDisjoint B ↔ B.LinearDisjoint A

Linear disjointness is symmetric in a commutative ring.

theorem Subalgebra.linearDisjoint_iff_injective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} : A.LinearDisjoint B ↔ Function.Injective ⇑(A.mulMap B)

Two subalgebras A, B in a commutative ring are linearly disjoint if and only if Subalgebra.mulMap A B is injective.

def Subalgebra.LinearDisjoint.mulMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) : TensorProduct R ↥A ↥B ≃ₐ[R] ↥(A ⊔ B)

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint, then there is the natural isomorphism A ⊗[R] B ≃ₐ[R] A ⊔ B induced by multiplication in S.

Equations

• H.mulMap = (AlgEquiv.ofInjective (A.mulMap B) ⋯).trans ((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯)

@[simp]

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

noncomputable def Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) : TensorProduct R ↥A ↥B ≃ₐ[↥A] S

If A and B are linearly disjoint subalgebras in a commutative algebra S over R such that A ⊔ B = S, then this is the natural isomorphism A ⊗[R] B ≃ₐ[A] S induced by multiplication in S.

Equations

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

@[simp]

theorem Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) (a : ↥A) (b : ↥B) : (H.mulMapLeftOfSupEqTop H') (a ⊗ₜ[R] b) = ↑a * ↑b

noncomputable def Subalgebra.LinearDisjoint.basisOfBasisRight {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B) : Module.Basis ι (↥A) S

If A and B are linearly disjoint subalgebras in a commutative algebra S over R such that A ⊔ B = S, then any R-basis of B is also an A-basis of S.

Equations

• H.basisOfBasisRight H' b = (Module.Basis.baseChange (↥A) b).map (H.mulMapLeftOfSupEqTop H').toLinearEquiv

@[simp]

theorem Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B) (i : ι) : (H.basisOfBasisRight H' b) i = (algebraMap (↥B) S) (b i)

@[simp]

theorem Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) (x : ↥B) : (H.mulMapLeftOfSupEqTop H').symm ↑x = 1 ⊗ₜ[R] x

theorem Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B) (x : ↥B) (i : ι) : (algebraMap (↥A) S) (((H.basisOfBasisRight H' b).repr ↑x) i) = (algebraMap R S) ((b.repr x) i)

theorem Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R ↥B) (x : ↥B) : (Algebra.leftMulMatrix (H.basisOfBasisRight H' b)) ((algebraMap (↥B) S) x) = (algebraMap R ↥A).mapMatrix ((Algebra.leftMulMatrix b) x)

noncomputable def Subalgebra.LinearDisjoint.basisOfBasisLeft {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) : Module.Basis ι (↥B) S

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint and such that A ⊔ B = S, then any R-basis of A is also a B-basis of S.

Equations

• H.basisOfBasisLeft H' b = (Module.Basis.baseChange (↥B) b).map (⋯.mulMapLeftOfSupEqTop ⋯).toLinearEquiv

@[simp]

theorem Subalgebra.LinearDisjoint.basisOfBasisLeft_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) (i : ι) : (H.basisOfBasisLeft H' b) i = (algebraMap (↥A) S) (b i)

theorem Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) (x : ↥A) (i : ι) : (algebraMap (↥B) S) (((H.basisOfBasisLeft H' b).repr ↑x) i) = (algebraMap R S) ((b.repr x) i)

theorem Subalgebra.LinearDisjoint.sup_free_of_free {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Free R ↥A] [Module.Free R ↥B] : Module.Free R ↥(A ⊔ B)

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint, and if they are free R-modules, then A ⊔ B is also a free R-module.

theorem Subalgebra.LinearDisjoint.isDomain {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [IsDomain S] : IsDomain (TensorProduct R ↥A ↥B)

If A and B are subalgebras in a domain S over R, and if they are linearly disjoint, then A ⊗[R] B is also a domain.

theorem Subalgebra.LinearDisjoint.isDomain_of_injective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] [IsDomain S] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {fa : A →ₐ[R] S} {fb : B →ₐ[R] S} (hfa : Function.Injective ⇑fa) (hfb : Function.Injective ⇑fb) (H : fa.range.LinearDisjoint fb.range) : IsDomain (TensorProduct R A B)

If A and B are R-algebras, such that there exists a domain S over R such that A and B inject into it and their images are linearly disjoint, then A ⊗[R] B is also a domain.

theorem Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (a : ι → ↥A) : LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) a) = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

theorem Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A} (ha : LinearIndependent R a) : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

If A and B are linearly disjoint, if B is a flat R-module, then for any family of R-linearly independent elements of A, they are also B-linearly independent in the opposite ring.

theorem Subalgebra.LinearDisjoint.of_basis_left_op {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (a : Module.Basis ι R ↥A) (H : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ ⇑a)) : A.LinearDisjoint B

If a basis of A is also B-linearly independent in the opposite ring, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (b : ι → ↥B) : LinearMap.ker ((toSubmodule A).mulRightMap b) = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)

theorem Subalgebra.LinearDisjoint.linearIndependent_right_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥A] {ι : Type u_1} {b : ι → ↥B} (hb : LinearIndependent R b) : LinearIndependent (↥A) (⇑B.val ∘ b)

If A and B are linearly disjoint, if A is a flat R-module, then for any family of R-linearly independent elements of B, they are also A-linearly independent.

theorem Subalgebra.LinearDisjoint.of_basis_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (b : Module.Basis ι R ↥B) (H : LinearIndependent (↥A) (⇑B.val ∘ ⇑b)) : A.LinearDisjoint B

If a basis of B is also A-linearly independent, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A} (ha : LinearIndependent R a) (hc : ∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) : LinearIndependent (↥B) (⇑A.val ∘ a)

If A and B are linearly disjoint and their elements commute, if B is a flat R-module, then for any family of R-linearly independent elements of A, they are also B-linearly independent.

theorem Subalgebra.LinearDisjoint.of_basis_left_of_commute {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (a : Module.Basis ι R ↥A) (H : LinearIndependent (↥B) (⇑A.val ∘ ⇑a)) (hc : ∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) : A.LinearDisjoint B

If a basis of A is also B-linearly independent, if elements in A and B commute, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥A] {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B} (ha : LinearIndependent R a) (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)

If A and B are linearly disjoint, if A is flat, then for any family of R-linearly independent elements { a_i } of A, and any family of R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is also R-linearly independent.

theorem Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B} (ha : LinearIndependent R a) (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)

If A and B are linearly disjoint, if B is flat, then for any family of R-linearly independent elements { a_i } of A, and any family of R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is also R-linearly independent.

theorem Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (hf : Module.Flat R ↥A ∨ Module.Flat R ↥B) {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B} (ha : LinearIndependent R a) (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)

If A and B are linearly disjoint, if one of A and B is flat, then for any family of R-linearly independent elements { a_i } of A, and any family of R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is also R-linearly independent.

theorem Subalgebra.LinearDisjoint.of_basis_mul {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {κ : Type u_1} {ι : Type u_2} (a : Module.Basis κ R ↥A) (b : Module.Basis ι R ↥B) (H : LinearIndependent R fun (i : κ × ι) => ↑(a i.1) * ↑(b i.2)) : A.LinearDisjoint B

If { a_i } is an R-basis of A, if { b_j } is an R-basis of B, such that the family { a_i * b_j } in S is R-linearly independent, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.of_le_left_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) {A' : Subalgebra R S} (h : A' ≤ A) [Module.Flat R ↥B] : A'.LinearDisjoint B

theorem Subalgebra.LinearDisjoint.of_le_right_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) {B' : Subalgebra R S} (h : B' ≤ B) [Module.Flat R ↥A] : A.LinearDisjoint B'

theorem Subalgebra.LinearDisjoint.of_le_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) {A' B' : Subalgebra R S} (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R ↥B] [Module.Flat R ↥A'] : A'.LinearDisjoint B'

theorem Subalgebra.LinearDisjoint.of_le_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) {A' B' : Subalgebra R S} (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R ↥A] [Module.Flat R ↥B'] : A'.LinearDisjoint B'

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (hf : Module.Flat R ↥A ∨ Module.Flat R ↥B) (hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥A] (hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] (hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {A : Subalgebra R S} (H : A.LinearDisjoint A) [Module.Flat R ↥A] (hc : ∀ (a b : ↥A), Commute ↑a ↑b) (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥A = 1

theorem Subalgebra.LinearDisjoint.trace_algebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R ↥B] [Module.Finite R ↥B] (x : ↥B) : (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint and such that A ⊔ B = S, then trace and algebraMap commutes.

theorem Subalgebra.LinearDisjoint.norm_algebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R ↥B] [Module.Finite R ↥B] (x : ↥B) : (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)

If A and B are subalgebras in a commutative algebra S over R, and if they are linearly disjoint and such that A ⊔ B = S, then norm and algebraMap commutes.

theorem Subalgebra.LinearDisjoint.linearIndependent_left_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A} (ha : LinearIndependent R a) : LinearIndependent (↥B) (⇑A.val ∘ a)

In a commutative ring, if A and B are linearly disjoint, if B is a flat R-module, then for any family of R-linearly independent elements of A, they are also B-linearly independent.

theorem Subalgebra.LinearDisjoint.of_basis_left {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (a : Module.Basis ι R ↥A) (H : LinearIndependent (↥B) (⇑A.val ∘ ⇑a)) : A.LinearDisjoint B

In a commutative ring, if a basis of A is also B-linearly independent, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective (R : Type u) [CommRing R] (A : Type v) [CommRing A] (B : Type w) [CommRing B] [Algebra R A] [Algebra R B] [Module.Flat R A] [Module.Flat R B] [IsDomain (TensorProduct R A B)] (ha : Function.Injective ⇑(algebraMap R A)) (hb : Function.Injective ⇑(algebraMap R B)) : ∃ (K : Type (max v w)) (x : Field K) (x_1 : Algebra R K) (fa : A →ₐ[R] K) (fb : B →ₐ[R] K), Function.Injective ⇑fa ∧ Function.Injective ⇑fb ∧ fa.range.LinearDisjoint fb.range

If A and B are flat algebras over R, such that A ⊗[R] B is a domain, and such that the algebra maps are injective, then there exists an R-algebra K that is a field that A and B inject into with linearly disjoint images. Note: K can chosen to be the fraction field of A ⊗[R] B, but here we hide this fact.

theorem Subalgebra.LinearDisjoint.of_isField {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : IsField (TensorProduct R ↥A ↥B)) : A.LinearDisjoint B

If A ⊗[R] B is a field, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.of_isField' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A : Type v} [Ring A] {B : Type w} [Ring B] [Algebra R A] [Algebra R B] (H : IsField (TensorProduct R A B)) (fa : A →ₐ[R] S) (fb : B →ₐ[R] S) (hfa : Function.Injective ⇑fa) (hfb : Function.Injective ⇑fb) : fa.range.LinearDisjoint fb.range

If A ⊗[R] B is a field, then for any R-algebra S and injections of A and B into S, their images are linearly disjoint.

theorem Algebra.TensorProduct.not_isField_of_transcendental (R : Type u) [CommRing R] (A : Type v) [CommRing A] (B : Type w) [CommRing B] [Algebra R A] [Algebra R B] [Module.Flat R A] [Module.Flat R B] [Algebra.Transcendental R A] [Algebra.Transcendental R B] : ¬IsField (TensorProduct R A B)

If A and B are flat R-algebras, both of them are transcendental, then A ⊗[R] B cannot be a field.

theorem Algebra.TensorProduct.isAlgebraic_of_isField (R : Type u) [CommRing R] (A : Type v) [CommRing A] (B : Type w) [CommRing B] [Algebra R A] [Algebra R B] [Module.Flat R A] [Module.Flat R B] (H : IsField (TensorProduct R A B)) : Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

If A and B are flat R-algebras, such that A ⊗[R] B is a field, then one of A and B is algebraic over R.

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (hf : Module.Flat R ↥A ∨ Module.Flat R ↥B) (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥A] (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Flat R ↥B] (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥(A ⊓ B) = 1

theorem Subalgebra.LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A : Subalgebra R S} (H : A.LinearDisjoint A) [Module.Flat R ↥A] (hinj : Function.Injective ⇑(algebraMap R S)) : Module.rank R ↥A = 1

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

In a commutative ring, if subalgebras A and B are linearly disjoint and they are free modules, then the rank of A ⊔ B is equal to the product of the rank of A and B.

theorem Subalgebra.LinearDisjoint.finrank_sup_of_free {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Free R ↥A] [Module.Free R ↥B] : Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B

In a commutative ring, if subalgebras A and B are linearly disjoint and they are free modules, then the rank of A ⊔ B is equal to the product of the rank of A and B.

theorem Subalgebra.LinearDisjoint.of_finrank_sup_of_free {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} [Module.Free R ↥A] [Module.Free R ↥B] [Module.Finite R ↥A] [Module.Finite R ↥B] (H : Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B) : A.LinearDisjoint B

In a commutative ring, if A and B are subalgebras which are free modules of finite rank, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Free R ↥A] [Module.Flat R ↥B] [Nontrivial R] [Nontrivial S] : Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A) = Module.rank R ↥A

If A and B are linearly disjoint, if A is free and B is flat, then [B[A] : B] = [A : R]. See also Subalgebra.adjoin_rank_le.

theorem Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) [Module.Free R ↥B] [Module.Flat R ↥A] [Nontrivial R] [Nontrivial S] : Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B) = Module.rank R ↥B

If A and B are linearly disjoint, if B is free and A is flat, then [A[B] : A] = [B : R]. See also Subalgebra.adjoin_rank_le.

theorem Subalgebra.LinearDisjoint.of_finrank_coprime_of_free {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} [Module.Free R ↥A] [Module.Free R ↥B] [Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)] [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)] (H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)) : A.LinearDisjoint B

If the rank of A and B are coprime, and they satisfy some freeness condition, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (A B : Subalgebra R S) [Algebra.IsIntegral R ↥A] (H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B) : A.LinearDisjoint B

If A/R is integral, such that A' and B are linearly disjoint for all subalgebras A' of A which are finitely generated R-modules, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.of_linearDisjoint_finite_right {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (A B : Subalgebra R S) [Algebra.IsIntegral R ↥B] (H : ∀ B' ≤ B, ∀ [Module.Finite R ↥B'], A.LinearDisjoint B') : A.LinearDisjoint B

If B/R is integral, such that A and B' are linearly disjoint for all subalgebras B' of B which are finitely generated R-modules, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.of_linearDisjoint_finite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} [Algebra.IsIntegral R ↥A] [Algebra.IsIntegral R ↥B] (H : ∀ (A' B' : Subalgebra R S), A' ≤ A → B' ≤ B → ∀ [Module.Finite R ↥A'] [Module.Finite R ↥B'], A'.LinearDisjoint B') : A.LinearDisjoint B

If A/R and B/R are integral, such that any finite subalgebras in A and B are linearly disjoint, then A and B are linearly disjoint.

theorem Subalgebra.LinearDisjoint.inf_eq_bot_of_commute {R : Type u} {S : Type v} [Field R] [Ring S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) (hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) : A ⊓ B = ⊥

theorem Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self {R : Type u} {S : Type v} [Field R] [Ring S] [Algebra R S] {A : Subalgebra R S} (H : A.LinearDisjoint A) (hc : ∀ (a b : ↥A), Commute ↑a ↑b) : A = ⊥

theorem Subalgebra.LinearDisjoint.inf_eq_bot {R : Type u} {S : Type v} [Field R] [CommRing S] [Algebra R S] {A B : Subalgebra R S} (H : A.LinearDisjoint B) : A ⊓ B = ⊥

theorem Subalgebra.LinearDisjoint.eq_bot_of_self {R : Type u} {S : Type v} [Field R] [CommRing S] [Algebra R S] {A : Subalgebra R S} (H : A.LinearDisjoint A) : A = ⊥