TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Correspondence theorem for submodules of a quotient module

Statement

For $N \leq M$ , inverse image and quotient induce mutually inverse inclusion-preserving bijections between submodules of $M / N$ and submodules of $M$ containing $N$ . They preserve sums, intersections, and successive quotients. See Quotient module $M / N$ with scalar multiplication on additive cosets.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For $N \leq M$ , the additive cosets $m + N$ form the quotient module $M / N$ under the well-defined scalar action $r (m + N) : = r m + N .$ (Quotient module $M / N$ with scalar multiplication on additive cosets).

[L2]

Let $f : M \to P$ be a module homomorphism and let $N \leq M$ satisfy $N \subseteq \ker f$ . There is a unique module homomorphism $\overset{ˉ}{f} : M / N ⟶ P$ such that $\overset{ˉ}{f} (m + N) = f (m)$ , equivalently $f = \overset{ˉ}{f} \circ π$ . (A module homomorphism vanishing on $N$ factors uniquely through $M / N$ ).

[L3]

If $N \leq L \leq M$ , then $L / N$ is a submodule of $M / N$ and $(M / N) / (L / N) ≅ M / L .$ (Third isomorphism theorem for modules).

Proof

technique · direct

1.1

Inverse image and quotient give mutually inverse inclusion-preserving bijections between submodules of $M / N$ and submodules of $M$ containing $N$ .

L1L2L3givenalgebra

2.1

If $P \leq M / N$ , then $π (π^{- 1} P) = P$ by surjectivity of $π$ ; if $L \leq M$ contains $N$ , then $π^{- 1} (L / N) = L$ . Direct calculation with inverse images gives preservation of sums and intersections, while [L3] identifies successive quotients. This proves the stated claim.

L3step 1.1givenalgebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 24 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)