FactorialClosure.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Factorial closure of the kernel of a locally nilpotent derivation

This file formalizes bun:factorial-closure from Section 4 of the paper, using the highest nonzero iterates and the general Leibniz rule. No exponential/action correspondence is needed for this elementary step.

def OAI.StableCoordinate.IsLocallyNilpotent line 22
Source documentation
A derivation is locally nilpotent if each element is killed by some iterate.
```
def IsLocallyNilpotent (D : Derivation k A A) : Prop :=
…
```

theorem OAI.StableCoordinate.derivation_iterate_mul line 26

Source documentation

The general Leibniz formula for a ring derivation, with natural binomial coefficients.

theorem derivation_iterate_mul (D : Derivation k A A) (n : ℕ) (a b : A) :
    (D : A → A)^[n] (a * b) =
      ∑ ij ∈ antidiagonal n,
        n.choose ij.1 • ((D : A → A)^[ij.1] a * (D : A → A)^[ij.2] b) := by
…

theorem OAI.StableCoordinate.derivation_iterate_eq_zero_of_le line 43

Source documentation

Once an iterate vanishes, all later iterates vanish.

theorem derivation_iterate_eq_zero_of_le (D : Derivation k A A) {a : A} {m n : ℕ}
    (hm : (D : A → A)^[m] a = 0) (hmn : m ≤ n) :
    (D : A → A)^[n] a = 0 := by
…

theorem OAI.StableCoordinate.exists_last_nonzero_iterate line 51

Source documentation

A nonzero locally nilpotent element has a last nonzero iterate.

theorem exists_last_nonzero_iterate (D : Derivation k A A) {a : A}
    (ha : a ≠ 0) (hnil : ∃ n : ℕ, (D : A → A)^[n] a = 0) :
    ∃ m : ℕ, (D : A → A)^[m] a ≠ 0 ∧ (D : A → A)^[m + 1] a = 0 := by
…

theorem OAI.StableCoordinate.derivation_iterate_top_mul line 66

Source documentation

The only surviving term at the sum of the last possible derivative indices.

theorem derivation_iterate_top_mul (D : Derivation k A A) (a b : A) (m n : ℕ)
    (hm : (D : A → A)^[m + 1] a = 0)
    (hn : (D : A → A)^[n + 1] b = 0) :
    (D : A → A)^[m + n] (a * b) =
      (m + n).choose m • ((D : A → A)^[m] a * (D : A → A)^[n] b) := by
…

theorem OAI.StableCoordinate.lnd_factorial_closure line 88
Source documentation
The kernel of a locally nilpotent derivation on a characteristic-zero domain is factorially closed. This is bun:factorial-closure from the source.
```
theorem lnd_factorial_closure [IsDomain A] [CharZero A]
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) {a b : A}
    (ha : a ≠ 0) (hb : b ≠ 0) (hab : D (a * b) = 0) :
    D a = 0 ∧ D b = 0 := by
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent

theorem OAI.StableCoordinate.lnd_fixed_of_difference_of_squares line 107

Source documentation

The difference-of-squares step of the rigidity proof: fixing a²u²-d² forces the three factors a, d, and u to be fixed.

theorem lnd_fixed_of_difference_of_squares [IsDomain A] [CharZero A]
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) {a d u : A}
    (ha : a ≠ 0) (hu : u ≠ 0)
    (hminus : a * u - d ≠ 0) (hplus : a * u + d ≠ 0)
    (hv : D (a ^ 2 * u ^ 2 - d ^ 2) = 0) :
    D a = 0 ∧ D d = 0 ∧ D u = 0 := by
…

Mentions: OAI.StableCoordinate.IsLocallyNilpotent