CoordinateDerivation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Derivations obtained from polynomial coordinate systems

The first step of §3 of the manuscript chooses a partial derivative in a coordinate distinct from the distinguished coordinate and a positive-degree invariant. This file supplies the algebraic part of that choice: partial derivatives of multivariate polynomials are locally nilpotent, and this property, nonvanishing, and the values on coordinates transport through an actual algebra equivalence.

theorem OAI.StableCoordinate.CoordinateDerivation.coeff_iterate_pderiv_eq_zero line 29

Source documentation

A coefficient vanishes once the number of differentiations exceeds the available exponent in the chosen variable.

theorem coeff_iterate_pderiv_eq_zero (i : σ) (p : MvPolynomial σ k)
    (n : ℕ) (m : σ →₀ ℕ) (h : p.degreeOf i < m i + n) :
    (((pderiv i : Derivation k (MvPolynomial σ k)
      (MvPolynomial σ k)) : MvPolynomial σ k → MvPolynomial σ k)^[n] p).coeff m = 0 := by
…

theorem OAI.StableCoordinate.CoordinateDerivation.pderiv_locallyNilpotent line 48

Source documentation

Multivariate partial derivatives are pointwise locally nilpotent, over an arbitrary commutative coefficient semiring.

theorem pderiv_locallyNilpotent (i : σ) (p : MvPolynomial σ k) :
    ∃ n : ℕ, (((pderiv i : Derivation k (MvPolynomial σ k)
      (MvPolynomial σ k)) : MvPolynomial σ k → MvPolynomial σ k)^[n]) p = 0 := by
…

def OAI.StableCoordinate.CoordinateDerivation.transport line 65
Source documentation
Transport of a derivation through an algebra equivalence.
```
def transport (e : A ≃ₐ[k] B) (D : Derivation k A A) : Derivation k B B where
…
```
theorem OAI.StableCoordinate.CoordinateDerivation.transport_apply line 73
theorem OAI.StableCoordinate.CoordinateDerivation.transport_iterate line 78
Source documentation
Iterating a transported derivation is conjugate to iterating the original one. In particular, no fixed bound on the nilpotence index is assumed.
```
theorem transport_iterate (e : A ≃ₐ[k] B) (D : Derivation k A A) (n : ℕ) (b : B) :
    ((transport e D : B → B)^[n]) b = e (((D : A → A)^[n]) (e.symm b)) := by
…
```
Mentions: OAI.StableCoordinate.CoordinateDerivation.transport
theorem OAI.StableCoordinate.CoordinateDerivation.transport_locallyNilpotent line 85
Source documentation
Pointwise local nilpotence is invariant under an algebra equivalence.
```
theorem transport_locallyNilpotent (e : A ≃ₐ[k] B) (D : Derivation k A A)
    (hD : ∀ a, ∃ n : ℕ, ((D : A → A)^[n]) a = 0) :
    ∀ b, ∃ n : ℕ, ((transport e D : B → B)^[n]) b = 0 := by
…
```
Mentions: OAI.StableCoordinate.CoordinateDerivation.transport
theorem OAI.StableCoordinate.CoordinateDerivation.transport_apply_image line 92
theorem OAI.StableCoordinate.CoordinateDerivation.transport_ne_zero line 96
Source documentation
Transport does not turn a nonzero derivation into zero.
```
theorem transport_ne_zero (e : A ≃ₐ[k] B) (D : Derivation k A A) (hD : D ≠ 0) :
    transport e D ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.CoordinateDerivation.transport
def OAI.StableCoordinate.CoordinateDerivation.coordinatePartial line 112
Source documentation
Partial differentiation in a specified member of a polynomial coordinate system, expressed intrinsically on the target algebra.
```
def coordinatePartial (e : MvPolynomial σ k ≃ₐ[k] A) (i : σ) : Derivation k A A :=
…
```
theorem OAI.StableCoordinate.CoordinateDerivation.coordinatePartial_self line 115
theorem OAI.StableCoordinate.CoordinateDerivation.coordinatePartial_other line 119
theorem OAI.StableCoordinate.CoordinateDerivation.coordinatePartial_locallyNilpotent line 123
theorem OAI.StableCoordinate.CoordinateDerivation.coordinatePartial_ne_zero line 127

theorem OAI.StableCoordinate.CoordinateDerivation.exists_nonzero_locallyNilpotent_killing_two line 135

Source documentation

In a polynomial coordinate system, any coordinate can be differentiated while two distinct other coordinates remain invariant.

theorem exists_nonzero_locallyNilpotent_killing_two [Nontrivial A]
    (e : MvPolynomial σ k ≃ₐ[k] A) (i j l : σ) (hji : j ≠ i) (hli : l ≠ i) :
    ∃ D : Derivation k A A, D ≠ 0 ∧
      (∀ a, ∃ n : ℕ, ((D : A → A)^[n]) a = 0) ∧
      D (e (X j)) = 0 ∧ D (e (X l)) = 0 := by
…

theorem OAI.StableCoordinate.CoordinateDerivation.exists_coordinate_not_mem line 147
Source documentation
A proper subalgebra cannot contain every member of a polynomial coordinate system. For the manuscript this subalgebra is the degree-at-most-zero part of the multiplicative integer filtration.
```
theorem exists_coordinate_not_mem (e : MvPolynomial σ k ≃ₐ[k] A)
    (S : Subalgebra k A) (hS : S ≠ ⊤) : ∃ j, e (X j) ∉ S := by
…
```

theorem OAI.StableCoordinate.CoordinateDerivation.exists_lnd_invariant_outside line 169

Source documentation

The exact algebraic choice at the start of the coordinate obstruction: if the distinguished coordinate lies in a proper subalgebra of a polynomial ring of dimension at least three, a nonzero locally nilpotent derivation kills both that coordinate and a coordinate outside the subalgebra.

theorem exists_lnd_invariant_outside [Nontrivial A] {n : ℕ} (hn : 2 < n)
    (e : MvPolynomial (Fin n) k ≃ₐ[k] A) (S : Subalgebra k A)
    (hS : S ≠ ⊤) (i : Fin n) (hi : e (X i) ∈ S) :
    ∃ D : Derivation k A A, D ≠ 0 ∧
      (∀ a, ∃ r : ℕ, ((D : A → A)^[r]) a = 0) ∧
      D (e (X i)) = 0 ∧ ∃ j : Fin n, j ≠ i ∧ e (X j) ∉ S ∧ D (e (X j)) = 0 := by
…