(* Title: CategoryWithPullbacks Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2019 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) 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" (* TODO: Rework the ugly development of equalizers into this form. *) 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