Exact filtered Schreyer criterion

This file isolates the abstract equivalence used when a right-linear presentation is combined with a lower filtration piece. The right action is encoded by the opposite scalar ring, while the lower piece is only an additive subgroup. No Ore, Weyl, or characteristic-variety structure is needed.

theorem AlgebraicAnalysis.FilteredSchreyer.map_rightSMul {A : Type u} {E : Type v} [Ring A] [AddCommGroup E] [Module Aᵐᵒᵖ E] (phi : E →ₗ[Aᵐᵒᵖ] A) (b : E) (x : A) : phi (MulOpposite.op x • b) = phi b * x

A right-linear presentation map sends the explicit right action on its source to right multiplication in the target ring.

theorem AlgebraicAnalysis.FilteredSchreyer.range_add_lower_iff_preimage_add_rightMultiple {A : Type u} {E : Type v} [Ring A] [AddCommGroup E] [Module Aᵐᵒᵖ E] (phi : E →ₗ[Aᵐᵒᵖ] A) (L : AddSubgroup A) (a : E) (C x : A) (ha : phi a = 1 + C * x) (hone : 1 ∈ L) (hLx : ∀ z ∈ L, z * x ∈ L) (hstrict : ∀ (z : A), z * x ∈ L → z ∈ L) : (∃ (b : E), ∃ l ∈ L, C = phi b + l) ↔ ∃ (t : E) (b : E), phi t ∈ L ∧ a = t + MulOpposite.op x • b

Exact filtered Schreyer criterion for one distinguished right action.

The left side says that C lies in the image of phi modulo the lower subgroup L. The right side expresses the corresponding source relation as an element mapping into L, plus an explicit right multiple of x. The hypotheses separate the two directions: right-coordinate stability is used forward, and strictness under that coordinate is used backward.