UnivariateLND.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Locally nilpotent derivations in one polynomial variable

This file supplies the one-variable derivation step in the proof of Proposition prop:rigidity, §5 of the source manuscript. Over an integral domain of characteristic zero, a locally nilpotent derivation of K[X] maps X to a constant. Local nilpotence is stated explicitly as the vanishing of a sufficiently high iterate on every polynomial.

theorem OAI.StableCoordinate.UnivariateLND.apply_eq_derivative_mul line 27
Source documentation
A derivation of a univariate polynomial algebra is multiplication of the ordinary derivative by its value on the indeterminate.
```
theorem apply_eq_derivative_mul (D : Derivation K K[X] K[X]) (p : K[X]) :
    D p = p.derivative * D X := by
…
```
theorem OAI.StableCoordinate.UnivariateLND.natDegree_apply_pos line 33
Source documentation
If the value on X has positive degree, a derivation preserves positive degree. This excludes nilpotence on X.
```
theorem natDegree_apply_pos (D : Derivation K K[X] K[X])
    (hD : 0 < (D X).natDegree) {p : K[X]} (hp : 0 < p.natDegree) :
    0 < (D p).natDegree := by
…
```
theorem OAI.StableCoordinate.UnivariateLND.natDegree_iterate_X_pos line 45
Source documentation
Every iterate on X retains positive degree if the value on X has positive degree.
```
theorem natDegree_iterate_X_pos (D : Derivation K K[X] K[X])
    (hD : 0 < (D X).natDegree) (n : ℕ) :
    0 < (((D : K[X] → K[X])^[n]) X).natDegree := by
…
```
theorem OAI.StableCoordinate.UnivariateLND.natDegree_apply_X_eq_zero_of_iterate_eq_zero line 56
Source documentation
Vanishing of one iterate on the indeterminate already forces a univariate derivation's value on the indeterminate to have degree zero.
```
theorem natDegree_apply_X_eq_zero_of_iterate_eq_zero
    (D : Derivation K K[X] K[X])
    (hD : ∃ n : ℕ, ((D : K[X] → K[X])^[n]) X = 0) :
    (D X).natDegree = 0 := by
…
```
theorem OAI.StableCoordinate.UnivariateLND.apply_X_eq_C_of_locallyNilpotent line 68
Source documentation
The needed rigidity fact: every locally nilpotent derivation of a one-variable polynomial algebra over a characteristic-zero domain sends the variable to a constant in the coefficient field.
```
theorem apply_X_eq_C_of_locallyNilpotent (D : Derivation K K[X] K[X])
    (hD : ∀ p : K[X], ∃ n : ℕ, ((D : K[X] → K[X])^[n]) p = 0) :
    D X = C ((D X).coeff 0) := by
…
```

theorem OAI.StableCoordinate.UnivariateLND.exists_apply_X_eq_C_of_locallyNilpotent line 75

Source documentation

Existential form matching the source's statement D(X) ∈ K.

theorem exists_apply_X_eq_C_of_locallyNilpotent (D : Derivation K K[X] K[X])
    (hD : ∀ p : K[X], ∃ n : ℕ, ((D : K[X] → K[X])^[n]) p = 0) :
    ∃ c : K, D X = C c :=
…