Theory InitialTerminal
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