RationalKernels.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Rational polynomial kernels and normalization without cancellation

theorem OAI.Nagata.W18.exponent_injective_on_diagonal line 27

Source documentation

On a fixed diagonal α + j α = u, the normal exponent determines α.

theorem exponent_injective_on_diagonal (s : Finset ℕ) (j : ℕ → ℕ) (u : ℕ)
    (hweight : ∀ a ∈ s, a + j a = u) :
    Set.InjOn j (↑s : Set ℕ) := by
…

theorem OAI.Nagata.W18.coefficient_of_injective_monomial_sum line 38

Source documentation

A sum of monomials with distinct exponents retains each selected coefficient.

theorem coefficient_of_injective_monomial_sum {R : Type*} [Semiring R]
    (s : Finset ℕ) (j : ℕ → ℕ) (c : ℕ → R)
    (hinj : Set.InjOn j (↑s : Set ℕ)) (a : ℕ) (ha : a ∈ s) :
    (∑ b ∈ s, Polynomial.monomial (j b) (c b)).coeff (j a) = c a := by
…

theorem OAI.Nagata.W18.injective_monomial_sum_ne_zero line 53

Source documentation

One nonzero coefficient suffices for noncancellation when exponents are distinct.

theorem injective_monomial_sum_ne_zero {R : Type*} [Semiring R]
    (s : Finset ℕ) (j : ℕ → ℕ) (c : ℕ → R)
    (hinj : Set.InjOn j (↑s : Set ℕ))
    (hcoeff : ∃ a ∈ s, c a ≠ 0) :
    (∑ b ∈ s, Polynomial.monomial (j b) (c b)) ≠ 0 := by
…

theorem OAI.Nagata.W18.diagonal_monomial_sum_ne_zero line 67

Source documentation

The exact finite noncancellation step used after choosing the minimum weight.

theorem diagonal_monomial_sum_ne_zero {R : Type*} [Semiring R]
    (s : Finset ℕ) (j : ℕ → ℕ) (c : ℕ → R) (u : ℕ)
    (hweight : ∀ a ∈ s, a + j a = u)
    (hne : s.Nonempty) (hcoeff : ∀ a ∈ s, c a ≠ 0) :
    (∑ b ∈ s, Polynomial.monomial (j b) (c b)) ≠ 0 := by
…

theorem OAI.Nagata.W18.exists_lowest_weight_polynomial line 81

Source documentation

A finite nonzero family has a nonzero lowest-weight polynomial.

The construction also records the inequality needed to make every exponent of s in the divided family nonnegative. This is finite algebra only.

theorem exists_lowest_weight_polynomial {R : Type*} [Semiring R]
    (s : Finset ℕ) (j : ℕ → ℕ) (c : ℕ → R)
    (hne : s.Nonempty) (hcoeff : ∀ a ∈ s, c a ≠ 0) :
    ∃ u : ℕ,
      (∀ a ∈ s, u ≤ a + j a) ∧
      (s.filter (fun a => a + j a = u)).Nonempty ∧
      (∑ b ∈ s.filter (fun a => a + j a = u),
        Polynomial.monomial (j b) (c b)) ≠ 0 := by
…

theorem OAI.Nagata.W18.normalize_parameter_vector line 122

Source documentation

A nonzero polynomial vector has a least parameter degree occurring in any coordinate, even when the index type is not assumed finite.

theorem normalize_parameter_vector {K ι : Type*} [Field K]
    (p : ι → Polynomial K) (hp : p ≠ 0) :
    ∃ n : ℕ, ∃ q : ι → Polynomial K,
      (∀ i, p i = Polynomial.X ^ n * q i) ∧
      ∃ i, (q i).coeff 0 ≠ 0 := by
…

theorem OAI.Nagata.W18.normalize_parameter_kernel line 159

Source documentation

Removing a common parameter power preserves every polynomial matrix kernel equation and leaves a vector whose value at zero is nonzero.

theorem normalize_parameter_kernel {K ι κ : Type*} [Field K] [Fintype ι]
    (A : Matrix κ ι (Polynomial K)) (p : ι → Polynomial K)
    (hp : p ≠ 0) (hAp : A.mulVec p = 0) :
    ∃ n : ℕ, ∃ q : ι → Polynomial K,
      (∀ i, p i = Polynomial.X ^ n * q i) ∧
      (∃ i, (q i).coeff 0 ≠ 0) ∧ A.mulVec q = 0 := by
…

theorem OAI.Nagata.W18.specialization_zero_ne_zero line 176

Source documentation

The nonzero constant coefficient is exactly nonzero specialization at zero.

theorem specialization_zero_ne_zero {K ι : Type*} [Field K]
    (q : ι → Polynomial K) (hq : ∃ i, (q i).coeff 0 ≠ 0) :
    (fun i => (q i).eval 0) ≠ 0 := by
…

theorem OAI.Nagata.W18.clear_finite_denominators line 202

Source documentation

A finite family in a fraction field has a common nonzero denominator.

theorem clear_finite_denominators {R : Type*} [CommRing R] [IsDomain R]
    {ι : Type*} [Finite ι] (v : ι → FractionRing R) :
    ∃ d : R, d ≠ 0 ∧ ∃ p : ι → R,
      ∀ i, algebraMap R (FractionRing R) (p i) =
        algebraMap R (FractionRing R) d * v i := by
…

theorem OAI.Nagata.W18.map_scalar_identity line 216

Source documentation

Mapping a scalar identity matrix maps only its scalar.

theorem map_scalar_identity {R K : Type*} [CommRing R] [CommRing K]
    {ι : Type*} [DecidableEq ι] (f : R →+* K) (d : R) :
    (d • (1 : Matrix ι ι R)).map f = f d • (1 : Matrix ι ι K) := by
…

theorem OAI.Nagata.W18.polynomial_scaled_left_inverse line 224

Source documentation

An injective fraction-field matrix has a polynomial left inverse up to a single nonzero scalar. This is an actual denominator-cleared identity.

theorem polynomial_scaled_left_inverse {R : Type*} [CommRing R] [IsDomain R]
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (A : Matrix κ ι R)
    (hinj : Function.Injective (A.map (algebraMap R (FractionRing R))).mulVec) :
    ∃ d : R, d ≠ 0 ∧ ∃ D : Matrix ι κ R, D * A = d • (1 : Matrix ι ι R) := by
…

theorem OAI.Nagata.W18.clear_fraction_kernel line 249

Source documentation

Clearing a nonzero fraction-field kernel preserves nonzeroness and produces an actual kernel vector over the original domain.

theorem clear_fraction_kernel {R : Type*} [CommRing R] [IsDomain R]
    {ι κ : Type*} [Fintype ι] (A : Matrix κ ι R)
    (v : ι → FractionRing R) (hv : v ≠ 0)
    (hAv : (A.map (algebraMap R (FractionRing R))).mulVec v = 0) :
    ∃ p : ι → R, p ≠ 0 ∧ A.mulVec p = 0 := by
…

theorem OAI.Nagata.W18.specialize_polynomial_kernel line 278

Source documentation

Polynomial kernel identities specialize at every parameter value.

theorem specialize_polynomial_kernel {K ι κ : Type*} [Field K] [Fintype ι]
    (A : Matrix κ ι (Polynomial K)) (p : ι → Polynomial K)
    (hp : A.mulVec p = 0) (s : K) :
    (A.map (Polynomial.evalRingHom s)).mulVec (fun i => (p i).eval s) = 0 := by
…

theorem OAI.Nagata.W18.exists_parameter_avoiding_roots line 290

Source documentation

A polynomial nonzero scalar cannot vanish at every parameter outside a finite exceptional set.

theorem exists_parameter_avoiding_roots {K : Type*} [Field K] [Infinite K]
    (E : Finset K) (d : Polynomial K) (hd : d ≠ 0) :
    ∃ s : K, s ∉ E ∧ d.eval s ≠ 0 := by
…

theorem OAI.Nagata.W18.rational_kernel_of_general_specialized_kernel line 297

Source documentation

General specialized kernels force a kernel over the rational function field.

theorem rational_kernel_of_general_specialized_kernel
    {K : Type*} [Field K] [Infinite K]
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (A : Matrix κ ι (Polynomial K)) (E : Finset K)
    (hkernel : ∀ s ∉ E, ∃ v : ι → K, v ≠ 0 ∧
      (A.map (Polynomial.evalRingHom s)).mulVec v = 0) :
    ∃ v : ι → FractionRing (Polynomial K), v ≠ 0 ∧
      (A.map (algebraMap (Polynomial K) (FractionRing (Polynomial K)))).mulVec v = 0 := by
…

theorem OAI.Nagata.W18.polynomial_kernel_of_general_specialized_kernel line 340

Source documentation

The complete algebraic family step: kernels at all general parameters supply a nonzero polynomial family of coefficient vectors in the kernel.

theorem polynomial_kernel_of_general_specialized_kernel
    {K : Type*} [Field K] [Infinite K]
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (A : Matrix κ ι (Polynomial K)) (E : Finset K)
    (hkernel : ∀ s ∉ E, ∃ v : ι → K, v ≠ 0 ∧
      (A.map (Polynomial.evalRingHom s)).mulVec v = 0) :
    ∃ p : ι → Polynomial K, p ≠ 0 ∧ A.mulVec p = 0 := by
…

theorem OAI.Nagata.W18.normalized_kernel_of_general_specialized_kernel line 361

Source documentation

The manuscript's algebraic family conclusion, including nonzero constant coefficient, follows from nonzero kernels at all general parameters.

theorem normalized_kernel_of_general_specialized_kernel
    {K : Type*} [Field K] [Infinite K]
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (A : Matrix κ ι (Polynomial K)) (E : Finset K)
    (hkernel : ∀ s ∉ E, ∃ v : ι → K, v ≠ 0 ∧
      (A.map (Polynomial.evalRingHom s)).mulVec v = 0) :
    ∃ q : ι → Polynomial K, (∃ i, (q i).coeff 0 ≠ 0) ∧ A.mulVec q = 0 := by
…