Base Change Functor

definition theorem example

For an arrow $f:b\to a$ in a category with pullbacks, the base-change functor (pullback functor, substitution)

$$f^{\ast }:\mathcal{C}/a\to \mathcal{C}/b$$

sends a fibration $⟨e,p:e\to a⟩$ to $⟨f^{\ast }e,f^{\ast }p⟩$, the pullback of $p$ along $f$, and a fiber-preserving map $h:e^{\prime }\to e$ to the unique $f^{\ast }h:f^{\ast }{e}^{\prime }\to f^{\ast }e$ induced by the universal property (DaoFP Exercise 11.2.4). Note that $f^{\ast }$ runs opposite to $f$.

Sources: DaoFP §11.2 (“Pullbacks”, “Substitution”, “Base-change functor”), Exercise 11.2.4, §11.3–11.4; 7 Sketches §7.2 (pullback of subobjects), §3.4 (${\Delta }_F$ as pullback of instances); Kittenlab Lecture 14 (pullback of a subset is its preimage).

• In $\mathbf{Set}$: $f^{\ast }E=\{(x,e)\mid f(x)=p(e)\}$. Think of $f$ as cutting the base $B$ into patches $f^{-1}(y)$ (with $A$ an atlas of patch names): $f^{\ast }E$ plants a clone of the fiber $p^{-1}(y)$ over every point of the patch $f^{-1}(y)$. Countries $A$, cities $B$, languages $E$ fibered by country: $f^{\ast }E$ assigns each city its country’s languages.
• If $a=1$: $f^{\ast }E=B\times E$, the trivial bundle. A general bundle is locally a product — a sum over patches of (patch $\times$ fiber), the atlas idea of differential geometry (Möbius strip, Klein bottle).
• Pulling back along a point $x:1\to b$ extracts the single Fiber over $x$.
• Adjoints (in a Locally Cartesian Closed Category): ${\Sigma }_f⊣f^{\ast }⊣{\Pi }_f$, i.e. $f_{!}⊣f^{\ast }⊣f_{\ast }$ — the Dependent Sum ($f_{!}(s,q)=(s,f\circ q)$) and Dependent Product. On subobjects this is ${\exists }_f⊣f^{-1}⊣{\forall }_f$ (Quantification, Direct Image, Preimage, and Dual Image).
• Type-theoretically $f^{\ast }$ is substitution: from the family $T(y)$, $y:B$, form $T(f(x))$, $x:A$. Also called weakening when $f$ is a projection $\Gamma \times X\to \Gamma$.

JuliaLeanHaskell

Docs: FinSets · Limits & colimits — Kittenlab Lecture 14

using Catlab
# base change in FinSet: pull the bundle p : E → A back along f : B → A
p = FinFunction([1, 1, 2], 2)          # E = 3 over A = 2: fibers of size 2 and 1
f = FinFunction([1, 1, 1, 2], 2)       # B = 4: patch {1,2,3} ↦ 1, patch {4} ↦ 2
P = pullback(f, p)
f_star_E = ob(P)                       # FinSet(7) = 3·2 + 1·1
f_star_p = legs(P)[1]                  # the new projection f*E → B
[length(preimage(f_star_p, x)) for x in 1:4]   # [2, 2, 2, 1]: fibers replanted over patches

import Mathlib
open CategoryTheory
#check @CategoryTheory.Over.pullback          -- (f : X ⟶ Y) : Over Y ⥤ Over X
#check @CategoryTheory.Over.mapPullbackAdj     -- Over.map f ⊣ Over.pullback f   (Σ_f ⊣ f^*)
#check @CategoryTheory.Over.pullbackComp       -- (f ≫ g)^* ≅ g^* ⋙ f^*

-- base change on finite "bundles" represented as association lists (element, base point)
type Bundle e b = [(e, b)]
baseChange :: Eq a => (b -> a) -> Bundle e a -> [b] -> Bundle (b, e) b
baseChange f bundle bs = [ ((x, e), x) | x <- bs, (e, y) <- bundle, f x == y ]