(* Title: InitialTerminal Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter InitialTerminal theory InitialTerminal imports EpiMonoIso begin text‹ This theory defines the notions of initial and terminal object in a category and establishes some properties of these notions, including that when they exist they are unique up to isomorphism. › context category begin definition initial where "initial a ≡ ide a ∧ (∀b. ide b ⟶ (∃!f. «f : a → b»))" definition terminal where "terminal b ≡ ide b ∧ (∀a. ide a ⟶ (∃!f. «f : a → b»))" abbreviation initial_arr where "initial_arr f ≡ arr f ∧ initial (dom f)" abbreviation terminal_arr where "terminal_arr f ≡ arr f ∧ terminal (cod f)" abbreviation point where "point f ≡ arr f ∧ terminal (dom f)" lemma initial_arr_unique: assumes "par f f'" and "initial_arr f" and "initial_arr f'" shows "f = f'" using assms in_homI initial_def ide_cod by blast lemma initialI [intro]: assumes "ide a" and "⋀b. ide b ⟹ ∃!f. «f : a → b»" shows "initial a" using assms initial_def by auto lemma initialE [elim]: assumes "initial a" and "ide b" obtains f where "«f : a → b»" and "⋀f'. «f' : a → b» ⟹ f' = f" using assms initial_def initial_arr_unique by meson lemma terminal_arr_unique: assumes "par f f'" and "terminal_arr f" and "terminal_arr f'" shows "f = f'" using assms in_homI terminal_def ide_dom by blast lemma terminalI [intro]: assumes "ide b" and "⋀a. ide a ⟹ ∃!f. «f : a → b»" shows "terminal b" using assms terminal_def by auto lemma terminalE [elim]: assumes "terminal b" and "ide a" obtains f where "«f : a → b»" and "⋀f'. «f' : a → b» ⟹ f' = f" using assms terminal_def terminal_arr_unique by meson lemma terminal_objs_isomorphic: assumes "terminal a" and "terminal b" shows "isomorphic a b" proof - from assms obtain f where f: "«f : a → b»" using terminal_def by meson from assms obtain g where g: "«g : b → a»" using terminal_def by meson have "iso f" using assms f g by (metis arr_iff_in_hom cod_comp retractionI sectionI seqI' terminal_def dom_comp in_homE iso_iff_section_and_retraction ide_in_hom) thus ?thesis using f by auto qed lemma isomorphic_to_terminal_is_terminal: assumes "terminal a" and "isomorphic a a'" shows "terminal a'" proof show "ide a'" using assms terminal_def isomorphic_def by auto obtain h h' where h: "«h : a → a'» ∧ inverse_arrows h h'" using assms isomorphic_def by auto fix b assume b: "ide b" obtain t where t: "«t : b → a»" using assms b by blast show "∃!f. «f : b → a'»" proof show "«h ⋅ t : b → a'»" using h t by blast show "⋀f. «f : b → a'» ⟹ f = h ⋅ t" proof - fix f assume f: "«f : b → a'»" have "«h' ⋅ f : b → a»" by (metis f h inv_in_hom inverse_unique comp_in_homI isoI) hence "h ⋅ h' ⋅ f = h ⋅ t" using assms f h terminal_def by (metis t terminal_arr_unique in_homE) thus "f = h ⋅ t" by (metis f h comp_arr_inv' comp_cod_arr inverse_unique in_homE isoI comp_assoc) qed qed qed lemma initial_objs_isomorphic: assumes "initial a" and "initial b" shows "isomorphic a b" proof - from assms obtain f where f: "«f : a → b»" using initial_def by auto from assms obtain g where g: "«g : b → a»" using initial_def by auto have "iso f" using assms f g by (metis (no_types, lifting) arr_iff_in_hom cod_comp in_homE initial_def retractionI sectionI dom_comp iso_iff_section_and_retraction ide_in_hom seqI') thus ?thesis using f by auto qed lemma isomorphic_to_initial_is_initial: assumes "initial a" and "isomorphic a a'" shows "initial a'" proof show "ide a'" using assms initial_def isomorphic_def by auto obtain h h' where h: "«h : a' → a» ∧ inverse_arrows h h'" using assms isomorphic_def by (meson isoE isomorphic_symmetric) fix b assume b: "ide b" obtain i where i: "«i : a → b»" using assms b by blast show "∃!f. «f : a' → b»" proof show "«i ⋅ h : a' → b»" using h i by blast show "⋀f. «f : a' → b» ⟹ f = i ⋅ h" proof - fix f assume f: "«f : a' → b»" have "«f ⋅ h' : a → b»" by (metis f h inv_in_hom inverse_unique comp_in_homI isoI) hence "f ⋅ h' ⋅ h = i ⋅ h" using assms f h initial_def comp_assoc by (metis i initial_arr_unique in_homE) thus "f = i ⋅ h" by (metis f h comp_inv_arr' comp_arr_dom inverse_unique in_homE isoI) qed qed qed lemma point_is_mono: assumes "point f" shows "mono f" proof - have "ide (cod f)" using assms by auto from this obtain t where t: "«t: cod f → dom f»" using assms terminal_def by blast thus ?thesis using assms terminal_def monoI by (metis seqE in_homI dom_comp ide_dom terminal_def) qed end end