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

Instances For

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

    Instances For

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

      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.

        Instances For

          A random maximal ideal that contains spanEval k

          Instances For

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

            Instances For

              The canonical ring homomorphism to AdjoinMonic k.

              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.

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

                  The nth step of constructing AlgebraicClosure.

                  Instances For

                    The canonical inclusion to the 0th step.

                    Instances For

                      The canonical ring homomorphism to the next step.

                      Instances For

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

                        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 => Nat.leRecOn h (fun n => ↑(AlgebraicClosure.toStepSucc k n)) a
                          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.

                          Instances For

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

                            Instances For

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

                              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.

                                Instances For