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]

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

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

            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
              • One or more equations did not get rendered due to their size.
              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

                            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
                                Equations