Documentation

Mathlib.FieldTheory.IntermediateField.Algebraic

Results on finite dimensionality and algebraicity of intermediate fields. #

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

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

Equations
  • hS.toIntermediateField = { toSubalgebra := S, inv_mem' := }
Instances For
    @[reducible, inline]

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

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