Theory CartesianCategory
chapter "Cartesian Category"
text‹
In this chapter, we explore the notion of a ``cartesian category'', which we define
to be a category having binary products and a terminal object.
We show that every cartesian category extends to an ``elementary cartesian category'',
whose definition assumes that specific choices have been made for projections and
terminal object.
Conversely, the underlying category of an elementary cartesian category is a
cartesian category.
We also show that cartesian categories are the same thing as categories with
finite products.
›
theory CartesianCategory
imports Limit SetCat CategoryWithPullbacks
begin
section "Category with Binary Products"
subsection "Binary Product Diagrams"
text ‹
The ``shape'' of a binary product diagram is a category having two distinct identity arrows
and no non-identity arrows.
›
locale binary_product_shape
begin
sublocale concrete_category ‹UNIV :: bool set› ‹λa b. if a = b then {()} else {}›
‹λ_. ()› ‹λ_ _ _ _ _. ()›
apply (unfold_locales, auto)
apply (meson empty_iff)
by (meson empty_iff)
abbreviation comp
where "comp ≡ COMP"
abbreviation FF
where "FF ≡ MkIde False"
abbreviation TT
where "TT ≡ MkIde True"
lemma arr_char:
shows "arr f ⟷ f = FF ∨ f = TT"
using arr_char by (cases f, simp_all)
lemma ide_char:
shows "ide f ⟷ f = FF ∨ f = TT"
using ide_char⇩C⇩C ide_MkIde by (cases f, auto)
lemma is_discrete:
shows "ide f ⟷ arr f"
using arr_char ide_char by simp
lemma dom_simp [simp]:
assumes "arr f"
shows "dom f = f"
using assms is_discrete by simp
lemma cod_simp [simp]:
assumes "arr f"
shows "cod f = f"
using assms is_discrete by simp
lemma seq_char:
shows "seq f g ⟷ arr f ∧ f = g"
by auto
lemma comp_simp [simp]:
assumes "seq f g"
shows "comp f g = f"
using assms seq_char by fastforce
end
locale binary_product_diagram =
J: binary_product_shape +
C: category C
for C :: "'c comp" (infixr "⋅" 55)
and a0 :: 'c
and a1 :: 'c +
assumes is_discrete: "C.ide a0 ∧ C.ide a1"
begin
notation J.comp (infixr "⋅⇩J" 55)
fun map
where "map J.FF = a0"
| "map J.TT = a1"
| "map _ = C.null"
sublocale diagram J.comp C map
proof
show "⋀f. ¬ J.arr f ⟹ map f = C.null"
using J.arr_char map.elims by auto
fix f
assume f: "J.arr f"
show "C.arr (map f)"
using f J.arr_char is_discrete C.ideD(1) map.simps(1-2) by metis
show "C.dom (map f) = map (J.dom f)"
using f J.arr_char J.dom_char is_discrete by force
show "C.cod (map f) = map (J.cod f)"
using f J.arr_char J.cod_char is_discrete by force
next
fix f g
assume fg: "J.seq g f"
show "map (g ⋅⇩J f) = map g ⋅ map f"
using fg J.arr_char J.seq_char J.null_char J.not_arr_null is_discrete
by (metis (no_types, lifting) C.comp_ide_self J.comp_simp map.simps(1-2))
qed
end
subsection "Category with Binary Products"
text ‹
A \emph{binary product} in a category @{term C} is a limit of a binary product diagram
in @{term C}.
›
context binary_product_diagram
begin
definition mkCone
where "mkCone p0 p1 ≡ λj. if j = J.FF then p0 else if j = J.TT then p1 else C.null"
abbreviation is_rendered_commutative_by
where "is_rendered_commutative_by p0 p1 ≡
C.seq a0 p0 ∧ C.seq a1 p1 ∧ C.dom p0 = C.dom p1"
abbreviation has_as_binary_product
where "has_as_binary_product p0 p1 ≡ limit_cone (C.dom p0) (mkCone p0 p1)"
lemma cone_mkCone:
assumes "is_rendered_commutative_by p0 p1"
shows "cone (C.dom p0) (mkCone p0 p1)"
proof -
interpret E: constant_functor J.comp C ‹C.dom p0›
using assms by unfold_locales auto
show "cone (C.dom p0) (mkCone p0 p1)"
using assms mkCone_def J.arr_char E.map_simp is_discrete C.comp_ide_arr C.comp_arr_dom
by unfold_locales auto
qed
lemma is_rendered_commutative_by_cone:
assumes "cone a χ"
shows "is_rendered_commutative_by (χ J.FF) (χ J.TT)"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
show ?thesis
using is_discrete by simp
qed
lemma mkCone_cone:
assumes "cone a χ"
shows "mkCone (χ J.FF) (χ J.TT) = χ"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
interpret mkCone_χ: cone J.comp C map ‹C.dom (χ J.FF)› ‹mkCone (χ J.FF) (χ J.TT)›
using assms is_rendered_commutative_by_cone cone_mkCone by blast
show ?thesis
using mkCone_def χ.is_extensional J.ide_char mkCone_def
NaturalTransformation.eqI [of J.comp C]
χ.natural_transformation_axioms mkCone_χ.natural_transformation_axioms
by fastforce
qed
lemma cone_iff_span:
shows "cone (C.dom h) (mkCone h k) ⟷ C.span h k ∧ C.cod h = a0 ∧ C.cod k = a1"
by (metis (no_types, lifting) C.cod_eqI C.comp_cod_arr C.comp_ide_arr J.arr.simps(1)
cone_mkCone is_discrete is_rendered_commutative_by_cone mkCone_def)
lemma cones_map_mkCone_eq_iff:
assumes "is_rendered_commutative_by p0 p1" and "is_rendered_commutative_by p0' p1'"
and "«h : C.dom p0' → C.dom p0»"
shows "cones_map h (mkCone p0 p1) = mkCone p0' p1' ⟷ p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof -
interpret χ: cone J.comp C map ‹C.dom p0› ‹mkCone p0 p1›
using assms(1) cone_mkCone [of p0 p1] by blast
interpret χ': cone J.comp C map ‹C.dom p0'› ‹mkCone p0' p1'›
using assms(2) cone_mkCone [of p0' p1'] by blast
show ?thesis
proof
assume 1: "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
show "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof
show "p0 ⋅ h = p0'"
proof -
have "p0' = cones_map h (mkCone p0 p1) J.FF"
using 1 mkCone_def J.arr_char by simp
also have "... = p0 ⋅ h"
using assms mkCone_def J.arr_char χ.cone_axioms by auto
finally show ?thesis by auto
qed
show "p1 ⋅ h = p1'"
proof -
have "p1' = cones_map h (mkCone p0 p1) J.TT"
using 1 mkCone_def J.arr_char by simp
also have "... = p1 ⋅ h"
using assms mkCone_def J.arr_char χ.cone_axioms by auto
finally show ?thesis by auto
qed
qed
next
assume "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
thus "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
using assms χ.cone_axioms mkCone_def J.arr_char by auto
qed
qed
end
locale binary_product_cone =
J: binary_product_shape +
C: category C +
D: binary_product_diagram C f0 f1 +
limit_cone J.comp C D.map ‹C.dom p0› ‹D.mkCone p0 p1›
for C :: "'c comp" (infixr "⋅" 55)
and f0 :: 'c
and f1 :: 'c
and p0 :: 'c
and p1 :: 'c
begin
lemma renders_commutative:
shows "D.is_rendered_commutative_by p0 p1"
using cone_axioms D.is_rendered_commutative_by_cone D.mkCone_def D.cone_iff_span
by force
lemma is_universal':
assumes "D.is_rendered_commutative_by p0' p1'"
shows "∃!h. «h : C.dom p0' → C.dom p0» ∧ p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof -
have "D.cone (C.dom p0') (D.mkCone p0' p1')"
using assms D.cone_mkCone by blast
hence "∃!h. «h : C.dom p0' → C.dom p0» ∧
D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1'"
using is_universal by simp
moreover have "⋀h. «h : C.dom p0' → C.dom p0» ⟹
D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1' ⟷
p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
using assms D.cones_map_mkCone_eq_iff [of p0 p1 p0' p1'] renders_commutative
by blast
ultimately show ?thesis by blast
qed
lemma induced_arrowI':
assumes "D.is_rendered_commutative_by p0' p1'"
shows "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0' → C.dom p0»"
and "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
and "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
proof -
interpret A': constant_functor J.comp C ‹C.dom p0'›
using assms by (unfold_locales, auto)
have cone: "D.cone (C.dom p0') (D.mkCone p0' p1')"
using assms D.cone_mkCone [of p0' p1'] by blast
show 0: "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
proof -
have "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') =
D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) J.FF"
using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
also have "... = p0'"
by (metis (no_types, lifting) D.mkCone_def cone induced_arrowI(2)
mem_Collect_eq restrict_apply)
finally show ?thesis by auto
qed
show "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
proof -
have "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') =
D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) J.TT"
using assms cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by fastforce
also have "... = p1'"
proof -
have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) =
D.mkCone p0' p1'"
using cone induced_arrowI by blast
thus ?thesis
using J.arr_char D.mkCone_def by simp
qed
finally show ?thesis by auto
qed
show "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0' → C.dom p0»"
using 0 cone induced_arrowI by simp
qed
end
context category
begin
definition has_as_binary_product
where "has_as_binary_product a0 a1 p0 p1 ≡
ide a0 ∧ ide a1 ∧ binary_product_diagram.has_as_binary_product C a0 a1 p0 p1"
definition has_binary_products
where "has_binary_products =
(∀a0 a1. ide a0 ∧ ide a1 ⟶ (∃p0 p1. has_as_binary_product a0 a1 p0 p1))"
lemma has_as_binary_productI [intro]:
assumes "span p q" and "cod p = a" and "cod q = b"
and "⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!h. «h : x → dom p» ∧ p ⋅ h = f ∧ q ⋅ h = g"
shows "has_as_binary_product a b p q"
proof (unfold has_as_binary_product_def, intro conjI)
show a: "ide a"
using assms by auto
show b: "ide b"
using assms by auto
let ?c = "dom p"
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using a b by unfold_locales auto
show "D.has_as_binary_product p q"
proof -
have 1: "D.is_rendered_commutative_by p q"
using assms a b ide_in_hom by blast
let ?χ = "D.mkCone p q"
interpret χ: cone J.comp C D.map ?c ?χ
using assms(4) D.cone_mkCone 1 by auto
interpret χ: limit_cone J.comp C D.map ?c ?χ
proof
fix x χ'
assume χ': "D.cone x χ'"
interpret χ': cone J.comp C D.map x χ'
using χ' by simp
have 2: "∃!h. «h : x → ?c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
proof -
have "«χ' J.FF : x → a» ∧ «χ' J.TT : x → b»"
by auto
thus ?thesis
using assms(4) [of "χ' J.FF" x "χ' J.TT"] by simp
qed
have 3: "D.is_rendered_commutative_by (χ' J.FF) (χ' J.TT)"
using a b by force
obtain h where h: "«h : x → ?c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
using 2 by blast
have 4: "«h : dom (χ' (J.MkIde False)) → dom p»"
using assms(3) h by auto
have "«h : x → ?c» ∧ D.cones_map h (D.mkCone p q) = χ'"
proof (intro conjI)
show "«h : x → ?c»"
using h by blast
show "D.cones_map h (D.mkCone p q) = χ'"
proof
fix j
show "D.cones_map h (D.mkCone p q) j = χ' j"
using h 1 3 4 D.cones_map_mkCone_eq_iff [of p q "χ' J.FF" "χ' J.TT"]
χ.cone_axioms J.is_discrete χ'.is_extensional
D.mkCone_def binary_product_shape.ide_char
apply (cases "J.ide j")
by (metis (no_types, lifting))+
qed
qed
moreover have "⋀h'. «h' : x → ?c» ∧ D.cones_map h' (D.mkCone p q) = χ' ⟹ h' = h"
proof -
fix h'
assume 5: "«h' : x → ?c» ∧ D.cones_map h' (D.mkCone p q) = χ'"
have "∃!h. «h : x → ?c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
by (simp add: assms(4) in_homI)
moreover have "«h : x → ?c» ∧ χ' J.FF = p ⋅ h ∧ q ⋅ h = χ' J.TT"
using h by simp
moreover have "«h' : x → ?c» ∧ χ' J.FF = p ⋅ h' ∧ q ⋅ h' = χ' J.TT"
using 5 χ.cone_axioms D.mkCone_def [of p q] by auto
ultimately show "h' = h" by auto
qed
ultimately show "∃!h. «h : x → ?c» ∧ D.cones_map h (D.mkCone p q) = χ'"
by blast
qed
show "D.has_as_binary_product p q"
using assms χ.limit_cone_axioms by blast
qed
qed
lemma has_as_binary_productE [elim]:
assumes "has_as_binary_product a b p q"
and "⟦«p : dom p → a»; «q : dom p → b»;
⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!h. p ⋅ h = f ∧ q ⋅ h = g⟧ ⟹ T"
shows T
proof -
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using assms(1) has_as_binary_product_def
by (simp add: binary_product_diagram.intro binary_product_diagram_axioms.intro
category_axioms)
have 1: "⋀h k. span h k ∧ cod h = a ∧ cod k = b ⟷ D.cone (dom h) (D.mkCone h k)"
using D.cone_iff_span by presburger
let ?χ = "D.mkCone p q"
interpret χ: limit_cone J.comp C D.map ‹dom p› ?χ
using assms(1) has_as_binary_product_def D.cone_mkCone by blast
have span: "span p q"
using 1 χ.cone_axioms by blast
moreover have "«p : dom p → a» ∧ «q : dom p → b»"
using span χ.preserves_hom χ.cone_axioms binary_product_shape.arr_char
by (metis D.cone_iff_span arr_iff_in_hom)
moreover have "⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!l. p ⋅ l = f ∧ q ⋅ l = g"
proof -
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
let ?χ' = "D.mkCone f g"
interpret χ': cone J.comp C D.map x ?χ'
using 1 f g by blast
have 2: "∃!l. «l : x → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 1 f g χ.is_universal [of x "D.mkCone f g"] χ'.cone_axioms by fastforce
obtain l where l: "«l : x → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 2 by blast
have "p ⋅ l = f ∧ q ⋅ l = g"
proof
show "p ⋅ l = f"
proof -
have "p ⋅ l = ?χ J.FF ⋅ l"
using D.mkCone_def by presburger
also have "... = D.cones_map l ?χ J.FF"
using χ.cone_axioms
apply simp
using l by fastforce
also have "... = f"
using D.mkCone_def l by presburger
finally show ?thesis by blast
qed
show "q ⋅ l = g"
proof -
have "q ⋅ l = ?χ J.TT ⋅ l"
using D.mkCone_def by simp
also have "... = D.cones_map l ?χ J.TT"
using χ.cone_axioms
apply simp
using l by fastforce
also have "... = g"
using D.mkCone_def l by simp
finally show "q ⋅ l = g" by blast
qed
qed
moreover have "⋀l'. p ⋅ l' = f ∧ q ⋅ l' = g ⟹ l' = l"
proof -
fix l'
assume 1: "p ⋅ l' = f ∧ q ⋅ l' = g"
have 2: "«l' : x → dom p»"
using 1 f by blast
moreover have "D.cones_map l' ?χ = ?χ'"
using 1 2 D.cones_map_mkCone_eq_iff [of p q f g l']
by (metis (no_types, lifting) f g ‹«p : dom p → a» ∧ «q : dom p → b»›
comp_cod_arr in_homE)
ultimately show "l' = l"
using l χ.is_universal χ'.cone_axioms by blast
qed
ultimately show "∃!l. p ⋅ l = f ∧ q ⋅ l = g" by blast
qed
ultimately show T
using assms(2) by simp
qed
end
locale category_with_binary_products =
category +
assumes has_binary_products: has_binary_products
subsection "Elementary Category with Binary Products"
text ‹
An \emph{elementary category with binary products} is a category equipped with a specific
way of mapping each pair of objects ‹a› and ‹b› to a pair of arrows ‹𝔭⇩1[a, b]› and ‹𝔭⇩0[a, b]›
that comprise a universal span.
›
locale elementary_category_with_binary_products =
category C
for C :: "'a comp" (infixr "⋅" 55)
and pr0 :: "'a ⇒ 'a ⇒ 'a" ("𝔭⇩0[_, _]")
and pr1 :: "'a ⇒ 'a ⇒ 'a" ("𝔭⇩1[_, _]") +
assumes span_pr: "⟦ ide a; ide b ⟧ ⟹ span 𝔭⇩1[a, b] 𝔭⇩0[a, b]"
and cod_pr0: "⟦ ide a; ide b ⟧ ⟹ cod 𝔭⇩0[a, b] = b"
and cod_pr1: "⟦ ide a; ide b ⟧ ⟹ cod 𝔭⇩1[a, b] = a"
and universal: "span f g ⟹ ∃!l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
begin
lemma pr0_in_hom':
assumes "ide a" and "ide b"
shows "«𝔭⇩0[a, b] : dom 𝔭⇩0[a, b] → b»"
using assms span_pr cod_pr0 by auto
lemma pr1_in_hom':
assumes "ide a" and "ide b"
shows "«𝔭⇩1[a, b] : dom 𝔭⇩0[a, b] → a»"
using assms span_pr cod_pr1 by auto
text ‹
We introduce a notation for tupling, which denotes the arrow into a product that
is induced by a span.
›
definition tuple ("⟨_, _⟩")
where "⟨f, g⟩ ≡ if span f g then
THE l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g
else null"
text ‹
The following defines product of arrows (not just of objects). It will take a little
while before we can prove that it is functorial, but for right now it is nice to have
it as a notation for the apex of a product cone. We have to go through some slightly
unnatural contortions in the development here, though, to avoid having to introduce a
separate preliminary notation just for the product of objects.
›
definition prod (infixr "⊗" 51)
where "f ⊗ g ≡ ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
lemma seq_pr_tuple:
assumes "span f g"
shows "seq 𝔭⇩0[cod f, cod g] ⟨f, g⟩"
proof -
have "𝔭⇩0[cod f, cod g] ⋅ ⟨f, g⟩ = g"
unfolding tuple_def
using assms universal theI [of "λl. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"]
by simp meson
thus ?thesis
using assms by simp
qed
lemma tuple_pr_arr:
assumes "ide a" and "ide b" and "seq 𝔭⇩0[a, b] h"
shows "⟨𝔭⇩1[a, b] ⋅ h, 𝔭⇩0[a, b] ⋅ h⟩ = h"
unfolding tuple_def
using assms span_pr cod_pr0 cod_pr1 universal [of "𝔭⇩1[a, b] ⋅ h" "𝔭⇩0[a, b] ⋅ h"]
theI_unique [of "λl. 𝔭⇩1[a, b] ⋅ l = 𝔭⇩1[a, b] ⋅ h ∧ 𝔭⇩0[a, b] ⋅ l = 𝔭⇩0[a, b] ⋅ h" h]
by auto
lemma pr_tuple [simp]:
assumes "span f g" and "cod f = a" and "cod g = b"
shows "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f" and "𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g"
proof -
have 1: "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f ∧ 𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g"
unfolding tuple_def
using assms universal theI [of "λl. 𝔭⇩1[a, b] ⋅ l = f ∧ 𝔭⇩0[a, b] ⋅ l = g"]
by simp meson
show "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f" using 1 by simp
show "𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g" using 1 by simp
qed
lemma cod_tuple:
assumes "span f g"
shows "cod ⟨f, g⟩ = cod f ⊗ cod g"
proof -
have "cod f ⊗ cod g = ⟨𝔭⇩1[cod f, cod g], 𝔭⇩0[cod f, cod g]⟩"
unfolding prod_def
using assms comp_cod_arr span_pr cod_pr0 cod_pr1 by simp
also have "... = ⟨𝔭⇩1[cod f, cod g] ⋅ dom 𝔭⇩0[cod f, cod g],
𝔭⇩0[cod f, cod g] ⋅ dom 𝔭⇩0[cod f, cod g]⟩"
using assms span_pr comp_arr_dom by simp
also have "... = dom 𝔭⇩0[cod f, cod g]"
using assms tuple_pr_arr span_pr by simp
also have "... = cod ⟨f, g⟩"
using assms seq_pr_tuple by blast
finally show ?thesis by simp
qed
lemma tuple_in_hom [intro]:
assumes "«f : a → b»" and "«g : a → c»"
shows "«⟨f, g⟩ : a → b ⊗ c»"
using assms pr_tuple dom_comp cod_tuple
apply (elim in_homE, intro in_homI)
apply (metis seqE)
by metis+
lemma tuple_in_hom' [simp]:
assumes "arr f" and "dom f = a" and "cod f = b"
and "arr g" and "dom g = a" and "cod g = c"
shows "«⟨f, g⟩ : a → b ⊗ c»"
using assms by auto
lemma tuple_ext:
assumes "¬ span f g"
shows "⟨f, g⟩ = null"
unfolding tuple_def
by (simp add: assms)
lemma tuple_simps [simp]:
assumes "span f g"
shows "arr ⟨f, g⟩" and "dom ⟨f, g⟩ = dom f" and "cod ⟨f, g⟩ = cod f ⊗ cod g"
proof -
show "arr ⟨f, g⟩"
using assms tuple_in_hom by blast
show "dom ⟨f, g⟩ = dom f"
using assms tuple_in_hom
by (metis dom_comp pr_tuple(1))
show "cod ⟨f, g⟩ = cod f ⊗ cod g"
using assms cod_tuple by auto
qed
lemma tuple_pr [simp]:
assumes "ide a" and "ide b"
shows "⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ = a ⊗ b"
proof -
have 1: "dom 𝔭⇩0[a, b] = a ⊗ b"
using assms seq_pr_tuple cod_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"] span_pr
pr0_in_hom' pr1_in_hom'
by (metis cod_pr0 cod_pr1 seqE)
hence "⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ = ⟨𝔭⇩1[a, b] ⋅ (a ⊗ b), 𝔭⇩0[a, b] ⋅ (a ⊗ b)⟩"
using assms pr0_in_hom' pr1_in_hom' comp_arr_dom span_pr by simp
thus ?thesis
using assms 1 tuple_pr_arr span_pr
by (metis comp_arr_dom)
qed
lemma pr_in_hom [intro, simp]:
assumes "ide a" and "ide b" and "x = a ⊗ b"
shows "«𝔭⇩0[a, b] : x → b»" and "«𝔭⇩1[a, b] : x → a»"
proof -
show 0: "«𝔭⇩0[a, b] : x → b»"
using assms pr0_in_hom' seq_pr_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"]
cod_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"] span_pr cod_pr0 cod_pr1
by (intro in_homI, auto)
show "«𝔭⇩1[a, b] : x → a»"
using assms 0 span_pr pr1_in_hom' by fastforce
qed
lemma pr_simps [simp]:
assumes "ide a" and "ide b"
shows "arr 𝔭⇩0[a, b]" and "dom 𝔭⇩0[a, b] = a ⊗ b" and "cod 𝔭⇩0[a, b] = b"
and "arr 𝔭⇩1[a, b]" and "dom 𝔭⇩1[a, b] = a ⊗ b" and "cod 𝔭⇩1[a, b] = a"
using assms pr_in_hom by blast+
lemma pr_joint_monic:
assumes "ide a" and "ide b" and "seq 𝔭⇩0[a, b] h"
and "𝔭⇩0[a, b] ⋅ h = 𝔭⇩0[a, b] ⋅ h'" and "𝔭⇩1[a, b] ⋅ h = 𝔭⇩1[a, b] ⋅ h'"
shows "h = h'"
using assms by (metis tuple_pr_arr)
lemma comp_tuple_arr [simp]:
assumes "span f g" and "arr h" and "dom f = cod h"
shows "⟨f, g⟩ ⋅ h = ⟨f ⋅ h, g ⋅ h⟩"
proof (intro pr_joint_monic [where h = "⟨f, g⟩ ⋅ h"])
show "ide (cod f)" and "ide (cod g)"
using assms ide_cod by blast+
show "seq 𝔭⇩0[cod f, cod g] (⟨f, g⟩ ⋅ h)"
using assms by fastforce
show "𝔭⇩0[cod f, cod g] ⋅ ⟨f, g⟩ ⋅ h = 𝔭⇩0[cod f, cod g] ⋅ ⟨f ⋅ h, g ⋅ h⟩"
using assms(1-3) comp_reduce by auto
show "𝔭⇩1[cod f, cod g] ⋅ ⟨f, g⟩ ⋅ h = 𝔭⇩1[cod f, cod g] ⋅ ⟨f ⋅ h, g ⋅ h⟩"
using assms comp_reduce by auto
qed
lemma ide_prod [intro, simp]:
assumes "ide a" and "ide b"
shows "ide (a ⊗ b)"
using assms pr_simps ide_dom [of "𝔭⇩0[a, b]"] by simp
lemma prod_in_hom [intro]:
assumes "«f : a → c»" and "«g : b → d»"
shows "«f ⊗ g : a ⊗ b → c ⊗ d»"
using assms prod_def by fastforce
lemma prod_in_hom' [simp]:
assumes "arr f" and "dom f = a" and "cod f = c"
and "arr g" and "dom g = b" and "cod g = d"
shows "«f ⊗ g : a ⊗ b → c ⊗ d»"
using assms by blast
lemma prod_simps [simp]:
assumes "arr f0" and "arr f1"
shows "arr (f0 ⊗ f1)"
and "dom (f0 ⊗ f1) = dom f0 ⊗ dom f1"
and "cod (f0 ⊗ f1) = cod f0 ⊗ cod f1"
using assms prod_in_hom by blast+
lemma has_as_binary_product:
assumes "ide a" and "ide b"
shows "has_as_binary_product a b 𝔭⇩1[a, b] 𝔭⇩0[a, b]"
proof
show "span 𝔭⇩1[a, b] 𝔭⇩0[a, b]" and "cod 𝔭⇩1[a, b] = a" and "cod 𝔭⇩0[a, b] = b"
using assms by auto
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
have "span f g"
using f g by auto
hence "∃!l. 𝔭⇩1[a, b] ⋅ l = f ∧ 𝔭⇩0[a, b] ⋅ l = g"
using assms f g universal [of f g]
by (metis in_homE)
thus "∃!h. «h : x → dom 𝔭⇩1[a, b]» ∧ 𝔭⇩1[a, b] ⋅ h = f ∧ 𝔭⇩0[a, b] ⋅ h = g"
using f by blast
qed
end
lemma (in category) elementary_category_with_binary_productsI:
assumes "⋀a b. ⟦ide a; ide b⟧ ⟹ has_as_binary_product a b (p a b) (q a b)"
shows "elementary_category_with_binary_products C
(λa b. if ide a ∧ ide b then q a b else null)
(λa b. if ide a ∧ ide b then p a b else null)"
proof -
let ?p = "λa b. if ide a ∧ ide b then p a b else null"
let ?q = "λa b. if ide a ∧ ide b then q a b else null"
show ?thesis
proof
fix a b
assume a: "ide a" and b: "ide b"
show "span (?p a b) (?q a b)"
using assms a b
by auto force
show "cod (?q a b) = b"
using a b assms has_as_binary_productE by auto
show "cod (?p a b) = a"
using a b assms has_as_binary_productE by auto
next
fix f g
assume fg: "span f g"
have 1: "has_as_binary_product (cod f) (cod g)
(p (cod f) (cod g)) (q (cod f) (cod g))"
using assms fg by simp
obtain l where "p (cod f) (cod g) ⋅ l = f ∧ q (cod f) (cod g) ⋅ l = g"
using 1 fg has_as_binary_productE
by (metis in_homI)
hence "∃l. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g"
using fg by auto
moreover have
"⋀l l'. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g ∧
?p (cod f) (cod g) ⋅ l' = f ∧ ?q (cod f) (cod g) ⋅ l' = g
⟹ l = l'"
using 1 fg arr_iff_in_hom ide_cod
by (elim has_as_binary_productE, auto) metis
ultimately show "∃!l. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g"
by blast
qed
qed
subsection "Agreement between the Definitions"
text ‹
We now show that a category with binary products extends (by making a choice)
to an elementary category with binary products, and that the underlying category
of an elementary category with binary products is a category with binary products.
›
context category_with_binary_products
begin
definition some_pr1 ("𝔭⇩1⇧?[_, _]")
where "some_pr1 a b ≡ if ide a ∧ ide b then
fst (SOME x. has_as_binary_product a b (fst x) (snd x))
else null"
definition some_pr0 ("𝔭⇩0⇧?[_, _]")
where "some_pr0 a b ≡ if ide a ∧ ide b then
snd (SOME x. has_as_binary_product a b (fst x) (snd x))
else null"
lemma pr_yields_binary_product:
assumes "ide a" and "ide b"
shows "has_as_binary_product a b 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
proof -
have "∃x. has_as_binary_product a b (fst x) (snd x)"
using assms has_binary_products has_binary_products_def has_as_binary_product_def
by simp
thus ?thesis
using assms has_binary_products has_binary_products_def some_pr0_def some_pr1_def
someI_ex [of "λx. has_as_binary_product a b (fst x) (snd x)"]
by simp
qed
interpretation elementary_category_with_binary_products C some_pr0 some_pr1
proof
fix a b
assume a: "ide a" and b: "ide b"
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using a b by unfold_locales auto
let ?χ = "D.mkCone 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝔭⇩1⇧?[a, b]› ?χ
using a b pr_yields_binary_product
by (simp add: has_as_binary_product_def)
have 1: "𝔭⇩1⇧?[a, b] = ?χ J.FF ∧ 𝔭⇩0⇧?[a, b] = ?χ J.TT"
using D.mkCone_def by simp
show "span 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
using 1 χ.preserves_reflects_arr J.seqE J.arr_char J.seq_char J.is_category
D.is_rendered_commutative_by_cone χ.cone_axioms
by metis
show "cod 𝔭⇩1⇧?[a, b] = a"
using 1 χ.preserves_cod [of J.FF] J.cod_char J.arr_char by auto
show "cod 𝔭⇩0⇧?[a, b] = b"
using 1 χ.preserves_cod [of J.TT] J.cod_char J.arr_char by auto
next
fix f g
assume fg: "span f g"
show "∃!l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
proof -
interpret J: binary_product_shape .
interpret D: binary_product_diagram C ‹cod f› ‹cod g›
using fg by unfold_locales auto
let ?χ = "D.mkCone 𝔭⇩1⇧?[cod f, cod g] 𝔭⇩0⇧?[cod f, cod g]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝔭⇩1⇧?[cod f, cod g]› ?χ
using fg pr_yields_binary_product [of "cod f" "cod g"] has_as_binary_product_def
by simp
interpret χ: binary_product_cone C ‹cod f› ‹cod g› ‹𝔭⇩1⇧?[cod f, cod g]› ‹𝔭⇩0⇧?[cod f, cod g]› ..
have 1: "𝔭⇩1⇧?[cod f, cod g] = ?χ J.FF ∧ 𝔭⇩0⇧?[cod f, cod g] = ?χ J.TT"
using D.mkCone_def by simp
show "∃!l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
proof -
have "∃!l. «l : dom f → dom 𝔭⇩1⇧?[cod f, cod g]» ∧
𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
using fg χ.is_universal' by simp
moreover have "⋀l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ⟹ «l : dom f → dom 𝔭⇩1⇧?[cod f, cod g]»"
using fg dom_comp in_homI seqE seqI by metis
ultimately show ?thesis by auto
qed
qed
qed
proposition extends_to_elementary_category_with_binary_products:
shows "elementary_category_with_binary_products C some_pr0 some_pr1"
..
abbreviation some_prod (infixr "⊗⇧?" 51)
where "some_prod ≡ prod"
end
locale binary_product =
category C
for C :: "'a comp"
and a :: 'a
and b :: 'a
and p :: 'a
and q :: 'a +
assumes has_as_binary_product: "has_as_binary_product a b p q"
begin
definition product
where "product ≡ dom p"
lemma ide_product [intro, simp]:
shows "ide product"
unfolding product_def
using has_as_binary_product by fastforce
lemma prj_in_hom [intro, simp]:
shows "«p : product → a»"
and "«q : product → b»"
using has_as_binary_product product_def by auto
lemma prj_simps [simp]:
shows "dom p = product" and "cod p = a" and "dom q = product" and "cod q = b"
using prj_in_hom by blast+
definition tuple
where "tuple f g ≡ (THE h. C p h = f ∧ C q h = g)"
lemma tuple_props:
assumes "span f g" and "cod f = a" and "cod g = b"
shows [intro, simp]: "«tuple f g : dom f → product»"
and [simp]: "dom (tuple f g) = dom f"
and [simp]: "cod (tuple f g) = product"
and [simp]: "C p (tuple f g) = f"
and [simp]: "C q (tuple f g) = g"
and "⋀h. ⟦C p h = f; C q h = g⟧ ⟹ h = tuple f g"
proof -
have 0: "∃!h. C p h = f ∧ C q h = g"
using assms has_as_binary_product by blast
hence *: "C p (tuple f g) = f ∧ C q (tuple f g) = g"
using tuple_def theI' [of "λh. C p h = f ∧ C q h = g"] by simp
show 1: "«tuple f g : dom f → product»"
using assms *
by (metis dom_comp in_homI prj_simps(3) seqE)
show "dom (tuple f g) = dom f"
using 1 by auto
show "cod (tuple f g) = product"
using 1 by auto
show 2: "C p (tuple f g) = f"
using * by auto
show 3: "C q (tuple f g) = g"
using * by auto
show 4: "⋀h. ⟦C p h = f; C q h = g⟧ ⟹ h = tuple f g"
using * 0 2 3 by blast
qed
lemma tuple_proj:
shows [simp]: "tuple p q = product"
by (metis comp_arr_dom in_homE tuple_props(6) prj_in_hom(1-2))
lemma pr_joint_monic:
assumes "seq p x" and "seq p y" and "C p x = C p y" and "C q x = C q y"
shows "x = y"
by (metis (mono_tags, lifting) assms(1,3-4) cod_comp dom_comp tuple_props(6)
product_def arrI prj_in_hom(2) prj_simps(2-4) seqE seqI)
end
lemma (in category) binary_products_are_isomorphic:
assumes "has_as_binary_product a b p q" and "has_as_binary_product a b p' q'"
shows "isomorphic (dom p) (dom p')"
and "inverse_arrows (binary_product.tuple C p q p' q')
(binary_product.tuple C p' q' p q)"
proof -
show "isomorphic (dom p) (dom p')"
using assms limits_are_isomorphic(1)
unfolding has_as_binary_product_def by blast
interpret pq: binary_product C a b p q
using assms(1) by unfold_locales auto
interpret p'q': binary_product C a b p' q'
using assms(2) by unfold_locales auto
show "inverse_arrows (pq.tuple p' q') (p'q'.tuple p q)"
proof
show "ide (p'q'.tuple p q ⋅ pq.tuple p' q')"
proof -
have "p' ⋅ p'q'.tuple p q ⋅ pq.tuple p' q' = p' ⋅ p'q'.product ∧
q' ⋅ p'q'.tuple p q ⋅ pq.tuple p' q' = q' ⋅ p'q'.product"
using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
comp_assoc
by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4) pq.product_def)
thus ?thesis
by (metis comp_arr_dom p'q'.ide_product p'q'.tuple_props(6)
p'q'.prj_in_hom(1-2) p'q'.prj_simps(1-4) arrI)
qed
show "ide (pq.tuple p' q' ⋅ p'q'.tuple p q)"
proof -
have "p ⋅ pq.tuple p' q' ⋅ p'q'.tuple p q = p ⋅ pq.product ∧
q ⋅ pq.tuple p' q' ⋅ p'q'.tuple p q = q ⋅ pq.product"
using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
comp_assoc
by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4)
pq.product_def)
thus ?thesis
by (metis arrI comp_arr_dom ide_char' pq.tuple_props(6) pq.prj_in_hom(1-2)
pq.prj_simps(2-4) pq.product_def seqE)
qed
qed
qed
context elementary_category_with_binary_products
begin
sublocale category_with_binary_products C
proof
show "has_binary_products"
by (meson has_as_binary_product has_binary_products_def)
qed
proposition is_category_with_binary_products:
shows "category_with_binary_products C"
..
end
subsection "Further Properties"
context elementary_category_with_binary_products
begin
lemma interchange:
assumes "seq h f" and "seq k g"
shows "(h ⊗ k) ⋅ (f ⊗ g) = h ⋅ f ⊗ k ⋅ g"
using assms prod_def comp_tuple_arr comp_assoc by fastforce
lemma pr_naturality [simp]:
assumes "arr g" and "dom g = b" and "cod g = d"
and "arr f" and "dom f = a" and "cod f = c"
shows "𝔭⇩0[c, d] ⋅ (f ⊗ g) = g ⋅ 𝔭⇩0[a, b]"
and "𝔭⇩1[c, d] ⋅ (f ⊗ g) = f ⋅ 𝔭⇩1[a, b]"
using assms prod_def by fastforce+
abbreviation dup ("𝖽[_]")
where "𝖽[f] ≡ ⟨f, f⟩"
lemma dup_in_hom [intro, simp]:
assumes "«f : a → b»"
shows "«𝖽[f] : a → b ⊗ b»"
using assms by fastforce
lemma dup_simps [simp]:
assumes "arr f"
shows "arr 𝖽[f]" and "dom 𝖽[f] = dom f" and "cod 𝖽[f] = cod f ⊗ cod f"
using assms dup_in_hom by auto
lemma dup_naturality:
assumes "«f : a → b»"
shows "𝖽[b] ⋅ f = (f ⊗ f) ⋅ 𝖽[a]"
using assms prod_def comp_arr_dom comp_cod_arr comp_tuple_arr comp_assoc
by fastforce
lemma pr_dup [simp]:
assumes "ide a"
shows "𝔭⇩0[a, a] ⋅ 𝖽[a] = a" and "𝔭⇩1[a, a] ⋅ 𝖽[a] = a"
using assms by simp_all
lemma prod_tuple:
assumes "span f g" and "seq h f" and "seq k g"
shows "(h ⊗ k) ⋅ ⟨f, g⟩ = ⟨h ⋅ f, k ⋅ g⟩"
using assms prod_def comp_assoc comp_tuple_arr by fastforce
lemma tuple_eqI:
assumes "ide b" and "ide c" and "seq 𝔭⇩0[b, c] f" and "seq 𝔭⇩1[b, c] f"
and "𝔭⇩0[b, c] ⋅ f = f0" and "𝔭⇩1[b, c] ⋅ f = f1"
shows "f = ⟨f1, f0⟩"
using assms pr_joint_monic [of b c "⟨f1, f0⟩" f] pr_tuple by auto
lemma tuple_expansion:
assumes "span f g"
shows "(f ⊗ g) ⋅ 𝖽[dom f] = ⟨f, g⟩"
using assms prod_tuple comp_arr_dom by simp
definition assoc ("𝖺[_, _, _]")
where "𝖺[a, b, c] ≡ ⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩"
definition assoc' ("𝖺⇧-⇧1[_, _, _]")
where "𝖺⇧-⇧1[a, b, c] ≡ ⟨⟨𝔭⇩1[a, b ⊗ c], 𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]⟩, 𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]⟩"
lemma assoc_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ (b ⊗ c)»"
using assms assoc_def by auto
lemma assoc_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺[a, b, c]"
and "dom 𝖺[a, b, c] = (a ⊗ b) ⊗ c"
and "cod 𝖺[a, b, c] = a ⊗ (b ⊗ c)"
using assms assoc_in_hom by auto
lemma assoc'_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺⇧-⇧1[a, b, c] : a ⊗ (b ⊗ c) → (a ⊗ b) ⊗ c»"
using assms assoc'_def by auto
lemma assoc'_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺⇧-⇧1[a, b, c]"
and "dom 𝖺⇧-⇧1[a, b, c] = a ⊗ (b ⊗ c)"
and "cod 𝖺⇧-⇧1[a, b, c] = (a ⊗ b) ⊗ c"
using assms assoc'_in_hom by auto
lemma pr_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a ⊗ b, c]"
and "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
and "𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
using assms assoc_def by force+
lemma pr_assoc':
assumes "ide a" and "ide b" and "ide c"
shows "𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩1[a, b ⊗ c]"
and "𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]"
and "𝔭⇩0[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]"
using assms assoc'_def by force+
lemma assoc_naturality:
assumes "«f0 : a0 → b0»" and "«f1 : a1 → b1»" and "«f2 : a2 → b2»"
shows "𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) = (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
𝔭⇩0[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
(𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using comp_assoc by simp
also have "... = ⟨𝔭⇩0[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2], 𝔭⇩0[b0 ⊗ b1, b2]⟩ ⋅ ((f0 ⊗ f1) ⊗ f2)"
using assms assoc_def by fastforce
also have "... = ⟨(𝔭⇩0[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2),
𝔭⇩0[b0 ⊗ b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2)⟩"
using assms comp_tuple_arr by fastforce
also have "... = ⟨(𝔭⇩0[b0, b1] ⋅ (f0 ⊗ f1)) ⋅ 𝔭⇩1[a0 ⊗ a1, a2], f2 ⋅ 𝔭⇩0[a0 ⊗ a1, a2]⟩"
using assms comp_assoc by fastforce
also have "... = ⟨f1 ⋅ 𝔭⇩0[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2], f2 ⋅ 𝔭⇩0[a0 ⊗ a1, a2]⟩"
using assms comp_assoc
by (metis in_homE pr_naturality(1))
also have "... = 𝔭⇩0[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
using assms comp_assoc assoc_def prod_tuple by fastforce
finally show ?thesis by blast
qed
moreover have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
(𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using comp_assoc by simp
also have "... = (𝔭⇩1[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using assms assoc_def by fastforce
also have "... = (𝔭⇩1[b0, b1] ⋅ (f0 ⊗ f1)) ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms comp_assoc by fastforce
also have "... = f0 ⋅ 𝔭⇩1[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms comp_assoc
by (metis in_homE pr_naturality(2))
also have "... = 𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2] =
(𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2))) ⋅ 𝖺[a0, a1, a2]"
using comp_assoc by simp
also have "... = f0 ⋅ 𝔭⇩1[a0, a1 ⊗ a2] ⋅ 𝖺[a0, a1, a2]"
using assms comp_assoc by fastforce
also have "... = f0 ⋅ 𝔭⇩1[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms assoc_def by fastforce
finally show ?thesis by simp
qed
finally show ?thesis by blast
qed
ultimately show ?thesis
using assms pr_joint_monic [of b0 "b1 ⊗ b2" "𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2)"
"(f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"]
by fastforce
qed
lemma pentagon:
assumes "ide a" and "ide b" and "ide c" and "ide d"
shows "((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) = 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof (intro pr_joint_monic
[where h = "((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
and h' = "𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"])
show "ide a" by fact
show "ide (b ⊗ (c ⊗ d))"
by (simp add: assms(2-4))
show "seq 𝔭⇩0[a, b ⊗ (c ⊗ d)] (((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d))"
using assms by simp
show "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof -
have "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
((𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ (a ⊗ 𝖺[b, c, d])) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
using comp_assoc by simp
also have "... = (𝔭⇩1[a, (b ⊗ c) ⊗ d] ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
using assms pr_naturality(2) comp_cod_arr by force
also have "... = 𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)"
using assms assoc_def comp_assoc by simp
also have "... = (𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c]) ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
using assms pr_naturality(2) comp_assoc by fastforce
also have "... = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
using assms assoc_def comp_assoc by simp
finally have "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
by blast
also have "... = 𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
using assms assoc_def comp_assoc by auto
finally show ?thesis by blast
qed
show "𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof -
have "𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩0[a, b ⊗ c ⊗ d] ⋅
((a ⊗ ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩) ⋅
⟨𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d],
⟨𝔭⇩0[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d], 𝔭⇩0[a ⊗ b ⊗ c, d]⟩⟩) ⋅
(⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩ ⊗ d)"
using assms assoc_def by simp
also have "... = ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d],
⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩ ⋅ (𝔭⇩0[a, (b ⊗ c) ⊗ d] ⋅
⟨𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d],
⟨𝔭⇩0[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d], 𝔭⇩0[a ⊗ b ⊗ c, d]⟩⟩) ⋅
(⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c],
⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩ ⊗ d)"
proof -
have "𝔭⇩0[a, b ⊗ c ⊗ d] ⋅
(a ⊗ ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩) =
⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩ ⋅
𝔭⇩0[a, (b ⊗ c) ⊗ d]"
using assms assoc_def ide_in_hom pr_naturality(1) by auto
thus ?thesis using comp_assoc by metis
qed
also have "... = ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d],
⟨𝔭⇩0[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d], d ⋅ 𝔭⇩0[(a ⊗ b) ⊗ c, d]⟩⟩"
using assms comp_assoc by simp
also have "... = ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d],
⟨𝔭⇩0[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d], 𝔭⇩0[(a ⊗ b) ⊗ c, d]⟩⟩"
using assms comp_cod_arr by simp
also have "... = 𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
using assms assoc_def comp_assoc by simp
finally show ?thesis by simp
qed
qed
lemma inverse_arrows_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "inverse_arrows 𝖺[a, b, c] 𝖺⇧-⇧1[a, b, c]"
using assms assoc_def assoc'_def comp_assoc
by (auto simp add: tuple_pr_arr)
lemma inv_prod:
assumes "iso f" and "iso g"
shows "iso (prod f g)"
and "inv (prod f g) = prod (inv f) (inv g)"
proof -
have 1: "inverse_arrows (prod f g) (prod (inv f) (inv g))"
by (auto simp add: assms comp_inv_arr' comp_arr_inv' iso_is_arr interchange)
show "iso (prod f g)"
using 1 by blast
show "inv (prod f g) = prod (inv f) (inv g)"
using 1 by (simp add: inverse_unique)
qed
interpretation CC: product_category C C ..
abbreviation Prod
where "Prod fg ≡ fst fg ⊗ snd fg"
abbreviation Prod'
where "Prod' fg ≡ snd fg ⊗ fst fg"
interpretation Π: binary_functor C C C Prod
using tuple_ext CC.comp_char interchange
apply unfold_locales
apply auto
by (metis prod_def seqE)+
interpretation Prod': binary_functor C C C Prod'
using tuple_ext CC.comp_char interchange
apply unfold_locales
apply auto
by (metis prod_def seqE)+
lemma binary_functor_Prod:
shows "binary_functor C C C Prod" and "binary_functor C C C Prod'"
..
interpretation CCC: product_category C CC.comp ..
interpretation T: binary_endofunctor C Prod ..
interpretation ToTC: "functor" CCC.comp C T.ToTC
using T.functor_ToTC by auto
interpretation ToCT: "functor" CCC.comp C T.ToCT
using T.functor_ToCT by auto
abbreviation α
where "α f ≡ 𝖺[cod (fst f), cod (fst (snd f)), cod (snd (snd f))] ⋅
((fst f ⊗ fst (snd f)) ⊗ snd (snd f))"
lemma α_simp_ide:
assumes "CCC.ide a"
shows "α a = 𝖺[fst a, fst (snd a), snd (snd a)]"
using assms comp_arr_dom by auto
interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
proof
fix f
show "¬ CCC.arr f ⟹ α f = null"
by (metis CC.arr_char CCC.arr_char ext prod_def seqE tuple_ext)
assume f: "CCC.arr f"
show "dom (α f) = T.ToTC (CCC.dom f)"
using f by auto
show "cod (α f) = T.ToCT (CCC.cod f)"
using f by auto
show "T.ToCT f ⋅ α (CCC.dom f) = α f"
using f T.ToCT_def T.ToTC_def comp_assoc
assoc_naturality
[of "fst f" "dom (fst f)" "cod (fst f)"
"fst (snd f)" "dom (fst (snd f))" "cod (fst (snd f))"
"snd (snd f)" "dom (snd (snd f))" "cod (snd (snd f))"]
by (simp add: comp_arr_dom in_homI)
show "α (CCC.cod f) ⋅ T.ToTC f = α f"
using T.ToTC_def comp_arr_dom f by auto
next
show "⋀a. CCC.ide a ⟹ iso (α a)"
using CCC.ide_char⇩P⇩C CC.ide_char⇩P⇩C comp_arr_dom inverse_arrows_assoc isoI
by (metis assoc_simps(1-2) ideD(3))
qed
lemma α_is_natural_isomorphism:
shows "natural_isomorphism CCC.comp C T.ToTC T.ToCT α"
..
definition sym ("𝗌[_, _]")
where "𝗌[a1, a0] ≡ if ide a0 ∧ ide a1 then ⟨𝔭⇩0[a1, a0], 𝔭⇩1[a1, a0]⟩ else null"
lemma sym_in_hom [intro]:
assumes "ide a" and "ide b"
shows "«𝗌[a, b] : a ⊗ b → b ⊗ a»"
using assms sym_def by auto
lemma sym_simps [simp]:
assumes "ide a" and "ide b"
shows "arr 𝗌[a, b]" and "dom 𝗌[a, b] = a ⊗ b" and "cod 𝗌[a, b] = b ⊗ a"
using assms sym_in_hom by auto
lemma comp_sym_tuple [simp]:
assumes "«f0 : a → b0»" and "«f1 : a → b1»"
shows "𝗌[b0, b1] ⋅ ⟨f0, f1⟩ = ⟨f1, f0⟩"
using assms sym_def comp_tuple_arr by fastforce
lemma prj_sym [simp]:
assumes "ide a0" and "ide a1"
shows "𝔭⇩0[a1, a0] ⋅ 𝗌[a0, a1] = 𝔭⇩1[a0, a1]"
and "𝔭⇩1[a1, a0] ⋅ 𝗌[a0, a1] = 𝔭⇩0[a0, a1]"
using assms sym_def by auto
lemma comp_sym_sym [simp]:
assumes "ide a0" and "ide a1"
shows "𝗌[a1, a0] ⋅ 𝗌[a0, a1] = (a0 ⊗ a1)"
using assms sym_def comp_tuple_arr by auto
lemma sym_inverse_arrows:
assumes "ide a0" and "ide a1"
shows "inverse_arrows 𝗌[a0, a1] 𝗌[a1, a0]"
using assms sym_in_hom comp_sym_sym by auto
lemma sym_assoc_coherence:
assumes "ide a" and "ide b" and "ide c"
shows "𝖺[b, c, a] ⋅ 𝗌[a, b ⊗ c] ⋅ 𝖺[a, b, c] = (b ⊗ 𝗌[a, c]) ⋅ 𝖺[b, a, c] ⋅ (𝗌[a, b] ⊗ c)"
using assms sym_def assoc_def comp_assoc prod_tuple comp_cod_arr by simp
lemma sym_naturality:
assumes "«f0 : a0 → b0»" and "«f1 : a1 → b1»"
shows "𝗌[b0, b1] ⋅ (f0 ⊗ f1) = (f1 ⊗ f0) ⋅ 𝗌[a0, a1]"
using assms sym_def comp_assoc prod_tuple by fastforce
abbreviation σ
where "σ fg ≡ 𝗌[cod (fst fg), cod (snd fg)] ⋅ (fst fg ⊗ snd fg)"
interpretation σ: natural_transformation CC.comp C Prod Prod' σ
using sym_def CC.arr_char CC.null_char comp_arr_dom comp_cod_arr
apply unfold_locales
apply auto
using arr_cod_iff_arr ideD(1)
apply metis
using arr_cod_iff_arr ideD(1)
apply metis
using prod_tuple by simp
lemma σ_is_natural_transformation:
shows "natural_transformation CC.comp C Prod Prod' σ"
..
abbreviation Diag
where "Diag f ≡ if arr f then (f, f) else CC.null"
interpretation Δ: "functor" C CC.comp Diag
by (unfold_locales, auto)
lemma functor_Diag:
shows "functor C CC.comp Diag"
..
interpretation ΔoΠ: composite_functor CC.comp C CC.comp Prod Diag ..
interpretation ΠoΔ: composite_functor C CC.comp C Diag Prod ..
abbreviation π
where "π ≡ λ(f, g). (𝔭⇩1[cod f, cod g] ⋅ (f ⊗ g), 𝔭⇩0[cod f, cod g] ⋅ (f ⊗ g))"
interpretation π: transformation_by_components CC.comp CC.comp ΔoΠ.map CC.map π
using pr_naturality comp_arr_dom comp_cod_arr
by unfold_locales auto
lemma π_is_natural_transformation:
shows "natural_transformation CC.comp CC.comp ΔoΠ.map CC.map π"
proof -
have "π.map = π"
using π.map_def ext Π.is_extensional comp_arr_dom comp_cod_arr by auto
thus "natural_transformation CC.comp CC.comp ΔoΠ.map CC.map π"
using π.natural_transformation_axioms by simp
qed
interpretation δ: natural_transformation C C map ΠoΔ.map dup
using dup_naturality comp_arr_dom comp_cod_arr prod_tuple tuple_ext
by unfold_locales auto
lemma dup_is_natural_transformation:
shows "natural_transformation C C map ΠoΔ.map dup"
..
interpretation ΔoΠoΔ: composite_functor C CC.comp CC.comp Diag ΔoΠ.map ..
interpretation ΠoΔoΠ: composite_functor CC.comp C C Prod ΠoΔ.map ..
interpretation Δoδ: natural_transformation C CC.comp Diag ΔoΠoΔ.map ‹Diag ∘ dup›
proof -
have "Diag ∘ map = Diag"
by auto
thus "natural_transformation C CC.comp Diag ΔoΠoΔ.map (Diag ∘ dup)"
using Δ.as_nat_trans.natural_transformation_axioms δ.natural_transformation_axioms
o_assoc horizontal_composite [of C C map ΠoΔ.map dup CC.comp Diag Diag Diag]
by metis
qed
interpretation δoΠ: natural_transformation CC.comp C Prod ΠoΔoΠ.map ‹dup ∘ Prod›
using δ.natural_transformation_axioms Π.as_nat_trans.natural_transformation_axioms
o_assoc horizontal_composite [of CC.comp C Prod Prod Prod C map ΠoΔ.map dup]
by simp
interpretation πoΔ: natural_transformation C CC.comp ΔoΠoΔ.map Diag ‹π.map ∘ Diag›
using π.natural_transformation_axioms Δ.as_nat_trans.natural_transformation_axioms
horizontal_composite
[of C CC.comp Diag Diag Diag CC.comp ΔoΠ.map CC.map π.map]
by simp
interpretation Πoπ: natural_transformation CC.comp C ΠoΔoΠ.map Prod ‹Prod ∘ π.map›
proof -
have "Prod ∘ ΔoΠ.map = ΠoΔoΠ.map"
by auto
thus "natural_transformation CC.comp C ΠoΔoΠ.map Prod (Prod ∘ π.map)"
using π.natural_transformation_axioms Π.as_nat_trans.natural_transformation_axioms
o_assoc
horizontal_composite
[of CC.comp CC.comp ΔoΠ.map CC.map π.map C Prod Prod Prod]
by simp
qed
interpretation Δoδ_πoΔ: vertical_composite C CC.comp Diag ΔoΠoΔ.map Diag
‹Diag ∘ dup› ‹π.map ∘ Diag›
..
interpretation Πoπ_δoΠ: vertical_composite CC.comp C Prod ΠoΔoΠ.map Prod
‹dup ∘ Prod› ‹Prod ∘ π.map›
..
interpretation ΔΠ: unit_counit_adjunction CC.comp C Diag Prod dup π.map
proof
show "Δoδ_πoΔ.map = Diag"
proof
fix f
have "¬ arr f ⟹ Δoδ_πoΔ.map f = Diag f"
by (simp add: Δoδ_πoΔ.is_extensional)
moreover have "arr f ⟹ Δoδ_πoΔ.map f = Diag f"
using comp_cod_arr comp_assoc Δoδ_πoΔ.map_def by auto
ultimately show "Δoδ_πoΔ.map f = Diag f" by blast
qed
show "Πoπ_δoΠ.map = Prod"
proof
fix fg
show "Πoπ_δoΠ.map fg = Prod fg"
proof -
have "¬ CC.arr fg ⟹ ?thesis"
by (simp add: Π.is_extensional Πoπ_δoΠ.is_extensional)
moreover have "CC.arr fg ⟹ ?thesis"
proof -
assume fg: "CC.arr fg"
have 1: "dup (Prod fg) = ⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩ ⋅
(fst fg ⊗ snd fg)"
using fg δ.is_natural_2
apply simp
by (metis (no_types, lifting) prod_simps(1) prod_simps(3))
have "Πoπ_δoΠ.map fg =
(𝔭⇩1[cod (fst fg), cod (snd fg)] ⊗ 𝔭⇩0[cod (fst fg), cod (snd fg)]) ⋅
⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩ ⋅
(fst fg ⊗ snd fg)"
using fg 1 Πoπ_δoΠ.map_def comp_cod_arr by simp
also have "... = ((𝔭⇩1[cod (fst fg), cod (snd fg)] ⊗ 𝔭⇩0[cod (fst fg), cod (snd fg)]) ⋅
⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩) ⋅
(fst fg ⊗ snd fg)"
using comp_assoc by simp
also have "... = ⟨𝔭⇩1[cod (fst fg), cod (snd fg)] ⋅ (cod (fst fg) ⊗ cod (snd fg)),
𝔭⇩0[cod (fst fg), cod (snd fg)] ⋅ (cod (fst fg) ⊗ cod (snd fg))⟩ ⋅
(fst fg ⊗ snd fg)"
using fg prod_tuple by simp
also have "... = Prod fg"
using fg comp_arr_dom Π.as_nat_trans.is_natural_2 by auto
finally show ?thesis by simp
qed
ultimately show ?thesis by blast
qed
qed
qed
proposition induces_unit_counit_adjunction:
shows "unit_counit_adjunction CC.comp C Diag Prod dup π.map"
using ΔΠ.unit_counit_adjunction_axioms by simp
end
section "Category with Terminal Object"
locale category_with_terminal_object =
category +
assumes has_terminal: "∃t. terminal t"
locale elementary_category_with_terminal_object =
category C
for C :: "'a comp" (infixr "⋅" 55)
and one :: "'a" ("𝟭")
and trm :: "'a ⇒ 'a" ("𝗍[_]") +
assumes ide_one: "ide 𝟭"
and trm_in_hom [intro, simp]: "ide a ⟹ «𝗍[a] : a → 𝟭»"
and trm_eqI: "⟦ ide a; «f : a → 𝟭» ⟧ ⟹ f = 𝗍[a]"
begin
lemma trm_simps [simp]:
assumes "ide a"
shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = 𝟭"
using assms trm_in_hom by blast+
lemma trm_one:
shows "𝗍[𝟭] = 𝟭"
using ide_one trm_eqI ide_in_hom by auto
lemma terminal_one:
shows "terminal 𝟭"
using ide_one trm_in_hom trm_eqI terminal_def by metis
lemma trm_naturality:
assumes "arr f"
shows "𝗍[cod f] ⋅ f = 𝗍[dom f]"
using assms trm_eqI
by (metis comp_in_homI' ide_cod ide_dom in_homE trm_in_hom)
sublocale category_with_terminal_object C
apply unfold_locales
using terminal_one by auto
proposition is_category_with_terminal_object:
shows "category_with_terminal_object C"
..
definition τ
where "τ = (λf. if arr f then trm (dom f) else null)"
lemma τ_in_hom [intro, simp]:
assumes "arr f"
shows "«τ f : dom f → 𝟭»"
by (simp add: τ_def assms)
lemma τ_simps [simp]:
assumes "arr f"
shows "arr (τ f)" and "dom (τ f) = dom f" and "cod (τ f) = 𝟭"
using assms by (auto simp add: τ_def assms)
sublocale Ω: constant_functor C C 𝟭
using ide_one
by unfold_locales auto
sublocale τ: natural_transformation C C map Ω.map τ
unfolding τ_def
using trm_simps(1-3) comp_cod_arr trm_naturality
by unfold_locales auto
end
context category_with_terminal_object
begin
definition some_terminal ("𝟭⇧?")
where "some_terminal ≡ SOME t. terminal t"
definition "some_terminator" ("𝗍⇧?[_]")
where "𝗍⇧?[f] ≡ if arr f then THE t. «t : dom f → 𝟭⇧?» else null"
lemma terminal_some_terminal [intro]:
shows "terminal 𝟭⇧?"
using some_terminal_def has_terminal someI_ex [of "λt. terminal t"] by presburger
lemma ide_some_terminal:
shows "ide 𝟭⇧?"
using terminal_def by blast
lemma some_trm_in_hom [intro]:
assumes "arr f"
shows "«𝗍⇧?[f] : dom f → 𝟭⇧?»"
proof -
have "ide (dom f)" using assms by fastforce
hence "∃!t. «t : dom f → 𝟭⇧?»"
using assms some_terminator_def terminal_def terminal_some_terminal by simp
thus ?thesis
using assms some_terminator_def [of f] theI' [of "λt. «t : dom f → 𝟭⇧?»"] by auto
qed
lemma some_trm_simps [simp]:
assumes "arr f"
shows "arr 𝗍⇧?[f]" and "dom 𝗍⇧?[f] = dom f" and "cod 𝗍⇧?[f] = 𝟭⇧?"
using assms some_trm_in_hom by auto
lemma some_trm_eqI:
assumes "«t : dom f → 𝟭⇧?»"
shows "t = 𝗍⇧?[f]"
proof -
have "ide (dom f)" using assms
by (metis ide_dom in_homE)
hence "∃!t. «t : dom f → 𝟭⇧?»"
using terminal_def [of "𝟭⇧?"] terminal_some_terminal by auto
moreover have "«t : dom f → 𝟭⇧?»"
using assms by simp
ultimately show ?thesis
using assms some_terminator_def the1_equality [of "λt. «t : dom f → 𝟭⇧?»" t]
‹ide (dom f)› arr_dom_iff_arr
by fastforce
qed
proposition extends_to_elementary_category_with_terminal_object:
shows "elementary_category_with_terminal_object C 𝟭⇧? (λa. 𝗍⇧?[a])"
using ide_some_terminal some_trm_eqI
by unfold_locales auto
end
lemma (in category_with_terminal_object) binary_product_is_pullback:
assumes "has_as_binary_product a b p q"
shows "has_as_pullback 𝗍⇧?[a] 𝗍⇧?[b] p q"
proof
interpret elementary_category_with_terminal_object C ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_category_with_terminal_object by blast
show "cospan 𝗍⇧?[a] 𝗍⇧?[b]"
using assms by fastforce
show "commutative_square 𝗍⇧?[a] 𝗍⇧?[b] p q"
using assms trm_naturality by fastforce
show "⋀h k. commutative_square 𝗍⇧?[a] 𝗍⇧?[b] h k ⟹ ∃!l. p ⋅ l = h ∧ q ⋅ l = k"
proof -
fix h k
assume 1: "commutative_square 𝗍⇧?[a] 𝗍⇧?[b] h k"
have "«h : dom h → a» ∧ «k : dom h → b»"
by (metis 1 ‹commutative_square 𝗍⇧?[a] 𝗍⇧?[b] p q› arr_iff_in_hom assms
commutative_squareE has_as_binary_productE in_homE)
thus "∃!l. p ⋅ l = h ∧ q ⋅ l = k"
using assms has_as_binary_productE [of a b p q] by metis
qed
qed
section "Cartesian Category"
locale cartesian_category =
category_with_binary_products +
category_with_terminal_object
locale category_with_pullbacks_and_terminal_object =
category_with_pullbacks +
category_with_terminal_object
begin
sublocale category_with_binary_products C
proof
interpret elementary_category_with_terminal_object C ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_category_with_terminal_object by blast
show "has_binary_products"
proof -
have "⋀a0 a1. ⟦ide a0; ide a1⟧ ⟹ ∃p0 p1. has_as_binary_product a0 a1 p0 p1"
proof -
fix a0 a1
assume a0: "ide a0" and a1: "ide a1"
obtain p0 p1 where p0p1: "has_as_pullback 𝗍⇧?[a0] 𝗍⇧?[a1] p0 p1"
using a0 a1 has_pullbacks has_pullbacks_def by force
have "has_as_binary_product a0 a1 p0 p1"
proof
show "span p0 p1"
using p0p1 by blast
show "cod p0 = a0" and "cod p1 = a1"
using p0p1 a0 a1 commutative_squareE has_as_pullbackE in_homI trm_simps(2)
by metis+
fix x f g
assume f: "«f : x → a0»" and g: "«g : x → a1»"
have "commutative_square 𝗍⇧?[a0] 𝗍⇧?[a1] f g"
by (metis a0 has_as_pullbackE in_homE commutative_squareI f g p0p1 trm_naturality
trm_simps(2))
moreover have "⋀l. p0 ⋅ l = f ∧ p1 ⋅ l = g ⟹ «l : x → dom p0»"
using f g by blast
ultimately show "∃!l. «l : x → dom p0» ∧ p0 ⋅ l = f ∧ p1 ⋅ l = g"
by (metis has_as_pullbackE p0p1)
qed
thus "∃p0 p1. has_as_binary_product a0 a1 p0 p1"
by auto
qed
thus ?thesis
using has_binary_products_def by force
qed
qed
sublocale cartesian_category C ..
end
locale elementary_cartesian_category =
elementary_category_with_binary_products +
elementary_category_with_terminal_object
begin
sublocale cartesian_category C
using cartesian_category.intro is_category_with_binary_products
is_category_with_terminal_object
by auto
proposition is_cartesian_category:
shows "cartesian_category C"
..
end
context cartesian_category
begin
proposition extends_to_elementary_cartesian_category:
shows "elementary_cartesian_category C some_pr0 some_pr1 𝟭⇧? (λa. 𝗍⇧?[a])"
by (simp add: elementary_cartesian_category_def
extends_to_elementary_category_with_terminal_object
extends_to_elementary_category_with_binary_products)
end
subsection "Monoidal Structure"
text ‹
Here we prove some facts that will later allow us to show that an elementary cartesian
category is a monoidal category.
›
context elementary_cartesian_category
begin
abbreviation ι
where "ι ≡ 𝔭⇩0[𝟭, 𝟭]"
lemma pr_coincidence:
shows "ι = 𝔭⇩1[𝟭, 𝟭]"
using ide_one
by (simp add: terminal_arr_unique terminal_one)
lemma unit_is_terminal_arr:
shows "terminal_arr ι"
using ide_one
by (simp add: terminal_one)
lemma unit_eq_trm:
shows "ι = 𝗍[𝟭 ⊗ 𝟭]"
by (metis unit_is_terminal_arr cod_pr1 comp_cod_arr pr_simps(5) trm_naturality ide_one
pr_coincidence trm_one)
lemma inverse_arrows_ι:
shows "inverse_arrows ι ⟨𝟭, 𝟭⟩"
using ide_one
by (metis unit_is_terminal_arr cod_pr0 comp_tuple_arr ide_char ide_dom inverse_arrows_def
prod_def pr_coincidence pr_dup(2) pr_simps(2))
lemma ι_is_iso:
shows "iso ι"
using inverse_arrows_ι by auto
lemma trm_tensor:
assumes "ide a" and "ide b"
shows "𝗍[a ⊗ b] = ι ⋅ (𝗍[a] ⊗ 𝗍[b])"
using assms unit_is_terminal_arr terminal_arr_unique ide_one
by (simp add: unit_eq_trm)
abbreviation runit ("𝗋[_]")
where "𝗋[a] ≡ 𝔭⇩1[a, 𝟭]"
abbreviation runit' ("𝗋⇧-⇧1[_]")
where "𝗋⇧-⇧1[a] ≡ ⟨a, 𝗍[a]⟩"
abbreviation lunit ("𝗅[_]")
where "𝗅[a] ≡ 𝔭⇩0[𝟭, a]"
abbreviation lunit' ("𝗅⇧-⇧1[_]")
where "𝗅⇧-⇧1[a] ≡ ⟨𝗍[a], a⟩"
lemma runit_in_hom:
assumes "ide a"
shows "«𝗋[a] : a ⊗ 𝟭 → a»"
using assms ide_one by simp
lemma runit'_in_hom:
assumes "ide a"
shows "«𝗋⇧-⇧1[a] : a → a ⊗ 𝟭»"
using assms ide_in_hom trm_in_hom by blast
lemma lunit_in_hom:
assumes "ide a"
shows "«𝗅[a] : 𝟭 ⊗ a → a»"
using assms ide_one by simp
lemma lunit'_in_hom:
assumes "ide a"
shows "«𝗅⇧-⇧1[a] : a → 𝟭 ⊗ a»"
using assms ide_in_hom trm_in_hom by blast
lemma runit_naturality:
assumes "arr f"
shows "𝗋[cod f] ⋅ (f ⊗ 𝟭) = f ⋅ 𝗋[dom f]"
using assms pr_naturality(2) ide_char ide_one by blast
lemma inverse_arrows_runit:
assumes "ide a"
shows "inverse_arrows 𝗋[a] 𝗋⇧-⇧1[a]"
proof
show "ide (𝗋[a] ⋅ 𝗋⇧-⇧1[a])"
using assms by auto
show "ide (𝗋⇧-⇧1[a] ⋅ 𝗋[a])"
proof -
have "ide (a ⊗ 𝟭)"
using assms ide_one by blast
moreover have "𝗋⇧-⇧1[a] ⋅ 𝗋[a] = a ⊗ 𝟭"
proof (intro pr_joint_monic [of a 𝟭 "𝗋⇧-⇧1[a] ⋅ 𝗋[a]" "a ⊗ 𝟭"])
show "ide a" by fact
show "ide 𝟭"
using ide_one by blast
show "seq 𝔭⇩0[a, 𝟭] (𝗋⇧-⇧1[a] ⋅ 𝗋[a])"
using assms ide_one runit'_in_hom [of a]
by (intro seqI) auto
show "𝔭⇩0[a, 𝟭] ⋅ 𝗋⇧-⇧1[a] ⋅ 𝗋[a] = 𝔭⇩0[a, 𝟭] ⋅ (a ⊗ 𝟭)"
proof -
have "𝔭⇩0[a, 𝟭] ⋅ 𝗋⇧-⇧1[a] ⋅ 𝗋[a] = (𝔭⇩0[a, 𝟭] ⋅ 𝗋⇧-⇧1[a]) ⋅ 𝗋[a]"
using comp_assoc by simp
also have "... = 𝗍[a] ⋅ 𝗋[a]"
using assms ide_one
by (metis in_homE pr_tuple(2) ide_char trm_in_hom)
also have "... = 𝗍[a ⊗ 𝟭]"
using assms ide_one trm_naturality [of "𝗋[a]"] by simp
also have "... = 𝔭⇩0[a, 𝟭] ⋅ (a ⊗ 𝟭)"
by (simp add: assms ide_one trm_one trm_tensor)
finally show ?thesis by blast
qed
show "𝔭⇩1[a, 𝟭] ⋅ 𝗋⇧-⇧1[a] ⋅ 𝗋[a] = 𝔭⇩1[a, 𝟭] ⋅ (a ⊗ 𝟭)"
using assms
by (metis ‹ide (𝗋[a] ⋅ 𝗋⇧-⇧1[a])› cod_comp cod_pr1 dom_comp ide_compE ide_one
comp_assoc runit_naturality)
qed
ultimately show ?thesis by simp
qed
qed
lemma lunit_naturality:
assumes "arr f"
shows "C 𝗅[cod f] (𝟭 ⊗ f) = C f 𝗅[dom f]"
using assms pr_naturality(1) ide_char ide_one by blast
lemma inverse_arrows_lunit:
assumes "ide a"
shows "inverse_arrows 𝗅[a] 𝗅⇧-⇧1[a]"
proof
show "ide (C 𝗅[a] 𝗅⇧-⇧1[a])"
using assms by auto
show "ide (𝗅⇧-⇧1[a] ⋅ 𝗅[a])"
proof -
have "𝗅⇧-⇧1[a] ⋅ 𝗅[a] = 𝟭 ⊗ a"
proof (intro pr_joint_monic [of 𝟭 a "𝗅⇧-⇧1[a] ⋅ 𝗅[a]" "𝟭 ⊗ a"])
show "ide a" by fact
show "ide 𝟭"
using ide_one by blast
show "seq 𝗅[a] (𝗅⇧-⇧1[a] ⋅ 𝗅[a])"
using assms ‹ide (𝗅[a] ⋅ 𝗅⇧-⇧1[a])› by blast
show "𝗅[a] ⋅ 𝗅⇧-⇧1[a] ⋅ 𝗅[a] = 𝗅[a] ⋅ (𝟭 ⊗ a)"
using assms
by (metis ‹ide (𝗅[a] ⋅ 𝗅⇧-⇧1[a])› cod_comp cod_pr0 dom_cod ide_compE ide_one
comp_assoc lunit_naturality)
show "𝔭⇩1[𝟭, a] ⋅ 𝗅⇧-⇧1[a] ⋅ 𝗅[a] = 𝔭⇩1[𝟭, a] ⋅ (𝟭 ⊗ a)"
proof -
have "𝔭⇩1[𝟭, a] ⋅ 𝗅⇧-⇧1[a] ⋅ 𝗅[a] = (𝔭⇩1[𝟭, a] ⋅ 𝗅⇧-⇧1[a]) ⋅ 𝗅[a]"
using comp_assoc by simp
also have "... = 𝗍[a] ⋅ 𝗅[a]"
using assms ide_one
by (metis pr_tuple(1) ide_char in_homE trm_in_hom)
also have "... = 𝗍[𝟭 ⊗ a]"
using assms ide_one trm_naturality [of "𝗅[a]"] by simp
also have "... = 𝔭⇩1[𝟭, a] ⋅ (𝟭 ⊗ a)"
by (simp add: assms ide_one pr_coincidence trm_one trm_tensor)
finally show ?thesis by simp
qed
qed
moreover have "ide (𝟭 ⊗ a)"
using assms ide_one by simp
finally show ?thesis by blast
qed
qed
lemma pr_expansion:
assumes "ide a" and "ide b"
shows "𝔭⇩0[a, b] = 𝗅[b] ⋅ (𝗍[a] ⊗ b)" and "𝔭⇩1[a, b] = 𝗋[a] ⋅ (a ⊗ 𝗍[b])"
using assms
by (auto simp add: comp_ide_arr)
lemma comp_lunit_term_dup:
assumes "ide a"
shows "𝗅[a] ⋅ (𝗍[a] ⊗ a) ⋅ 𝖽[a] = a"
using assms prod_tuple by force
lemma comp_runit_term_dup:
assumes "ide a"
shows "𝗋[a] ⋅ (a ⊗ 𝗍[a]) ⋅ 𝖽[a] = a"
using assms prod_tuple by force
lemma dup_coassoc:
assumes "ide a"
shows "𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a] = (a ⊗ 𝖽[a]) ⋅ 𝖽[a]"
proof (intro pr_joint_monic
[of a "a ⊗ a" "𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a]" "(a ⊗ 𝖽[a]) ⋅ 𝖽[a]"])
show "ide a" by fact
show "ide (a ⊗ a)"
by (simp add: assms)
show "seq 𝔭⇩0[a, a ⊗ a] (𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a])"
using assms by simp
show "𝔭⇩0[a, a ⊗ a] ⋅ 𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a] = 𝔭⇩0[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a]) ⋅ 𝖽[a]"
proof -
have "𝔭⇩0[a, a ⊗ a] ⋅ 𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a] =
((𝔭⇩0[a, a ⊗ a] ⋅ 𝖺[a, a, a]) ⋅ (𝖽[a] ⊗ a)) ⋅ 𝖽[a]"
using comp_assoc by simp
also have "... = ⟨((𝔭⇩0[a, a] ⋅ 𝔭⇩1[a ⊗ a, a]) ⋅ (𝖽[a] ⊗ a)) ⋅ 𝖽[a], (a ⋅ 𝔭⇩0[a, a]) ⋅ 𝖽[a]⟩"
using assms assoc_def by simp
also have "... = 𝖽[a]"
using assms comp_assoc by simp
also have "... = (𝔭⇩0[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a])) ⋅ 𝖽[a]"
using assms assoc_def comp_assoc by simp
also have "... = 𝔭⇩0[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a]) ⋅ 𝖽[a]"
using comp_assoc by simp
finally show ?thesis by blast
qed
show "𝔭⇩1[a, a ⊗ a] ⋅ 𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a] = 𝔭⇩1[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a]) ⋅ 𝖽[a]"
proof -
have "𝔭⇩1[a, a ⊗ a] ⋅ 𝖺[a, a, a] ⋅ (𝖽[a] ⊗ a) ⋅ 𝖽[a] =
((𝔭⇩1[a, a ⊗ a] ⋅ 𝖺[a, a, a]) ⋅ (𝖽[a] ⊗ a)) ⋅ 𝖽[a]"
using comp_assoc by simp
also have "... = ((𝔭⇩1[a, a] ⋅ 𝔭⇩1[a ⊗ a, a]) ⋅ (𝖽[a] ⊗ a)) ⋅ 𝖽[a]"
using assms assoc_def by simp
also have "... = a"
using assms comp_assoc by simp
also have "... = (a ⋅ 𝔭⇩1[a, a]) ⋅ 𝖽[a]"
using assms comp_assoc by simp
also have "... = (𝔭⇩1[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a])) ⋅ 𝖽[a]"
using assms by simp
also have "... = 𝔭⇩1[a, a ⊗ a] ⋅ (a ⊗ 𝖽[a]) ⋅ 𝖽[a]"
using comp_assoc by simp
finally show ?thesis by blast
qed
qed
lemma comp_assoc_tuple:
assumes "«f0 : a → b0»" and "«f1 : a → b1»" and "«f2 : a → b2»"
shows "𝖺[b0, b1, b2] ⋅ ⟨⟨f0, f1⟩, f2⟩ = ⟨f0, ⟨f1, f2⟩⟩"
and "𝖺⇧-⇧1[b0, b1, b2] ⋅ ⟨f0, ⟨f1, f2⟩⟩ = ⟨⟨f0, f1⟩, f2⟩"
using assms assoc_def assoc'_def comp_assoc by fastforce+
lemma dup_tensor:
assumes "ide a" and "ide b"
shows "𝖽[a ⊗ b] = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ 𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b])"
proof (intro pr_joint_monic [of "a ⊗ b" "a ⊗ b" "𝖽[a ⊗ b]"])
show "ide (a ⊗ b)" and "ide (a ⊗ b)"
by (auto simp add: assms)
show "seq 𝔭⇩0[a ⊗ b, a ⊗ b] (𝖽[a ⊗ b])"
using assms by simp
have 1: "𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ 𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b]) =
⟨a ⊗ b, a ⊗ b⟩"
proof -
have "𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ 𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b])
= 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ ⟨𝔭⇩1[a, b], ⟨𝔭⇩1[a, b], 𝖽[b] ⋅ 𝔭⇩0[a, b]⟩⟩"
proof -
have "𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b]) = ⟨𝔭⇩1[a, b], ⟨𝔭⇩1[a, b], 𝖽[b] ⋅ 𝔭⇩0[a, b]⟩⟩"
using assms assoc_def comp_assoc pr_naturality comp_cod_arr by simp
thus ?thesis by presburger
qed
also have "... = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅
⟨a ⋅ a ⋅ a ⋅ 𝔭⇩1[a, b],
𝖺[b, a, b] ⋅ (𝗌[a, b] ⋅ (a ⊗ b) ⊗ b) ⋅
𝖺⇧-⇧1[a, b, b] ⋅ ⟨𝔭⇩1[a, b], 𝖽[b ⋅ 𝔭⇩0[a, b]]⟩⟩"
using assms prod_tuple by simp
also have "... = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅
⟨𝔭⇩1[a, b],
𝖺[b, a, b] ⋅ (𝗌[a, b] ⊗ b) ⋅ 𝖺⇧-⇧1[a, b, b] ⋅ ⟨𝔭⇩1[a, b], 𝖽[𝔭⇩0[a, b]]⟩⟩"
proof -
have "a ⋅ a ⋅ a ⋅ 𝔭⇩1[a, b] = 𝔭⇩1[a, b]"
using assms comp_cod_arr by simp
moreover have "b ⋅ 𝔭⇩0[a, b] = 𝔭⇩0[a, b]"
using assms comp_cod_arr by simp
moreover have "𝗌[a, b] ⋅ (a ⊗ b) ⊗ b = 𝗌[a, b] ⊗ b"
using assms comp_arr_dom by simp
ultimately show ?thesis by simp
qed
also have "... = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ ⟨𝔭⇩1[a, b], 𝖺[b, a, b] ⋅ (𝗌[a, b] ⊗ b) ⋅
⟨⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩, 𝔭⇩0[a, b]⟩⟩"
proof -
have "𝖺⇧-⇧1[a, b, b] ⋅ ⟨𝔭⇩1[a, b], 𝖽[𝔭⇩0[a, b]]⟩ = ⟨⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩, 𝔭⇩0[a, b]⟩"
using assms comp_assoc_tuple(2) by blast
thus ?thesis by simp
qed
also have "... = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ ⟨𝔭⇩1[a, b], 𝖺[b, a, b] ⋅ ⟨𝗌[a, b], 𝔭⇩0[a, b]⟩⟩"
using assms prod_tuple comp_arr_dom comp_cod_arr by simp
also have "... = 𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ ⟨𝔭⇩1[a, b], ⟨𝔭⇩0[a, b], ⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩⟩⟩"
using assms comp_assoc_tuple(1)
by (metis sym_def pr_in_hom)
also have "... = ⟨⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩, ⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩⟩"
using assms comp_assoc_tuple(2)
by (metis ‹ide (a ⊗ b)› ide_in_hom pr_in_hom tuple_pr)
also have "... = 𝖽[a ⊗ b]"
using assms by simp
finally show ?thesis by simp
qed
show "𝔭⇩0[a ⊗ b, a ⊗ b] ⋅ 𝖽[a ⊗ b]
= 𝔭⇩0[a ⊗ b, a ⊗ b] ⋅
𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ 𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b])"
using assms 1 by force
show "𝔭⇩1[a ⊗ b, a ⊗ b] ⋅ 𝖽[a ⊗ b]
= 𝔭⇩1[a ⊗ b, a ⊗ b] ⋅
𝖺⇧-⇧1[a, b, a ⊗ b] ⋅ (a ⊗ 𝖺[b, a, b]) ⋅ (a ⊗ σ (a, b) ⊗ b) ⋅
(a ⊗ 𝖺⇧-⇧1[a, b, b]) ⋅ 𝖺[a, a, b ⊗ b] ⋅ (𝖽[a] ⊗ 𝖽[b])"
using assms 1 by force
qed
lemma terminal_tensor_one_one:
shows "terminal (𝟭 ⊗ 𝟭)"
proof
show "ide (𝟭 ⊗ 𝟭)"
using ide_one by simp
show "⋀a. ide a ⟹ ∃!f. «f : a → 𝟭 ⊗ 𝟭»"
proof -
fix a
assume a: "ide a"
show "∃!f. «f : a → 𝟭 ⊗ 𝟭»"
proof
show "«inv ι ⋅ 𝗍[a] : a → 𝟭 ⊗ 𝟭»"
using a ide_one inverse_arrows_ι inverse_unique trm_in_hom by fastforce
show "⋀f. «f : a → 𝟭 ⊗ 𝟭» ⟹ f = inv ι ⋅ 𝗍[a]"
by (metis ‹«local.inv ι ⋅ 𝗍[a] : a → 𝟭 ⊗ 𝟭»› a in_homE ide_one pr_coincidence
pr_joint_monic trm_naturality trm_simps(1) unit_eq_trm)
qed
qed
qed
end
subsection "Exponentials"
text ‹
The following prepare the way for the definition of cartesian closed categories.
The notion of exponential has to be defined in relation to products.
Here we use a generic choice of products for this purpose.
›
context cartesian_category
begin
definition has_as_exponential
where "has_as_exponential b c x e ≡
ide b ∧ ide x ∧ «e : some_prod x b → c» ∧
(∀a g. ide a ∧ «g : some_prod a b → c» ⟶
(∃!f. «f : a → x» ∧ g = C e (some_prod f b)))"
lemma has_as_exponentialI [intro]:
assumes "ide b" and "ide x" and "«e : some_prod x b → c»"
and "⋀a g. ⟦ide a; «g : some_prod a b → c»⟧ ⟹ ∃!f. «f : a → x» ∧ g = C e (some_prod f b)"
shows "has_as_exponential b c x e"
using assms has_as_exponential_def by simp
lemma has_as_exponentialE [elim]:
assumes "has_as_exponential b c x e"
and "⟦ide b; ide x; «e : some_prod x b → c»;
⋀a g. ⟦ide a; «g : some_prod a b → c»⟧ ⟹ ∃!f. «f : a → x» ∧ g = C e (some_prod f b)⟧
⟹ T"
shows T
using assms has_as_exponential_def by simp
lemma exponentials_are_isomorphic:
assumes "has_as_exponential b c x e" and "has_as_exponential b c x' e'"
shows "∃!h. «h : x → x'» ∧ e = e' ⋅ some_prod h b"
and "⋀h. ⟦«h : x → x'»; e = e' ⋅ (some_prod h b)⟧ ⟹ iso h"
proof -
have "ide b ∧ ide c"
using assms(1) has_as_exponential_def by auto
have "ide x ∧ «e : some_prod x b → c»"
using assms(1) has_as_exponential_def by blast
have "ide x' ∧ «e' : some_prod x' b → c»"
using assms(2) has_as_exponential_def by blast
show 1: "∃!h. «h : x → x'» ∧ e = e' ⋅ some_prod h b"
using assms has_as_exponential_def by simp
have 2: "∃!h. «h : x' → x» ∧ e' = e ⋅ some_prod h b"
using assms has_as_exponential_def by simp
have 3: "∃!h. «h : x → x» ∧ e = e ⋅ some_prod h b"
using assms has_as_exponential_def by simp
have 4: "∃!h. «h : x' → x'» ∧ e' = e' ⋅ some_prod h b"
using assms has_as_exponential_def by simp
have 5: "⋀h. «h : x → x» ∧ e = e ⋅ some_prod h b ⟹ h = x"
by (metis assms(1) 3 category.in_homE category_axioms comp_arr_dom has_as_exponential_def
partial_composition.ide_in_hom partial_composition_axioms)
have 6: "⋀h. «h : x' → x'» ∧ e' = e' ⋅ some_prod h b ⟹ h = x'"
by (metis assms(2) 4 category.in_homE category_axioms comp_arr_dom has_as_exponential_def
partial_composition.ide_in_hom partial_composition_axioms)
let ?f = "THE h. «h : x' → x» ∧ e' = e ⋅ some_prod h b"
let ?g = "THE h. «h : x → x'» ∧ e = e' ⋅ some_prod h b"
have "inverse_arrows ?f ?g"
proof
have "?g ⋅ ?f = x'"
proof -
have "«?g ⋅ ?f : x' → x'» ∧ e' = e' ⋅ some_prod ?g b ⋅ some_prod ?f b"
proof
show "«?g ⋅ ?f : x' → x'»"
using 1 2 theI [of "λh. «h : x → x'» ∧ e = e' ⋅ some_prod h b"]
theI [of "λh. «h : x' → x» ∧ e' = e ⋅ some_prod h b"]
by (meson comp_in_homI)
show "e' = e' ⋅ some_prod ?g b ⋅ some_prod ?f b"
using 1 2 theI [of "λh. «h : x → x'» ∧ e = e' ⋅ some_prod h b"]
theI [of "λh. «h : x' → x» ∧ e' = e ⋅ some_prod h b"]
by (metis (no_types, lifting) comp_assoc)
qed
hence "«?g ⋅ ?f : x' → x'» ∧ e' = e' ⋅ some_prod (?g ⋅ ?f) (b ⋅ b)"
by (metis (no_types, lifting) ‹ide b ∧ ide c› arrI ext
elementary_category_with_binary_products.interchange
extends_to_elementary_category_with_binary_products ide_def)
thus ?thesis
using 6
by (simp add: ‹ide b ∧ ide c›)
qed
thus "ide (?g ⋅ ?f)"
using ‹ide x' ∧ «e' : some_prod x' b → c»› by presburger
have "?f ⋅ ?g = x"
proof -
have "«?f ⋅ ?g : x → x» ∧ e = e ⋅ some_prod ?f b ⋅ some_prod ?g b"
proof
show "«?f ⋅ ?g : x → x»"
using 1 2 theI [of "λh. «h : x → x'» ∧ e = e' ⋅ some_prod h b"]
theI [of "λh. «h : x' → x» ∧ e' = e ⋅ some_prod h b"]
by (meson comp_in_homI)
show "e = e ⋅ some_prod ?f b ⋅ some_prod ?g b"
using 1 2 theI [of "λh. «h : x → x'» ∧ e = e' ⋅ some_prod h b"]
theI [of "λh. «h : x' → x» ∧ e' = e ⋅ some_prod h b"]
by (metis (no_types, lifting) comp_assoc)
qed
hence "«?f ⋅ ?g : x → x» ∧ e = e ⋅ some_prod (?f ⋅ ?g) (b ⋅ b)"
by (metis (no_types, lifting) ‹ide b ∧ ide c› arrI ext
elementary_category_with_binary_products.interchange
extends_to_elementary_category_with_binary_products ide_def)
thus ?thesis
using 5
by (simp add: ‹ide b ∧ ide c›)
qed
thus "ide (?f ⋅ ?g)"
using ‹ide x ∧ «e : some_prod x b → c»› by presburger
qed
hence "iso ?g"
by blast
moreover have "⋀h. ⟦«h : x → x'»; e = e' ⋅ (some_prod h b)⟧ ⟹ h = ?g"
using 1 theI [of "λh. «h : x → x'» ∧ e = e' ⋅ some_prod h b"] by auto
ultimately show "⋀h. ⟦«h : x → x'»; e = e' ⋅ (some_prod h b)⟧ ⟹ iso h" by simp
qed
end
section "Category with Finite Products"
text ‹
In this last section, we show that the notion ``cartesian category'', which we defined
to be a category with binary products and terminal object, coincides with the notion
``category with finite products''. Due to the inability to quantify over types in HOL,
we content ourselves with defining the latter notion as "has ‹I›-indexed products
for every finite set ‹I› of natural numbers." We can transfer this property to finite
sets at other types using the fact that products are preserved under bijections of
the index sets.
›
locale category_with_finite_products =
category C
for C :: "'c comp" +
assumes has_finite_products: "finite (I :: nat set) ⟹ has_products I"
begin
lemma has_finite_products':
assumes "I ≠ UNIV"
shows "finite I ⟹ has_products I"
proof -
assume I: "finite I"
obtain n φ where φ: "bij_betw φ {k. k < (n :: nat)} I"
using I finite_imp_nat_seg_image_inj_on inj_on_imp_bij_betw by fastforce
show "has_products I"
using assms(1) φ has_finite_products has_products_preserved_by_bijection
category_with_finite_products.has_finite_products
by blast
qed
end
lemma (in category) has_binary_products_if:
assumes "has_products ({0, 1} :: nat set)"
shows "has_binary_products"
proof (unfold has_binary_products_def)
show "∀a0 a1. ide a0 ∧ ide a1 ⟶ (∃p0 p1. has_as_binary_product a0 a1 p0 p1)"
proof (intro allI impI)
fix a0 a1
assume 1: "ide a0 ∧ ide a1"
show "∃p0 p1. has_as_binary_product a0 a1 p0 p1"
proof -
interpret J: binary_product_shape
by unfold_locales
interpret D: binary_product_diagram C a0 a1
using 1 by unfold_locales auto
interpret discrete_diagram J.comp C D.map
using J.is_discrete
by unfold_locales auto
show "∃p0 p1. has_as_binary_product a0 a1 p0 p1"
proof (unfold has_as_binary_product_def)
text ‹
Here we have to work around the fact that ‹has_finite_products› is defined
in terms of @{typ "nat set"}, whereas ‹has_as_binary_product› is defined
in terms of ‹J.arr set›.
›
let ?φ = "(λx :: nat. if x = 0 then J.FF else J.TT)"
let ?ψ = "λj. if j = J.FF then 0 else 1"
have 2: "∃a π. D.limit_cone a π"
proof -
have "bij_betw ?φ ({0, 1} :: nat set) {J.FF, J.TT}"
using bij_betwI [of ?φ "{0, 1} :: nat set" "{J.FF, J.TT}" ?ψ] by fastforce
hence "has_products {J.FF, J.TT}"
using assms has_products_def [of "{J.FF, J.TT}"]
has_products_preserved_by_bijection
[of "{0, 1} :: nat set" ?φ "{J.FF, J.TT}"]
by blast
hence "∃a. has_as_product J.comp D.map a"
using has_products_def [of "{J.FF, J.TT}"]
discrete_diagram_axioms J.arr_char
by blast
hence "∃a π. product_cone J.comp C D.map a π"
using has_as_product_def by blast
thus ?thesis
unfolding product_cone_def by simp
qed
obtain a π where π: "D.limit_cone a π"
using 2 by auto
interpret π: limit_cone J.comp C D.map a π
using π by auto
have "π = D.mkCone (π J.FF) (π J.TT)"
proof -
have "⋀a. J.ide a ⟹ π a = D.mkCone (π J.FF) (π J.TT) a"
using D.mkCone_def J.ide_char by auto
moreover have "a = dom (π J.FF)"
by simp
moreover have "D.cone a (D.mkCone (π (J.MkIde False)) (π (J.MkIde True)))"
using 1 D.cone_mkCone [of "π J.FF" "π J.TT"] by auto
ultimately show ?thesis
using D.mkCone_def π.natural_transformation_axioms
D.cone_mkCone [of "π J.FF" "π J.TT"]
NaturalTransformation.eqI
[of "J.comp" C π.A.map "D.map" π "D.mkCone (π J.FF) (π J.TT)"]
cone_def [of J.comp C D.map a "D.mkCone (π J.FF) (π J.TT)"] J.ide_char
by blast
qed
hence "D.limit_cone (dom (π J.FF)) (D.mkCone (π J.FF) (π J.TT))"
using π.limit_cone_axioms by simp
thus "∃p0 p1. ide a0 ∧ ide a1 ∧ D.has_as_binary_product p0 p1"
using 1 by blast
qed
qed
qed
qed
sublocale category_with_finite_products ⊆ category_with_binary_products C
using has_binary_products_if has_finite_products
by (unfold_locales, unfold has_binary_products_def) simp
proposition (in category_with_finite_products) is_category_with_binary_products⇩C⇩F⇩P:
shows "category_with_binary_products C"
..
sublocale category_with_finite_products ⊆ category_with_terminal_object C
proof
interpret J: discrete_category "{} :: nat set"
by unfold_locales auto
interpret D: empty_diagram J.comp C "λj. null"
by unfold_locales auto
interpret D: discrete_diagram J.comp C "λj. null"
using J.is_discrete by unfold_locales auto
have "⋀a. D.has_as_limit a ⟷ has_as_product J.comp (λj. null) a"
using product_cone_def J.category_axioms category_axioms D.discrete_diagram_axioms
has_as_product_def product_cone_def
by metis
moreover have "∃a. has_as_product J.comp (λj. null) a"
using has_finite_products [of "{} :: nat set"] has_products_def [of "{} :: nat set"]
D.discrete_diagram_axioms
by blast
ultimately have "∃a. D.has_as_limit a" by blast
thus "∃a. terminal a" using D.has_as_limit_iff_terminal by blast
qed
proposition (in category_with_finite_products) is_category_with_terminal_object⇩C⇩F⇩P:
shows "category_with_terminal_object C"
..
sublocale category_with_finite_products ⊆ cartesian_category ..
proposition (in category_with_finite_products) is_cartesian_category⇩C⇩F⇩P:
shows "cartesian_category C"
..
context category
begin
lemma binary_product_of_products_is_product:
assumes "has_as_product J0 D0 a0" and "has_as_product J1 D1 a1"
and "has_as_binary_product a0 a1 p0 p1"
and "Collect (partial_composition.arr J0) ∩ Collect (partial_composition.arr J1) = {}"
and "partial_magma.null J0 = partial_magma.null J1"
shows "has_as_product
(discrete_category.comp
(Collect (partial_composition.arr J0) ∪ Collect (partial_composition.arr J1))
(partial_magma.null J0))
(λi. if i ∈ Collect (partial_composition.arr J0) then D0 i
else if i ∈ Collect (partial_composition.arr J1) then D1 i
else null)
(dom p0)"
proof -
obtain π0 where π0: "product_cone J0 (⋅) D0 a0 π0"
using assms(1) has_as_product_def by blast
obtain π1 where π1: "product_cone J1 (⋅) D1 a1 π1"
using assms(2) has_as_product_def by blast
interpret J0: category J0
using π0 product_cone.axioms(1) by metis
interpret J1: category J1
using π1 product_cone.axioms(1) by metis
interpret D0: discrete_diagram J0 C D0
using π0 product_cone.axioms(3) by metis
interpret D1: discrete_diagram J1 C D1
using π1 product_cone.axioms(3) by metis
interpret π0: product_cone J0 C D0 a0 π0
using π0 by auto
interpret π1: product_cone J1 C D1 a1 π1
using π1 by auto
interpret J: discrete_category ‹Collect J0.arr ∪ Collect J1.arr› J0.null
using J0.not_arr_null assms(5) by unfold_locales auto
interpret X: binary_product_shape .
interpret a0xa1: binary_product_diagram C a0 a1
using assms(3) has_as_binary_product_def
by (simp add: binary_product_diagram.intro binary_product_diagram_axioms.intro
category_axioms)
have p0p1: "a0xa1.has_as_binary_product p0 p1"
using assms(3) has_as_binary_product_def [of a0 a1 p0 p1] by simp
let ?D = "(λi. if i ∈ Collect J0.arr then D0 i
else if i ∈ Collect J1.arr then D1 i
else null)"
let ?a = "dom p0"
let ?π = "λi. if i ∈ Collect J0.arr then π0 i ⋅ p0
else if i ∈ Collect J1.arr then π1 i ⋅ p1
else null"
let ?p0p1 = "a0xa1.mkCone p0 p1"
interpret p0p1: limit_cone X.comp C a0xa1.map ?a ?p0p1
using p0p1 by simp
have a: "ide ?a"
using p0p1.ide_apex by simp
have p0: "«p0 : ?a → a0»"
using a0xa1.mkCone_def p0p1.preserves_hom [of X.FF X.FF X.FF] X.ide_char X.ide_in_hom
by auto
have p1: "«p1 : ?a → a1»"
using a0xa1.mkCone_def p0p1.preserves_hom [of X.TT X.TT X.TT] X.ide_char X.ide_in_hom
by auto
interpret D: discrete_diagram J.comp C ?D
using assms J.arr_char J.dom_char J.cod_char J.is_discrete D0.is_discrete D1.is_discrete
J.cod_comp J.seq_char
by unfold_locales auto
interpret A: constant_functor J.comp C ?a
using p0p1.ide_apex by unfold_locales simp
interpret π: natural_transformation J.comp C A.map ?D ?π
proof
fix j
show "¬ J.arr j ⟹ ?π j = null"
by simp
assume j: "J.arr j"
have π0j: "J0.arr j ⟹ «π0 j : a0 → D0 j»"
using D0.is_discrete by auto
have π1j: "J1.arr j ⟹ «π1 j : a1 → D1 j»"
using D1.is_discrete by auto
show "dom (?π j) = A.map (J.dom j)"
using j J.arr_char p0 p1 π0j π1j
by fastforce
show "cod (?π j) = ?D (J.cod j)"
using j J.arr_char p0 p1 π0j π1j
by fastforce
show "?D j ⋅ ?π (J.dom j) = ?π j"
proof -
have 0: "J0.arr j ⟹ D0 j ⋅ π0 j ⋅ p0 = π0 j ⋅ p0"
by (metis D0.is_discrete J0.ide_char π0.is_natural_1 comp_assoc)
have 1: "J1.arr j ⟹ D1 j ⋅ π1 j ⋅ p1 = π1 j ⋅ p1"
by (metis D1.is_discrete J1.ide_char π1.is_natural_1 comp_assoc)
show ?thesis
using 0 1 by auto
qed
show "?π (J.cod j) ⋅ A.map j = ?π j"
using j comp_arr_dom p0 p1 comp_assoc by auto
qed
interpret π: cone J.comp C ?D ?a ?π ..
interpret π: product_cone J.comp C ?D ?a ?π
proof
show "⋀a' χ'. D.cone a' χ' ⟹ ∃!f. «f : a' → ?a» ∧ D.cones_map f ?π = χ'"
proof -
fix a' χ'
assume χ': "D.cone a' χ'"
interpret χ': cone J.comp C ?D a' χ'
using χ' by simp
show "∃!f. «f : a' → ?a» ∧ D.cones_map f ?π = χ'"
proof
let ?χ0' = "λi. if i ∈ Collect J0.arr then χ' i else null"
let ?χ1' = "λi. if i ∈ Collect J1.arr then χ' i else null"
have 0: "⋀i. i ∈ Collect J0.arr ⟹ χ' i ∈ hom a' (D0 i)"
using J.arr_char by auto
have 1: "⋀i. i ∈ Collect J1.arr ⟹ χ' i ∈ hom a' (D1 i)"
using J.arr_char ‹Collect J0.arr ∩ Collect J1.arr = {}› by force
interpret A0': constant_functor J0 C a'
apply unfold_locales using χ'.ide_apex by auto
interpret A1': constant_functor J1 C a'
apply unfold_locales using χ'.ide_apex by auto
interpret χ0': cone J0 C D0 a' ?χ0'
proof (unfold_locales)
fix j
show "¬ J0.arr j ⟹ (if j ∈ Collect J0.arr then χ' j else null) = null"
by simp
assume j: "J0.arr j"
show 0: "dom (?χ0' j) = A0'.map (J0.dom j)"
using j by simp
show 1: "cod (?χ0' j) = D0 (J0.cod j)"
using j J.arr_char J.cod_char D0.is_discrete by simp
show "D0 j ⋅ (?χ0' (J0.dom j)) = ?χ0' j"
using 1 j J.arr_char D0.is_discrete comp_cod_arr by simp
show "?χ0' (J0.cod j) ⋅ A0'.map j = ?χ0' j"
using 0 j J.arr_char D0.is_discrete comp_arr_dom by simp
qed
interpret χ1': cone J1 C D1 a' ?χ1'
proof (unfold_locales)
fix j
show "¬ J1.arr j ⟹ (if j ∈ Collect J1.arr then χ' j else null) = null"
by simp
assume j: "J1.arr j"
show 0: "dom (?χ1' j) = A1'.map (J1.dom j)"
using j by simp
show 1: "cod (?χ1' j) = D1 (J1.cod j)"
using assms(4) j J.arr_char J.cod_char D1.is_discrete by auto
show "D1 j ⋅ (?χ1' (J1.dom j)) = ?χ1' j"
using 1 j J.arr_char D1.is_discrete comp_cod_arr by simp
show "?χ1' (J1.cod j) ⋅ A1'.map j = ?χ1' j"
using 0 j J.arr_char D1.is_discrete comp_arr_dom by simp
qed
define f0 where "f0 = π0.induced_arrow a' ?χ0'"
define f1 where "f1 = π1.induced_arrow a' ?χ1'"
have f0: "«f0 : a' → a0»"
using f0_def π0.induced_arrowI χ0'.cone_axioms by simp
have f1: "«f1 : a' → a1»"
using f1_def π1.induced_arrowI χ1'.cone_axioms by simp
have 2: "a0xa1.is_rendered_commutative_by f0 f1"
using f0 f1 by auto
interpret p0p1: binary_product_cone C a0 a1 p0 p1 ..
interpret f0f1: cone X.comp C a0xa1.map a' ‹a0xa1.mkCone f0 f1›
using 2 f0 f1 a0xa1.cone_mkCone [of f0 f1] by auto
define f where "f = p0p1.induced_arrow a' (a0xa1.mkCone f0 f1)"
have f: "«f : a' → ?a»"
using f_def 2 f0 f1 p0p1.induced_arrowI'(1) by auto
moreover have χ': "D.cones_map f ?π = χ'"
proof
fix j
show "D.cones_map f ?π j = χ' j"
proof (cases "J0.arr j", cases "J1.arr j")
show "⟦J0.arr j; J1.arr j⟧ ⟹ D.cones_map f ?π j = χ' j"
using assms(4) by auto
show "⟦J0.arr j; ¬ J1.arr j⟧ ⟹ D.cones_map f ?π j = χ' j"
proof -
assume J0: "J0.arr j" and J1: "¬ J1.arr j"
have "D.cones_map f ?π j = (π0 j ⋅ p0) ⋅ f"
using f J0 J1 π.cone_axioms by auto
also have "... = π0 j ⋅ p0 ⋅ f"
using comp_assoc by simp
also have "... = π0 j ⋅ f0"
using 2 f0 f1 f_def p0p1.induced_arrowI' by auto
also have "... = χ' j"
proof -
have "π0 j ⋅ f0 = π0 j ⋅ π0.induced_arrow' a' χ'"
unfolding f0_def by simp
also have "... = (λj. if J0.arr j then
π0 j ⋅ π0.induced_arrow a'
(λi. if i ∈ Collect J0.arr then χ' i else null)
else null) j"
using J0 by simp
also have "... = D0.mkCone χ' j"
proof -
have "(λj. if J0.arr j then
π0 j ⋅ π0.induced_arrow a'
(λi. if i ∈ Collect J0.arr then χ' i else null)
else null) =
D0.mkCone χ'"
using f0 f0_def π0.induced_arrowI(2) [of ?χ0' a'] J0
D0.mkCone_cone χ0'.cone_axioms π0.cone_axioms J0
by auto
thus ?thesis by meson
qed
also have "... = χ' j"
using J0 by simp
finally show ?thesis by blast
qed
finally show ?thesis by simp
qed
show "¬ J0.arr j ⟹ D.cones_map f ?π j = χ' j"
proof (cases "J1.arr j")
show "⟦¬ J0.arr j; ¬ J1.arr j⟧ ⟹ D.cones_map f ?π j = χ' j"
using f π.cone_axioms χ'.is_extensional by auto
show "⟦¬ J0.arr j; J1.arr j⟧ ⟹ D.cones_map f ?π j = χ' j"
proof -
assume J0: "¬ J0.arr j" and J1: "J1.arr j"
have "D.cones_map f ?π j = (π1 j ⋅ p1) ⋅ f"
using J0 J1 f π.cone_axioms by auto
also have "... = π1 j ⋅ p1 ⋅ f"
using comp_assoc by simp
also have "... = π1 j ⋅ f1"
using 2 f0 f1 f_def p0p1.induced_arrowI' by auto
also have "... = χ' j"
proof -
have "π1 j ⋅ f1 = π1 j ⋅ π1.induced_arrow' a' χ'"
unfolding f1_def by simp
also have "... = (λj. if J1.arr j then
π1 j ⋅ π1.induced_arrow a'
(λi. if i ∈ Collect J1.arr
then χ' i else null)
else null) j"
using J1 by simp
also have "... = D1.mkCone χ' j"
proof -
have "(λj. if J1.arr j then
π1 j ⋅ π1.induced_arrow a'
(λi. if i ∈ Collect J1.arr then χ' i else null)
else null) =
D1.mkCone χ'"
using f1 f1_def π1.induced_arrowI(2) [of ?χ1' a'] J1
D1.mkCone_cone [of a' χ'] χ1'.cone_axioms π1.cone_axioms J1
by auto
thus ?thesis by meson
qed
also have "... = χ' j"
using J1 by simp
finally show ?thesis by blast
qed
finally show ?thesis by simp
qed
qed
qed
qed
ultimately show "«f : a' → ?a» ∧ D.cones_map f ?π = χ'" by blast
show "⋀f'. «f' : a' → ?a» ∧ D.cones_map f' ?π = χ' ⟹ f' = f"
proof -
fix f'
assume f': "«f' : a' → ?a» ∧ D.cones_map f' ?π = χ'"
let ?f0' = "p0 ⋅ f'"
let ?f1' = "p1 ⋅ f'"
have 1: "a0xa1.is_rendered_commutative_by ?f0' ?f1'"
using f' p0 p1 p0p1.renders_commutative seqI' by auto
have f0': "«?f0' : a' → a0»"
using f' p0 by auto
have f1': "«?f1' : a' → a1»"
using f' p1 by auto
have "p0 ⋅ f = p0 ⋅ f'"
proof -
have "D0.cones_map (p0 ⋅ f) π0 = ?χ0'"
using f p0 π0.cone_axioms χ' π.cone_axioms comp_assoc assms(4) seqI'
by fastforce
moreover have "D0.cones_map (p0 ⋅ f') π0 = ?χ0'"
using f' p0 π0.cone_axioms π.cone_axioms comp_assoc assms(4) seqI'
by fastforce
moreover have "p0 ⋅ f = f0"
using 2 f0 f_def p0p1.induced_arrowI'(2) by blast
ultimately show ?thesis
using f0 f0' χ0'.cone_axioms π0.is_universal [of a'] by auto
qed
moreover have "p1 ⋅ f = p1 ⋅ f'"
proof -
have "D1.cones_map (p1 ⋅ f) π1 = ?χ1'"
proof
fix j
show "D1.cones_map (p1 ⋅ f) π1 j = ?χ1' j"
using f p1 π1.cone_axioms χ' π.cone_axioms comp_assoc assms(4) seqI'
apply auto
by auto
qed
moreover have "D1.cones_map (p1 ⋅ f') π1 = ?χ1'"
proof
fix j
show "D1.cones_map (p1 ⋅ f') π1 j = ?χ1' j"
using f' p1 π1.cone_axioms π.cone_axioms comp_assoc assms(4) seqI'
apply auto
by auto
qed
moreover have "p1 ⋅ f = f1"
using 2 f1 f_def p0p1.induced_arrowI'(3) by blast
ultimately show ?thesis
using f1 f1' χ1'.cone_axioms π1.is_universal [of a'] by auto
qed
ultimately show "f' = f"
using f f' p0p1.is_universal' [of a']
by (metis (no_types, lifting) "1" dom_comp in_homE p0p1.is_universal' p1 seqI')
qed
qed
qed
qed
show "has_as_product J.comp ?D ?a"
unfolding has_as_product_def
using π.product_cone_axioms by auto
qed
end
sublocale cartesian_category ⊆ category_with_finite_products
proof
obtain t where t: "terminal t" using has_terminal by blast
{ fix n :: nat
have "⋀I :: nat set. finite I ∧ card I = n ⟹ has_products I"
proof (induct n)
show "⋀I :: nat set. finite I ∧ card I = 0 ⟹ has_products I"
proof -
fix I :: "nat set"
assume "finite I ∧ card I = 0"
hence I: "I = {}" by force
thus "has_products I"
proof -
interpret elementary_category_with_terminal_object C ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_category_with_terminal_object by blast
interpret J: discrete_category I 0
apply unfold_locales using I by auto
have "⋀D. discrete_diagram J.comp C D ⟹ ∃a. has_as_product J.comp D a"
proof -
fix D
assume D: "discrete_diagram J.comp C D"
interpret D: discrete_diagram J.comp C D using D by auto
interpret D: empty_diagram J.comp C D
using I J.arr_char by unfold_locales simp
have "has_as_product J.comp D t"
using t D.has_as_limit_iff_terminal has_as_product_def product_cone_def
J.category_axioms category_axioms D.discrete_diagram_axioms
by metis
thus "∃a. has_as_product J.comp D a" by blast
qed
moreover have "I ≠ UNIV"
using I by blast
ultimately show ?thesis
using I has_products_def
by (metis has_terminal discrete_diagram.product_coneI discrete_diagram_def
empty_diagram.has_as_limit_iff_terminal empty_diagram.intro
empty_diagram_axioms.intro empty_iff has_as_product_def mem_Collect_eq)
qed
qed
show "⋀n I :: nat set.
⟦ (⋀I :: nat set. finite I ∧ card I = n ⟹ has_products I);
finite I ∧ card I = Suc n ⟧
⟹ has_products I"
proof -
fix n :: nat
fix I :: "nat set"
assume IH: "⋀I :: nat set. finite I ∧ card I = n ⟹ has_products I"
assume I: "finite I ∧ card I = Suc n"
show "has_products I"
proof -
have "card I = 1 ⟹ has_products I"
using I has_unary_products by blast
moreover have "card I ≠ 1 ⟹ has_products I"
proof -
assume "card I ≠ 1"
hence cardI: "card I > 1" using I by simp
obtain i where i: "i ∈ I" using cardI by fastforce
let ?I0 = "{i}" and ?I1 = "I - {i}"
have 1: "I = ?I0 ∪ ?I1 ∧ ?I0 ∩ ?I1 = {} ∧ card ?I0 = 1 ∧ card ?I1 = n"
using i I cardI by auto
show "has_products I"
proof (unfold has_products_def, intro conjI allI impI)
show "I ≠ UNIV"
using I by auto
fix J D
assume D: "discrete_diagram J C D ∧ Collect (partial_composition.arr J) = I"
interpret D: discrete_diagram J C D
using D by simp
have Null: "D.J.null ∉ ?I0 ∧ D.J.null ∉ ?I1"
using D D.J.not_arr_null i by blast
interpret J0: discrete_category ?I0 D.J.null
using 1 Null D by unfold_locales auto
interpret J1: discrete_category ?I1 D.J.null
using Null by unfold_locales auto
interpret J0uJ1: discrete_category ‹Collect J0.arr ∪ Collect J1.arr› J0.null
using Null 1 J0.null_char J1.null_char by unfold_locales auto
interpret D0: discrete_diagram_from_map ?I0 C D D.J.null
using 1 J0.ide_char D.preserves_ide D D.is_discrete i by unfold_locales auto
interpret D1: discrete_diagram_from_map ?I1 C D D.J.null
using 1 J1.ide_char D.preserves_ide D D.is_discrete i by unfold_locales auto
obtain a0 where a0: "has_as_product J0.comp D0.map a0"
using 1 has_unary_products [of ?I0] has_products_def [of ?I0]
D0.discrete_diagram_axioms
by fastforce
obtain a1 where a1: "has_as_product J1.comp D1.map a1"
using 1 I IH [of ?I1] has_products_def [of ?I1] D1.discrete_diagram_axioms
by blast
have 2: "∃p0 p1. has_as_binary_product a0 a1 p0 p1"
proof -
have "ide a0 ∧ ide a1"
using a0 a1 product_is_ide by auto
thus ?thesis
using a0 a1 has_binary_products has_binary_products_def by simp
qed
obtain p0 p1 where a: "has_as_binary_product a0 a1 p0 p1"
using 2 by auto
let ?a = "dom p0"
have "has_as_product J D ?a"
proof -
have "D = (λj. if j ∈ Collect J0.arr then D0.map j
else if j ∈ Collect J1.arr then D1.map j
else null)"
proof
fix j
show "D j = (if j ∈ Collect J0.arr then D0.map j
else if j ∈ Collect J1.arr then D1.map j
else null)"
using 1 D0.map_def D1.map_def D.is_extensional D J0.arr_char J1.arr_char
by auto
qed
moreover have "J = J0uJ1.comp"
proof -
have "⋀j j'. J j j' = J0uJ1.comp j j'"
proof -
fix j j'
show "J j j' = J0uJ1.comp j j'"
using D J0uJ1.arr_char J0.arr_char J1.arr_char D.is_discrete i
apply (cases "j ∈ ?I0", cases "j' ∈ ?I0")
apply simp_all
apply auto[1]
apply (metis D.J.comp_arr_ide D.J.comp_ide_arr D.J.ext D.J.seqE
D.is_discrete J0.null_char J0uJ1.null_char)
by (metis D.J.comp_arr_ide D.J.comp_ide_arr D.J.comp_ide_self
D.J.ext D.J.seqE D.is_discrete J0.null_char J0uJ1.null_char
mem_Collect_eq)
qed
thus ?thesis by blast
qed
moreover have "Collect J0.arr ∩ Collect J1.arr = {}"
by auto
moreover have "J0.null = J1.null"
using J0.null_char J1.null_char by simp
ultimately show "has_as_product J D ?a"
using binary_product_of_products_is_product
[of J0.comp D0.map a0 J1.comp D1.map a1 p0 p1]
J0.arr_char J1.arr_char
1 a0 a1 a
by simp
qed
thus "∃a. has_as_product J D a" by blast
qed
qed
ultimately show "has_products I" by blast
qed
qed
qed
}
hence 1: "⋀n I :: nat set. finite I ∧ card I = n ⟹ has_products I" by simp
thus "⋀I :: nat set. finite I ⟹ has_products I" by blast
qed
proposition (in cartesian_category) is_category_with_finite_products:
shows "category_with_finite_products C"
..
end