context | F:(a→z←b)⟶C |
definition | ⟨Fa×FzFb,π⟩:=limF |
Here we consider a functor F from the category a→z←b, consisting of three object and two non-identity arrows fa and fb, to a category C.
For readability, let's write A≡Fa,B≡Fb,Z≡Fz,α≡fa and β≡fb.
(In the picture we have X≡Fa,Y≡Fb,Z≡Fz,f≡fa,g≡fb and the pullback object is P≡X×ZY.)
Consider two arrows γ:C[X,A] and δ:C[X,B], which fulfill the structural condition α∘γ=β∘δ. I.e. when forwarded to Z via α, resp. β, they collapse into a single arrow.
Such two arrows γ,δ can be partially glued together, in the sense that they can both be written as a unique arrow u (with codomain A×ZB) followed by the projections πa,πb.
The pullback object A×ZB is the full solution to the equation posed by α and β. In Set, it's literally the set of pairs ⟨x,y⟩∈A×ZB⊆A×B, for which α(x)=β(y).
When the category contains a terminal object 1 (where α and β are trivial arrows and form a trivial condition), we have A×1B≅A×B.
The universal property says that all other solution embed in this object, in this is what is meant by full solution.
(In the picture, f is α and g,f are our γ,δ.)
A finite pullback in Set that I just made up:
Fa={2,4,6,8}, Fb={10,20}, Fz={77,88,99}
F(fa)(2)=77, F(fa)(4)=77, F(fa)(6)=88, F(fa)(8)=99
F(fb)(10)=88, F(fb)(20)=77
Then
Fa×FzFb={⟨2,20⟩,⟨4,20⟩,⟨6,10⟩}
and π are projections like for the product.
Two more prominent examples:
Digression: The exponential object BA is a prominent example of an object which isn't a limit, but it can be specifies via universal morphism construction. For sets or types, that's the function space A→B and for propositions it's the implication. If a category has product, exponential object and a terminal object, then it's called Cartesian closed. A Cartesian closed category with subobject classifier is a topos. We see now how a topos is a general kind of set theory, and simultaneously defines an internal logic.
Wikipedia: Pullback (category theory), Subobject classifier