(* Title: EpiMonoIso Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) 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 (* * TODO: epiE and monoE don't need both seq hypotheses. * Also, they are not stated in the form of elimination rules. *) lemma epiE [elim]: assumes "epi f" and "seq g f" and "seq g' f" and "g ⋅ f = g' ⋅ f" shows "g = g'" using assms unfolding epi_def inj_on_def by blast lemma monoI [intro]: assumes "arr g" and "⋀f f'. ⟦seq g 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 monoE [elim]: assumes "mono g" and "seq g f" and "seq g f'" and "g ⋅ f = g ⋅ f'" shows "f' = f" using assms unfolding mono_def inj_on_def by blast 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; 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 monoE 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 epiE 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 monoE 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 epiE 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 monoE 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 epiE 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' epiE 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 monoE) 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