Theory CategoryWithFiniteLimits
chapter "Category with Finite Limits"
theory CategoryWithFiniteLimits
imports CartesianCategory CategoryWithPullbacks
begin
text‹
In this chapter we define ``category with finite limits'' and show that such
categories coincide with those having pullbacks and a terminal object.
Since we can't quantify over types in HOL, the best we can do at defining the notion
``category with finite limits'' is to state it for a fixed choice of type (e.g.~@{typ nat})
for the arrows of the ``diagram shape''. However, we then have to go to some
trouble to show the existence of finite limits for diagram shapes at other types.
›
locale category_with_finite_limits =
category +
assumes has_finite_limits:
"⟦ category (J :: nat comp); finite (Collect (partial_composition.arr J)) ⟧
⟹ has_limits_of_shape J"
begin
text‹
We show that a category with finite limits has pullbacks and a terminal object
and is therefore also a cartesian category.
›
interpretation category_with_pullbacks C
proof -
interpret J: cospan_shape
by unfold_locales
have 1: "finite (Collect J.arr)"
proof -
have "Collect J.arr = {J.AA, J.BB, J.TT, J.AT, J.BT}"
using J.arr_char cospan_shape.Dom.cases by auto
thus ?thesis by simp
qed
obtain J' :: "nat comp" where J': "isomorphic_categories J' J.comp"
using 1 J.finite_imp_ex_iso_nat_comp by blast
interpret J'J: isomorphic_categories J' J.comp
using J' by simp
obtain φ ψ where φψ: "inverse_functors J.comp J' φ ψ"
using J'J.iso inverse_functors_sym by blast
interpret φψ: inverse_functors J.comp J' φ ψ
using φψ by simp
interpret ψ: invertible_functor J.comp J' ψ
using φψ.inverse_functors_axioms
by unfold_locales auto
show "category_with_pullbacks C"
proof
show "has_pullbacks"
proof (unfold has_pullbacks_def has_as_pullback_def, intro allI impI)
fix f0 f1
assume cospan: "cospan f0 f1"
interpret D: cospan_diagram C f0 f1
using cospan
by (simp add: category_axioms cospan_diagram_axioms_def cospan_diagram_def)
have 2: "has_limits_of_shape J.comp"
using 1 bij_betw_finite J'J.A.category_axioms has_finite_limits ψ.bij_betw_arr_sets
has_limits_preserved_by_isomorphism J'J.isomorphic_categories_axioms
by blast
obtain a χ where χ: "limit_cone J.comp C D.map a χ"
using 2 D.diagram_axioms has_limits_of_shape_def by blast
interpret χ: limit_cone J.comp C D.map a χ
using χ by simp
have "D.map = cospan_diagram.map C f0 f1" by simp
moreover have "a = dom (χ J.AA)"
using J.arr_char χ.component_in_hom by force
moreover have "χ = cospan_diagram.mkCone (⋅) f0 f1 (χ J.AA) (χ J.BB)"
using D.mkCone_cone χ.cone_axioms by auto
ultimately have "limit_cone (⋅⇩J) (⋅)
(cospan_diagram.map (⋅) f0 f1) (dom (χ J.AA))
(cospan_diagram.mkCone (⋅) f0 f1 (χ J.AA) (χ J.BB))"
using χ.limit_cone_axioms by simp
thus "∃p0 p1. cospan f0 f1 ∧
limit_cone (⋅⇩J) (⋅)
(cospan_diagram.map (⋅) f0 f1) (dom p0)
(cospan_diagram.mkCone (⋅) f0 f1 p0 p1)"
using cospan by auto
qed
qed
qed
lemma is_category_with_pullbacks:
shows "category_with_pullbacks C"
..
sublocale category_with_pullbacks C ..
interpretation category_with_terminal_object C
proof
show "∃a. terminal a"
proof -
interpret J: discrete_category ‹{} :: nat set› 0
by unfold_locales simp
have 1: "has_limits_of_shape J.comp"
using has_finite_limits
by (metis Collect_empty_eq J.arr_char J.is_category empty_iff finite.emptyI)
interpret D: diagram J.comp C ‹λ_. null›
by unfold_locales auto
obtain t τ where τ: "D.limit_cone t τ"
using 1 D.diagram_axioms has_limits_of_shape_def by blast
interpret τ: limit_cone J.comp C ‹λ_. null› t τ
using τ by simp
have "terminal t"
proof
show "ide t"
using τ.ide_apex by simp
fix a
assume a: "ide a"
show "∃!f. «f : a → t»"
proof -
interpret a: constant_functor J.comp C a
using a by unfold_locales
interpret χ: cone J.comp C ‹λ_.null› a ‹λ_.null›
apply unfold_locales
apply simp
using dom_null cod_null null_is_zero
by blast+
have "∃!f. «f : a → t» ∧ D.cones_map f τ = (λ_. null)"
using τ.induced_arrowI [of "λ_.null" a] χ.cone_axioms
τ.is_universal [of a "λ_. null"]
by simp
moreover have "⋀f. «f : a → t» ⟹ D.cones_map f τ = (λ_. null)"
using τ.cone_axioms by auto
ultimately show ?thesis by auto
qed
qed
thus ?thesis by blast
qed
qed
lemma is_category_with_terminal_object:
shows "category_with_terminal_object C"
..
sublocale category_with_terminal_object C ..
sublocale category_with_finite_products
using has_finite_limits has_finite_products_if_has_finite_limits
has_limits_of_shape_def diagram_def
by unfold_locales blast
sublocale cartesian_category ..
end
locale category_with_pullbacks_and_terminal =
category_with_pullbacks +
category_with_terminal_object
sublocale category_with_finite_limits ⊆ category_with_pullbacks_and_terminal ..
text‹
Conversely, we show that a category with pullbacks and a terminal object also
has finite products and equalizers, and therefore has finite limits.
›
context category_with_pullbacks_and_terminal
begin
interpretation ECP: elementary_category_with_pullbacks C some_prj0 some_prj1
using extends_to_elementary_category_with_pullbacks by simp
abbreviation some_prj0'
where "some_prj0' a b ≡ (if ide a ∧ ide b then some_prj0 𝗍⇧?[a] 𝗍⇧?[b] else null)"
abbreviation some_prj1'
where "some_prj1' a b ≡ (if ide a ∧ ide b then some_prj1 𝗍⇧?[a] 𝗍⇧?[b] else null)"
interpretation ECC: elementary_category_with_terminal_object C ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_category_with_terminal_object by blast
interpretation ECC: elementary_cartesian_category C some_prj0' some_prj1' ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using ECC.trm_naturality ECP.universal
by unfold_locales auto
interpretation category_with_equalizers C
proof (unfold_locales, unfold has_equalizers_def, intro allI impI)
fix f0 f1
assume par: "par f0 f1"
interpret J: parallel_pair
by unfold_locales
interpret D: parallel_pair_diagram C f0 f1
using par by unfold_locales auto
have 1: "cospan (ECC.prod f1 (dom f0)) (ECC.prod f0 (dom f0))"
using par by simp
let ?g0 = "ECC.prod f0 (dom f0) ⋅ ECC.dup (dom f0)"
let ?g1 = "ECC.prod f1 (dom f1) ⋅ ECC.dup (dom f1)"
have g0: "«?g0 : dom f0 → ECC.prod (cod f0) (dom f0)»"
using par by simp
have g1: "«?g1 : dom f1 → ECC.prod (cod f1) (dom f1)»"
using par by simp
define e0 where "e0 = 𝗉⇩0⇧?[?g1, ?g0]"
define e1 where "e1 = 𝗉⇩1⇧?[?g1, ?g0]"
have e0: "«e0 : dom e0 → dom f0»"
using par 1 e0_def by auto
have e1: "«e1 : dom e0 → dom f1»"
using par 1 e1_def e0_def by auto
have eq: "e0 = e1"
proof -
have "e1 = some_prj0' (cod f1) (dom f1) ⋅ ?g1 ⋅ e1"
proof -
have "((some_prj0' (cod f1) (dom f1) ⋅ (ECC.prod f1 (dom f1))) ⋅ ECC.dup (dom f1)) ⋅ e1 =
dom f1 ⋅ e1"
using par ECC.pr_naturality(1) [of "dom f1" "dom f1" "dom f1" f1 "dom f1" "cod f1"]
comp_cod_arr ECC.pr_dup(1)
by auto
also have "... = e1"
using par e1 comp_cod_arr by blast
finally show ?thesis
using comp_assoc by simp
qed
also have "... = some_prj0' (cod f1) (dom f1) ⋅ ?g0 ⋅ e0"
using par ECP.pullback_commutes
unfolding commutative_square_def e0_def e1_def by simp
also have "... = e0"
proof -
have "((some_prj0' (cod f1) (dom f1) ⋅ (ECC.prod f0 (dom f0))) ⋅ ECC.dup (dom f0)) ⋅ e0 =
dom f0 ⋅ e0"
using par ECC.pr_naturality(1) [of "dom f0" "dom f0" "dom f1" f0 "dom f0" "cod f0"]
comp_cod_arr ECC.pr_dup(1) ide_dom
by auto
also have "... = e0"
using e0 comp_cod_arr by blast
finally show ?thesis
using comp_assoc by simp
qed
finally show ?thesis by auto
qed
have equalizes: "D.is_equalized_by e0"
proof
show "seq f0 e0"
using par e0 by auto
show "f0 ⋅ e0 = f1 ⋅ e0"
proof -
have "f0 ⋅ e0 = (f0 ⋅ dom f0) ⋅ e0"
using par comp_arr_dom by simp
also have "... = (f0 ⋅ (some_prj1' (dom f0) (dom f0) ⋅ ECC.dup (dom f0))) ⋅ e0"
using par ECC.pr_dup(2) by auto
also have "... = ((f0 ⋅ some_prj1' (dom f0) (dom f0)) ⋅ ECC.dup (dom f0)) ⋅ e0"
using comp_assoc by auto
also have "... = some_prj1' (cod f1) (dom f1) ⋅ ?g0 ⋅ e0"
using par ECC.pr_naturality(2) [of "dom f0" "dom f0" "dom f1" f0 "dom f0" "cod f0"]
by (metis (no_types, lifting) arr_dom cod_dom dom_dom comp_assoc)
also have "... = some_prj1' (cod f1) (dom f1) ⋅ ?g1 ⋅ e1"
using par ECP.pullback_commutes [of ?g1 ?g0]
unfolding commutative_square_def e0_def e1_def by simp
also have "... = (some_prj1' (cod f1) (dom f1) ⋅ ?g1) ⋅ e1"
using comp_assoc by simp
also have "... = (f1 ⋅ (some_prj1' (dom f1) (dom f1) ⋅ ECC.dup (dom f1))) ⋅ e1"
using par ECC.pr_naturality(2) [of "dom f1" "dom f1" "dom f1" f1 "dom f1" "cod f1"]
by (metis (no_types, lifting) arr_dom cod_dom dom_dom comp_assoc)
also have "... = (f1 ⋅ dom f1) ⋅ e1"
using par ECC.pr_dup(2) by auto
also have "... = f1 ⋅ e1"
using par comp_arr_dom by simp
also have "... = f1 ⋅ e0"
using eq by simp
finally show ?thesis by simp
qed
qed
show "∃e. has_as_equalizer f0 f1 e"
proof
interpret E: constant_functor J.comp C ‹dom e0›
using par e0 by unfold_locales auto
interpret χ: cone J.comp C D.map ‹dom e0› ‹D.mkCone e0›
using equalizes D.cone_mkCone e0_def by auto
interpret χ: limit_cone J.comp C D.map ‹dom e0› ‹D.mkCone e0›
proof
show "⋀a' χ'. D.cone a' χ' ⟹
∃!f. «f : a' → dom e0» ∧ D.cones_map f (D.mkCone e0) = χ'"
proof -
fix a' χ'
assume χ': "D.cone a' χ'"
interpret χ': cone J.comp C D.map a' χ'
using χ' by simp
have 3: "commutative_square ?g1 ?g0 (χ' J.Zero) (χ' J.Zero)"
proof
show "cospan ?g1 ?g0"
using par g0 g1 by simp
show 4: "span (χ' J.Zero) (χ' J.Zero)"
using J.arr_char by simp
show 5: "dom ?g1 = cod (χ' J.Zero)"
using par g1 J.arr_char D.map_def by simp
show "?g1 ⋅ χ' J.Zero = ?g0 ⋅ χ' J.Zero"
proof -
have "?g1 ⋅ χ' J.Zero = ECC.prod f1 (dom f1) ⋅ ECC.dup (dom f1) ⋅ χ' J.Zero"
using comp_assoc by simp
also have "... = ECC.prod f1 (dom f1) ⋅ ECC.tuple (χ' J.Zero) (χ' J.Zero)"
using par D.map_def J.arr_char comp_cod_arr by auto
also have "... = ECC.tuple (f1 ⋅ χ' J.Zero) (χ' J.Zero)"
using par ECC.prod_tuple [of "χ' J.Zero" "χ' J.Zero" f1 "dom f1"]
comp_cod_arr
by (metis (no_types, lifting) 4 5 g1 in_homE seqI)
also have "... = ECC.tuple (f0 ⋅ χ' J.Zero) (χ' J.Zero)"
using par D.is_equalized_by_cone χ'.cone_axioms by auto
also have "... = ECC.prod f0 (dom f0) ⋅ ECC.tuple (χ' J.Zero) (χ' J.Zero)"
using par ECC.prod_tuple [of "χ' J.Zero" "χ' J.Zero" f0 "dom f0"]
comp_cod_arr
by (metis (no_types, lifting) 4 5 g1 in_homE seqI)
also have "... = ECC.prod f0 (dom f0) ⋅ ECC.dup (dom f0) ⋅ χ' J.Zero"
using par D.map_def J.arr_char comp_cod_arr by auto
also have "... = ?g0 ⋅ χ' J.Zero"
using comp_assoc by simp
finally show ?thesis by blast
qed
qed
show "∃!f. «f : a' → dom e0» ∧ D.cones_map f (D.mkCone e0) = χ'"
proof
define f where "f = ECP.tuple (χ' J.Zero) ?g1 ?g0 (χ' J.Zero)"
have 4: "e0 ⋅ f = χ' J.Zero"
using ECP.universal by (simp add: "3" e1_def eq f_def)
have f: "«f : a' → dom e0»"
proof -
have "a' = dom (χ' J.Zero)"
by (simp add: J.arr_char)
thus ?thesis
using 3 f_def e0_def g0 g1 ECP.tuple_in_hom ECP.pbdom_def by simp
qed
moreover have 5: "D.cones_map f (D.mkCone e0) = χ'"
proof -
have "⋀j. J.arr j ⟹ D.mkCone e0 j ⋅ f = χ' j"
proof -
fix j
assume j: "J.arr j"
show "D.mkCone e0 j ⋅ f = χ' j"
proof (cases "j = J.Zero")
case True
moreover have "e0 ⋅ f = χ' J.Zero"
using 4 by simp
ultimately show ?thesis
unfolding f_def D.mkCone_def comp_assoc
using J.arr_char by simp
next
case F: False
hence 1: "(f0 ⋅ e0) ⋅ f = f0 ⋅ χ' J.Zero"
using 4 comp_assoc by simp
also have "... = χ' j"
by (metis (no_types, lifting) F D.mkCone_cone D.mkCone_def
χ'.cone_axioms j)
finally show ?thesis
by (simp add: F D.mkCone_def j)
qed
qed
thus ?thesis
using f e0 χ.cone_axioms χ'.is_extensional by auto
qed
ultimately show "«f : a' → dom e0» ∧ D.cones_map f (D.mkCone e0) = χ'"
by simp
fix f'
assume f': "«f' : a' → dom e0» ∧ D.cones_map f' (D.mkCone e0) = χ'"
show "f' = f"
proof -
have "e0 ⋅ f' = χ' J.Zero"
using f' D.mkCone_cone D.mkCone_def χ'.cone_axioms
comp_assoc J.arr_char χ.cone_axioms
by auto
thus ?thesis
using f' 3 4 eq ECP.universal [of ?g1 ?g0 "e1 ⋅ f'" "e0 ⋅ f'"] e0_def e1_def
by (metis (no_types, lifting))
qed
qed
qed
qed
show "has_as_equalizer f0 f1 e0"
proof -
have "par f0 f1"
by fact
moreover have "D.has_as_equalizer e0"
..
ultimately show ?thesis
using has_as_equalizer_def by blast
qed
qed
qed
interpretation category_with_finite_products C
by (simp add: ECC.is_cartesian_category cartesian_category.is_category_with_finite_products)
lemma has_finite_products:
shows "category_with_finite_products C"
..
lemma has_finite_limits:
shows "category_with_finite_limits C"
proof
fix J :: "nat comp"
assume J: "category J"
interpret J: category J
using J by simp
assume finite: "finite (Collect J.arr)"
show "has_limits_of_shape J"
proof -
have "Collect (partial_composition.ide J) ⊆ Collect J.arr"
by auto
hence 1: "finite (Collect J.ide)"
using finite finite_subset by blast
have "has_products (Collect (partial_composition.ide J))"
using 1 J.ideD(1) J.not_arr_null ECC.has_finite_products by auto
moreover have "Collect (partial_composition.ide J) ≠ UNIV"
using J.not_arr_null by blast
moreover have "Collect (partial_composition.arr J) ≠ UNIV"
using J.not_arr_null by blast
ultimately show ?thesis
using finite 1 J.category_axioms has_limits_if_has_products
ECC.has_finite_products' [of "Collect J.ide"]
ECC.has_finite_products' [of "Collect J.arr"]
by simp
qed
qed
sublocale category_with_finite_limits C
using has_finite_limits by simp
end
end