TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

The meet of two subobjects is their pullback

Statement

Let $B$ and $C$ be subobjects of an object $A$ in an abelian category, represented by monomorphisms $b : B ↣ A$ and $c : C ↣ A$ . Then the meet $B \land C$ in the subobject order is represented by the pullback of $b$ and $c$ .

Facts & Assumptions

Given: Monomorphisms $b : B ↣ A$ and $c : C ↣ A$ .

[L1]

Pullbacks are defined by their commutative square and universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L2]

A pullback of a monomorphism is a monomorphism (A pullback of a monomorphism is a monomorphism, and a pushout of an epimorphism is an epimorphism).

[L3]

Subobject inequalities are factorization relations between representatives (Subobjects and quotient objects form oppositely oriented partially ordered collections).

Proof

technique · direct

1.1L1L2L3

Form a pullback square tikzcd P \arrow[r, "q"] \arrow[d, "p"'] & C \arrow[d, "c"] \\ B \arrow[r, "b"'] & A. By [L2], the pullback leg $p$ is monic, so the composite $m : = b p = c q : P \to A$ is monic as well. Because $m$ factors through both $b$ and $c$ , it is a lower bound of the two subobjects.

1.2L1L3construct

Let $n : N ↣ A$ be any lower bound. Then $n = b u = c v$ for some $u : N \to B$ and $v : N \to C$ . By the pullback universal property [L1], there is a unique $w : N \to P$ with $p w = u$ and $q w = v$ . Therefore $m w = b u = n$ , so $n$ factors through $m$ . Hence $n \leq m$ .

2.1L3step 1.1step 1.2∎

Steps 1.1 and 1.2 show that $m$ is a lower bound above every other lower bound. By [L3], the pullback subobject is exactly $B \land C$ .

Depends on

Dependency tree · 2 levels

Sources

Daniel Murfet, Abelian Categories, Section 4.2