Direct Image, Preimage, and Dual Image

example definition theorem program

Let $f:A\to B$ be a Function — think of $A$ as apples, $B$ as buckets, and $f$ as putting each apple in a bucket. Three monotone maps between the power sets are induced automatically, forming two Galois connections $f_{!}⊣f^{\ast }⊣f_{\ast }$:

map	formula	apples & buckets
preimage / pullback $f^{\ast }:\mathcal{P}(B)\to \mathcal{P}(A)$	$f^{\ast }(B^{\prime })=f^{-1}(B^{\prime })=\{a\mid f(a)\in B^{\prime }\}$	all apples in the chosen buckets
direct image $f_{!}:\mathcal{P}(A)\to \mathcal{P}(B)$ (left adjoint)	$f_{!}(A^{\prime })=\{b\mid \exists a\in A^{\prime }.f(a)=b\}$	buckets containing at least one chosen apple
dual image $f_{\ast }:\mathcal{P}(A)\to \mathcal{P}(B)$ (right adjoint)	$f_{\ast }(A^{\prime })=\{b\mid \forall a.f(a)=b\Rightarrow a\in A^{\prime }\}$	buckets all of whose apples are chosen (empty buckets count)

Sources: 7 Sketches Example 1.117, Exercise 1.118; Kittenlab Lecture 14 (“Pullback”, “Direct image”); DaoFP §11.3–11.4 (dependent sum and product as adjoints to substitution), §7.4.4 of 7 Sketches (quantification); CTfS Example 3.4.3.2, Exercise 3.4.3.4, §5.1.1.10 (“Quantifiers as adjoints”)

Kittenlab (Lecture 14) phrases the same in terms of characteristic functions: $f^{\ast }(\chi )=\chi \circ f$ (“pullback”, also “preimage”), and $f_{\ast }(\chi )(y)=[\exists x.\chi (x)\wedge f(x)=y]$ (its $f_{\ast }$ is 7 Sketches’ $f_{!}$). Both preserve the ordering of subsets, making $\mathcal{P}$ a contravariant and a covariant Functor $\mathbf{Set}\to \mathbf{Pos}$.

Proof that $f^{\ast }$ is monotone (Kittenlab): if $\chi \subseteq {\chi }^{\prime }$ and $f^{\ast }(\chi )(x)$ holds then $\chi (f(x))$, hence ${\chi }^{\prime }(f(x))$, hence $f^{\ast }({\chi }^{\prime })(x)$. $■$

Why it matters. “We did not invent these mappings: they were induced by $f$. It is one of the pleasures of category theory that adjoints so often turn out to have interesting semantic interpretations.” The adjoints $f_{!}⊣f^{\ast }⊣f_{\ast }$ are the existential and universal quantifiers ${\exists }_f⊣f^{\ast }⊣{\forall }_f$ of topos logic (7 Sketches §7.4.4) and, at the level of categories, the Dependent Sum ${\Sigma }_f⊣f^{\ast }⊣{\Pi }_f$ Dependent Product adjoints to the base-change (DaoFP Ch. 11); for databases, ${\Sigma }_F⊣{\Delta }_F⊣{\Pi }_F$ (Data Migration Functor).

Example (7S Exercise 1.118 solution): $X=\{a_1,c_1,c_2\}\to Y=\{a,b,c\}$ projecting down. $f^{\ast }\{a,b\}=\{a_1\}$, $f^{\ast }\{c\}=\{c_1,c_2\}$; $f_{!}\{a_1,c_1\}=\{a,c\}$; $f_{\ast }\varnothing =\{b\}$ (the empty bucket), $f_{\ast }\{a_1,c_1\}=\{a,b\}$.

JuliaLeanHaskell

Docs: FinSets — Kittenlab Lecture 14

Builds on: Category (FinFunction) — run that note’s Julia code first.

# Kittenlab Lecture 14 on subsets of {1..n} as BitVectors
struct FinSet′; n::Int end
struct FinFunction′; dom::FinSet′; codom::FinSet′; values::Vector{Int} end
const FinSubset = BitVector
 
pullback_subset(f::FinFunction′, U::FinSubset) = FinSubset([U[y] for y in f.values])   # f^*
 
function direct_image(f::FinFunction′, U::FinSubset)                                 # f_!
  V = FinSubset(zeros(Bool, f.codom.n))
  for i in 1:f.dom.n
    U[i] && (V[f.values[i]] = true)
  end
  V
end
 
function dual_image(f::FinFunction′, U::FinSubset)                                   # f_*
  FinSubset([all(U[i] for i in 1:f.dom.n if f.values[i] == y) for y in 1:f.codom.n])
end
 
f = FinFunction′(FinSet′(3), FinSet′(3), [1, 3, 3])   # a₁ ↦ a, c₁,c₂ ↦ c
direct_image(f, FinSubset([true, true, false]))        # {a, c}
dual_image(f, FinSubset([false, false, false]))        # {b}: the empty bucket

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab (a separate session): fibers of a FinFunction
using Catlab
g = FinFunction([1, 3, 3], 3)
preimage(g, 3)          # [2, 3]

#check @Set.image        -- f '' A  = f_! A
#check @Set.preimage     -- f ⁻¹' B = f^* B
-- the two Galois connections
#check @Set.image_preimage   -- GaloisConnection (Set.image f) (Set.preimage f)
#check @Set.preimage_kernImage -- GaloisConnection (Set.preimage f) (Set.kernImage f)  (f_* = kernImage)

type Subset a = a -> Bool
 
preimage :: (a -> b) -> Subset b -> Subset a
preimage f chi = chi . f                                        -- f^*
 
directImage :: Eq b => [a] -> (a -> b) -> Subset a -> Subset b
directImage as f chi b = or  [chi a | a <- as, f a == b]        -- f_! : ∃
 
dualImage :: Eq b => [a] -> (a -> b) -> Subset a -> Subset b
dualImage as f chi b = and [chi a | a <- as, f a == b]          -- f_* : ∀