Theory Category3.EpiMonoIso
chapter EpiMonoIso
theory EpiMonoIso
imports Category
begin
text‹
This theory defines and develops properties of epimorphisms, monomorphisms,
isomorphisms, sections, and retractions.
›
context category
begin
definition epi
where "epi f = (arr f ∧ inj_on (λg. g ⋅ f) {g. seq g f})"
definition mono
where "mono f = (arr f ∧ inj_on (λg. f ⋅ g) {g. seq f g})"
lemma epiI [intro]:
assumes "arr f" and "⋀g g'. ⟦seq g f; seq g' f; g ⋅ f = g' ⋅ f⟧ ⟹ g = g'"
shows "epi f"
using assms epi_def inj_on_def by blast
lemma epi_implies_arr:
assumes "epi f"
shows "arr f"
using assms epi_def by auto
lemma epi_cancel:
assumes "epi f"
and "seq g f" and "g ⋅ f = g' ⋅ f"
shows "g = g'"
using assms unfolding epi_def inj_on_def by auto
lemma monoI [intro]:
assumes "arr g" and "⋀f f'. ⟦seq g f; g ⋅ f = g ⋅ f'⟧ ⟹ f = f'"
shows "mono g"
using assms mono_def inj_on_def by blast
lemma mono_implies_arr:
assumes "mono f"
shows "arr f"
using assms mono_def by auto
lemma mono_cancel:
assumes "mono g"
and "seq g f" and "g ⋅ f = g ⋅ f'"
shows "f' = f"
using assms unfolding mono_def inj_on_def by auto
definition inverse_arrows
where "inverse_arrows f g ≡ ide (g ⋅ f) ∧ ide (f ⋅ g)"
lemma inverse_arrowsI [intro]:
assumes "ide (g ⋅ f)" and "ide (f ⋅ g)"
shows "inverse_arrows f g"
using assms inverse_arrows_def by blast
lemma inverse_arrowsE [elim]:
assumes "inverse_arrows f g"
and "⟦ ide (g ⋅ f); ide (f ⋅ g) ⟧ ⟹ T"
shows "T"
using assms inverse_arrows_def by blast
lemma inverse_arrows_sym:
shows "inverse_arrows f g ⟷ inverse_arrows g f"
using inverse_arrows_def by auto
lemma ide_self_inverse:
assumes "ide a"
shows "inverse_arrows a a"
using assms by auto
lemma inverse_arrow_unique:
assumes "inverse_arrows f g" and "inverse_arrows f g'"
shows "g = g'"
using assms apply (elim inverse_arrowsE)
by (metis comp_cod_arr ide_compE comp_assoc seqE)
lemma inverse_arrows_compose:
assumes "seq g f" and "inverse_arrows f f'" and "inverse_arrows g g'"
shows "inverse_arrows (g ⋅ f) (f' ⋅ g')"
using assms apply (elim inverse_arrowsE, intro inverse_arrowsI)
apply (metis seqE comp_arr_dom ide_compE comp_assoc)
by (metis seqE comp_arr_dom ide_compE comp_assoc)
definition "section"
where "section f ≡ ∃g. ide (g ⋅ f)"
lemma sectionI [intro]:
assumes "ide (g ⋅ f)"
shows "section f"
using assms section_def by auto
lemma sectionE [elim]:
assumes "section f"
obtains g where "ide (g ⋅ f)"
using assms section_def by blast
definition retraction
where "retraction g ≡ ∃f. ide (g ⋅ f)"
lemma retractionI [intro]:
assumes "ide (g ⋅ f)"
shows "retraction g"
using assms retraction_def by auto
lemma retractionE [elim]:
assumes "retraction g"
obtains f where "ide (g ⋅ f)"
using assms retraction_def by blast
lemma section_is_mono:
assumes "section g"
shows "mono g"
proof
show "arr g" using assms section_def by blast
from assms obtain h where h: "ide (h ⋅ g)" by blast
have hg: "seq h g" using h by auto
thus "⋀f f'. ⟦seq g f; g ⋅ f = g ⋅ f'⟧ ⟹ f = f'"
using hg h ide_compE seqE comp_assoc comp_cod_arr by metis
qed
lemma retraction_is_epi:
assumes "retraction g"
shows "epi g"
proof
show "arr g" using assms retraction_def by blast
from assms obtain f where f: "ide (g ⋅ f)" by blast
have gf: "seq g f" using f by auto
thus "⋀h h'. ⟦seq h g; seq h' g; h ⋅ g = h' ⋅ g⟧ ⟹ h = h'"
using gf f ide_compE seqE comp_assoc comp_arr_dom by metis
qed
lemma section_retraction_compose:
assumes "ide (e ⋅ m)" and "ide (e' ⋅ m')" and "seq m' m"
shows "ide ((e ⋅ e') ⋅ (m' ⋅ m))"
using assms seqI seqE ide_compE comp_assoc comp_arr_dom by metis
lemma sections_compose [intro]:
assumes "section m" and "section m'" and "seq m' m"
shows "section (m' ⋅ m)"
using assms section_def section_retraction_compose by metis
lemma retractions_compose [intro]:
assumes "retraction e" and "retraction e'" and "seq e' e"
shows "retraction (e' ⋅ e)"
proof -
from assms(1-2) obtain m m'
where *: "ide (e ⋅ m) ∧ ide (e' ⋅ m')"
using retraction_def by auto
hence "seq m m'"
using assms(3) by (metis seqE seqI ide_compE)
with * show ?thesis
using section_retraction_compose retractionI by blast
qed
lemma monos_compose [intro]:
assumes "mono m" and "mono m'" and "seq m' m"
shows "mono (m' ⋅ m)"
proof -
have "inj_on (λf. (m' ⋅ m) ⋅ f) {f. seq (m' ⋅ m) f}"
unfolding inj_on_def
using assms
by (metis CollectD seqE mono_cancel comp_assoc)
thus ?thesis using assms(3) mono_def by force
qed
lemma epis_compose [intro]:
assumes "epi e" and "epi e'" and "seq e' e"
shows "epi (e' ⋅ e)"
proof -
have "inj_on (λg. g ⋅ (e' ⋅ e)) {g. seq g (e' ⋅ e)}"
unfolding inj_on_def
using assms by (metis CollectD epi_cancel match_2 comp_assoc)
thus ?thesis using assms(3) epi_def by force
qed
definition iso
where "iso f ≡ ∃g. inverse_arrows f g"
lemma isoI [intro]:
assumes "inverse_arrows f g"
shows "iso f"
using assms iso_def by auto
lemma isoE [elim]:
assumes "iso f"
obtains g where "inverse_arrows f g"
using assms iso_def by blast
lemma ide_is_iso [simp]:
assumes "ide a"
shows "iso a"
using assms ide_self_inverse by auto
lemma iso_is_arr:
assumes "iso f"
shows "arr f"
using assms by blast
lemma iso_is_section:
assumes "iso f"
shows "section f"
using assms inverse_arrows_def by blast
lemma iso_is_retraction:
assumes "iso f"
shows "retraction f"
using assms inverse_arrows_def by blast
lemma iso_iff_mono_and_retraction:
shows "iso f ⟷ mono f ∧ retraction f"
proof
show "iso f ⟹ mono f ∧ retraction f"
by (simp add: iso_is_retraction iso_is_section section_is_mono)
show "mono f ∧ retraction f ⟹ iso f"
proof -
assume f: "mono f ∧ retraction f"
from f obtain g where g: "ide (f ⋅ g)" by blast
have "inverse_arrows f g"
using f g comp_arr_dom comp_cod_arr comp_assoc inverse_arrowsI
by (metis ide_char' ide_compE mono_cancel mono_implies_arr)
thus "iso f" by auto
qed
qed
lemma iso_iff_section_and_epi:
shows "iso f ⟷ section f ∧ epi f"
proof
show "iso f ⟹ section f ∧ epi f"
by (simp add: iso_is_retraction iso_is_section retraction_is_epi)
show "section f ∧ epi f ⟹ iso f"
proof -
assume f: "section f ∧ epi f"
from f obtain g where g: "ide (g ⋅ f)" by blast
have "inverse_arrows f g"
using f g comp_arr_dom comp_cod_arr epi_implies_arr
comp_assoc ide_compE inverse_arrowsI epi_cancel ide_char'
by metis
thus "iso f" by auto
qed
qed
lemma iso_iff_section_and_retraction:
shows "iso f ⟷ section f ∧ retraction f"
using iso_is_retraction iso_is_section iso_iff_mono_and_retraction section_is_mono
by auto
lemma isos_compose [intro]:
assumes "iso f" and "iso f'" and "seq f' f"
shows "iso (f' ⋅ f)"
proof -
from assms(1) obtain g where g: "inverse_arrows f g" by blast
from assms(2) obtain g' where g': "inverse_arrows f' g'" by blast
have "inverse_arrows (f' ⋅ f) (g ⋅ g')"
using assms g g inverse_arrowsI inverse_arrowsE section_retraction_compose
by (simp add: g' inverse_arrows_compose)
thus ?thesis using iso_def by auto
qed
lemma iso_cancel_left:
assumes "iso f" and "f ⋅ g = f ⋅ g'" and "seq f g"
shows "g = g'"
using assms iso_is_section section_is_mono mono_cancel by metis
lemma iso_cancel_right:
assumes "iso g" and "f ⋅ g = f' ⋅ g" and "seq f g" and "iso g"
shows "f = f'"
using assms iso_is_retraction retraction_is_epi epi_cancel by metis
definition isomorphic
where "isomorphic a a' = (∃f. «f : a → a'» ∧ iso f)"
lemma isomorphicI [intro]:
assumes "iso f"
shows "isomorphic (dom f) (cod f)"
using assms isomorphic_def iso_is_arr by blast
lemma isomorphicE [elim]:
assumes "isomorphic a a'"
obtains f where "«f : a → a'» ∧ iso f"
using assms isomorphic_def by meson
definition iso_in_hom (‹«_ : _ ≅ _»›)
where "iso_in_hom f a b ≡ «f : a → b» ∧ iso f"
lemma iso_in_homI [intro]:
assumes "«f : a → b»" and "iso f"
shows "«f : a ≅ b»"
using assms iso_in_hom_def by simp
lemma iso_in_homE [elim]:
assumes "«f : a ≅ b»"
and "⟦«f : a → b»; iso f⟧ ⟹ T"
shows T
using assms iso_in_hom_def by simp
lemma isomorphicI':
assumes "«f : a ≅ b»"
shows "isomorphic a b"
using assms iso_in_hom_def isomorphic_def by auto
lemma ide_iso_in_hom:
assumes "ide a"
shows "«a : a ≅ a»"
using assms by fastforce
lemma comp_iso_in_hom [intro]:
assumes "«f : a ≅ b»" and "«g : b ≅ c»"
shows "«g ⋅ f : a ≅ c»"
using assms iso_in_hom_def by auto
definition inv
where "inv f = (SOME g. inverse_arrows f g)"
lemma inv_is_inverse:
assumes "iso f"
shows "inverse_arrows f (inv f)"
using assms inv_def someI [of "inverse_arrows f"] by auto
lemma iso_inv_iso [intro, simp]:
assumes "iso f"
shows "iso (inv f)"
using assms inv_is_inverse inverse_arrows_sym by blast
lemma inverse_unique:
assumes "inverse_arrows f g"
shows "inv f = g"
using assms inv_is_inverse inverse_arrow_unique isoI by auto
lemma inv_ide [simp]:
assumes "ide a"
shows "inv a = a"
using assms by (simp add: inverse_arrowsI inverse_unique)
lemma inv_inv [simp]:
assumes "iso f"
shows "inv (inv f) = f"
using assms inverse_arrows_sym inverse_unique by blast
lemma comp_arr_inv:
assumes "inverse_arrows f g"
shows "f ⋅ g = dom g"
using assms by auto
lemma comp_inv_arr:
assumes "inverse_arrows f g"
shows "g ⋅ f = dom f"
using assms by auto
lemma comp_arr_inv':
assumes "iso f"
shows "f ⋅ inv f = cod f"
using assms inv_is_inverse by blast
lemma comp_inv_arr':
assumes "iso f"
shows "inv f ⋅ f = dom f"
using assms inv_is_inverse by blast
lemma inv_in_hom [simp]:
assumes "iso f" and "«f : a → b»"
shows "«inv f : b → a»"
using assms inv_is_inverse seqE inverse_arrowsE
by (metis ide_compE in_homE in_homI)
lemma arr_inv [simp]:
assumes "iso f"
shows "arr (inv f)"
using assms inv_in_hom by blast
lemma dom_inv [simp]:
assumes "iso f"
shows "dom (inv f) = cod f"
using assms inv_in_hom by blast
lemma cod_inv [simp]:
assumes "iso f"
shows "cod (inv f) = dom f"
using assms inv_in_hom by blast
lemma inv_comp:
assumes "iso f" and "iso g" and "seq g f"
shows "inv (g ⋅ f) = inv f ⋅ inv g"
using assms inv_is_inverse inverse_unique inverse_arrows_compose inverse_arrows_def
by meson
lemma isomorphic_reflexive:
assumes "ide f"
shows "isomorphic f f"
unfolding isomorphic_def
using assms ide_is_iso ide_in_hom by blast
lemma isomorphic_symmetric:
assumes "isomorphic f g"
shows "isomorphic g f"
using assms inv_in_hom by blast
lemma isomorphic_transitive [trans]:
assumes "isomorphic f g" and "isomorphic g h"
shows "isomorphic f h"
using assms isomorphic_def isos_compose by auto
text ‹
A section or retraction of an isomorphism is in fact an inverse.
›
lemma section_retraction_of_iso:
assumes "iso f"
shows "ide (g ⋅ f) ⟹ inverse_arrows f g"
and "ide (f ⋅ g) ⟹ inverse_arrows f g"
proof -
show "ide (g ⋅ f) ⟹ inverse_arrows f g"
using assms
by (metis comp_inv_arr' epi_cancel ide_compE inv_is_inverse
iso_iff_section_and_epi)
show "ide (f ⋅ g) ⟹ inverse_arrows f g"
using assms
by (metis ide_compE comp_arr_inv' inv_is_inverse iso_iff_mono_and_retraction
mono_cancel)
qed
text ‹
A situation that occurs frequently is that we have a commuting triangle,
but we need the triangle obtained by inverting one side that is an isomorphism.
The following fact streamlines this derivation.
›
lemma invert_side_of_triangle:
assumes "arr h" and "f ⋅ g = h"
shows "iso f ⟹ seq (inv f) h ∧ g = inv f ⋅ h"
and "iso g ⟹ seq h (inv g) ∧ f = h ⋅ inv g"
proof -
show "iso f ⟹ seq (inv f) h ∧ g = inv f ⋅ h"
by (metis assms seqE inv_is_inverse comp_cod_arr comp_inv_arr comp_assoc)
show "iso g ⟹ seq h (inv g) ∧ f = h ⋅ inv g"
by (metis assms seqE inv_is_inverse comp_arr_dom comp_arr_inv dom_inv comp_assoc)
qed
text ‹
A similar situation is where we have a commuting square and we want to
invert two opposite sides.
›
lemma invert_opposite_sides_of_square:
assumes "seq f g" and "f ⋅ g = h ⋅ k"
shows "⟦ iso f; iso k ⟧ ⟹ seq g (inv k) ∧ seq (inv f) h ∧ g ⋅ inv k = inv f ⋅ h"
by (metis assms invert_side_of_triangle comp_assoc)
text ‹
The following versions of ‹inv_comp› provide information needed for repeated
application to a composition of more than two arrows and seem often to be more
useful.
›
lemma inv_comp_left:
assumes "iso (g ⋅ f)" and "iso g"
shows "inv (g ⋅ f) = inv f ⋅ inv g" and "iso f"
proof -
have 1: "inv f = inv (g ⋅ f) ⋅ g"
proof -
have "inv (g ⋅ f) ⋅ g = inv (g ⋅ f) ⋅ inv (inv g)"
using assms by simp
also have "... = inv (inv g ⋅ g ⋅ f)"
using assms inv_comp iso_is_arr by simp
also have "... = inv ((inv g ⋅ g) ⋅ f)"
using comp_assoc by simp
also have "... = inv f"
using assms comp_ide_arr invert_side_of_triangle(1) iso_is_arr comp_assoc
by metis
finally show ?thesis by simp
qed
show "inv (g ⋅ f) = inv f ⋅ inv g"
using assms 1 comp_arr_dom comp_assoc
by (metis arr_inv cod_comp dom_inv invert_side_of_triangle(2) iso_is_arr seqI)
show "iso f"
using assms 1 comp_assoc inv_is_inverse
by (metis arr_inv invert_side_of_triangle(1) inv_inv iso_inv_iso isos_compose)
qed
lemma inv_comp_right:
assumes "iso (g ⋅ f)" and "iso f"
shows "inv (g ⋅ f) = inv f ⋅ inv g" and "iso g"
proof -
have 1: "inv g = f ⋅ inv (g ⋅ f)"
proof -
have "f ⋅ inv (g ⋅ f) = inv (inv f) ⋅ inv (g ⋅ f)"
using assms by simp
also have "... = inv ((g ⋅ f) ⋅ inv f)"
using assms inv_comp iso_is_arr by simp
also have "... = inv (g ⋅ f ⋅ inv f)"
using comp_assoc by simp
also have "... = inv g"
using assms comp_arr_dom invert_side_of_triangle(2) iso_is_arr comp_assoc
by metis
finally show ?thesis by simp
qed
show "inv (g ⋅ f) = inv f ⋅ inv g"
using assms 1 comp_cod_arr comp_assoc
by (metis arr_inv cod_inv dom_comp seqI invert_side_of_triangle(1) iso_is_arr)
show "iso g"
using assms 1 comp_assoc inv_is_inverse
by (metis arr_inv invert_side_of_triangle(2) inv_inv iso_inv_iso isos_compose)
qed
end
end