Documentation

Mathlib.RingTheory.LinearDisjoint

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 #

Main results #

Equivalent characterization of linear disjointness #

Equivalent characterization by IsDomain or IsField of tensor product #

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

Other main results #

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

Tags #

linearly disjoint, linearly independent, tensor product

source
@[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)
Instances For
    source
    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 ↔ (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B)
    source
    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
    source
    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
    source
    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.

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

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

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

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

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

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

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

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

    source
    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
    Instances For
      source
      @[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
      source
      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.

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

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

      source
      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 (Subalgebra.toSubmodule B) a) = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
      source
      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.

      source
      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 : 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.

      source
      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 ((Subalgebra.toSubmodule A).mulRightMap b) = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)
      source
      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.

      source
      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 : 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.

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

      source
      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 : 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.

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

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

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

      source
      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 : 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.

      source
      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
      source
      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'
      source
      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'
      source
      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'
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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.

      source
      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 : 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.

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

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

      source
      theorem Subalgebra.LinearDisjoint.of_isField' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {A : Type v} [CommRing A] {B : Type w} [CommRing 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.

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

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

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

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

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

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

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

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

      source
      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, ∀ [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.

      source
      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, ∀ [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.

      source
      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 → ∀ [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.

      source
      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 = ⊥
      source
      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 = ⊥
      source
      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 = ⊥
      source
      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 = ⊥