ChartLNDConstant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Constant coefficients forced by a locally nilpotent derivation on a chart

This is the complete one-chart part of the §5 rigidity argument. Starting with a locally nilpotent derivation of A, not with an assumed derivation on the chart, we localize at an invariant element, transport through a polynomial chart, and enlarge the coefficient ring to its localization. The one-variable LND theorem then forces a vertical coefficient to be constant on the chart.

theorem OAI.StableCoordinate.ChartLNDConstant.chart_coefficient_eq_C line 37
Source documentation
A chart coordinate coefficient is constant if it occurs in the derivative of the polynomial chart variable, multiplied by the inverted coefficient. All localization, transport, scalar-linearity, and nilpotence obligations are proved from the original derivation and the displayed chart identities.
```
theorem chart_coefficient_eq_C
    (D : Derivation k A A)
    (hD : ∀ x : A, ∃ n : ℕ, ((D : A → A)^[n]) x = 0)
    (hi : ∀ r : R, D (i r) = 0)
    (e : L ≃ₐ[k] S[X])
    (he : ∀ r : R, e (algebraMap A L (i r)) = C (algebraMap R S r))
    (b q : A)
    (hb : e (algebraMap A L b) = X)
    (hDb : D b = i a * q) :
    e (algebraMap A L q) = C ((e (algebraMap A L q)).coeff 0) := by
…
```
Mentions: OAI.StableCoordinate.R

theorem OAI.StableCoordinate.ChartLNDConstant.exists_chart_coefficient line 78

Source documentation

Existential form of the chart-constant conclusion.

theorem exists_chart_coefficient
    (D : Derivation k A A)
    (hD : ∀ x : A, ∃ n : ℕ, ((D : A → A)^[n]) x = 0)
    (hi : ∀ r : R, D (i r) = 0)
    (e : L ≃ₐ[k] S[X])
    (he : ∀ r : R, e (algebraMap A L (i r)) = C (algebraMap R S r))
    (b q : A)
    (hb : e (algebraMap A L b) = X)
    (hDb : D b = i a * q) :
    ∃ s : S, e (algebraMap A L q) = C s :=
…

Mentions: OAI.StableCoordinate.R