MovingConfigurations.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Polynomial motion of tuples, exceptional parameters, and gradients

theorem OAI.Nagata.Workers.W14.finite_polynomial_exceptions line 19

Source documentation

Finitely many polynomial conditions, valid at zero, remain valid outside one finite union of their actual root sets.

theorem finite_polynomial_exceptions {K ι : Type*} [Field K] [Fintype ι]
    (P : ι → Polynomial K) (hP : ∀ i, (P i).eval 0 ≠ 0) :
    ∃ E : Finset K, 0 ∉ E ∧ ∀ s ∉ E, ∀ i, (P i).eval s ≠ 0 := by
…

theorem OAI.Nagata.Workers.W14.exists_parameter_for_finite_polynomials line 45

Source documentation

Arbitrary further finite exclusions can be included without losing existence of a good parameter over an infinite field.

theorem exists_parameter_for_finite_polynomials {K ι : Type*}
    [Field K] [Infinite K] [Fintype ι]
    (P : ι → Polynomial K) (hP : ∀ i, (P i).eval 0 ≠ 0) (F : Finset K) :
    ∃ s : K, s ∉ F ∧ ∀ i, (P i).eval s ≠ 0 := by
…

def OAI.Nagata.Workers.W14.evaluateMotion line 69

Source documentation

Evaluate a polynomial homogeneous-coordinate motion at a parameter.

def evaluateMotion {K : Type*} [Field K] {r n : ℕ}
    (P : Fin r → Fin n → Polynomial K) (s : K) (i : Fin r) : Fin n → K :=
…

theorem OAI.Nagata.Workers.W14.polynomial_motion_separated_cofinite line 75

Source documentation

A tuple of polynomial vectors with nonzero coordinates and pair-separating minors at zero preserves both properties off one finite root set.

theorem polynomial_motion_separated_cofinite {K : Type*} [Field K] {r n : ℕ}
    (P : Fin r → Fin n → Polynomial K)
    (hzero : ∀ i, evaluateMotion P 0 i ≠ 0)
    (hsep : ∀ i j, i ≠ j → ∃ a b,
      evaluateMotion P 0 i a * evaluateMotion P 0 j b -
        evaluateMotion P 0 i b * evaluateMotion P 0 j a ≠ 0) :
    ∃ E : Finset K, 0 ∉ E ∧
      (∀ s ∉ E, ∀ i, evaluateMotion P s i ≠ 0) ∧
      ∀ s ∉ E, ∀ i j, i ≠ j → ∃ a b,
        evaluateMotion P s i a * evaluateMotion P s j b -
          evaluateMotion P s i b * evaluateMotion P s j a ≠ 0 := by
…

Mentions: OAI.Nagata.Workers.W14.evaluateMotion

theorem OAI.Nagata.Workers.W14.polynomial_projective_motion_cofinite line 140

Source documentation

Polynomial representative motions whose classes are distinct at zero remain nonzero and pairwise projectively distinct outside one finite set. The same finite set controls every representative and every pair simultaneously.

theorem polynomial_projective_motion_cofinite {K : Type*} [Field K] {r n : ℕ}
    (P : Fin r → Fin n → Polynomial K)
    (hzero : ∀ i, evaluateMotion P 0 i ≠ 0)
    (hinj : Function.Injective
      (fun i => Projectivization.mk K (evaluateMotion P 0 i) (hzero i))) :
    ∃ E : Finset K, 0 ∉ E ∧
      ∃ hvalid : ∀ s ∉ E, ∀ i, evaluateMotion P s i ≠ 0,
        ∀ s (hs : s ∉ E), Function.Injective
          (fun i => Projectivization.mk K (evaluateMotion P s i) (hvalid s hs i)) := by
…

Mentions: OAI.Nagata.Workers.W14.evaluateMotion

def OAI.Nagata.Workers.W14.linearMotion line 165

Source documentation

The affine-linear homogeneous-coordinate motion a + s V.

def linearMotion {K : Type*} [Field K] {r n : ℕ}
    (a V : Fin r → Fin n → K) : Fin r → Fin n → Polynomial K :=
…

theorem OAI.Nagata.Workers.W14.evaluate_linearMotion line 169

theorem OAI.Nagata.Workers.W14.linear_projective_motion_cofinite line 178

Source documentation

The manuscript's actual affine-linear motions satisfy the cofinite tuple condition, for arbitrary velocity vectors.

theorem linear_projective_motion_cofinite {r : ℕ}
    (a V : Fin r → Fin 3 → ℂ) (ha : ∀ i, a i ≠ 0)
    (hinj : Function.Injective (fun i => Projectivization.mk ℂ (a i) (ha i))) :
    ∃ E : Finset ℂ, 0 ∉ E ∧
      ∃ hvalid : ∀ s ∉ E, ∀ i, a i + s • V i ≠ 0,
        ∀ s (hs : s ∉ E), Function.Injective
          (fun i => Projectivization.mk ℂ (a i + s • V i) (hvalid s hs i)) := by
…

theorem OAI.Nagata.Workers.W14.projective_tuple_linear_motion_cofinite line 195

Source documentation

Starting directly from an actual distinct projective tuple, Mathlib's nonzero representatives give affine-linear homogeneous-coordinate motions with one finite exceptional parameter set.

theorem projective_tuple_linear_motion_cofinite {r : ℕ}
    (p : Fin r → Projectivization ℂ (Fin 3 → ℂ)) (hp : Function.Injective p)
    (V : Fin r → Fin 3 → ℂ) :
    ∃ E : Finset ℂ, 0 ∉ E ∧
      ∃ hvalid : ∀ s ∉ E, ∀ i, (p i).rep + s • V i ≠ 0,
        ∀ s (hs : s ∉ E), Function.Injective
          (fun i => Projectivization.mk ℂ ((p i).rep + s • V i) (hvalid s hs i)) := by
…

theorem OAI.Nagata.Workers.W14.pderiv_polynomial_substitution line 218
theorem OAI.Nagata.Workers.W14.eval_pderiv_substitution_eq_zero_of_singular line 231
def OAI.Nagata.Workers.W14.chartPolynomialRepresentatives line 268
Source documentation
Polynomial homogeneous representatives with fixed distinguished coordinate one in a separately chosen affine chart at every marked point.
```
def chartPolynomialRepresentatives {r : ℕ} (c : Fin r → Fin 3)
    (p : Fin r × Fin 2 → Polynomial ℂ) : Fin r → Fin 3 → Polynomial ℂ :=
…
```

theorem OAI.Nagata.Workers.W14.evaluate_chartPolynomialRepresentatives line 273

Source documentation

Parameter evaluation commutes with the genuine chart embedding.

theorem evaluate_chartPolynomialRepresentatives {r : ℕ} (c : Fin r → Fin 3)
    (p : Fin r × Fin 2 → Polynomial ℂ) (s : ℂ) (i : Fin r) :
    evaluateMotion (chartPolynomialRepresentatives c p) s i =
      chartVector₂ (c i) (fun j => (p (i, j)).eval s) := by
…

Mentions: OAI.Nagata.Workers.W14.evaluateMotion, OAI.Nagata.Workers.W14.chartPolynomialRepresentatives

theorem OAI.Nagata.Workers.W14.chart_polynomial_motion_cofinite line 286

Source documentation

Validity of distinct polynomial affine-chart configurations outside one finite exceptional parameter set, with no restriction on the polynomial degrees.

theorem chart_polynomial_motion_cofinite {r : ℕ} (c : Fin r → Fin 3)
    (p : Fin r × Fin 2 → Polynomial ℂ)
    (hbase : Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval 0))) :
    ∃ E : Finset ℂ, 0 ∉ E ∧ ∀ s ∉ E, Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval s)) := by
…

theorem OAI.Nagata.Workers.W14.order_directChart_of_multiplicity line 309
Source documentation
A projective multiplicity lower bound gives exactly the direct chart order used by the global homogeneous coefficient matrix, at a normalized chart point.
```
theorem order_directChart_of_multiplicity {F : MvPolynomial (Fin 3) ℂ}
    (c : Fin 3) (z : Fin 2 → ℂ) (m : ℕ)
    (h : multiplicityAtLeast F (chartPoint₂ c z) m) :
    Nagata.AffineMultiplicity.orderAtLeast z m (Nagata.W27.directChartHom c F) := by
…
```
Mentions: OAI.Nagata.W27.directChartHom
theorem OAI.Nagata.Workers.W14.coordinateLineRestriction_basisChange line 332
theorem OAI.Nagata.Workers.W14.basis_line_partial_zero_of_singular line 350