TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16

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.

Direct image, preimage, and universal image form an adjoint triple on power sets

Statement

For a function $f : A \to B$ , order the power sets by inclusion and define

$f_{!} (S) : = f [S], f^{- 1} (T) : = {a \in A : f (a) \in T},$

$f_{*} (S) : = {b \in B : f^{- 1} [{b}] \subseteq S} .$

Then

$f_{!} ⊣ f^{- 1} ⊣ f_{*} .$

Thus direct image is left adjoint to preimage, and universal image is right adjoint to preimage. The notation $f_{*}$ here always denotes universal image.

Facts & Assumptions

Given: A function $f : A \to B$ , subsets $S \subseteq A$ and $T \subseteq B$ .

[F1]

For a relation, image and preimage are $R [A] = {b : \exists a \in A ((a, b) \in R)}$ and $R^{- 1} [B] = {a : \exists b \in B ((a, b) \in R)}$ (The image $R [A]$ and the preimage $R^{- 1} [B]$ of a set under a relation).

[L1]

For posets, an adjunction is a Galois connection: $P (x) \leq y$ if and only if $x \leq Q (y)$ (Galois connection between preorders).

Proof

technique · direct

1.1F1

By [F1], $f [S] \subseteq T$ means that every $a \in S$ satisfies $f (a) \in T$ , which is equivalent to $S \subseteq f^{- 1} [T]$ .

1.2F1

The inclusion $f^{- 1} [T] \subseteq S$ means that whenever $b \in T$ , every $a$ in the fibre $f^{- 1} [{b}]$ lies in $S$ ; this is equivalent to $T \subseteq f_{*} (S)$ .

2.1step 1.2

Step 1.2 also covers an empty fibre, because the empty set is a subset of every $S$ ; hence no surjectivity hypothesis on $f$ is present.

3.1step 1.1step 1.2L1∎

Applying [L1] to steps 1.1 and 1.2 gives $f_{!} ⊣ f^{- 1}$ and $f^{- 1} ⊣ f_{*}$ , respectively.

Depends on

Used by

The image-preimage adjunctions explain the set-operation preservation laws Remark

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

Emily Riehl, Category Theory in Context, 2nd ed., Example 4.1.8 (standard reference, not scraped)