Commuting derivations and the next Ore stage

This file contains the coefficientwise lift needed in the iterated Ore tower. If two coefficient derivations commute, the second one extends through the first derivation-Ore extension by differentiating every coefficient in left normal form. The formulas at the coefficient embedding and at the Ore variable are part of the interface used by later tower stages.

Commuting iterates

theorem AlgebraicAnalysis.OreTower.iterate_apply_commute {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (n : ℕ) (b : B) : E.toFun (D.toFun^[n] b) = D.toFun^[n] (E.toFun b)

theorem AlgebraicAnalysis.OreTower.coefficientDerivation_commute {B : Type u_1} [Ring B] (E F : OreDivisionDerivation B) (hcomm : ∀ (b : B), E.toFun (F.toFun b) = F.toFun (E.toFun b)) (p : Polynomial B) : (OreAssociativity.coefficientDerivation E) ((OreAssociativity.coefficientDerivation F) p) = (OreAssociativity.coefficientDerivation F) ((OreAssociativity.coefficientDerivation E) p)

theorem AlgebraicAnalysis.OreTower.coefficientDerivation_rightTerm {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (i : ℕ) (a b : B) (j : ℕ) : (OreAssociativity.coefficientDerivation E) (OreDivision.rightTerm D i a b j) = OreDivision.rightTerm D i (E.toFun a) b j + OreDivision.rightTerm D i a (E.toFun b) j

theorem AlgebraicAnalysis.OreTower.coefficientDerivation_rightMulMonomial {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (p : Polynomial B) (b : B) (j : ℕ) : (OreAssociativity.coefficientDerivation E) (OreDivision.rightMulMonomial D p b j) = OreDivision.rightMulMonomial D ((OreAssociativity.coefficientDerivation E) p) b j + OreDivision.rightMulMonomial D p (E.toFun b) j

theorem AlgebraicAnalysis.OreTower.coefficientDerivation_rightMul {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (p q : Polynomial B) : (OreAssociativity.coefficientDerivation E) (OreDivision.rightMul D p q) = OreDivision.rightMul D ((OreAssociativity.coefficientDerivation E) p) q + OreDivision.rightMul D p ((OreAssociativity.coefficientDerivation E) q)

The lifted derivation

noncomputable def AlgebraicAnalysis.OreTower.liftDerivation {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) : OreDivisionDerivation ↥(OreAssociativity.NormalOre D)

Differentiate the coefficients of a left-normal Ore polynomial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicAnalysis.OreTower.liftDerivation_apply_normalForm {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (p : Polynomial B) : (liftDerivation D E hcomm).toFun (OreAssociativity.normalForm D p) = OreAssociativity.normalForm D ((OreAssociativity.coefficientDerivation E) p)

@[simp]

theorem AlgebraicAnalysis.OreTower.liftDerivation_apply_coefficient {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (b : B) : (liftDerivation D E hcomm).toFun ((OreAssociativity.normalCoefficient D) b) = (OreAssociativity.normalCoefficient D) (E.toFun b)

@[simp]

theorem AlgebraicAnalysis.OreTower.liftDerivation_apply_variable {B : Type u_1} [Ring B] (D E : OreDivisionDerivation B) (hcomm : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) : (liftDerivation D E hcomm).toFun (OreAssociativity.normalVariable D) = 0

theorem AlgebraicAnalysis.OreTower.liftDerivation_commute {B : Type u_1} [Ring B] (D E F : OreDivisionDerivation B) (hDE : ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)) (hDF : ∀ (b : B), D.toFun (F.toFun b) = F.toFun (D.toFun b)) (hEF : ∀ (b : B), E.toFun (F.toFun b) = F.toFun (E.toFun b)) (z : ↥(OreAssociativity.NormalOre D)) : (liftDerivation D E hDE).toFun ((liftDerivation D F hDF).toFun z) = (liftDerivation D F hDF).toFun ((liftDerivation D E hDE).toFun z)