Finite iterated derivation-Ore towers

For a finite list of pairwise commuting coefficient derivations, this file builds the corresponding iterated normal Ore ring. The construction stores, at every stage, the lift of every further commuting derivation and the proof that such lifts commute. Thus the construction can be iterated without any new compatibility postulate.

The final result is an additive iterated normal-form equivalence. Operator faithfulness and freeness over a rational Weyl subring are deliberately not asserted here.

@[reducible, inline]

abbrev AlgebraicAnalysis.OreIteratedTower.Derivation (B : Type u) [Ring B] : Type u

A derivation used to build one stage of an iterated Ore tower.

Equations

• AlgebraicAnalysis.OreIteratedTower.Derivation B = AlgebraicAnalysis.OreDivisionDerivation B

def AlgebraicAnalysis.OreIteratedTower.Commutes {B : Type u} [Ring B] (D E : Derivation B) : Prop

Commutation of two coefficient derivations.

Equations

• AlgebraicAnalysis.OreIteratedTower.Commutes D E = ∀ (b : B), D.toFun (E.toFun b) = E.toFun (D.toFun b)

def AlgebraicAnalysis.OreIteratedTower.PairwiseCommutes {B : Type u} [Ring B] : List (Derivation B) → Prop

Pairwise commutation for a finite ordered family.

Equations

• AlgebraicAnalysis.OreIteratedTower.PairwiseCommutes [] = True
• AlgebraicAnalysis.OreIteratedTower.PairwiseCommutes (D :: Ds) = ((∀ E ∈ Ds, AlgebraicAnalysis.OreIteratedTower.Commutes D E) ∧ AlgebraicAnalysis.OreIteratedTower.PairwiseCommutes Ds)

def AlgebraicAnalysis.OreIteratedTower.CommutesWith {B : Type u} [Ring B] (D : Derivation B) : List (Derivation B) → Prop

Commutation of one derivation with every member of a list.

Equations

• AlgebraicAnalysis.OreIteratedTower.CommutesWith D x✝ = ∀ E ∈ x✝, AlgebraicAnalysis.OreIteratedTower.Commutes D E

theorem AlgebraicAnalysis.OreIteratedTower.commutes_symm {B : Type u} [Ring B] {D E : Derivation B} (h : Commutes D E) : Commutes E D

theorem AlgebraicAnalysis.OreIteratedTower.pairwise_tail {B : Type u} [Ring B] {D : Derivation B} {Ds : List (Derivation B)} (h : PairwiseCommutes (D :: Ds)) : PairwiseCommutes Ds

theorem AlgebraicAnalysis.OreIteratedTower.pairwise_head {B : Type u} [Ring B] {D : Derivation B} {Ds : List (Derivation B)} (h : PairwiseCommutes (D :: Ds)) : CommutesWith D Ds

theorem AlgebraicAnalysis.OreIteratedTower.commutesWith_tail {B : Type u} [Ring B] {D E : Derivation B} {Es : List (Derivation B)} (h : CommutesWith D (E :: Es)) : CommutesWith D Es

theorem AlgebraicAnalysis.OreIteratedTower.commutes_refl {B : Type u} [Ring B] (D : Derivation B) : Commutes D D

A recursive tower bundle

structure AlgebraicAnalysis.OreIteratedTower.TowerBuild {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : Type (u + 1)

TowerBuild Ds h contains the carrier ring for the tower on Ds, together with the lift of any derivation commuting with Ds. Bundling the lifts and their commutation proof avoids a circular definition of the tower type.

• carrier : Type u

  The carrier type of the recursively built tower.

• ring : Ring self.carrier

  The ring structure on the tower carrier.

• extend (D : Derivation B) : CommutesWith D Ds → OreDivisionDerivation self.carrier

  Extend a commuting coefficient derivation through the tower.

• extend_commutes (D E : Derivation B) (hD : CommutesWith D Ds) (hE : CommutesWith E Ds) : Commutes D E → Commutes (self.extend D hD) (self.extend E hE)

def AlgebraicAnalysis.OreIteratedTower.build {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : TowerBuild Ds hDs

Recursively construct the finite commuting derivation-Ore tower.

Equations

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

@[reducible, inline]

abbrev AlgebraicAnalysis.OreIteratedTower.OreTower {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : Type u

The carrier ring of the finite iterated tower.

Equations

• AlgebraicAnalysis.OreIteratedTower.OreTower Ds hDs = (AlgebraicAnalysis.OreIteratedTower.build Ds hDs).carrier

@[instance_reducible]

noncomputable instance AlgebraicAnalysis.OreIteratedTower.oreTowerRing {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : Ring (OreTower Ds hDs)

Equations

• AlgebraicAnalysis.OreIteratedTower.oreTowerRing Ds hDs = (AlgebraicAnalysis.OreIteratedTower.build Ds hDs).ring

noncomputable def AlgebraicAnalysis.OreIteratedTower.extendThrough {B : Type u} [Ring B] (D : Derivation B) (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) (hD : CommutesWith D Ds) : OreDivisionDerivation (OreTower Ds hDs)

The recursively lifted version of a coefficient derivation.

Equations

• AlgebraicAnalysis.OreIteratedTower.extendThrough D Ds hDs hD = (AlgebraicAnalysis.OreIteratedTower.build Ds hDs).extend D hD

theorem AlgebraicAnalysis.OreIteratedTower.extendThrough_commutes {B : Type u} [Ring B] (D E : Derivation B) (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) (hD : CommutesWith D Ds) (hE : CommutesWith E Ds) (hDE : Commutes D E) : Commutes (extendThrough D Ds hDs hD) (extendThrough E Ds hDs hE)

Iterated normal forms

structure AlgebraicAnalysis.OreIteratedTower.PolynomialBuild {B : Type u} [Ring B] (Ds : List (Derivation B)) : Type (u + 1)

A nested polynomial carrier together with the ring instance it needs.

• carrier : Type u

  The nested polynomial carrier.

• ring : Ring self.carrier

  The ring structure on the nested polynomial carrier.

def AlgebraicAnalysis.OreIteratedTower.polynomialBuild {B : Type u} [Ring B] (Ds : List (Derivation B)) : PolynomialBuild Ds

Recursively construct the nested polynomial coefficient carrier.

Equations

• AlgebraicAnalysis.OreIteratedTower.polynomialBuild [] = { carrier := B, ring := inferInstance }
• AlgebraicAnalysis.OreIteratedTower.polynomialBuild (D :: Ds) = { carrier := Polynomial (AlgebraicAnalysis.OreIteratedTower.polynomialBuild Ds).carrier, ring := inferInstance }

@[reducible, inline]

abbrev AlgebraicAnalysis.OreIteratedTower.iteratedPolynomial {B : Type u} [Ring B] (Ds : List (Derivation B)) : Type u

Nested coefficient-left polynomial data for the tower.

Equations

• AlgebraicAnalysis.OreIteratedTower.iteratedPolynomial Ds = (AlgebraicAnalysis.OreIteratedTower.polynomialBuild Ds).carrier

@[instance_reducible]

noncomputable instance AlgebraicAnalysis.OreIteratedTower.iteratedPolynomialRing {B : Type u} [Ring B] (Ds : List (Derivation B)) : Ring (iteratedPolynomial Ds)

Equations

• AlgebraicAnalysis.OreIteratedTower.iteratedPolynomialRing Ds = (AlgebraicAnalysis.OreIteratedTower.polynomialBuild Ds).ring

def AlgebraicAnalysis.OreIteratedTower.iteratedNormalForm {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : iteratedPolynomial Ds ≃+ OreTower Ds hDs

Additive equivalence between nested polynomial data and the Ore tower.

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicAnalysis.OreIteratedTower.iteratedNormalForm [] x_2 = AddEquiv.refl B

theorem AlgebraicAnalysis.OreIteratedTower.iteratedNormalForm_injective {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : Function.Injective ⇑(iteratedNormalForm Ds hDs)

theorem AlgebraicAnalysis.OreIteratedTower.iteratedNormalForm_surjective {B : Type u} [Ring B] (Ds : List (Derivation B)) (hDs : PairwiseCommutes Ds) : Function.Surjective ⇑(iteratedNormalForm Ds hDs)