Active-coordinate decomposition in a derivation Ore extension

This file isolates a reusable algebraic interface for one distinguished coefficient coordinate. The coefficient ring may be noncommutative; the coordinate is required to be central in that ring, while the active derivation annihilates ground scalars and sends the coordinate to 1.

The results use only the checked normal-form construction. They do not postulate a PBW basis, a presented Weyl algebra, or an operator realization.

The source-relative active-coordinate data

structure AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData (k : Type u_1) (C : Type u_2) [CommRing k] [Ring C] [Algebra k C] : Type u_2

Hypotheses for one active differential-Ore coordinate.

The coefficient ring can be noncommutative. coordinate_central is the exact hypothesis needed for coefficients of an active-variable expansion to commute with polynomials in the coordinate. The two derivation hypotheses record that the active derivation fixes ground scalars and differentiates the coordinate.

• derivation : OreDivisionDerivation C

  The coefficient derivation defining the Ore relation.

• coordinate : C

  The distinguished central coefficient coordinate.

• coordinate_central (c : C) : Commute self.coordinate c
• derivation_smul (a : k) : self.derivation.toFun ((algebraMap k C) a) = 0
• derivation_coordinate : self.derivation.toFun self.coordinate = (algebraMap k C) 1

@[reducible, inline]

abbrev AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.Ore {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) : Subring (AddMonoid.End (Polynomial C))

The active one-variable derivation Ore ring.

Equations

• A.Ore = AlgebraicAnalysis.OreAssociativity.NormalOre A.derivation

noncomputable def AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.coefficient {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (c : C) : ↥A.Ore

The coefficient embedding into the active Ore ring.

Equations

• A.coefficient c = (AlgebraicAnalysis.OreAssociativity.normalCoefficient A.derivation) c

noncomputable def AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.activeVariable {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) : ↥A.Ore

The active Ore variable.

Equations

• A.activeVariable = AlgebraicAnalysis.OreAssociativity.normalVariable A.derivation

noncomputable def AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.coordinatePolynomial {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (p : Polynomial k) : ↥A.Ore

The central-coordinate polynomial algebra inside the active Ore ring.

Equations

• A.coordinatePolynomial p = Polynomial.eval₂ ((AlgebraicAnalysis.OreAssociativity.normalCoefficient A.derivation).comp (algebraMap k C)) (A.coefficient A.coordinate) p

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.variable_mul_coordinate {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) : A.activeVariable * A.coefficient A.coordinate = A.coefficient A.coordinate * A.activeVariable + A.coefficient ((algebraMap k C) 1)

The defining differential-Ore relation at the distinguished coordinate.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.variable_mul_smul {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (a : k) : A.activeVariable * A.coefficient ((algebraMap k C) a) = A.coefficient ((algebraMap k C) a) * A.activeVariable

Ground scalars commute with the active Ore variable.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.coefficient_commute_smul {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (c : C) (a : k) : Commute (A.coefficient c) (A.coefficient ((algebraMap k C) a))

Every coefficient commutes with the image of a ground scalar.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.coefficient_commute_coordinate {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (c : C) : Commute (A.coefficient c) (A.coefficient A.coordinate)

Every coefficient commutes with the distinguished coordinate.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.coefficient_commute_coordinatePolynomial {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (c : C) (p : Polynomial k) : Commute (A.coefficient c) (A.coordinatePolynomial p)

Every coefficient commutes with every polynomial in the central coordinate.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.normalForm_eq_support_sum {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (p : Polynomial C) : OreAssociativity.normalForm A.derivation p = ∑ j ∈ p.support, A.coefficient (p.coeff j) * A.activeVariable ^ j

The coefficient-left normal form is an explicit finite active-variable expansion.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.recombine_coordinate_polynomial {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (p : Polynomial C) (b : ↥A.Ore) (q : Polynomial k) : ∑ j ∈ p.support, b * A.coefficient (p.coeff j) * (A.coordinatePolynomial q * A.activeVariable ^ j) = b * A.coordinatePolynomial q * OreAssociativity.normalForm A.derivation p

Recombination using only coefficient/coordinate commutation; the active Ore variable remains on the right throughout.

theorem AlgebraicAnalysis.OreActiveCoordinate.ActiveCoordinateData.exists_active_expansion {k : Type u_1} {C : Type u_2} [CommRing k] [Ring C] [Algebra k C] (A : ActiveCoordinateData k C) (d : ↥A.Ore) : ∃ (p : Polynomial C), d = ∑ j ∈ p.support, A.coefficient (p.coeff j) * A.activeVariable ^ j ∧ ∀ (n : ℕ) (q : Polynomial k), Commute (A.coefficient (p.coeff n)) (A.coordinatePolynomial q)

Normal-form surjectivity supplies a finite active-variable expansion and the coefficient commutations needed to use it source-relatively.