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