Maximal-submodule splice

These are lattice-theoretic module lemmas used by finite-length correction arguments. They contain no finite-length, Ore, or differential-operator assumption. The hypotheses that construct the relevant submodules remain with the application.

theorem AlgebraicAnalysis.Splice.isCoatom_of_covBy_sup_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N N' U : Submodule R M} (hNU : N ≤ U) (hNN' : N ⋖ N') (hsup : N' ⊔ U = ⊤) (hUtop : U ≠ ⊤) : IsCoatom U

A simple layer turns a proper submodule whose sum with the layer is top into a maximal submodule.

theorem AlgebraicAnalysis.Splice.maximal_submodule_splice {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N' U H : Submodule R M} (hsupU : N' ⊔ U = ⊤) (hUH : U ≤ H) (hN'H : N' ≤ H) : H = ⊤

A submodule containing both terms of a spanning pair is the whole module.

theorem AlgebraicAnalysis.Splice.exists_affine_correction_mod_simple_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Submodule R M} (v : M) (hv : v ∈ P) (hsimple : IsSimpleModule R (M ⧸ P)) (alpha : R) (hescape : ∃ (delta : M), alpha • delta ∉ P) : ∃ (delta : M), R ∙ P.mkQ (v - alpha • delta) = ⊤

If v lies in P and some scalar multiple of a vector escapes P, then the class of the corresponding affine correction generates the simple quotient.