Documentation

Mathlib.FieldTheory.IsAlgClosed.Basic

Algebraically Closed Field #

In this file we define the typeclass for algebraically closed fields and algebraic closures, and prove some of their properties.

Main Definitions #

Tags #

algebraic closure, algebraically closed

TODO #

class IsAlgClosed (k : Type u) [Field k] :

Typeclass for algebraically closed fields.

To show Polynomial.Splits p f for an arbitrary ring homomorphism f, see IsAlgClosed.splits_codomain and IsAlgClosed.splits_domain.

Instances
    theorem IsAlgClosed.splits_codomain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : K →+* k} (p : Polynomial K) :

    Every polynomial splits in the field extension f : K →+* k if k is algebraically closed.

    See also IsAlgClosed.splits_domain for the case where K is algebraically closed.

    theorem IsAlgClosed.splits_domain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : Polynomial k) :

    Every polynomial splits in the field extension f : K →+* k if K is algebraically closed.

    See also IsAlgClosed.splits_codomain for the case where k is algebraically closed.

    theorem IsAlgClosed.exists_root {k : Type u} [Field k] [IsAlgClosed k] (p : Polynomial k) (hp : Polynomial.degree p 0) :
    ∃ (x : k), Polynomial.IsRoot p x
    theorem IsAlgClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsAlgClosed k] (x : k) {n : } (hn : 0 < n) :
    ∃ (z : k), z ^ n = x
    theorem IsAlgClosed.exists_eq_mul_self {k : Type u} [Field k] [IsAlgClosed k] (x : k) :
    ∃ (z : k), x = z * z
    theorem IsAlgClosed.exists_eval₂_eq_zero_of_injective {k : Type u} [Field k] {R : Type u_1} [Ring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective f) (p : Polynomial R) (hp : Polynomial.degree p 0) :
    ∃ (x : k), Polynomial.eval₂ f x p = 0
    theorem IsAlgClosed.exists_eval₂_eq_zero {k : Type u} [Field k] {R : Type u_1} [Field R] [IsAlgClosed k] (f : R →+* k) (p : Polynomial R) (hp : Polynomial.degree p 0) :
    ∃ (x : k), Polynomial.eval₂ f x p = 0
    theorem IsAlgClosed.exists_aeval_eq_zero_of_injective (k : Type u) [Field k] {R : Type u_1} [CommRing R] [IsAlgClosed k] [Algebra R k] (hinj : Function.Injective (algebraMap R k)) (p : Polynomial R) (hp : Polynomial.degree p 0) :
    ∃ (x : k), (Polynomial.aeval x) p = 0
    theorem IsAlgClosed.exists_aeval_eq_zero (k : Type u) [Field k] {R : Type u_1} [Field R] [IsAlgClosed k] [Algebra R k] (p : Polynomial R) (hp : Polynomial.degree p 0) :
    ∃ (x : k), (Polynomial.aeval x) p = 0
    theorem IsAlgClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), Polynomial.Monic pIrreducible p∃ (x : k), Polynomial.eval x p = 0) :
    theorem IsAlgClosed.of_ringEquiv (k : Type u) [Field k] (k' : Type u) [Field k'] (e : k ≃+* k') [IsAlgClosed k] :

    If k is algebraically closed, K / k is a field extension, L / k is an intermediate field which is algebraic, then L is equal to k. A corollary of IsAlgClosed.algebraMap_surjective_of_isAlgebraic.

    class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :

    Typeclass for an extension being an algebraic closure.

    Instances
      instance IsAlgClosure.normal (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] :
      Normal R K
      Equations
      • =
      instance IsAlgClosure.separable (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] [CharZero R] :
      Equations
      • =
      theorem IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic {K : Type u} [Field K] {L : Type v} {M : Type w} [Field L] [Algebra K L] [Field M] [Algebra K M] [IsAlgClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] (hE : Algebra.IsAlgebraic L E) :

      If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K. Known as the extension lemma in https://math.stackexchange.com/a/687914.

      @[irreducible]
      noncomputable def IsAlgClosed.lift {M : Type u_1} [Field M] [IsAlgClosed M] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [NoZeroSMulDivisors R S] [NoZeroSMulDivisors R M] (hS : Algebra.IsAlgebraic R S) :

      A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.

      Equations
      Instances For
        theorem IsAlgClosed.lift_def {M : Type u_1} [Field M] [IsAlgClosed M] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [NoZeroSMulDivisors R S] [NoZeroSMulDivisors R M] (hS : Algebra.IsAlgebraic R S) :
        IsAlgClosed.lift hS = let_fun this := ; let_fun this_1 := ; let_fun this_2 := ; let f := IsAlgClosed.lift_aux (FractionRing R) (FractionRing S) M this_2; AlgHom.comp (AlgHom.restrictScalars R f) (AlgHom.restrictScalars R (Algebra.ofId S (FractionRing S)))
        noncomputable instance IsAlgClosed.perfectRing (k : Type u) [Field k] (p : ) [Fact (Nat.Prime p)] [CharP k p] [IsAlgClosed k] :
        Equations
        • =
        noncomputable instance IsAlgClosed.perfectField (k : Type u) [Field k] [IsAlgClosed k] :
        Equations
        • =

        Algebraically closed fields are infinite since Xⁿ⁺¹ - 1 is separable when #K = n

        Equations
        • =
        noncomputable def IsAlgClosure.equiv (R : Type u) [CommRing R] (L : Type v) (M : Type w) [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L] :

        A (random) isomorphism between two algebraic closures of R.

        Equations
        Instances For
          theorem IsAlgClosure.ofAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) [Field K] [Field J] [Field L] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] (hKJ : Algebra.IsAlgebraic K J) :

          If J is an algebraic extension of K and L is an algebraic closure of J, then it is also an algebraic closure of K.

          noncomputable def IsAlgClosure.equivOfAlgebraic' (R : Type u) (S : Type u_3) (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] [Algebra R S] [Algebra R L] [IsScalarTower R S L] [Nontrivial S] [NoZeroSMulDivisors R S] (hRL : Algebra.IsAlgebraic R L) :

          A (random) isomorphism between an algebraic closure of R and an algebraic closure of an algebraic extension of R

          Equations
          Instances For
            noncomputable def IsAlgClosure.equivOfAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) (M : Type w) [Field K] [Field J] [Field L] [Field M] [Algebra K M] [IsAlgClosure K M] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] (hKJ : Algebra.IsAlgebraic K J) :

            A (random) isomorphism between an algebraic closure of K and an algebraic closure of an algebraic extension of K

            Equations
            Instances For
              noncomputable def IsAlgClosure.equivOfEquivAux {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :

              Used in the definition of equivOfEquiv

              Equations
              Instances For
                noncomputable def IsAlgClosure.equivOfEquiv {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :
                L ≃+* M

                Algebraic closure of isomorphic fields are isomorphic

                Equations
                Instances For
                  @[simp]
                  theorem IsAlgClosure.equivOfEquiv_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :
                  @[simp]
                  theorem IsAlgClosure.equivOfEquiv_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) (s : S) :
                  (IsAlgClosure.equivOfEquiv L M hSR) ((algebraMap S L) s) = (algebraMap R M) (hSR s)
                  @[simp]
                  theorem IsAlgClosure.equivOfEquiv_symm_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) (r : R) :
                  theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) [IsAlgClosed A] (x : K) :
                  (Set.range fun (ψ : K →ₐ[F] A) => ψ x) = Polynomial.rootSet (minpoly F x) A

                  Let A be an algebraically closed field and let x ∈ K, with K/F an algebraic extension of fields. Then the images of x by the F-algebra morphisms from K to A are exactly the roots in A of the minimal polynomial of x over F.

                  @[simp]
                  theorem IntermediateField.algHomEquivAlgHomOfSplits_symm_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : IntermediateField F A) (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (f : K →ₐ[F] A) :
                  (IntermediateField.algHomEquivAlgHomOfSplits A hK L hL).symm f = AlgHom.codRestrict f L.toSubalgebra
                  @[simp]
                  theorem IntermediateField.algHomEquivAlgHomOfSplits_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : IntermediateField F A) (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (φ₂ : K →ₐ[F] L) :
                  def IntermediateField.algHomEquivAlgHomOfSplits {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : IntermediateField F A) (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) :
                  (K →ₐ[F] L) (K →ₐ[F] A)

                  All F-embeddings of a field K into another field A factor through any intermediate field of A/F in which the minimal polynomial of elements of K splits.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem IntermediateField.algHomEquivAlgHomOfSplits_apply_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : IntermediateField F A) (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (f : K →ₐ[F] L) (x : K) :
                    ((IntermediateField.algHomEquivAlgHomOfSplits A hK L hL) f) x = (algebraMap (L) A) (f x)
                    noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) :
                    (K →ₐ[F] L) (K →ₐ[F] A)

                    All F-embeddings of a field K into another field A factor through any subextension of A/F in which the minimal polynomial of elements of K splits.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] (hK : Algebra.IsAlgebraic F K) (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (f : K →ₐ[F] L) (x : K) :