LocalizationLND.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Localization of locally nilpotent derivations at invariants

This module proves the localization step used twice in the manuscript: Section 3 after equation (gr:iterate), and Section 5 before the univariate locally nilpotent derivation argument. Denominators are required to be annihilated by the derivation; there is no characteristic or domain assumption for the extension and its local nilpotence.

theorem OAI.StableCoordinate.LocalizationLND.numerator_wellDefined line 28
def OAI.StableCoordinate.LocalizationLND.localizeFun line 41
Source documentation
On fractions with invariant denominators the extension differentiates only the numerator.
```
def localizeFun (x : Localization M) : Localization M :=
…
```
theorem OAI.StableCoordinate.LocalizationLND.localizeFun_mk line 45
theorem OAI.StableCoordinate.LocalizationLND.localizeFun_add line 48
theorem OAI.StableCoordinate.LocalizationLND.localizeFun_one line 57
theorem OAI.StableCoordinate.LocalizationLND.localizeFun_mul line 60
theorem OAI.StableCoordinate.LocalizationLND.localizeFun_algebraMap line 70
def OAI.StableCoordinate.LocalizationLND.localize line 75
Source documentation
Extend a derivation to a localization whose denominators it annihilates.
```
def localize : Derivation k (Localization M) (Localization M) where
…
```
theorem OAI.StableCoordinate.LocalizationLND.localize_mk line 87
theorem OAI.StableCoordinate.LocalizationLND.localize_algebraMap line 90
theorem OAI.StableCoordinate.LocalizationLND.localize_iterate_mk line 95
Source documentation
Iteration continues to differentiate only the numerator.
```
theorem localize_iterate_mk (n : ℕ) (a : A) (b : M) :
    (localize D M hM : Localization M → Localization M)^[n] (Localization.mk a b) =
      Localization.mk ((D : A → A)^[n] a) b := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.localize
theorem OAI.StableCoordinate.LocalizationLND.localize_locallyNilpotent line 104
Source documentation
Local nilpotence is preserved on localization at invariant denominators.
```
theorem localize_locallyNilpotent
    (hD : ∀ a : A, ∃ n : ℕ, (D : A → A)^[n] a = 0) :
    ∀ x : Localization M, ∃ n : ℕ,
      (localize D M hM : Localization M → Localization M)^[n] x = 0 := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.localize
def OAI.StableCoordinate.LocalizationLND.transport line 123
Source documentation
Transport a derivation across an algebra equivalence.
```
def transport (e : A ≃ₐ[k] B) : Derivation k B B :=
…
```
theorem OAI.StableCoordinate.LocalizationLND.transport_apply line 128
theorem OAI.StableCoordinate.LocalizationLND.transport_iterate line 133
Source documentation
Iteration commutes with transport.
```
theorem transport_iterate (e : A ≃ₐ[k] B) (n : ℕ) (a : A) :
    (transport D e : B → B)^[n] (e a) = e ((D : A → A)^[n] a) := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.transport
theorem OAI.StableCoordinate.LocalizationLND.transport_locallyNilpotent line 141
Source documentation
Local nilpotence is independent of the chosen algebra presentation.
```
theorem transport_locallyNilpotent (e : A ≃ₐ[k] B)
    (hD : ∀ a : A, ∃ n : ℕ, (D : A → A)^[n] a = 0) :
    ∀ b : B, ∃ n : ℕ, (transport D e : B → B)^[n] b = 0 := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.transport
theorem OAI.StableCoordinate.LocalizationLND.transport_ne_zero line 150
Source documentation
Transport preserves nonzero derivations.
```
theorem transport_ne_zero (e : A ≃ₐ[k] B) (hD : D ≠ 0) : transport D e ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.transport
def OAI.StableCoordinate.LocalizationLND.localizeTo line 167
Source documentation
Extend to any algebra satisfying the localization universal property.
```
def localizeTo : Derivation k S S :=
…
```
theorem OAI.StableCoordinate.LocalizationLND.localizeTo_mk' line 170
theorem OAI.StableCoordinate.LocalizationLND.localizeTo_algebraMap line 178
theorem OAI.StableCoordinate.LocalizationLND.localizeTo_locallyNilpotent line 184
Source documentation
The extension to any localization is locally nilpotent.
```
theorem localizeTo_locallyNilpotent
    (hD : ∀ a : A, ∃ n : ℕ, (D : A → A)^[n] a = 0) :
    ∀ s : S, ∃ n : ℕ, (localizeTo D M hM S : S → S)^[n] s = 0 :=
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.localizeTo
theorem OAI.StableCoordinate.LocalizationLND.localizeTo_ne_zero line 190
Source documentation
If localization is injective, a nonzero derivation remains nonzero.
```
theorem localizeTo_ne_zero (hinj : Function.Injective (algebraMap A S)) (hD : D ≠ 0) :
    localizeTo D M hM S ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.localizeTo
theorem OAI.StableCoordinate.LocalizationLND.annihilates_powers line 210
Source documentation
Killing one element implies killing all powers used as denominators.
```
theorem annihilates_powers : ∀ m : Submonoid.powers a, D (m : A) = 0 := by
…
```
def OAI.StableCoordinate.LocalizationLND.localizeAway line 219
Source documentation
The common special case of localization at one invariant element.
```
def localizeAway : Derivation k S S :=
…
```
theorem OAI.StableCoordinate.LocalizationLND.localizeAway_algebraMap line 222
theorem OAI.StableCoordinate.LocalizationLND.localizeAway_locallyNilpotent line 227
Source documentation
Localization at a single invariant preserves local nilpotence.
```
theorem localizeAway_locallyNilpotent
    (hD : ∀ b : A, ∃ n : ℕ, (D : A → A)^[n] b = 0) :
    ∀ s : S, ∃ n : ℕ, (localizeAway D a ha S : S → S)^[n] s = 0 :=
…
```
Mentions: OAI.StableCoordinate.LocalizationLND.localizeAway