LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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

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

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