Documentation

Mathlib.FieldTheory.AlgebraicClosure

Relative Algebraic Closure #

In this file we construct the relative algebraic closure of a field extension.

Main Definitions #

source
def algebraicClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
IntermediateField F E

The relative algebraic closure of a field F in a field extension E, also called the maximal algebraic subextension of E / F, is defined to be the subalgebra integralClosure F E upgraded to an intermediate field (since F and E are both fields). This is exactly the intermediate field of E / F consisting of all integral/algebraic elements.

Equations
Instances For
    source
    theorem mem_algebraicClosure_iff' {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} :
    x ∈ algebraicClosure F E ↔ IsIntegral F x

    An element is contained in the algebraic closure of F in E if and only if it is an integral element.

    source
    theorem mem_algebraicClosure_iff {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} :
    x ∈ algebraicClosure F E ↔ IsAlgebraic F x

    An element is contained in the algebraic closure of F in E if and only if it is an algebraic element.

    source
    theorem map_mem_algebraicClosure_iff {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E →ₐ[F] K) {x : E} :
    i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E

    If i is an F-algebra homomorphism from E to K, then i x is contained in algebraicClosure F K if and only if x is contained in algebraicClosure F E.

    source
    theorem algebraicClosure.comap_eq_of_algHom {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E →ₐ[F] K) :
    IntermediateField.comap i (algebraicClosure F K) = algebraicClosure F E

    If i is an F-algebra homomorphism from E to K, then the preimage of algebraicClosure F K under the map i is equal to algebraicClosure F E.

    source
    theorem algebraicClosure.map_le_of_algHom {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E →ₐ[F] K) :
    IntermediateField.map i (algebraicClosure F E) ≤ algebraicClosure F K

    If i is an F-algebra homomorphism from E to K, then the image of algebraicClosure F E under the map i is contained in algebraicClosure F K.

    source
    theorem algebraicClosure.map_eq_of_algebraicClosure_eq_bot (F : Type u_1) {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (h : algebraicClosure E K = ⊥) :
    IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K

    If K / E / F is a field extension tower, such that K / E has no non-trivial algebraic subextensions (this means that it is purely transcendental), then the image of algebraicClosure F E in K is equal to algebraicClosure F K.

    source
    theorem algebraicClosure.map_eq_of_algEquiv {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :
    IntermediateField.map (↑i) (algebraicClosure F E) = algebraicClosure F K

    If i is an F-algebra isomorphism of E and K, then the image of algebraicClosure F E under the map i is equal to algebraicClosure F K.

    source
    def algebraicClosure.algEquivOfAlgEquiv {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :
    ↥(algebraicClosure F E) ≃ₐ[F] ↥(algebraicClosure F K)

    If E and K are isomorphic as F-algebras, then algebraicClosure F E and algebraicClosure F K are also isomorphic as F-algebras.

    Equations
    Instances For
      source
      def algebraicClosure.AlgEquiv.algebraicClosure {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) :
      ↥(algebraicClosure F E) ≃ₐ[F] ↥(algebraicClosure F K)

      Alias of algebraicClosure.algEquivOfAlgEquiv.

      If E and K are isomorphic as F-algebras, then algebraicClosure F E and algebraicClosure F K are also isomorphic as F-algebras.

      Equations
      Instances For
        source
        instance algebraicClosure.isAlgebraic (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
        Algebra.IsAlgebraic F ↥(algebraicClosure F E)

        The algebraic closure of F in E is algebraic over F.

        Equations
        • ⋯ = ⋯
        source
        instance algebraicClosure.isIntegralClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
        IsIntegralClosure (↥(algebraicClosure F E)) F E

        The algebraic closure of F in E is the integral closure of F in E.

        Equations
        • ⋯ = ⋯
        source
        theorem le_algebraicClosure' (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} (hs : ∀ (x : ↥L), IsAlgebraic F x) :
        L ≤ algebraicClosure F E

        An intermediate field of E / F is contained in the algebraic closure of F in E if all of its elements are algebraic over F.

        source
        theorem le_algebraicClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [Algebra.IsAlgebraic F ↥L] :
        L ≤ algebraicClosure F E

        An intermediate field of E / F is contained in the algebraic closure of F in E if it is algebraic over F.

        source
        theorem le_algebraicClosure_iff (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) :
        L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F ↥L

        An intermediate field of E / F is contained in the algebraic closure of F in E if and only if it is algebraic over F.

        source
        theorem algebraicClosure.algebraicClosure_eq_bot (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
        algebraicClosure (↥(algebraicClosure F E)) E = ⊥

        The algebraic closure in E of the algebraic closure of F in E is equal to itself.

        source
        theorem algebraicClosure.normalClosure_eq_self (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
        normalClosure F (↥(algebraicClosure F E)) E = algebraicClosure F E

        The normal closure in E/F of the algebraic closure of F in E is equal to itself.

        source
        theorem IsAlgClosed.algebraicClosure_eq_bot_iff (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [IsAlgClosed E] :
        algebraicClosure F E = ⊥ ↔ IsAlgClosed F

        If E / F is a field extension and E is algebraically closed, then the algebraic closure of F in E is equal to F if and only if F is algebraically closed.

        source
        theorem IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] {S : Set E} :
        Algebra.IsAlgebraic F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x

        F(S) / F is a algebraic extension if and only if all elements of S are algebraic elements.

        source
        instance algebraicClosure.isAlgClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [IsAlgClosed E] :
        IsAlgClosure F ↥(algebraicClosure F E)

        If E is algebraically closed, then the algebraic closure of F in E is an absolute algebraic closure of F.

        Equations
        • ⋯ = ⋯
        source
        theorem algebraicClosure.eq_top_iff (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
        algebraicClosure F E = ⊤ ↔ Algebra.IsAlgebraic F E

        The algebraic closure of F in E is equal to E if and only if E / F is algebraic.

        source
        theorem algebraicClosure.le_restrictScalars (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (K : Type u_3) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
        algebraicClosure F K ≤ IntermediateField.restrictScalars F (algebraicClosure E K)

        If K / E / F is a field extension tower, then algebraicClosure F K is contained in algebraicClosure E K.

        source
        theorem algebraicClosure.eq_restrictScalars_of_isAlgebraic (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (K : Type u_3) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] :
        algebraicClosure F K = IntermediateField.restrictScalars F (algebraicClosure E K)

        If K / E / F is a field extension tower, such that E / F is algebraic, then algebraicClosure F K is equal to algebraicClosure E K.

        source
        theorem algebraicClosure.adjoin_le (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (K : Type u_3) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] :
        IntermediateField.adjoin E ↑(algebraicClosure F K) ≤ algebraicClosure E K

        If K / E / F is a field extension tower, then E adjoin algebraicClosure F K is contained in algebraicClosure E K.