VerticalLND.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Vertical locally nilpotent derivations of the determinant ring

The vertical-coefficient step is the assertion in Section 5 that a locally nilpotent derivation fixing a,d,u has coefficient in k[a,d,u]. The coefficient is the actual element c * D b - b * D c of the determinant-one quotient, not an assumed polynomial representative.

theorem OAI.StableCoordinate.VerticalLND.annihilates_baseMap line 27
Source documentation
Fixing the three displayed variables means fixing the entire polynomial coefficient subalgebra; no algebraic-independence assumption is inserted.
```
theorem annihilates_baseMap (D : Derivation k (DeterminantRing.C k) (DeterminantRing.C k))
    (ha : D (a k) = 0) (hd : D (d k) = 0) (hu : D (u k) = 0) :
    ∀ p : Base k, D (baseMap p) = 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C
def OAI.StableCoordinate.VerticalLND.coefficient line 38
Source documentation
The source's common coefficient in the two remaining generator values.
```
def coefficient (D : Derivation k (DeterminantRing.C k) (DeterminantRing.C k)) :
    DeterminantRing.C k := rigidityCoefficient D (b k) (c k)
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.rigidityCoefficient
theorem OAI.StableCoordinate.VerticalLND.coefficient_equations line 42
Source documentation
The coefficient formulas hold in the exact determinant quotient.
```
theorem coefficient_equations
    (D : Derivation k (DeterminantRing.C k) (DeterminantRing.C k))
    (ha : D (a k) = 0) (hd : D (d k) = 0) :
    D (b k) = a k * coefficient D ∧ D (c k) = d k * coefficient D :=
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.VerticalLND.coefficient

theorem OAI.StableCoordinate.VerticalLND.coefficient_chartA_eq_C line 56

Source documentation

The source coefficient is constant on the actual a-chart.

theorem coefficient_chartA_eq_C
    (D : Derivation K (DeterminantRing.C K) (DeterminantRing.C K))
    (hD : ∀ z : DeterminantRing.C K, ∃ n : ℕ,
      (D : DeterminantRing.C K → DeterminantRing.C K)^[n] z = 0)
    (ha : D (a K) = 0) (hd : D (d K) = 0) (hu : D (u K) = 0) :
    chartMapA K (coefficient D) =
      Polynomial.C ((chartMapA K (coefficient D)).coeff 0) := by
…

Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.VerticalLND.coefficient

theorem OAI.StableCoordinate.VerticalLND.coefficient_chartD_eq_C line 87

Source documentation

The same source coefficient is constant on the actual d-chart.

theorem coefficient_chartD_eq_C
    (D : Derivation K (DeterminantRing.C K) (DeterminantRing.C K))
    (hD : ∀ z : DeterminantRing.C K, ∃ n : ℕ,
      (D : DeterminantRing.C K → DeterminantRing.C K)^[n] z = 0)
    (ha : D (a K) = 0) (hd : D (d K) = 0) (hu : D (u K) = 0) :
    chartMapD K (coefficient D) =
      Polynomial.C ((chartMapD K (coefficient D)).coeff 0) := by
…

Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.VerticalLND.coefficient

theorem OAI.StableCoordinate.VerticalLND.exists_polynomial_coefficient line 119

Source documentation

Every vertical LND on the exact determinant hypersurface has a polynomial coefficient in the three independent variables a,d,u.

theorem exists_polynomial_coefficient
    (D : Derivation K (DeterminantRing.C K) (DeterminantRing.C K))
    (hD : ∀ z : DeterminantRing.C K, ∃ n : ℕ,
      (D : DeterminantRing.C K → DeterminantRing.C K)^[n] z = 0)
    (ha : D (a K) = 0) (hd : D (d K) = 0) (hu : D (u K) = 0) :
    ∃ r : Base K, baseMap r = coefficient D :=
…

Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.VerticalLND.coefficient

theorem OAI.StableCoordinate.VerticalLND.coefficient_mem_baseRange line 129

Source documentation

Subalgebra-membership form of the polynomial-coefficient result.

theorem coefficient_mem_baseRange
    (D : Derivation K (DeterminantRing.C K) (DeterminantRing.C K))
    (hD : ∀ z : DeterminantRing.C K, ∃ n : ℕ,
      (D : DeterminantRing.C K → DeterminantRing.C K)^[n] z = 0)
    (ha : D (a K) = 0) (hd : D (d K) = 0) (hu : D (u K) = 0) :
    coefficient D ∈ (baseMap (k := K)).range :=
…

Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.VerticalLND.coefficient

theorem OAI.StableCoordinate.VerticalLND.classification line 139

Source documentation

Exact generator-value classification of vertical locally nilpotent derivations; the polynomial representative is constructed, not assumed.

theorem classification
    (D : Derivation K (DeterminantRing.C K) (DeterminantRing.C K))
    (hD : ∀ z : DeterminantRing.C K, ∃ n : ℕ,
      (D : DeterminantRing.C K → DeterminantRing.C K)^[n] z = 0)
    (ha : D (a K) = 0) (hd : D (d K) = 0) (hu : D (u K) = 0) :
    ∃ r : Base K, D (b K) = a K * baseMap r ∧ D (c K) = d K * baseMap r := by
…

Mentions: OAI.StableCoordinate.DeterminantRing.C