(* Title: CategoryWithFiniteLimits Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2020 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) 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