PBW monicity as concrete outer-Ore monicity

The successor-rank iterated Weyl tower is an outer Ore extension in the newest momentum. This file exposes its concrete coefficient-left polynomial, proves the exact coefficient formula relating the nested PBW normal form to that polynomial, and turns the checked PBW coefficient-one bound into Polynomial.Monic.

@[instance_reducible]

noncomputable def Stafford38.WeylOuterOreMonic.instAlgebraIteratedPairStage (k : Type u) [Field k] (n : ℕ) : Algebra k (OreIteratedPairStage.IteratedPairStage k n)

The base-field algebra structure on an iterated pair stage for outer Ore normalization.

Equations

• Stafford38.WeylOuterOreMonic.instAlgebraIteratedPairStage k n = Stafford38.WeylIteratedEquivalence.iteratedPairStageAlgebra k n

@[instance_reducible]

noncomputable def Stafford38.WeylOuterOreMonic.instAlgebraSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStage (k : Type u) [Field k] (n : ℕ) : Algebra k ↥OreCoordinateStage.CoordinateStage

The base-field algebra structure on the outer coordinate stage.

Equations

• Stafford38.WeylOuterOreMonic.instAlgebraSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStage k n = Stafford38.OrePairStage.coordinateStageAlgebra

@[instance_reducible]

noncomputable def Stafford38.WeylOuterOreMonic.instAlgebraSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStagePairStage (k : Type u) [Field k] (n : ℕ) : Algebra k ↥OrePairStage.PairStage

The base-field algebra structure on the outer pair stage.

Equations

• Stafford38.WeylOuterOreMonic.instAlgebraSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStagePairStage k n = Stafford38.OrePairStage.pairStageAlgebra

noncomputable def Stafford38.WeylOuterOreMonic.presentedOuterPolynomial (k : Type u) [Field k] (n : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : Polynomial ↥OreCoordinateStage.CoordinateStage

The polynomial in the outer Ore variable representing a presented Weyl element.

Equations

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

noncomputable def Stafford38.WeylOuterOreMonic.coordinateCoefficientNormalForm (k : Type u) [Field k] (n : ℕ) : ↥OreCoordinateStage.CoordinateStage ≃ₗ[k] Polynomial (Characteristic.SymbolRing k n)

The coordinate-stage linear normal form with coefficients in the transverse symbol ring.

Equations

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

noncomputable def Stafford38.WeylOuterOreMonic.presentedNestedNormalForm (k : Type u) [Field k] (n : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : Polynomial (Polynomial (Characteristic.SymbolRing k n))

The two-variable nested polynomial normal form of the outer Weyl pair.

Equations

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

theorem Stafford38.WeylOuterOreMonic.flatten_presentedNestedNormalForm (k : Type u) [Field k] (n : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (WeylPBW.flattenPairSymbols k n) (presentedNestedNormalForm k n d) = (WeylPBW.presentedNormalFormLinearEquiv k (n + 1)) d

theorem Stafford38.WeylOuterOreMonic.presentedNestedNormalForm_eq_mapRange (k : Type u) [Field k] (n : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : presentedNestedNormalForm k n d = (OreLinearNormalForm.polynomialMapRangeLinearEquiv (coordinateCoefficientNormalForm k n)) (presentedOuterPolynomial k n d)

noncomputable def Stafford38.WeylOuterOreMonic.pairExponent (n a p : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) : Characteristic.PhaseVar (n + 1) →₀ ℕ

The PBW exponent combining outer momentum and coordinate powers with transverse exponents.

Equations

• Stafford38.WeylOuterOreMonic.pairExponent n a p m = Stafford38.WeylFiltration.extendPhaseExponent n a p m

@[simp]

theorem Stafford38.WeylOuterOreMonic.mapDomain_oldIndex_newCoordinate (n : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) : (Finsupp.mapDomain WeylIteratedEquivalence.oldIndex m) (Sum.inl 0) = 0

@[simp]

theorem Stafford38.WeylOuterOreMonic.mapDomain_oldIndex_newMomentum (n : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) : (Finsupp.mapDomain WeylIteratedEquivalence.oldIndex m) (Sum.inr 0) = 0

theorem Stafford38.WeylOuterOreMonic.coeff_flattenPairSymbols_monomial (k : Type u) [Field k] (n a p a' p' : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) (r : Characteristic.SymbolRing k n) : ((WeylPBW.flattenPairSymbols k n) ((Polynomial.monomial p') ((Polynomial.monomial a') r))).coeff (pairExponent n a p m) = if p' = p ∧ a' = a then r.coeff m else 0

theorem Stafford38.WeylOuterOreMonic.coeff_flattenPairSymbols (k : Type u) [Field k] (n a p : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) (q : Polynomial (Polynomial (Characteristic.SymbolRing k n))) : ((WeylPBW.flattenPairSymbols k n) q).coeff (pairExponent n a p m) = ((q.coeff p).coeff a).coeff m

theorem Stafford38.WeylOuterOreMonic.coeff_polynomialMapRangeLinearEquiv (k : Type u) [Field k] {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [Algebra k R] [Algebra k S] (e : R ≃ₗ[k] S) (q : Polynomial R) (p : ℕ) : ((OreLinearNormalForm.polynomialMapRangeLinearEquiv e) q).coeff p = e (q.coeff p)

@[simp]

theorem Stafford38.WeylOuterOreMonic.degree_pairExponent (n a p : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) : Finsupp.degree (pairExponent n a p m) = p + a + Finsupp.degree (Finsupp.mapDomain WeylIteratedEquivalence.oldIndex m)

@[simp]

theorem Stafford38.WeylOuterOreMonic.pairExponent_newMomentum (n a p : ℕ) (m : Characteristic.PhaseVar n →₀ ℕ) : (pairExponent n a p m) (Sum.inr 0) = p

theorem Stafford38.WeylOuterOreMonic.nested_coeff_eq_zero_of_outer_exponent_gt (k : Type u) [Field k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) {p : ℕ} (hp : N < p) : (presentedNestedNormalForm k n d).coeff p = 0

theorem Stafford38.WeylOuterOreMonic.nested_coeff_eq_one_at_bound (k : Type u) [Field k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : (presentedNestedNormalForm k n d).coeff N = 1

theorem Stafford38.WeylOuterOreMonic.presentedNestedNormalForm_coeff (k : Type u) [Field k] (n p : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (presentedNestedNormalForm k n d).coeff p = (coordinateCoefficientNormalForm k n) ((presentedOuterPolynomial k n d).coeff p)

theorem Stafford38.WeylOuterOreMonic.coordinateCoefficientNormalForm_one (k : Type u) [Field k] (n : ℕ) : (coordinateCoefficientNormalForm k n) 1 = 1

theorem Stafford38.WeylOuterOreMonic.outer_coeff_eq_one_at_bound (k : Type u) [Field k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : (presentedOuterPolynomial k n d).coeff N = 1

theorem Stafford38.WeylOuterOreMonic.outer_coeff_eq_zero_of_exponent_gt (k : Type u) [Field k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) {p : ℕ} (hp : N < p) : (presentedOuterPolynomial k n d).coeff p = 0

theorem Stafford38.WeylOuterOreMonic.presentedOuterPolynomial_monic (k : Type u) [Field k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : (presentedOuterPolynomial k n d).Monic