Iterated coordinate-momentum pair stages

This file recursively repeats the checked PairStage construction over an arbitrary coefficient ring. It records only the resulting tower and the canonical data introduced at each successor; it does not identify the tower with a presented Weyl algebra.

structure Stafford38.OreIteratedPairStage.RingStage : Type (u + 1)

A type together with the ring structure used at the next Ore stage.

• carrier : Type u

  The carrier of the current Ore stage.

• ring : Ring self.carrier

  The ring structure used for the next coordinate-momentum extension.

def Stafford38.OreIteratedPairStage.iteratedPairData (B : Type u) [Ring B] : ℕ → RingStage

The recursively constructed ring data after adjoining n Weyl pairs.

Equations

• Stafford38.OreIteratedPairStage.iteratedPairData B 0 = { carrier := B, ring := inferInstance }
• Stafford38.OreIteratedPairStage.iteratedPairData B n.succ = { carrier := ↥Stafford38.OrePairStage.PairStage, ring := inferInstance }

def Stafford38.OreIteratedPairStage.IteratedPairStage (B : Type u) [Ring B] (n : ℕ) : Type u

The ring obtained from B after recursively adjoining n checked coordinate-momentum pairs.

Equations

• Stafford38.OreIteratedPairStage.IteratedPairStage B n = (Stafford38.OreIteratedPairStage.iteratedPairData B n).carrier

@[instance_reducible]

noncomputable instance Stafford38.OreIteratedPairStage.iteratedPairStageRing (B : Type u) [Ring B] (n : ℕ) : Ring (IteratedPairStage B n)

Equations

• Stafford38.OreIteratedPairStage.iteratedPairStageRing B n = (Stafford38.OreIteratedPairStage.iteratedPairData B n).ring

theorem Stafford38.OreIteratedPairStage.iteratedPairStage_zero (B : Type u) [Ring B] : IteratedPairStage B 0 = B

The zeroth stage is the original coefficient type.

theorem Stafford38.OreIteratedPairStage.iteratedPairStage_succ (B : Type u) [Ring B] (n : ℕ) : IteratedPairStage B (n + 1) = ↥OrePairStage.PairStage

Every successor is definitionally the checked PairStage construction over its predecessor.

noncomputable def Stafford38.OreIteratedPairStage.stageEmbedding (B : Type u) [Ring B] (n : ℕ) : IteratedPairStage B n →+* IteratedPairStage B (n + 1)

The canonical embedding from stage n into stage n + 1.

Equations

• Stafford38.OreIteratedPairStage.stageEmbedding B n = Stafford38.OrePairStage.pairCoefficient

noncomputable def Stafford38.OreIteratedPairStage.stageCoordinate (B : Type u) [Ring B] (n : ℕ) : IteratedPairStage B (n + 1)

The coordinate introduced at the successor of stage n.

Equations

• Stafford38.OreIteratedPairStage.stageCoordinate B n = Stafford38.OrePairStage.pairCoordinate

noncomputable def Stafford38.OreIteratedPairStage.stageMomentum (B : Type u) [Ring B] (n : ℕ) : IteratedPairStage B (n + 1)

The momentum introduced at the successor of stage n.

Equations

• Stafford38.OreIteratedPairStage.stageMomentum B n = Stafford38.OrePairStage.pairMomentum

theorem Stafford38.OreIteratedPairStage.stageCoordinate_mul_embedding (B : Type u) [Ring B] (n : ℕ) (b : IteratedPairStage B n) : stageCoordinate B n * (stageEmbedding B n) b = (stageEmbedding B n) b * stageCoordinate B n

The coordinate introduced at stage n + 1 commutes with the embedded predecessor ring.

theorem Stafford38.OreIteratedPairStage.stageMomentum_mul_embedding (B : Type u) [Ring B] (n : ℕ) (b : IteratedPairStage B n) : stageMomentum B n * (stageEmbedding B n) b = (stageEmbedding B n) b * stageMomentum B n

The momentum introduced at stage n + 1 commutes with the embedded predecessor ring.

theorem Stafford38.OreIteratedPairStage.stageMomentum_mul_coordinate (B : Type u) [Ring B] (n : ℕ) : stageMomentum B n * stageCoordinate B n = stageCoordinate B n * stageMomentum B n + 1

The generators introduced at stage n + 1 satisfy the checked Weyl relation.