Alphabeta Math
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.

✓ 9 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Exactness and the Member Calculus — Examples

1 · Prerequisites

2 · Summary

These examples keep the categorical language concrete. The first group shows how members look inside abelian groups, where honest elements coexist with members but do not exhaust them. The later examples work through short exact sequences and the composite kernel-cokernel sequence explicitly, so the reader can see where the abstract exactness lemmas differ from ordinary element manipulation and where they coincide.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

Members of an abelian group correspond to its subgroups

Example

In Ab, a member x:X→A corresponds exactly to the subgroup im⁡(x)≤A. Two members are equivalent exactly when they have the same image subgroup. Thus the member-calculus bijection of Members modulo equivalence correspond to subobjects becomes the usual identification of subgroup data with image subgroups.

Facts & Assumptions

Given: An abelian group A and a homomorphism x:X→A.

[L1]

The category Ab is abelian (Abelian groups form an abelian category).

[L2]

Member-equivalence classes correspond to subobjects (Members modulo equivalence correspond to subobjects).

Verification

technique · direct
1.1L1L2

In Ab, subobjects of A are exactly subgroup inclusions into A, so [L2] identifies the class of x with the subgroup represented by its image inclusion.

2.1step 1.1∎

Therefore the abstract member-subobject correspondence is, in this category, the ordinary rule x↦im⁡(x).

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

An ordinary element as the member from the integers

Example

Let A be an abelian group and let a∈A. The homomorphism xa:Z→A,xa(n)=na, is a member of A in the sense of Member of an object. Its associated subobject is the cyclic subgroup generated by a.

Facts & Assumptions

Given: An abelian group A and an element a∈A.

[L1]

A member of an object is just a morphism into it (Member of an object).

[L2]

Member classes correspond to subobjects (Members modulo equivalence correspond to subobjects).

[L3]

The category Ab is abelian (Abelian groups form an abelian category).

Verification

technique · direct
1.1L1L3

The map xa is a group homomorphism Z→A, hence a member of A by [L1].

2.1L2step 1.1∎

Its image is the subgroup ⟨a⟩, so [L2] identifies the corresponding subobject with the cyclic subgroup generated by a.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

A general member of an abelian group need not come from an element

Statement refuted

Every member of an abelian group is equivalent to one arising from an ordinary element, that is, from a morphism Z→A.

Facts & Assumptions

Given: The identity member 1Z2:Z2→Z2.

[L1]

Member classes correspond to subobjects (Members modulo equivalence correspond to subobjects).

[L2]

The category Ab is abelian (Abelian groups form an abelian category).

Counterexample

technique · direct
1.1L1L2

The image of the member 1Z2 is all of Z2. By [L1], its equivalence class corresponds to the whole subgroup Z2≤Z2.

2.1L1step 1.1algebra

Any member coming from a map Z→Z2 has cyclic image, because the image of Z is generated by the image of 1. The subgroup Z2 is not cyclic. Therefore 1Z2 is not equivalent to any member Z→Z2.

3.1step 2.1∎

This refutes the statement.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

A member chase verifying monicity

Example

Consider the inclusion i:2Z↪Z. If x:X→2Z is a member with ix≡0, then ix=0 on a common epic cover, so already x≡0. This is the member-calculus proof that i is monic.

Facts & Assumptions

Given: The inclusion i:2Z↪Z.

[L1]

Monicity is detected by the implication ix≡0⇒x≡0 (Monicity is detected by members).

[L2]

Member cancellation is an equivalent reformulation (Monicity by member cancellation).

[L3]

The category Ab is abelian (Abelian groups form an abelian category).

Verification

technique · direct
1.1L1L3algebra

If ix≡0, choose an epic cover u:W→X with ixu=0. Since i is the subgroup inclusion, xu=0. Hence x≡0.

2.1L1L2step 1.1∎

By [L1], this proves that i is monic; by [L2], it is the same computation as cancellation of equal members after applying i.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The covering criterion checked in abelian groups

Example

For the short exact sequence 0→2Z→iZ→qZ/2→0, the covering criterion says that every homomorphism h:W→Z with qh=0 factors through i after the trivial epic cover 1W:W→W.

Facts & Assumptions

Given: The displayed short exact sequence in Ab.

[L1]

The covering criterion is equivalent to exactness (The covering criterion for exactness).

[L2]

The category Ab is abelian (Abelian groups form an abelian category).

Verification

technique · direct
1.1L2algebraconstruct

If qh=0, then every value of h is even, so h(W)⊆2Z. Therefore there is a unique homomorphism l:W→2Z with h=il.

2.1L1step 1.1∎

This realizes the cover in [L1] with V=W and k=1W. So the exactness criterion is visible here without any nontrivial refinement of domains.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

The kernel-cokernel sequence of a composite of module maps

Example

In Z-Mod, take f:Z→Z,f(n)=2n,g:Z→Z/2,g(n)=n mod 2. Then gf=0, and the sequence of The kernel-cokernel sequence of a composite becomes 0→0→Z→×22Z→0Z/2→1Z/2Z/2→0→0, which is exact.

Facts & Assumptions

Given: The maps f and g in Z-Mod.

[L1]

Module categories are abelian (Modules over a ring form an abelian category).

[L2]

Every composite has the kernel-cokernel exact sequence (The kernel-cokernel sequence of a composite).

Verification

technique · direct
1.1L1algebra

Here ker⁡(f)=0, ker⁡(gf)=Z, ker⁡(g)=2Z, coker⁡(f)≅Z/2, coker⁡(gf)≅Z/2, and coker⁡(g)=0.

2.1L2step 1.1algebra

The map ker⁡(gf)→ker⁡(g) is just f, so it is multiplication by 2 onto the subgroup 2Z. The connecting map ker⁡(g)→coker⁡(f) is zero because it is induced by the cokernel map qf:Z→Z/2, which kills every even integer. The map coker⁡(f)→coker⁡(gf) is the identity on Z/2, and the remaining arrows are the obvious zero maps. This is the displayed sequence.

3.1step 2.1algebra∎

That concrete sequence is exact by direct inspection.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A non-split short exact sequence of abelian groups

Statement refuted

Every short exact sequence of abelian groups splits.

Facts & Assumptions

Given: The short exact sequence 0→Z→×2Z→qZ/2→0.

[L1]

The category Ab is abelian (Abelian groups form an abelian category).

[L2]

A short exact sequence splits exactly when the quotient map has a section (Split short exact sequence in an abelian category, Splitting lemma in an abelian category).

Counterexample

technique · direct
1.1L1givenalgebra

The sequence is short exact in Ab by the usual kernel-image computation.

1.2L2assume-hypalgebra

If q had a section s, then x:=s(1+2Z) would be an odd integer with 2x=s(0)=0, impossible in Z. So no section exists.

2.1L2step 1.1step 1.2∎

By [L2], the short exact sequence is nonsplit. This refutes the statement.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

The splitting lemma instantiated at the published module theorem

Example

The categorical splitting lemma Splitting lemma in an abelian category specializes in R-Mod to the published module statement The splitting lemma for short exact sequences of modules. The section, retraction, and direct-sum identity are literally the same equations.

Facts & Assumptions

Given: A short exact sequence of modules together with either a section of its quotient map or a retraction of its inclusion.

[L1]

From either a section or a retraction, the categorical splitting lemma produces the unique complementary retraction or section (Splitting lemma in an abelian category).

[L2]

The published module splitting lemma states the same criterion in the module category (The splitting lemma for short exact sequences of modules).

Verification

technique · direct
1.1givenL1L2

A short exact sequence of modules is a short exact sequence in an abelian category, and the given section or retraction is exactly the additional datum required by [L1].

2.1L1L2step 1.1

The complementary map produced by [L1] satisfies ps=1, ri=1, and ir+sp=1, exactly the module equations stated in [L2].

3.1step 2.1∎

Therefore the module theorem is the concrete R-Mod instance of the categorical one.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The kernel row failure for multiplication by two computed

Example

For the multiplication-by-two morphism of short exact sequences used in The kernel row of a morphism of short exact sequences need not be short exact, the kernel row is 0→0→0→Z/2, so its failure to be short exact is visible before one ever constructs the snake connecting map.

Facts & Assumptions

Given: The multiplication-by-two diagram of the cited counterexample.

[L1]

That diagram lives in the abelian category Ab (Abelian groups form an abelian category).

[L2]

The cited counterexample computes the kernel row and shows it is not short exact (The kernel row of a morphism of short exact sequences need not be short exact).

Verification

technique · direct
1.1L1L2algebra

The vertical kernels are 0, 0, and Z/2, so the kernel row is exactly 0→0→0→Z/2.

2.1L2step 1.1algebra

The last arrow is the zero map 0→Z/2, hence not epic.

3.1step 2.1∎

So the row cannot be short exact.

Sources