Alphabeta Math
False statementConstruction: AI-adaptedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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.

FALSE: the integral notation of Yoneda's original paper means the same as the modern one

Statement

False claim: the integral signs used in Yoneda's 1960 paper carry the same meaning as the modern ones, so a formula copied from that paper may be read directly with the conventions in force on this page (The end and the coend of a functor Cop×C→D, Orientation and notation conventions in force on this page).

Facts & Assumptions

Given: The notation fixed on this page, and the historical record of Yoneda's 1960 paper as reported by the sources listed in this item's references.

[F1]

The vertex of an end is written ∫cT(c,c) and the vertex of a coend ∫cT(c,c), so the subscripted integral denotes the end and the superscripted one the coend (The end and the coend of a functor Cop×C→D).

[L1]

The conventions in force on this page fix, among others, that the subscripted integral denotes the end and the superscripted integral the coend (Orientation and notation conventions in force on this page).

[A1]

Reported by Loregian, Remark 1.1.14, and by Richter, Remark 4.6.2: Yoneda's 1960 paper calls integration the operation now called the coend and writes it with the subscripted integral sign, and calls cointegration the operation now called the end, writing it with a starred superscript. Loregian, Remark 1.1.16, records further that the opposite of the modern convention adopted here is also in current use.

Refutation

technique · direct
1.1

On this page the subscripted integral names the terminal wedge and the superscripted integral the initial cowedge, by [F1] and [L1]. These are the two conventions the claim proposes to read a historical formula against.

F1L1given
2.1

By [A1] the historical notation attaches the subscripted sign to what is here the superscripted one. So the same symbol names the end on this page and the coend in that paper, and the two readings of one formula differ whenever the end and the coend of the integrand differ.

A1step 1.1
3.1

They do differ in general: the page's own witness on the walking arrow with the hom-bifunctor as integrand has a one-element end and a two-element coend. Hence the claim is false, and a formula transcribed from the 1960 paper must have its integral signs exchanged before it is read with the conventions of [L1]. The mathematics is unaffected by the transcription; only the symbols move.

A1L1step 2.1∎

Remarks

The refutation is documentary, and deliberately so. It makes no claim about what the historical paper proves, only about which symbol it attaches to which construction, and that is reported by the two references listed above rather than asserted here.

A reader converting between conventions needs one rule and no mathematics: exchange subscript and superscript, and check the source's own statement of its convention rather than assuming the modern one. That the opposite convention is also in current use, and not only historical, is what makes the check worth performing every time.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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