Documentation

Mathlib.FieldTheory.IntermediateField.Algebraic

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