PolynomialJets.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Two-generator ideal powers, monomial membership, and polynomial jet ideals

abbrev OAI.Nagata.Workers.W30.JetIndex line 25
Source documentation
A dependent finite type encoding the manuscript's row set without duplicates. The sigma order is (b,ell); jetIndexPair restores the manuscript order.
```
abbrev JetIndex (q m : ℕ) := Σ b : Fin m, Fin (q * (m - b.val))
```
def OAI.Nagata.Workers.W30.jetIndexPair line 27
theorem OAI.Nagata.Workers.W30.jetIndexPair_bounds line 30
def OAI.Nagata.Workers.W30.jetIndexEquivPairs line 35
Source documentation
Explicit equivalence with the subset of natural-number pairs written in §03.
```
def jetIndexEquivPairs (q m : ℕ) :
    JetIndex q m ≃ {p : ℕ × ℕ // p.2 < m ∧ p.1 < q * (m - p.2)} where
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex
theorem OAI.Nagata.Workers.W30.card_jetIndex_sum line 43
Source documentation
The row count as the sum of the widths of its m horizontal slices.
```
theorem card_jetIndex_sum (q m : ℕ) :
    Fintype.card (JetIndex q m) = ∑ b ∈ Finset.range m, q * (m - b) := by
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex
theorem OAI.Nagata.Workers.W30.row_sum_succ line 48
theorem OAI.Nagata.Workers.W30.card_jetIndex_mul_two line 55
Source documentation
An integral form of the cardinality formula, avoiding division.
```
theorem card_jetIndex_mul_two (q m : ℕ) :
    Fintype.card (JetIndex q m) * 2 = q * m * (m + 1) := by
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex
theorem OAI.Nagata.Workers.W30.card_jetIndex line 66
Source documentation
The exact cardinality stated after the collision lemma.
```
theorem card_jetIndex (q m : ℕ) :
    Fintype.card (JetIndex q m) = q * m * (m + 1) / 2 := by
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex

theorem OAI.Nagata.Workers.W30.mem_monomial_span_iff line 90

Source documentation

A polynomial lies in a monomial ideal iff each support exponent dominates one of the generating exponents.

theorem mem_monomial_span_iff {p : MvPolynomial σ R} {s : Set (σ →₀ ℕ)} :
    p ∈ Ideal.span ((fun a => monomial a (1 : R)) '' s) ↔
      ∀ a ∈ p.support, ∃ g ∈ s, g ≤ a := by
…

def OAI.Nagata.Workers.W30.GeneratorDivides line 135
Source documentation
An exponent pair divisible by one of the listed monomial generators.
```
def GeneratorDivides (q m ell b : Nat) : Prop :=
…
```
theorem OAI.Nagata.Workers.W30.generatorDivides_iff line 139
Source documentation
A generator divides precisely when the exponent escapes the finite jet region.
```
theorem generatorDivides_iff {q m ell b : Nat} :
    GeneratorDivides q m ell b ↔ m ≤ b ∨ q * (m - b) ≤ ell := by
…
```
Mentions: OAI.Nagata.Workers.W30.GeneratorDivides
theorem OAI.Nagata.Workers.W30.not_generatorDivides_iff line 154
Source documentation
The complement of the monomial-generator divisibility region is exactly I={(ell,b):b<m,ell<q*(m-b)} from the manuscript.
```
theorem not_generatorDivides_iff {q m ell b : Nat} :
    ¬ GeneratorDivides q m ell b ↔ b < m ∧ ell < q * (m - b) := by
…
```
Mentions: OAI.Nagata.Workers.W30.GeneratorDivides
theorem OAI.Nagata.Workers.W30.GeneratorDivides.add line 161
Source documentation
The divisibility region is closed under multiplication by any monomial, expressed as addition of nonnegative exponents.
```
theorem GeneratorDivides.add {q m ell b c d : Nat}
    (h : GeneratorDivides q m ell b) : GeneratorDivides q m (ell + c) (b + d) := by
…
```
Mentions: OAI.Nagata.Workers.W30.GeneratorDivides
theorem OAI.Nagata.Workers.W30.pair_set_pow line 181
Source documentation
The products of m choices from {x,y} are precisely x^(m-k)*y^k.
```
theorem pair_set_pow (x y : A) (m : ℕ) :
    ({x,y} : Set A) ^ m = {z | ∃ k ≤ m, z = x ^ (m - k) * y ^ k} := by
…
```

theorem OAI.Nagata.Workers.W30.pair_ideal_pow line 212

Source documentation

Exact generating set for the genuine ideal power.

theorem pair_ideal_pow (x y : A) (m : ℕ) :
    (Ideal.span {x,y}) ^ m =
      Ideal.span {z | ∃ k ≤ m, z = x ^ (m - k) * y ^ k} := by
…

def OAI.Nagata.Workers.W30.exponentPair line 226
Source documentation
Bivariate exponent vector in coordinate order (X,Y).
```
noncomputable def exponentPair (ell b : ℕ) : Fin 2 →₀ ℕ :=
…
```
theorem OAI.Nagata.Workers.W30.exponentPair_zero line 229
theorem OAI.Nagata.Workers.W30.exponentPair_one line 232
lemma OAI.Nagata.Workers.W30.exponentPair_eta line 235
lemma OAI.Nagata.Workers.W30.exponentPair_le_iff line 243
lemma OAI.Nagata.Workers.W30.exponentPair_injective line 255
def OAI.Nagata.Workers.W30.jetExponent line 261
theorem OAI.Nagata.Workers.W30.jetIndexPair_injective line 264
theorem OAI.Nagata.Workers.W30.jetExponent_injective line 270
theorem OAI.Nagata.Workers.W30.jetExponent_inj line 276
def OAI.Nagata.Workers.W30.jetCoeffMap line 297
Source documentation
Extract the coefficients at the finite collision jet indices.
```
noncomputable def jetCoeffMap :
    MvPolynomial (Fin 2) R →ₗ[R] (JetIndex q m → R) :=
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex
theorem OAI.Nagata.Workers.W30.jetCoeffMap_apply line 301
def OAI.Nagata.Workers.W30.jetPolynomial line 305
Source documentation
The polynomial with exactly the prescribed finite jet coefficients.
```
noncomputable def jetPolynomial (v : JetIndex q m → R) : MvPolynomial (Fin 2) R :=
…
```
Mentions: OAI.Nagata.Workers.W30.JetIndex
theorem OAI.Nagata.Workers.W30.jetCoeffMap_jetPolynomial line 308
theorem OAI.Nagata.Workers.W30.jetCoeffMap_surjective line 315
Source documentation
Coefficient projection onto the prescribed finite jet indices is surjective.
```
theorem jetCoeffMap_surjective : Function.Surjective (jetCoeffMap R q m) := by
…
```
Mentions: OAI.Nagata.Workers.W30.jetCoeffMap
abbrev OAI.Nagata.Workers.W30.Bivariate line 333
def OAI.Nagata.Workers.W30.collisionIdeal line 336
Source documentation
(X^q,Y)^m in the genuine bivariate polynomial ring.
```
noncomputable def collisionIdeal (R : Type*) [CommRing R] (q m : ℕ) : Ideal (Bivariate R) :=
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate
lemma OAI.Nagata.Workers.W30.monomial_exponentPair line 339
def OAI.Nagata.Workers.W30.collisionGenerators line 344
Source documentation
Exact set of the exponent vectors of the standard generators of (X^q,Y)^m.
```
def collisionGenerators (q m : ℕ) : Set (Fin 2 →₀ ℕ) :=
…
```
theorem OAI.Nagata.Workers.W30.collisionIdeal_eq_monomial_span line 348
Source documentation
The ordinary power ideal is exactly the monomial ideal with these generators.
```
theorem collisionIdeal_eq_monomial_span (q m : ℕ) :
    collisionIdeal R q m =
      Ideal.span ((fun a => monomial a (1 : R)) '' collisionGenerators q m) := by
…
```
Mentions: OAI.Nagata.Workers.W30.collisionIdeal, OAI.Nagata.Workers.W30.collisionGenerators
lemma OAI.Nagata.Workers.W30.exists_collisionGenerator_le_iff line 361
theorem OAI.Nagata.Workers.W30.mem_collisionIdeal_iff_support line 370
Source documentation
Membership in the genuine ideal power is the support divisibility criterion.
```
theorem mem_collisionIdeal_iff_support (q m : ℕ) (p : Bivariate R) :
    p ∈ collisionIdeal R q m ↔
      ∀ a ∈ p.support, GeneratorDivides q m (a 0) (a 1) := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.collisionIdeal, OAI.Nagata.Workers.W30.GeneratorDivides
theorem OAI.Nagata.Workers.W30.mem_collisionIdeal_iff_coefficients line 378
Source documentation
The exact coefficient-vanishing characterization of (X^q,Y)^m. No positive-parameter assumption is needed, including the zero ideal-power case.
```
theorem mem_collisionIdeal_iff_coefficients (q m : ℕ) (p : Bivariate R) :
    p ∈ collisionIdeal R q m ↔
      ∀ b < m, ∀ ell < q * (m-b), p.coeff (exponentPair ell b) = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.collisionIdeal, OAI.Nagata.Workers.W30.exponentPair
theorem OAI.Nagata.Workers.W30.mem_collisionIdeal_iff_jetCoeffMap line 395
Source documentation
Membership is equivalent to vanishing of the actual finite jet coefficient map.
```
theorem mem_collisionIdeal_iff_jetCoeffMap (q m : ℕ) (p : Bivariate R) :
    p ∈ collisionIdeal R q m ↔ jetCoeffMap R q m p = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.collisionIdeal, OAI.Nagata.Workers.W30.jetCoeffMap
lemma OAI.Nagata.Workers.W30.range_X_fin_two line 420
theorem OAI.Nagata.Workers.W30.mem_originIdeal_pow_iff line 436
Source documentation
Membership in the ordinary origin maximal ideal to power m is exactly vanishing of every coefficient of total degree less than m.
```
theorem mem_originIdeal_pow_iff (m : ℕ) (p : Bivariate R) :
    p ∈ (Ideal.span (Set.range (X : Fin 2 → Bivariate R))) ^ m ↔
      ∀ ell b : ℕ, ell + b < m → p.coeff (exponentPair ell b) = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W30.Bivariate, OAI.Nagata.Workers.W30.exponentPair