Homogenization.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Guarded homogenization of affine incidence equations

def OAI.Nagata.W27.blockOrder line 24
Source documentation
Affine degree in one point-coordinate block.
```
def blockOrder (a : (Fin r × Fin 2) →₀ ℕ) (i : Fin r) : ℕ :=
…
```
def OAI.Nagata.W27.blockDegreeBound line 28
Source documentation
A separate degree bound for each point-coordinate block.
```
def blockDegreeBound (f : MvPolynomial (Fin r × Fin 2) R) (i : Fin r) : ℕ :=
…
```
theorem OAI.Nagata.W27.blockOrder_le_bound line 31
def OAI.Nagata.W27.guardedExponent line 38
Source documentation
Insert the distinguished projective-coordinate exponent. The extra one is the guard: every term vanishes outside the chosen product affine chart.
```
def guardedExponent (c : Fin r → Fin 3) (D : Fin r → ℕ)
    (a : (Fin r × Fin 2) →₀ ℕ) : (Fin r × Fin 3) →₀ ℕ :=
…
```
theorem OAI.Nagata.W27.guardedExponent_same line 45
theorem OAI.Nagata.W27.guardedExponent_other line 50
theorem OAI.Nagata.W27.guardedExponent_block_sum line 55

def OAI.Nagata.W27.guardedHomogenize line 64

Source documentation

Guarded block homogenization of an arbitrary affine polynomial.

def guardedHomogenize (c : Fin r → Fin 3)
    (f : MvPolynomial (Fin r × Fin 2) R) : MvPolynomial (Fin r × Fin 3) R :=
…

theorem OAI.Nagata.W27.guardedHomogenize_homogeneous line 69

Source documentation

Each actual support monomial has the prescribed degree in every block.

theorem guardedHomogenize_homogeneous (c : Fin r → Fin 3)
    (f : MvPolynomial (Fin r × Fin 2) R)
    (b : (Fin r × Fin 3) →₀ ℕ) (hb : b ∈ (guardedHomogenize c f).support)
    (i : Fin r) : (∑ j : Fin 3, b (i, j)) = blockDegreeBound f i + 1 := by
…

Mentions: OAI.Nagata.W27.guardedHomogenize, OAI.Nagata.W27.blockDegreeBound

theorem OAI.Nagata.W27.eval_guardedHomogenize_zero line 84

Source documentation

A zero distinguished coordinate kills every guarded term.

theorem eval_guardedHomogenize_zero (c : Fin r → Fin 3)
    (f : MvPolynomial (Fin r × Fin 2) R) (v : Fin r × Fin 3 → R)
    (i : Fin r) (hi : v (i, c i) = 0) :
    eval v (guardedHomogenize c f) = 0 := by
…

Mentions: OAI.Nagata.W27.guardedHomogenize

theorem OAI.Nagata.W27.eval_guardedHomogenize_normalized line 100

Source documentation

On normalized homogeneous representatives the homogenized polynomial evaluates to the original affine polynomial.

theorem eval_guardedHomogenize_normalized (c : Fin r → Fin 3)
    (f : MvPolynomial (Fin r × Fin 2) R) (v : Fin r × Fin 3 → R)
    (hv : ∀ i, v (i, c i) = 1) :
    eval v (guardedHomogenize c f) =
      eval (fun ij => v (ij.1, (c ij.1).succAbove ij.2)) f := by
…

Mentions: OAI.Nagata.W27.guardedHomogenize

theorem OAI.Nagata.W27.eval_guardedHomogenize_scale line 120

Source documentation

Scaling each homogeneous coordinate block scales the polynomial by its actual block degree.

theorem eval_guardedHomogenize_scale (c : Fin r → Fin 3)
    (f : MvPolynomial (Fin r × Fin 2) R)
    (a : Fin r → R) (v : Fin r × Fin 3 → R) :
    eval (fun ij => a ij.1 * v ij) (guardedHomogenize c f) =
      (∏ i, a i ^ (blockDegreeBound f i + 1)) * eval v (guardedHomogenize c f) := by
…

Mentions: OAI.Nagata.W27.guardedHomogenize, OAI.Nagata.W27.blockDegreeBound

theorem OAI.Nagata.W27.eval_guardedHomogenize_chart line 142

Source documentation

For arbitrary nonzero chart coordinates the denominator-clearing factor is explicit and nonzero.

theorem eval_guardedHomogenize_chart {K : Type*} [Field K]
    (c : Fin r → Fin 3) (f : MvPolynomial (Fin r × Fin 2) K)
    (v : Fin r × Fin 3 → K) (hv : ∀ i, v (i, c i) ≠ 0) :
    eval v (guardedHomogenize c f) =
      (∏ i, v (i, c i) ^ (blockDegreeBound f i + 1)) *
        eval (fun ij => v (ij.1, (c ij.1).succAbove ij.2) / v (ij.1, c ij.1)) f := by
…

Mentions: OAI.Nagata.W27.guardedHomogenize, OAI.Nagata.W27.blockDegreeBound

theorem OAI.Nagata.W27.eval_guardedHomogenize_eq_zero_iff line 159