# Results on finite dimensionality and algebraicity of intermediate fields. #

source
theorem IntermediateField.coe_isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {R : Type u_3} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {x : ↥S} :
IsIntegral R ↑x ↔ IsIntegral R x
source
def Subalgebra.IsAlgebraic.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : Subalgebra K L} (hS : S.IsAlgebraic) :
IntermediateField K L

Turn an algebraic subalgebra into an intermediate field, `Subalgebra.IsAlgebraic` version.

Equations

- hS.toIntermediateField = { toSubalgebra := S, inv_mem' := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Algebra.IsAlgebraic.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) [Algebra.IsAlgebraic K ↥S] :
IntermediateField K L

Turn an algebraic subalgebra into an intermediate field, `Algebra.IsAlgebraic` version.

Equations

- Algebra.IsAlgebraic.toIntermediateField S = ⋯.toIntermediateField

Instances For

source
instance IntermediateField.isAlgebraic_tower_bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} [Algebra.IsAlgebraic K L] :
Algebra.IsAlgebraic K ↥S
source
instance IntermediateField.isAlgebraic_tower_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} [Algebra.IsAlgebraic K L] :
Algebra.IsAlgebraic (↥S) L
source
instance IntermediateField.finiteDimensional_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] :
FiniteDimensional K ↥F
source
instance IntermediateField.finiteDimensional_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] :
FiniteDimensional (↥F) L
source
@[simp]
theorem IntermediateField.rank_eq_rank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
Module.rank K ↥F.toSubalgebra = Module.rank K ↥F
source
@[simp]
theorem IntermediateField.finrank_eq_finrank_subalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) :
Module.finrank K ↥F.toSubalgebra = Module.finrank K ↥F
source
theorem IntermediateField.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥E ≤ Module.finrank K ↥F) :
F = E

If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite, then `F = E`.

source
theorem IntermediateField.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥F = Module.finrank K ↥E) :
F = E

If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite, then `F = E`.

source
theorem IntermediateField.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional (↥F) L] (h_le : F ≤ E) (h_finrank : Module.finrank (↥F) L ≤ Module.finrank (↥E) L) :
F = E

If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite, then `F = E`.

source
theorem IntermediateField.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional (↥F) L] (h_le : F ≤ E) (h_finrank : Module.finrank (↥F) L = Module.finrank (↥E) L) :
F = E

If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite, then `F = E`.

source
theorem IntermediateField.finrank_dvd_of_le_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F ≤ E) :
Module.finrank (↥E) L ∣ Module.finrank (↥F) L
source
theorem IntermediateField.finrank_dvd_of_le_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F ≤ E) :
Module.finrank K ↥F ∣ Module.finrank K ↥E
source
theorem IntermediateField.finrank_le_of_le_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional (↥F) L] (h : F ≤ E) :
Module.finrank (↥E) L ≤ Module.finrank (↥F) L
source
theorem IntermediateField.finrank_le_of_le_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional K ↥E] (h : F ≤ E) :
Module.finrank K ↥F ≤ Module.finrank K ↥E
source
instance IntermediateField.finiteDimensional_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (f : L →ₐ[K] L) [FiniteDimensional K ↥E] :
FiniteDimensional K ↥(map f E)

Mapping a finite-dimensional intermediate field along an algebra equivalence gives a finite-dimensional intermediate field.

source
@[deprecated IntermediateField.finiteDimensional_map (since := "2025-05-02")]
theorem im_finiteDimensional {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (f : L →ₐ[K] L) [FiniteDimensional K ↥E] :
FiniteDimensional K ↥(IntermediateField.map f E)

Alias of `IntermediateField.finiteDimensional_map`.

Mapping a finite-dimensional intermediate field along an algebra equivalence gives a finite-dimensional intermediate field.

source
theorem IntermediateField.isAlgebraic_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : ↥S} :
IsAlgebraic K x ↔ IsAlgebraic K ↑x
source
theorem IntermediateField.isIntegral_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {x : ↥S} :
IsIntegral K x ↔ IsIntegral K ↑x
source
theorem IntermediateField.minpoly_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} (x : ↥S) :
minpoly K x = minpoly K ↑x
source
def subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] :
Subalgebra K L ≃o IntermediateField K L

If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.

Equations

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

Instances For

source
@[simp]
theorem mem_subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : Subalgebra K L} {x : L} :
x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S
source
@[simp]
theorem mem_subalgebraEquivIntermediateField_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] {S : IntermediateField K L} {x : L} :
x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S