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 linearly 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.

Other main results

• Subalgebra.LinearDisjoint.symm_of_commute, Subalgebra.linearDisjoint_symm_of_commute: linearly disjoint is symmetric under some commutative conditions.

• 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 : Subalgebra R S) (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 : Subalgebra R S) (B : Subalgebra R S) : A.LinearDisjoint B ↔ (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B)

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

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

Linearly disjoint is symmetric if elements in the module commute.

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

Linearly disjoint is symmetric if elements in the module commute.

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

Linearly disjoint is symmetric in a commutative ring.

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

Linearly disjoint is symmetric in a commutative ring.

def Subalgebra.LinearDisjoint.mulMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A : Subalgebra R S} {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 : Subalgebra R S} {B : Subalgebra R S} (H : A.LinearDisjoint B) (a : ↥A) (b : ↥B) : ↑(H.mulMap (a ⊗ₜ[R] b)) = ↑a * ↑b

theorem Subalgebra.LinearDisjoint.sup_free_of_free {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {A : Subalgebra R S} {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.mulLeftMap_ker_eq_bot_iff_linearIndependent_op {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (a : ι → ↥A) : LinearMap.ker (Submodule.mulLeftMap (Subalgebra.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 : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (a : 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 : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (b : ι → ↥B) : LinearMap.ker ((Subalgebra.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 : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (b : 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 : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (a : 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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) {κ : Type u_1} {ι : Type u_2} (a : Basis κ R ↥A) (b : 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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {B : Subalgebra R S} (H : A.LinearDisjoint B) {A' : Subalgebra R S} {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 : Subalgebra R S} {B : Subalgebra R S} (H : A.LinearDisjoint B) {A' : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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.linearIndependent_left_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) {ι : Type u_1} (a : 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.rank_inf_eq_one_of_flat_of_inj {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S} {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 : Subalgebra R S) (B : Subalgebra R S) [Algebra.IsIntegral R ↥A] (H : ∀ A' ≤ A, ∀ [inst : 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 : Subalgebra R S) (B : Subalgebra R S) [Algebra.IsIntegral R ↥B] (H : ∀ B' ≤ B, ∀ [inst : 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 : Subalgebra R S} {B : Subalgebra R S} [Algebra.IsIntegral R ↥A] [Algebra.IsIntegral R ↥B] (H : ∀ (A' B' : Subalgebra R S), A' ≤ A → B' ≤ B → ∀ [inst : Module.Finite R ↥A'] [inst : 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 : Subalgebra R S} {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 : Subalgebra R S} {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 = ⊥