LaurentWeightedMap.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted polynomial evaluation in a Laurent polynomial algebra

The source convention has degree T = -1. Consequently a variable of integer weight w i is evaluated as a constant times T (-w i). This module supplies the graded compatibility needed when extending the leading derivation to the source's Laurent localization.

def OAI.StableCoordinate.LaurentWeightedMap.evaluate line 26
Source documentation
The polynomial map with prescribed homogeneous Laurent images.
```
def evaluate (w : σ → ℤ) (c : σ → B) : MvPolynomial σ k →ₐ[k] B[T;T⁻¹] :=
…
```
theorem OAI.StableCoordinate.LaurentWeightedMap.evaluate_X line 29

theorem OAI.StableCoordinate.LaurentWeightedMap.evaluate_monomial line 34

Source documentation

The exact Laurent exponent of an evaluated monomial.

theorem evaluate_monomial (w : σ → ℤ) (c : σ → B) (d : σ →₀ ℕ) (r : k) :
    evaluate w c (MvPolynomial.monomial d r) =
      C (MvPolynomial.aeval c (MvPolynomial.monomial d r)) * T (-Finsupp.weight w d) := by
…

Mentions: OAI.StableCoordinate.LaurentWeightedMap.evaluate

theorem OAI.StableCoordinate.LaurentWeightedMap.evaluate_homogeneous line 45
Source documentation
Every polynomial homogeneous for the integer weights maps to a single Laurent exponent. The coefficient is its ordinary evaluation.
```
theorem evaluate_homogeneous (w : σ → ℤ) (c : σ → B)
    {p : MvPolynomial σ k} {m : ℤ} (hp : p.IsWeightedHomogeneous w m) :
    evaluate w c p = C (MvPolynomial.aeval c p) * T (-m) := by
…
```
Mentions: OAI.StableCoordinate.LaurentWeightedMap.evaluate
theorem OAI.StableCoordinate.LaurentWeightedMap.coeff_evaluate_eq_zero line 60
Source documentation
Coefficient-support formulation, used by Laurent derivation descent.
```
theorem coeff_evaluate_eq_zero (w : σ → ℤ) (c : σ → B)
    {p : MvPolynomial σ k} {m : ℤ} (hp : p.IsWeightedHomogeneous w m)
    (j : ℤ) (hj : j ≠ -m) :
    (evaluate w c p).coeff j = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentWeightedMap.evaluate

theorem OAI.StableCoordinate.LaurentWeightedMap.map_homogeneous line 69

Source documentation

The graded compatibility is true for any polynomial map with these generator images, not merely for the displayed evaluation map.

theorem map_homogeneous (w : σ → ℤ) (c : σ → B)
    (φ : MvPolynomial σ k →ₐ[k] B[T;T⁻¹])
    (hφ : ∀ i : σ, φ (MvPolynomial.X i) = C (c i) * T (-w i))
    {p : MvPolynomial σ k} {m : ℤ} (hp : p.IsWeightedHomogeneous w m) :
    φ p = C (MvPolynomial.aeval c p) * T (-m) := by
…