Generation from coordinates and coordinate derivations

This is the presentation-free coordinate-elimination argument. A finite family of elements and dual derivations generates every intrinsic finite-order differential operator, provided that commuting with all the coordinates already characterizes multiplication operators.

A derivation is a finite-order operator. This is exported separately from the coordinate-generation theorem so concrete carriers can expose their derivation generators without importing an application-specific predicate.

theorem AlgebraicAnalysis.DifferentialOperators.CoordinateGeneration.derivation_mem_algebra {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] (D : Derivation k R R) : ↑D ∈ algebra

theorem AlgebraicAnalysis.DifferentialOperators.CoordinateGeneration.mem_submodule_of_coordinates' {k : Type u_1} {R : Type u_2} [Field k] [CharZero k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (D : Fin n → Derivation k R R) (hdual : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (hcoordinate : ∀ P ∈ algebra, (∀ (i : Fin n), commutator P (x i) = 0) → P = multiplication (P 1)) (H : Submodule k (Module.End k R)) (hmul : ∀ (r : R), multiplication r ∈ H) (hright : ∀ (i : Fin n), ∀ Q ∈ H, Q * ↑(D i) ∈ H) (P : Module.End k R) (hP : P ∈ algebra) : P ∈ H

Finite-order variant: the coordinate-rigidity hypothesis is required only for operators in algebra. Every intrinsic finite-order differential operator belongs to any linear subspace containing all multiplications and stable under right composition by a finite dual coordinate frame. No multiplicative closure of the subspace, or commutation hypothesis among the derivations, is required.

theorem AlgebraicAnalysis.DifferentialOperators.CoordinateGeneration.mem_submodule_of_coordinates {k : Type u_1} {R : Type u_2} [Field k] [CharZero k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (D : Fin n → Derivation k R R) (hdual : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (hcoordinate : ∀ (P : Module.End k R), (∀ (i : Fin n), commutator P (x i) = 0) → P = multiplication (P 1)) (H : Submodule k (Module.End k R)) (hmul : ∀ (r : R), multiplication r ∈ H) (hright : ∀ (i : Fin n), ∀ Q ∈ H, Q * ↑(D i) ∈ H) (P : Module.End k R) (hP : P ∈ algebra) : P ∈ H

Every intrinsic finite-order differential operator belongs to any linear subspace containing all multiplications and stable under right composition by a finite dual coordinate frame. No multiplicative closure of the subspace, or commutation hypothesis among the derivations, is required.

theorem AlgebraicAnalysis.DifferentialOperators.CoordinateGeneration.mem_subalgebra_of_coordinates' {k : Type u_1} {R : Type u_2} [Field k] [CharZero k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (D : Fin n → Derivation k R R) (hdual : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (hcoordinate : ∀ P ∈ algebra, (∀ (i : Fin n), commutator P (x i) = 0) → P = multiplication (P 1)) (H : Subalgebra k (Module.End k R)) (hmul : ∀ (r : R), multiplication r ∈ H) (hder : ∀ (i : Fin n), ↑(D i) ∈ H) (P : Module.End k R) (hP : P ∈ algebra) : P ∈ H

Finite-order variant: the coordinate-rigidity hypothesis is required only for operators in algebra. Subalgebras containing the coordinate derivations satisfy the weaker right-stability hypothesis automatically.

theorem AlgebraicAnalysis.DifferentialOperators.CoordinateGeneration.mem_subalgebra_of_coordinates {k : Type u_1} {R : Type u_2} [Field k] [CharZero k] [CommRing R] [Algebra k R] {n : ℕ} (x : Fin n → R) (D : Fin n → Derivation k R R) (hdual : ∀ (i j : Fin n), (D i) (x j) = if i = j then 1 else 0) (hcoordinate : ∀ (P : Module.End k R), (∀ (i : Fin n), commutator P (x i) = 0) → P = multiplication (P 1)) (H : Subalgebra k (Module.End k R)) (hmul : ∀ (r : R), multiplication r ∈ H) (hder : ∀ (i : Fin n), ↑(D i) ∈ H) (P : Module.End k R) (hP : P ∈ algebra) : P ∈ H

Subalgebras containing the coordinate derivations satisfy the weaker right-stability hypothesis automatically.