Positive outer-Ore remainders

An element whose outer momentum support is strictly below N acquires a right coordinate factor after multiplication by x^N on either side. The cofactors remain in the concrete Euler subring.

@[instance_reducible]

noncomputable def Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialMemSubringCoordinateStage (B : Type u_1) [Ring B] [Algebra ℚ B] : Algebra ℚ ↥OreCoordinateStage.CoordinateStage

The rational scalar algebra structure on the coordinate stage.

Equations

• Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialMemSubringCoordinateStage B = Stafford38.OrePairStage.coordinateStageAlgebra

@[instance_reducible]

noncomputable def Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialMemSubringCoordinateStagePairStage (B : Type u_1) [Ring B] [Algebra ℚ B] : Algebra ℚ ↥OrePairStage.PairStage

The rational scalar algebra structure on the pair stage.

Equations

• Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialMemSubringCoordinateStagePairStage B = Stafford38.OrePairStage.pairStageAlgebra

def Stafford38.WeylEulerRemainder.HasPositiveCoordinateFactor (B : Type u_1) [Ring B] (N : ℕ) (z : ↥OrePairStage.PairStage) : Prop

Both products by x^N have a right x factor with cofactor in the Euler subring.

Equations

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

theorem Stafford38.WeylEulerRemainder.hasPositiveCoordinateFactor_zero (B : Type u_1) [Ring B] (N : ℕ) : HasPositiveCoordinateFactor B N 0

theorem Stafford38.WeylEulerRemainder.hasPositiveCoordinateFactor_add (B : Type u_1) [Ring B] {N : ℕ} {z w : ↥OrePairStage.PairStage} (hz : HasPositiveCoordinateFactor B N z) (hw : HasPositiveCoordinateFactor B N w) : HasPositiveCoordinateFactor B N (z + w)

theorem Stafford38.WeylEulerRemainder.pairCoordinate_pow_mul_coefficient (B : Type u_1) [Ring B] (b : B) (N : ℕ) : OrePairStage.pairCoordinate ^ N * OrePairStage.pairCoefficient b = OrePairStage.pairCoefficient b * OrePairStage.pairCoordinate ^ N

theorem Stafford38.WeylEulerRemainder.pairOrderedMonomial_hasPositiveCoordinateFactor (B : Type u_1) [Ring B] [Algebra ℚ B] (b : B) (a j N : ℕ) (hjN : j < N) : HasPositiveCoordinateFactor B N (OrePairStage.pairCoefficient b * OrePairStage.pairCoordinate ^ a * OrePairStage.pairMomentum ^ j)

A single ordered monomial with outer momentum exponent below N has the two required positive factorizations.

theorem Stafford38.WeylEulerRemainder.hasPositiveCoordinateFactor_of_outer_support (B : Type u_1) [Ring B] [Algebra ℚ B] (z : ↥OrePairStage.PairStage) (N : ℕ) (hsupport : ∀ j ∈ ((AlgebraicAnalysis.OreAssociativity.normalFormAddEquiv OreCoordinateStage.coordinateDerivation).symm z).support, j < N) : HasPositiveCoordinateFactor B N z

Every element whose outer momentum support lies below N has both positive right-coordinate factorizations.

theorem Stafford38.WeylEulerRemainder.support_sub_X_pow_lt (B : Type u_1) [Ring B] (H : Polynomial ↥OreCoordinateStage.CoordinateStage) (N : ℕ) (hN : H.coeff N = 1) (hgt : ∀ (j : ℕ), N < j → H.coeff j = 0) (j : ℕ) : j ∈ (H - Polynomial.X ^ N).support → j < N

theorem Stafford38.WeylEulerRemainder.normalForm_sub_X_pow_hasPositiveCoordinateFactor (B : Type u_1) [Ring B] [Algebra ℚ B] (H : Polynomial ↥OreCoordinateStage.CoordinateStage) (N : ℕ) (hN : H.coeff N = 1) (hgt : ∀ (j : ℕ), N < j → H.coeff j = 0) : HasPositiveCoordinateFactor B N (AlgebraicAnalysis.OreAssociativity.normalForm OreCoordinateStage.coordinateDerivation (H - Polynomial.X ^ N))

Subtracting the monic outer power leaves an element to which the positive factor theorem applies.

theorem Stafford38.WeylEulerRemainder.positiveEulerResidue_eq_eulerSubring_mul_coordinate (B : Type u_1) [Ring B] [Algebra ℚ B] (d sigma : ↥OrePairStage.PairStage) (N : ℕ) (hd : d = OrePairStage.pairMomentum ^ N + sigma) (hpositive : HasPositiveCoordinateFactor B N sigma) : ∃ (U : ↥(WeylEulerSubring.pairEulerSubring B)), 1 + ↑U * OrePairStage.pairCoordinate ∈ WeylEulerResidue.canonicalRightIdeal OrePairStage.pairCoordinate d N

The positive-factor interface turns the explicit Euler residue into the exact shaped residue consumed by quotient surjectivity.

theorem Stafford38.WeylEulerRemainder.closure_pairOldSubring_union_coordinate_momentum_eq_top (B : Type u_1) [Ring B] : Subring.closure (↑(WeylEulerSubring.pairOldSubring B) ∪ {OrePairStage.pairCoordinate, OrePairStage.pairMomentum}) = ⊤

The old coefficient ring together with the new coordinate and momentum generates the complete pair stage.

@[instance_reducible]

def Stafford38.WeylEulerRemainder.iteratedRatAlgebra (k : Type u) [Field k] [Algebra ℚ k] (n : ℕ) : Algebra ℚ (OreIteratedPairStage.IteratedPairStage k n)

Rational scalar algebra structures on all iterated pair stages, defined recursively.

Equations

• Stafford38.WeylEulerRemainder.iteratedRatAlgebra k 0 = id inferInstance
• Stafford38.WeylEulerRemainder.iteratedRatAlgebra k n.succ = id Stafford38.OrePairStage.pairStageAlgebra

@[instance_reducible]

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

The base-field algebra structure on an iterated pair stage.

Equations

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

@[instance_reducible]

noncomputable def Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStage (k : Type u) [Field k] [Algebra ℚ k] (n : ℕ) : Algebra ℚ ↥OreCoordinateStage.CoordinateStage

The rational scalar algebra structure on the next coordinate stage of the iteration.

Equations

• Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStage k n = Stafford38.OrePairStage.coordinateStageAlgebra

@[instance_reducible]

noncomputable def Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStagePairStage (k : Type u) [Field k] [Algebra ℚ k] (n : ℕ) : Algebra ℚ ↥OrePairStage.PairStage

The rational scalar algebra structure on the next pair stage of the iteration.

Equations

• Stafford38.WeylEulerRemainder.instAlgebraRatSubtypeEndPolynomialIteratedPairStageMemSubringCoordinateStagePairStage k n = Stafford38.OrePairStage.pairStageAlgebra

theorem Stafford38.WeylEulerRemainder.presentedRemainder_hasPositiveCoordinateFactor (k : Type u) [Field k] [Algebra ℚ k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : HasPositiveCoordinateFactor (OreIteratedPairStage.IteratedPairStage k n) N ((WeylIteratedEquivalence.presentedToIterated k (n + 1)) d - OreIteratedPairStage.stageMomentum k n ^ N)

The concrete remainder of a normalized presented Weyl operator satisfies both positive-coordinate factorizations.

theorem Stafford38.WeylEulerRemainder.presentedPositiveEulerResidue (k : Type u) [Field k] [Algebra ℚ k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : ∃ (U : ↥(WeylEulerSubring.pairEulerSubring (OreIteratedPairStage.IteratedPairStage k n))), 1 + ↑U * OrePairStage.pairCoordinate ∈ WeylEulerResidue.canonicalRightIdeal OrePairStage.pairCoordinate ((WeylIteratedEquivalence.presentedToIterated k (n + 1)) d) N

The normalized presented operator has the exact positive Euler residue in its literal canonical right ideal.

theorem Stafford38.WeylEulerRemainder.presentedCanonicalQuotient_rightMul_coordinate_surjective (k : Type u) [Field k] [Algebra ℚ k] (n N : ℕ) {d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)} (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : Function.Surjective (EulerSurjectivity.rightMul (WeylEulerResidue.canonicalRightIdeal OrePairStage.pairCoordinate ((WeylIteratedEquivalence.presentedToIterated k (n + 1)) d) N) OrePairStage.pairCoordinate)

Right multiplication by the selected coordinate is onto the concrete canonical quotient.