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

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

Documentation

Mathlib.FieldTheory.IntermediateField.Algebraic

Results on finite dimensionality and algebraicity of intermediate fields. #