UniversalReduction.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Permutation, universal support, and simultaneous multiplicity reduction

theorem OAI.Nagata.W13.permutation_sum_independent line 23

Source documentation

Permutation symmetrization gives the same multiplicity at every position.

theorem permutation_sum_independent {α : Type*} [Fintype α] [DecidableEq α]
    (m : α → ℕ) (i j : α) :
    (∑ σ : Equiv.Perm α, m (σ i)) = ∑ σ : Equiv.Perm α, m (σ j) := by
…

theorem OAI.Nagata.W13.card_mul_permutation_sum line 31

Source documentation

The double sum counts each permutation's total multiplicity once.

theorem card_mul_permutation_sum {α : Type*} [Fintype α] [DecidableEq α]
    (m : α → ℕ) (i : α) :
    Fintype.card α * (∑ σ : Equiv.Perm α, m (σ i)) =
      (Fintype.card α).factorial * ∑ j, m j := by
…

theorem OAI.Nagata.W13.permutation_sum_multiplicity line 49

Source documentation

Each original multiplicity occurs (r-1)! times at each position.

theorem permutation_sum_multiplicity {r : ℕ} (hr : 0 < r)
    (m : Fin r → ℕ) (i : Fin r) :
    (∑ σ : Equiv.Perm (Fin r), m (σ i)) =
      (r - 1).factorial * ∑ j, m j := by
…

theorem OAI.Nagata.W13.permutation_product_ne_zero line 61

Source documentation

The product of the chosen nonzero forms remains nonzero in a domain.

theorem permutation_product_ne_zero {α R : Type*} [Fintype α] [DecidableEq α]
    [CommMonoidWithZero R] [Nontrivial R] [NoZeroDivisors R]
    (f : Equiv.Perm α → R) (hf : ∀ σ, f σ ≠ 0) :
    (∏ σ, f σ) ≠ 0 := by
…

def OAI.Nagata.W13.UniversalSupport line 85
Source documentation
Every ordered distinct tuple supports a nonzero equation with the given multiplicity vector. This is a definition of the intermediate universal system, not an assumption about which such systems exist.
```
def UniversalSupport (r d : ℕ) (m : Fin r → ℕ) : Prop :=
…
```

theorem OAI.Nagata.W13.multiplicityAtLeast_prod line 92

Source documentation

Finite products add the chart ideal-power multiplicity lower bounds.

theorem multiplicityAtLeast_prod {ι : Type*} (s : Finset ι)
    (p : PlanePoint) (m : ι → ℕ) (F : ι → MvPolynomial (Fin 3) ℂ)
    (h : ∀ i ∈ s, multiplicityAtLeast (F i) p (m i)) :
    multiplicityAtLeast (∏ i ∈ s, F i) p (∑ i ∈ s, m i) := by
…

theorem OAI.Nagata.W13.universalSupport_permute line 106

Source documentation

Reordering a configuration reorders the prescribed multiplicities.

theorem universalSupport_permute {r d : ℕ} {m : Fin r → ℕ}
    (h : UniversalSupport r d m) (σ : Equiv.Perm (Fin r)) :
    UniversalSupport r d (fun i => m (σ i)) := by
…

Mentions: OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.W13.universalSupport_symmetrize line 120
Source documentation
Universal support of an arbitrary multiplicity vector gives universal support of the constant vector (r-1)! * sum m, at degree r! * d. This includes unequal and zero entries in m and all nonzero homogeneous forms, including reducible and nonreduced equations.
```
theorem universalSupport_symmetrize {r d : ℕ} (hr : 0 < r)
    {m : Fin r → ℕ} (h : UniversalSupport r d m) :
    UniversalSupport r (r.factorial * d)
      (fun _ => (r - 1).factorial * ∑ i, m i) := by
…
```
Mentions: OAI.Nagata.W13.UniversalSupport
theorem OAI.Nagata.W13.universalSupport_pow line 149
Source documentation
Raising each actual equation to a power scales its degree and every multiplicity lower bound, so universal systems are closed under common multiples.
```
theorem universalSupport_pow {r d : ℕ} {m : Fin r → ℕ}
    (h : UniversalSupport r d m) (N : ℕ) :
    UniversalSupport r (d * N) (fun i => m i * N) := by
…
```
Mentions: OAI.Nagata.W13.UniversalSupport
def OAI.Nagata.W13.supportLocus line 170
Source documentation
The actual homogeneous-polynomial incidence condition at a configuration.
```
def supportLocus (r : ℕ) (i : Workers.W25.IncidenceIndex r) :
    Set (OrderedDistinctPoints r) :=
…
```
Mentions: OAI.Nagata.Workers.W25.IncidenceIndex
def OAI.Nagata.W13.supportExceptionalUnion line 178
Source documentation
One exceptional union indexed by all positive degrees and all nonnegative multiplicity vectors, retaining exactly the proper support loci.
```
def supportExceptionalUnion (r : ℕ) : Set (OrderedDistinctPoints r) :=
…
```
theorem OAI.Nagata.W13.properSupportFamily_countable line 183
Source documentation
The proper support loci form a countable family covering all positive integer degrees and all nonnegative multiplicity vectors simultaneously.
```
theorem properSupportFamily_countable (r : ℕ) :
    {S : Set (OrderedDistinctPoints r) |
      ∃ i : Workers.W25.IncidenceIndex r,
        supportLocus r i ≠ Set.univ ∧ S = supportLocus r i}.Countable :=
…
```
Mentions: OAI.Nagata.Workers.W25.IncidenceIndex, OAI.Nagata.W13.supportLocus

theorem OAI.Nagata.W13.universalSupport_of_avoids line 191

Source documentation

Outside the one exceptional union, every supported multiplicity system is universal on the whole genuine configuration space.

theorem universalSupport_of_avoids {r d : ℕ} (hd : 0 < d)
    {m : Fin r → ℕ} {p : OrderedDistinctPoints r}
    (hp : p ∉ supportExceptionalUnion r)
    (hF : ∃ F : MvPolynomial (Fin 3) ℂ,
      F ≠ 0 ∧ F.IsHomogeneous d ∧
        ∀ i, multiplicityAtLeast F (p.val i) (m i)) :
    UniversalSupport r d m := by
…

Mentions: OAI.Nagata.W13.supportExceptionalUnion, OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.W13.universalEqualSupport_of_violation line 210

Source documentation

A violating equation outside the single exceptional union produces positive integers D,M with D/M ≤ sqrt r and universal equal-multiplicity support. Topological closedness and nonemptiness of avoidance remain separate; there is no assumption about normal bundles or interpolation in this reduction.

theorem universalEqualSupport_of_violation {r d : ℕ} (hr : 0 < r) (hd : 0 < d)
    {m : Fin r → ℕ} {p : OrderedDistinctPoints r}
    (hp : p ∉ supportExceptionalUnion r)
    (hF : ∃ F : MvPolynomial (Fin 3) ℂ,
      F ≠ 0 ∧ F.IsHomogeneous d ∧
        ∀ i, multiplicityAtLeast F (p.val i) (m i))
    (hbad : (d : ℝ) * Real.sqrt r ≤ ∑ i, (m i : ℝ)) :
    ∃ D M : ℕ, 0 < D ∧ 0 < M ∧ (D : ℝ) / M ≤ Real.sqrt r ∧
      UniversalSupport r D (fun _ => M) := by
…

Mentions: OAI.Nagata.W13.supportExceptionalUnion, OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.W13.source_universal_reduction_of_incidence_closed line 244

Source documentation

The source reduction, conditional only on projective closedness of actual support loci. The same exceptional sequence handles every positive degree and all nonnegative unequal multiplicity vectors simultaneously.

theorem source_universal_reduction_of_incidence_closed
    (r : ℕ) (hr : 10 ≤ r)
    (hclosed : ∀ i : Workers.W25.IncidenceIndex r,
      IsConfigurationZariskiClosed (supportLocus r i)) :
    ∃ E : ℕ → Set (OrderedDistinctPoints r),
      (∀ n, IsConfigurationZariskiClosed (E n) ∧ E n ≠ Set.univ) ∧
      (∃ p : OrderedDistinctPoints r, ∀ n, p ∉ E n) ∧
      ∀ p : OrderedDistinctPoints r, (∀ n, p ∉ E n) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ F : MvPolynomial (Fin 3) ℂ, F ≠ 0 → F.IsHomogeneous d →
        ∀ m : Fin r → ℕ,
          (∀ i, multiplicityAtLeast F (p.val i) (m i)) →
…

Mentions: OAI.Nagata.Workers.W25.IncidenceIndex, OAI.Nagata.W13.supportLocus

theorem OAI.Nagata.W13.strict_bound_of_incidence_closed_and_no_universal line 267