CoordinatePartials.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual polynomial coordinate partials: commuting, locally nilpotent, linearly independent over the polynomial ring, and with exact constant common kernel in characteristic zero. No localization equivalence is assumed here.

theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partials_commute line 17
theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partial_iterate_eq_zero line 29
Source documentation
Vanishing of all coefficients at exponent at least n implies annihilation by the nth partial iterate. This works over every commutative ring.
```
theorem coordinate_partial_iterate_eq_zero (i : σ) (n : ℕ) (p : MvPolynomial σ B)
    (hp : ∀ m : σ →₀ ℕ, n ≤ m i → p.coeff m = 0) :
    (pderiv i : MvPolynomial σ B → MvPolynomial σ B)^[n] p = 0 := by
…
```
Mentions: OAI.AbhyankarSathaye.p
theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partial_nilpotence_bound line 50
Source documentation
An explicit pointwise bound: one more than the largest exponent of i among the finitely many supported monomials.
```
theorem coordinate_partial_nilpotence_bound (i : σ) (p : MvPolynomial σ B) :
    (pderiv i : MvPolynomial σ B → MvPolynomial σ B)^[
      p.support.sup (fun m => m i) + 1] p = 0 := by
…
```
Mentions: OAI.AbhyankarSathaye.p
theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partial_locallyNilpotent line 62
theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficient_eq_zero_of_all_partials_zero line 68
Source documentation
Exact coefficient consequence of the common-kernel condition.
```
theorem coefficient_eq_zero_of_all_partials_zero [IsDomain B] [CharZero B]
    (p : MvPolynomial σ B) (hp : ∀ i, pderiv i p = 0)
    (m : σ →₀ ℕ) (hm : m ≠ 0) : p.coeff m = 0 := by
…
```
Mentions: OAI.AbhyankarSathaye.p
theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partials_common_kernel line 92
Source documentation
The common kernel is literally the coefficient ring, with witness equal to the constant coefficient. In particular this applies to Laurent coefficients over C, once that coefficient algebra's domain and characteristic are installed.
```
theorem coordinate_partials_common_kernel [IsDomain B] [CharZero B]
    (p : MvPolynomial σ B) :
    (∀ i, pderiv i p = 0) ↔ ∃ b : B, p = C b := by
…
```
Mentions: OAI.AbhyankarSathaye.p
theorem OAI.AbhyankarSathaye.CommutingDerivations.coordinate_partials_linearIndependent line 107