Theory CategoryWithBoundedPushouts
section "Categories with Bounded Pushouts"
subsection "Bounded Spans"
text‹
We call a span in a category ``bounded'' if it can be completed to a
commuting square. A category with bounded pushouts is a category in which
every bounded span has a pushout.
›
theory CategoryWithBoundedPushouts
imports Category3.EpiMonoIso Category3.CategoryWithPullbacks
begin
context category
begin
definition bounded_span
where "bounded_span h k ≡ ∃f g. commutative_square f g h k"
lemma bounded_spanI [intro]:
assumes "commutative_square f g h k"
shows "bounded_span h k"
using assms bounded_span_def by auto
lemma bounded_spanE [elim]:
assumes "bounded_span h k"
obtains f g where "commutative_square f g h k"
using assms bounded_span_def by auto
lemma bounded_span_sym:
shows "bounded_span h k ⟹ bounded_span k h"
unfolding bounded_span_def commutative_square_def
by (metis seqE seqI)
end
subsection "Pushouts"
text‹
Here we give a definition of the notion ``pushout square'' in a category, and prove that
pushout squares compose. The definition here is currently a ``free-standing'' one,
because it has been stated on its own, without deriving it from a general notion of colimit.
At some future time, once the general development of limits given in \<^cite>‹"Category3-AFP"›
has been suitably dualized to obtain a corresponding development of colimits,
this formal connection should be made.
›
context category
begin
definition pushout_square
where "pushout_square f g h k ≡
commutative_square f g h k ∧
(∀f' g'. commutative_square f' g' h k ⟶ (∃!l. l ⋅ f = f' ∧ l ⋅ g = g'))"
lemma pushout_squareI [intro]:
assumes "cospan f g" and "span h k" and "dom f = cod h" and "f ⋅ h = g ⋅ k"
and "⋀f' g'. commutative_square f' g' h k ⟹ ∃!l. l ⋅ f = f' ∧ l ⋅ g = g'"
shows "pushout_square f g h k"
using assms pushout_square_def by simp
lemma composition_of_pushouts:
assumes "pushout_square u' t' t u" and "pushout_square v' t'' t' v"
shows "pushout_square (v' ⋅ u') t'' t (v ⋅ u)"
proof
show 1: "cospan (v' ⋅ u') t''"
using assms
by (metis (mono_tags, lifting) commutative_square_def seqI cod_comp
pushout_square_def)
show "span t (v ⋅ u)"
using assms pushout_square_def by fastforce
show "dom (v' ⋅ u') = cod t"
using assms
by (metis 1 commutative_squareE dom_comp pushout_square_def)
show "(v' ⋅ u') ⋅ t = t'' ⋅ v ⋅ u"
using assms
by (metis commutative_squareE comp_assoc pushout_square_def)
fix w x
assume wx: "commutative_square w x t (v ⋅ u)"
show "∃!l. l ⋅ v' ⋅ u' = w ∧ l ⋅ t'' = x"
proof -
have 1: "commutative_square w (x ⋅ v) t u"
using wx
by (metis (mono_tags, lifting) cod_comp commutative_square_def
dom_comp comp_assoc seqE seqI)
hence *: "∃!z. z ⋅ u' = w ∧ z ⋅ t' = x ⋅ v"
using assms pushout_square_def by auto
obtain z where z: "z ⋅ u' = w ∧ z ⋅ t' = x ⋅ v"
using * by auto
have 2: "commutative_square z x t' v"
using z
by (metis (mono_tags, lifting) 1 cod_comp commutative_square_def
dom_comp seqE)
hence **: "∃l. l ⋅ v' = z ∧ l ⋅ t'' = x"
by (meson assms(2) pushout_square_def)
obtain l where l: "l ⋅ v' = z ∧ l ⋅ t'' = x"
using ** by auto
have "l ⋅ v' ⋅ u' = w ∧ l ⋅ t'' = x"
using l comp_assoc z by force
moreover have "⋀l l'. ⟦l ⋅ v' ⋅ u' = w ∧ l ⋅ t'' = x;
l' ⋅ v' ⋅ u' = w ∧ l' ⋅ t'' = x⟧
⟹ l = l'"
proof -
fix l l'
assume l: "l ⋅ v' ⋅ u' = w ∧ l ⋅ t'' = x"
assume l': "l' ⋅ v' ⋅ u' = w ∧ l' ⋅ t'' = x"
have "(l ⋅ v') ⋅ u' = w ∧ (l ⋅ v') ⋅ t' = x ⋅ v ∧
(l' ⋅ v') ⋅ u' = w ∧ (l' ⋅ v') ⋅ t' = x ⋅ v"
using assms(2)
by (metis commutative_squareE pushout_square_def l l' comp_assoc)
thus "l = l'"
by (metis * 2 assms(2) l l' pushout_square_def z)
qed
ultimately show ?thesis by blast
qed
qed
end
locale category_with_bounded_pushouts =
category C
for C :: "'a comp" (infixr "⋅" 55) +
assumes has_bounded_pushouts: "bounded_span h k ⟹ ∃f g. pushout_square f g h k"
locale elementary_category_with_bounded_pushouts =
category C
for C :: "'a comp" (infixr ‹⋅› 55)
and inj0 :: "'a ⇒ 'a ⇒ 'a" (‹𝗂⇩0[_, _]›)
and inj1 :: "'a ⇒ 'a ⇒ 'a" (‹𝗂⇩1[_, _]›) +
assumes inj0_ext: "¬ bounded_span h k ⟹ 𝗂⇩0[h, k] = null"
and inj1_ext: "¬ bounded_span h k ⟹ 𝗂⇩1[h, k] = null"
and pushout_commutes [intro]:
"bounded_span h k ⟹ commutative_square 𝗂⇩1[h, k] 𝗂⇩0[h, k] h k"
and pushout_universal:
"commutative_square f g h k ⟹ ∃!l. l ⋅ 𝗂⇩1[h, k] = f ∧ l ⋅ 𝗂⇩0[h, k] = g"
begin
lemma dom_inj [simp]:
assumes "bounded_span h k"
shows "dom 𝗂⇩0[h, k] = cod k" and "dom 𝗂⇩1[h, k] = cod h"
using assms pushout_commutes by blast+
lemma cod_inj:
assumes "bounded_span h k"
shows "cod 𝗂⇩1[h, k] = cod 𝗂⇩0[h, k]"
using assms pushout_commutes by auto
lemma has_bounded_pushouts:
assumes "bounded_span h k"
shows "pushout_square 𝗂⇩1[h, k] 𝗂⇩0[h, k] h k"
using assms pushout_square_def pushout_commutes pushout_universal by simp
sublocale category_with_bounded_pushouts C
using has_bounded_pushouts
by unfold_locales auto
lemma is_category_with_bounded_pushouts:
shows "category_with_bounded_pushouts C"
..
end
context category_with_bounded_pushouts
begin
definition inj0 ("𝗂⇩0[_, _]")
where "inj0 h k ≡ if bounded_span h k
then fst (SOME inj. pushout_square (snd inj) (fst inj) h k)
else null"
definition inj1 ("𝗂⇩1[_, _]")
where "inj1 h k ≡ if bounded_span h k
then snd (SOME inj. pushout_square (snd inj) (fst inj) h k)
else null"
lemma extends_to_elementary_category_with_bounded_pushouts:
shows "elementary_category_with_bounded_pushouts C inj0 inj1"
proof
show "⋀h k. ¬ bounded_span h k ⟹ 𝗂⇩0[h, k] = null"
unfolding inj0_def by simp
show "⋀h k. ¬ bounded_span h k ⟹ 𝗂⇩1[h, k] = null"
unfolding inj1_def by simp
have 1: "⋀h k. bounded_span h k ⟹ pushout_square 𝗂⇩1[h, k] 𝗂⇩0[h, k] h k"
proof -
fix h k
assume hk: "bounded_span h k"
show "pushout_square 𝗂⇩1[h, k] 𝗂⇩0[h, k] h k"
using hk has_bounded_pushouts inj0_def inj1_def
someI_ex [of "λx. pushout_square (snd x) (fst x) h k"]
by (metis (no_types, lifting) split_pairs)
qed
show "⋀h k. bounded_span h k ⟹ commutative_square 𝗂⇩1[h, k] 𝗂⇩0[h, k] h k"
using 1 pushout_square_def by auto
show "⋀f g h k. commutative_square f g h k ⟹ ∃!l. l ⋅ 𝗂⇩1[h, k] = f ∧ l ⋅ 𝗂⇩0[h, k] = g"
using 1 pushout_square_def bounded_spanI by force
qed
end
end