Forms.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous polynomial forms and dehomogenization

abbrev OAI.Nagata.W16.PlanePolynomial line 26
Also declared: ComparatorChallenges/Nagata.lean:188 (same declaration text).

theorem OAI.Nagata.W16.homogeneous_eval₂_scale line 30

Source documentation

Homogeneous scaling after an arbitrary coefficient-ring map. This version also applies to evaluations in localizations of affine coordinate rings.

theorem homogeneous_eval₂_scale {σ K R : Type*} [CommSemiring K] [CommSemiring R]
    {F : MvPolynomial σ K} {d : ℕ} (hF : F.IsHomogeneous d)
    (k : K →+* R) (x : σ → R) (a : R) :
    MvPolynomial.eval₂ k (fun i => a * x i) F =
      a ^ d * MvPolynomial.eval₂ k x F := by
…

theorem OAI.Nagata.W16.homogeneous_eval_scale line 45
Source documentation
Homogeneity gives the representative scaling law needed to descend a homogeneous zero locus from nonzero vectors to projective points.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:195 (different declaration text). Qualify references as OAI.Nagata.W16.homogeneous_eval_scale@path.
```
theorem homogeneous_eval_scale {σ K : Type*} [CommSemiring K]
    {F : MvPolynomial σ K} {d : ℕ} (hF : F.IsHomogeneous d)
    (x : σ → K) (a : K) :
    MvPolynomial.eval (fun i => a * x i) F = a ^ d * MvPolynomial.eval x F := by
…
```

theorem OAI.Nagata.W16.homogeneous_eval_scale_eq_zero_iff line 59

Source documentation

Vanishing of a homogeneous equation is invariant under nonzero rescaling of its representative.

theorem homogeneous_eval_scale_eq_zero_iff {σ K : Type*} [CommRing K]
    [IsDomain K] {F : MvPolynomial σ K} {d : ℕ}
    (hF : F.IsHomogeneous d) (x : σ → K) {a : K} (ha : a ≠ 0) :
    MvPolynomial.eval (fun i => a * x i) F = 0 ↔ MvPolynomial.eval x F = 0 := by
…

structure OAI.Nagata.W16.NonzeroHomogeneousForm line 68
Source documentation
A nonzero degree-d homogeneous ternary complex polynomial. Nonreduced and reducible equations are allowed.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:190 (different declaration text). Qualify references as OAI.Nagata.W16.NonzeroHomogeneousForm@path.
```
structure NonzeroHomogeneousForm (d : ℕ) where
…
```
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.totalDegree_eq line 75
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.exists_eval_ne_zero line 80
Source documentation
A nonzero equation over ℂ cannot vanish at every affine vector.
```
theorem exists_eval_ne_zero {d : ℕ} (F : NonzeroHomogeneousForm d) :
    ∃ x : Fin 3 → ℂ, MvPolynomial.eval x F.polynomial ≠ 0 := by
…
```
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.eval_zero_of_degree_pos line 91
Source documentation
Positive-degree homogeneous equations vanish at the zero vector.
```
theorem eval_zero_of_degree_pos {d : ℕ} (F : NonzeroHomogeneousForm d)
    (hd : 0 < d) : MvPolynomial.eval (0 : Fin 3 → ℂ) F.polynomial = 0 := by
…
```
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.exists_nonzero_vector_eval_ne_zero line 98
Source documentation
A positive-degree nonzero equation has a nonzero vector outside its zero locus, providing the representative needed for projective properness.
```
theorem exists_nonzero_vector_eval_ne_zero {d : ℕ}
    (F : NonzeroHomogeneousForm d) (hd : 0 < d) :
    ∃ x : Fin 3 → ℂ, x ≠ 0 ∧ MvPolynomial.eval x F.polynomial ≠ 0 := by
…
```
def OAI.Nagata.W16.NonzeroHomogeneousForm.mul line 108
Source documentation
Multiplying equations adds degrees and preserves nonzeroness.
```
def mul {d e : ℕ} (F : NonzeroHomogeneousForm d)
    (G : NonzeroHomogeneousForm e) : NonzeroHomogeneousForm (d + e) where
…
```
def OAI.Nagata.W16.NonzeroHomogeneousForm.pow line 115
Source documentation
Taking a power multiplies the degree, including the zeroth power.
```
def pow {d : ℕ} (F : NonzeroHomogeneousForm d) (N : ℕ) :
    NonzeroHomogeneousForm (d * N) where
…
```
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.mul_totalDegree line 121
theorem OAI.Nagata.W16.NonzeroHomogeneousForm.pow_totalDegree line 126

theorem OAI.Nagata.W16.finite_product_forms line 136

Source documentation

A finite product of nonzero forms has the sum of the prescribed degrees. The finite set may be empty, in which case the product is the constant one.

theorem finite_product_forms {ι : Type*} (s : Finset ι)
    (F : ι → PlanePolynomial) (d : ι → ℕ)
    (hhom : ∀ i ∈ s, (F i).IsHomogeneous (d i))
    (hne : ∀ i ∈ s, F i ≠ 0) :
    (∏ i ∈ s, F i) ≠ 0 ∧
      (∏ i ∈ s, F i).IsHomogeneous (∑ i ∈ s, d i) ∧
      (∏ i ∈ s, F i).totalDegree = ∑ i ∈ s, d i := by
…

Mentions: OAI.Nagata.W16.PlanePolynomial

theorem OAI.Nagata.W16.finite_product_equal_degree line 149

Source documentation

Equal-degree product formula needed for the permutation product.

theorem finite_product_equal_degree {ι : Type*} (s : Finset ι)
    (F : ι → PlanePolynomial) (d : ℕ)
    (hhom : ∀ i ∈ s, (F i).IsHomogeneous d)
    (hne : ∀ i ∈ s, F i ≠ 0) :
    (∏ i ∈ s, F i) ≠ 0 ∧
      (∏ i ∈ s, F i).totalDegree = s.card * d := by
…

Mentions: OAI.Nagata.W16.PlanePolynomial

theorem OAI.Nagata.W16.permutation_product_degree line 161
Source documentation
The permutation product in §1 is a nonzero equation of degree r! * d. Each factor can be chosen independently; no symmetry of its coefficients is required.
```
theorem permutation_product_degree (r d : ℕ)
    (F : Equiv.Perm (Fin r) → PlanePolynomial)
    (hhom : ∀ σ, (F σ).IsHomogeneous d) (hne : ∀ σ, F σ ≠ 0) :
    (∏ σ, F σ) ≠ 0 ∧
      (∏ σ, F σ).totalDegree = Nat.factorial r * d := by
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial
def OAI.Nagata.W16.binaryAffine line 186
theorem OAI.Nagata.W16.binaryAffine_eq_sum line 189
theorem OAI.Nagata.W16.binaryAffine_eval line 197
theorem OAI.Nagata.W16.binaryAffine_normalized line 202
theorem OAI.Nagata.W16.binaryAffine_eq_zero_imp line 213
theorem OAI.Nagata.W16.binaryAffine_ne_zero line 228
theorem OAI.Nagata.W16.binaryAffine_natDegree_le line 233
theorem OAI.Nagata.W16.eval_dehomogenize line 265
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:211 (different declaration text). Qualify references as OAI.Nagata.W16.eval_dehomogenize@path.
theorem OAI.Nagata.W16.eval_dehomogenize_normalized line 278
Source documentation
The affine chart evaluation formula has its exact homogeneous scaling factor, with no division performed at a zero chart coordinate.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:224 (different declaration text). Qualify references as OAI.Nagata.W16.eval_dehomogenize_normalized@path.
```
theorem eval_dehomogenize_normalized {d : ℕ} {F : PlanePolynomial}
    (hF : F.IsHomogeneous d) (c : Fin 3) (x : Fin 3 → ℂ) (hc : x c ≠ 0) :
    MvPolynomial.eval (fun j : ChartVariables c => x j.val / x c)
        (dehomogenize c F) =
      (x c)⁻¹ ^ d * MvPolynomial.eval x F := by
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial
theorem OAI.Nagata.W16.eval_eq_zero_of_dehomogenize_eq_zero line 296
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:244 (different declaration text). Qualify references as OAI.Nagata.W16.eval_eq_zero_of_dehomogenize_eq_zero@path.
theorem OAI.Nagata.W16.eq_zero_of_dehomogenize_eq_zero line 307
Source documentation
A homogeneous equation whose restriction to one affine chart is zero is the zero polynomial. Multiplication by the distinguished coordinate handles vectors on the omitted hyperplane.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:255 (different declaration text). Qualify references as OAI.Nagata.W16.eq_zero_of_dehomogenize_eq_zero@path.
```
theorem eq_zero_of_dehomogenize_eq_zero {d : ℕ} {F : PlanePolynomial}
    (hF : F.IsHomogeneous d) (c : Fin 3) (hchart : dehomogenize c F = 0) : F = 0 := by
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial
theorem OAI.Nagata.W16.dehomogenize_ne_zero line 318
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:268 (different declaration text). Qualify references as OAI.Nagata.W16.dehomogenize_ne_zero@path.

theorem OAI.Nagata.W16.dehomogenize_injective_fixed_degree line 325

Source documentation

Affine restriction is injective on each fixed homogeneous degree.

theorem dehomogenize_injective_fixed_degree {d : ℕ} {F G : PlanePolynomial}
    (hF : F.IsHomogeneous d) (hG : G.IsHomogeneous d) (c : Fin 3)
    (hchart : dehomogenize c F = dehomogenize c G) : F = G := by
…

Mentions: OAI.Nagata.W16.PlanePolynomial

def OAI.Nagata.W16.blockDehomogenize line 357

Source documentation

Restrict every point block to [1 : z₀ : z₁].

def blockDehomogenize {r : ℕ} (F : MultihomogeneousEquation r) :
    MvPolynomial (Fin r × Fin 2) ℂ :=
…

theorem OAI.Nagata.W16.multihomogeneous_eval_scale line 365

Source documentation

Independent rescaling of the point blocks gives the multidegree factor.

theorem multihomogeneous_eval_scale {r : ℕ} (F : MultihomogeneousEquation r)
    (x : Fin r × Fin 3 → ℂ) (a : Fin r → ℂ) :
    MvPolynomial.eval (fun ij => a ij.1 * x ij) F.polynomial =
      (∏ i, a i ^ F.multidegree i) * MvPolynomial.eval x F.polynomial := by
…

theorem OAI.Nagata.W16.eval_blockDehomogenize line 384
theorem OAI.Nagata.W16.eval_blockDehomogenize_normalized line 397
theorem OAI.Nagata.W16.eq_zero_of_blockDehomogenize_eq_zero line 416
Source documentation
A zero simultaneous affine restriction forces the multihomogeneous polynomial itself to vanish.
```
theorem eq_zero_of_blockDehomogenize_eq_zero {r : ℕ}
    (F : MultihomogeneousEquation r) (hchart : blockDehomogenize F = 0) :
    F.polynomial = 0 := by
…
```
Mentions: OAI.Nagata.W16.blockDehomogenize
theorem OAI.Nagata.W16.blockDehomogenize_ne_zero line 448
Source documentation
Every nonzero multihomogeneous equation stays nonzero on the standard simultaneous affine chart.
```
theorem blockDehomogenize_ne_zero {r : ℕ} (F : MultihomogeneousEquation r)
    (hne : F.polynomial ≠ 0) : blockDehomogenize F ≠ 0 := by
…
```
Mentions: OAI.Nagata.W16.blockDehomogenize