Differential-order filtration on a right-ideal quotient

This file constructs the filtration induced on the actual additive quotient by a right ideal and identifies each associated graded piece with homogeneous symbols modulo the principal components of the filtered ideal. Thus the degreewise object is derived from A / I; it is not the cyclic SymbolRing / orderInitialIdeal model.

The remaining global step is to assemble these degreewise equivalences into a graded SymbolRing-module equivalence and identify its annihilator/support with orderInitialIdeal.

PresentedWeyl is a RingQuot, whose AddCommMonoid and Ring instances are declared independently. The two induced AddCommMonoid structures on a submodule of it are definitionally equal but not syntactically identical, and since Lean 4.33 instance arguments are matched only up to instance transparency. Mathlib's Submodule.hasQuotient expects the group-derived shape, so without the two alignments below no quotient ↥p ⧸ q of a differential-order piece elaborates. Both are rfl, so nothing about the k-module structure changes.

@[instance_reducible]

def Stafford38.CharacteristicFilteredQuotient.pieceAddCommMonoid (k : Type u) [Field k] {n : ℕ} (p : Submodule k (WeylIteratedEquivalence.PresentedWeyl k n)) : AddCommMonoid ↥p

The additive-monoid structure used for a filtered Weyl submodule.

Equations

• Stafford38.CharacteristicFilteredQuotient.pieceAddCommMonoid k p = p.addCommGroup.toAddCommMonoid

@[instance_reducible]

def Stafford38.CharacteristicFilteredQuotient.pieceModule (k : Type u) [Field k] {n : ℕ} (p : Submodule k (WeylIteratedEquivalence.PresentedWeyl k n)) : Module k ↥p

The scalar-module structure inherited by a filtered Weyl submodule.

Equations

• Stafford38.CharacteristicFilteredQuotient.pieceModule k p = p.module

def Stafford38.CharacteristicFilteredQuotient.rightIdealKSubmodule (k : Type u) [Field k] {A : Type u_1} [Ring A] [Algebra k A] (I : EulerSurjectivity.RightIdeal A) : Submodule k A

A right ideal, regarded only as a k-linear subspace. Its carrier is literally unchanged.

Equations

• Stafford38.CharacteristicFilteredQuotient.rightIdealKSubmodule k I = { carrier := ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Stafford38.CharacteristicFilteredQuotient.mem_rightIdealKSubmodule (k : Type u) [Field k] {A : Type u_1} [Ring A] [Algebra k A] (I : EulerSurjectivity.RightIdeal A) (a : A) : a ∈ rightIdealKSubmodule k I ↔ a ∈ I

theorem Stafford38.CharacteristicFilteredQuotient.rightIdealKSubmodule_eq_restrictScalars (k : Type u) [Field k] {A : Type u_1} [Ring A] [Algebra k A] (I : EulerSurjectivity.RightIdeal A) : rightIdealKSubmodule k I = Submodule.restrictScalars k I

def Stafford38.CharacteristicFilteredQuotient.filteredRightQuotientEquivRightQuotient (k : Type u) [Field k] {A : Type u_1} [Ring A] [Algebra k A] (I : EulerSurjectivity.RightIdeal A) : (A ⧸ rightIdealKSubmodule k I) ≃ₗ[k] EulerSurjectivity.RightQuotient I

The k-linear quotient used for the filtration is canonically the same underlying quotient as the regular right-module quotient.

Equations

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

@[reducible, inline]

abbrev Stafford38.CharacteristicFilteredQuotient.FilteredRightQuotient (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) : Type u

The additive quotient by the underlying k-subspace of a right ideal.

Equations

• Stafford38.CharacteristicFilteredQuotient.FilteredRightQuotient k I = (Stafford38.WeylIteratedEquivalence.PresentedWeyl k n ⧸ Stafford38.CharacteristicFilteredQuotient.rightIdealKSubmodule k I)

@[instance_reducible, instance 10000]

instance Stafford38.CharacteristicFilteredQuotient.filteredRightQuotientAddCommMonoid (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) : AddCommMonoid (FilteredRightQuotient k I)

Global alignment for the actual filtered quotient. Lean 4.33 matches instance arguments only up to instance transparency, and the default Submodule.Quotient.addCommMonoid is not the additive monoid derived from the quotient's AddCommGroup. Without this alignment the direct sum of the pieces below inherits an additive monoid that Submodule.hasQuotient cannot match, and FilteredQuotientSpecialFibre cannot state its quotient. This is the same repair already made below for QuotientOrderGradedPiece.

Equations

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

@[instance_reducible, instance 10000]

instance Stafford38.CharacteristicFilteredQuotient.filteredRightQuotientModule (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) : Module k (FilteredRightQuotient k I)

Equations

• Stafford38.CharacteristicFilteredQuotient.filteredRightQuotientModule k I = Submodule.Quotient.module (Stafford38.CharacteristicFilteredQuotient.rightIdealKSubmodule k I)

noncomputable def Stafford38.CharacteristicFilteredQuotient.quotientOrderPiece (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Submodule k (FilteredRightQuotient k I)

The image of the differential-order piece in the actual quotient.

Equations

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

noncomputable def Stafford38.CharacteristicFilteredQuotient.quotientOrderStrictLowerPiece (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Submodule k (FilteredRightQuotient k I)

The image of the strict lower differential-order piece in the actual quotient.

Equations

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

theorem Stafford38.CharacteristicFilteredQuotient.quotientOrderStrictLowerPiece_le (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : quotientOrderStrictLowerPiece k I N ≤ quotientOrderPiece k I N

@[reducible, inline]

abbrev Stafford38.CharacteristicFilteredQuotient.QuotientOrderGradedPiece (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Type u

The degree-N associated graded piece of the filtration induced on the actual quotient A / I.

Equations

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

@[instance_reducible, instance 10000]

noncomputable instance Stafford38.CharacteristicFilteredQuotient.quotientOrderGradedPieceAddCommMonoid (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : AddCommMonoid (QuotientOrderGradedPiece k I N)

The same global alignment for the actual graded pieces: they are the components of QuotientOrderAssociatedGraded, whose AddCommGroup instance needs the group-derived additive monoid on each component.

Equations

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

@[instance_reducible, instance 10000]

noncomputable instance Stafford38.CharacteristicFilteredQuotient.quotientOrderGradedPieceModule (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Module k (QuotientOrderGradedPiece k I N)

Equations

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

noncomputable def Stafford38.CharacteristicFilteredQuotient.orderQuotientRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Submodule k ↥(WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N)

Relations in the degree-N filtered algebra piece: an element is zero in the quotient graded piece exactly when it lies in I + F_{<N} A.

Equations

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

noncomputable def Stafford38.CharacteristicFilteredQuotient.orderPieceToQuotientPiece (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : ↥(WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N) →ₗ[k] ↥(quotientOrderPiece k I N)

The canonical map from a filtered algebra piece to the corresponding filtered piece of the actual quotient.

Equations

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

noncomputable def Stafford38.CharacteristicFilteredQuotient.orderPieceToQuotientGraded (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : ↥(WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N) →ₗ[k] QuotientOrderGradedPiece k I N

The canonical map from a filtered algebra piece to the corresponding graded piece of the actual quotient.

Equations

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

theorem Stafford38.CharacteristicFilteredQuotient.orderPieceToQuotientGraded_surjective (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Function.Surjective ⇑(orderPieceToQuotientGraded k I N)

theorem Stafford38.CharacteristicFilteredQuotient.ker_orderPieceToQuotientGraded (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : (orderPieceToQuotientGraded k I N).ker = orderQuotientRelation k I N

Exact kernel computation for the filtered quotient map.

noncomputable def Stafford38.CharacteristicFilteredQuotient.quotientOrderGradedPieceEquivRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : (↥(WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N) ⧸ orderQuotientRelation k I N) ≃ₗ[k] QuotientOrderGradedPiece k I N

The actual quotient graded piece is the filtered algebra piece modulo I + F_{<N} A.

Equations

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

noncomputable def Stafford38.CharacteristicFilteredQuotient.orderSymbolRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Submodule k ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N)

Homogeneous symbol relations arising from I + F_{<N} A. The strict lower summand maps to zero, so these are precisely the degree-N principal components contributed by filtered elements of I.

Equations

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

@[instance_reducible, instance 10000]

noncomputable instance Stafford38.CharacteristicFilteredQuotient.orderSymbolQuotientAddCommMonoid (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : AddCommMonoid (↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N) ⧸ orderSymbolRelation k I N)

Align the additive monoid structure on a degree-N symbol quotient with its additive group structure. Submodule.Quotient declares the two independently, so DirectSum's AddCommGroup instance, and hence Submodule.liftQ into the graded relation module, does not apply without this rfl alignment. Unlike the alignments above this one is global, because OrderSymbolRelationGraded is assembled from these quotients in a later module.

Equations

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

@[instance_reducible, instance 10000]

noncomputable instance Stafford38.CharacteristicFilteredQuotient.orderSymbolQuotientModule (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Module k (↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N) ⧸ orderSymbolRelation k I N)

Equations

• Stafford38.CharacteristicFilteredQuotient.orderSymbolQuotientModule k I N = Submodule.Quotient.module (Stafford38.CharacteristicFilteredQuotient.orderSymbolRelation k I N)

noncomputable def Stafford38.CharacteristicFilteredQuotient.quotientPrincipalComponentMap (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : ↥(WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N) ⧸ orderQuotientRelation k I N →ₗ[k] ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N) ⧸ orderSymbolRelation k I N

Principal component, descended to the quotient by the exact source and target relation submodules.

Equations

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

theorem Stafford38.CharacteristicFilteredQuotient.quotientPrincipalComponentMap_surjective (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Function.Surjective ⇑(quotientPrincipalComponentMap k I N)

theorem Stafford38.CharacteristicFilteredQuotient.quotientPrincipalComponentMap_injective (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : Function.Injective ⇑(quotientPrincipalComponentMap k I N)

noncomputable def Stafford38.CharacteristicFilteredQuotient.quotientOrderGradedPieceEquivSymbols (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) : QuotientOrderGradedPiece k I N ≃ₗ[k] ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N) ⧸ orderSymbolRelation k I N

Degreewise filtered-quotient bridge: the actual associated graded piece of A / I is canonically equivalent to homogeneous symbols modulo the principal components of I + F_{<N} A.

Equations

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

theorem Stafford38.CharacteristicFilteredQuotient.principalComponent_mem_orderSymbolRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) (z : WeylIteratedEquivalence.PresentedWeyl k n) (hzN : z ∈ WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N) (hzI : z ∈ I) : (WeylAssociatedGraded.principalComponentOnPiece k WeylFiltration.orderWeight N) ⟨z, hzN⟩ ∈ orderSymbolRelation k I N

Every filtered element of the right ideal contributes its principal component to the exact symbol relation in the actual quotient graded piece.

theorem Stafford38.CharacteristicFilteredQuotient.mem_orderSymbolRelation_iff (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) (P : ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N)) : P ∈ orderSymbolRelation k I N ↔ ∃ (z : WeylIteratedEquivalence.PresentedWeyl k n) (hzN : z ∈ WeylFiltration.presentedWeightPiece k WeylFiltration.orderWeight N), z ∈ I ∧ P = (WeylAssociatedGraded.principalComponentOnPiece k WeylFiltration.orderWeight N) ⟨z, hzN⟩

Exact description of the degree-N symbol relations: they are precisely the principal components of elements of I lying in F_N A.

theorem Stafford38.CharacteristicFilteredQuotient.coe_mem_orderInitialGeneratorSet_of_mem_orderSymbolRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) (P : ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N)) (hP : P ∈ orderSymbolRelation k I N) : ↑P ∈ CharacteristicInitialIdeal.orderInitialGeneratorSet k I

Every exact degree-N relation of the actual quotient is one of the generators used by the existing order initial ideal.

theorem Stafford38.CharacteristicFilteredQuotient.coe_mem_orderInitialIdeal_of_mem_orderSymbolRelation (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (N : ℕ) (P : ↥(MvPolynomial.weightedHomogeneousSubmodule k WeylFiltration.orderWeight N)) (hP : P ∈ orderSymbolRelation k I N) : ↑P ∈ CharacteristicInitialIdeal.orderInitialIdeal k I