Module

PrimitiveReduction.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.PrimitiveReduction

10 declarations indexed from sourceView source ↗

Module documentation

Primitive polynomials detected by reduction

The construction calls a polynomial over a valuation ring primitive when its reduction modulo the maximal ideal is nonzero. The lemma below identifies that condition with the divisibility notion used by mathlib's Gauss lemma.

Imports3

Nyll.ValuedFieldTheory.Valuation.Henselian.Core
Mathlib.RingTheory.Polynomial.GaussLemma
Mathlib.RingTheory.Polynomial.ContentIdeal

Imported by9

theorem

polynomial_isPrimitive_of_residue_ne_zero

L28 ↗

DiscreteValuationField.polynomial_isPrimitive_of_residue_ne_zero

Documentation

Over a local ring, a polynomial whose residue is nonzero is primitive in the Gauss-lemma sense: every constant divisor is a unit.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem polynomial_isPrimitive_of_residue_ne_zero
    {R : Type*} [CommRing R] [IsLocalRing R]
    {f : Polynomial R}
    (hf : f.map (IsLocalRing.residue R) ≠ 0) :
    f.IsPrimitive

theorem

exists_isUnit_coeff_of_isPrimitive

L45 ↗

DiscreteValuationField.exists_isUnit_coeff_of_isPrimitive

Documentation

A primitive polynomial over a valuation subring has a unit coefficient. The proof chooses a coefficient of maximal valuation; it divides every other coefficient, so primitivity forces it to be a unit.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem exists_isUnit_coeff_of_isPrimitive
    {K : Type*} [Field K] (V : ValuationSubring K)
    {f : Polynomial V} (hf : f.IsPrimitive) :
    ∃ i : ℕ, IsUnit (f.coeff i)

theorem

polynomial_residue_ne_zero_of_isPrimitive

L74 ↗

DiscreteValuationField.polynomial_residue_ne_zero_of_isPrimitive

Documentation

The reduction of a primitive polynomial over a valuation subring is nonzero.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem polynomial_residue_ne_zero_of_isPrimitive
    {K : Type*} [Field K] (V : ValuationSubring K)
    {f : Polynomial V} (hf : f.IsPrimitive) :
    f.map (IsLocalRing.residue V) ≠ 0

theorem

associated_multiset_map_prod_of_forall

L88 ↗

DiscreteValuationField.associated_multiset_map_prod_of_forall

Documentation

Pointwise associated factors have associated multiset products.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem associated_multiset_map_prod_of_forall
    {I M : Type*} [CommMonoid M]
    (s : Multiset I) (f g : I → M)
    (h : ∀ i ∈ s, Associated (f i) (g i)) :
    Associated (s.map f).prod (s.map g).prod

theorem

associated_of_isPrimitive_of_map_associated

L103 ↗

DiscreteValuationField.associated_of_isPrimitive_of_map_associated

Documentation

Gauss association descends through a valuation subring: primitive polynomials that become associated over the fraction field are already associated over the valuation ring.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem associated_of_isPrimitive_of_map_associated
    {K : Type*} [Field K] (V : ValuationSubring K)
    {f g : Polynomial V} (hf : f.IsPrimitive) (hg : g.IsPrimitive)
    (hassoc : Associated (f.map V.subtype) (g.map V.subtype)) :
    Associated f g

theorem

isPrimitive_mul_of_valuationSubring

L165 ↗

DiscreteValuationField.isPrimitive_mul_of_valuationSubring

Documentation

Gauss's product lemma for a valuation subring, stated without choosing a NormalizedGCDMonoid structure.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem isPrimitive_mul_of_valuationSubring
    {K : Type*} [Field K] (V : ValuationSubring K)
    {f g : Polynomial V} (hf : f.IsPrimitive) (hg : g.IsPrimitive) :
    (f * g).IsPrimitive

theorem

isPrimitive_finset_prod_of_valuationSubring

L174 ↗

DiscreteValuationField.isPrimitive_finset_prod_of_valuationSubring

Documentation

A finite product of primitive polynomials over a valuation subring is primitive.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem isPrimitive_finset_prod_of_valuationSubring
    {K I : Type*} [Field K] (V : ValuationSubring K)
    (s : Finset I) (f : I → Polynomial V)
    (hf : ∀ i ∈ s, (f i).IsPrimitive) :
    (∏ i ∈ s, f i).IsPrimitive

theorem

isPrimitive_multiset_prod_of_valuationSubring

L190 ↗

DiscreteValuationField.isPrimitive_multiset_prod_of_valuationSubring

Documentation

Multiset form of the preceding primitive-product lemma, convenient for unique-factorization multisets over K[X].

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem isPrimitive_multiset_prod_of_valuationSubring
    {K : Type*} [Field K] (V : ValuationSubring K)
    (s : Multiset (Polynomial V))
    (hs : ∀ f ∈ s, f.IsPrimitive) :
    s.prod.IsPrimitive

theorem

exists_primitive_irreducible_lift_of_irreducible

L208 ↗

DiscreteValuationField.exists_primitive_irreducible_lift_of_irreducible

Documentation

Every irreducible polynomial over the fraction field of a valuation subring is associated to the image of a primitive irreducible polynomial over the valuation subring. This is the normalization step used when the the construction factors a primitive polynomial over K and then rescales each irreducible factor back into the valuation ring.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem exists_primitive_irreducible_lift_of_irreducible
    {K : Type*} [Field K] (V : ValuationSubring K)
    {p : Polynomial K} (hp : Irreducible p) :
    ∃ q : Polynomial V,
      q.IsPrimitive ∧ Irreducible q ∧
        Associated (q.map V.subtype) p

theorem

primitive_associated_prod_primitive_irreducible_map_factors

L287 ↗

DiscreteValuationField.primitive_associated_prod_primitive_irreducible_map_factors

Documentation

A primitive polynomial over a valuation subring is, up to a unit over that valuation subring, a finite product of primitive polynomials whose fraction-field images are irreducible.

Source context 4 commands

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

noncomputable section
open Polynomial
open UniqueFactorizationMonoid
namespace DiscreteValuationField

Lean source · statement

theorem primitive_associated_prod_primitive_irreducible_map_factors
    {K : Type*} [Field K] (V : ValuationSubring K)
    (f : Polynomial V) (hf : f.IsPrimitive) :
    ∃ factors : Multiset (Polynomial V),
      (∀ Q ∈ factors, Q.IsPrimitive ∧ Irreducible (Q.map V.subtype)) ∧
        Associated factors.prod f

Module documentation

Primitive polynomials detected by reduction

Declarations