Strict filtered endomorphisms

A strict surjective endomorphism of a filtered module is surjective on every subquotient of the filtration. The formulation here uses only submodules and their quotients; it does not introduce a separate associated-graded framework.

def AlgebraicAnalysis.FilteredStrictness.IsStrict {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F : ℕ → Submodule R M) (f : M →ₗ[R] M) : Prop

An endomorphism is strict for F when its image of every filtration piece is the intersection of that piece with its global range.

Equations

• AlgebraicAnalysis.FilteredStrictness.IsStrict F f = ∀ (n : ℕ), Submodule.map f (F n) = F n ⊓ f.range

@[reducible, inline]

abbrev AlgebraicAnalysis.FilteredStrictness.GradedQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F : ℕ → Submodule R M) (hF : Monotone F) (lower upper : ℕ) (h : lower ≤ upper) : Type u_2

The filtration subquotient F upper / F lower, represented inside F upper. The monotonicity assumption identifies the denominator with the expected copy of F lower.

Equations

• AlgebraicAnalysis.FilteredStrictness.GradedQuotient F hF lower upper h = (↥(F upper) ⧸ (Submodule.inclusion ⋯).range)

def AlgebraicAnalysis.FilteredStrictness.gradedQuotientMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F : ℕ → Submodule R M) (hF : Monotone F) (f : M →ₗ[R] M) (hpres : ∀ (n : ℕ), ∀ x ∈ F n, f x ∈ F n) (lower upper : ℕ) (h : lower ≤ upper) : GradedQuotient F hF lower upper h →ₗ[R] GradedQuotient F hF lower upper h

The endomorphism induced on a filtration subquotient.

Equations

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

theorem AlgebraicAnalysis.FilteredStrictness.gradedQuotientMap_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F : ℕ → Submodule R M) (hF : Monotone F) (f : M →ₗ[R] M) (hpres : ∀ (n : ℕ), ∀ x ∈ F n, f x ∈ F n) (hstrict : IsStrict F f) (hsurj : Function.Surjective ⇑f) (lower upper : ℕ) (h : lower ≤ upper) : Function.Surjective ⇑(gradedQuotientMap F hF f hpres lower upper h)

A globally surjective filtration-preserving strict endomorphism induces a surjection on every filtration subquotient, hence on each graded piece.