Documentation

Mathlib.FieldTheory.Relrank

Relative rank of subfields and intermediate fields #

This file contains basics about the relative rank of subfields and intermediate fields.

Main definitions #

source
noncomputable def Subfield.relrank {E : Type v} [Field E] (A B : Subfield E) :
Cardinal.{v}

Subfield.relrank A B is defined to be [B : A ⊓ B] as a Cardinal, in particular, when A ≤ B it is [B : A], the degree of the field extension B / A. This is similar to Subgroup.relindex but it is Cardinal valued.

Equations
source
noncomputable def Subfield.relfinrank {E : Type v} [Field E] (A B : Subfield E) :
ℕ

The Nat version of Subfield.relrank. If B / A ⊓ B is an infinite extension, then it is zero.

Equations
source
theorem Subfield.relfinrank_eq_toNat_relrank {E : Type v} [Field E] (A B : Subfield E) :
A.relfinrank B = Cardinal.toNat (A.relrank B)
source
theorem Subfield.relrank_eq_of_inf_eq {E : Type v} [Field E] {A B C : Subfield E} (h : A ⊓ C = B ⊓ C) :
A.relrank C = B.relrank C
source
theorem Subfield.relfinrank_eq_of_inf_eq {E : Type v} [Field E] {A B C : Subfield E} (h : A ⊓ C = B ⊓ C) :
A.relfinrank C = B.relfinrank C
source
theorem Subfield.relrank_eq_rank_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relrank B = Module.rank ↥A ↥(extendScalars h)

If A ≤ B, then Subfield.relrank A B is [B : A].

source
theorem Subfield.relfinrank_eq_finrank_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relfinrank B = Module.finrank ↥A ↥(extendScalars h)

If A ≤ B, then Subfield.relfinrank A B is [B : A].

source
theorem Subfield.inf_relrank_right {E : Type v} [Field E] (A B : Subfield E) :
(A ⊓ B).relrank B = A.relrank B
source
theorem Subfield.inf_relfinrank_right {E : Type v} [Field E] (A B : Subfield E) :
(A ⊓ B).relfinrank B = A.relfinrank B
source
theorem Subfield.inf_relrank_left {E : Type v} [Field E] (A B : Subfield E) :
(A ⊓ B).relrank A = B.relrank A
source
theorem Subfield.inf_relfinrank_left {E : Type v} [Field E] (A B : Subfield E) :
(A ⊓ B).relfinrank A = B.relfinrank A
source
@[simp]
theorem Subfield.relrank_self {E : Type v} [Field E] (A : Subfield E) :
A.relrank A = 1
source
@[simp]
theorem Subfield.relfinrank_self {E : Type v} [Field E] (A : Subfield E) :
A.relfinrank A = 1
source
theorem Subfield.relrank_eq_one_of_le {E : Type v} [Field E] {A B : Subfield E} (h : B ≤ A) :
A.relrank B = 1
source
theorem Subfield.relfinrank_eq_one_of_le {E : Type v} [Field E] {A B : Subfield E} (h : B ≤ A) :
A.relfinrank B = 1
source
theorem Subfield.relrank_mul_rank_top {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
source
theorem Subfield.relfinrank_mul_finrank_top {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
source
@[simp]
theorem Subfield.relrank_top_left {E : Type v} [Field E] (A : Subfield E) :
⊤.relrank A = 1
source
@[simp]
theorem Subfield.relfinrank_top_left {E : Type v} [Field E] (A : Subfield E) :
⊤.relfinrank A = 1
source
@[simp]
theorem Subfield.relrank_top_right {E : Type v} [Field E] (A : Subfield E) :
A.relrank ⊤ = Module.rank (↥A) E
source
@[simp]
theorem Subfield.relfinrank_top_right {E : Type v} [Field E] (A : Subfield E) :
A.relfinrank ⊤ = Module.finrank (↥A) E
source
theorem Subfield.lift_relrank_map_map {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) :
Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem Subfield.relrank_map_map {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : E →+* L) :
(map f A).relrank (map f B) = A.relrank B
source
theorem Subfield.lift_relrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) :
Cardinal.lift.{v, w} ((comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (map f B))
source
theorem Subfield.relrank_comap {E : Type v} [Field E] (A : Subfield E) {L : Type v} [Field L] (f : L →+* E) (B : Subfield L) :
(comap f A).relrank B = A.relrank (map f B)
source
theorem Subfield.relfinrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) :
(comap f A).relfinrank B = A.relfinrank (map f B)
source
theorem Subfield.lift_rank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) :
Cardinal.lift.{v, w} (Module.rank (↥(comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
source
theorem Subfield.rank_comap {E : Type v} [Field E] (A : Subfield E) {L : Type v} [Field L] (f : L →+* E) :
Module.rank (↥(comap f A)) L = A.relrank f.fieldRange
source
theorem Subfield.finrank_comap {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) :
Module.finrank (↥(comap f A)) L = A.relfinrank f.fieldRange
source
theorem Subfield.relfinrank_map_map {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) :
(map f A).relfinrank (map f B) = A.relfinrank B
source
theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
source
theorem Subfield.relrank_comap_comap_eq_relrank_inf {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) :
(comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)
source
theorem Subfield.relfinrank_comap_comap_eq_relfinrank_inf {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) :
(comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)
source
theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : B ≤ f.fieldRange) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem Subfield.relrank_comap_comap_eq_relrank_of_le {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) (h : B ≤ f.fieldRange) :
(comap f A).relrank (comap f B) = A.relrank B
source
theorem Subfield.relfinrank_comap_comap_eq_relfinrank_of_le {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : B ≤ f.fieldRange) :
(comap f A).relfinrank (comap f B) = A.relfinrank B
source
theorem Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_surjective {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : Function.Surjective ⇑f) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem Subfield.relrank_comap_comap_eq_relrank_of_surjective {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : L →+* E) (h : Function.Surjective ⇑f) :
(comap f A).relrank (comap f B) = A.relrank B
source
theorem Subfield.relfinrank_comap_comap_eq_relfinrank_of_surjective {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : L →+* E) (h : Function.Surjective ⇑f) :
(comap f A).relfinrank (comap f B) = A.relfinrank B
source
theorem Subfield.relrank_dvd_rank_top_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relrank B ∣ Module.rank (↥A) E
source
theorem Subfield.relfinrank_dvd_finrank_top_of_le {E : Type v} [Field E] {A B : Subfield E} (h : A ≤ B) :
A.relfinrank B ∣ Module.finrank (↥A) E
source
theorem Subfield.relrank_mul_relrank {E : Type v} [Field E] {A B C : Subfield E} (h1 : A ≤ B) (h2 : B ≤ C) :
A.relrank B * B.relrank C = A.relrank C
source
theorem Subfield.relfinrank_mul_relfinrank {E : Type v} [Field E] {A B C : Subfield E} (h1 : A ≤ B) (h2 : B ≤ C) :
A.relfinrank B * B.relfinrank C = A.relfinrank C
source
theorem Subfield.relrank_inf_mul_relrank {E : Type v} [Field E] (A B C : Subfield E) :
A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
source
theorem Subfield.relfinrank_inf_mul_relfinrank {E : Type v} [Field E] (A B C : Subfield E) :
A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
source
theorem Subfield.relrank_mul_relrank_eq_inf_relrank {E : Type v} [Field E] (A : Subfield E) {B C : Subfield E} (h : B ≤ C) :
A.relrank B * B.relrank C = (A ⊓ B).relrank C
source
theorem Subfield.relfinrank_mul_relfinrank_eq_inf_relfinrank {E : Type v} [Field E] (A : Subfield E) {B C : Subfield E} (h : B ≤ C) :
A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
source
theorem Subfield.relrank_inf_mul_relrank_of_le {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
A.relrank (B ⊓ C) * B.relrank C = A.relrank C
source
theorem Subfield.relfinrank_inf_mul_relfinrank_of_le {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
source
theorem Subfield.relrank_dvd_of_le_left {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
B.relrank C ∣ A.relrank C
source
theorem Subfield.relfinrank_dvd_of_le_left {E : Type v} [Field E] {A B : Subfield E} (C : Subfield E) (h : A ≤ B) :
B.relfinrank C ∣ A.relfinrank C
source
noncomputable def IntermediateField.relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
Cardinal.{v}

IntermediateField.relrank A B is defined to be [B : A ⊓ B] as a Cardinal, in particular, when A ≤ B it is [B : A], the degree of the field extension B / A. This is similar to Subgroup.relindex but it is Cardinal valued.

Equations
source
noncomputable def IntermediateField.relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
ℕ

The Nat version of IntermediateField.relrank. If B / A ⊓ B is an infinite extension, then it is zero.

Equations
source
theorem IntermediateField.relfinrank_eq_toNat_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
A.relfinrank B = Cardinal.toNat (A.relrank B)
source
theorem IntermediateField.relrank_eq_of_inf_eq {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h : A ⊓ C = B ⊓ C) :
A.relrank C = B.relrank C
source
theorem IntermediateField.relfinrank_eq_of_inf_eq {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h : A ⊓ C = B ⊓ C) :
A.relfinrank C = B.relfinrank C
source
theorem IntermediateField.relrank_eq_rank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relrank B = Module.rank ↥A ↥(extendScalars h)

If A ≤ B, then IntermediateField.relrank A B is [B : A]

source
theorem IntermediateField.relfinrank_eq_finrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relfinrank B = Module.finrank ↥A ↥(extendScalars h)

If A ≤ B, then IntermediateField.relrank A B is [B : A]

source
theorem IntermediateField.inf_relrank_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
(A ⊓ B).relrank B = A.relrank B
source
theorem IntermediateField.inf_relfinrank_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
(A ⊓ B).relfinrank B = A.relfinrank B
source
theorem IntermediateField.inf_relrank_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
(A ⊓ B).relrank A = B.relrank A
source
theorem IntermediateField.inf_relfinrank_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
(A ⊓ B).relfinrank A = B.relfinrank A
source
@[simp]
theorem IntermediateField.relrank_self {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relrank A = 1
source
@[simp]
theorem IntermediateField.relfinrank_self {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relfinrank A = 1
source
theorem IntermediateField.relrank_eq_one_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : B ≤ A) :
A.relrank B = 1
source
theorem IntermediateField.relfinrank_eq_one_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : B ≤ A) :
A.relfinrank B = 1
source
theorem IntermediateField.lift_rank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) :
Cardinal.lift.{v, w} (Module.rank (↥(comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
source
theorem IntermediateField.rank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
Module.rank (↥(comap f A)) L = A.relrank f.fieldRange
source
theorem IntermediateField.finrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) :
Module.finrank (↥(comap f A)) L = A.relfinrank f.fieldRange
source
theorem IntermediateField.lift_relrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L) :
Cardinal.lift.{v, w} ((comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (map f B))
source
theorem IntermediateField.relrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (B : IntermediateField F L) :
(comap f A).relrank B = A.relrank (map f B)
source
theorem IntermediateField.relfinrank_comap {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L) :
(comap f A).relfinrank B = A.relfinrank (map f B)
source
theorem IntermediateField.lift_relrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L) :
Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem IntermediateField.relrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : E →ₐ[F] L) :
(map f A).relrank (map f B) = A.relrank B
source
theorem IntermediateField.relfinrank_map_map {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L) :
(map f A).relfinrank (map f B) = A.relfinrank B
source
theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
source
theorem IntermediateField.relrank_comap_comap_eq_relrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
(comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)
source
theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) :
(comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)
source
theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem IntermediateField.relrank_comap_comap_eq_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
(comap f A).relrank (comap f B) = A.relrank B
source
theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
(comap f A).relfinrank (comap f B) = A.relfinrank B
source
theorem IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
source
theorem IntermediateField.relrank_comap_comap_eq_relrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
(comap f A).relrank (comap f B) = A.relrank B
source
theorem IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_surjective {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {L : Type w} [Field L] [Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E) (h : Function.Surjective ⇑f) :
(comap f A).relfinrank (comap f B) = A.relfinrank B
source
theorem IntermediateField.relrank_mul_rank_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
source
theorem IntermediateField.relfinrank_mul_finrank_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
source
theorem IntermediateField.rank_bot_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
Module.rank F ↥A * A.relrank B = Module.rank F ↥B
source
theorem IntermediateField.finrank_bot_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
Module.finrank F ↥A * A.relfinrank B = Module.finrank F ↥B
source
theorem IntermediateField.relrank_dvd_rank_top_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relrank B ∣ Module.rank (↥A) E
source
theorem IntermediateField.relfinrank_dvd_finrank_top_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (h : A ≤ B) :
A.relfinrank B ∣ Module.finrank (↥A) E
source
theorem IntermediateField.relrank_dvd_rank_bot {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
A.relrank B ∣ Module.rank F ↥B
source
theorem IntermediateField.relfinrank_dvd_finrank_bot {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
A.relfinrank B ∣ Module.finrank F ↥B
source
theorem IntermediateField.relrank_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h1 : A ≤ B) (h2 : B ≤ C) :
A.relrank B * B.relrank C = A.relrank C
source
theorem IntermediateField.relfinrank_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B C : IntermediateField F E} (h1 : A ≤ B) (h2 : B ≤ C) :
A.relfinrank B * B.relfinrank C = A.relfinrank C
source
theorem IntermediateField.relrank_inf_mul_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B C : IntermediateField F E) :
A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
source
theorem IntermediateField.relfinrank_inf_mul_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B C : IntermediateField F E) :
A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
source
theorem IntermediateField.relrank_mul_relrank_eq_inf_relrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {B C : IntermediateField F E} (h : B ≤ C) :
A.relrank B * B.relrank C = (A ⊓ B).relrank C
source
theorem IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) {B C : IntermediateField F E} (h : B ≤ C) :
A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C
source
theorem IntermediateField.relrank_inf_mul_relrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
A.relrank (B ⊓ C) * B.relrank C = A.relrank C
source
theorem IntermediateField.relfinrank_inf_mul_relfinrank_of_le {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C
source
@[simp]
theorem IntermediateField.relrank_top_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
⊤.relrank A = 1
source
@[simp]
theorem IntermediateField.relfinrank_top_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
⊤.relfinrank A = 1
source
@[simp]
theorem IntermediateField.relrank_top_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relrank ⊤ = Module.rank (↥A) E
source
@[simp]
theorem IntermediateField.relfinrank_top_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relfinrank ⊤ = Module.finrank (↥A) E
source
@[simp]
theorem IntermediateField.relrank_bot_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
⊥.relrank A = Module.rank F ↥A
source
@[simp]
theorem IntermediateField.relfinrank_bot_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
⊥.relfinrank A = Module.finrank F ↥A
source
@[simp]
theorem IntermediateField.relrank_bot_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relrank ⊥ = 1
source
@[simp]
theorem IntermediateField.relfinrank_bot_right {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) :
A.relfinrank ⊥ = 1
source
theorem IntermediateField.relrank_dvd_of_le_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
B.relrank C ∣ A.relrank C
source
theorem IntermediateField.relfinrank_dvd_of_le_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {A B : IntermediateField F E} (C : IntermediateField F E) (h : A ≤ B) :
B.relfinrank C ∣ A.relfinrank C