Documentation

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Algebraic Closure #

In this file we construct the algebraic closure of a field

Main Definitions #

Tags #

algebraic closure, algebraically closed

@[reducible, inline]

The subtype of monic irreducible polynomials

Equations
Instances For

    Sends a monic irreducible polynomial f to f(x_f) where x_f is a formal indeterminate.

    Equations
    Instances For

      The span of f(x_f) across monic irreducible polynomials f where x_f is an indeterminate.

      Equations
      Instances For

        Given a finset of monic irreducible polynomials, construct an algebra homomorphism to the splitting field of the product of the polynomials sending each indeterminate x_f represented by the polynomial f in the finset to a root of f.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          A random maximal ideal that contains spanEval k

          Equations
          Instances For
            Equations
            • =

            The first step of constructing AlgebraicClosure: adjoin a root of all monic polynomials

            Equations
            Instances For

              The canonical ring homomorphism to AdjoinMonic k.

              Equations
              Instances For
                def AlgebraicClosure.stepAux (k : Type u) [Field k] (n : ) :
                (α : Type u) × Field α

                The nth step of constructing AlgebraicClosure, together with its Field instance.

                Equations
                Instances For
                  def AlgebraicClosure.Step (k : Type u) [Field k] (n : ) :

                  The nth step of constructing AlgebraicClosure.

                  Equations
                  Instances For

                    The canonical inclusion to the 0th step.

                    Equations
                    Instances For

                      The canonical ring homomorphism to the next step.

                      Equations
                      Instances For

                        The canonical ring homomorphism to a step with a greater index.

                        Equations
                        Instances For
                          @[simp]
                          theorem AlgebraicClosure.coe_toStepOfLE (k : Type u) [Field k] (m : ) (n : ) (h : m n) :
                          (AlgebraicClosure.toStepOfLE k m n h) = fun (a : AlgebraicClosure.Step k m) => Nat.leRecOn h (fun (n : ) => (AlgebraicClosure.toStepSucc k n)) a
                          Equations
                          • =
                          def AlgebraicClosureAux (k : Type u) [Field k] :

                          Auxiliary construction for AlgebraicClosure. Although AlgebraicClosureAux does define the algebraic closure of a field, it is redefined at AlgebraicClosure in order to make sure certain instance diamonds commute by definition.

                          Equations
                          Instances For

                            The canonical ring embedding from the nth step to the algebraic closure.

                            Equations
                            Instances For
                              theorem AlgebraicClosureAux.exists_root (k : Type u) [Field k] {f : Polynomial (AlgebraicClosureAux k)} (hfm : f.Monic) (hfi : Irreducible f) :

                              Canonical algebra embedding from the nth step to the algebraic closure.

                              Equations
                              Instances For
                                def AlgebraicClosure (k : Type u) [Field k] :

                                The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field.

                                Equations
                                Instances For
                                  instance AlgebraicClosure.instIsScalarTower (k : Type u) [Field k] {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra S k] [Algebra R k] [IsScalarTower R S k] :
                                  Equations
                                  • =
                                  Equations
                                  Equations
                                  • =
                                  instance AlgebraicClosure.instCharP (k : Type u) [Field k] {p : } [CharP k p] :
                                  Equations
                                  • =