NYLL
Module

LinearChange.lean

Nyll.SchemeTheory.NoetherNormalization.LinearChange
21 declarations indexed from sourceView source ↗

Module documentation

Linear changes of variables for Noether normalization

This file formalizes the triangular linear substitution used in Fried--Jarden, Lemma 22.5.1. It fixes the first variable and sends each remaining variable Xᵢ to Xᵢ + cᵢ X₀.

Imports1
Imported by3

Declarations

def

linearChangeFirst

L30 ↗
FieldArithmetic.Chapter06.linearChangeFirst
Documentation

The triangular linear substitution fixing X₀ and sending Xᵢ₊₁ to Xᵢ₊₁ + cᵢ X₀.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
def linearChangeFirst {n : ℕ} (c : Fin n → K) :
    MvPolynomial (Fin (n + 1)) K →ₐ[K] MvPolynomial (Fin (n + 1)) K
theorem

linearChangeFirst_X_zero

L35 ↗
FieldArithmetic.Chapter06.linearChangeFirst_X_zero
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearChangeFirst_X_zero {n : ℕ} (c : Fin n → K) :
    linearChangeFirst c (X 0) = X 0
theorem

linearChangeFirst_X_succ

L40 ↗
FieldArithmetic.Chapter06.linearChangeFirst_X_succ
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearChangeFirst_X_succ {n : ℕ} (c : Fin n → K) (i : Fin n) :
    linearChangeFirst c (X i.succ) = X i.succ + C (c i) * X 0
theorem

linearChangeFirst_comp_neg

L44 ↗
FieldArithmetic.Chapter06.linearChangeFirst_comp_neg
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearChangeFirst_comp_neg {n : ℕ} (c : Fin n → K) :
    (linearChangeFirst c).comp (linearChangeFirst (-c)) =
      AlgHom.id K (MvPolynomial (Fin (n + 1)) K)
def

linearChangeFirstEquiv

L56 ↗
FieldArithmetic.Chapter06.linearChangeFirstEquiv
Documentation

The triangular linear 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 MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
def linearChangeFirstEquiv {n : ℕ} (c : Fin n → K) :
    MvPolynomial (Fin (n + 1)) K ≃ₐ[K] MvPolynomial (Fin (n + 1)) K
theorem

linearChangeFirst_isHomogeneous

L62 ↗
FieldArithmetic.Chapter06.linearChangeFirst_isHomogeneous
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearChangeFirst_isHomogeneous {n d : ℕ} (c : Fin n → K)
    {F : MvPolynomial (Fin (n + 1)) K} (hF : F.IsHomogeneous d) :
    (linearChangeFirst c F).IsHomogeneous d
theorem

eval_linearChangeFirst_finCons_one_zero

L82 ↗
FieldArithmetic.Chapter06.eval_linearChangeFirst_finCons_one_zero
Documentation

Evaluating the triangular transform at (1, 0, ..., 0) is the same as evaluating the original polynomial at (1, c₁, ..., cₙ).

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem eval_linearChangeFirst_finCons_one_zero {n : ℕ} (c : Fin n → K)
    (F : MvPolynomial (Fin (n + 1)) K) :
    eval (Fin.cons 1 0) (linearChangeFirst c F) = eval (Fin.cons 1 c) F
theorem

aeval_finCons_eq_eval₂_finSuccEquiv

L99 ↗
FieldArithmetic.Chapter06.aeval_finCons_eq_eval₂_finSuccEquiv
Documentation

Evaluation through finSuccEquiv: the first multivariable coordinate becomes the univariate polynomial variable and the remaining coordinates evaluate the coefficients.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem aeval_finCons_eq_eval₂_finSuccEquiv
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x₀ : A) (x : Fin n → A) (F : MvPolynomial (Fin (n + 1)) K) :
    aeval (Fin.cons x₀ x) F =
      Polynomial.eval₂ (aeval x).toRingHom x₀ (finSuccEquiv K n F)
def

linearTailCoordinatesFirst

L114 ↗
FieldArithmetic.Chapter06.linearTailCoordinatesFirst
Documentation

The n tail coordinates after the inverse triangular change.

Source context 5 commands

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

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

linearCoordinatesFirst

L120 ↗
FieldArithmetic.Chapter06.linearCoordinatesFirst
Documentation

The full tuple after the inverse triangular change.

Source context 5 commands

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

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

linearCoordinatesFirst_zero

L126 ↗
FieldArithmetic.Chapter06.linearCoordinatesFirst_zero
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearCoordinatesFirst_zero
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A) :
    linearCoordinatesFirst c x 0 = x 0
theorem

linearCoordinatesFirst_succ

L132 ↗
FieldArithmetic.Chapter06.linearCoordinatesFirst_succ
Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem linearCoordinatesFirst_succ
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A) (i : Fin n) :
    linearCoordinatesFirst c x i.succ =
      x i.succ - algebraMap K A (c i) * x 0
theorem

aeval_linearChangeFirst_linearCoordinates

L142 ↗
FieldArithmetic.Chapter06.aeval_linearChangeFirst_linearCoordinates
Documentation

The triangular substitution evaluated at its inverse coordinate change 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 MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem aeval_linearChangeFirst_linearCoordinates
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A)
    (F : MvPolynomial (Fin (n + 1)) K) :
    aeval (linearCoordinatesFirst c x) (linearChangeFirst c F) = aeval x F
theorem

eval_finCons_one_zero_eq_constantCoeff_coeff

L165 ↗
FieldArithmetic.Chapter06.eval_finCons_one_zero_eq_constantCoeff_coeff
Documentation

For a homogeneous polynomial, evaluation at (1, 0, ..., 0) extracts the constant coefficient of its coefficient of X₀ᵈ.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem eval_finCons_one_zero_eq_constantCoeff_coeff {n d : ℕ}
    {F : MvPolynomial (Fin (n + 1)) K} (hF : F.IsHomogeneous d) :
    eval (Fin.cons 1 0) F =
      MvPolynomial.constantCoeff ((finSuccEquiv K n F).coeff d)
theorem

coeff_finSuccEquiv_linearChangeFirst

L194 ↗
FieldArithmetic.Chapter06.coeff_finSuccEquiv_linearChangeFirst
Documentation

The coefficient of X₀ᵈ after the triangular substitution of a degree-d homogeneous polynomial is the scalar obtained by evaluating it at (1, c₁, ..., cₙ).

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem coeff_finSuccEquiv_linearChangeFirst {n d : ℕ} (c : Fin n → K)
    {F : MvPolynomial (Fin (n + 1)) K} (hF : F.IsHomogeneous d) :
    (finSuccEquiv K n (linearChangeFirst c F)).coeff d =
      C (eval (Fin.cons 1 c) F)
theorem

coeff_finSuccEquiv_eq_zero_of_isHomogeneous_lt

L218 ↗
FieldArithmetic.Chapter06.coeff_finSuccEquiv_eq_zero_of_isHomogeneous_lt
Documentation

A coefficient whose distinguished-variable exponent is larger than the homogeneous degree vanishes.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem coeff_finSuccEquiv_eq_zero_of_isHomogeneous_lt {n i j : ℕ}
    {F : MvPolynomial (Fin (n + 1)) K} (hF : F.IsHomogeneous i) (hij : i < j) :
    (finSuccEquiv K n F).coeff j = 0
theorem

homogeneousComponent_totalDegree_ne_zero

L233 ↗
FieldArithmetic.Chapter06.homogeneousComponent_totalDegree_ne_zero
Documentation

The top homogeneous component of a nonzero polynomial is nonzero.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem homogeneousComponent_totalDegree_ne_zero {σ : Type*}
    {F : MvPolynomial σ K} (hF : F ≠ 0) :
    homogeneousComponent F.totalDegree F ≠ 0
theorem

coeff_finSuccEquiv_linearChangeFirst_eq_top

L251 ↗
FieldArithmetic.Chapter06.coeff_finSuccEquiv_linearChangeFirst_eq_top
Documentation

At the top total degree, the transformed polynomial and the transform of its top homogeneous component have the same X₀ coefficient.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem coeff_finSuccEquiv_linearChangeFirst_eq_top {n : ℕ}
    (c : Fin n → K) (F : MvPolynomial (Fin (n + 1)) K) :
    (finSuccEquiv K n (linearChangeFirst c F)).coeff F.totalDegree =
      (finSuccEquiv K n
        (linearChangeFirst c (homogeneousComponent F.totalDegree F))).coeff F.totalDegree
theorem

coeff_finSuccEquiv_linearChangeFirst_eq_zero_of_totalDegree_lt

L281 ↗
FieldArithmetic.Chapter06.coeff_finSuccEquiv_linearChangeFirst_eq_zero_of_totalDegree_lt
Documentation

Coefficients above total degree remain zero after the linear change.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem coeff_finSuccEquiv_linearChangeFirst_eq_zero_of_totalDegree_lt {n j : ℕ}
    (c : Fin n → K) (F : MvPolynomial (Fin (n + 1)) K) (hj : F.totalDegree < j) :
    (finSuccEquiv K n (linearChangeFirst c F)).coeff j = 0
theorem

exists_linearChangeFirst_coeff_isUnit

L302 ↗
FieldArithmetic.Chapter06.exists_linearChangeFirst_coeff_isUnit
Documentation

Over an infinite field, a nonzero homogeneous polynomial admits a triangular linear change for which its X₀ᵈ coefficient is a unit.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem exists_linearChangeFirst_coeff_isUnit [Infinite K]
    {n d : ℕ} {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F.IsHomogeneous d) (hF₀ : F ≠ 0) :
    ∃ c : Fin n → K,
      IsUnit ((finSuccEquiv K n (linearChangeFirst c F)).coeff d)
theorem

exists_linearChangeFirst_leadingCoeff_isUnit

L317 ↗
FieldArithmetic.Chapter06.exists_linearChangeFirst_leadingCoeff_isUnit
Documentation

Over an infinite field, every nonzero polynomial admits a triangular linear change for which the resulting univariate polynomial in X₀ has unit leading coefficient.

Source context 5 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
variable {K : Type*} [Field K]
Lean source · statement
theorem exists_linearChangeFirst_leadingCoeff_isUnit [Infinite K]
    {n : ℕ} {F : MvPolynomial (Fin (n + 1)) K} (hF : F ≠ 0) :
    ∃ c : Fin n → K,
      IsUnit (finSuccEquiv K n (linearChangeFirst c F)).leadingCoeff

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