Research proof index

If p is an associated prime of M and p meets the multiplicative set S, then p is an associated prime of the kernel of the localization map mkLinearMap S M : M →ₗ[R] LocalizedModule S M. This is the “meets S” direction used to identify associated primes of ker (mkLinearMap S M) with the associated primes of M that are not disjoint from...

If p is an associated prime of the quotient M ⧸ ker(mkLinearMap S M) and p is disjoint from the multiplicative set S, then p is already an associated prime of M. This lemma is used to identify the “disjoint part” of the associated primes of M with the associated primes of the localization quotient.

Construct a Jordan–Hölder RelSeries from an existing filtration. Given the existence instance for JordanHolderFiltration μ, we build a RelSeries for the relation JordanHolderRel μ whose head is ⊤ and whose last element is ⊥. API note: this is the RelSeries-shaped entry point corresponding to the existence instance.

Existence of a semistable RelSeries from ⊥ to ⊤ with strictly decreasing slopes. From the canonical HarderNarasimhanFiltration μ, we build a RelSeries over the relation IntervalSemistableRel μ. The step field is given by the strict-mono successor property together with piecewise_semistable. The final conjunct states the slope strictness co...

Uniqueness of the semistable RelSeries in the complete linear order case. When S is a complete linear order, Harder–Narasimhan filtrations are unique. Using impl.hHFil_of_hNSeries, any RelSeries satisfying the slope condition produces a filtration; uniqueness of filtrations then implies uniqueness of such series (up to extensional equality).

Any coprimary filtration underlies a Harder–Narasimhan filtration. We reuse the same filtration function and verify the Harder–Narasimhan axioms: piecewise semistability (via rmk4d14₂ and semistable_res_iff_semistable_quot) and strict decrease of the minimal associated primes.