LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

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 pullback of a monomorphism is a monomorphism, and a pushout of an epimorphism is an epimorphism

Statement

In a pullback square

if $m$ is monic, then $p$ is monic. Dually, in a pushout square, the pushout of an epimorphism is an epimorphism.

Facts & Assumptions

Given: The displayed pullback and a monomorphism $m$ .

[F1]

The pullback legs satisfy $f p = m q$ and have the stated universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

Pullback legs are jointly monic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

[F2]

A monomorphism cancels on the left and an epimorphism cancels on the right (Monomorphism and epimorphism by left and right cancellation).

[L2]

Pullbacks dualize to pushouts (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · cancellation

1.1

Let $r, s : W \to P$ satisfy $p r = p s$ . Then $m q r = f p r = f p s = m q s$ by the pullback equation.

F1givenalgebra

2.1

Since $m$ is monic, [F2] gives $q r = q s$ . The two pullback legs now have equal composites with $r$ and $s$ , so [L1] gives $r = s$ . Thus $p$ is monic.

F2L1step 1.1

3.1

Reversing the displayed square changes the pullback into a pushout, $m$ into an epimorphism, and the conclusion into epicity of its pushout. Applying [L2] to steps 1.1 and 2.1 proves the dual assertion.

L2step 1.1step 2.1∎

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: 12 results over 8 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

E. Riehl, Category Theory in Context, Exercise 3.1.v (standard reference, not scraped)