Theory Category3.CategoryWithPullbacks
chapter "Category with Pullbacks"
theory CategoryWithPullbacks
imports Limit
begin
text ‹
\sloppypar
In this chapter, we give a traditional definition of pullbacks in a category as
limits of cospan diagrams and we define a locale ‹category_with_pullbacks› that
is satisfied by categories in which every cospan diagram has a limit.
These definitions build on the general definition of limit that we gave in
@{theory Category3.Limit}. We then define a locale ‹elementary_category_with_pullbacks›
that axiomatizes categories equipped with chosen functions that assign to each cospan
a corresponding span of ``projections'', which enjoy the familiar universal property
of a pullback. After developing consequences of the axioms, we prove that the two
locales are in agreement, in the sense that every interpretation of
‹category_with_pullbacks› extends to an interpretation of
‹elementary_category_with_pullbacks›, and conversely, the underlying category of
an interpretation of ‹elementary_category_with_pullbacks› always yields an interpretation
of ‹category_with_pullbacks›.
›
section "Commutative Squares"
context category
begin
text ‹
The following provides some useful technology for working with commutative squares.
›
definition commutative_square
where "commutative_square f g h k ≡ cospan f g ∧ span h k ∧ dom f = cod h ∧ f ⋅ h = g ⋅ k"
lemma commutative_squareI [intro, simp]:
assumes "cospan f g" and "span h k" and "dom f = cod h" and "f ⋅ h = g ⋅ k"
shows "commutative_square f g h k"
using assms commutative_square_def by auto
lemma commutative_squareE [elim]:
assumes "commutative_square f g h k"
and "⟦ arr f; arr g; arr h; arr k; cod f = cod g; dom h = dom k; dom f = cod h;
dom g = cod k; f ⋅ h = g ⋅ k ⟧ ⟹ T"
shows T
using assms commutative_square_def
by (metis (mono_tags, lifting) seqE seqI)
lemma commutative_square_comp_arr:
assumes "commutative_square f g h k" and "seq h l"
shows "commutative_square f g (h ⋅ l) (k ⋅ l)"
using assms
apply (elim commutative_squareE, intro commutative_squareI, auto)
using comp_assoc by metis
lemma arr_comp_commutative_square:
assumes "commutative_square f g h k" and "seq l f"
shows "commutative_square (l ⋅ f) (l ⋅ g) h k"
using assms comp_assoc
by (elim commutative_squareE, intro commutative_squareI, auto)
end
section "Cospan Diagrams"
text ‹
The ``shape'' of a cospan diagram is a category having two non-identity arrows
with distinct domains and a common codomain.
›
locale cospan_shape
begin