Alphabeta MathHow 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 image-preimage adjunctions explain the set-operation preservation laws
In Direct image, preimage, and universal image form an adjoint triple on power sets, is a left adjoint, so its preservation of joins recovers the union law for images in For and : , and ; both inclusions are equalities for all and if and only if is injective. The middle functor is both a left and a right adjoint, so it preserves both joins and meets, agreeing with the union and intersection laws in For and : , , , and . The direct set proofs remain stronger as concrete formulas, including the difference law, which is not a bare consequence of adjointness.
Depends on
- Direct image, preimage, and universal image form an adjoint triple on power sets
- For $f : A \to B$ and $T, U \subseteq B$: $f^{-1}[T \cup U] = f^{-1}[T] \cup f^{-1}[U]$, $f^{-1}[T \cap U] = f^{-1}[T] \cap f^{-1}[U]$, $f^{-1}[T \setminus U] = f^{-1}[T] \setminus f^{-1}[U]$, and $f^{-1}[B \setminus T] = A \setminus f^{-1}[T]$
- For $f : A \to B$ and $S, T \subseteq A$: $f[S \cup T] = f[S] \cup f[T]$, $f[S \cap T] \subseteq f[S] \cap f[T]$ and $f[S] \setminus f[T] \subseteq f[S \setminus T]$; both inclusions are equalities for all $S$ and $T$ if and only if $f$ is injective
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: 26 results over 10 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
- Emily Riehl, Category Theory in Context, 2nd ed., Example 4.1.8 (standard reference, not scraped)