NYLL
Module

PowerChange.lean

Nyll.SchemeTheory.NoetherNormalization.PowerChange
24 declarations indexed from sourceView source ↗

Module documentation

Power-triangular normalization over an arbitrary field

This file exposes the power-triangular change of variables used in Nagata's proof of Noether normalization. The degree-coding argument is adapted from Mathlib.RingTheory.NoetherNormalization (Apache-2.0; authors Riccardo Brasca, Sihan Su, Wan Lin, and Xiaoyang Su), where the corresponding declarations are private.

The distinguished variable is X 0. Every other variable X i is sent to X i + X 0 ^ mᵢ, with rapidly growing exponents mᵢ. Distinct monomials of a fixed nonzero polynomial then acquire distinct degrees in X 0, so the transformed polynomial has invertible leading coefficient over every field.

Imports2
Imported by2

Declarations

def

powerNormalizationBase

L35 ↗
FieldArithmetic.Chapter06.powerNormalizationBase
Documentation

The base used to encode monomial exponent vectors as natural numbers.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
def powerNormalizationBase (F : MvPolynomial (Fin (n + 1)) K) : ℕ
def

powerNormalizationExponent

L39 ↗
FieldArithmetic.Chapter06.powerNormalizationExponent
Documentation

The power assigned to a variable in the power-triangular substitution.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
def powerNormalizationExponent
    (F : MvPolynomial (Fin (n + 1)) K) (i : Fin (n + 1)) : ℕ
abbrev

powerChangeFirstAux

L47 ↗
FieldArithmetic.Chapter06.powerChangeFirstAux
Documentation

The power-triangular algebra map fixing X 0 and sending every other X i to X i + c • X 0 ^ powerNormalizationExponent F i.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
abbrev powerChangeFirstAux
    (F : MvPolynomial (Fin (n + 1)) K) (c : K) :
    MvPolynomial (Fin (n + 1)) K →ₐ[K]
      MvPolynomial (Fin (n + 1)) K
theorem

powerChangeFirstAux_X_zero

L56 ↗
FieldArithmetic.Chapter06.powerChangeFirstAux_X_zero
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerChangeFirstAux_X_zero
    (F : MvPolynomial (Fin (n + 1)) K) (c : K) :
    powerChangeFirstAux F c (X 0) = X 0
theorem

powerChangeFirstAux_X_succ

L62 ↗
FieldArithmetic.Chapter06.powerChangeFirstAux_X_succ
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerChangeFirstAux_X_succ
    (F : MvPolynomial (Fin (n + 1)) K) (c : K) (i : Fin n) :
    powerChangeFirstAux F c (X i.succ) =
      X i.succ + c • X 0 ^ powerNormalizationExponent F i.succ
theorem

powerChangeFirstAux_comp_neg

L68 ↗
FieldArithmetic.Chapter06.powerChangeFirstAux_comp_neg
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerChangeFirstAux_comp_neg
    (F : MvPolynomial (Fin (n + 1)) K) (c : K) :
    (powerChangeFirstAux F c).comp (powerChangeFirstAux F (-c)) =
      AlgHom.id K (MvPolynomial (Fin (n + 1)) K)
abbrev

powerChangeFirstEquiv

L77 ↗
FieldArithmetic.Chapter06.powerChangeFirstEquiv
Documentation

The power-triangular substitution as an algebra equivalence.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
abbrev powerChangeFirstEquiv
    (F : MvPolynomial (Fin (n + 1)) K) :
    MvPolynomial (Fin (n + 1)) K ≃ₐ[K]
      MvPolynomial (Fin (n + 1)) K
lemma

powerDigits_lt_base

L94 ↗
FieldArithmetic.Chapter06.powerDigits_lt_base
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
lemma powerDigits_lt_base {v : Fin (n + 1) →₀ ℕ}
    (vlt : ∀ i, v i < up) :
    ∀ l ∈ ofFn v, l < up
lemma

power_weightedSum_ne

L99 ↗
FieldArithmetic.Chapter06.power_weightedSum_ne
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
lemma power_weightedSum_ne
    (vlt : ∀ i, v i < up) (wlt : ∀ i, w i < up) (hne : v ≠ w) :
    ∑ x : Fin (n + 1), r x * v x ≠
      ∑ x : Fin (n + 1), r x * w x
lemma

degreeOf_zero_powerChange_monomial

L112 ↗
FieldArithmetic.Chapter06.degreeOf_zero_powerChange_monomial
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
lemma degreeOf_zero_powerChange_monomial {a : K} (ha : a ≠ 0) :
    (T (monomial v a)).degreeOf 0 =
      ∑ i : Fin (n + 1), r i * v i
lemma

degreeOf_powerChange_ne_of_ne

L145 ↗
FieldArithmetic.Chapter06.degreeOf_powerChange_ne_of_ne
Documentation

Distinct monomials in the support of F acquire distinct degrees in X 0 after the power-triangular substitution.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
lemma degreeOf_powerChange_ne_of_ne
    (hv : v ∈ F.support) (hw : w ∈ F.support) (hne : v ≠ w) :
    (T (monomial v (F.coeff v))).degreeOf 0 ≠
      (T (monomial w (F.coeff w))).degreeOf 0
lemma

leadingCoeff_finSuccEquiv_powerChange_monomial

L156 ↗
FieldArithmetic.Chapter06.leadingCoeff_finSuccEquiv_powerChange_monomial
Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
lemma leadingCoeff_finSuccEquiv_powerChange_monomial :
    (finSuccEquiv K n
      (T ((monomial v) (F.coeff v)))).leadingCoeff =
        algebraMap K _ (F.coeff v)
theorem

powerChangeFirst_leadingCoeff_isUnit

L185 ↗
FieldArithmetic.Chapter06.powerChangeFirst_leadingCoeff_isUnit
Documentation

Every nonzero polynomial admits the canonical power-triangular change for which it is monic up to a unit as a polynomial in X 0.

Source context 8 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
section LeadingCoefficient
variable (F : MvPolynomial (Fin (n + 1)) K)
variable (v w : Fin (n + 1) →₀ ℕ)
Lean source · statement
theorem powerChangeFirst_leadingCoeff_isUnit (hF : F ≠ 0) :
    IsUnit (finSuccEquiv K n (T F)).leadingCoeff
def

powerTailCoordinatesFirst

L231 ↗
FieldArithmetic.Chapter06.powerTailCoordinatesFirst
Documentation

The transformed tail coordinates in an arbitrary K-algebra. They are the inverse-coordinate expressions for powerChangeFirstEquiv F.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
def powerTailCoordinatesFirst
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) : Fin n → A
def

powerCoordinatesFirst

L240 ↗
FieldArithmetic.Chapter06.powerCoordinatesFirst
Documentation

The full inverse-coordinate tuple, retaining the first coordinate.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
def powerCoordinatesFirst
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) : Fin (n + 1) → A
theorem

powerCoordinatesFirst_zero

L247 ↗
FieldArithmetic.Chapter06.powerCoordinatesFirst_zero
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerCoordinatesFirst_zero
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) :
    powerCoordinatesFirst F x 0 = x 0
theorem

powerCoordinatesFirst_succ

L254 ↗
FieldArithmetic.Chapter06.powerCoordinatesFirst_succ
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerCoordinatesFirst_succ
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) (i : Fin n) :
    powerCoordinatesFirst F x i.succ =
      x i.succ - x 0 ^ powerNormalizationExponent F i.succ
theorem

aeval_powerChangeFirst_powerCoordinates

L265 ↗
FieldArithmetic.Chapter06.aeval_powerChangeFirst_powerCoordinates
Documentation

Evaluating the power transform at its inverse-coordinate tuple recovers evaluation at the original tuple.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem aeval_powerChangeFirst_powerCoordinates
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A)
    (P : MvPolynomial (Fin (n + 1)) K) :
    aeval (powerCoordinatesFirst F x) (powerChangeFirstEquiv F P) =
      aeval x P
theorem

powerCoordinatesFirst_isIntegral

L293 ↗
FieldArithmetic.Chapter06.powerCoordinatesFirst_isIntegral
Documentation

A nonzero relation makes the first coordinate integral over the algebra generated by the canonical power-tail coordinates.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem powerCoordinatesFirst_isIntegral
    {A : Type*} [CommRing A] [Algebra K A]
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    IsIntegral
      (Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x))) (x 0)
theorem

adjoin_powerTailCoordinatesFirst_le

L356 ↗
FieldArithmetic.Chapter06.adjoin_powerTailCoordinatesFirst_le
Documentation

Every canonical power-tail coordinate belongs to the algebra generated by the original tuple.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem adjoin_powerTailCoordinatesFirst_le
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) :
    Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x)) ≤
      Algebra.adjoin K (Set.range x)
theorem

adjoin_range_eq_adjoin_powerTailCoordinatesFirst_union

L375 ↗
FieldArithmetic.Chapter06.adjoin_range_eq_adjoin_powerTailCoordinatesFirst_union
Documentation

The canonical power-tail coordinates together with the retained first coordinate generate the same algebra as the original tuple.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem adjoin_range_eq_adjoin_powerTailCoordinatesFirst_union
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A) :
    Algebra.adjoin K (Set.range x) =
      Algebra.adjoin K
        (Set.range (powerTailCoordinatesFirst F x) ∪ {x 0})
theorem

isIntegral_of_mem_adjoin_range_powerFirst

L419 ↗
FieldArithmetic.Chapter06.isIntegral_of_mem_adjoin_range_powerFirst
Documentation

If the retained first coordinate is integral over the canonical power-tail algebra, then every element generated by the original tuple is integral over that tail algebra.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · statement
theorem isIntegral_of_mem_adjoin_range_powerFirst
    {A : Type*} [CommRing A] [Algebra K A]
    (F : MvPolynomial (Fin (n + 1)) K)
    (x : Fin (n + 1) → A)
    (hfirst :
      IsIntegral
        (Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x)))
        (x 0)) :
    ∀ y ∈ Algebra.adjoin K (Set.range x),
      IsIntegral
        (Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x))) y
theorem

exists_powerCoordinatesFirst_isIntegral

L460 ↗
FieldArithmetic.Chapter06.exists_powerCoordinatesFirst_isIntegral
Documentation

Existential form of powerCoordinatesFirst_isIntegral, exposing the powers assigned to the n tail coordinates.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · full declaration
theorem exists_powerCoordinatesFirst_isIntegral
    {A : Type*} [CommRing A] [Algebra K A]
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ m : Fin n → ℕ,
      IsIntegral
        (Algebra.adjoin K
          (Set.range fun i =>
            x i.succ - x 0 ^ m i)) (x 0) := by
  refine ⟨fun i => powerNormalizationExponent F i.succ, ?_⟩
  change
    IsIntegral
      (Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x))) (x 0)
  exact powerCoordinatesFirst_isIntegral x hF hrel
theorem

exists_generatorReducing_powerTail

L480 ↗
FieldArithmetic.Chapter06.exists_generatorReducing_powerTail
Documentation

One arbitrary-field generator-reducing step. It exposes the chosen power family and returns both the generating equality and integrality of the whole old generated algebra over the new n-element tail algebra.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open Polynomial MvPolynomial Nat RingHom List
variable {K : Type*} [Field K] {n : ℕ}
Lean source · full declaration
theorem exists_generatorReducing_powerTail
    {A : Type*} [CommRing A] [Algebra K A]
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ m : Fin n → ℕ,
      let t : Fin n → A := fun i => x i.succ - x 0 ^ m i
      Algebra.adjoin K (Set.range t) ≤ Algebra.adjoin K (Set.range x) ∧
        Algebra.adjoin K (Set.range x) =
          Algebra.adjoin K (Set.range t ∪ {x 0}) ∧
        ∀ y ∈ Algebra.adjoin K (Set.range x),
          IsIntegral (Algebra.adjoin K (Set.range t)) y := by
  let m : Fin n → ℕ := fun i => powerNormalizationExponent F i.succ
  refine ⟨m, ?_, ?_, ?_⟩
  · change
      Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x)) ≤
        Algebra.adjoin K (Set.range x)
    exact adjoin_powerTailCoordinatesFirst_le F x
  · change
      Algebra.adjoin K (Set.range x) =
        Algebra.adjoin K
          (Set.range (powerTailCoordinatesFirst F x) ∪ {x 0})
    exact adjoin_range_eq_adjoin_powerTailCoordinatesFirst_union F x
  · change
      ∀ y ∈ Algebra.adjoin K (Set.range x),
        IsIntegral
          (Algebra.adjoin K (Set.range (powerTailCoordinatesFirst F x))) y
    exact isIntegral_of_mem_adjoin_range_powerFirst F x
      (powerCoordinatesFirst_isIntegral x hF hrel)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.