HomogeneousFamilies.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Polynomial families, homogeneous lifts, and parameter transposition; Factored homogeneous families in affine charts

def OAI.Nagata.Workers.W17.HomogeneousPlaneFamily line 31
Source documentation
Genuine one-parameter families of homogeneous plane forms.
```
def HomogeneousPlaneFamily (K : Type*) [CommRing K] (d : Nat) :=
…
```

theorem OAI.Nagata.Workers.W17.homogeneous_factor_degree line 39

Source documentation

Dividing a nonzero homogeneous polynomial by a homogeneous factor produces a homogeneous quotient of the degree difference.

theorem homogeneous_factor_degree {P Q : MvPolynomial σ K} {k d : Nat}
    (hP : P.IsHomogeneous k) (hPQ : (P * Q).IsHomogeneous d)
    (hne : P * Q ≠ 0) :
    k ≤ d ∧ Q.IsHomogeneous (d - k) := by
…

theorem OAI.Nagata.Workers.W17.homogeneous_power_remainder line 62

Source documentation

The remainder lift in S=G^j*T has degree d-kj and kj≤d.

theorem homogeneous_power_remainder {S G T : MvPolynomial σ K} {d k j : Nat}
    (hS : S.IsHomogeneous d) (hG : G.IsHomogeneous k)
    (hne : S ≠ 0) (hfactor : S = G ^ j * T) :
    k * j ≤ d ∧ T.IsHomogeneous (d - k * j) := by
…

theorem OAI.Nagata.Workers.W17.homogeneous_power_exponent_bound line 71

Source documentation

The normal exponent is bounded by floor(d/k), with k positive.

theorem homogeneous_power_exponent_bound {S G T : MvPolynomial σ K} {d k j : Nat}
    (hS : S.IsHomogeneous d) (hG : G.IsHomogeneous k)
    (hne : S ≠ 0) (hfactor : S = G ^ j * T) (hk : 0 < k) :
    j ≤ d / k := by
…

theorem OAI.Nagata.Workers.W17.positive_homogeneous_not_isUnit line 88
Source documentation
Positive-degree homogeneous equations are nonunits in the genuine polynomial ring, including the zero equation.
```
theorem positive_homogeneous_not_isUnit {K σ : Type*} [CommRing K] [Nontrivial K]
    {G : MvPolynomial σ K} {k : ℕ} (hG : G.IsHomogeneous k) (hk : 0 < k) :
    ¬IsUnit G := by
…
```

theorem OAI.Nagata.Workers.W17.exists_factored_coefficients line 121

Source documentation

Extract maximal G-powers from all nonzero coefficients of an actual polynomial. Values at zero coefficients are normalized to exponent zero.

theorem exists_factored_coefficients (S : Polynomial A) (G : A)
    (hG : ¬IsUnit G) :
    ∃ (j : Nat → Nat) (T : Nat → A),
      (∀ α, S.coeff α = G ^ j α * T α) ∧
      (∀ α, S.coeff α ≠ 0 → ¬G ∣ T α) := by
…

theorem OAI.Nagata.Workers.W17.exists_nonzero_normal_initial line 139

Source documentation

A nonzero family has a nonzero lowest normal polynomial after reduction modulo G. All factorization and minimum-weight data are constructed here.

theorem exists_nonzero_normal_initial
    (S : Polynomial A) (G : A) (hS : S ≠ 0) (hG : ¬IsUnit G) :
    ∃ (j : Nat → Nat) (T : Nat → A) (u : Nat),
      (∀ α, S.coeff α = G ^ j α * T α) ∧
      (∀ α ∈ S.support, ¬G ∣ T α) ∧
      (∀ α ∈ S.support, u ≤ α + j α) ∧
      (S.support.filter (fun α => α + j α = u)).Nonempty ∧
      (∑ α ∈ S.support.filter (fun α => α + j α = u),
        Polynomial.monomial (j α)
          (Ideal.Quotient.mk (Ideal.span ({G} : Set A)) (T α))) ≠ 0 := by
…

theorem OAI.Nagata.Workers.W17.initial_weight_bound_from_constant line 166
Source documentation
Normalization S(0)≠0 bounds the selected weight by the extracted G-exponent of the zeroth coefficient.
```
theorem initial_weight_bound_from_constant (S : Polynomial A)
    (j : Nat → Nat) (u : Nat) (hzero : S.coeff 0 ≠ 0)
    (hmin : ∀ α ∈ S.support, u ≤ α + j α) : u ≤ j 0 := by
…
```
def OAI.Nagata.Workers.W17.liftedNormalPolynomial line 192

theorem OAI.Nagata.Workers.W17.coeff_liftedNormalPolynomial line 197

Source documentation

Grouping by normal exponent retains actual coefficient-ring elements.

theorem coeff_liftedNormalPolynomial
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → A) (n : Nat) :
    (liftedNormalPolynomial indices j T).coeff n =
      ∑ α ∈ indices.filter (fun α => j α = n), T α := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.map_liftedNormalPolynomial line 206

Source documentation

Mapping the actual lifted polynomial gives the literal quotient sum.

theorem map_liftedNormalPolynomial {B : Type*} [CommRing B]
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → A) (f : A →+* B) :
    (liftedNormalPolynomial indices j T).map f =
      ∑ α ∈ indices, Polynomial.monomial (j α) (f (T α)) := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.quotient_liftedNormalPolynomial_ne_zero line 214

Source documentation

The quotient of the lifted polynomial is nonzero; no global section or reduction-to-lines property is assumed.

theorem quotient_liftedNormalPolynomial_ne_zero
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → A) (G : A) (u : Nat)
    (hne : indices.Nonempty) (hweight : ∀ α ∈ indices, α + j α = u)
    (hnot : ∀ α ∈ indices, ¬G ∣ T α) :
    (liftedNormalPolynomial indices j T).map
      (Ideal.Quotient.mk (Ideal.span ({G} : Set A))) ≠ 0 := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.coeff_liftedNormalPolynomial_eq_zero_above line 225

Source documentation

A bound for selected exponents is a bound for every nonzero coefficient.

theorem coeff_liftedNormalPolynomial_eq_zero_above
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → A) (bound n : Nat)
    (hbound : ∀ α ∈ indices, j α ≤ bound) (hn : bound < n) :
    (liftedNormalPolynomial indices j T).coeff n = 0 := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.natDegree_liftedNormalPolynomial_le line 238

Source documentation

The genuine lifted polynomial has bounded normal-variable degree.

theorem natDegree_liftedNormalPolynomial_le
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → A) (bound : Nat)
    (hbound : ∀ α ∈ indices, j α ≤ bound) :
    (liftedNormalPolynomial indices j T).natDegree ≤ bound := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

def OAI.Nagata.Workers.W17.indexedPlaneFamily line 263
theorem OAI.Nagata.Workers.W17.coeff_indexedPlaneFamily line 268
theorem OAI.Nagata.Workers.W17.monomial_coeff_indexedPlaneFamily line 279
theorem OAI.Nagata.Workers.W17.indexedPlaneFamily_homogeneous line 293
theorem OAI.Nagata.Workers.W17.indexedPlaneFamily_constant_ne_zero line 301
theorem OAI.Nagata.Workers.W17.eval_indexedPlaneFamily line 311

theorem OAI.Nagata.Workers.W17.eval_indexedPlaneFamily_eq_coordinates_symm line 324

Source documentation

The specialization is the exact form used by the finite jet matrix.

theorem eval_indexedPlaneFamily_eq_coordinates_symm (d : Nat)
    (q : HomogeneousMonomial d → Polynomial K) (s : K) :
    (indexedPlaneFamily d q).eval (MvPolynomial.C s) =
      ((homogeneousCoordinates d).symm (fun ν => (q ν).eval s)).val := by
…

Mentions: OAI.Nagata.Workers.W17.indexedPlaneFamily

theorem OAI.Nagata.Workers.W17.exists_degree_bounded_plane_initial line 376

Source documentation

All algebraic initial-form data, including actual homogeneous lifts and floor(d/k) bounds, are constructed from a genuine polynomial family.

theorem exists_degree_bounded_plane_initial
    (S : Polynomial (MvPolynomial (Fin 3) K))
    (G : MvPolynomial (Fin 3) K) (d k : Nat)
    (hcoeff : ∀ α, (S.coeff α).IsHomogeneous d)
    (hG : G.IsHomogeneous k) (hunit : ¬IsUnit G) (hk : 0 < k)
    (hzero : S.coeff 0 ≠ 0) :
    ∃ (j : Nat → Nat) (T : Nat → MvPolynomial (Fin 3) K) (u : Nat),
      (∀ α, S.coeff α = G ^ j α * T α) ∧
      (∀ α ∈ S.support, ¬G ∣ T α) ∧
      (∀ α ∈ S.support, j α ≤ d / k ∧ (T α).IsHomogeneous (d - k * j α)) ∧
      (∀ α ∈ S.support, u ≤ α + j α) ∧
      u ≤ d / k ∧
…

theorem OAI.Nagata.Workers.W17.homogeneous_coeff_liftedNormalPolynomial line 425

Source documentation

Actual grouped plane coefficients have exactly the manuscript's degree.

theorem homogeneous_coeff_liftedNormalPolynomial
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → MvPolynomial σ K)
    (d k : Nat) (hT : ∀ α ∈ indices, (T α).IsHomogeneous (d - k * j α))
    (n : Nat) :
    ((liftedNormalPolynomial indices j T).coeff n).IsHomogeneous (d - k * n) := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.nonzero_coeff_liftedNormalPolynomial_bound line 438

Source documentation

Every nonzero coefficient has an exponent within the selected degree bound.

theorem nonzero_coeff_liftedNormalPolynomial_bound
    (indices : Finset Nat) (j : Nat → Nat) (T : Nat → MvPolynomial σ K)
    (bound n : Nat) (hbound : ∀ α ∈ indices, j α ≤ bound)
    (hne : (liftedNormalPolynomial indices j T).coeff n ≠ 0) : n ≤ bound := by
…

Mentions: OAI.Nagata.Workers.W17.liftedNormalPolynomial

theorem OAI.Nagata.Workers.W17.directChart_factored_family line 458

Source documentation

Dehomogenizing a factored homogeneous family yields exactly the finite G-adic polynomial family consumed by analytic normal specialization.

theorem directChart_factored_family
    (S : Polynomial (MvPolynomial (Fin 3) ℂ))
    (G : MvPolynomial (Fin 3) ℂ) (j : ℕ → ℕ)
    (T : ℕ → MvPolynomial (Fin 3) ℂ)
    (hfactor : ∀ α, S.coeff α = G ^ j α * T α)
    (c : Fin 3) (s : ℂ) :
    Nagata.W27.directChartHom c (S.eval (MvPolynomial.C s)) =
      Nagata.Workers.W28.factoredPlaneFamily S.support j
        (fun α => Nagata.W27.directChartHom c (T α))
        (Nagata.W27.directChartHom c G) s := by
…

Mentions: OAI.Nagata.W27.directChartHom, OAI.Nagata.Workers.W28.factoredPlaneFamily