Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28
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 generator detects comparison of subobjects

Statement

Let G be a generator of an abelian category, and let B,CA be subobjects. Then

BCevery morphism GA factoring through B also factors through C.

Facts & Assumptions

Given: A generator G and subobjects B,CA, represented by monomorphisms b:BA and c:CA.

[L1]

A generator separates distinct morphisms by precomposition (Generator and cogenerator of a category).

[L2]

The meet BC is represented by the pullback of b and c (The meet of two subobjects is their pullback).

[L3]

In an abelian category, a morphism that is both monic and epic is an isomorphism (An abelian category is balanced).

[L4]

In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero (In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero).

[L5]

Abelian categories have cokernels (Abelian category).

Proof

technique · direct
1.1

If BC, then any map GA factoring through B also factors through C by composition.

givenalgebra
1.2

To prove the converse, assume BC. By [L2], let p:PB be the pullback subobject of b and c. If p were epic, then [L3] would make it an isomorphism, forcing b to factor through c. So p is not epic.

L2L3contrapositive-reduce
2.1

Let q:BQ be a cokernel of p, which exists by [L5]. Since p is not epic, [L4] implies q0.

L4L5step 1.2
3.1

The morphisms q and 0B,Q are therefore distinct, so [L1] gives some u:GB with qu0. If bu factored through c, the pullback property in [L2] would force u to factor through p, hence qu=0, impossible. Thus bu:GA factors through B but not through C.

L1L2step 2.1construct
4.1

Step 1.1 proves the forward implication, and steps 1.2, 2.1, and 3.1 prove the contrapositive of the reverse implication. Therefore BC exactly when every morphism GA factoring through B also factors through C.

step 1.1step 1.2step 2.1step 3.1discharge-contrapositive: reverse implication

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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