Module

PolynomialFactors.lean

Nyll.ValuedFieldTheory.Valuation.Completion.PolynomialFactors

14 declarations indexed from sourceView source ↗

Module documentation

Irreducible factors as conjugacy classes of roots

This file records the algebraic source lemma underlying the extension-factor correspondence. Multiplicities are deliberately discarded: extensions of a valuation correspond to the distinct irreducible factors over the completion.

Imports4

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.FieldTheory.Minpoly.IsConjRoot
Mathlib.Algebra.Polynomial.FieldDivision
Mathlib.RingTheory.Adjoin.PowerBasis

Imported by3

def

polynomialNormalizedFactors

L35 ↗

ValuationTheory.Completion.polynomialNormalizedFactors

Documentation

The canonical monic normalization of polynomial factors over a field. The normalization instances for an arbitrary field require a decidable equality; this definition installs the classical one internally instead of exposing it as an assumption of the extension-factor correspondence.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

def polynomialNormalizedFactors
    {F : Type u} [Field F] (p : F[X]) : Multiset F[X]

def

polynomialDistinctNormalizedFactors

L44 ↗

ValuationTheory.Completion.polynomialDistinctNormalizedFactors

Documentation

The finite set underlying polynomialNormalizedFactors, with repeated factors removed.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

def polynomialDistinctNormalizedFactors
    {F : Type u} [Field F] (p : F[X]) : Finset F[X]

theorem

polynomialNormalizedFactors_eq_of_associated

L50 ↗

ValuationTheory.Completion.polynomialNormalizedFactors_eq_of_associated

Documentation

Associated polynomials have the same multiset of normalized irreducible factors.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem polynomialNormalizedFactors_eq_of_associated
    {F : Type u} [Field F] {p q : F[X]} (h : Associated p q) :
    polynomialNormalizedFactors p = polynomialNormalizedFactors q

theorem

polynomialDistinctNormalizedFactors_eq_of_associated

L58 ↗

ValuationTheory.Completion.polynomialDistinctNormalizedFactors_eq_of_associated

Documentation

Associated polynomials have the same set of distinct normalized factors.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem polynomialDistinctNormalizedFactors_eq_of_associated
    {F : Type u} [Field F] {p q : F[X]} (h : Associated p q) :
    polynomialDistinctNormalizedFactors p =
      polynomialDistinctNormalizedFactors q

abbrev

DistinctNormalizedFactors

L69 ↗

ValuationTheory.Completion.DistinctNormalizedFactors

Documentation

The distinct normalized irreducible factors of a nonzero polynomial. Using toFinset removes the multiplicities retained by normalizedFactors.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

abbrev DistinctNormalizedFactors
    {F : Type u} [Field F] (p : F[X])

abbrev

PolynomialRootsIn

L74 ↗

ValuationTheory.Completion.PolynomialRootsIn

Documentation

The roots in E of a polynomial over the base field F.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

abbrev PolynomialRootsIn
    {F : Type u} [Field F] (E : Type v) [Field E] [Algebra F E]
    (p : F[X])

def

rootMinpoly

L80 ↗

ValuationTheory.Completion.rootMinpoly

Documentation

Send a root to its monic minimal polynomial over the base field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

def rootMinpoly
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    (p : F[X]) : PolynomialRootsIn E p → F[X]

abbrev

rootMinpolySetoid

L87 ↗

ValuationTheory.Completion.rootMinpolySetoid

Documentation

Equality of the minimal polynomials of two roots. Over a normal closure, this is equivalently conjugacy under the absolute Galois group.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

abbrev rootMinpolySetoid
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    (p : F[X]) : Setoid (PolynomialRootsIn E p)

theorem

rootMinpoly_mem_normalizedFactors

L93 ↗

ValuationTheory.Completion.rootMinpoly_mem_normalizedFactors

Documentation

The minimal polynomial of a root occurs among the normalized factors of the polynomial.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem rootMinpoly_mem_normalizedFactors
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    [Algebra.IsAlgebraic F E] {p : F[X]} (hp : p ≠ 0)
    (x : PolynomialRootsIn E p) :
    rootMinpoly p x ∈ polynomialDistinctNormalizedFactors p

theorem

range_rootMinpoly_eq_distinctNormalizedFactors

L107 ↗

ValuationTheory.Completion.range_rootMinpoly_eq_distinctNormalizedFactors

Documentation

Minimal polynomials of roots exhaust the distinct normalized factors.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem range_rootMinpoly_eq_distinctNormalizedFactors
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    [Algebra.IsAlgebraic F E] [IsAlgClosed E]
    {p : F[X]} (hp : p ≠ 0) :
    Set.range (rootMinpoly p : PolynomialRootsIn E p → F[X]) =
      {g : F[X] | g ∈ polynomialDistinctNormalizedFactors p}

def

rootClassesEquivDistinctNormalizedFactors

L137 ↗

ValuationTheory.Completion.rootClassesEquivDistinctNormalizedFactors

Documentation

Conjugacy classes of roots of p are in canonical bijection with the distinct normalized irreducible factors of p.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

def rootClassesEquivDistinctNormalizedFactors
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    [Algebra.IsAlgebraic F E] [IsAlgClosed E]
    {p : F[X]} (hp : p ≠ 0) :
    Quotient (rootMinpolySetoid (E := E) p) ≃
      DistinctNormalizedFactors p

theorem

rootMinpolySetoid_rel_iff_isConjRoot

L147 ↗

ValuationTheory.Completion.rootMinpolySetoid_rel_iff_isConjRoot

Documentation

Two roots are equivalent precisely when they are conjugate roots.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem rootMinpolySetoid_rel_iff_isConjRoot
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    {p : F[X]} (x y : PolynomialRootsIn E p) :
    (rootMinpolySetoid p).r x y ↔ IsConjRoot F (x : E) (y : E)

theorem

rootMinpolySetoid_rel_iff_orbitRel

L154 ↗

ValuationTheory.Completion.rootMinpolySetoid_rel_iff_orbitRel

Documentation

Minimal-polynomial equivalence of roots agrees with the Galois orbit relation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

theorem rootMinpolySetoid_rel_iff_orbitRel
    {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E]
    [Normal F E] {p : F[X]} (x y : PolynomialRootsIn E p) :
    (rootMinpolySetoid p).r x y ↔
      MulAction.orbitRel Gal(E / F) E (x : E) (y : E)

def

simpleEmbeddingsEquivMappedMinpolyRoots

L164 ↗

ValuationTheory.Completion.simpleEmbeddingsEquivMappedMinpolyRoots

Documentation

For a simple finite extension L = K(α), K-embeddings into an extension of K' are the roots, in that extension, of the minimal polynomial of α after base change from K to K'.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace ValuationTheory
namespace Completion
universe u v

Lean source · statement

def simpleEmbeddingsEquivMappedMinpolyRoots
    {K : Type u} {L : Type v} {K' E : Type*}
    [Field K] [Field L] [Field K'] [Field E]
    [Algebra K L] [Algebra K K'] [Algebra K E] [Algebra K' E]
    [IsScalarTower K K' E]
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    (L →ₐ[K] E) ≃
      PolynomialRootsIn E
        ((minpoly K α).map (algebraMap K K'))

Module documentation

Irreducible factors as conjugacy classes of roots

Declarations