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
  • 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
    Instances For
      source
      def algebraicClosure {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :
      IntermediateField K L

      The algebraic closure of a field K in an extension L, the subalgebra integralClosure K L upgraded to an intermediate field (when K and L are both fields).

      Equations
      Instances For
        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
        Equations
        • ⋯ = ⋯
        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
        Equations
        • ⋯ = ⋯
        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
        @[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
        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 : 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.

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

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

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

        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