Alphabeta Math
False statementConstruction: Literature-sourcedVerification: 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.

Every equivalence of categories is an isomorphism of categories

Statement

FALSE. Every equivalence of categories is an isomorphism of categories.

Facts & Assumptions

Given: The indiscrete preorder C={0,1}C=\{0,1\} and the terminal one-object category D={∗}D=\{*\}.

[L1]

Preorders define thin categories (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[L2]

Equivalence is witnessed by quasi-inverses up to natural isomorphism (Equivalence, quasi-inverse, and adjoint equivalence of categories).

[L3]

Isomorphism of categories requires a bijection on objects (A functor is an isomorphism of categories exactly when its object and morphism maps are bijective).

Refutation

technique · direct
1.1

The unique F:C→DF:C\to D and the functor G:D→CG:D\to C selecting 00 satisfy FG=1DFG=1_D. The unique arrows x→0x\to0 in the indiscrete preorder form a natural isomorphism 1C⇒GF1_C\Rightarrow GF.

L1
1.2

No functor C→DC\to D is bijective on objects because CC has two objects and DD one, so the categories are not isomorphic by [L3].

L3
2.1

Therefore FF is an equivalence by [L2].

step 1.1L2
3.1

This equivalent but nonisomorphic pair refutes the statement.

step 2.1step 1.2∎

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: 27 results over 10 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