The linear symplectic layer of the A₂ reduction

This file isolates the part of the generic-monic reduction which is purely linear algebra. A Weyl presentation is encoded by a finite family z whose pairwise commutators are the entries of a fixed skew matrix. A matrix M preserving that form gives a new family by linear combination, and the new family has exactly the same Weyl commutators.

The result is deliberately stated for an arbitrary finite index type and an arbitrary symplectic form. The A₂ instance is obtained with ι = Fin 2 ⊕ Fin 2 and Matrix.J (Fin 2) k, so this is not a list of hand-picked coordinate changes.

This is the algebraic prerequisite for applying Stafford's ring-equivalence transport to a Weyl change of generators. The final section also descends a form-preserving change to a homomorphism of the presented quotient and proves the A₂ symplectic change is invertible using the inverse matrix and generator-extensionality. The PBW identification and generic monic normalization belong to the downstream Weyl modules, outside this module's linear-algebra scope. Reusable commutator identities are imported from AlgebraicAnalysis.

def Stafford.commutator {A : Type u_2} [Ring A] (u v : A) : A

Historical namespace for the shared ring commutator.

Equations

• Stafford.commutator u v = AlgebraicAnalysis.ringCommutator u v

@[simp]

theorem Stafford.commutator_eq_shared {A : Type u_2} [Ring A] (u v : A) : commutator u v = AlgebraicAnalysis.ringCommutator u v

def Stafford.linearCombination {k : Type u_1} {A : Type u_2} {ι : Type u_3} [Field k] [Ring A] [Algebra k A] [Fintype ι] (M : Matrix ι ι k) (z : ι → A) (i : ι) : A

The linear combination of a family of generators specified by a matrix.

Equations

• Stafford.linearCombination M z i = ∑ j : ι, (algebraMap k A) (M i j) * z j

theorem Stafford.commutator_sum_left {A : Type u_2} {ι : Type u_3} [Ring A] [Fintype ι] (u : ι → A) (v : A) : commutator (∑ i : ι, u i) v = ∑ i : ι, commutator (u i) v

theorem Stafford.commutator_sum_right {A : Type u_2} {ι : Type u_3} [Ring A] [Fintype ι] (u : A) (v : ι → A) : commutator u (∑ i : ι, v i) = ∑ i : ι, commutator u (v i)

theorem Stafford.commutator_smul_smul {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (a b : k) (u v : A) : commutator ((algebraMap k A) a * u) ((algebraMap k A) b * v) = (algebraMap k A) (a * b) * commutator u v

theorem Stafford.commutator_linearCombination {k : Type u_1} {A : Type u_2} {ι : Type u_3} [Field k] [Ring A] [Algebra k A] [Fintype ι] (M : Matrix ι ι k) (z : ι → A) (omega : Matrix ι ι k) (i l : ι) (hcomm : ∀ (j n : ι), commutator (z j) (z n) = (algebraMap k A) (omega j n)) : commutator (linearCombination M z i) (linearCombination M z l) = (algebraMap k A) (∑ j : ι, ∑ n : ι, M i j * omega j n * M l n)

theorem Stafford.symplectic_linear_change_preserves_commutator {k : Type u_1} {A : Type u_2} {ι : Type u_3} [Field k] [Ring A] [Algebra k A] [Fintype ι] (M : Matrix ι ι k) (z : ι → A) (omega : Matrix ι ι k) (hcomm : ∀ (j n : ι), commutator (z j) (z n) = (algebraMap k A) (omega j n)) (hM : M * omega * M.transpose = omega) (i l : ι) : commutator (linearCombination M z i) (linearCombination M z l) = (algebraMap k A) (omega i l)

A matrix preserving omega preserves all Weyl commutators.

The standard A₂ specialization

@[reducible, inline]

abbrev Stafford.A2Index : Type

The two coordinate and two momentum indices of the second Weyl algebra.

Equations

• Stafford.A2Index = (Fin 2 ⊕ Fin 2)

@[reducible, inline]

abbrev Stafford.A2SymplecticForm (k : Type u_4) [CommRing k] : Matrix A2Index A2Index k

The standard symplectic form on the four generators of the second Weyl algebra.

Equations

• Stafford.A2SymplecticForm k = Matrix.J (Fin 2) k

theorem Stafford.a2_symplectic_linear_change_preserves_weyl {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (M : Matrix A2Index A2Index k) (z : A2Index → A) (hcomm : ∀ (j n : A2Index), commutator (z j) (z n) = (algebraMap k A) (A2SymplecticForm k j n)) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) (i l : A2Index) : commutator (linearCombination M z i) (linearCombination M z l) = (algebraMap k A) (A2SymplecticForm k i l)

theorem Stafford.a2_symplectic_group_change_preserves_weyl {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (M : ↥(Matrix.symplecticGroup (Fin 2) k)) (z : A2Index → A) (hcomm : ∀ (j n : A2Index), commutator (z j) (z n) = (algebraMap k A) (A2SymplecticForm k j n)) (i l : Fin 2 ⊕ Fin 2) : commutator (linearCombination (↑M) z i) (linearCombination (↑M) z l) = (algebraMap k A) (A2SymplecticForm k i l)

Descent to the presented Weyl algebra

RingQuot is Mathlib's universal quotient for a possibly noncommutative ring. The following definitions use it to make the universal-property step explicit. This is still presentation-level algebra: identifying the quotient with a PBW Weyl algebra remains separate, while the inverse-matrix argument below proves the form-preserving A₂ map is an automorphism.

def Stafford.freeWeylRelation {k : Type u_1} {ι : Type u_3} [Field k] (omega : Matrix ι ι k) (a b : FreeAlgebra k ι) : Prop

The generating relation equating each generator commutator with the corresponding scalar form entry.

Equations

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

@[reducible, inline]

abbrev Stafford.FreeWeyl (k : Type u_4) [Field k] (ι : Type u_5) (omega : Matrix ι ι k) : Type (max u_5 u_4)

The quotient of the free algebra by the commutator relations prescribed by omega.

Equations

• Stafford.FreeWeyl k ι omega = RingQuot (Stafford.freeWeylRelation omega)

def Stafford.freeWeylGenerator {k : Type u_1} {ι : Type u_3} [Field k] (omega : Matrix ι ι k) (i : ι) : FreeWeyl k ι omega

The image of a free generator in the Weyl quotient.

Equations

• Stafford.freeWeylGenerator omega i = (RingQuot.mkAlgHom k (Stafford.freeWeylRelation omega)) (FreeAlgebra.ι k i)

theorem Stafford.freeWeylGenerator_commutator {k : Type u_1} {ι : Type u_3} [Field k] (omega : Matrix ι ι k) (i j : ι) : commutator (freeWeylGenerator omega i) (freeWeylGenerator omega j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)

def Stafford.freeWeylLinearCombination {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] {omega : Matrix ι ι k} (M : Matrix ι ι k) (z : ι → FreeWeyl k ι omega) (i : ι) : FreeWeyl k ι omega

The linear combination of Weyl elements specified by a row of a matrix.

Equations

• Stafford.freeWeylLinearCombination M z i = ∑ j : ι, (algebraMap k (Stafford.FreeWeyl k ι omega)) (M i j) * z j

def Stafford.freeWeylMap {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M omega : Matrix ι ι k) : FreeAlgebra k ι →ₐ[k] FreeWeyl k ι omega

The free-algebra homomorphism sending generators to their matrix linear combinations.

Equations

• Stafford.freeWeylMap M omega = (FreeAlgebra.lift k) fun (i : ι) => Stafford.freeWeylLinearCombination M (Stafford.freeWeylGenerator omega) i

theorem Stafford.freeWeylMapRespects {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M omega : Matrix ι ι k) (hpres : ∀ (i j : ι), commutator (freeWeylLinearCombination M (freeWeylGenerator omega) i) (freeWeylLinearCombination M (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) ⦃a b : FreeAlgebra k ι⦄ : freeWeylRelation omega a b → (freeWeylMap M omega) a = (freeWeylMap M omega) b

A matrix substitution preserving the prescribed commutators respects the quotient relations.

def Stafford.freeWeylSymplecticAlgHom {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M omega : Matrix ι ι k) (hpres : ∀ (i j : ι), commutator (freeWeylLinearCombination M (freeWeylGenerator omega) i) (freeWeylLinearCombination M (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) : FreeWeyl k ι omega →ₐ[k] FreeWeyl k ι omega

The endomorphism of the Weyl quotient induced by a commutator-preserving matrix substitution.

Equations

• Stafford.freeWeylSymplecticAlgHom M omega hpres = (RingQuot.liftAlgHom k) ⟨Stafford.freeWeylMap M omega, ⋯⟩

theorem Stafford.freeWeylSymplecticAlgHom_generator {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M omega : Matrix ι ι k) (hpres : ∀ (i j : ι), commutator (freeWeylLinearCombination M (freeWeylGenerator omega) i) (freeWeylLinearCombination M (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) (i : ι) : (freeWeylSymplecticAlgHom M omega hpres) (freeWeylGenerator omega i) = freeWeylLinearCombination M (freeWeylGenerator omega) i

theorem Stafford.freeWeylSymplecticAlgHom_map_linearCombination {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M N omega : Matrix ι ι k) (hpres : ∀ (i j : ι), commutator (freeWeylLinearCombination M (freeWeylGenerator omega) i) (freeWeylLinearCombination M (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) (i : ι) : (freeWeylSymplecticAlgHom M omega hpres) (freeWeylLinearCombination N (freeWeylGenerator omega) i) = freeWeylLinearCombination (N * M) (freeWeylGenerator omega) i

theorem Stafford.freeWeylLinearCombination_one {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] [DecidableEq ι] (omega : Matrix ι ι k) (i : ι) : freeWeylLinearCombination 1 (freeWeylGenerator omega) i = freeWeylGenerator omega i

theorem Stafford.freeWeylSymplecticAlgHom_comp_generator {k : Type u_1} {ι : Type u_3} [Field k] [Fintype ι] (M N omega : Matrix ι ι k) (hM : ∀ (i j : ι), commutator (freeWeylLinearCombination M (freeWeylGenerator omega) i) (freeWeylLinearCombination M (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) (hN : ∀ (i j : ι), commutator (freeWeylLinearCombination N (freeWeylGenerator omega) i) (freeWeylLinearCombination N (freeWeylGenerator omega) j) = (algebraMap k (FreeWeyl k ι omega)) (omega i j)) (i : ι) : (freeWeylSymplecticAlgHom M omega hM) ((freeWeylSymplecticAlgHom N omega hN) (freeWeylGenerator omega i)) = freeWeylLinearCombination (N * M) (freeWeylGenerator omega) i

theorem Stafford.a2_freeWeyl_symplectic_hpres {k : Type u_1} [Field k] (M : Matrix A2Index A2Index k) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) (i l : A2Index) : commutator (freeWeylLinearCombination M (freeWeylGenerator (A2SymplecticForm k)) i) (freeWeylLinearCombination M (freeWeylGenerator (A2SymplecticForm k)) l) = (algebraMap k (FreeWeyl k A2Index (A2SymplecticForm k))) (A2SymplecticForm k i l)

A symplectic change of the four generators preserves the defining Weyl commutators.

def Stafford.a2FreeWeylSymplecticHom {k : Type u_1} [Field k] (M : Matrix A2Index A2Index k) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) : FreeWeyl k A2Index (A2SymplecticForm k) →ₐ[k] FreeWeyl k A2Index (A2SymplecticForm k)

The endomorphism of the second Weyl quotient induced by a symplectic matrix.

Equations

• Stafford.a2FreeWeylSymplecticHom M hM = Stafford.freeWeylSymplecticAlgHom M (Stafford.A2SymplecticForm k) ⋯

theorem Stafford.a2_freeWeyl_symplectic_hom_generator {k : Type u_1} [Field k] (M : Matrix A2Index A2Index k) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) (i : A2Index) : (a2FreeWeylSymplecticHom M hM) (freeWeylGenerator (A2SymplecticForm k) i) = freeWeylLinearCombination M (freeWeylGenerator (A2SymplecticForm k)) i

theorem Stafford.a2_freeWeyl_symplectic_hom_comp_generator {k : Type u_1} [Field k] (M N : Matrix A2Index A2Index k) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) (hN : N * A2SymplecticForm k * N.transpose = A2SymplecticForm k) (i : A2Index) : (a2FreeWeylSymplecticHom M hM) ((a2FreeWeylSymplecticHom N hN) (freeWeylGenerator (A2SymplecticForm k) i)) = freeWeylLinearCombination (N * M) (freeWeylGenerator (A2SymplecticForm k)) i

theorem Stafford.a2_freeWeyl_symplectic_hom_comp_eq_id {k : Type u_1} [Field k] (M N : Matrix A2Index A2Index k) (hM : M * A2SymplecticForm k * M.transpose = A2SymplecticForm k) (hN : N * A2SymplecticForm k * N.transpose = A2SymplecticForm k) (hNM : N * M = 1) : (a2FreeWeylSymplecticHom M hM).comp (a2FreeWeylSymplecticHom N hN) = AlgHom.id k (FreeWeyl k A2Index (A2SymplecticForm k))

def Stafford.a2FreeWeylSymplecticEquiv {k : Type u_1} [Field k] (M : ↥(Matrix.symplecticGroup (Fin 2) k)) : FreeWeyl k A2Index (A2SymplecticForm k) ≃+* FreeWeyl k A2Index (A2SymplecticForm k)

The automorphism of the second Weyl quotient induced by a symplectic group element.

Equations

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