| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Category3/ Datei vom 31.4.2026 mit Größe 172 kB |
|
Quellcode-Bibliothek Adjunction.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Adjunction Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) chapter Adjunction theory Adjunction imports Yoneda begin text‹ This theory defines the notions of adjoint functor and adjunction in various ways and establishes their equivalence. The notions ``left adjoint functor'' and ``right adjoint functor'' are defined in terms of universal arrows. ``Meta-adjunctions'' are defined in terms of natural bijections between hom-sets where the notion of naturality is axiomatized directly. ``Hom-adjunctions'' formalize the notion of adjunction in terms of natural isomorphisms of hom-functors. ``Unit-counit adjunctions'' define adjunctions in terms of functors equipped with unit and counit natural transformations that satisfy the usual ``triangle identities.'' The ‹adjunction› locale is defined as the grand unification of all the definitions, and includes formulas that connect the data from each of them. It is shown that each of the definitions induces an interpretation of the ‹adjunction› locale, so that all the definitions are essentially equivalent. Finally, it is shown that right adjoint functors are unique up to natural isomorphism. The reference cite‹"Wikipedia-Adjoint-Functors"› was useful in constructing this section "Left Adjoint Functor" text‹ ``@{term e} is an arrow from @{term "F x"} to @{term y}.'' › locale arrow_from_functor = C: category C + D: category D + F: "functor" D C F for D :: "'d comp" (infixr ‹⋅D› 55) and C :: "'c comp" (infixr ‹⋅C› 55) and F :: "'d ==> 'c" and x :: 'd and y :: 'c and e :: 'c + assumes arrow: "D.ide x ∧ C.in_hom e (F x) y" begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) text‹ ``@{term g} is a @{term[source=true] D}-coextension of @{term f} along @{term e} definition is_coext :: "'d ==> 'c ==> 'd ==> bool" where "is_coext x' f g ≡ «g : x' →D x¬ ∧ f = e ⋅C F g" end text‹ ``@{term e} is a terminal arrow from @{term "F x"} to @{term y}.'' › locale terminal_arrow_from_functor = arrow_from_functor D C F x y e for D :: "'d comp" (infixr ‹⋅D› 55) and C :: "'c comp" (infixr ‹⋅C› 55) and F :: "'d ==> 'c" and x :: 'd and y :: 'c and e :: 'c + assumes is_terminal: "arrow_from_functor D C F x' y f ==> (∃!g. is_coext x' f g)" begin definition the_coext :: "'d ==> 'c ==> 'd" where "the_coext x' f = (THE g. is_coext x' f g)" lemma the_coext_prop: assumes "arrow_from_functor D C F x' y f" shows "«the_coext x' f : x' →D x¬" and "f = e ⋅C F (the_coext x' f)" by (metis assms is_coext_def is_terminal the_coext_def the_equality)+ lemma the_coext_unique: assumes "arrow_from_functor D C F x' y f" and "is_coext x' f g" shows "g = the_coext x' f" using assms is_terminal the_coext_def the_equality by metis end text‹ A left adjoint functor is a functor ‹F: D → C› that enjoys the following universal coextension property: for each object @{term y} of @{term C} there exists an object @{term x} of @{term D} and an arrow ‹e ∈ C.hom (F x) y› such that for any arrow ‹f ∈ C.hom (F x') y› there exists a unique ‹g ∈ D.hom x' x› such that @{term "f = C e (F g)"}. › locale left_adjoint_functor = C: category C + D: category D + "functor" D C F for D :: "'d comp" (infixr ‹⋅D› 55) and C :: "'c comp" (infixr ‹⋅C› 55) and F :: "'d ==> 'c" + assumes ex_terminal_arrow: "C.ide y ==> (∃x e. terminal_arrow_from_functor D C F x begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) end section "Right Adjoint Functor" text‹ ``@{term e} is an arrow from @{term x} to @{term "G y"}.'' › locale arrow_to_functor = C: category C + D: category D + G: "functor" C D G for C :: "'c comp" (infixr ‹⋅C› 55) and D :: "'d comp" (infixr ‹⋅D› 55) and G :: "'c ==> 'd" and x :: 'd and y :: 'c and e :: 'd + assumes arrow: "C.ide y ∧ D.in_hom e x (G y)" begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) text‹ ``@{term f} is a @{term[source=true] C}-extension of @{term g} along @{term e}.' definition is_ext :: "'c ==> 'd ==> 'c ==> bool" where "is_ext y' g f ≡ «f : y →C y'¬ ∧ g = G f ⋅D e" end text‹ ``@{term e} is an initial arrow from @{term x} to @{term "G y"}.'' › locale initial_arrow_to_functor = arrow_to_functor C D G x y e for C :: "'c comp" (infixr ‹⋅C› 55) and D :: "'d comp" (infixr ‹⋅D› 55) and G :: "'c ==> 'd" and x :: 'd and y :: 'c and e :: 'd + assumes is_initial: "arrow_to_functor C D G x y' g ==> (∃!f. is_ext y' g f)" begin definition the_ext :: "'c ==> 'd ==> 'c" where "the_ext y' g = (THE f. is_ext y' g f)" lemma the_ext_prop: assumes "arrow_to_functor C D G x y' g" shows "«the_ext y' g : y →C y'¬" and "g = G (the_ext y' g) ⋅D e" by (metis assms is_initial is_ext_def the_equality the_ext_def)+ lemma the_ext_unique: assumes "arrow_to_functor C D G x y' g" and "is_ext y' g f" shows "f = the_ext y' g" using assms is_initial the_ext_def the_equality by metis end text‹ A right adjoint functor is a functor ‹G: C → D› that enjoys the following universal extension property: for each object @{term x} of @{term D} there exists an object @{term y} of @{ter and an arrow ‹e ∈ D.hom x (G y)› such that for any arrow ‹g ∈ D.hom x (G y')› there exists a unique ‹f ∈ C.hom y y'› such that @{term "h = D e (G f)"}. locale right_adjoint_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 ex_initial_arrow: "D.ide x ==> (∃y e. initial_arrow_to_functor C D G x y e begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) end section "Various Definitions of Adjunction" subsection "Meta-Adjunction" text‹ A ``meta-adjunction'' consists of a functor ‹F: D → C›, a functor ‹G: C → D›, and for each object @{term x} of @{term C} and @{term y} of @{term D} a bijection between ‹C.hom (F y) x› to ‹D.hom y (G x)› which is natural in @{term x} and @{term y}. The naturality is easy to express at the meta-level without havi to resort to the formal baggage of ``set category,'' ``hom-functor,'' and ``natural isomorphism,'' hence the name. locale meta_adjunction = C: category C + D: category D + F: "functor" D C F + G: "functor" C D G for C :: "'c comp" (infixr ‹⋅C› 55) and D :: "'d comp" (infixr ‹⋅D› 55) and F :: "'d ==> 'c" and G :: "'c ==> 'd" and φ :: "'d ==> 'c ==> 'd" and ψ :: "'c ==> 'd ==> 'c" + assumes φ_in_hom: "[ D.ide y; C.in_hom f (F y) x ] ==> D.in_hom (φ y f) y (G x)" and ψ_in_hom: "[ C.ide x; D.in_hom g y (G x) ] ==> C.in_hom (ψ x g) (F y) x" and ψ_φ: "[ D.ide y; C.in_hom f (F y) x ] ==> ψ x (φ y f) = f" and φ_ψ: "[ C.ide x; D.in_hom g y (G x) ] ==> φ y (ψ x g) = g" and φ_naturality: "[ C.in_hom f x x'; D.in_hom g y' y; C.in_hom h (F y) x ] ==> φ y' (f ⋅C h ⋅C F g) = G f ⋅D φ y h ⋅D g" begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) text‹ The naturality of @{term ψ} is a consequence of the naturality of @{term φ} and the other assumptions. › lemma ψ_naturality: assumes f: "«f : x →C x'¬" and g: "«g : y' →D y¬" and h: "«h : y →D G x¬" shows "f ⋅C ψ x h ⋅C F g = ψ x' (G f ⋅D h ⋅D g)" using f g h φ_naturality ψ_in_hom C.ide_dom D.ide_dom D.in_homE φ_ψ ψ_φ by (metis C.comp_in_homI' F.preserves_hom C.in_homE D.in_homE) lemma respects_natural_isomorphism: assumes "natural_isomorphism D C F' F τ" and "natural_isomorphism C D G G' μ" shows "meta_adjunction C D F' G' (λy f. μ (C.cod f) ⋅D φ y (f ⋅C inverse_transformation.map D C F τ y)) (λx g. ψ x ((inverse_transformation.map C D G' μ x) ⋅D g) ⋅C τ (D.dom g))" proof - interpret τ: natural_isomorphism D C F' F τ using assms(1) by simp interpret τ': inverse_transformation D C F' F τ .. interpret μ: natural_isomorphism C D G G' μ using assms(2) by simp interpret μ': inverse_transformation C D G G' μ .. let ?φ' = "λy f. μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y)" let ?ψ' = "λx g. ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g)" show "meta_adjunction C D F' G' ?φ' ?ψ'" proof show "∧y f x. [D.ide y; «f : F' y →C x¬] ==> «μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y) : y →D G' x¬" proof - fix x y f assume y: "D.ide y" and f: "«f : F' y →C x¬" show "«μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y) : y →D G' x¬" proof (intro D.comp_in_homI) show "«μ (C.cod f) : G x →D G' x¬" using f by fastforce show "«φ y (f ⋅C τ'.map y) : y →D G x¬" using f y φ_in_hom by auto qed qed show "∧x g y. [C.ide x; «g : y →D G' x¬] ==> «ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g) : F' y →C x¬" proof - fix x y g assume x: "C.ide x" and g: "«g : y →D G' x¬" show "«ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g) : F' y →C x¬" proof (intro C.comp_in_homI) show "«τ (D.dom g) : F' y →C F y¬" using g by fastforce show "«ψ x (μ'.map x ⋅D g) : F y →C x¬" using x g ψ_in_hom by auto qed qed show "∧y f x. [D.ide y; «f : F' y →C x¬] ==> ψ x (μ'.map x ⋅D μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y)) ⋅C τ (D.dom (μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y))) = f" proof - fix x y f assume y: "D.ide y" and f: "«f : F' y →C x¬" have 1: "«φ y (f ⋅C τ'.map y) : y →D G x¬" using f y φ_in_hom by auto show "ψ x (μ'.map x ⋅D μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y)) ⋅C τ (D.dom (μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y))) = f" proof - have "ψ x (μ'.map x ⋅D μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y)) ⋅C τ (D.dom (μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y))) = ψ x ((μ'.map x ⋅D μ (C.cod f)) ⋅D φ y (f ⋅C τ'.map y)) ⋅C τ (D.dom (μ (C.cod f) ⋅D φ y (f ⋅C τ'.map y)))" using D.comp_assoc by simp also have "... = ψ x (φ y (f ⋅C τ'.map y)) ⋅C τ y" by (metis "1" C.arr_cod C.dom_cod C.ide_cod C.in_homE D.comp_ide_arr D.dom_comp D.ide_compE D.in_homE D.inverse_arrowsE μ'.inverts_components μ.preserves_dom μ.preserves_reflects_arr category.seqI f meta_adjunction_axioms meta_adjunction_def) also have "... = f" using f y ψ_φ C.comp_assoc τ'.inverts_components [of y] C.comp_arr_dom by fastforce finally show ?thesis by blast qed qed show "∧x g y. [C.ide x; «g : y →D G' x¬] ==> μ (C.cod (ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g))) ⋅D φ y ((ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g)) ⋅C τ'.map y) = g" proof - fix x y g assume x: "C.ide x" and g: "«g : y →D G' x¬" have 1: "«ψ x (μ'.map x ⋅D g) : F y →C x¬" using x g ψ_in_hom by auto show "μ (C.cod (ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g))) ⋅D φ y ((ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g)) ⋅C τ'.map y) = g" proof - have "μ (C.cod (ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g))) ⋅D φ y ((ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g)) ⋅C τ'.map y) = μ (C.cod (ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g))) ⋅D φ y (ψ x (μ'.map x ⋅D g) ⋅C τ (D.dom g) ⋅C τ'.map y)" using C.comp_assoc by simp also have "... = μ x ⋅D φ y (ψ x (μ'.map x ⋅D g))" using 1 C.comp_arr_dom C.comp_arr_inv' g by fastforce also have "... = (μ x ⋅D μ'.map x) ⋅D g" using x g φ_ψ D.comp_assoc by auto also have "... = g" using x g μ'.inverts_components [of x] D.comp_cod_arr by fastforce finally show ?thesis by blast qed qed show "∧f x x' g y' y h. [«f : x →C x'¬; «g : y' →D y¬; «h : F' y →C x¬] ==> μ (C.cod (f ⋅C h ⋅C F' g)) ⋅D φ y' ((f ⋅C h ⋅C F' g) ⋅C τ'.map y') = G' f ⋅D (μ (C.cod h) ⋅D φ y (h ⋅C τ'.map y)) ⋅D g" proof - fix x y x' y' f g h assume f: "«f : x →C x'¬" and g: "«g : y' →D y¬" and h: "«h : F' y →C x¬" show "μ (C.cod (f ⋅C h ⋅C F' g)) ⋅D φ y' ((f ⋅C h ⋅C F' g) ⋅C τ'.map y') = G' f ⋅D (μ (C.cod h) ⋅D φ y (h ⋅C τ'.map y)) ⋅D g" proof - have "μ (C.cod (f ⋅C h ⋅C F' g)) ⋅D φ y' ((f ⋅C h ⋅C F' g) ⋅C τ'.map y') = μ x' ⋅D φ y' ((f ⋅C h ⋅C F' g) ⋅C τ'.map y')" using f g h by fastforce also have "... = μ x' ⋅D φ y' (f ⋅C (h ⋅C τ'.map y) ⋅C F g)" using g τ'.naturality C.comp_assoc by auto also have "... = (μ x' ⋅D G f) ⋅D φ y (h ⋅C τ'.map y) ⋅D g" using f g h φ_naturality [of f x x' g y' y "h ⋅C τ'.map y"] D.comp_assoc by fastforce also have "... = (G' f ⋅D μ x) ⋅D φ y (h ⋅C τ'.map y) ⋅D g" using f μ.naturality by auto also have "... = G' f ⋅D (μ (C.cod h) ⋅D φ y (h ⋅C τ'.map y)) ⋅D g" using h D.comp_assoc by auto finally show ?thesis by blast qed qed qed qed end subsection "Hom-Adjunction" text‹ The bijection between hom-sets that defines an adjunction can be represented formally as a natural isomorphism of hom-functors. However, stating the definit this way is more complex than was the case for ‹meta_adjunction›. One reason is that we need to have a ``set category'' that is suitable as a target category for the hom-functors, and since the arrows of the categories @{term C} and @{term D} will in general have distinct types, we need a set categ that simultaneously embeds both. Another reason is that we simply have to forma construct the various categories and functors required to express the definition This is a good place to point out that I have often included more sublocales in a locale than are strictly required. The main reason for this is the fact th the locale system in Isabelle only gives one name to each entity introduced by a locale: the name that it has in the first locale in which it occurs. This means that entities that make their first appearance deeply nested in sublo will have to be referred to by long qualified names that can be difficult to understand, or even to discover. To counteract this, I have typically introduce sublocales before the superlocales that contain them to ensure that the entities in the sublocales can be referred to by short meaningful (and predictable) names In my opinion, though, it would be better if the locale system would make entiti that occur in multiple locales accessible by \emph{all} possible qualified names so that the most perspicuous name could be used in any particular context. locale hom_adjunction = C: category C + D: category D + S: set_category S setp + Cop: dual_category C + Dop: dual_category D + CopxC: product_category Cop.comp C + DopxD: product_category Dop.comp D + DopxC: product_category Dop.comp C + F: "functor" D C F + G: "functor" C D G + HomC: hom_functor C S setp φC + HomD: hom_functor D S setp φD + Fop: dual_functor Dop.comp Cop.comp F + FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map + DopxG: product_functor Dop.comp C Dop.comp D Dop.map G + Hom_FopxC: composite_functor DopxC.comp CopxC.comp S FopxC.map HomC.map + Hom_DopxG: composite_functor DopxC.comp DopxD.comp S DopxG.map HomD.map + Hom_FopxC: set_valued_functor DopxC.comp S setp Hom_FopxC.map + Hom_DopxG: set_valued_functor DopxC.comp S setp Hom_DopxG.map + Φ: set_valued_transformation DopxC.comp S setp Hom_FopxC.map Hom_DopxG.map Φ + Ψ: set_valued_transformation DopxC.comp S setp Hom_DopxG.map Hom_FopxC.map Ψ + ΦΨ: inverse_transformations DopxC.comp S Hom_FopxC.map Hom_DopxG.map Φ Ψ for C :: "'c comp" (infixr ‹⋅C› 55) and D :: "'d comp" (infixr ‹⋅D› 55) and S :: "'s comp" (infixr ‹⋅S› 55) and setp :: "'s set ==> bool" and φC :: "'c * 'c ==> 'c ==> 's" and φD :: "'d * 'd ==> 'd ==> 's" and F :: "'d ==> 'c" and G :: "'c ==> 'd" and Φ :: "'d * 'c ==> 's" and Ψ :: "'d * 'c ==> 's" begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) abbreviation ψC :: "'c * 'c ==> 's ==> 'c" where "ψC ≡ HomC.ψ" abbreviation ψD :: "'d * 'd ==> 's ==> 'd" where "ψD ≡ HomD.ψ" end subsection "Unit/Counit Adjunction" text‹ Expressed in unit/counit terms, an adjunction consists of functors ‹F: D → C› and ‹G: C → D›, equipped with natural transformations ‹η: 1 → GF› and ‹ε: FG → 1› satisfying certain ``triangle identities''. › locale unit_counit_adjunction = C: category C + D: category D + F: "functor" D C F + G: "functor" C D G + GF: composite_functor D C D F G + FG: composite_functor C D C G F + FGF: composite_functor D C C F ‹F o G› + GFG: composite_functor C D D G ‹G o F› + η: natural_transformation D D D.map ‹G o F› η + ε: natural_transformation C C ‹F o G› C.map ε + Fη: natural_transformation D C F ‹F o G o F› ‹F o η› + ηG: natural_transformation C D G ‹G o F o G› ‹η o G› + εF: natural_transformation D C ‹F o G o F› F ‹ε o F› + Gε: natural_transformation C D ‹G o F o G› G ‹G o ε› + εFoFη: vertical_composite D C F ‹F o G o F› F ‹F o η› ‹ε o F› + GεoηG: vertical_composite C D G ‹G o F o G› G ‹η o G› ‹G o ε› 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" + assumes triangle_F: "εFoFη.map = F" and triangle_G: "GεoηG.map = G" begin notation C.in_hom (‹«_ : _ →C _¬›) notation D.in_hom (‹«_ : _ →D _¬›) end lemma unit_determines_counit: assumes "unit_counit_adjunction C D F G η ε" and "unit_counit_adjunction C D F G η ε'" shows "ε = ε'" proof - (* IDEA: \<epsilon>' = \<epsilon>'FG o (FG\<epsilon> o F\<eta>G) = \<epsilon>'\<epsilon> o F\<eta>G = \<epsil interpret Adj: unit_counit_adjunction C D F G η ε using assms(1) by auto interpret Adj': unit_counit_adjunction C D F G η ε' using assms(2) by auto interpret FGFG: composite_functor C D C G ‹F o G o F› .. interpret FGε: natural_transformation C C ‹(F o G) o (F o G)› ‹F o G› ‹(F o G) o ε› using Adj.ε.natural_transformation_axioms Adj.FG.as_nat_trans.natural_transformatio horizontal_composite by fastforce interpret FηG: natural_transformation C C ‹F o G› ‹F o G o F o G› ‹F o η o G› using Adj.η.natural_transformation_axioms Adj.Fη.natural_transformation_axioms Adj.G.as_nat_trans.natural_transformation_axioms horizontal_composite by blast interpret ε'ε: natural_transformation C C ‹F o G o F o G› Adj.C.map ‹ε' o ε› proof - have "natural_transformation C C ((F o G) o (F o G)) Adj.C.map (ε' o ε)" using Adj.ε.natural_transformation_axioms Adj'.ε.natural_transformation_axioms horizontal_composite Adj.C.is_functor comp_functor_identity by (metis (no_types, lifting)) thus "natural_transformation C C (F o G o F o G) Adj.C.map (ε' o ε)" using o_assoc by metis qed interpret ε'εoFηG: vertical_composite C C ‹F o G› ‹F o G o F o G› Adj.C.map ‹F o η o G› ‹ε' o ε› .. have "ε' = vertical_composite.map C C (F o Adj.GεoηG.map) ε'" using vcomp_ide_dom [of C C "F o G" Adj.C.map ε'] Adj.triangle_G by (simp add: Adj'.ε.natural_transformation_axioms) also have "... = vertical_composite.map C C (vertical_composite.map C C (F o η o G) (F o G o ε)) ε'" using whisker_left Adj.F.functor_axioms Adj.Gε.natural_transformation_axioms Adj.ηG.natural_transformation_axioms o_assoc by (metis (no_types, lifting)) also have "... = vertical_composite.map C C (vertical_composite.map C C (F o η o G) (ε' o F o G)) ε" proof - have "vertical_composite.map C C (vertical_composite.map C C (F o η o G) (F o G o ε)) ε' = vertical_composite.map C C (F o η o G) (vertical_composite.map C C (F o G o ε) ε')" using vcomp_assoc by (metis (no_types, lifting) Adj'.ε.natural_transformation_axioms FGε.natural_transformation_axioms FηG.natural_transformation_axioms o_assoc) also have "... = vertical_composite.map C C (F o η o G) (vertical_composite.map C C (ε' o F o G) ε)" using Adj'.ε.natural_transformation_axioms Adj.ε.natural_transformation_axioms interchange_spc [of C C "F o G" Adj.C.map ε C "F o G" Adj.C.map ε'] by (metis hcomp_ide_cod hcomp_ide_dom o_assoc) also have "... = vertical_composite.map C C (vertical_composite.map C C (F o η o G) (ε' o F o G)) ε" using vcomp_assoc by (metis Adj'.εF.natural_transformation_axioms Adj.G.as_nat_trans.natural_transformation_axioms Adj.ε.natural_transformation_axioms FηG.natural_transformation_axioms horizontal_composite) finally show ?thesis by simp qed also have "... = vertical_composite.map C C (vertical_composite.map D C (F o η) (ε' o F) o G) ε" using whisker_right Adj'.εF.natural_transformation_axioms Adj.Fη.natural_transformation_axioms Adj.G.functor_axioms by metis also have "... = ε" using Adj'.triangle_F vcomp_ide_cod Adj.ε.natural_transformation_axioms by simp finally show ?thesis by simp qed lemma counit_determines_unit: assumes "unit_counit_adjunction C D F G η ε" and "unit_counit_adjunction C D F G η' ε" shows "η = η'" proof - interpret Adj: unit_counit_adjunction C D F G η ε using assms(1) by auto interpret Adj': unit_counit_adjunction C D F G η' ε using assms(2) by auto interpret GFGF: composite_functor D C D F ‹G o F o G› .. interpret GFη: natural_transformation D D ‹G o F› ‹(G o F) o (G o F)› ‹(G o F) o η› using Adj.η.natural_transformation_axioms Adj.GF.functor_axioms Adj.GF.as_nat_trans.natural_transformation_axioms comp_functor_identity horizontal_composite by (metis (no_types, lifting)) interpret η'GF: natural_transformation D D ‹G o F› ‹(G o F) o (G o F)› ‹η' o (G o F)› using Adj'.η.natural_transformation_axioms Adj.GF.functor_axioms Adj.GF.as_nat_trans.natural_transformation_axioms comp_identity_functor horizontal_composite by (metis (no_types, lifting)) interpret GεF: natural_transformation D D ‹G o F o G o F› ‹G o F› ‹G o ε o F› using Adj.ε.natural_transformation_axioms Adj.F.as_nat_trans.natural_transformation Adj.Gε.natural_transformation_axioms horizontal_composite by blast interpret η'η: natural_transformation D D Adj.D.map ‹G o F o G o F› ‹η' o η› proof - have "natural_transformation D D Adj.D.map ((G o F) o (G o F)) (η' o η)" using Adj'.η.natural_transformation_axioms Adj.D.identity_functor_axioms Adj.η.natural_transformation_axioms horizontal_composite identity_functor.is_functo by fastforce thus "natural_transformation D D Adj.D.map (G o F o G o F) (η' o η)" using o_assoc by metis qed interpret GεFoη'η: vertical_composite D D Adj.D.map ‹G o F o G o F› ‹G o F› ‹η' o η› ‹G o ε o F› .. have "η' = vertical_composite.map D D η' (G o Adj.εFoFη.map)" using vcomp_ide_cod [of D D Adj.D.map "G o F" η'] Adj.triangle_F by (simp add: Adj'.η.natural_transformation_axioms) also have "... = vertical_composite.map D D η' (vertical_composite.map D D (G o (F o η)) (G o (ε o F)))" using whisker_left Adj.Fη.natural_transformation_axioms Adj.G.functor_axioms Adj.εF.natural_transformation_axioms by fastforce also have "... = vertical_composite.map D D (vertical_composite.map D D η' (G o (F o η))) (G o ε o F)" using vcomp_assoc Adj'.η.natural_transformation_axioms GFη.natural_transformation_axioms GεF.natural_transformation_axioms o_assoc by (metis (no_types, lifting)) also have "... = vertical_composite.map D D (vertical_composite.map D D η (η' o G o F)) (G o ε o F)" using interchange_spc [of D D Adj.D.map "G o F" η D Adj.D.map "G o F" η'] Adj.η.natural_transformation_axioms Adj'.η.natural_transformation_axioms by (metis hcomp_ide_cod hcomp_ide_dom o_assoc) also have "... = vertical_composite.map D D η (vertical_composite.map D D (η' o G o F) (G o ε o F))" using vcomp_assoc by (metis (no_types, lifting) Adj.η.natural_transformation_axioms GεF.natural_transformation_axioms η'GF.natural_transformation_axioms o_assoc) also have "... = vertical_composite.map D D η (vertical_composite.map C D (η' o G) (G o ε) o F)" using whisker_right Adj'.ηG.natural_transformation_axioms Adj.F.functor_axioms Adj.Gε.natural_transformation_axioms by fastforce also have "... = η" using Adj'.triangle_G vcomp_ide_dom Adj.GF.functor_axioms Adj.η.natural_transformation_axioms by simp finally show ?thesis by simp qed subsection "Adjunction" text‹ The grand unification of everything to do with an adjunction. › locale adjunction = C: category C + D: category D + S: set_category S setp + Cop: dual_category C + Dop: dual_category D + CopxC: product_category Cop.comp C + DopxD: product_category Dop.comp D + DopxC: product_category Dop.comp C + idDop: identity_functor Dop.comp + HomC: hom_functor C S setp φC + HomD: hom_functor D S setp φD + F: left_adjoint_functor D C F + G: right_adjoint_functor C D G + GF: composite_functor D C D F G + FG: composite_functor C D C G F + FGF: composite_functor D C C F FG.map + GFG: composite_functor C D D G GF.map + Fop: dual_functor Dop.comp Cop.comp F + FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map + DopxG: product_functor Dop.comp C Dop.comp D Dop.map G + Hom_FopxC: composite_functor DopxC.comp CopxC.comp S FopxC.map HomC.map + Hom_DopxG: composite_functor DopxC.comp DopxD.comp S DopxG.map HomD.map + Hom_FopxC: set_valued_functor DopxC.comp S setp Hom_FopxC.map + Hom_DopxG: set_valued_functor DopxC.comp S setp Hom_DopxG.map + η: natural_transformation D D D.map GF.map η + ε: natural_transformation C C FG.map C.map ε + Fη: natural_transformation D C F ‹F o G o F› ‹F o η› + ηG: natural_transformation C D G ‹G o F o G› ‹η o G› + εF: natural_transformation D C ‹F o G o F› F ‹ε o F› + Gε: natural_transformation C D ‹G o F o G› G ‹G o ε› + εFoFη: vertical_composite D C F FGF.map F ‹F o η› ‹ε o F› + GεoηG: vertical_composite C D G GFG.map G ‹η o G› ‹G o ε› + φψ: meta_adjunction C D F G φ ψ + ηε: unit_counit_adjunction C D F G η ε + ΦΨ: hom_adjunction C D S setp φC φD F G Φ Ψ for C :: "'c comp" (infixr ‹⋅C› 55) and D :: "'d comp" (infixr ‹⋅D› 55) and S :: "'s comp" (infixr ‹⋅S› 55) and setp :: "'s set ==> bool" and φC :: "'c * 'c ==> 'c ==> 's" and φD :: "'d * 'd ==> 'd ==> 's" and F :: "'d ==> 'c" and G :: "'c ==> 'd" and φ :: "'d ==> 'c ==> 'd" and ψ :: "'c ==> 'd ==> 'c" and η :: "'d ==> 'd" and ε :: "'c ==> 'c" and Φ :: "'d * 'c ==> 's" and Ψ :: "'d * 'c ==> 's" + assumes φ_in_terms_of_η: "[ D.ide y; «f : F y →C x¬ ] ==> φ y f = G f ⋅D η y" and ψ_in_terms_of_ε: "[ C.ide x; «g : y →D G x¬ ] ==> ψ x g = ε x ⋅C F g" and η_in_terms_of_φ: "D.ide y ==> η y = φ y (F y)" and ε_in_terms_of_ψ: "C.ide x ==> ε x = ψ x (G x)" and φ_in_terms_of_Φ: "[ D.ide y; «f : F y →C x¬ ] ==> φ y f = (ΦΨ.ψD (y, G x) o S.Fun (Φ (y, x)) o φC (F y, x)) f" and ψ_in_terms_of_Ψ: "[ C.ide x; «g : y →D G x¬ ] ==> ψ x g = (ΦΨ.ψC (F y, x) o S.Fun (Ψ (y, x)) o φD (y, G x)) g" and Φ_in_terms_of_φ: "[ C.ide x; D.ide y ] ==> Φ (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (φD (y, G x) o φ y o ΦΨ.ψC (F y, x))" and Ψ_in_terms_of_ψ: "[ C.ide x; D.ide y ] ==> Ψ (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (φC (F y, x) o ψ x o ΦΨ.ψD (y, G x))" section "Meta-Adjunctions Induce Unit/Counit Adjunctions" context meta_adjunction begin interpretation GF: composite_functor D C D F G .. interpretation FG: composite_functor C D C G F .. interpretation FGF: composite_functor D C C F FG.map .. interpretation GFG: composite_functor C D D G GF.map .. definition ηo :: "'d ==> 'd" where "ηo y = φ y (F y)" lemma ηo_in_hom: assumes "D.ide y" shows "«ηo y : y →D G (F y)¬" using assms D.ide_in_hom ηo_def φ_in_hom by force lemma φ_in_terms_of_ηo: assumes "D.ide y" and "«f : F y →C x¬" shows "φ y f = G f ⋅D ηo y" proof (unfold ηo_def) have 1: "«F y : F y →C F y¬" using assms(1) D.ide_in_hom by blast hence "φ y (F y) = φ y (F y) ⋅D y" by (metis assms(1) D.in_homE φ_in_hom D.comp_arr_dom) thus "φ y f = G f ⋅D φ y (F y)" using assms 1 D.ide_in_hom by (metis C.comp_arr_dom C.in_homE φ_naturality) qed lemma φ_F_char: assumes "«g : y' →D y¬" shows "φ y' (F g) = ηo y ⋅D g" using assms ηo_def φ_in_hom [of y "F y" "F y"] D.comp_cod_arr [of "D (φ y (F y)) g" "G (F y)"] φ_naturality [of "F y" "F y" "F y" g y' y "F y"] by (metis C.ide_in_hom D.arr_cod_iff_arr D.arr_dom D.cod_cod D.cod_dom D.comp_ide_arr D.comp_ide_self D.ide_cod D.in_homE F.as_nat_trans.naturality2 F.functor_axioms F.preserves_section_retraction φ_in_hom functor.preserves_hom) interpretation η: transformation_by_components D D D.map GF.map ηo proof show "∧a. D.ide a ==> «ηo a : D.map a →D GF.map a¬" using ηo_def φ_in_hom D.ide_in_hom by force fix f assume f: "D.arr f" show "ηo (D.cod f) ⋅D D.map f = GF.map f ⋅D ηo (D.dom f)" using f φ_F_char [of "D.map f" "D.dom f" "D.cod f"] φ_in_terms_of_ηo [of "D.dom f" "F f" "F (D.cod f)"] by force qed lemma η_map_simp: assumes "D.ide y" shows "η.map y = φ y (F y)" using assms η.map_simp_ide ηo_def by simp definition εo :: "'c ==> 'c" where "εo x = ψ x (G x)" lemma εo_in_hom: assumes "C.ide x" shows "«εo x : F (G x) →C x¬" using assms C.ide_in_hom εo_def ψ_in_hom by force lemma ψ_in_terms_of_εo: assumes "C.ide x" and "«g : y →D G x¬" shows "ψ x g = εo x ⋅C F g" proof - have "εo x ⋅C F g = x ⋅C ψ x (G x) ⋅C F g" using assms εo_def ψ_in_hom [of x "G x" "G x"] C.comp_cod_arr [of "ψ x (G x) ⋅C F g" x] by fastforce also have "... = ψ x (G x ⋅D G x ⋅D g)" using assms ψ_naturality [of x x x g y "G x" "G x"] by force also have "... = ψ x g" using assms D.comp_cod_arr by fastforce finally show ?thesis by simp qed lemma ψ_G_char: assumes "«f: x →C x'¬" shows "ψ x' (G f) = f ⋅C εo x" proof (unfold εo_def) have 0: "C.ide x ∧ C.ide x'" using assms by auto thus "ψ x' (G f) = f ⋅C ψ x (G x)" using 0 assms ψ_naturality ψ_in_hom [of x "G x" "G x"] G.preserves_hom εo_def ψ_in_terms_of_εo G.as_nat_trans.naturality1 C.ide_in_hom by (metis C.arrI C.in_homE) qed interpretation ε: transformation_by_components C C FG.map C.map εo apply unfold_locales using εo_in_hom apply simp using ψ_G_char ψ_in_terms_of_εo by (metis C.arr_iff_in_hom C.ide_cod C.map_simp G.preserves_hom comp_apply) lemma ε_map_simp: assumes "C.ide x" shows "ε.map x = ψ x (G x)" using assms εo_def by simp interpretation FD: composite_functor D D C D.map F .. interpretation CF: composite_functor D C C F C.map .. interpretation GC: composite_functor C C D C.map G .. interpretation DG: composite_functor C D D G D.map .. interpretation Fη: natural_transformation D C F ‹F o G o F› ‹F o η.map› by (metis (no_types, lifting) F.as_nat_trans.natural_transformation_axioms F.functor_axioms η.natural_transformation_axioms comp_functor_identity horizontal_composite o_assoc) interpretation εF: natural_transformation D C ‹F o G o F› F ‹ε.map o F› using ε.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce interpretation ηG: natural_transformation C D G ‹G o F o G› ‹η.map o G› using η.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce interpretation Gε: natural_transformation C D ‹G o F o G› G ‹G o ε.map› by (metis (no_types, lifting) G.as_nat_trans.natural_transformation_axioms G.functor_axioms ε.natural_transformation_axioms comp_functor_identity horizontal_composite o_assoc) interpretation εFoFη: vertical_composite D C F ‹F o G o F› F ‹F o η.map› ‹ε.map o F› .. interpretation GεoηG: vertical_composite C D G ‹G o F o G› G ‹η.map o G› ‹G o ε.map› .. lemma unit_counit_F: assumes "D.ide y" shows "F y = εo (F y) ⋅C F (ηo y)" using assms ψ_in_terms_of_εo ηo_def ψ_φ ηo_in_hom F.preserves_ide C.ide_in_hom by metis lemma unit_counit_G: assumes "C.ide x" shows "G x = G (εo x) ⋅D ηo (G x)" using assms φ_in_terms_of_ηo εo_def φ_ψ εo_in_hom G.preserves_ide D.ide_in_hom by metis lemma induces_unit_counit_adjunction': shows "unit_counit_adjunction C D F G η.map ε.map" proof show "εFoFη.map = F" using εFoFη.is_natural_transformation εFoFη.map_simp_ide unit_counit_F F.as_nat_trans.natural_transformation_axioms by (intro natural_transformation_eqI) auto show "GεoηG.map = G" using GεoηG.is_natural_transformation GεoηG.map_simp_ide unit_counit_G G.as_nat_trans.natural_transformation_axioms by (intro natural_transformation_eqI) auto qed definition η :: "'d ==> 'd" where "η ≡ η.map" definition ε :: "'c ==> 'c" where "ε ≡ ε.map" theorem induces_unit_counit_adjunction: shows "unit_counit_adjunction C D F G η ε" unfolding η_def ε_def using induces_unit_counit_adjunction' by simp lemma η_naturalitytransformation: shows "natural_transformation D D D.map GF.map η" unfolding η_def .. lemma ε_naturalitytransformation: shows "natural_transformation C C FG.map C.map ε" unfolding ε_def .. text‹ From the defined @{term η} and @{term ε} we can recover the original @{term φ} and lemma φ_in_terms_of_η: assumes "D.ide y" and "«f : F y →C x¬" shows "φ y f = G f ⋅D η y" using assms η_def by (simp add: φ_in_terms_of_ηo) lemma ψ_in_terms_of_ε: assumes "C.ide x" and "«g : y →D G x¬" shows "ψ x g = ε x ⋅C F g" using assms ε_def by (simp add: ψ_in_terms_of_εo) end section "Meta-Adjunctions Induce Left and Right Adjoint Functors" context meta_adjunction begin interpretation unit_counit_adjunction C D F G η ε using induces_unit_counit_adjunction η_def ε_def by auto lemma has_terminal_arrows_from_functor: assumes x: "C.ide x" shows "terminal_arrow_from_functor D C F (G x) x (ε x)" and "∧y' f. arrow_from_functor D C F y' x f ==> terminal_arrow_from_functor.the_coext D C F (G x) (ε x) y' f = φ y' f" proof - interpret εx: arrow_from_functor D C F ‹G x› x ‹ε x› using x ε.preserves_hom G.preserves_ide by unfold_locales auto have 1: "∧y' f. arrow_from_functor D C F y' x f ==> εx.is_coext y' f (φ y' f) ∧ (∀g'. εx.is_coext y' f g' ⟶ g' = φ y' f)" using x by (metis (full_types) εx.is_coext_def φ_ψ ψ_in_terms_of_ε arrow_from_functor.arrow φ_in_hom ψ_φ) interpret εx: terminal_arrow_from_functor D C F ‹G x› x ‹ε x› using 1 by unfold_locales blast show "terminal_arrow_from_functor D C F (G x) x (ε x)" .. show "∧y' f. arrow_from_functor D C F y' x f ==> εx.the_coext y' f = φ y' f" using 1 εx.the_coext_def by auto qed lemma has_left_adjoint_functor: shows "left_adjoint_functor D C F" apply unfold_locales using has_terminal_arrows_from_functor by auto lemma has_initial_arrows_to_functor: assumes y: "D.ide y" shows "initial_arrow_to_functor C D G y (F y) (η y)" and "∧x' g. arrow_to_functor C D G y x' g ==> initial_arrow_to_functor.the_ext C D G (F y) (η y) x' g = ψ x' g" proof - interpret ηy: arrow_to_functor C D G y ‹F y› ‹η y› using y by unfold_locales auto have 1: "∧x' g. arrow_to_functor C D G y x' g ==> ηy.is_ext x' g (ψ x' g) ∧ (∀f'. ηy.is_ext x' g f' ⟶ f' = ψ x' g)" using y by (metis (full_types) ηy.is_ext_def ψ_φ φ_in_terms_of_η arrow_to_functor.arrow ψ_in_hom φ_ψ) interpret ηy: initial_arrow_to_functor C D G y ‹F y› ‹η y› apply unfold_locales using 1 by blast show "initial_arrow_to_functor C D G y (F y) (η y)" .. show "∧x' g. arrow_to_functor C D G y x' g ==> ηy.the_ext x' g = ψ x' g" using 1 ηy.the_ext_def by auto qed lemma has_right_adjoint_functor: shows "right_adjoint_functor C D G" apply unfold_locales using has_initial_arrows_to_functor by auto end section "Unit/Counit Adjunctions Induce Meta-Adjunctions" context unit_counit_adjunction begin definition φ :: "'d ==> 'c ==> 'd" where "φ y h = G h ⋅D η y" definition ψ :: "'c ==> 'd ==> 'c" where "ψ x h = ε x ⋅C F h" interpretation meta_adjunction C D F G φ ψ proof fix x :: 'c and y :: 'd and f :: 'c assume y: "D.ide y" and f: "«f : F y →C x¬" show 0: "«φ y f : y →D G x¬" using f y G.preserves_hom η.preserves_hom φ_def D.ide_in_hom by auto show "ψ x (φ y f) = f" proof - have "ψ x (φ y f) = (ε x ⋅C F (G f)) ⋅C F (η y)" using y f φ_def ψ_def C.comp_assoc by auto also have "... = (f ⋅C ε (F y)) ⋅C F (η y)" using y f ε.naturality by auto also have "... = f" using y f εFoFη.map_simp_2 triangle_F C.comp_arr_dom D.ide_in_hom C.comp_assoc by fastforce finally show ?thesis by auto qed next fix x :: 'c and y :: 'd and g :: 'd assume x: "C.ide x" and g: "«g : y →D G x¬" show "«ψ x g : F y →C x¬" using g x ψ_def by fastforce show "φ y (ψ x g) = g" proof - have "φ y (ψ x g) = (G (ε x) ⋅D η (G x)) ⋅D g" using g x φ_def ψ_def η.naturality [of g] D.comp_assoc by auto also have "... = g" using x g triangle_G D.comp_ide_arr GεoηG.map_simp_ide by auto finally show ?thesis by auto qed next fix f :: 'c and g :: 'd and h :: 'c and x :: 'c and x' :: 'c and y :: 'd and y' :: 'd assume f: "«f : x →C x'¬" and g: "«g : y' →D y¬" and h: "«h : F y →C x¬" show "φ y' (f ⋅C h ⋅C F g) = G f ⋅D φ y h ⋅D g" using φ_def f g h η.naturality D.comp_assoc by fastforce qed theorem induces_meta_adjunction: shows "meta_adjunction C D F G φ ψ" .. text‹ From the defined @{term φ} and @{term ψ} we can recover the original @{term η} and lemma η_in_terms_of_φ: assumes "D.ide y" shows "η y = φ y (F y)" using assms φ_def D.comp_cod_arr by auto lemma ε_in_terms_of_ψ: assumes "C.ide x" shows "ε x = ψ x (G x)" using assms ψ_def C.comp_arr_dom by auto end section "Left and Right Adjoint Functors Induce Meta-Adjunctions" text‹ A left adjoint functor induces a meta-adjunction, modulo the choice of a right adjoint and counit. › context left_adjoint_functor begin definition Go :: "'c ==> 'd" where "Go a = (SOME b. ∃e. terminal_arrow_from_functor D C F b a e)" definition εo :: "'c ==> 'c" where "εo a = (SOME e. terminal_arrow_from_functor D C F (Go a) a e)" lemma Go_εo_terminal: assumes "∃b e. terminal_arrow_from_functor D C F b a e" shows "terminal_arrow_from_functor D C F (Go a) a (εo a)" using assms Go_def εo_def someI_ex [of "λb. ∃e. terminal_arrow_from_functor D C F b a e"] someI_ex [of "λe. terminal_arrow_from_functor D C F (Go a) a e"] by simp text‹ The right adjoint @{term G} to @{term F} takes each arrow @{term f} of @{term[source=true] C} to the unique @{term[source=true] D}-coextension of @{term "C f (εo (C.dom f))"} along @{term "εo (C.cod f)"}. › definition G :: "'c ==> 'd" where "G f = (if C.arr f then terminal_arrow_from_functor.the_coext D C F (Go (C.cod f)) (εo (C.cod f)) (Go (C.dom f)) (f ⋅C εo (C.dom f)) else D.null)" lemma G_ide: assumes "C.ide x" shows "G x = Go x" proof - interpret terminal_arrow_from_functor D C F ‹Go x› x ‹εo x› using assms ex_terminal_arrow Go_εo_terminal by blast have 1: "arrow_from_functor D C F (Go x) x (εo x)" .. have "is_coext (Go x) (εo x) (Go x)" using arrow is_coext_def C.in_homE C.comp_arr_dom by auto hence "Go x = the_coext (Go x) (εo x)" using 1 the_coext_unique by blast moreover have "εo x = C x (εo (C.dom x))" using assms arrow C.comp_ide_arr C.seqI' C.ide_in_hom C.in_homE by metis ultimately show ?thesis using assms G_def C.cod_dom C.ide_in_hom C.in_homE by metis qed lemma G_is_functor: shows "functor C D G" proof fix f :: 'c assume "¬C.arr f" thus "G f = D.null" using G_def by auto next fix f :: 'c assume f: "C.arr f" let ?x = "C.dom f" let ?x' = "C.cod f" interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ‹?x› ‹εo ?x› using f ex_terminal_arrow Go_εo_terminal by simp interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ‹?x'› ‹εo ?x'› using f ex_terminal_arrow Go_εo_terminal by simp have 1: "arrow_from_functor D C F (Go ?x) ?x' (C f (εo ?x))" using f xε.arrow by (unfold_locales, auto) have "G f = x'ε.the_coext (Go ?x) (C f (εo ?x))" using f G_def by simp hence Gf: "«G f : Go ?x →D Go ?x'¬ ∧ f ⋅C εo ?x = εo ?x' ⋅C F (G f)" using 1 x'ε.the_coext_prop by simp show "D.arr (G f)" using Gf by auto show "D.dom (G f) = G ?x" using f Gf G_ide by auto show "D.cod (G f) = G ?x'" using f Gf G_ide by auto next fix f f' :: 'c assume ff': "C.arr (C f' f)" have f: "C.arr f" using ff' by auto let ?x = "C.dom f" let ?x' = "C.cod f" let ?x'' = "C.cod f'" interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ‹?x› ‹εo ?x› using f ex_terminal_arrow Go_εo_terminal by simp interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ‹?x'› ‹εo ?x'› using f ex_terminal_arrow Go_εo_terminal by simp interpret x''ε: terminal_arrow_from_functor D C F ‹Go ?x''› ‹?x''› ‹εo ?x''› using ff' ex_terminal_arrow Go_εo_terminal by auto have 1: "arrow_from_functor D C F (Go ?x) ?x' (f ⋅C εo ?x)" using f xε.arrow by (unfold_locales, auto) have 2: "arrow_from_functor D C F (Go ?x') ?x'' (f' ⋅C εo ?x')" using ff' x'ε.arrow by (unfold_locales, auto) have "G f = x'ε.the_coext (Go ?x) (C f (εo ?x))" using f G_def by simp hence Gf: "D.in_hom (G f) (Go ?x) (Go ?x') ∧ f ⋅C εo ?x = εo ?x' ⋅C F (G f)" using 1 x'ε.the_coext_prop by simp have "G f' = x''ε.the_coext (Go ?x') (f' ⋅C εo ?x')" using ff' G_def by auto hence Gf': "«G f' : Go (C.cod f) →D Go (C.cod f')¬ ∧ f' ⋅C εo ?x' = εo ?x'' ⋅C F (G f') using 2 x''ε.the_coext_prop by simp show "G (f' ⋅C f) = G f' ⋅D G f" proof - have "x''ε.is_coext (Go ?x) ((f' ⋅C f) ⋅C εo ?x) (G f' ⋅D G f)" proof - have 3: "«G f' ⋅D G f : Go (C.dom f) →D Go (C.cod f')¬" using 1 2 Gf Gf' by auto moreover have "(f' ⋅C f) ⋅C εo ?x = εo ?x'' ⋅C F (G f' ⋅D G f)" by (metis 3 C.comp_assoc D.in_homE Gf Gf' preserves_comp) ultimately show ?thesis using x''ε.is_coext_def by auto qed moreover have "arrow_from_functor D C F (Go ?x) ?x'' ((f' ⋅C f) ⋅C εo ?x)" using ff' xε.arrow by unfold_locales blast ultimately show ?thesis using ff' G_def x''ε.the_coext_unique C.seqE C.cod_comp C.dom_comp by auto qed qed interpretation G: "functor" C D G using G_is_functor by auto lemma G_simp: assumes "C.arr f" shows "G f = terminal_arrow_from_functor.the_coext D C F (Go (C.cod f)) (εo (C.cod (Go (C.dom f)) (f ⋅C εo (C.dom f))" using assms G_def by simp interpretation idC: identity_functor C .. interpretation GF: composite_functor C D C G F .. interpretation ε: transformation_by_components C C GF.map C.map εo proof fix x :: 'c assume x: "C.ide x" show "«εo x : GF.map x →C C.map x¬" proof - interpret terminal_arrow_from_functor D C F ‹Go x› x ‹εo x› using x Go_εo_terminal ex_terminal_arrow by simp show ?thesis using x G_ide arrow by auto qed next fix f :: 'c assume f: "C.arr f" show "εo (C.cod f) ⋅C GF.map f = C.map f ⋅C εo (C.dom f)" proof - let ?x = "C.dom f" let ?x' = "C.cod f" interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ?x ‹εo ?x› using f Go_εo_terminal ex_terminal_arrow by simp interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ?x' ‹εo ?x'› using f Go_εo_terminal ex_terminal_arrow by simp have 1: "arrow_from_functor D C F (Go ?x) ?x' (C f (εo ?x))" using f xε.arrow by unfold_locales auto have "G f = x'ε.the_coext (Go ?x) (f ⋅C εo ?x)" using f G_simp by blast hence "x'ε.is_coext (Go ?x) (f ⋅C εo ?x) (G f)" using 1 x'ε.the_coext_prop x'ε.is_coext_def by auto thus ?thesis using f x'ε.is_coext_def by simp qed qed definition ψ where "ψ x h = C (ε.map x) (F h)" lemma ψ_in_hom: assumes "C.ide x" and "«g : y →D G x¬" shows "«ψ x g : F y →C x¬" unfolding ψ_def using assms ε.maps_ide_in_hom by auto lemma ψ_natural: assumes f: "«f : x →C x'¬" and g: "«g : y' →D y¬" and h: "«h : y →D G x¬" shows "f ⋅C ψ x h ⋅C F g = ψ x' ((G f ⋅D h) ⋅D g)" proof - have "f ⋅C ψ x h ⋅C F g = f ⋅C (ε.map x ⋅C F h) ⋅C F g" unfolding ψ_def by auto also have "... = (f ⋅C ε.map x) ⋅C F h ⋅C F g" using C.comp_assoc by fastforce also have "... = (f ⋅C ε.map x) ⋅C F (h ⋅D g)" using g h by fastforce also have "... = (ε.map x' ⋅C F (G f)) ⋅C F (h ⋅D g)" using f ε.naturality by auto also have "... = ε.map x' ⋅C F ((G f ⋅D h) ⋅D g)" using f g h C.comp_assoc by fastforce also have "... = ψ x' ((G f ⋅D h) ⋅D g)" unfolding ψ_def by auto finally show ?thesis by auto qed lemma ψ_inverts_coext: assumes x: "C.ide x" and g: "«g : y →D G x¬" shows "arrow_from_functor.is_coext D C F (G x) (ε.map x) y (ψ x g) g" proof - interpret xε: arrow_from_functor D C F ‹G x› x ‹ε.map x› using x ε.maps_ide_in_hom by unfold_locales auto show "xε.is_coext y (ψ x g) g" using x g ψ_def xε.is_coext_def G_ide by blast qed lemma ψ_invertible: assumes y: "D.ide y" and f: "«f : F y →C x¬" shows "∃!g. «g : y →D G x¬ ∧ ψ x g = f" proof have x: "C.ide x" using f by auto interpret xε: terminal_arrow_from_functor D C F ‹Go x› x ‹εo x› using x ex_terminal_arrow Go_εo_terminal by auto have 1: "arrow_from_functor D C F y x f" using y f by (unfold_locales, auto) let ?g = "xε.the_coext y f" have "ψ x ?g = f" using 1 x y ψ_def xε.the_coext_prop G_ide ψ_inverts_coext xε.is_coext_def by simp thus "«?g : y →D G x¬ ∧ ψ x ?g = f" using 1 x xε.the_coext_prop G_ide by simp show "∧g'. «g' : y →D G x¬ ∧ ψ x g' = f ==> g' = ?g" using 1 x y ψ_inverts_coext G_ide xε.the_coext_unique by force qed definition φ where "φ y f = (THE g. «g : y →D G (C.cod f)¬ ∧ ψ (C.cod f) g = f)" lemma φ_in_hom: assumes "D.ide y" and "«f : F y →C x¬" shows "«φ y f : y →D G x¬" using assms ψ_invertible φ_def theI' [of "λg. «g : y →D G x¬ ∧ ψ x g = f"] by auto lemma φ_ψ: assumes "C.ide x" and "«g : y →D G x¬" shows "φ y (ψ x g) = g" proof - have "φ y (ψ x g) = (THE g'. «g' : y →D G x¬ ∧ ψ x g' = ψ x g)" proof - have "C.cod (ψ x g) = x" using assms ψ_in_hom by auto thus ?thesis using φ_def by auto qed moreover have "∃!g'. «g' : y →D G x¬ ∧ ψ x g' = ψ x g" using assms ψ_in_hom ψ_invertible D.ide_dom by blast ultimately show "φ y (ψ x g) = g" using assms(2) by auto qed lemma ψ_φ: assumes "D.ide y" and "«f : F y →C x¬" shows "ψ x (φ y f) = f" using assms ψ) by auto \>: assumes : "', b, 'c) psi" howsφ\<^sub>C F g) = (G f ⋅ \phih ⋅D g" proof - have "C.ide and D.ide y ∧ y using_in_hom by auto thus ?thesis usingp_in_homI<_natural [of f x x' g y' y "φ y h"] φ_ψ ψ_φ by auto qed theorem induces_meta_adjunction shows "meta_adjunction C DF G\phi<>" φ_in_hom_ψ_<>φ_naturalD.comp_assoc by unfold_locales auto end textjava.lang.NullPointerException: Cannot invoke "String.equals(Object)" becaus nctoruloeice left › P ↝ Q" context right_adjoint_functor egin finition : "'Rightarrow'c" where "y=ME>u. initial_arrow_to_functor C D G y x u)" on\o :: "'d 🚫bn α* Ψ<bn * P<close τ.P<Longrightarrow ≺ P'' ∼ \o y = (SOME u. initial_arrow_to_functor C D G y (Fo y) u)" lemma Fo_η assumesx u. initial_arrow_to_functor C D G y x u" shows "initial_arrow_to_functor C D G y (Fo y) (ηo y)" usingssms Fo_def\etao_def someI_exx. ∃ someI_exofu. initial_arrow_to_functor C D y (FohainCons and, P, Q) ∈ text< The left adjoint @{term F} to @{termrow "Ψ ⊳ Q ==>^Qby simp @{term "\etao (D.cod g)) g"} along @{term "ηo (D.dom g)"}. \<> definition F :: "'d ==> 'c" where "F g = (if D.arr g then ow_to_functor. (<oDPsi, P[xvec:ecvecin Rel" (Fo (D.cod g)) (ηD g) else C.null)" lemma F_ide: assumes shows proof - interprettial_arrow_to_functorfunctorFo y› ηo y› using assms ex_initial_arrow Fo_η haverow_to_functoro ).. have "is_ext (Fo y) (ηo y) (Fo y)" unfolding is_ext_def using arrow D.comp_ide_arr [ofo y"] by force hence "Fo y = the_ext (Fo y) (ηo usingopen xvec = length Tvec›distinct xvec› usinguest moreover have "\ by auto using assms arrow D.comp_arr_ide D.comp__dom by auto ultimately show ?thesis using assms F_def D.dom_cod D.nhm .d_n_hom y etis qed lemma F_is_functor: shows "functor" f fix assume "¬(Ψ, P, Q) ∈ Rel have "(Ψ ⊗i> Rel" by(rule rExt) thusullng fix g :: 'd assume g:Dr g" case Tau let ?y' = "D.cod g" interpret y\<etaetaFo ?y› ‹ assumesl" interpret y'\<eta>:tial_arrow_to_functor\<open> ?y'\<close> \<open>\<eta>o ?y'\<close> using g ex_initial_arrow Fo_\<eta>o_initial by simp e1 rrow_to_functor D G y ()( (\<eta>oy )java.lang.StringIndexOutOfBoundsException: Index using g y'\<eta>.arrow by unfold_locales auto have "Fy<eta>the_ext (Fo ?y') (D (\etao ?y') g)" using g F_def by simp hence Fg: "\<guillemotleft\<^sub>Co\uillemotright \<and> \<eta>o ?y' \<cdot>\<^sub>D g = G (F g) \<cdot>\< case(cTau'java.lang.StringIndexOutOfBoundsException: Index 15 out of bounds for show "C.arr showdom(F =gFg show "C.cod (F g) yngFg o next fix g :: 'd fix g' : 'd assume g' "Darr" have g: "D.arr g" using let ?y = "D.dom g" let ?y' = "D.cod g" let ?y' java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 using g ex_initial_arrow Fo_\<eta>o_initial by simp interpret'\: initial_arrow_to_functor C D G ?y\<openoy\close\<open>\<eta>o ?y'\<close> using g ex_initial_arrow Fo_\<eta>o_initial by simp interpret y''\<eta>: initial_arrow_to_functor C Gy<pen> ?y''\<close> \<open>\<eta>o ?y''\<close> java.lang.StringIndexOutOfBoundsException: Index 66 out of bounds for length 60 have 1: "arrow_to_functor C D G using g y'\<eta>.arrow by unfold_locales auto "F g = y\<eta>.the_ext (Fo ?y') (\<eta>o ?y' \<cdot>\<^sub>D g)" using g F_def by simp hence Fg: "\<guillemotleft>F o y\<ghtarrow<^subFoy\guillemotright \<and> \<eta>o y' \<cdot>\<^sub>D g using 1 y\<eta>.the_ext_prop by simp have 2: "arrow_to_functor C D G ?y' (Fo ?y'') (\<eta>o''>sub g')" using g' y''\<ta>arrow by unfold_locales auto =>the_ext (o ?y''\\<^sub>D g')" using g' F_def y java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds f hence Fg': "\<guillemotleft>F g' : Fo ?y' \<rightarrow>\<^subC Fo ?y''\guillemotright> \<and> \<eta>o qed showg\cdot\<sub>D g) = F g' \<cdot>\<^sub>C F g" proof - applydrule_tacbisimEmE)java.lang.StringIndexOutOfBoundsException: Index 32 out o have:guillemotleft>F g' \<cdot>\<^b : <>^> Fo ?y''\<guillemotright>" using 1 2 Fg Fg'by moreover have "\o ?y'' \<cdot>\^subg\><^sub>D g = G (Fcdot<^sub>C F g) \<cdot>\<^sub>D \<etay Fg Fg' g g' 3 y''\<eta>.arrow by (metis C.arrI D.comp_assoc preserves_comp) ultimately show ?thesis sing eta.is_ext_def by auto moreover have "arrow_to_functor C D G ?y (Fo ?y'') (\<eta>o ?y'' \<cdot>\<^sub>D g' \<cdot>\<^sub>D g)" using g g' y''\<eta>.arrow by unfold_locales auto ultimately show ?thesis using g g' F_def y\<eta>.the_ext_unique D.dom_comp D.cod_comp by auto qed qed interpretation F: "functor" D C F using F_is_functor by auto lemmamp nitial_arrow_to_functortor.the_extexttG ( Ddom) (D.dom g \<Psi> P.(Psi, P, P) \<in> Rel" using assms F_def by simp erpretationtation FGomposite_functorD C G interpretation \<eta>: transformation_by_components D D D.map FG.map\<eta>o proof java.lang.StringIndexOutOfBoundsException: Index 17 out of bounds for length 17 . y show "<guillemotleftetao y : D.map y \rightarrow>\<^sub>D FG. y\<guillemotright>" proof - interpret initial_arrow_to_functornext ngo_<>initial initial_arrowal_arrow_rrowbysimp show ?thesis using y F_ide arrow byto qed next fix g :: 'd assume g: "D.arr g" show\>o (.codd g) \<ot>\<sub>D D.mapgFG.map g<\<^sub>D \<eta>o (D.dom g)" proof let ?y = ".dom let ?y' = "D.cod g" interpret: initial_arrow_to_functor C?y \<ny\<close> \<open<eta> ?y\<close> interpret y\<>: initial_arrow_to_functor C D G ?y' \openFo ?y'\<close> \<open>\<eta>o ?y'\<close> using g Fo_\<eta>ultimately show ? by tforce have "arrow_to_functor C D G ?y (Fo ?y') (\<eta>o java.lang.StringIndexOutOfBoundsException using g y'\<eta>.arrow by unfold_localesutojava.lang.StringIndexOutOfBoundsException: moreoverve g=<eta>the_ext_ext y')<eta> '\<><^sub>D g)" java.lang.StringIndexOutOfBoundsException: Index 100 out of bounds for length 33 ultimately have "y\<eta>.is_ext (Fo ?y') (\<eta>o ?y' \<cdot>\<^sub>D g) (F g)" using y\<eta>.the_ext_prop y\<eta>.is_ext_def by auto thus ?thesis using g y\<eta>.is_ext_def_efsimp qed qed definition \<phi> where "\<phi> y h = D (G h) (java.lang.StringIndexOutOfBoundsException: Index 0 out of bou lemma \<phi>_in_hom: assumes y: "D.ide y" and f: "\<guillemotleft>f : F \<^sub>C x\<guillemotright>" java.lang.StringIndexOutOfBoundsException: Index 87 out of bounds for length 85 unfolding \<phii>efusingng \<ta.maps_ide_in_hom by auto \>_natural: assumes<f : x \<rightarrow<subC x'\<guillemotright>" and g: "\<guillemotleft>g : y' \rightarrow\<b shows "\<phi> y' (f \<cdot>\<^sub>C h \<cdot>\<^open>\<Psi> \<otimes> \<Psi>' \<rhd> P[xvec::=Tvec] \<sim> Pclos proof - have "(G f \<casejava.lang.StringIndexOutOfBoundsException: Index 14 out of bounds f unfolding \<phi>_def by auto also have "... = ( <cdot>^> G h) \<cdot>\<ub <eta.pcdot\<^sub>D g" fastforce also have "... = G (f \<cdot>\<^ h \<anaturality also have "... = (<><^sub>C h) \<cdot>\<^sub> F \<\<^sub>D \<aapjava.lang.StringIndexOutOfBoundsExcep usingrce also have "... = G (f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) \<cdot>\<^sub>D \<eta>.map y'" case cTau also have ". y' (f \<cdotsubC h \<cdot>\<^sub>C F g)" unfolding \<phi>_ef yuto finally show qed lemma \<phi>_inverts_ext: assumes y: "D.ide y" and f: "\<guillemotleft>fwith open>\<Psi> \<rhd> (\<tau>.(P) oplus Q \<sim> P'\<clos java.lang.StringIndexOutOfBoundsException: Index 31 out of bounds for length 31 proof interpret y\<>ow_to_functor y<pen y\<close> \<open>\<eta>.map y\<close> using y \<eta>.maps_ide_in_hom by unfold_locales auto \<eta>.is_ext x (\<phi> y f) f" using f y \<phi>_def y\<eta>t_def_deby blast qed aphi>__invertible: assumes x: "C.ide x" and g: "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" shows "\<exists>!f. \<guillemotleft>f : F y \<rightarrow>\<^sub>C x\<guillemotright> \<and> \<phi> y f = g" proof y: "D.ide y" using g by auto interpret y\<eta>: initial_arrow_to_functor C D G y \<open>Fo y\<close> \<open>\<eta>o y\<close> _al_arrowetao_initial by auto have 1: "arrow_to_functor C D G y x g" using x g by (unfold_locales, auto) let ?f = "y\<eta>.the_ext x g" have "\<phi> y ?f = g" using \<phi>_def y\<eta>.the_ext_prop 1 F_ide x y \<phi>_inverts_ext y\<eta>.is_ext_def by fastfor moreover have "\<guillemotleft>?f : F y \<rightarrow>\<^sub>C x\<guillemotright>" using 1 y y\<eta>.the_ext_prop F_ide by simp ultimately show "\<guillemotleft>?f : F y \<rightarrow>\<^sub>C x\<guillemotright> \<and> \<phi> y ?f = g show "\<And>f'. \<guillemotleft>f' : F y \<rightarrow>\<^sub>C x\<guillemotright> \<and> \<phi> y f' = g \<Lo using 1 y \<phi>_inverts_ext y\<eta>.the_ext_unique F_ide by force qed definition \<psi> where "\<psi> x g = (THE f. \<guillemotleft>f : F (D.dom g) \<rightarrow>\<^sub>C x\<guillemotright> \<an lemma \<psi>_in_hom: assumes "C.ide x" and "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" shows "C.in_hom (\<psi> x g) (F y) x" using assms \<phi>_invertible \<psi>_def theI' [of "\<lambda>f. \<guillemotleft>f : F y \<rightarrow> by auto lemma \<psi>_\<phi>: assumes "D.ide y" and "\<guillemotleft>f : F y \<rightarrow>\<^sub>C x\<guillemotright>" shows "\<psi> x (\<phi> y f) = f" proof - have "D.dom (\<phi> y f) = y" using assms \<phi>_in_hom by blast hence "\<psi> x (\<phi> y f) = (THE f'. \<guillemotleft>f' : F y \<rightarrow>\<^sub>C x\<guillemotright> \< using \<psi>_def by auto moreover have "\<exists>!f'. \<guillemotleft>f' : F y \<rightarrow>\<^sub>C x\<guillemotright> \<and> using assms \<phi>_in_hom \<phi>_invertible C.ide_cod by blast ultimately show ?thesis using assms(2) by auto qed lemma \<phi>_\<psi>: assumes "C.ide x" and "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" shows "\<phi> y (\<psi> x g) = g" using assms \<phi>_invertible \<psi>_def theI' [of "\<lambda>f. \<guillemotleft>f : F y \<rightarrow> by auto theorem induces_meta_adjunction: shows "meta_adjunction C D F G \<phi> \<psi>" using \<phi>_in_hom \<psi>_in_hom \<phi>_\<psi> \<psi>_\<phi> \<phi>_natural D.comp_assoc by (unfold_locales, auto) end section "Meta-Adjunctions Induce Hom-Adjunctions" text\<open> To obtain a hom-adjunction from a meta-adjunction, we need to exhibit hom-functors from @{term C} and @{term D} to a common set category @{term S}, so it is necessary to apply an actual concrete construction of such a category. We use the replete set category generated by the disjoint sum @{typ "('c+'d)"} of the arrow types of @{term C} and @{term D}. \<close> context meta_adjunction begin interpretation S: replete_setcat \<open>TYPE('c+'d)\<close> . definition inC :: "'c \<Rightarrow> ('c+'d) setcat.arr" where "inC \<equiv> S.UP o Inl" definition inD :: "'d \<Rightarrow> ('c+'d) setcat.arr" where "inD \<equiv> S.UP o Inr" interpretation S: replete_setcat \<open>TYPE('c+'d)\<close> . interpretation Cop: dual_category C .. interpretation Dop: dual_category D .. interpretation CopxC: product_category Cop.comp C .. interpretation DopxD: product_category Dop.comp D .. interpretation DopxC: product_category Dop.comp C .. interpretation HomC: hom_functor C S.comp S.setp \<open>\<lambda>_. inC\<close> proof show "\<And>f. C.arr f \<Longrightarrow> inC f \<in> S.Univ" unfolding inC_def using S.UP_mapsto by auto thus "\<And>b a. \<lbrakk>C.ide b; C.ide a\<rbrakk> \<Longrightarrow> inC ` C.hom b a \<subseteq> S.Univ by blast show "\<And>b a. \<lbrakk>C.ide b; C.ide a\<rbrakk> \<Longrightarrow> inj_on inC (C.hom b a)" unfolding inC_def using S.inj_UP by (metis injD inj_Inl inj_compose inj_on_def) qed interpretation HomD: hom_functor D S.comp S.setp \<open>\<lambda>_. inD\<close> proof show "\<And>f. D.arr f \<Longrightarrow> inD f \<in> S.Univ" unfolding inD_def using S.UP_mapsto by auto thus "\<And>b a. \<lbrakk>D.ide b; D.ide a\<rbrakk> \<Longrightarrow> inD ` D.hom b a \<subseteq> S.Univ by blast show "\<And>b a. \<lbrakk>D.ide b; D.ide a\<rbrakk> \<Longrightarrow> inj_on inD (D.hom b a)" unfolding inD_def using S.inj_UP by (metis injD inj_Inr inj_compose inj_on_def) qed interpretation Fop: dual_functor D C F .. interpretation FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map .. interpretation DopxG: product_functor Dop.comp C Dop.comp D Dop.map G .. interpretation Hom_FopxC: composite_functor DopxC.comp CopxC.comp S.comp FopxC.map HomC.map .. interpretation Hom_DopxG: composite_functor DopxC.comp DopxD.comp S.comp DopxG.map HomD.map .. lemma inC_\<psi> [simp]: assumes "C.ide b" and "C.ide a" and "x \<in> inC ` C.hom b a" shows "inC (HomC.\<psi> (b, a) x) = x" using assms by auto lemma \<psi>_inC [simp]: assumes "C.arr f" shows "HomC.\<psi> (C.dom f, C.cod f) (inC f) = f" using assms HomC.\<psi>_\<phi> by blast lemma inD_\<psi> [simp]: assumes "D.ide b" and "D.ide a" and "x \<in> inD ` D.hom b a" shows "inD (HomD.\<psi> (b, a) x) = x" using assms by auto lemma \<psi>_inD [simp]: assumes "D.arr f" shows "HomD.\<psi> (D.dom f, D.cod f) (inD f) = f" using assms HomD.\<psi>_\<phi> by blast lemma Hom_FopxC_simp: assumes "DopxC.arr gf" shows "Hom_FopxC.map gf = S.mkArr (HomC.set (F (D.cod (fst gf)), C.dom (snd gf))) (HomC.set (F (D.dom (fst gf)), C.cod (snd gf))) (inC \<circ> (\<lambda>h. snd gf \<cdot>\<^sub>C h \<cdot>\<^sub>C F (fst gf)) \<circ> HomC.\<psi> (F (D.cod (fst gf)), C.dom (snd gf)))" using assms HomC.map_def by simp lemma Hom_DopxG_simp: assumes "DopxC.arr gf" shows "Hom_DopxG.map gf = S.mkArr (HomD.set (D.cod (fst gf), G (C.dom (snd gf)))) (HomD.set (D.dom (fst gf), G (C.cod (snd gf)))) (inD \<circ> (\<lambda>h. G (snd gf) \<cdot>\<^sub>D h \<cdot>\<^sub>D fst gf) \<circ> HomD.\<psi> (D.cod (fst gf), G (C.dom (snd gf))))" using assms HomD.map_def by simp definition \<Phi>o where "\<Phi>o yx = S.mkArr (HomC.set (F (fst yx), snd yx)) (HomD.set (fst yx, G (snd yx))) (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))" lemma \<Phi>o_in_hom: assumes yx: "DopxC.ide yx" shows "\<guillemotleft>\<Phi>o yx : Hom_FopxC.map yx \<rightarrow>\<^sub>S Hom_DopxG.map yx\<guil proof - have "Hom_FopxC.map yx = S.mkIde (HomC.set (F (fst yx), snd yx))" using yx HomC.map_ide by auto moreover have "Hom_DopxG.map yx = S.mkIde (HomD.set (fst yx, G (snd yx)))" using yx HomD.map_ide by auto moreover have "\<guillemotleft>S.mkArr (HomC.set (F (fst yx), snd yx)) (HomD.set (fst yx, G (snd yx))) (inD \<circ> \<phi> (fst yx) \<circ> HomC.\<psi> (F (fst yx), snd yx)) : S.mkIde (HomC.set (F (fst yx), snd yx)) \<rightarrow>\<^sub>S S.mkIde (HomD.set (fst yx, G (snd yx)))\<guillemotright>" proof (intro S.mkArr_in_hom) show "HomC.set (F (fst yx), snd yx) \<subseteq> S.Univ" using yx HomC.set_subset_Univ by simp show "HomD.set (fst yx, G (snd yx)) \<subseteq> S.Univ" using yx HomD.set_subset_Univ by simp show "inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx) \<in> HomC.set (F (fst yx), snd yx) \<rightarrow> HomD.set (fst yx, G (snd yx))" proof fix x assume x: "x \<in> HomC.set (F (fst yx), snd yx)" show "(inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)) x \<in> HomD.set (fst yx, G (snd yx))" using x yx HomC.\<psi>_mapsto [of "F (fst yx)" "snd yx"] \<phi>_in_hom [of "fst yx"] HomD.\<phi>_mapsto [of "fst yx" "G (snd yx)"] by auto qed qed ultimately show ?thesis using \<Phi>o_def by auto qed interpretation \<Phi>: transformation_by_components DopxC.comp S.comp Hom_FopxC.map Hom_DopxG.map \<Phi>o proof fix yx assume yx: "DopxC.ide yx" show "\<guillemotleft>\<Phi>o yx : Hom_FopxC.map yx \<rightarrow>\<^sub>S Hom_DopxG.map yx\<guill using yx \<Phi>o_in_hom by auto next fix gf assume gf: "DopxC.arr gf" show "S.comp (\<Phi>o (DopxC.cod gf)) (Hom_FopxC.map gf) = S.comp (Hom_DopxG.map gf) (\<Phi>o (DopxC.dom gf))" proof - let ?g = "fst gf" let ?f = "snd gf" let ?x = "C.dom ?f" let ?x' = "C.cod ?f" let ?y = "D.cod ?g" let ?y' = "D.dom ?g" let ?Fy = "F ?y" let ?Fy' = "F ?y'" let ?Fg = "F ?g" let ?Gx = "G ?x" let ?Gx' = "G ?x'" let ?Gf = "G ?f" have 1: "S.arr (Hom_FopxC.map gf) \<and> Hom_FopxC.map gf = S.mkArr (HomC.set (?Fy, ?x)) (HomC.set (?Fy', ?x')) (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))" using gf Hom_FopxC.preserves_arr Hom_FopxC_simp by blast have 2: "S.arr (\<Phi>o (DopxC.cod gf)) \<and> \<Phi>o (DopxC.cod gf) = S.mkArr (HomC.set (?Fy', ?x')) (HomD.set (?y', ?Gx')) (inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x'))" using gf \<Phi>o_in_hom [of "DopxC.cod gf"] \<Phi>o_def [of "DopxC.cod gf"] \<phi>_in_hom by auto have 3: "S.arr (\<Phi>o (DopxC.dom gf)) \<and> \<Phi>o (DopxC.dom gf) = S.mkArr (HomC.set (?Fy, ?x)) (HomD.set (?y, ?Gx)) (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x))" using gf \<Phi>o_in_hom [of "DopxC.dom gf"] \<Phi>o_def [of "DopxC.dom gf"] \<phi>_in_hom by auto have 4: "S.arr (Hom_DopxG.map gf) \<and> Hom_DopxG.map gf = S.mkArr (HomD.set (?y, ?Gx)) (HomD.set (?y', ?Gx')) (inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx))" using gf Hom_DopxG.preserves_arr Hom_DopxG_simp by blast have 5: "S.seq (\<Phi>o (DopxC.cod gf)) (Hom_FopxC.map gf) \<and> S.comp (\<Phi>o (DopxC.cod gf)) (Hom_FopxC.map gf) = S.mkArr (HomC.set (?Fy, ?x)) (HomD.set (?y', ?Gx')) ((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x)))" by (metis gf 1 2 DopxC.arr_iff_in_hom DopxC.ide_cod Hom_FopxC.preserves_hom S.comp_mkArr S.seqI' \<Phi>o_in_hom) have 6: "S.comp (Hom_DopxG.map gf) (\<Phi>o (DopxC.dom gf)) = S.mkArr (HomC.set (?Fy, ?x)) (HomD.set (?y', ?Gx')) ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x)))" by (metis 3 4 S.comp_mkArr) have 7: "restrict ((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))) (HomC.set (?Fy, ? = restrict ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x))) (HomC.set (?Fy, ?x))" proof (intro restrict_ext) show "\<And>h. h \<in> HomC.set (?Fy, ?x) \<Longrightarrow> ((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))) h = ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x))) h" proof - fix h assume h: "h \<in> HomC.set (?Fy, ?x)" have \<psi>h: "\<guillemotleft>HomC.\<psi> (?Fy, ?x) h : ?Fy \<rightarrow>\<^sub>C ?x\<guillemotrigh using gf h HomC.\<psi>_mapsto [of ?Fy ?x] CopxC.ide_char by auto show "((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))) h = ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x))) h" proof - have "((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))) h = inD (\<phi> ?y' (?f \<cdot>\<^sub>C HomC.\<psi> (?Fy, ?x) h \<cdot>\<^sub>C ?Fg))" > HomC.>_mapsto HomC.\<>_mapsto \<phi>_in_hom _inC of"f\cdot><sub>C HomC.\<psi> (?Fy, ?x) h \<cdot>\<^sub>C ?Fg"] by auto also have "... = inD (D ?Gf (D (\<phi> ?y (HomC.\<psi> hconf : ' bool" ( (no_types, lifting)Carr_codC.arr_dom_iff_arrC.arr_iff_in_hom C \<phi>_naturality \<psi>h) also have "... = ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x))) h" using gf \<psi>h \<phi>_in_hom by simp finally show ?thesis by auto qed qed qed have 8: "S.mkArr (HomC.set (?Fy, ?x)) (HomD.set (?y', ?Gx')) ((inD o \<phi> ?y' o HomC.\<psi> (?Fy', ?x')) o (inC o (\<lambda>h. ?f \<cdot>\<^sub>C h \<cdot>\<^sub>C ?Fg) o HomC.\<psi> (?Fy, ?x))) = S.mkArr (HomC.set (?Fy, ?x)) (HomD.set (?y', ?Gx')) ((inD o (\<lambda>h. ?Gf \<cdot>\<^sub>D h \<cdot>\<^sub>D ?g) o HomD.\<psi> (?y, ?Gx)) o (inD o \<phi> ?y o HomC.\<psi> (?Fy, ?x)))" using 5 7 by force show ?thesis using 5 6 8 by auto qed qed lemma \<Phi>_simp: assumes YX: "DopxC.ide yx" shows "\<Phi>.map yx = S.mkArr (HomC.set (F (fst yx), snd yx)) (HomD.set (fst yx, G (snd yx))) (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))" using YX \<Phi>o_def by simp abbreviation \<Psi>o where "\<Psi>o yx \<equiv> S.mkArr (HomD.set (fst yx, G (snd yx))) (HomC.set (F (fst yx), snd yx)) (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)))" lemma \<Psi>o_in_hom: assumes yx: "DopxC.ide yx" shows "\<guillemotleft>\<Psi>o yx : Hom_DopxG.map yx \<rightarrow>\<^sub>S Hom_FopxC.map yx\<guil proof - have "Hom_FopxC.map yx = S.mkIde (HomC.set (F (fst yx), snd yx))" using yx HomC.map_ide by auto moreover have "Hom_DopxG.map yx = S.mkIde (HomD.set (fst yx, G (snd yx)))" using yx HomD.map_ide by auto moreover have "\<guillemotleft>\<Psi>o yx : S.mkIde (HomD.set (fst yx, G (snd yx))) \<rightarrow>\<^sub>S S.mkIde (HomC.set (F (fst yx), snd yx))\<guillemotright>" proof (intro S.mkArr_in_hom) show "HomC.set (F (fst yx), snd yx) \<subseteq> S.Univ" using yx HomC.set_subset_Univ by simp show "HomD.set (fst yx, G (snd yx)) \<subseteq> S.Univ" using yx HomD.set_subset_Univ by simp show "inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)) \<in> HomD.set (fst yx, G (snd yx)) \<rightarrow> HomC.set (F (fst yx), snd yx)" proof fix x assume x: "x \<in> HomD.set (fst yx, G (snd yx))" show "(inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))) x \<in> HomC.set (F (fst yx), snd yx)" using x yx HomD.\<psi>_mapsto [of "fst yx" "G (snd yx)"] \<psi>_in_hom [of "snd yx"] HomC.\<phi>_mapsto [of "F (fst yx)" "snd yx"] by auto qed qed ultimately show ?thesis by auto qed lemma \<Phi>_inv: assumes yx: "DopxC.ide yx" shows "S.inverse_arrows (\<Phi>.map yx) (\<Psi>o yx)" proof - have 1: "\<guillemotleft>\<Phi>.map yx : Hom_FopxC.map yx \<rightarrow>\<^sub>S Hom_DopxG.map yx\< using yx \<Phi>.preserves_hom [of yx yx yx] DopxC.ide_in_hom by blast have 2: "\<guillemotleft>\<Psi>o yx : Hom_DopxG.map yx \<rightarrow>\<^sub>S Hom_FopxC.map yx\<gui using yx \<Psi>o_in_hom by simp have 3: "\<Phi>.map yx = S.mkArr (HomC.set (F (fst yx), snd yx)) (HomD.set (fst yx, G (snd yx))) (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))" using yx \<Phi>_simp by blast have antipar: "S.antipar (\<Phi>.map yx) (\<Psi>o yx)" using 1 2 by blast moreover have "S.ide (S.comp (\<Psi>o yx) (\<Phi>.map yx))" proof - have "S.comp (\<Psi>o yx) (\<Phi>.map yx) = S.mkArr (HomC.set (F (fst yx), snd yx)) (HomC.set (F (fst yx), snd yx)) ((inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))) o (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)))" using 1 2 3 antipar S.comp_mkArr by auto also have "... = S.mkArr (HomC.set (F (fst yx), snd yx)) (HomC.set (F (fst yx), snd yx)) (\<lambda>x. x)" proof - have "S.mkArr (HomC.set (F (fst yx), snd yx)) (HomC.set (F (fst yx), snd yx)) (\<lambda>x. x) = ..." proof show "S.arr (S.mkArr (HomC.set (F (fst yx), snd yx)) (HomC.set (F (fst yx), snd yx)) (\<lambda>x. x))" using yx HomC.set_subset_Univ by simp show "\<And>x. x \<in> HomC.set (F (fst yx), snd yx) \<Longrightarrow> x = ((inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))) o (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))) x" proof - fix x assume x: "x \<in> HomC.set (F (fst yx), snd yx)" have "((inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))) o (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))) x = inC (\<psi> (snd yx) (HomD.\<psi> (fst yx, G (snd yx)) (inD (\<phi> (fst yx) (HomC.\<psi> (F (fst yx), snd yx) x)))))" by simp also have "... = inC (\<psi> (snd yx) (\<phi> (fst yx) (HomC.\<psi> (F (fst yx), snd yx) x)))" using x yx HomC.\<psi>_mapsto [of "F (fst yx)" "snd yx"] \<phi>_in_hom by force also have "... = inC (HomC.\<psi> (F (fst yx), snd yx) x)" using x yx HomC.\<psi>_mapsto [of "F (fst yx)" "snd yx"] \<psi>_\<phi> by force also have "... = x" using x yx inC_\<psi> by simp finally show "x = ((inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))) o (inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx))) x" by auto qed qed thus ?thesis by auto qed also have "... = S.mkIde (HomC.set (F (fst yx), snd yx))" using yx S.mkIde_as_mkArr HomC.set_subset_Univ by force finally have "S.comp (\<Psi>o yx) (\<Phi>.map yx) = S.mkIde (HomC.set (F (fst yx), snd yx))" by auto thus ?thesis using yx HomC.set_subset_Univ S.ide_mkIde by simp qed moreover have "S.ide (S.comp (\<Phi>.map yx) (\<Psi>o yx))" proof - have "S.comp (\<Phi>.map yx) (\<Psi>o yx) = S.mkArr (HomD.set (fst yx, G (snd yx))) (HomD.set (fst yx, G (snd yx))) ((inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)) o (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx))))" using 1 2 3 S.comp_mkArr antipar by fastforce also have "... = S.mkArr (HomD.set (fst yx, G (snd yx))) (HomD.set (fst yx, G (snd yx))) (\<lambda>x. x)" proof - have "S.mkArr (HomD.set (fst yx, G (snd yx))) (HomD.set (fst yx, G (snd yx))) (\<lambda>x. x) = ..." proof show "S.arr (S.mkArr (HomD.set (fst yx, G (snd yx))) (HomD.set (fst yx, G (snd yx))) (\<lambda>x. x))" using yx HomD.set_subset_Univ by simp show "\<And>x. x \<in> (HomD.set (fst yx, G (snd yx))) \<Longrightarrow> x = ((inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)) o (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)))) x" proof - fix x assume x: "x \<in> HomD.set (fst yx, G (snd yx))" have "((inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)) o (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)))) x = inD (\<phi> (fst yx) (HomC.\<psi> (F (fst yx), snd yx) (inC (\<psi> (snd yx) (HomD.\<psi> (fst yx, G (snd yx)) x)))))" by simp also have "... = inD (\<phi> (fst yx) (\<psi> (snd yx) (HomD.\<psi> (fst yx, G (snd yx)) x)))" proof - have "\<guillemotleft>\<psi> (snd yx) (HomD.\<psi> (fst yx, G (snd yx)) x) : F (fst yx) \<rightarrow> sn using x yx HomD.\<psi>_mapsto [of "fst yx" "G (snd yx)"] \<psi>_in_hom by auto thus ?thesis by simp qed also have "... = inD (HomD.\<psi> (fst yx, G (snd yx)) x)" using x yx HomD.\<psi>_mapsto [of "fst yx" "G (snd yx)"] \<phi>_\<psi> by force also have "... = x" using x yx inD_\<psi> by simp finally show "x = ((inD o \<phi> (fst yx) o HomC.\<psi> (F (fst yx), snd yx)) o (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)))) x" by auto qed qed thus ?thesis by auto qed also have "... = S.mkIde (HomD.set (fst yx, G (snd yx)))" using yx S.mkIde_as_mkArr HomD.set_subset_Univ by force finally have "S.comp (\<Phi>.map yx) (\<Psi>o yx) = S.mkIde (HomD.set (fst yx, G (snd yx)))" by auto thus ?thesis using yx HomD.set_subset_Univ S.ide_mkIde by simp qed ultimately show ?thesis by auto qed interpretation \<Phi>: natural_isomorphism DopxC.comp S.comp Hom_FopxC.map Hom_DopxG.map \<Phi>.map using \<Phi>_inv by unfold_locales blast interpretation \<Psi>: inverse_transformation DopxC.comp S.comp Hom_FopxC.map Hom_DopxG.map \<Phi>.map .. interpretation \<Phi>\<Psi>: inverse_transformations DopxC.comp S.comp Hom_FopxC.map Hom_DopxG.map \<Phi>.map \<Psi>.map using \<Psi>.inverts_components by unfold_locales simp abbreviation \<Phi> where "\<Phi> \<equiv> \<Phi>.map" abbreviation \<Psi> where "\<Psi> \<equiv> \<Psi>.map" abbreviation HomC where "HomC \<equiv> HomC.map" abbreviation \<phi>C where "\<phi>C \<equiv> \<lambda>_. inC" abbreviation HomD where "HomD \<equiv> HomD.map" abbreviation \<phi>D where "\<phi>D \<equiv> \<lambda>_. inD" theorem induces_hom_adjunction: "hom_adjunction C D S.comp S.setp \<phi>C \<phi>D F G \<Phi> \<Psi>" lemma \<Psi>_simp: assumes yx: "DopxC.ide yx" shows "\<Psi> yx = S.mkArr (HomD.set (fst yx, G (snd yx))) (HomC.set (F (fst yx), snd yx)) (inC o \<psi> (snd yx) o HomD.\<psi> (fst yx, G (snd yx)))" using assms \<Phi>o_def \<Phi>_inv S.inverse_unique by simp text\<open> The original @{term \<phi>} and @{term \<psi>} can be recovered from @{term \<Phi>} and @{term \<Psi>}. \<close> interpretation \<Phi>: set_valued_transformation DopxC.comp S.comp S.setp Hom_FopxC.map Hom_DopxG.map \<Phi>.map .. interpretation \<Psi>: set_valued_transformation DopxC.comp S.comp S.setp Hom_DopxG.map Hom_FopxC.map \<Psi>.map .. lemma \<phi>_in_terms_of_\<Phi>': assumes y: "D.ide y" and f: "\<guillemotleft>f: F y \<rightarrow>\<^sub>C x\<guillemotright>" shows "\<phi> y f = (HomD.\<psi> (y, G x) o \<Phi>.FUN (y, x) o inC) f" proof - have x: "C.ide x" using f by auto have "(HomD.\<psi> (y, G x) o \<Phi>.FUN (y, x) o inC) f = HomD.\<psi> (y, G x) (restrict (inD o \<phi> y o HomC.\<psi> (F y, x)) (HomC.set (F y, x)) (inC f))" proof - have "S.arr (\<Phi> (y, x))" using x y by fastforce thus ?thesis using x y \<Phi>o_def by simp qed also have "... = \<phi> y f" using x y f HomC.\<phi>_mapsto \<phi>_in_hom HomC.\<psi>_mapsto C.ide_in_hom D.ide_in_hom by auto finally show ?thesis by auto qed lemma \<psi>_in_terms_of_\<Psi>': assumes x: "C.ide x" and g: "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" shows "\<psi> x g = (HomC.\<psi> (F y, x) o \<Psi>.FUN (y, x) o inD) g" proof - have y: "D.ide y" using g by auto have "(HomC.\<psi> (F y, x) o \<Psi>.FUN (y, x) o inD) g = HomC.\<psi> (F y, x) (restrict (inC o \<psi> x o HomD.\<psi> (y, G x)) (HomD.set (y, G x)) (inD g))" proof - have "S.arr (\<Psi> (y, x))" using x y \<Psi>.preserves_reflects_arr [of "(y, x)"] by simp thus ?thesis using x y \<Psi>_simp by simp qed also have "... = \<psi> x g" using x y g HomD.\<phi>_mapsto \<psi>_in_hom HomD.\<psi>_mapsto C.ide_in_hom D.ide_in_hom by auto finally show ?thesis by auto qed end section "Hom-Adjunctions Induce Meta-Adjunctions" context hom_adjunction begin definition \<phi> :: "'d \<Rightarrow> 'c \<Rightarrow> 'd" where "\<phi> y h = (HomD.\<psi> (y, G (C.cod h)) o \<Phi>.FUN (y, C.cod h) o \<phi>C (F y, C.cod h)) h" definition \<psi> :: "'c \<Rightarrow> 'd \<Rightarrow> 'c" where "\<psi> x h = (HomC.\<psi> (F (D.dom h), x) o \<Psi>.FUN (D.dom h, x) o \<phi>D (D.dom h, G x)) h" lemma Hom_FopxC_map_simp: assumes "DopxC.arr gf" shows "Hom_FopxC.map gf = S.mkArr (HomC.set (F (D.cod (fst gf)), C.dom (snd gf))) (HomC.set (F (D.dom (fst gf)), C.cod (snd gf))) (\<phi>C (F (D.dom (fst gf)), C.cod (snd gf)) o (\<lambda>h. snd gf \<cdot>\<^sub>C h \<cdot>\<^sub>C F (fst gf)) o HomC.\<psi> (F (D.cod (fst gf)), C.dom (snd gf)))" using assms HomC.map_def by simp lemma Hom_DopxG_map_simp: assumes "DopxC.arr gf" shows "Hom_DopxG.map gf = S.mkArr (HomD.set (D.cod (fst gf), G (C.dom (snd gf)))) (HomD.set (D.dom (fst gf), G (C.cod (snd gf)))) (\<phi>D (D.dom (fst gf), G (C.cod (snd gf))) o (\<lambda>h. G (snd gf) \<cdot>\<^sub>D h \<cdot>\<^sub>D fst gf) o HomD.\<psi> (D.cod (fst gf), G (C.dom (snd gf))))" using assms HomD.map_def by simp lemma \<Phi>_Fun_mapsto: assumes "D.ide y" and "\<guillemotleft>f : F y \<rightarrow>\<^sub>C x\<guillemotright>" shows "\<Phi>.FUN (y, x) \<in> HomC.set (F y, x) \<rightarrow> HomD.set (y, G x)" proof - have "S.arr (\<Phi> (y, x)) \<and> \<Phi>.DOM (y, x) = HomC.set (F y, x) \<and> \<Phi>.COD (y, x) = HomD.set (y, G x)" using assms HomC.set_map HomD.set_map by auto thus ?thesis using S.Fun_mapsto by blast qed lemma \<phi>_mapsto: assumes y: "D.ide y" shows "\<phi> y \<in> C.hom (F y) x \<rightarrow> D.hom y (G x)" proof fix h assume h: "h \<in> C.hom (F y) x" hence 1: " \<guillemotleft>h : F y \<rightarrow>\<^sub>C x\<guillemotright>" by simp show "\<phi> y h \<in> D.hom y (G x)" proof - have "\<phi>C (F y, x) h \<in> HomC.set (F y, x)" using y h 1 HomC.\<phi>_mapsto [of "F y" x] by fastforce hence "\<Phi>.FUN (y, x) (\<phi>C (F y, x) h) \<in> HomD.set (y, G x)" using h y \<Phi>_Fun_mapsto by auto thus ?thesis using y h 1 \<phi>_def HomC.\<phi>_mapsto HomD.\<psi>_mapsto [of y "G x"] by fastforce qed qed lemma \<Phi>_simp: assumes "D.ide y" and "C.ide x" shows "S.arr (\<Phi> (y, x))" and "\<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))" proof - show 1: "S.arr (\<Phi> (y, x))" using assms by auto hence "\<Phi> (y, x) = S.mkArr (\<Phi>.DOM (y, x)) (\<Phi>.COD (y, x)) (\<Phi>.FUN (y, x))" using S.mkArr_Fun by metis also have "... = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<Phi>.FUN (y, x))" using assms HomC.set_map HomD.set_map by fastforce also have "... = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))" proof (intro S.mkArr_eqI') show 2: "S.arr (S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<Phi>.FUN (y, x)))" using 1 calculation by argo show "\<And>h. h \<in> HomC.set (F y, x) \<Longrightarrow> \<Phi>.FUN (y, x) h = (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) h" proof - fix h assume h: "h \<in> HomC.set (F y, x)" have "(\<phi>D (y, G x) o \<phi> y o HomC.\<psi> (F y, x)) h = \<phi>D (y, G x) (\<psi>D (y, G x) (\<Phi>.FUN (y, x) (\<phi>C (F y, x) (\<psi>C (F y, x) h))))" proof - have "\<guillemotleft>\<psi>C (F y, x) h : F y \<rightarrow>\<^sub>C x\<guillemotright>" using assms h HomC.\<psi>_mapsto [of "F y" x] by auto thus ?thesis using h \<phi>_def by auto qed also have "... = \<phi>D (y, G x) (\<psi>D (y, G x) (\<Phi>.FUN (y, x) h))" using assms h HomC.\<phi>_\<psi> \<Phi>_Fun_mapsto by simp also have "... = \<Phi>.FUN (y, x) h" using assms h \<Phi>_Fun_mapsto [of y "\<psi>C (F y, x) h"] HomC.\<psi>_mapsto HomD.\<phi>_\<psi> [of y "G x"] C.ide_in_hom D.ide_in_hom by blast finally show "\<Phi>.FUN (y, x) h = (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) h" by auto qed qed finally show "\<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))" by force qed lemma \<Psi>_Fun_mapsto: assumes "C.ide x" and "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" shows "\<Psi>.FUN (y, x) \<in> HomD.set (y, G x) \<rightarrow> HomC.set (F y, x)" proof - have "S.arr (\<Psi> (y, x)) \<and> \<Psi>.COD (y, x) = HomC.set (F y, x) \<and> \<Psi>.DOM (y, x) = HomD.set (y, G x)" using assms HomC.set_map HomD.set_map by auto thus ?thesis using S.Fun_mapsto by fast qed lemma \<psi>_mapsto: assumes x: "C.ide x" shows "\<psi> x \<in> D.hom y (G x) \<rightarrow> C.hom (F y) x" proof fix h assume h: "h \<in> D.hom y (G x)" hence 1: "\<guillemotleft>h : y \<rightarrow>\<^sub>D G x\<guillemotright>" by auto show "\<psi> x h \<in> C.hom (F y) x" proof - have "\<Psi>.FUN (y, x) (\<phi>D (y, G x) h) \<in> HomC.set (F y, x)" proof - have "\<phi>D (y, G x) h \<in> HomD.set (y, G x)" using x h 1 HomD.\<phi>_mapsto [of y "G x"] by fastforce thus ?thesis using h x \<Psi>_Fun_mapsto by auto qed thus ?thesis using x h 1 \<psi>_def HomD.\<phi>_mapsto HomC.\<psi>_mapsto [of "F y" x] by fastforce qed qed lemma \<Psi>_simp: assumes "D.ide y" and "C.ide x" shows "S.arr (\<Psi> (y, x))" and "\<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" proof - show 1: "S.arr (\<Psi> (y, x))" using assms by auto hence "\<Psi> (y, x) = S.mkArr (\<Psi>.DOM (y, x)) (\<Psi>.COD (y, x)) (\<Psi>.FUN (y, x))" using S.mkArr_Fun by metis also have "... = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<Psi>.FUN (y, x))" using assms HomC.set_map HomD.set_map by auto also have "... = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" proof (intro S.mkArr_eqI') show "S.arr (S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<Psi>.FUN (y, x)))" using 1 calculation by argo show "\<And>h. h \<in> HomD.set (y, G x) \<Longrightarrow> \<Psi>.FUN (y, x) h = (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)) h" proof - fix h assume h: "h \<in> HomD.set (y, G x)" have "(\<phi>C (F y, x) o \<psi> x o HomD.\<psi> (y, G x)) h = \<phi>C (F y, x) (\<psi>C (F y, x) (\<Psi>.FUN (y, x) (\<phi>D (y, G x) (\<psi>D (y, G x) h))))" proof - have "\<guillemotleft>\<psi>D (y, G x) h : y \<rightarrow>\<^sub>D G x\<guillemotright>" using assms h HomD.\<psi>_mapsto [of y "G x"] by auto thus ?thesis using h \<psi>_def by auto qed also have "... = \<phi>C (F y, x) (\<psi>C (F y, x) (\<Psi>.FUN (y, x) h))" using assms h HomD.\<phi>_\<psi> \<Psi>_Fun_mapsto by simp also have "... = \<Psi>.FUN (y, x) h" using assms h \<Psi>_Fun_mapsto HomD.\<psi>_mapsto [of y "G x"] HomC.\<phi>_\<psi> [of "F y" x] C.ide_in_hom D.ide_in_hom by blast finally show "\<Psi>.FUN (y, x) h = (\<phi>C (F y, x) o \<psi> x o HomD.\<psi> (y, G x)) h" by auto qed qed finally show "\<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" by force qed text\<open> The length of the next proof stems from having to use properties of composition of arrows in @{term[source=true] S} to infer properties of the composition of the corresponding functions. \<close> interpretation \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> proof fix y :: 'd and x :: 'c and h :: 'c assume y: "D.ide y" and h: "\<guillemotleft>h : F y \<rightarrow>\<^sub>C x\<guillemotright>" have x: "C.ide x" using h by auto show "\<guillemotleft>\<phi> y h : y \<rightarrow>\<^sub>D G x\<guillemotright>" proof - have "\<Phi>.FUN (y, x) \<in> HomC.set (F y, x) \<rightarrow> HomD.set (y, G x)" using y h \<Phi>_Fun_mapsto by blast thus ?thesis using x y h \<phi>_def HomD.\<psi>_mapsto [of y "G x"] HomC.\<phi>_mapsto [of "F y" x] by auto qed show "\<psi> x (\<phi> y h) = h" proof - have 0: "restrict (\<lambda>h. h) (HomC.set (F y, x)) = restrict (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) (HomC.set (F y, x))" proof - have 1: "S.ide (\<Psi> (y, x) \<cdot>\<^sub>S \<Phi> (y, x))" using x y \<Phi>\<Psi>.inv [of "(y, x)"] by auto hence 6: "S.seq (\<Psi> (y, x)) (\<Phi> (y, x))" by auto have 2: "\<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) \<and> \<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" using x y \<Phi>_simp \<Psi>_simp by force have 3: "S (\<Psi> (y, x)) (\<Phi> (y, x)) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x))" proof - have 4: "S.arr (\<Psi> (y, x) \<cdot>\<^sub>S \<Phi> (y, x))" using 1 by auto hence "S (\<Psi> (y, x)) (\<Phi> (y, x)) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) ((\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))" using 1 2 S.ide_in_hom S.comp_mkArr by fastforce also have "... = S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x))" proof (intro S.mkArr_eqI') show "S.arr (S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) ((\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))))" using 4 calculation by simp show "\<And>h. h \<in> HomC.set (F y, x) \<Longrightarrow> ((\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) h = (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) h" proof - fix h assume h: "h \<in> HomC.set (F y, x)" hence "\<guillemotleft>\<phi> y (\<psi>C (F y, x) h) : y \<rightarrow>\<^sub>D G x\<guillemotright>" using x y h HomC.\<psi>_mapsto [of "F y" x] \<phi>_mapsto by auto thus "((\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) h = (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) h" using x y 1 \<phi>_mapsto HomD.\<psi>_\<phi> by simp qed qed finally show ?thesis by simp qed moreover have "\<Psi> (y, x) \<cdot>\<^sub>S \<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<lambda>h. h)" using 1 2 6 calculation S.mkIde_as_mkArr S.arr_mkArr S.dom_mkArr S.ideD(2) by metis ultimately have 4: "S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<lambda>h. h)" by auto have 5: "S.arr (S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)))" using 1 3 6 by presburger hence "restrict (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) (HomC.set (F y, x)) = S.Fun (S.mkArr (HomC.set (F y, x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)))" by auto also have "... = restrict (\<lambda>h. h) (HomC.set (F y, x))" using 4 5 by auto finally show ?thesis by auto qed moreover have "\<phi>C (F y, x) h \<in> HomC.set (F y, x)" using x y h HomC.\<phi>_mapsto [of "F y" x] by auto ultimately have "\<phi>C (F y, x) h = (\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) (\<phi>C (F y, x) h)" using x y h HomC.\<phi>_mapsto [of "F y" x] by fast hence "\<psi>C (F y, x) (\<phi>C (F y, x) h) = \<psi>C (F y, x) ((\<phi>C (F y, x) o (\<psi> x o \<phi> y) o \<psi>C (F y, x)) (\<phi>C (F y, x) h))" by simp hence "h = \<psi>C (F y, x) (\<phi>C (F y, x) (\<psi> x (\<phi> y (\<psi>C (F y, x) (\<phi>C (F y, x) h)))))" using x y h HomC.\<psi>_\<phi> [of "F y" x] by simp also have "... = \<psi> x (\<phi> y h)" using x y h HomC.\<psi>_\<phi> HomC.\<psi>_\<phi> \<phi>_mapsto \<psi>_mapsto by (metis PiE mem_Collect_eq) finally show ?thesis by auto qed next fix x :: 'c and h :: 'd and y :: 'd assume x: "C.ide x" and h: "\<guillemotleft>h : y \<rightarrow>\<^sub>D G x\<guillemotright>" have y: "D.ide y" using h by auto show "\<guillemotleft>\<psi> x h : F y \<rightarrow>\<^sub>C x\<guillemotright>" using x y h \<psi>_mapst show "\<phi> y (\<psi> x h) = h" proof - have 0: "restrict (\<lambda>h. h) (HomD.set (y, G x)) = restrict (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) (HomD.set (y, G x))" proof - have 1: "S.ide (S (\<Phi> (y, x)) (\<Psi> (y, x)))" using x y \<Phi>\<Psi>.inv by force hence 6: "S.seq (\<Phi> (y, x)) (\<Psi> (y, x))" by auto have 2: "\<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) \<and> \<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" using x h \<Phi>_simp \<Psi>_simp by auto have 3: "S (\<Phi> (y, x)) (\<Psi> (y, x)) = S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x))" proof - have 4: "S.seq (\<Phi> (y, x)) (\<Psi> (y, x))" using 1 by auto hence "S (\<Phi> (y, x)) (\<Psi> (y, x)) = S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) ((\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) o (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x)))" using 1 2 6 S.ide_in_hom S.comp_mkArr by fastforce also have "... = S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x))" proof show "S.arr (S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) ((\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) o (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))))" using 4 calculation by simp show "\<And>h. h \<in> HomD.set (y, G x) \<Longrightarrow> ((\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) o (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))) h = (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) h" proof - fix h assume h: "h \<in> HomD.set (y, G x)" hence "\<guillemotleft>\<psi> x (\<psi>D (y, G x) h) : F y \<rightarrow>\<^sub>C x\<guillemotright>" using x y HomD.\<psi>_mapsto [of y "G x"] \<psi>_mapsto by auto thus "((\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)) o (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))) h = (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) h" using x y HomC.\<psi>_\<phi> by simp qed qed finally show ?thesis by auto qed moreover have "\<Phi> (y, x) \<cdot>\<^sub>S \<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<lambda>h. h)" using 1 2 6 calculation by (metis S.arr_mkArr S.cod_mkArr S.ide_in_hom S.mkIde_as_mkArr S.in_homE) ultimately have 4: "S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) = S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<lambda>h. h)" by auto have 5: "S.arr (S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)))" using 1 3 by fastforce hence "restrict (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) (HomD.set (y, G x)) = S.Fun (S.mkArr (HomD.set (y, G x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)))" by auto also have "... = restrict (\<lambda>h. h) (HomD.set (y, G x))" using 4 5 by auto finally show ?thesis by auto qed moreover have "\<phi>D (y, G x) h \<in> HomD.set (y, G x)" using x y h HomD.\<phi>_mapsto [of y "G x"] by auto ultimately have "\<phi>D (y, G x) h = (\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) (\<phi>D (y, G x) h)" by fast hence "\<psi>D (y, G x) (\<phi>D (y, G x) h) = \<psi>D (y, G x) ((\<phi>D (y, G x) o (\<phi> y o \<psi> x) o \<psi>D (y, G x)) (\<phi>D (y, G x) h))" by simp hence "h = \<psi>D (y, G x) (\<phi>D (y, G x) (\<phi> y (\<psi> x (\<psi>D (y, G x) (\<phi>D (y, G x) h)))))" using x y h HomD.\<psi>_\<phi> by simp also have "... = \<phi> y (\<psi> x h)" using x y h HomD.\<psi>_\<phi> HomD.\<psi>_\<phi> [of "\<phi> y (\<psi> x h)" y "G x"] \<phi>_mapsto \<psi>_maps by fastforce finally show ?thesis by auto qed next fix x :: 'c and x' :: 'c and y :: 'd and y' :: 'd and f :: 'c and g :: 'd and h :: 'c assume f: "\<guillemotleft>f : x \<rightarrow>\<^sub>C x'\<guillemotright>" and g: "\<guillemotlef have x: "C.ide x" using f by auto have y: "D.ide y" using g by auto have x': "C.ide x'" using f by auto have y': "D.ide y'" using g by auto show "\<phi> y' (f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) = G f \<cdot>\<^sub>D \<phi> y h \<cdot>\<^sub>D g" proof - have 0: "restrict ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) (HomC.set (F y, x)) = restrict ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g)) o \<psi>C (F y, x)) (HomC.set (F y, x))" proof - have 1: "S.arr (\<Phi> (y, x)) \<and> \<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))" using x y \<Phi>_simp [of y x] by auto have 2: "S.arr (\<Phi> (y', x')) \<and> \<Phi> (y', x') = S.mkArr (HomC.set (F y', x')) (HomD.set (y', G x')) (\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x'))" using x' y' \<Phi>_simp [of y' x'] by auto have 3: "S.arr (S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))) \<and> S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) = S (S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))) (S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))" proof - have 1: "S.seq (S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))) (S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))" proof - have "S.arr (Hom_DopxG.map (g, f)) \<and> Hom_DopxG.map (g, f) = S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))" using f g Hom_DopxG.preserves_arr Hom_DopxG_map_simp by fastforce thus ?thesis using 1 S.cod_mkArr S.dom_mkArr S.seqI by metis qed have "S.seq (S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))) (S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))" using 1 by (intro S.seqI', auto) moreover have "S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) = S (S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))) (S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x)))" using 1 S.comp_mkArr by fastforce ultimately show ?thesis by auto qed moreover have 4: "S.arr (S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))) \<and> S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))) = S (S.mkArr (HomC.set (F y', x')) (HomD.set (y', G x')) (\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x'))) (S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))" proof - have 5: "S.seq (S.mkArr (HomC.set (F y', x')) (HomD.set (y', G x')) (\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x'))) (S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))" proof - have "S.arr (Hom_FopxC.map (g, f)) \<and> Hom_FopxC.map (g, f) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))" using f g Hom_FopxC.preserves_arr Hom_FopxC_map_simp by fastforce thus ?thesis using 2 S.cod_mkArr S.dom_mkArr S.seqI by metis qed have "S.seq (S.mkArr (HomC.set (F y', x')) (HomD.set (y', G x')) (\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x'))) (S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))" using 5 by (intro S.seqI', auto) moreover have "S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))) = S (S.mkArr (HomC.set (F y', x')) (HomD.set (y', G x')) (\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x'))) (S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))" using 5 S.comp_mkArr by fastforce ultimately show ?thesis by argo qed moreover have 2: "S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) = S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x)))" proof - have "S (Hom_DopxG.map (g, f)) (\<Phi> (y, x)) = S (\<Phi> (y', x')) (Hom_FopxC.map (g, f))" using f g \<Phi>.naturality1 \<Phi>.naturality2 by fastforce moreover have "Hom_DopxG.map (g, f) = S.mkArr (HomD.set (y, G x)) (HomD.set (y', G x')) (\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x))" using f g Hom_DopxG_map_simp [of "(g, f)"] by fastforce moreover have "Hom_FopxC.map (g, f) = S.mkArr (HomC.set (F y, x)) (HomC.set (F y', x')) (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))" using f g Hom_FopxC_map_simp [of "(g, f)"] by fastforce ultimately show ?thesis using 1 2 3 4 by simp qed ultimately have 6: "S.arr (S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))))" by fast hence "restrict ((\<phi>D (y', G x') o (\<lambda>h. D (G f) (D h g)) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))) (HomC.set (F y, x)) = S.Fun (S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) o \<psi>D (y, G x)) o (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))))" by simp also have "... = S.Fun (S.mkArr (HomC.set (F y, x)) (HomD.set (y', G x')) ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))))" using 2 by argo also have "... = restrict ((\<phi>D (y', G x') o \<phi> y' o \<psi>C (F y', x')) o (\<phi>C (F y', x') o (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))) (HomC.set (F y, x))" using 4 S.Fun_mkArr by meson finally show ?thesis by auto qed hence 5: "((\<phi>D (y', G x') \<circ> (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) \<circ> \<psi>D (y, G x \<circ> (\<phi>D (y, G x) \<circ> \<phi> y \<circ> \<psi>C (F y, x))) (\<phi>C (F y, x) h) = (\<phi>D (y', G x') \<circ> \<phi> y' \<circ> \<psi>C (F y', x') \<circ> (\<phi>C (F y', x') \<circ> (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g)) \<circ> \<psi>C (F y, x)) ( proof - have "\<phi>C (F y, x) h \<in> HomC.set (F y, x)" using x y h HomC.\<phi>_mapsto [of "F y" x] by auto thus ?thesis using 0 h restr_eqE [of "(\<phi>D (y', G x') \<circ> (\<lambda>h. G f \<cdot>\<^sub>D h \<cdot>\<^sub>D g) \<cir \<circ> (\<phi>D (y, G x) \<circ> \<phi> y \<circ> \<psi>C (F y, x))" "HomC.set (F y, x)" "(\<phi>D (y', G x') \<circ> \<phi> y' \<circ> \<psi>C (F y', x')) \<circ> (\<phi>C (F y', x') \<circ> (\<lambda>h. f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) o \<psi>C (F y, x))"] by fast qed show ?thesis proof - have "\<phi> y' (C f (C h (F g))) = \<psi>D (y', G x') (\<phi>D (y', G x') (\<phi> y' (\<psi>C (F y', x') (\<phi>C (F y', x') (C f (C (\<psi>C (F y, x) (\<phi>C (F y, x) h)) (F g)))))))" proof - have "\<psi>D (y', G x') (\<phi>D (y', G x') (\<phi> y' (\<psi>C (F y', x') (\<phi>C (F y', x') (C f (C (\<psi>C (F y, x) (\<phi>C (F y, x) h)) (F g))))))) = \<psi>D (y', G x') (\<phi>D (y', G x') (\<phi> y' (\<psi>C (F y', x') (\<phi>C (F y', x') (C f (C h (F g)))))))" using x y h HomC.\<psi>_\<phi> by simp also have "... = \<psi>D (y', G x') (\<phi>D (y', G x') (\<phi> y' (C f (C h (F g)))))" using f g h HomC.\<psi>_\<phi> [of "C f (C h (F g))"] by fastforce also have "... = \<phi> y' (C f (C h (F g)))" proof - have "\<guillemotleft>\<phi> y' (f \<cdot>\<^sub>C h \<cdot>\<^sub>C F g) : y' \<rightarrow>\<^sub>D G x'\<gui using f g h y' x' \<phi>_mapsto [of y' x'] by auto thus ?thesis by simp qed finally show ?thesis by auto qed also have "... = \<psi>D (y', G x') (\<phi>D (y', G x') (G f \<cdot>\<^sub>D \<psi>D (y, G x) (\<phi>D (y, G x) (\<phi> y (\<psi>C (F y, x) (\<phi>C (F y, x) h)))) \<cdot>\<^sub>D g))" using 5 by force also have "... = D (G f) (D (\<phi> y h) g)" proof - have \<phi>yh: "\<guillemotleft>\<phi> y h : y \<rightarrow>\<^sub>D G x\<guillemotright>" using x y h \<phi>_mapsto by auto have "\<psi>D (y', G x') (\<phi>D (y', G x') (G f \<cdot>\<^sub>D \<psi>D (y, G x) (\<phi>D (y, G x) (\<phi> y (\<psi>C (F y, x) (\<phi>C (F y, x) h)))) \<cdot>\<^sub>D g)) = \<psi>D (y', G x') (\<phi>D (y', G x') (G f \<cdot>\<^sub>D \<psi>D (y, G x) (\<phi>D (y, G x) (\<phi> y h)) \<cdot>\<^ using x y f g h by auto also have "... = \<psi>D (y', G x') (\<phi>D (y', G x') (G f \<cdot>\<^sub>D \<phi> y h \<cdot>\<^sub>D g))" using \<phi>yh x' y' f g by simp also have "... = G f \<cdot>\<^sub>D \<phi> y h \<cdot>\<^sub>D g" using \<phi>yh f g by fastforce finally show ?thesis by auto qed finally show ?thesis by auto qed qed qed theorem induces_meta_adjunction: shows "meta_adjunction C D F G \<phi> \<psi>" .. end section "Putting it All Together" text\<open> Combining the above results, an interpretation of any one of the locales: \<open>left_adjoint_functor\<close>, \<open>right_adjoint_functor\<close>, \<open>meta_adjun \<open>hom_adjunction\<close>, and \<open>unit_counit_adjunction\<close> extends to an interpr of \<open>adjunction\<close>. \<close> context meta_adjunction begin interpretation S: replete_setcat . interpretation F: left_adjoint_functor D C F using has_left_adjoint_functor by auto interpretation G: right_adjoint_functor C D G using has_right_adjoint_functor by auto interpretation \<eta>\<epsilon>: unit_counit_adjunction C D F G \<eta> \<epsilon> using induces_unit_counit_adjunction \<eta>_def \<epsilon>_def by auto interpretation \<Phi>\<Psi>: hom_adjunction C D S.comp S.setp \<phi>C \<phi>D F G \<Phi> \<Psi> using induces_hom_adjunction by auto theorem induces_adjunction: shows "adjunction C D S.comp S.setp \<phi>C \<phi>D F G \<phi> \<psi> \<eta> \<epsilon> \<Phi> \<Psi>" using \<epsilon>_map_simp \<eta>_map_simp \<phi>_in_terms_of_\<eta> \<phi>_in_terms_of_\<Phi>' \<p \<psi>_in_terms_of_\<Psi>' \<Phi>_simp \<Psi>_simp \<eta>_def \<epsilon>_def by unfold_locales auto end context unit_counit_adjunction begin interpretation \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> using induces_meta_adjunction by interpretation S: replete_setcat . interpretation F: left_adjoint_functor D C F using \<phi>\<psi>.has_left_adjoint_functor by a interpretation G: right_adjoint_functor C D G using \<phi>\<psi>.has_right_adjoint_functor b interpretation \<Phi>\<Psi>: hom_adjunction C D S.comp S.setp \<phi>\<psi>.\<phi>C \<phi>\<psi>.\<phi>D F G \<phi>\<psi>.\<Phi> \<phi>\<psi>.\<Psi> using \<phi>\<psi>.induces_hom_adjunction by auto theorem induces_adjunction: shows "adjunction C D S.comp S.setp \<phi>\<psi>.\<phi>C \<phi>\<psi>.\<phi>D F G \<phi> \<psi> \<eta> \<epsilon> using \<epsilon>_in_terms_of_\<psi> \<eta>_in_terms_of_\<phi> \<phi>\<psi>.\<phi>_in_terms_of_\<Ph \<phi>\<psi>.\<Phi>_simp \<phi>\<psi>.\<Psi>_simp \<phi>_def by unfold_locales auto end context hom_adjunction begin interpretation \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> using induces_meta_adjunction by auto interpretation F: left_adjoint_functor D C F using \<phi>\<psi>.has_left_adjoint_functor by a interpretation G: right_adjoint_functor C D G using \<phi>\<psi>.has_right_adjoint_functor b interpretation \<eta>\<epsilon>: unit_counit_adjunction C D F G \<phi>\<psi>.\<eta> \<phi>\<psi>.\<epsi using \<phi>\<psi>.induces_unit_counit_adjunction \<phi>\<psi>.\<eta>_def \<phi>\<psi>.\<epsilon>_d theorem induces_adjunction: shows "adjunction C D S setp \<phi>C \<phi>D F G \<phi> \<psi> \<phi>\<psi>.\<eta> \<phi>\<psi>.\<epsilon> \<Phi> \<Ps proof fix x assume "C.ide x" thus "\<phi>\<psi>.\<epsilon> x = \<psi> x (G x)" using \<phi>\<psi>.\<epsilon>_map_simp \<phi>\<psi>.\<epsilon>_def by simp next fix y assume "D.ide y" thus "\<phi>\<psi>.\<eta> y = \<phi> y (F y)" using \<phi>\<psi>.\<eta>_map_simp \<phi>\<psi>.\<eta>_def by simp fix x y f assume y: "D.ide y" and f: "\<guillemotleft>f : F y \<rightarrow>\<^sub>C x\<guillemotright>" show "\<phi> y f = G f \<cdot>\<^sub>D \<phi>\<psi>.\<eta> y" using y f \<phi>\<psi>.\<phi>_in_terms_of_\<eta> \<phi>\<psi>.\<eta>_def by simp show "\<phi> y f = (\<psi>D (y, G x) \<circ> \<Phi>.FUN (y, x) \<circ> \<phi>C (F y, x)) f" using y f \<phi>_def by auto next fix x y g assume x: "C.ide x" and g: "\<guillemotleft>g : y \<rightarrow>\<^sub>D G x\<guillemotright>" show "\<psi> x g = \<phi>\<psi>.\<epsilon> x \<cdot>\<^sub>C F g" using x g \<phi>\<psi>.\<psi>_in_terms_of_\<epsilon> \<phi>\<psi>.\<epsilon>_def by simp show "\<psi> x g = (\<psi>C (F y, x) \<circ> \<Psi>.FUN (y, x) \<circ> \<phi>D (y, G x)) g" using x g \<psi>_def by fast next fix x y assume x: "C.ide x" and y: "D.ide y" show "\<Phi> (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x)) (\<phi>D (y, G x) o \<phi> y o \<psi>C (F y, x))" using x y \<Phi>_simp by simp show "\<Psi> (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x)) (\<phi>C (F y, x) o \<psi> x o \<psi>D (y, G x))" using x y \<Psi>_simp by simp qed end context left_adjoint_functor begin interpretation \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> using induces_meta_adjunction by auto interpretation S: replete_setcat . theorem induces_adjunction: shows "adjunction C D S.comp S.setp \<phi>\<psi>.\<phi>C \<phi>\<psi>.\<phi>D F G \<phi> \<psi> \<phi>\<psi>.\<et using \<phi>\<psi>.induces_adjunction by auto end context right_adjoint_functor begin interpretation \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> using induces_meta_adjunction by auto interpretation S: replete_setcat . theorem induces_adjunction: shows "adjunction C D S.comp S.setp \<phi>\<psi>.\<phi>C \<phi>\<psi>.\<phi>D F G \<phi> \<psi> \<phi>\<psi>.\<et using \<phi>\<psi>.induces_adjunction by auto end definition adjoint_functors where "adjoint_functors C D F G = (\<exists>\<phi> \<psi>. meta_adjunction C D F G \<phi> \<psi>)" lemma adjoint_functors_respects_naturally_isomorphic: assumes "adjoint_functors C D F G" and "naturally_isomorphic D C F' F" and "naturally_isomorphic C D G G'" shows "adjoint_functors C D F' G'" proof - obtain \<phi> \<psi> where \<phi>\<psi>: "meta_adjunction C D F G \<phi> \<psi>" using assms(1) adjoint_functors_def by blast interpret \<phi>\<psi>: meta_adjunction C D F G \<phi> \<psi> using \<phi>\<psi> by simp obtain \<tau> where \<tau>: "natural_isomorphism D C F' F \<tau>" using assms(2) naturally_isomorphic_def by blast obtain \<mu> where \<mu>: "natural_isomorphism C D G G' \<mu>" using assms(3) naturally_isomorphic_def by blast show ?thesis using adjoint_functors_def \<tau> \<mu> \<phi>\<psi>.respects_natural_isomorphism by blast qed lemma left_adjoint_functor_respects_naturally_isomorphic: assumes "left_adjoint_functor D C F" and "naturally_isomorphic D C F F'" shows "left_adjoint_functor D C F'" proof - interpret F: left_adjoint_functor D C F using assms(1) by simp have 1: "meta_adjunction C D F F.G F.\<phi> F.\<psi>" using F.induces_meta_adjunction by simp interpret \<phi>\<psi>: meta_adjunction C D F F.G F.\<phi> F.\<psi> using 1 by simp have "adjoint_functors C D F F.G" using 1 adjoint_functors_def by blast hence 2: "adjoint_functors C D F' F.G" using assms(2) adjoint_functors_respects_naturally_isomorphic [of C D F F.G F' F.G] naturally_isomorphic_reflexive naturally_isomorphic_symmetric \<phi>\<psi>.G.functor_axioms by blast obtain \<phi>' \<psi>' where \<phi>'\<psi>': "meta_adjunction C D F' F.G \<phi>' \<psi>'" using 2 adjoint_functors_def by blast interpret \<phi>'\<psi>': meta_adjunction C D F' F.G \<phi>' \<psi>' using \<phi>'\<psi>' by simp show ?thesis using \<phi>'\<psi>'.has_left_adjoint_functor by simp qed lemma right_adjoint_functor_respects_naturally_isomorphic: assumes "right_adjoint_functor C D G" and "naturally_isomorphic C D G G'" shows "right_adjoint_functor C D G'" proof - interpret G: right_adjoint_functor C D G using assms(1) by simp have 1: "meta_adjunction C D G.F G G.\<phi> G.\<psi>" using G.induces_meta_adjunction by simp interpret \<phi>\<psi>: meta_adjunction C D G.F G G.\<phi> G.\<psi> using 1 by simp have "adjoint_functors C D G.F G" using 1 adjoint_functors_def by blast hence 2: "adjoint_functors C D G.F G'" using assms(2) adjoint_functors_respects_naturally_isomorphic naturally_isomorphic_reflexive naturally_isomorphic_symmetric \<phi>\<psi>.F.functor_axioms by blast obtain \<phi>' \<psi>' where \<phi>'\<psi>': "meta_adjunction C D G.F G' \<phi>' \<psi>'" using 2 adjoint_functors_def by blast interpret \<phi>'\<psi>': meta_adjunction C D G.F G' \<phi>' \<psi>' using \<phi>'\<psi>' by simp show ?thesis using \<phi>'\<psi>'.has_right_adjoint_functor by simp qed section "Inverse Functors are Adjoints" (* TODO: This really should show that inverse functors induce an adjoint equivalence. *) lemma inverse_functors_induce_meta_adjunction: assumes "inverse_functors C D F G" shows "meta_adjunction C D F G (λx. G) (λy. F)" proof - interpret inverse_functors C D F G using assms by auto interpret meta_adjunction C D F G ‹λx. G› ‹λy. F› proof - have 1: "∧y. B.arr y ==> G (F y) = y" by (metis B.map_simp comp_apply inv) have 2: "∧x. A.arr x ==> F (G x) = x" by (metis A.map_simp comp_apply inv') show "meta_adjunction C D F G (λx. G) (λy. F)" proof fix y f x assume y: "B.ide y" and f: "«f : F y →A x¬" show "«G f : y →B G x¬" using y f 1 G.preserves_hom by (elim A.in_homE, auto) show "F (G f) = f" using f 2 by auto next fix x g y assume x: "A.ide x" and g: "«g : y →B G x¬" show "«F g : F y →A x¬" using x g 2 F.preserves_hom by (elim B.in_homE, auto) show "G (F g) = g" using g 1 A.map_def by blast next fix f x x' g y' y h assume f: "«f : x →A x'¬" and g: "«g : y' →B y¬" and h: "«h : F y →A x¬" show "G (C f (C h (F g))) = D (G f) (D (G h) g)" using f g h 1 2 inv inv' A.map_def B.map_def by (elim A.in_homE B.in_homE, auto) qed qed show ?thesis .. qed lemma inverse_functors_are_adjoints: assumes "inverse_functors A B F G" shows "adjoint_functors A B F G" using assms inverse_functors_induce_meta_adjunction adjoint_functors_def by fast context inverse_functors begin lemma η_char: shows "meta_adjunction.η B F (λx. G) = identity_functor.map B" proof (intro natural_transformation_eqI) interpret meta_adjunction A B F G ‹λy. G› ‹λx. F› using inverse_functors_induce_meta_adjunction inverse_functors_axioms by auto interpret S: replete_setcat . interpret adjunction A B S.comp S.setp φC φD F G ‹λy. G› ‹λx. F› η ε Φ Ψ using induces_adjunction by force show "natural_transformation B B B.map GF.map η" using η.natural_transformation_axioms by auto show "natural_transformation B B B.map GF.map B.map" by (simp add: B.as_nat_trans.natural_transformation_axioms inv) show "∧b. B.ide b ==> η b = B.map b" using η_in_terms_of_φ ηo_def ηo_in_hom by fastforce qed lemma ε_char: shows "meta_adjunction.ε A F G (λy. F) = identity_functor.map A" proof (intro natural_transformation_eqI) interpret meta_adjunction A B F G ‹λy. G› ‹λx. F› using inverse_functors_induce_meta_adjunction inverse_functors_axioms by auto interpret S: replete_setcat . interpret adjunction A B S.comp S.setp φC φD F G ‹λy. G› ‹λx. F› η ε Φ Ψ using induces_adjunction by force show "natural_transformation A A FG.map A.map ε" using ε.natural_transformation_axioms by auto show "natural_transformation A A FG.map A.map A.map" by (simp add: A.as_nat_trans.natural_transformation_axioms inv') show "∧a. A.ide a ==> ε a = A.map a" using ε_in_terms_of_ψ εo_def εo_in_hom by fastforce qed end section "Composition of Adjunctions" locale composite_adjunction = A: category A + B: category B + C: category C + F: "functor" B A F + G: "functor" A B G + F': "functor" C B F' + G': "functor" B C G' + FG: meta_adjunction A B F G φ ψ + F'G': meta_adjunction B C F' G' φ' ψ' for A :: "'a comp" (infixr ‹⋅A› 55) and B :: "'b comp" (infixr ‹⋅B› 55) and C :: "'c comp" (infixr ‹⋅C› 55) and F :: "'b ==> 'a" and G :: "'a ==> 'b" and F' :: "'c ==> 'b" and G' :: "'b ==> 'c" and φ :: "'b ==> 'a ==> 'b" and ψ :: "'a ==> 'b ==> 'a" and φ' :: "'c ==> 'b ==> 'c" and ψ' :: "'b ==> 'c ==> 'b" begin interpretation S: replete_setcat . interpretation FG: adjunction A B S.comp S.setp FG.φC FG.φD F G φ ψ FG.η FG.ε FG.Φ FG.Ψ using FG.induces_adjunction by simp interpretation F'G': adjunction B C S.comp S.setp F'G'.φC F'G'.φD F' G' φ' ψ' F'G'.η F'G'.ε F'G'.Φ F'G'.Ψ using F'G'.induces_adjunction by simp (* Notation for C.in_hom is inherited here somehow, but I don't know from where. *) lemma is_meta_adjunction: shows "meta_adjunction A C (F o F') (G' o G) (λz. φ' z o φ (F' z)) (λx. ψ x o ψ' (G x)) proof - interpret G'oG: composite_functor A B C G G' .. interpret FoF': composite_functor C B A F' F .. show ?thesis proof fix y f x assume y: "C.ide y" and f: "«f : FoF'.map y →A x¬" show "«(φ' y ∘ φ (F' y)) f : y →C G'oG.map x¬" using y f FG.φ_in_hom F'G'.φ_in_hom by simp show "(ψ x ∘ ψ' (G x)) ((φ' y ∘ φ (F' y)) f) = f" using y f FG.φ_in_hom F'G'.φ_in_hom FG.ψ_φ F'G'.ψ_φ by simp next fix x g y assume x: "A.ide x" and g: "«g : y →C G'oG.map x¬" show "«(ψ x ∘ ψ' (G x)) g : FoF'.map y →A x¬" using x g FG.ψ_in_hom F'G'.ψ_in_hom by auto show "(φ' y ∘ φ (F' y)) ((ψ x ∘ ψ' (G x)) g) = g" using x g FG.ψ_in_hom F'G'.ψ_in_hom FG.φ_ψ F'G'.φ_ψ by simp next fix f x x' g y' y h assume f: "«f : x →A x'¬" and g: "«g : y' →C y¬" and h: "«h : FoF'.map y →A x¬" show "(φ' y' ∘ φ (F' y')) (f ⋅A h ⋅A FoF'.map g) = G'oG.map f ⋅C (φ' y ∘ φ (F' y)) h ⋅C g" using f g h FG.φ_naturality [of f x x' "F' g" "F' y'" "F' y" h] F'G'.φ_naturality [of "G f" "G x" "G x'" g y' y "φ (F' y) h"] FG.φ_in_hom by fastforce qed qed interpretation KηH: natural_transformation C C ‹G' o F'› ‹G' o G o F o F'› ‹G' o FG.η o F'› proof - interpret ηF': natural_transformation C B F' ‹(G o F) o F'› ‹FG.η o F'› using FG.η_naturalitytransformation F'.as_nat_trans.natural_transformation_axioms horizontal_composite by fastforce interpret G'ηF': natural_transformation C C ‹G' o F'› ‹G' o (G o F o F')› ‹G' o (FG.η o F')› using ηF'.natural_transformation_axioms G'.as_nat_trans.natural_transformation_axio horizontal_composite by blast show "natural_transformation C C (G' o F') (G' o G o F o F') (G' o FG.η o F')" using G'ηF'.natural_transformation_axioms o_assoc by metis qed interpretation G'ηF'oη': vertical_composite C C C.map ‹G' o F'› ‹G' o G o F o F'› F'G'.η ‹G' o FG.η o F'› .. interpretation FεG: natural_transformation A A ‹F o F' o G' o G› ‹F o G› ‹F o F'G'.ε o G› proof - interpret Fε': natural_transformation B A ‹F o (F' o G')› F ‹F o F'G'.ε› using F'G'.ε.natural_transformation_axioms F.as_nat_trans.natural_transformation_ax horizontal_composite by fastforce interpret Fε'G: natural_transformation A A ‹F o (F' o G') o G› ‹F o G› ‹F o F'G'.ε o G› using Fε'.natural_transformation_axioms G.as_nat_trans.natural_transformation_axiom horizontal_composite by blast show "natural_transformation A A (F o F' o G' o G) (F o G) (F o F'G'.ε o G)" using Fε'G.natural_transformation_axioms o_assoc by metis qed interpretation εoFε'G: vertical_composite A A ‹F ∘ F' ∘ G' ∘ G› ‹F o G› A.map ‹F o F'G'.ε o G› FG.ε .. interpretation meta_adjunction A C ‹F o F'› ‹G' o G› ‹λz. φ' z o φ (F' z)› ‹λx. ψ x o ψ' (G x)› using is_meta_adjunction by auto interpretation S: replete_setcat . interpretation adjunction A C S.comp S.setp φC φD ‹F ∘ F'› ‹G' ∘ G› ‹λz. φ' z ∘ φ (F' z)› ‹λx. ψ x ∘ ψ' (G x)› η ε Φ Ψ using induces_adjunction by simp lemma η_char: shows "η = G'ηF'oη'.map" proof (intro natural_transformation_eqI) show "natural_transformation C C C.map (G' o G o F o F') G'ηF'oη'.map" .. show "natural_transformation C C C.map (G' o G o F o F') η" by (metis (no_types, lifting) η_naturalitytransformation o_assoc) fix a assume a: "C.ide a" show "η a = G'ηF'oη'.map a" unfolding η_def using a G'ηF'oη'.map_def FG.η.preserves_hom [of "F' a" "F' a" "F' a"] F'G'.φ_in_terms_of_η FG.η_map_simp η_map_simp [of a] C.ide_in_hom F'G'.η_def FG.η_def by auto qed lemma ε_char: shows "ε = εoFε'G.map" proof (intro natural_transformation_eqI) show "natural_transformation A A (F o F' o G' o G) A.map ε" by (metis (no_types, lifting) ε_naturalitytransformation o_assoc) show "natural_transformation A A (F ∘ F' ∘ G' ∘ G) A.map εoFε'G.map" .. fix a assume a: "A.ide a" show "ε a = εoFε'G.map a" proof - have "ε a = ψ a (ψ' (G a) (G' (G a)))" using a ε_in_terms_of_ψ by simp also have "... = FG.ε a ⋅A F (F'G'.ε (G a) ⋅B F' (G' (G a)))" by (metis F'G'.ε_in_terms_of_ψ F'G'.εo_def F'G'.εo_in_hom F'G'.ηε.ε_in_terms_of_ψ F'G'.ηε.ψ_def FG.Gε.natural_transformation_axioms FG.ψ_in_terms_of_ε a functor.preserves_ide natural_transformation_def) also have "... = εoFε'G.map a" using a B.comp_arr_dom εoFε'G.map_def by simp finally show ?thesis by blast qed qed end section "Right Adjoints are Unique up to Natural Isomorphism" text‹ As an example of the use of the of the foregoing development, we show that two r to the same functor are naturally isomorphic. theorem two_right_adjoints_naturally_isomorphic: assumes "adjoint_functors C D F G" and "adjoint_functors C D F G'" shows "naturally_isomorphic C D G G'" proof - text‹ For any object @{term x} of @{term C}, we have that ‹ε x ∈ C.hom (F (G x)) x› is a terminal arrow from @{term F} to @{term x}, and similarly for ‹ε' x›. We may therefore obtain the unique coextension ‹τ x ∈ D.hom (G x) (G' x)› of ‹ε x› along ‹ε' x›. An explicit formula for ‹τ x› is ‹D (G' (ε x)) (η' (G x))›. Similarly, we obtain ‹τ' x = D (G (ε' x)) (η (G' x)) ∈ D.hom (G' x) (G x)›. We show these are the components of inverse natural transformations between @{term G} and @{term G'}. › obtain φ ψ where φψ: "meta_adjunction C D F G φ ψ" using assms adjoint_functors_def by blast obtain φ' ψ' where φ'ψ': "meta_adjunction C D F G' φ' ψ'" using assms adjoint_functors_def by blast interpret Adj: meta_adjunction C D F G φ ψ using φψ by auto interpret S: replete_setcat . interpret Adj: adjunction C D S.comp S.setp Adj.φC Adj.φD F G φ ψ Adj.η Adj.ε Adj.Φ Adj.Ψ using Adj.induces_adjunction by auto interpret Adj': meta_adjunction C D F G' φ' ψ' using φ'ψ' by auto interpret Adj': adjunction C D S.comp S.setp Adj'.φC Adj'.φD F G' φ' ψ' Adj'.η Adj'.ε Adj'.Φ Adj'.Ψ using Adj'.induces_adjunction by auto write C (infixr ‹⋅C› 55) write D (infixr ‹⋅D› 55) write Adj.C.in_hom (‹«_ : _ →C _¬›) write Adj.D.in_hom (‹«_ : _ →D _¬›) let ?τo = "λa. G' (Adj.ε a) ⋅D Adj'.η (G a)" interpret τ: transformation_by_components C D G G' ?τo proof show "∧a. Adj.C.ide a ==> «G' (Adj.ε a) ⋅D Adj'.η (G a) : G a →D G' a¬" by fastforce show "∧f. Adj.C.arr f ==> (G' (Adj.ε (Adj.C.cod f)) ⋅D Adj'.η (G (Adj.C.cod f))) ⋅D G f = G' f ⋅D G' (Adj.ε (Adj.C.dom f)) ⋅D Adj'.η (G (Adj.C.dom f))" proof - fix f assume f: "Adj.C.arr f" let ?x = "Adj.C.dom f" let ?x' = "Adj.C.cod f" have "(G' (Adj.ε (Adj.C.cod f)) ⋅D Adj'.η (G (Adj.C.cod f))) ⋅D G f = G' (Adj.ε (Adj.C.cod f) ⋅C F (G f)) ⋅D Adj'.η (G (Adj.C.dom f))" using f Adj'.η.naturality [of "G f"] Adj.D.comp_assoc by simp also have "... = G' (f ⋅C Adj.ε (Adj.C.dom f)) ⋅D Adj'.η (G (Adj.C.dom f))" using f Adj.ε.naturality by simp also have "... = G' f ⋅D G' (Adj.ε (Adj.C.dom f)) ⋅D Adj'.η (G (Adj.C.dom f))" using f Adj.D.comp_assoc by simp finally show "(G' (Adj.ε (Adj.C.cod f)) ⋅D Adj'.η (G (Adj.C.cod f))) ⋅D G f = G' f ⋅D G' (Adj.ε (Adj.C.dom f)) ⋅D Adj'.η (G (Adj.C.dom f))" by auto qed qed interpret natural_isomorphism C D G G' τ.map proof fix a assume a: "Adj.C.ide a" show "Adj.D.iso (τ.map a)" proof show "Adj.D.inverse_arrows (τ.map a) (φ (G' a) (Adj'.ε a))" proof text‹ The proof that the two composites are identities is a modest diagram chase. This is a good example of the inference rules for the ‹category›, ‹functor›, and ‹natural_transformation› locales in action. Isabelle is able to use the single hypothesis that ‹a› is an identity to implicitly fill in all the details that the various quantities are in fact arrow and that the indicated composites are all well-defined, as well as to apply associativity of composition. In most cases, this is done by auto or simp witho even mentioning any of the rules that are used. $\xymatrix{ {G' a} \ar[dd]_{\eta'(G'a)} \ar[rr]^{\tau' a} \ar[dr]_{\eta(G'a)} && {G a} \ar[rr]^{\tau a} \ar[dr]_{\eta'(Ga)} && {G' a} \\ & {GFG'a} \rrtwocell\omit{\omit(2)} \ar[ur]_{G(\epsilon' a)} && {G'FGa} \drtwocell\omit{\omit(3)} \ar[ur]_{G'(\epsilon a)} & \\ {G'FG'a} \urtwocell\omit{\omit(1)} \ar[rr]_{G'F\eta(G'a)} \ar@/_8ex/[rrrr]_{G'FG && {G'FGFG'a} \dtwocell\omit{\omit(4)} \ar[ru]_{G'FG(\epsilon' a)} \ar[rr]_{G'(\ep && {G'FG'a} \ar[uu]_{G'(\epsilon' a)} \\ &&&& $$ show "Adj.D.ide (τ.map a ⋅D φ (G' a) (Adj'.ε a))" proof - have "τ.map a ⋅D φ (G' a) (Adj'.ε a) = G' a" proof - have "τ.map a ⋅D φ (G' a) (Adj'.ε a) = G' (Adj.ε a) ⋅D (Adj'.η (G a) ⋅D G (Adj'.ε a)) ⋅D Adj.η (G' a)" using a τ.map_simp_ide Adj.φ_in_terms_of_η Adj'.φ_in_terms_of_η Adj'.ε.preserves_hom [of a a a] Adj.C.ide_in_hom Adj.D.comp_assoc Adj.ε_def Adj.η_def by simp also have "... = G' (Adj.ε a) ⋅D (G' (F (G (Adj'.ε a))) ⋅D Adj'.η (G (F (G' a)))) ⋅D Adj.η (G' a)" using a Adj'.η.naturality [of "G (Adj'.ε a)"] by auto also have "... = (G' (Adj.ε a) ⋅D G' (F (G (Adj'.ε a)))) ⋅D G' (F (Adj.η (G' a))) ⋅D Adj'.η (G' a)" using a Adj'.η.naturality [of "Adj.η (G' a)"] Adj.D.comp_assoc by auto also have "... = G' (Adj'.ε a) ⋅D (G' (Adj.ε (F (G' a))) ⋅D G' (F (Adj.η (G' a)))) ⋅D Adj'.η (G' a)" proof - have "G' (Adj.ε a) ⋅D G' (F (G (Adj'.ε a))) = G' (Adj'.ε a) ⋅D G' (Adj.ε (F (G' a)))" proof - have "G' (Adj.ε a ⋅C F (G (Adj'.ε a))) = G' (Adj'.ε a ⋅C Adj.ε (F (G' a)))" using a Adj.ε.naturality [of "Adj'.ε a"] by auto thus ?thesis using a by force qed thus ?thesis using Adj.D.comp_assoc by auto qed also have "... = G' (Adj'.ε a) ⋅D Adj'.η (G' a)" proof - have "G' (Adj.ε (F (G' a))) ⋅D G' (F (Adj.η (G' a))) = G' (F (G' a))" proof - have "G' (Adj.ε (F (G' a))) ⋅D G' (F (Adj.η (G' a))) = G' (Adj.εFoFη.map (G' a))" using a Adj.εFoFη.map_simp_1 by auto moreover have "Adj.εFoFη.map (G' a) = F (G' a)" using a by (simp add: Adj.ηε.triangle_F) ultimately show ?thesis by auto qed thus ?thesis using a Adj.D.comp_cod_arr [of "Adj'.η (G' a)"] by auto qed also have "... = G' a" using a Adj'.ηε.triangle_G Adj'.GεoηG.map_simp_1 [of a] by auto finally show ?thesis by auto qed thus ?thesis using a by simp qed show "Adj.D.ide (φ (G' a) (Adj'.ε a) ⋅D τ.map a)" proof - have "φ (G' a) (Adj'.ε a) ⋅D τ.map a = G a" proof - have "φ (G' a) (Adj'.ε a) ⋅D τ.map a = G (Adj'.ε a) ⋅D (Adj.η (G' a) ⋅D G' (Adj.ε a)) ⋅D Adj'.η (G a)" using a τ.map_simp_ide Adj.φ_in_terms_of_η Adj'.ε.preserves_hom [of a a a] Adj.C.ide_in_hom Adj.D.comp_assoc Adj.η_def by auto also have "... = G (Adj'.ε a) ⋅D (G (F (G' (Adj.ε a))) ⋅D Adj.η (G' (F (G a)))) ⋅D Adj'.η (G a)" using a Adj.η.naturality [of "G' (Adj.ε a)"] by auto also have "... = (G (Adj'.ε a) ⋅D G (F (G' (Adj.ε a)))) ⋅D G (F (Adj'.η (G a))) ⋅D Adj.η (G a)" using a Adj.η.naturality [of "Adj'.η (G a)"] Adj.D.comp_assoc by auto also have "... = G (Adj.ε a) ⋅D (G (Adj'.ε (F (G a))) ⋅D G (F (Adj'.η (G a)))) ⋅D Adj.η (G a)" proof - have "G (Adj'.ε a) ⋅D G (F (G' (Adj.ε a))) = G (Adj.ε a) ⋅D G (Adj'.ε (F (G a)))" proof - have "G (Adj'.ε a ⋅C F (G' (Adj.ε a))) = G (Adj.ε a ⋅C Adj'.ε (F (G a)))" using a Adj'.ε.naturality [of "Adj.ε a"] by auto thus ?thesis using a by force qed thus ?thesis using Adj.D.comp_assoc by auto qed also have "... = G (Adj.ε a) ⋅D Adj.η (G a)" proof - have "G (Adj'.ε (F (G a))) ⋅D G (F (Adj'.η (G a))) = G (F (G a))" proof - have "G (Adj'.ε (F (G a))) ⋅D G (F (Adj'.η (G a))) = G (Adj'.εFoFη.map (G a))" using a Adj'.εFoFη.map_simp_1 [of "G a"] by auto moreover have "Adj'.εFoFη.map (G a) = F (G a)" using a by (simp add: Adj'.ηε.triangle_F) ultimately show ?thesis by auto qed thus ?thesis using a Adj.D.comp_cod_arr by auto qed also have "... = G a" using a Adj.ηε.triangle_G Adj.GεoηG.map_simp_1 [of a] by auto finally show ?thesis by auto qed thus ?thesis using a by auto qed qed qed qed have "natural_isomorphism C D G G' τ.map" .. thus "naturally_isomorphic C D G G'" using naturally_isomorphic_def by blast qed end
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.976Bemerkung: ¤*Bot Zugriff |
|
||||||||||||||
2026-06-12