Documentation

Mathlib.FieldTheory.IntermediateField.Algebraic

Results on finite dimensionality and algebraicity of intermediate fields. #

Equations
  • =
Equations
  • =
@[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
@[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
@[simp]
theorem IntermediateField.toSubalgebra_eq_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K L} :
F.toSubalgebra = E.toSubalgebra F = E
theorem IntermediateField.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {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.

theorem IntermediateField.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {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.

theorem IntermediateField.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {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.

theorem IntermediateField.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {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.

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} :
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} :
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

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
    @[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
    @[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