(* Title: EquivalenceOfCategories Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2017 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter "Equivalence of Categories" text ‹ In this chapter we define the notions of equivalence and adjoint equivalence of categories and establish some properties of functors that are part of an equivalence. › theory EquivalenceOfCategories imports Adjunction begin locale equivalence_of_categories = C: category C + D: category D + F: "functor" D C F + G: "functor" C D G + η: natural_isomorphism D D D.map "G o F" η + ε: natural_isomorphism C C "F o G" C.map ε for C :: "'c comp" (infixr "⋅⇩_{C}" 55) and D :: "'d comp" (infixr "⋅⇩_{D}" 55) and F :: "'d ⇒ 'c" and G :: "'c ⇒ 'd" and η :: "'d ⇒ 'd" and ε :: "'c ⇒ 'c" begin notation C.in_hom ("«_ : _ →⇩_{C}_»") notation D.in_hom ("«_ : _ →⇩_{D}_»") lemma C_arr_expansion: assumes "C.arr f" shows "ε (C.cod f) ⋅⇩_{C}F (G f) ⋅⇩_{C}C.inv (ε (C.dom f)) = f" and "C.inv (ε (C.cod f)) ⋅⇩_{C}f ⋅⇩_{C}ε (C.dom f) = F (G f)" proof - have ε_dom: "C.inverse_arrows (ε (C.dom f)) (C.inv (ε (C.dom f)))" using assms C.inv_is_inverse by auto have ε_cod: "C.inverse_arrows (ε (C.cod f)) (C.inv (ε (C.cod f)))" using assms C.inv_is_inverse by auto have "ε (C.cod f) ⋅⇩_{C}F (G f) ⋅⇩_{C}C.inv (ε (C.dom f)) = (ε (C.cod f) ⋅⇩_{C}F (G f)) ⋅⇩_{C}C.inv (ε (C.dom f))" using C.comp_assoc by force also have 1: "... = (f ⋅⇩_{C}ε (C.dom f)) ⋅⇩_{C}C.inv (ε (C.dom f))" using assms ε.naturality by simp also have 2: "... = f" using assms ε_dom C.comp_arr_inv C.comp_arr_dom C.comp_assoc by force finally show "ε (C.cod f) ⋅⇩_{C}F (G f) ⋅⇩_{C}C.inv (ε (C.dom f)) = f" by blast show "C.inv (ε (C.cod f)) ⋅⇩_{C}f ⋅⇩_{C}ε (C.dom f) = F (G f)" using assms 1 2 ε_dom ε_cod C.invert_side_of_triangle C.isoI C.iso_inv_iso by metis qed lemma G_is_faithful: shows "faithful_functor C D G" proof fix f f' assume par: "C.par f f'" and eq: "G f = G f'" show "f = f'" proof - have "C.inv (ε (C.cod f)) ∈ C.hom (C.cod f) (F (G (C.cod f))) ∧ C.iso (C.inv (ε (C.cod f)))" using par by auto moreover have 1: "ε (C.dom f) ∈ C.hom (F (G (C.dom f))) (C.dom f) ∧ C.iso (ε (C.dom f))" using par by auto ultimately have 2: "f ⋅⇩_{C}ε (C.dom f) = f' ⋅⇩_{C}ε (C.dom f)" using par C_arr_expansion eq C.iso_is_section C.section_is_mono by (metis C_arr_expansion(1) eq) show ?thesis proof - have "C.epi (ε (C.dom f))" using 1 par C.iso_is_retraction C.retraction_is_epi by blast thus ?thesis using 2 par by auto qed qed qed lemma G_is_essentially_surjective: shows "essentially_surjective_functor C D G" proof fix b assume b: "D.ide b" have "C.ide (F b) ∧ D.isomorphic (G (F b)) b" proof show "C.ide (F b)" using b by simp show "D.isomorphic (G (F b)) b" proof (unfold D.isomorphic_def) have "«D.inv (η b) : G (F b) →⇩_{D}b» ∧ D.iso (D.inv (η b))" using b by auto thus "∃f. «f : G (F b) →⇩_{D}b» ∧ D.iso f" by blast qed qed thus "∃a. C.ide a ∧ D.isomorphic (G a) b" by blast qed interpretation ε_inv: inverse_transformation C C ‹F o G› C.map ε .. interpretation η_inv: inverse_transformation D D D.map ‹G o F› η .. interpretation GF: equivalence_of_categories D C G F ε_inv.map η_inv.map .. lemma F_is_faithful: shows "faithful_functor D C F" using GF.G_is_faithful by simp lemma F_is_essentially_surjective: shows "essentially_surjective_functor D C F" using GF.G_is_essentially_surjective by simp lemma G_is_full: shows "full_functor C D G" proof fix a a' g assume a: "C.ide a" and a': "C.ide a'" assume g: "«g : G a →⇩_{D}G a'»" show "∃f. «f : a →⇩_{C}a'» ∧ G f = g" proof have εa: "C.inverse_arrows (ε a) (C.inv (ε a))" using a C.inv_is_inverse by auto have εa': "C.inverse_arrows (ε a') (C.inv (ε a'))" using a' C.inv_is_inverse by auto let ?f = "ε a' ⋅⇩_{C}F g ⋅⇩_{C}C.inv (ε a)" have f: "«?f : a →⇩_{C}a'»" using a a' g εa εa' ε.preserves_hom [of a' a' a'] ε_inv.preserves_hom [of a a a] by fastforce moreover have "G ?f = g" proof - interpret F: faithful_functor D C F using F_is_faithful by auto have "F (G ?f) = F g" proof - have "F (G ?f) = C.inv (ε a') ⋅⇩_{C}?f ⋅⇩_{C}ε a" using f C_arr_expansion(2) [of "?f"] by auto also have "... = (C.inv (ε a') ⋅⇩_{C}ε a') ⋅⇩_{C}F g ⋅⇩_{C}C.inv (ε a) ⋅⇩_{C}ε a" using a a' f g C.comp_assoc by fastforce also have "... = F g" using a a' g εa εa' C.comp_inv_arr C.comp_arr_dom C.comp_cod_arr by auto finally show ?thesis by blast qed moreover have "D.par (G (ε a' ⋅⇩_{C}F g ⋅⇩_{C}C.inv (ε a))) g" using f g by fastforce ultimately show ?thesis using f g F.is_faithful by blast qed ultimately show "«?f : a →⇩_{C}a'» ∧ G ?f = g" by blast qed qed end (* I'm not sure why I had to close and re-open the context here in order to * get the G_is_full fact in the interpretation GF. *) context equivalence_of_categories begin interpretation ε_inv: inverse_transformation C C ‹F o G› C.map ε .. interpretation η_inv: inverse_transformation D D D.map ‹G o F› η .. interpretation GF: equivalence_of_categories D C G F ε_inv.map η_inv.map .. lemma F_is_full: shows "full_functor D C F" using GF.G_is_full by simp end text ‹ Traditionally the term "equivalence of categories" is also used for a functor that is part of an equivalence of categories. However, it seems best to use that term for a situation in which all of the structure of an equivalence is explicitly given, and to have a different term for one of the functors involved. › locale equivalence_functor = C: category C + D: category D + "functor" C D G for C :: "'c comp" (infixr "⋅⇩_{C}" 55) and D :: "'d comp" (infixr "⋅⇩_{D}" 55) and G :: "'c ⇒ 'd" + assumes induces_equivalence: "∃F η ε. equivalence_of_categories C D F G η ε" begin notation C.in_hom ("«_ : _ →⇩_{C}_»") notation D.in_hom ("«_ : _ →⇩_{D}_»") end sublocale equivalence_of_categories ⊆ equivalence_functor C D G using equivalence_of_categories_axioms by (unfold_locales, blast) text ‹ An equivalence functor is fully faithful and essentially surjective. › sublocale equivalence_functor ⊆ fully_faithful_functor C D G proof - obtain F η ε where 1: "equivalence_of_categories C D F G η ε" using induces_equivalence by blast interpret equivalence_of_categories C D F G η ε using 1 by auto show "fully_faithful_functor C D G" using G_is_full G_is_faithful fully_faithful_functor.intro by auto qed sublocale equivalence_functor ⊆ essentially_surjective_functor C D G proof - obtain F η ε where 1: "equivalence_of_categories C D F G η ε" using induces_equivalence by blast interpret equivalence_of_categories C D F G η ε using 1 by auto show "essentially_surjective_functor C D G" using G_is_essentially_surjective by auto qed lemma (in inverse_functors) induce_equivalence: shows "equivalence_of_categories A B F G B.map A.map" using inv inv' A.is_extensional B.is_extensional B.comp_arr_dom B.comp_cod_arr A.comp_arr_dom A.comp_cod_arr by unfold_locales auto lemma (in invertible_functor) is_equivalence: shows "equivalence_functor A B G" using equivalence_functor_axioms.intro equivalence_functor_def equivalence_of_categories_def induce_equivalence by blast lemma (in identity_functor) is_equivalence: shows "equivalence_functor C C map" proof - interpret inverse_functors C C map map using map_def by unfold_locales auto interpret invertible_functor C C map using inverse_functors_axioms by unfold_locales blast show ?thesis using is_equivalence by blast qed text ‹ A special case of an equivalence functor is an endofunctor ‹F› equipped with a natural isomorphism from ‹F› to the identity functor. › context endofunctor begin lemma isomorphic_to_identity_is_equivalence: assumes "natural_isomorphism A A F A.map φ" shows "equivalence_functor A A F" proof - interpret φ: natural_isomorphism A A F A.map φ using assms by auto interpret φ': inverse_transformation A A F A.map φ .. interpret Fφ': natural_isomorphism A A F ‹F o F› ‹F o φ'.map› proof - interpret Fφ': natural_transformation A A F ‹F o F› ‹F o φ'.map› using φ'.natural_transformation_axioms functor_axioms horizontal_composite [of A A A.map F φ'.map A F F F] by simp show "natural_isomorphism A A F (F o F) (F o φ'.map)" apply unfold_locales using φ'.components_are_iso by fastforce qed interpret Fφ'oφ': vertical_composite A A A.map F ‹F o F› φ'.map ‹F o φ'.map› .. interpret Fφ'oφ': natural_isomorphism A A A.map ‹F o F› Fφ'oφ'.map using φ'.natural_isomorphism_axioms Fφ'.natural_isomorphism_axioms natural_isomorphisms_compose by fast interpret inv_Fφ'oφ': inverse_transformation A A A.map ‹F o F› Fφ'oφ'.map .. interpret F: equivalence_of_categories A A F F Fφ'oφ'.map inv_Fφ'oφ'.map .. show ?thesis .. qed end text ‹ An adjoint equivalence is an equivalence of categories that is also an adjunction. › locale adjoint_equivalence = unit_counit_adjunction C D F G η ε + η: natural_isomorphism D D D.map "G o F" η + ε: natural_isomorphism C C "F o G" C.map ε for C :: "'c comp" (infixr "⋅⇩_{C}" 55) and D :: "'d comp" (infixr "⋅⇩_{D}" 55) and F :: "'d ⇒ 'c" and G :: "'c ⇒ 'd" and η :: "'d ⇒ 'd" and ε :: "'c ⇒ 'c" text ‹ An adjoint equivalence is clearly an equivalence of categories. › sublocale adjoint_equivalence ⊆ equivalence_of_categories .. context adjoint_equivalence begin text ‹ The triangle identities for an adjunction reduce to inverse relations when ‹η› and ‹ε› are natural isomorphisms. › lemma triangle_G': assumes "C.ide a" shows "D.inverse_arrows (η (G a)) (G (ε a))" proof show "D.ide (G (ε a) ⋅⇩_{D}η (G a))" using assms triangle_G GεoηG.map_simp_ide by fastforce thus "D.ide (η (G a) ⋅⇩_{D}G (ε a))" using assms D.section_retraction_of_iso [of "G (ε a)" "η (G a)"] by auto qed lemma triangle_F': assumes "D.ide b" shows "C.inverse_arrows (F (η b)) (ε (F b))" proof show "C.ide (ε (F b) ⋅⇩_{C}F (η b))" using assms triangle_F εFoFη.map_simp_ide by auto thus "C.ide (F (η b) ⋅⇩_{C}ε (F b))" using assms C.section_retraction_of_iso [of "ε (F b)" "F (η b)"] by auto qed text ‹ An adjoint equivalence can be dualized by interchanging the two functors and inverting the natural isomorphisms. This is somewhat awkward to prove, but probably useful to have done it once and for all. › lemma dual_equivalence: assumes "adjoint_equivalence C D F G η ε" shows "adjoint_equivalence D C G F (inverse_transformation.map C C (C.map) ε) (inverse_transformation.map D D (G o F) η)" proof - interpret adjoint_equivalence C D F G η ε using assms by auto interpret ε': inverse_transformation C C ‹F o G› C.map ε .. interpret η': inverse_transformation D D D.map ‹G o F› η .. interpret Gε': natural_transformation C D G ‹G o F o G› ‹G o ε'.map› proof - have "natural_transformation C D G (G o (F o G)) (G o ε'.map)" using G.as_nat_trans.natural_transformation_axioms ε'.natural_transformation_axioms horizontal_composite by fastforce thus "natural_transformation C D G (G o F o G) (G o ε'.map)" using o_assoc by metis qed interpret η'G: natural_transformation C D ‹G o F o G› G ‹η'.map o G› using η'.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce interpret ε'F: natural_transformation D C F ‹F o G o F› ‹ε'.map o F› using ε'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce interpret Fη': natural_transformation D C ‹F o G o F› F ‹F o η'.map› proof - have "natural_transformation D C (F o (G o F)) F (F o η'.map)" using η'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce thus "natural_transformation D C (F o G o F) F (F o η'.map)" using o_assoc by metis qed interpret Fη'oε'F: vertical_composite D C F ‹(F o G) o F› F ‹ε'.map o F› ‹F o η'.map› .. interpret η'GoGε': vertical_composite C D G ‹G o F o G› G ‹G o ε'.map› ‹η'.map o G› .. show ?thesis proof show "η'GoGε'.map = G" proof (intro NaturalTransformation.eqI) show "natural_transformation C D G G G" using G.as_nat_trans.natural_transformation_axioms by auto show "natural_transformation C D G G η'GoGε'.map" using η'GoGε'.natural_transformation_axioms by auto show "⋀a. C.ide a ⟹ η'GoGε'.map a = G a" proof - fix a assume a: "C.ide a" show "η'GoGε'.map a = G a" using a η'GoGε'.map_simp_ide triangle_G' G.preserves_ide η'.inverts_components ε'.inverts_components D.inverse_unique G.preserves_inverse_arrows GεoηG.map_simp_ide D.inverse_arrows_sym triangle_G by (metis o_apply) qed qed show "Fη'oε'F.map = F" proof (intro NaturalTransformation.eqI) show "natural_transformation D C F F F" using F.as_nat_trans.natural_transformation_axioms by auto show "natural_transformation D C F F Fη'oε'F.map" using Fη'oε'F.natural_transformation_axioms by auto show "⋀b. D.ide b ⟹ Fη'oε'F.map b = F b" proof - fix b assume b: "D.ide b" show "Fη'oε'F.map b = F b" using b Fη'oε'F.map_simp_ide εFoFη.map_simp_ide triangle_F triangle_F' η'.inverts_components ε'.inverts_components F.preserves_ide C.inverse_unique F.preserves_inverse_arrows C.inverse_arrows_sym by (metis o_apply) qed qed qed qed end text ‹ Every fully faithful and essentially surjective functor underlies an adjoint equivalence. To prove this without repeating things that were already proved in @{theory Category3.Adjunction}, we first show that a fully faithful and essentially surjective functor is a left adjoint functor, and then we show that if the left adjoint in a unit-counit adjunction is fully faithful and essentially surjective, then the unit and counit are natural isomorphisms; hence the adjunction is in fact an adjoint equivalence. › locale fully_faithful_and_essentially_surjective_functor = C: category C + D: category D + fully_faithful_functor C D F + essentially_surjective_functor C D F for C :: "'c comp" (infixr "⋅⇩_{C}" 55) and D :: "'d comp" (infixr "⋅⇩_{D}" 55) and F :: "'c ⇒ 'd" begin notation C.in_hom ("«_ : _ →⇩_{C}_»") notation D.in_hom ("«_ : _ →⇩_{D}_»") lemma is_left_adjoint_functor: shows "left_adjoint_functor C D F" proof fix y assume y: "D.ide y" let ?x = "SOME x. C.ide x ∧ (∃e. D.iso e ∧ «e : F x →⇩_{D}y»)" let ?e = "SOME e. D.iso e ∧ «e : F ?x →⇩_{D}y»" have "∃x e. D.iso e ∧ terminal_arrow_from_functor C D F x y e" proof - have "∃x. D.iso ?e ∧ terminal_arrow_from_functor C D F x y ?e" proof - have x: "C.ide ?x ∧ (∃e. D.iso e ∧ «e : F ?x →⇩_{D}y»)" using y essentially_surjective someI_ex [of "λx. C.ide x ∧ (∃e. D.iso e ∧ «e : F x →⇩_{D}y»)"] by blast hence e: "D.iso ?e ∧ «?e : F ?x →⇩_{D}y»" using someI_ex [of "λe. D.iso e ∧ «e : F ?x →⇩_{D}y»"] by blast interpret arrow_from_functor C D F ?x y ?e using x e by (unfold_locales, simp) interpret terminal_arrow_from_functor C D F ?x y ?e proof fix x' f assume 1: "arrow_from_functor C D F x' y f" interpret f: arrow_from_functor C D F x' y f using 1 by simp have f: "«f: F x' →⇩_{D}y»" by (meson f.arrow) show "∃!g. is_coext x' f g" proof let ?g = "SOME g. «g : x' →⇩_{C}?x» ∧ F g = D.inv ?e ⋅⇩_{D}f" have g: "«?g : x' →⇩_{C}?x» ∧ F ?g = D.inv ?e ⋅⇩_{D}f" using f e x f.arrow is_full D.comp_in_homI D.inv_in_hom someI_ex [of "λg. «g : x' →⇩_{C}?x» ∧ F g = D.inv ?e ⋅⇩_{D}f"] by auto show 1: "is_coext x' f ?g" proof - have "«?g : x' →⇩_{C}?x»" using g by simp moreover have "?e ⋅⇩_{D}F ?g = f" proof - have "?e ⋅⇩_{D}F ?g = ?e ⋅⇩_{D}D.inv ?e ⋅⇩_{D}f" using g by simp also have "... = (?e ⋅⇩_{D}D.inv ?e) ⋅⇩_{D}f" using e f D.inv_in_hom by (metis D.comp_assoc) also have "... = f" proof - have "?e ⋅⇩_{D}D.inv ?e = y" using e D.comp_arr_inv D.inv_is_inverse by auto thus ?thesis using f D.comp_cod_arr by auto qed finally show ?thesis by blast qed ultimately show ?thesis unfolding is_coext_def by simp qed show "⋀g'. is_coext x' f g' ⟹ g' = ?g" proof - fix g' assume g': "is_coext x' f g'" have 2: "«g' : x' →⇩_{C}?x» ∧ ?e ⋅⇩_{D}F g' = f" using g' is_coext_def by simp have 3: "«?g : x' →⇩_{C}?x» ∧ ?e ⋅⇩_{D}F ?g = f" using 1 is_coext_def by simp have "F g' = F ?g" using e f 2 3 D.iso_is_section D.section_is_mono D.monoE D.arrI by (metis (no_types, lifting) D.arrI) moreover have "C.par g' ?g" using 2 3 by fastforce ultimately show "g' = ?g" using is_faithful [of g' ?g] by simp qed qed qed show ?thesis using e terminal_arrow_from_functor_axioms by auto qed thus ?thesis by auto qed thus "∃x e. terminal_arrow_from_functor C D F x y e" by blast qed lemma extends_to_adjoint_equivalence: shows "∃G η ε. adjoint_equivalence C D G F η ε" proof - interpret left_adjoint_functor C D F using is_left_adjoint_functor by blast interpret Adj: meta_adjunction D C F G φ ψ using induces_meta_adjunction by simp interpret S: replete_setcat . interpret Adj: adjunction D C S.comp S.setp Adj.φC Adj.φD F G φ ψ Adj.η Adj.ε Adj.Φ Adj.Ψ using induces_adjunction by simp interpret equivalence_of_categories D C F G Adj.η Adj.ε proof show 1: "⋀a. D.ide a ⟹ D.iso (Adj.ε a)" proof - fix a assume a: "D.ide a" interpret εa: terminal_arrow_from_functor C D F ‹G a› a ‹Adj.ε a› using a Adj.has_terminal_arrows_from_functor [of a] by blast have "D.retraction (Adj.ε a)" proof - obtain b φ where φ: "C.ide b ∧ D.iso φ ∧ «φ: F b →⇩_{D}a»" using a essentially_surjective by blast interpret φ: arrow_from_functor C D F b a φ using φ by (unfold_locales, simp) let ?g = "εa.the_coext b φ" have 1: "«?g : b →⇩_{C}G a» ∧ Adj.ε a ⋅⇩_{D}F ?g = φ" using φ.arrow_from_functor_axioms εa.the_coext_prop [of b φ] by simp have "a = (Adj.ε a ⋅⇩_{D}F ?g) ⋅⇩_{D}D.inv φ" using a 1 φ D.comp_cod_arr Adj.ε.preserves_hom D.invert_side_of_triangle(2) by auto also have "... = Adj.ε a ⋅⇩_{D}F ?g ⋅⇩_{D}D.inv φ" using a 1 φ D.inv_in_hom Adj.ε.preserves_hom [of a a a] D.comp_assoc by blast finally have "∃f. D.ide (Adj.ε a ⋅⇩_{D}f)" using a by metis thus ?thesis unfolding D.retraction_def by blast qed moreover have "D.mono (Adj.ε a)" proof show "D.arr (Adj.ε a)" using a by simp show "⋀f f'. ⟦D.seq (Adj.ε a) f; D.seq (Adj.ε a) f'; Adj.ε a ⋅⇩_{D}f = Adj.ε a ⋅⇩_{D}f'⟧ ⟹ f = f'" proof - fix f f' assume seq: "D.seq (Adj.ε a) f" and seq': "D.seq (Adj.ε a) f'" and eq: "Adj.ε a ⋅⇩_{D}f = Adj.ε a ⋅⇩_{D}f'" have f: "«f : D.dom f →⇩_{D}F (G a)»" using a seq Adj.ε.preserves_hom [of a a a] by fastforce have f': "«f' : D.dom f' →⇩_{D}F (G a)»" using a seq' Adj.ε.preserves_hom [of a a a] by fastforce have par: "D.par f f'" using f f' seq eq D.dom_comp [of "Adj.ε a" f] by force obtain b' φ where φ: "C.ide b' ∧ D.iso φ ∧ «φ: F b' →⇩_{D}D.dom f»" using par essentially_surjective D.ide_dom [of f] by blast have 1: "Adj.ε a ⋅⇩_{D}f ⋅⇩_{D}φ = Adj.ε a ⋅⇩_{D}f' ⋅⇩_{D}φ" using eq φ par D.comp_assoc by metis obtain g where g: "«g : b' →⇩_{C}G a» ∧ F g = f ⋅⇩_{D}φ" using a f φ is_full [of "G a" b' "f ⋅⇩_{D}φ"] by auto obtain g' where g': "«g' : b' →⇩_{C}G a» ∧ F g' = f' ⋅⇩_{D}φ" using a f' par φ is_full [of "G a" b' "f' ⋅⇩_{D}φ"] by auto interpret fφ: arrow_from_functor C D F b' a ‹Adj.ε a ⋅⇩_{D}f ⋅⇩_{D}φ› using a φ f Adj.ε.preserves_hom by (unfold_locales, fastforce) interpret f'φ: arrow_from_functor C D F b' a ‹Adj.ε a ⋅⇩_{D}f' ⋅⇩_{D}φ› using a φ f' par Adj.ε.preserves_hom by (unfold_locales, fastforce) have "εa.is_coext b' (Adj.ε a ⋅⇩_{D}f ⋅⇩_{D}φ) g" unfolding εa.is_coext_def using g 1 by auto moreover have "εa.is_coext b' (Adj.ε a ⋅⇩_{D}f' ⋅⇩_{D}φ) g'" unfolding εa.is_coext_def using g' 1 by auto ultimately have "g = g'" using 1 fφ.arrow_from_functor_axioms f'φ.arrow_from_functor_axioms εa.the_coext_unique εa.the_coext_unique [of b' "Adj.ε a ⋅⇩_{D}f' ⋅⇩_{D}φ" g'] by auto hence "f ⋅⇩_{D}φ = f' ⋅⇩_{D}φ" using g g' is_faithful by argo thus "f = f'" using φ f f' par D.iso_is_retraction D.retraction_is_epi D.epiE [of φ f f'] by auto qed qed ultimately show "D.iso (Adj.ε a)" using D.iso_iff_mono_and_retraction by simp qed interpret ε: natural_isomorphism D D ‹F o G› D.map Adj.ε using 1 by (unfold_locales, auto) interpret εF: natural_isomorphism C D ‹F o G o F› F ‹Adj.ε o F› using ε.components_are_iso by (unfold_locales, simp) show "⋀a. C.ide a ⟹ C.iso (Adj.η a)" proof - fix a assume a: "C.ide a" have "D.inverse_arrows ((Adj.ε o F) a) ((F o Adj.η) a)" using a ε.components_are_iso Adj.ηε.triangle_F Adj.εFoFη.map_simp_ide D.section_retraction_of_iso by simp hence "D.iso ((F o Adj.η) a)" by blast thus "C.iso (Adj.η a)" using a reflects_iso [of "Adj.η a"] by fastforce qed qed (* * Uggh, I should have started with "right_adjoint_functor D C G" so that the * following would come out right. Instead, another step is needed to dualize. * TODO: Maybe re-work this later. *) interpret adjoint_equivalence D C F G Adj.η Adj.ε .. interpret ε': inverse_transformation D D ‹F o G› D.map Adj.ε .. interpret η': inverse_transformation C C C.map ‹G o F› Adj.η .. interpret E: adjoint_equivalence C D G F ε'.map η'.map using adjoint_equivalence_axioms dual_equivalence by blast show ?thesis using E.adjoint_equivalence_axioms by auto qed lemma is_right_adjoint_functor: shows "right_adjoint_functor C D F" proof - obtain G η ε where E: "adjoint_equivalence C D G F η ε" using extends_to_adjoint_equivalence by auto interpret E: adjoint_equivalence C D G F η ε using E by simp interpret Adj: meta_adjunction C D G F E.φ E.ψ using E.induces_meta_adjunction by simp show ?thesis using Adj.has_right_adjoint_functor by simp qed lemma is_equivalence_functor: shows "equivalence_functor C D F" proof obtain G η ε where E: "adjoint_equivalence C D G F η ε" using extends_to_adjoint_equivalence by auto interpret E: adjoint_equivalence C D G F η ε using E by simp have "equivalence_of_categories C D G F η ε" .. thus "∃G η ε. equivalence_of_categories C D G F η ε" by blast qed sublocale equivalence_functor C D F using is_equivalence_functor by blast end context equivalence_of_categories begin text ‹ The following development shows that an equivalence of categories can be refined to an adjoint equivalence by replacing just the counit. › abbreviation ε' where "ε' a ≡ ε a ⋅⇩_{C}F (D.inv (η (G a))) ⋅⇩_{C}C.inv (ε (F (G a)))" interpretation ε': transformation_by_components C C ‹F ∘ G› C.map ε' proof show "⋀a. C.ide a ⟹ «ε' a : (F ∘ G) a →⇩_{C}C.map a»" using η.components_are_iso ε.components_are_iso by simp fix f assume f: "C.arr f" show "ε' (C.cod f) ⋅⇩_{C}(F ∘ G) f = C.map f ⋅⇩_{C}ε' (C.dom f)" proof - have "ε' (C.cod f) ⋅⇩_{C}(F ∘ G) f = ε (C.cod f) ⋅⇩_{C}F (D.inv (η (G (C.cod f)))) ⋅⇩_{C}C.inv (ε (F (G (C.cod f)))) ⋅⇩_{C}F (G f)" using f C.comp_assoc by simp also have "... = ε (C.cod f) ⋅⇩_{C}(F (D.inv (η (G (C.cod f)))) ⋅⇩_{C}F (G (F (G f)))) ⋅⇩_{C}C.inv (ε (F (G (C.dom f))))" using f ε.inv_naturality [of "F (G f)"] C.comp_assoc by simp also have "... = (ε (C.cod f) ⋅⇩_{C}F (G f)) ⋅⇩_{C}F (D.inv (η (G (C.dom f)))) ⋅⇩_{C}C.inv (ε (F (G (C.dom f))))" proof - have "F (D.inv (η (G (C.cod f)))) ⋅⇩_{C}F (G (F (G f))) = F (G f) ⋅⇩_{C}F (D.inv (η (G (C.dom f))))" proof - have "F (D.inv (η (G (C.cod f)))) ⋅⇩_{C}F (G (F (G f))) = F (D.inv (η (G (C.cod f))) ⋅⇩_{D}G (F (G f)))" using f by simp also have "... = F (G f ⋅⇩_{D}D.inv (η (G (C.dom f))))" using f η.inv_naturality [of "G f"] by simp also have "... = F (G f) ⋅⇩_{C}F (D.inv (η (G (C.dom f))))" using f by simp finally show ?thesis by blast qed thus ?thesis using C.comp_assoc by simp qed also have "... = C.map f ⋅⇩_{C}ε (C.dom f) ⋅⇩_{C}F (D.inv (η (G (C.dom f)))) ⋅⇩_{C}C.inv (ε (F (G (C.dom f))))" using f ε.naturality C.comp_assoc by simp finally show ?thesis by blast qed qed interpretation ε': natural_isomorphism C C ‹F ∘ G› C.map ε'.map proof show "⋀a. C.ide a ⟹ C.iso (ε'.map a)" unfolding ε'.map_def using η.components_are_iso ε.components_are_iso apply simp by (intro C.isos_compose) auto qed lemma Fη_inverse: assumes "D.ide b" shows "F (η (G (F b))) = F (G (F (η b)))" and "F (η b) ⋅⇩_{C}ε (F b) = ε (F (G (F b))) ⋅⇩_{C}F (η (G (F b)))" and "C.inverse_arrows (F (η b)) (ε' (F b))" and "F (η b) = C.inv (ε' (F b))" and "C.inv (F (η b)) = ε' (F b)" proof - let ?ε' = "λa. ε a ⋅⇩_{C}F (D.inv (η (G a))) ⋅⇩_{C}C.inv (ε (F (G a)))" show 1: "F (η (G (F b))) = F (G (F (η b)))" proof - have "F (η (G (F b))) ⋅⇩_{C}F (η b) = F (G (F (η b))) ⋅⇩_{C}F (η b)" proof - have "F (η (G (F b))) ⋅⇩_{C}F (η b) = F (η (G (F b)) ⋅⇩_{D}η b)" using assms by simp also have "... = F (G (F (η b)) ⋅⇩_{D}η b)" using assms η.naturality [of "η b"] by simp also have "... = F (G (F (η b))) ⋅⇩_{C}F (η b)" using assms by simp finally show ?thesis by blast qed thus ?thesis using assms η.components_are_iso C.iso_cancel_right by simp qed show "F (η b) ⋅⇩_{C}ε (F b) = ε (F (G (F b))) ⋅⇩_{C}F (η (G (F b)))" using assms 1 ε.naturality [of "F (η b)"] by simp show 2: "C.inverse_arrows (F (η b)) (?ε' (F b))" proof show 3: "C.ide (?ε' (F b) ⋅⇩_{C}F (η b))" proof - have "?ε' (F b) ⋅⇩_{C}F (η b) = ε (F b) ⋅⇩_{C}(F (D.inv (η (G (F b)))) ⋅⇩_{C}C.inv (ε (F (G (F b))))) ⋅⇩_{C}F (η b)" using C.comp_assoc by simp also have "... = ε (F b) ⋅⇩_{C}(F (D.inv (η (G (F b)))) ⋅⇩_{C}F (G (F (η b)))) ⋅⇩_{C}C.inv (ε (F b))" using assms ε.naturality [of "F (η b)"] ε.components_are_iso C.comp_assoc C.invert_opposite_sides_of_square [of "ε (F (G (F b)))" "F (G (F (η b)))" "F (η b)" "ε (F b)"] by simp also have "... = ε (F b) ⋅⇩_{C}C.inv (ε (F b))" proof - have "F (D.inv (η (G (F b)))) ⋅⇩_{C}F (G (F (η b))) = F (G (F b))" using assms 1 D.comp_inv_arr' η.components_are_iso by (metis D.ideD(1) D.ideD(2) F.preserves_comp F.preserves_ide G.preserves_ide η.preserves_dom D.map_simp) moreover have "F (G (F b)) ⋅⇩_{C}C.inv (ε (F b)) = C.inv (ε (F b))" using assms D.comp_cod_arr ε.components_are_iso C.inv_in_hom [of "ε (F b)"] by (metis C.comp_ide_arr C_arr_expansion(1) D.ide_char F.preserves_arr F.preserves_dom F.preserves_ide G.preserves_ide C.seqE) ultimately show ?thesis by simp qed also have "... = F b" using assms ε.components_are_iso C.comp_arr_inv' by simp finally have "(ε (F b) ⋅⇩_{C}F (D.inv (η (G (F b)))) ⋅⇩_{C}C.inv (ε (F (G (F b))))) ⋅⇩_{C}F (η b) = F b" by blast thus ?thesis using assms by simp qed show "C.ide (F (η b) ⋅⇩_{C}?ε' (F b))" proof - have "(F (η b) ⋅⇩_{C}?ε' (F b)) ⋅⇩_{C}F (η b) = F (G (F b)) ⋅⇩_{C}F (η b)" proof - have "(F (η b) ⋅⇩_{C}?ε' (F b)) ⋅⇩_{C}F (η b) = F (η b) ⋅⇩_{C}(ε (F b) ⋅⇩_{C}F (D.inv (η (G (F b)))) ⋅⇩_{C}C.inv (ε (F (G (F b))))) ⋅⇩_{C}F (η b)" using C.comp_assoc by simp also have "... = F (η b)" using assms 3 C.comp_arr_dom [of "F (η b)" "(ε (F b) ⋅⇩_{C}F (D.inv (η (G (F b)))) ⋅⇩_{C}C.inv (ε (F (G (F b))))) ⋅⇩_{C}F (η b)"] by auto also have "... = F (G (F b)) ⋅⇩_{C}F (η b)" using assms C.comp_cod_arr by simp finally show ?thesis by blast qed hence "F (η b) ⋅⇩_{C}?ε' (F b) = F (G (F b))" using assms C.iso_cancel_right by simp thus ?thesis using assms by simp qed qed show "C.inv (F (η b)) = ?ε' (F b)" using assms 2 C.inverse_unique by simp show "F (η b) = C.inv (?ε' (F b))" proof - have "C.inverse_arrows (?ε' (F b)) (F (η b))" using assms 2 by auto thus ?thesis using assms C.inverse_unique by simp qed qed interpretation FoGoF: composite_functor D C C F ‹F o G› .. interpretation GoFoG: composite_functor C D D G ‹G o F› .. interpretation natural_transformation D C F FoGoF.map ‹F ∘ η› proof - have "F ∘ D.map = F" using hcomp_ide_dom F.as_nat_trans.natural_transformation_axioms by blast moreover have "F o (G o F) = FoGoF.map" by auto ultimately show "natural_transformation D C F FoGoF.map (F ∘ η)" using η.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms horizontal_composite [of D D D.map "G o F" η C F F F] by simp qed interpretation natural_transformation C D G GoFoG.map ‹η ∘ G› using η.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms horizontal_composite [of C D G G G ] by fastforce interpretation natural_transformation D C FoGoF.map F ‹ε'.map ∘ F› using ε'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms horizontal_composite [of D C F F F] by fastforce interpretation natural_transformation C D GoFoG.map G ‹G ∘ ε'.map› proof - have "G o C.map = G" using hcomp_ide_dom G.as_nat_trans.natural_transformation_axioms by blast moreover have "G o (F o G) = GoFoG.map" by auto ultimately show "natural_transformation C D GoFoG.map G (G ∘ ε'.map)" using G.as_nat_trans.natural_transformation_axioms ε'.natural_transformation_axioms horizontal_composite [of C C "F o G" C.map ε'.map D G G G] by simp qed interpretation ε'F_Fη: vertical_composite D C F FoGoF.map F ‹F ∘ η› ‹ε'.map ∘ F› .. interpretation Gε'_ηG: vertical_composite C D G GoFoG.map G ‹η o G› ‹G o ε'.map› .. interpretation ηε': unit_counit_adjunction C D F G η ε'.map proof show 1: "ε'F_Fη.map = F" proof fix g show "ε'F_Fη.map g = F g" proof (cases "D.arr g") show "¬ D.arr g ⟹ ε'F_Fη.map g = F g" using ε'F_Fη.is_extensional F.is_extensional by simp assume g: "D.arr g" have "ε'F_Fη.map g = ε' (F (D.cod g)) ⋅⇩_{C}F (η g)" using g ε'F_Fη.map_def by simp also have "... = ε' (F (D.cod g)) ⋅⇩_{C}F (η (D.cod g) ⋅⇩_{D}g)" using g η.is_natural_2 by simp also have "... = (ε' (F (D.cod g)) ⋅⇩_{C}F (η (D.cod g))) ⋅⇩_{C}F g" using g C.comp_assoc by simp also have "... = F (D.cod g) ⋅⇩_{C}F g" using g Fη_inverse(3) [of "D.cod g"] by fastforce also have "... = F g" using g C.comp_cod_arr by simp finally show "ε'F_Fη.map g = F g" by blast qed qed show "Gε'_ηG.map = G" proof fix f show "Gε'_ηG.map f = G f" proof (cases "C.arr f") show "¬ C.arr f ⟹ Gε'_ηG.map f = G f" using Gε'_ηG.is_extensional G.is_extensional by simp assume f: "C.arr f" have "F (Gε'_ηG.map f) = F (G (ε' (C.cod f)) ⋅⇩_{D}η (G f))" using f Gε'_ηG.map_def D.comp_assoc by simp also have "... = F (G (ε' (C.cod f)) ⋅⇩_{D}η (G (C.cod f)) ⋅⇩_{D}G f)" using f η.is_natural_2 [of "G f"] by simp also have "... = F (G (ε' (C.cod f))) ⋅⇩_{C}F (η (G (C.cod f))) ⋅⇩_{C}F (G f)" using f by simp also have "... = (F (G (ε' (C.cod f))) ⋅⇩_{C}C.inv (ε' (F (G (C.cod f))))) ⋅⇩_{C}F (G f)" using f Fη_inverse(4) C.comp_assoc by simp also have "... = (C.inv (ε' (C.cod f)) ⋅⇩_{C}ε' (C.cod f)) ⋅⇩_{C}F (G f)" using f ε'.inv_naturality [of "ε' (C.cod f)"] by simp also have "... = F (G (C.cod f)) ⋅⇩_{C}F (G f)" using f C.comp_inv_arr' [of "ε' (C.cod f)"] ε'.components_are_iso by simp also have "... = F (G f)" using f C.comp_cod_arr by simp finally have "F (Gε'_ηG.map f) = F (G f)" by blast moreover have "D.par (Gε'_ηG.map f) (G f)" using f by simp ultimately show "Gε'_ηG.map f = G f" using f F_is_faithful by (simp add: faithful_functor_axioms_def faithful_functor_def) qed qed qed interpretation ηε': adjoint_equivalence C D F G η ε'.map .. lemma refines_to_adjoint_equivalence: shows "adjoint_equivalence C D F G η ε'.map" .. end end