LaurentLNDDescent.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous locally nilpotent derivations on a Laurent polynomial ring

The degree convention in the manuscript is deg τ = -1. Thus a derivation of degree m maps constants to Laurent monomials with exponent -m. We use the exponent q directly, so the source application takes q = -m.

theorem OAI.StableCoordinate.LaurentDescent.coeff_C_mul_T line 24
theorem OAI.StableCoordinate.LaurentDescent.derivation_T_eq_zero line 30
Source documentation
Vanishing of a derivation on T implies vanishing on every integral power.
```
theorem derivation_T_eq_zero (D : Derivation k A[T;T⁻¹] A[T;T⁻¹])
    (hT : D (T 1) = 0) (n : ℤ) : D (T n) = 0 := by
…
```
def OAI.StableCoordinate.LaurentDescent.coefficientLinear line 44
Source documentation
Constants followed by a specified coefficient of the derivation.
```
def coefficientLinear (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ) : A →ₗ[k] A where
…
```
def OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants line 53
Source documentation
The precise homogeneous-on-constants condition needed for Laurent descent.
```
def HomogeneousOnConstants (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ) : Prop :=
…
```
theorem OAI.StableCoordinate.LaurentDescent.homogeneousOnConstants_iff line 57
Source documentation
The homogeneous-on-constants condition is exactly absence of all other exponents.
```
theorem homogeneousOnConstants_iff (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ) :
    HomogeneousOnConstants D q ↔
      ∀ (a : A) (i : ℤ), i ≠ q → (D (C a)).coeff i = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants
def OAI.StableCoordinate.LaurentDescent.descend line 72
Source documentation
The coefficient derivation obtained from a homogeneous Laurent derivation.
```
def descend (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) : Derivation k A A where
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants
theorem OAI.StableCoordinate.LaurentDescent.descend_apply line 86
theorem OAI.StableCoordinate.LaurentDescent.derivation_C_eq line 91
Source documentation
The defining homogeneous expression in terms of the descended derivation.
```
theorem derivation_C_eq (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (a : A) :
    D (C a) = C (descend D q hq a) * T q := hq a
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.LaurentDescent.descend
theorem OAI.StableCoordinate.LaurentDescent.derivation_C_mul_T line 96
Source documentation
A homogeneous Laurent derivation differentiates a monomial only through its coefficient.
```
theorem derivation_C_mul_T (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0) (a : A) (j : ℤ) :
    D (C a * T j) = C (descend D q hq a) * T (q + j) := by
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.LaurentDescent.descend

theorem OAI.StableCoordinate.LaurentDescent.iterate_C line 103

Source documentation

The exact iterate formula; in the source q=-m.

theorem iterate_C (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0) (a : A) (n : ℕ) :
    (D : A[T;T⁻¹] → A[T;T⁻¹])^[n] (C a) =
      C ((descend D q hq : A → A)^[n] a) * T ((n : ℤ) * q) := by
…

Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.LaurentDescent.descend

theorem OAI.StableCoordinate.LaurentDescent.descend_locallyNilpotent line 117
Source documentation
Local nilpotence descends from the Laurent ring to the coefficient ring.
```
theorem descend_locallyNilpotent (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0)
    (hD : StableCoordinate.IsLocallyNilpotent D) :
    StableCoordinate.IsLocallyNilpotent (descend D q hq) := by
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.LaurentDescent.descend
theorem OAI.StableCoordinate.LaurentDescent.derivation_eq_zero_of_constants line 129
Source documentation
A derivation on the Laurent ring is determined by constants and T.
```
theorem derivation_eq_zero_of_constants (D : Derivation k A[T;T⁻¹] A[T;T⁻¹])
    (hC : ∀ a : A, D (C a) = 0) (hT : D (T 1) = 0) : D = 0 := by
…
```
theorem OAI.StableCoordinate.LaurentDescent.descend_ne_zero line 139
Source documentation
Nonzero homogeneous Laurent derivations descend to nonzero derivations.
```
theorem descend_ne_zero (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0) (hD : D ≠ 0) :
    descend D q hq ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.LaurentDescent.descend
theorem OAI.StableCoordinate.LaurentDescent.descend_invariant line 150
Source documentation
An invariant Laurent monomial has invariant coefficient after descent.
```
theorem descend_invariant (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0) {a : A} {j : ℤ}
    (ha : D (C a * T j) = 0) : descend D q hq a = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.LaurentDescent.descend

theorem OAI.StableCoordinate.LaurentDescent.exists_descended_lnd line 158

Source documentation

The standalone Laurent descent package used in gr:descent.

theorem exists_descended_lnd (D : Derivation k A[T;T⁻¹] A[T;T⁻¹]) (q : ℤ)
    (hq : HomogeneousOnConstants D q) (hT : D (T 1) = 0)
    (hD : StableCoordinate.IsLocallyNilpotent D) (hne : D ≠ 0) :
    ∃ E : Derivation k A A,
      StableCoordinate.IsLocallyNilpotent E ∧ E ≠ 0 ∧
      (∀ a : A, D (C a) = C (E a) * T q) ∧
      (∀ (a : A) (j : ℤ), D (C a * T j) = 0 → E a = 0) := by
…

Mentions: OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants, OAI.StableCoordinate.IsLocallyNilpotent