Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27
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.

A ring map induces a contraction map on prime spectra

Statement

Let φ:R→A be a ring homomorphism of commutative rings. Then contraction along φ defines a map

Spec⁡(φ):Spec⁡(A)⟶Spec⁡(R),q⟼φ−1(q).

For every ideal I⊴R, if IA denotes the ideal generated by φ(I), then

Spec⁡(φ)−1(V(I))=V(IA).

Facts & Assumptions

Given: A ring homomorphism φ:R→A of commutative rings.

[L1]

Contraction of prime ideals is well-defined and respects identities and composition (The spectrum map respects composition and identities).

[L2]

Contraction pulls back vanishing sets by the rule Spec⁡(φ)−1(V(I))=V(IA) (The spectrum map pulls back vanishing sets).

Proof

technique · direct
1.1

The first displayed assignment is well-defined on prime ideals by [L1].

L1
1.2

The stated pullback formula for vanishing sets is exactly [L2].

L2
2.1

Together, steps 1.1 and 1.2 give the spectrum map induced by φ and its basic effect on vanishing sets.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources