Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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: ideals of R/IR/I correspond to ideals of RR containing II

Statement

Correspondence theorem: ideals of R/IR/I correspond to ideals of RR containing II.

For I⊴RI\mathrel{\trianglelefteq}R, J↦J/IJ\mapsto J/I and K↦π−1(K)K\mapsto\pi^{-1}(K) are inverse inclusion-preserving bijections between ideals JJ of RR containing II and ideals KK of R/IR/I.

Facts & Assumptions

Given: An ideal I⊴RI\mathrel{\trianglelefteq}R and π:R→R/I\pi:R\to R/I.

[L1]

π\pi is a surjective ring homomorphism with kernel II (The canonical projection R→R/IR\to R/I is a surjective ring homomorphism with kernel II).

[L2]

Kernels of ring homomorphisms are ideals (The kernel of a ring homomorphism is a two-sided ideal).

[L3]

Ideals are additive subgroups with absorption (Left, right and two-sided ideals).

[L4]

R/IR/I is a ring (For a two-sided ideal II, the additive cosets form a ring R/IR/I with identity 1+I1+I).

Proof

technique · direct
1.1

If JJ contains II, then J/I=π[J]J/I=\pi[J] is an ideal of R/IR/I; if KK is an ideal of R/IR/I, then π−1(K)\pi^{-1}(K) is an ideal containing II.

L1L2L3L4givenconstruct
2.1

Surjectivity gives π[π−1(K)]=K\pi[\pi^{-1}(K)]=K, and I⊆JI\subseteq J gives π−1(π[J])=J\pi^{-1}(\pi[J])=J; inclusion is preserved.

step 1.1L1L2L3L4givenalgebra
3.1

Therefore the two assignments give the claimed correspondence.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 14 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