Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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→B, order the power sets by inclusion and define

f!(S):=f[S],f−1(T):={a∈A:f(a)∈T},

f∗(S):={b∈B:f−1[{b}]⊆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→B, subsets S⊆A and T⊆B.

[F1]

For a relation, image and preimage are R[A]={b:∃a∈A ((a,b)∈R)} and R−1[B]={a:∃b∈B ((a,b)∈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)≤y if and only if x≤Q(y) (Galois connection between preorders).

Proof

technique · direct
1.1

By [F1], f[S]⊆T means that every a∈S satisfies f(a)∈T, which is equivalent to S⊆f−1[T].

F1
1.2

The inclusion f−1[T]⊆S means that whenever b∈T, every a in the fibre f−1[{b}] lies in S; this is equivalent to T⊆f∗(S).

F1
2.1

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.

step 1.2
3.1

Applying [L1] to steps 1.1 and 1.2 gives f!⊣f−1 and f−1⊣f∗, respectively.

step 1.1step 1.2L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 18 results over 9 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