Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Under the Axiom of Choice, every epimorphism in Set\mathbf{Set} is a split epimorphism

Statement

Assume the Axiom of Choice. Every epimorphism in Set\mathbf{Set} is a split epimorphism.

Facts & Assumptions

Given: An epimorphism p:X→Yp:X\to Y in Set\mathbf{Set}.

[L1]

Epimorphisms in Set\mathbf{Set} are precisely surjections (In Set\mathbf{Set}, monomorphisms are exactly injections and epimorphisms are exactly surjections).

[L2]

The Axiom of Choice selects an element from every member of a set-indexed family of nonempty sets (The Axiom of Choice), and a split epimorphism has a right inverse (Split monomorphism, split epimorphism, retraction, and section).

Proof

technique · direct
1.1

By [L1], every fibre p−1({y})p^{-1}(\{y\}) for y∈Yy\in Y is nonempty.

givenL1
2.1

By [L2], choose s(y)∈p−1({y})s(y)\in p^{-1}(\{y\}) for every y∈Yy\in Y; if YY is empty this is the unique empty function, so the same construction covers that boundary case.

step 1.1L2choose
3.1

Then p(s(y))=yp(s(y))=y for every yy, so p∘s=1Yp\circ s=1_Y and pp is split epic.

step 2.1L2∎

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: 17 results over 5 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