DerivationScalarUpgrade.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Enlarging the coefficient ring of a derivation

For the two polynomial charts in Section 5, a derivation annihilating the coefficient ring can be regarded as linear over that ring. The second lemma shows that annihilation of the original coefficient algebra implies annihilation of its localization, so this upgrade introduces no new condition.

def OAI.StableCoordinate.DerivationScalarUpgrade.upgrade line 23
Source documentation
View a derivation as linear over any coefficient algebra that it kills.
```
def upgrade (D : Derivation k A A) (hS : ∀ s : S, D (algebraMap S A s) = 0) :
    Derivation S A A where
…
```
theorem OAI.StableCoordinate.DerivationScalarUpgrade.upgrade_apply line 32
theorem OAI.StableCoordinate.DerivationScalarUpgrade.upgrade_iterate line 37
Source documentation
Changing coefficient rings does not change the iterated function.
```
theorem upgrade_iterate (D : Derivation k A A)
    (hS : ∀ s : S, D (algebraMap S A s) = 0) (n : ℕ) (a : A) :
    (upgrade D hS : A → A)^[n] a = (D : A → A)^[n] a := rfl
```
Mentions: OAI.StableCoordinate.DerivationScalarUpgrade.upgrade

theorem OAI.StableCoordinate.DerivationScalarUpgrade.upgrade_locallyNilpotent line 42

Source documentation

Local nilpotence survives the coefficient-ring upgrade.

theorem upgrade_locallyNilpotent (D : Derivation k A A)
    (hS : ∀ s : S, D (algebraMap S A s) = 0)
    (hD : ∀ a : A, ∃ n : ℕ, (D : A → A)^[n] a = 0) :
    ∀ a : A, ∃ n : ℕ, (upgrade D hS : A → A)^[n] a = 0 := hD

Mentions: OAI.StableCoordinate.DerivationScalarUpgrade.upgrade

theorem OAI.StableCoordinate.DerivationScalarUpgrade.upgrade_ne_zero line 48
Source documentation
A nonzero derivation remains nonzero after upgrading its coefficient ring.
```
theorem upgrade_ne_zero (D : Derivation k A A)
    (hS : ∀ s : S, D (algebraMap S A s) = 0) (hD : D ≠ 0) :
    upgrade D hS ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.DerivationScalarUpgrade.upgrade

theorem OAI.StableCoordinate.DerivationScalarUpgrade.annihilates_mvPolynomial line 57

Source documentation

It suffices to check invariance of the images of polynomial generators.

theorem annihilates_mvPolynomial {σ : Type*} (D : Derivation k A A)
    (φ : MvPolynomial σ k →ₐ[k] A)
    (hX : ∀ j : σ, D (φ (MvPolynomial.X j)) = 0) :
    ∀ p : MvPolynomial σ k, D (φ p) = 0 := by
…

theorem OAI.StableCoordinate.DerivationScalarUpgrade.annihilates_localization line 79
Source documentation
If a derivation kills the image of the original coefficient algebra, it also kills the image of its entire localization.
```
theorem annihilates_localization (D : Derivation k A A) (φ : L →+* A)
    (hR : ∀ r : R, D (φ (algebraMap R L r)) = 0) :
    ∀ l : L, D (φ l) = 0 := by
…
```
Mentions: OAI.StableCoordinate.R