Theory InternalAdjunction
section "Adjunctions in a Bicategory"
theory InternalAdjunction
imports CanonicalIsos Strictness
begin
text ‹
An \emph{internal adjunction} in a bicategory is a four-tuple ‹(f, g, η, ε)›,
where ‹f› and ‹g› are antiparallel 1-cells and ‹«η : src f ⇒ g ⋆ f»› and
‹«ε : f ⋆ g ⇒ src g»› are 2-cells, such that the familiar ``triangle''
(or ``zig-zag'') identities are satisfied. We state the triangle identities
in two equivalent forms, each of which is convenient in certain situations.
›
locale adjunction_in_bicategory =
adjunction_data_in_bicategory +
assumes triangle_left: "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
and triangle_right: "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
begin
lemma triangle_left':
shows "𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] = f"
using triangle_left triangle_equiv_form by simp
lemma triangle_right':
shows "𝗋[g] ⋅ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g] = g"
using triangle_right triangle_equiv_form by simp
end
text ‹
Internal adjunctions have a number of properties, which we now develop,
that generalize those of ordinary adjunctions involving functors and
natural transformations.
›
context bicategory
begin
lemma adjunction_unit_determines_counit:
assumes "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε"
and "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε'"
shows "ε = ε'"
proof -
interpret E: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms(1) by auto
interpret E': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
using assms(2) by auto
text ‹
Note that since we want to prove the the result for an arbitrary bicategory,
not just in for a strict bicategory, the calculation is a little more involved
than one might expect from a treatment that suppresses canonical isomorphisms.
›
have "ε = ε ⋅ (f ⋆ 𝗋[g] ⋅ (g ⋆ ε') ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ 𝗅⇧-⇧1[g])"
using E'.triangle_right' comp_arr_dom by simp
also have "... = ε ⋅ (f ⋆ 𝗋[g]) ⋅ (f ⋆ g ⋆ ε') ⋅ (f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar whisker_left by simp
also have "... = ε ⋅ ((f ⋆ 𝗋[g]) ⋅ (f ⋆ g ⋆ ε')) ⋅ (f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using comp_assoc by simp
also have "... = ε ⋅ 𝗋[f ⋆ g] ⋅ (𝖺⇧-⇧1[f, g, src g] ⋅ (f ⋆ g ⋆ ε')) ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
proof -
have "f ⋆ 𝗋[g] = 𝗋[f ⋆ g] ⋅ 𝖺⇧-⇧1[f, g, src g]"
using E.antipar(1) runit_hcomp(3) by auto
thus ?thesis
using comp_assoc by simp
qed
also have "... = (ε ⋅ 𝗋[f ⋆ g]) ⋅ ((f ⋆ g) ⋆ ε') ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar E'.counit_in_hom assoc'_naturality [of f g ε'] comp_assoc by simp
also have "... = 𝗋[trg f] ⋅ ((ε ⋆ trg f) ⋅ ((f ⋆ g) ⋆ ε')) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar E.counit_in_hom runit_naturality [of ε] comp_assoc by simp
also have "... = (𝗅[src g] ⋅ (src g ⋆ ε')) ⋅ (ε ⋆ f ⋆ g) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
proof -
have "(ε ⋆ trg f) ⋅ ((f ⋆ g) ⋆ ε') = (src g ⋆ ε') ⋅ (ε ⋆ f ⋆ g)"
using E.antipar interchange E.counit_in_hom comp_arr_dom comp_cod_arr
by (metis E'.counit_simps(1-3) E.counit_simps(1-3))
thus ?thesis
using E.antipar comp_assoc unitor_coincidence by simp
qed
also have "... = ε' ⋅ 𝗅[f ⋆ g] ⋅ (ε ⋆ f ⋆ g) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
proof -
have "𝗅[src g] ⋅ (src g ⋆ ε') = ε' ⋅ 𝗅[f ⋆ g]"
using E.antipar lunit_naturality [of ε'] by simp
thus ?thesis
using comp_assoc by simp
qed
also have "... = ε' ⋅ (𝗅[f] ⋆ g) ⋅ (𝖺⇧-⇧1[trg f, f, g] ⋅ (ε ⋆ f ⋆ g)) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g]) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar lunit_hcomp comp_assoc by simp
also have "... = ε' ⋅ (𝗅[f] ⋆ g) ⋅ ((ε ⋆ f) ⋆ g) ⋅ (𝖺⇧-⇧1[f ⋆ g, f, g] ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅
(f ⋆ 𝖺[g, f, g])) ⋅ (f ⋆ η ⋆ g) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar assoc'_naturality [of ε f g] comp_assoc by simp
also have "... = ε' ⋅ (𝗅[f] ⋆ g) ⋅ ((ε ⋆ f) ⋆ g) ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ g) ⋅
(𝖺⇧-⇧1[f, g ⋆ f, g] ⋅ (f ⋆ η ⋆ g)) ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
proof -
have "𝖺⇧-⇧1[f ⋆ g, f, g] ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g] ⋅ (f ⋆ 𝖺[g, f, g]) =
(𝖺⇧-⇧1[f, g, f] ⋆ g) ⋅ 𝖺⇧-⇧1[f, g ⋆ f, g]"
using E.antipar iso_assoc' pentagon' comp_assoc
invert_side_of_triangle(2)
[of "𝖺⇧-⇧1[f ⋆ g, f, g] ⋅ 𝖺⇧-⇧1[f, g, f ⋆ g]"
"(𝖺⇧-⇧1[f, g, f] ⋆ g) ⋅ 𝖺⇧-⇧1[f, g ⋆ f, g]" "f ⋆ 𝖺⇧-⇧1[g, f, g]"]
by simp
thus ?thesis
using comp_assoc by simp
qed
also have "... = ε' ⋅ (𝗅[f] ⋆ g) ⋅ ((ε ⋆ f) ⋆ g) ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ g) ⋅
((f ⋆ η) ⋆ g) ⋅ 𝖺⇧-⇧1[f, trg g, g] ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar assoc'_naturality [of f η g] comp_assoc by simp
also have "... = ε' ⋅ (𝗅[f] ⋆ g) ⋅ ((ε ⋆ f) ⋆ g) ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ g) ⋅
((f ⋆ η) ⋆ g) ⋅ (𝗋⇧-⇧1[f] ⋆ g)"
proof -
have "𝖺⇧-⇧1[f, trg g, g] ⋅ (f ⋆ 𝗅⇧-⇧1[g]) = 𝗋⇧-⇧1[f] ⋆ g"
proof -
have "𝗋⇧-⇧1[f] ⋆ g = inv (𝗋[f] ⋆ g)"
using E.antipar by simp
also have "... = inv ((f ⋆ 𝗅[g]) ⋅ 𝖺[f, trg g, g])"
using E.antipar by (simp add: triangle)
also have "... = 𝖺⇧-⇧1[f, trg g, g] ⋅ (f ⋆ 𝗅⇧-⇧1[g])"
using E.antipar inv_comp by simp
finally show ?thesis by simp
qed
thus ?thesis by simp
qed
also have "... = ε' ⋅ (𝗅[f] ⋅ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ 𝗋⇧-⇧1[f] ⋆ g)"
using E.antipar whisker_right by simp
also have "... = ε'"
using E.triangle_left' comp_arr_dom by simp
finally show ?thesis by simp
qed
end
subsection "Adjoint Transpose"
context adjunction_in_bicategory
begin
interpretation E: self_evaluation_map V H 𝖺 𝗂 src trg ..
notation E.eval ("⦃_⦄")
text ‹
Just as for an ordinary adjunction between categories, an adjunction in a bicategory
determines bijections between hom-sets. There are two versions of this relationship:
depending on whether the transposition is occurring on the left (\emph{i.e.}~``output'')
side or the right (\emph{i.e.}~``input'') side.
›
definition trnl⇩η
where "trnl⇩η v μ ≡ (g ⋆ μ) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v]"
definition trnl⇩ε
where "trnl⇩ε u ν ≡ 𝗅[u] ⋅ (ε ⋆ u) ⋅ 𝖺⇧-⇧1[f, g, u] ⋅ (f ⋆ ν)"
lemma adjoint_transpose_left:
assumes "ide u" and "ide v" and "src f = trg v" and "src g = trg u"
shows "trnl⇩η v ∈ hom (f ⋆ v) u → hom v (g ⋆ u)"
and "trnl⇩ε u ∈ hom v (g ⋆ u) → hom (f ⋆ v) u"
and "«μ : f ⋆ v ⇒ u» ⟹ trnl⇩ε u (trnl⇩η v μ) = μ"
and "«ν : v ⇒ g ⋆ u» ⟹ trnl⇩η v (trnl⇩ε u ν) = ν"
and "bij_betw (trnl⇩η v) (hom (f ⋆ v) u) (hom v (g ⋆ u))"
and "bij_betw (trnl⇩ε u) (hom v (g ⋆ u)) (hom (f ⋆ v) u)"
proof -
show A: "trnl⇩η v ∈ hom (f ⋆ v) u → hom v (g ⋆ u)"
using assms antipar trnl⇩η_def by fastforce
show B: "trnl⇩ε u ∈ hom v (g ⋆ u) → hom (f ⋆ v) u"
using assms antipar trnl⇩ε_def by fastforce
show C: "⋀μ. «μ : f ⋆ v ⇒ u» ⟹ trnl⇩ε u (trnl⇩η v μ) = μ"
proof -
fix μ
assume μ: "«μ : f ⋆ v ⇒ u»"
have "trnl⇩ε u (trnl⇩η v μ) =
𝗅[u] ⋅ (ε ⋆ u) ⋅ 𝖺⇧-⇧1[f, g, u] ⋅ (f ⋆ (g ⋆ μ) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v])"
using trnl⇩η_def trnl⇩ε_def by simp
also have "... = 𝗅[u] ⋅ (ε ⋆ u) ⋅ (𝖺⇧-⇧1[f, g, u] ⋅ (f ⋆ g ⋆ μ)) ⋅ (f ⋆ 𝖺[g, f, v]) ⋅
(f ⋆ η ⋆ v) ⋅ (f ⋆ 𝗅⇧-⇧1[v])"
using assms μ antipar whisker_left comp_assoc by auto
also have "... = 𝗅[u] ⋅ ((ε ⋆ u) ⋅ ((f ⋆ g) ⋆ μ)) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) ⋅
(f ⋆ η ⋆ v) ⋅ (f ⋆ 𝗅⇧-⇧1[v])"
using assms μ antipar assoc'_naturality [of f g μ] comp_assoc by fastforce
also have "... = 𝗅[u] ⋅ (trg u ⋆ μ) ⋅
(ε ⋆ f ⋆ v) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) ⋅
(f ⋆ η ⋆ v) ⋅ (f ⋆ 𝗅⇧-⇧1[v])"
proof -
have "(ε ⋆ u) ⋅ ((f ⋆ g) ⋆ μ) = (trg u ⋆ μ) ⋅ (ε ⋆ f ⋆ v)"
using assms μ antipar comp_cod_arr comp_arr_dom
interchange [of "trg u" ε μ "f ⋆ v"] interchange [of ε "f ⋆ g" u μ]
by auto
thus ?thesis
using comp_assoc by simp
qed
also have "... = 𝗅[u] ⋅ (trg u ⋆ μ) ⋅ 𝖺[trg f, f, v] ⋅
((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋆ v) ⋅
𝖺⇧-⇧1[f, trg v, v] ⋅ (f ⋆ 𝗅⇧-⇧1[v])"
proof -
have 1: "(ε ⋆ f ⋆ v) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) ⋅ (f ⋆ η ⋆ v) =
𝖺[trg f, f, v] ⋅ ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋆ v) ⋅ 𝖺⇧-⇧1[f, trg v, v]"
proof -
have "(ε ⋆ f ⋆ v) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) ⋅ (f ⋆ η ⋆ v) =
(ε ⋆ f ⋆ v) ⋅
𝖺[f ⋆ g, f, v] ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ 𝖺⇧-⇧1[f, g ⋆ f, v] ⋅
(f ⋆ η ⋆ v)"
proof -
have "(ε ⋆ f ⋆ v) ⋅ 𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) ⋅ (f ⋆ η ⋆ v) =
(ε ⋆ f ⋆ v) ⋅ (𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v])) ⋅ (f ⋆ η ⋆ v)"
using comp_assoc by simp
also have "... = (ε ⋆ f ⋆ v) ⋅
𝖺[f ⋆ g, f, v] ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ 𝖺⇧-⇧1[f, g ⋆ f, v] ⋅
(f ⋆ η ⋆ v)"
proof -
have "𝖺⇧-⇧1[f, g, f ⋆ v] ⋅ (f ⋆ 𝖺[g, f, v]) =
𝖺[f ⋆ g, f, v] ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ 𝖺⇧-⇧1[f, g ⋆ f, v]"
using assms antipar canI_associator_0 whisker_can_left_0 whisker_can_right_0
canI_associator_hcomp(1-3)
by simp
thus ?thesis
using comp_assoc by simp
qed
finally show ?thesis by blast
qed
also have "... = ((ε ⋆ f ⋆ v) ⋅ 𝖺[f ⋆ g, f, v]) ⋅
(𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ ((f ⋆ η) ⋆ v) ⋅
𝖺⇧-⇧1[f, trg v, v]"
using assms μ antipar assoc'_naturality [of f η v] comp_assoc by simp
also have "... = (𝖺[trg f, f, v] ⋅ ((ε ⋆ f) ⋆ v)) ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ ((f ⋆ η) ⋆ v) ⋅
𝖺⇧-⇧1[f, trg v, v]"
using assms μ antipar assoc_naturality [of ε f v] by simp
also have "... = 𝖺[trg f, f, v] ⋅
(((ε ⋆ f) ⋆ v) ⋅ (𝖺⇧-⇧1[f, g, f] ⋆ v) ⋅ ((f ⋆ η) ⋆ v)) ⋅
𝖺⇧-⇧1[f, trg v, v]"
using comp_assoc by simp
also have "... = 𝖺[trg f, f, v] ⋅ ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋆ v) ⋅ 𝖺⇧-⇧1[f, trg v, v]"
using assms μ antipar whisker_right by simp
finally show ?thesis by simp
qed
show ?thesis
using 1 comp_assoc by metis
qed
also have "... = 𝗅[u] ⋅ (trg u ⋆ μ) ⋅
𝖺[trg f, f, v] ⋅ (𝗅⇧-⇧1[f] ⋅ 𝗋[f] ⋆ v) ⋅ 𝖺⇧-⇧1[f, trg v, v] ⋅ (f ⋆ 𝗅⇧-⇧1[v])"
using assms μ antipar triangle_left by simp
also have "... = 𝗅[u] ⋅ (trg u ⋆ μ) ⋅ can (❙⟨trg u❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨v❙⟩) (❙⟨f❙⟩ ❙⋆ ❙⟨v❙⟩)"
using assms μ antipar canI_unitor_0 canI_associator_1
canI_associator_1(1-2) [of f v] whisker_can_right_0 whisker_can_left_0
by simp
also have "... = 𝗅[u] ⋅ (trg u ⋆ μ) ⋅ 𝗅⇧-⇧1[f ⋆ v]"
unfolding can_def using assms antipar comp_arr_dom comp_cod_arr 𝔩_ide_simp
by simp
also have "... = (𝗅[u] ⋅ 𝗅⇧-⇧1[u]) ⋅ μ"
using assms μ lunit'_naturality [of μ] comp_assoc by auto
also have "... = μ"
using assms μ comp_cod_arr iso_lunit comp_arr_inv inv_is_inverse by auto
finally show "trnl⇩ε u (trnl⇩η v μ) = μ" by simp
qed
show D: "⋀ν. «ν : v ⇒ g ⋆ u» ⟹ trnl⇩η v (trnl⇩ε u ν) = ν"
proof -
fix ν
assume ν: "«ν : v ⇒ g ⋆ u»"
have "trnl⇩η v (trnl⇩ε u ν) =
(g ⋆ 𝗅[u] ⋅ (ε ⋆ u) ⋅ 𝖺⇧-⇧1[f, g, u] ⋅ (f ⋆ ν)) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v]"
using trnl⇩η_def trnl⇩ε_def by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ (g ⋆ f ⋆ ν) ⋅
𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v]"
using assms ν antipar interchange [of g "g ⋅ g ⋅ g"] comp_assoc by auto
also have "... = ((g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅
𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u)) ⋅ (trg v ⋆ ν) ⋅ 𝗅⇧-⇧1[v]"
proof -
have "(g ⋆ f ⋆ ν) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v] =
𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u) ⋅ (trg v ⋆ ν) ⋅ 𝗅⇧-⇧1[v]"
proof -
have "(g ⋆ f ⋆ ν) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v] =
𝖺[g, f, g ⋆ u] ⋅ ((g ⋆ f) ⋆ ν) ⋅ (η ⋆ v) ⋅ 𝗅⇧-⇧1[v]"
proof -
have "(g ⋆ f ⋆ ν) ⋅ 𝖺[g, f, v] = 𝖺[g, f, g ⋆ u] ⋅ ((g ⋆ f) ⋆ ν)"
using assms ν antipar assoc_naturality [of g f ν] by auto
thus ?thesis
using assms comp_assoc by metis
qed
also have "... = 𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u) ⋅ (trg v ⋆ ν) ⋅ 𝗅⇧-⇧1[v]"
proof -
have "((g ⋆ f) ⋆ ν) ⋅ (η ⋆ v) = (η ⋆ g ⋆ u) ⋅ (trg v ⋆ ν)"
using assms ν antipar comp_arr_dom comp_cod_arr
interchange [of "g ⋆ f" η ν v] interchange [of η "trg v" "g ⋆ u" ν]
by auto
thus ?thesis
using comp_assoc by metis
qed
finally show ?thesis by blast
qed
thus ?thesis using comp_assoc by simp
qed
also have "... = 𝗅[g ⋆ u] ⋅ (trg v ⋆ ν) ⋅ 𝗅⇧-⇧1[v]"
proof -
have "(g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u) =
𝗅[g ⋆ u]"
proof -
have "(g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u) =
(g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅
((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋆ u) ⋅
𝖺⇧-⇧1[trg v, g, u]"
proof -
have "(g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ (η ⋆ g ⋆ u) =
(g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅
((η ⋆ g ⋆ u) ⋅ 𝖺[trg v, g, u]) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
using assms antipar comp_arr_dom comp_assoc comp_assoc_assoc'(1) by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅
(𝖺[g ⋆ f, g, u] ⋅ ((η ⋆ g) ⋆ u)) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
using assms antipar assoc_naturality [of η g u] by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ (g ⋆ ε ⋆ u) ⋅
((g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u]) ⋅
((η ⋆ g) ⋆ u) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
using comp_assoc by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ ((𝖺[g, trg u, u] ⋅ 𝖺⇧-⇧1[g, trg u, u]) ⋅ (g ⋆ ε ⋆ u)) ⋅
((g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u]) ⋅
((η ⋆ g) ⋆ u) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
proof -
have "(𝖺[g, trg u, u] ⋅ 𝖺⇧-⇧1[g, trg u, u]) ⋅ (g ⋆ ε ⋆ u) = g ⋆ ε ⋆ u"
using assms antipar comp_cod_arr comp_assoc_assoc'(1) by simp
thus ?thesis
using comp_assoc by simp
qed
also have "... = (g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅ (𝖺⇧-⇧1[g, trg u, u] ⋅ (g ⋆ ε ⋆ u)) ⋅
(g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u] ⋅
((η ⋆ g) ⋆ u) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
using comp_assoc by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅ (((g ⋆ ε) ⋆ u) ⋅ (𝖺⇧-⇧1[g, f ⋆ g, u] ⋅
(g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u]) ⋅
((η ⋆ g) ⋆ u)) ⋅ 𝖺⇧-⇧1[trg v, g, u]"
using assms antipar assoc'_naturality [of g ε u] comp_assoc by simp
also have "... = (g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅
((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋆ u) ⋅
𝖺⇧-⇧1[trg v, g, u]"
proof -
have "𝖺⇧-⇧1[g, f ⋆ g, u] ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u] =
𝖺[g, f, g] ⋆ u"
using assms antipar canI_associator_0 whisker_can_left_0 whisker_can_right_0
canI_associator_hcomp
by simp
hence "((g ⋆ ε) ⋆ u) ⋅
(𝖺⇧-⇧1[g, f ⋆ g, u] ⋅ (g ⋆ 𝖺⇧-⇧1[f, g, u]) ⋅ 𝖺[g, f, g ⋆ u] ⋅ 𝖺[g ⋆ f, g, u]) ⋅
((η ⋆ g) ⋆ u) =
(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋆ u"
using assms antipar whisker_right by simp
thus ?thesis by simp
qed
finally show ?thesis by blast
qed
also have "... = (g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅ (𝗋⇧-⇧1[g] ⋅ 𝗅[g] ⋆ u) ⋅ 𝖺⇧-⇧1[trg g, g, u]"
using assms antipar triangle_right by simp
also have "... = can (❙⟨g❙⟩ ❙⋆ ❙⟨u❙⟩) (❙⟨trg g❙⟩⇩0 ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨u❙⟩)"
proof -
have "(g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅ (𝗋⇧-⇧1[g] ⋅ 𝗅[g] ⋆ u) ⋅ 𝖺⇧-⇧1[trg g, g, u] =
((g ⋆ 𝗅[u]) ⋅ 𝖺[g, trg u, u] ⋅ (𝗋⇧-⇧1[g] ⋅ 𝗅[g] ⋆ u) ⋅ 𝖺⇧-⇧1[trg g, g, u])"
using comp_assoc by simp
moreover have "... = can (❙⟨g❙⟩ ❙⋆ ❙⟨u❙⟩) (❙⟨trg g❙⟩⇩0 ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨u❙⟩)"
using assms antipar canI_unitor_0 canI_associator_1 [of g u] inv_can
whisker_can_left_0 whisker_can_right_0
by simp
ultimately show ?thesis by simp
qed
also have "... = 𝗅[g ⋆ u]"
unfolding can_def using assms comp_arr_dom comp_cod_arr 𝔩_ide_simp by simp
finally show ?thesis by simp
qed
thus ?thesis by simp
qed
also have "... = (𝗅[g ⋆ u] ⋅ 𝗅⇧-⇧1[g ⋆ u]) ⋅ ν"
using assms ν lunit'_naturality comp_assoc by auto
also have "... = ν"
using assms ν comp_cod_arr iso_lunit comp_arr_inv inv_is_inverse by auto
finally show "trnl⇩η v (trnl⇩ε u ν) = ν" by simp
qed
show "bij_betw (trnl⇩η v) (hom (f ⋆ v) u) (hom v (g ⋆ u))"
using A B C D by (intro bij_betwI) auto
show "bij_betw (trnl⇩ε u) (hom v (g ⋆ u)) (hom (f ⋆ v) u)"
using A B C D by (intro bij_betwI) auto
qed
lemma trnl⇩ε_comp:
assumes "ide u" and "seq μ ν" and "src f = trg μ"
shows "trnl⇩ε u (μ ⋅ ν) = trnl⇩ε u μ ⋅ (f ⋆ ν)"
using assms trnl⇩ε_def whisker_left [of f μ ν] comp_assoc by auto
definition trnr⇩η
where "trnr⇩η v μ ≡ (μ ⋆ f) ⋅ 𝖺⇧-⇧1[v, g, f] ⋅ (v ⋆ η) ⋅ 𝗋⇧-⇧1[v]"
definition trnr⇩ε
where "trnr⇩ε u ν ≡ 𝗋[u] ⋅ (u ⋆ ε) ⋅ 𝖺[u, f, g] ⋅ (ν ⋆ g)"
lemma adjoint_transpose_right:
assumes "ide u" and "ide v" and "src v = trg g" and "src u = trg f"
shows "trnr⇩η v ∈ hom (v ⋆ g) u → hom v (u ⋆ f)"
and "trnr⇩ε u ∈ hom v (u ⋆ f) → hom (v ⋆ g) u"
and "«μ : v ⋆ g ⇒ u» ⟹ trnr⇩ε u (trnr⇩η v μ) = μ"
and "«ν : v ⇒ u ⋆ f» ⟹ trnr⇩η v (trnr⇩ε u ν) = ν"
and "bij_betw (trnr⇩η v) (hom (v ⋆ g) u) (hom v (u ⋆ f))"
and "bij_betw (trnr⇩ε u) (hom v (u ⋆ f)) (hom (v ⋆ g) u)"
proof -
show A: "trnr⇩η v ∈ hom (v ⋆ g) u → hom v (u ⋆ f)"
using assms antipar trnr⇩η_def by fastforce
show B: "trnr⇩ε u ∈ hom v (u ⋆ f) → hom (v ⋆ g) u"
using assms antipar trnr⇩ε_def by fastforce
show C: "⋀μ. «μ : v ⋆ g ⇒ u» ⟹ trnr⇩ε u (trnr⇩η v μ) = μ"
proof -
fix μ
assume μ: "«μ : v ⋆ g ⇒ u»"
have "trnr⇩ε u (trnr⇩η v μ) =
𝗋[u] ⋅ (u ⋆ ε) ⋅ 𝖺[u, f, g] ⋅ ((μ ⋆ f) ⋅ 𝖺⇧-⇧1[v, g, f] ⋅ (v ⋆ η) ⋅ 𝗋⇧-⇧1[v] ⋆ g)"
unfolding trnr⇩ε_def trnr⇩η_def by simp
also have "... = 𝗋[u] ⋅ (u ⋆ ε) ⋅ (𝖺[u, f, g] ⋅ ((μ ⋆ f) ⋆ g)) ⋅
(𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
using assms μ antipar whisker_right comp_assoc by auto
also have "... = 𝗋[u] ⋅ (u ⋆ ε) ⋅ ((μ ⋆ f ⋆ g) ⋅ 𝖺[v ⋆ g, f, g]) ⋅
(𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
using assms μ antipar assoc_naturality [of μ f g] by auto
also have "... = 𝗋[u] ⋅ ((u ⋆ ε) ⋅ (μ ⋆ f ⋆ g)) ⋅ 𝖺[v ⋆ g, f, g] ⋅
(𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
using comp_assoc by auto
also have "... = 𝗋[u] ⋅ (μ ⋆ src u) ⋅ ((v ⋆ g) ⋆ ε) ⋅ 𝖺[v ⋆ g, f, g] ⋅
(𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
proof -
have "(u ⋆ ε) ⋅ (μ ⋆ f ⋆ g) = (μ ⋆ src u) ⋅ ((v ⋆ g) ⋆ ε)"
using assms μ antipar comp_arr_dom comp_cod_arr
interchange [of μ "v ⋆ g" "src u" ε] interchange [of u μ ε "f ⋆ g"]
by auto
thus ?thesis
using comp_assoc by simp
qed
also have "... = 𝗋[u] ⋅ (μ ⋆ src u) ⋅
(((v ⋆ g) ⋆ ε) ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g)) ⋅
(𝗋⇧-⇧1[v] ⋆ g)"
using comp_assoc by simp
also have "... = 𝗋[u] ⋅ (μ ⋆ src u) ⋅
(𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅
𝖺[v, src v, g]) ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
proof -
have "((v ⋆ g) ⋆ ε) ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) =
𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅ 𝖺[v, src v, g]"
proof -
have "((v ⋆ g) ⋆ ε) ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g) =
((𝖺⇧-⇧1[v, g, src u] ⋅ 𝖺[v, g, src u]) ⋅ ((v ⋆ g) ⋆ ε)) ⋅
𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g)"
proof -
have "arr v ∧ dom v = v ∧ cod v = v"
using assms(2) ide_char by blast
moreover have "arr g ∧ dom g = g ∧ cod g = g"
using ide_right ide_char by blast
ultimately show ?thesis
by (metis (no_types) antipar(2) assms(3-4) assoc_naturality
counit_simps(1,3,5) hcomp_reassoc(1) comp_assoc)
qed
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅ (𝖺[v, g, src u] ⋅ ((v ⋆ g) ⋆ ε)) ⋅
𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ ((v ⋆ η) ⋆ g)"
using comp_assoc by simp
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅ ((v ⋆ g ⋆ ε) ⋅ 𝖺[v, g, f ⋆ g]) ⋅
𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅
(𝖺⇧-⇧1[v, g ⋆ f, g] ⋅ 𝖺[v, g ⋆ f, g]) ⋅ ((v ⋆ η) ⋆ g)"
proof -
have "𝖺[v, g, src u] ⋅ ((v ⋆ g) ⋆ ε) = (v ⋆ g ⋆ ε) ⋅ 𝖺[v, g, f ⋆ g]"
using assms antipar assoc_naturality [of v g ε] by simp
moreover have "(𝖺⇧-⇧1[v, g ⋆ f, g] ⋅ 𝖺[v, g ⋆ f, g]) ⋅ ((v ⋆ η) ⋆ g) = (v ⋆ η) ⋆ g"
using assms antipar comp_cod_arr comp_assoc_assoc'(2) by simp
ultimately show ?thesis by simp
qed
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ g ⋆ ε) ⋅
𝖺[v, g, f ⋆ g] ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅
𝖺⇧-⇧1[v, g ⋆ f, g] ⋅ 𝖺[v, g ⋆ f, g] ⋅ ((v ⋆ η) ⋆ g)"
using comp_assoc by simp
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅ ((v ⋆ g ⋆ ε) ⋅
(𝖺[v, g, f ⋆ g] ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅
𝖺⇧-⇧1[v, g ⋆ f, g]) ⋅ (v ⋆ η ⋆ g)) ⋅ 𝖺[v, src v, g]"
using assms antipar assoc_naturality [of v η g] comp_assoc by simp
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅
((v ⋆ g ⋆ ε) ⋅ (v ⋆ 𝖺[g, f, g]) ⋅ (v ⋆ η ⋆ g)) ⋅
𝖺[v, src v, g]"
proof -
have "𝖺[v, g, f ⋆ g] ⋅ 𝖺[v ⋆ g, f, g] ⋅ (𝖺⇧-⇧1[v, g, f] ⋆ g) ⋅ 𝖺⇧-⇧1[v, g ⋆ f, g] =
v ⋆ 𝖺[g, f, g]"
using assms antipar canI_associator_0 canI_associator_hcomp
whisker_can_left_0 whisker_can_right_0
by simp
thus ?thesis
using assms antipar whisker_left by simp
qed
also have "... = 𝖺⇧-⇧1[v, g, src u] ⋅
(v ⋆ (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅
𝖺[v, src v, g]"
using assms antipar whisker_left by simp
finally show ?thesis by simp
qed
thus ?thesis by auto
qed
also have "... = 𝗋[u] ⋅ (μ ⋆ src u) ⋅
𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ 𝗋⇧-⇧1[g] ⋅ 𝗅[g]) ⋅
𝖺[v, src v, g] ⋅ (𝗋⇧-⇧1[v] ⋆ g)"
using triangle_right comp_assoc by simp
also have "... = 𝗋[u] ⋅ (μ ⋆ src u) ⋅ 𝗋⇧-⇧1[v ⋆ g]"
proof -
have "𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ 𝗋⇧-⇧1[g] ⋅ 𝗅[g]) ⋅ 𝖺[v, src v, g] ⋅ (𝗋⇧-⇧1[v] ⋆ g) = 𝗋⇧-⇧1[v ⋆ g]"
proof -
have "𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ 𝗋⇧-⇧1[g] ⋅ 𝗅[g]) ⋅ 𝖺[v, src v, g] ⋅ (𝗋⇧-⇧1[v] ⋆ g) =
𝖺⇧-⇧1[v, g, trg f] ⋅ can (❙⟨v❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) (❙⟨v❙⟩ ❙⋆ ❙⟨g❙⟩)"
using assms canI_unitor_0 canI_associator_1(2-3) whisker_can_left_0(1)
whisker_can_right_0
by simp
also have "... = 𝖺⇧-⇧1[v, g, src g] ⋅ can (❙⟨v❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) (❙⟨v❙⟩ ❙⋆ ❙⟨g❙⟩)"
using antipar by simp
also have "... = 𝖺⇧-⇧1[v, g, src g] ⋅ (v ⋆ can (❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) ❙⟨g❙⟩)"
using assms canI_unitor_0(2) whisker_can_left_0 by simp
also have "... = 𝖺⇧-⇧1[v, g, src g] ⋅ (v ⋆ 𝗋⇧-⇧1[g])"
using assms canI_unitor_0(2) by simp
also have "... = 𝗋⇧-⇧1[v ⋆ g]"
using assms runit_hcomp(2) by simp
finally have "𝖺⇧-⇧1[v, g, src u] ⋅ (v ⋆ 𝗋⇧-⇧1[g] ⋅ 𝗅[g]) ⋅ 𝖺[v, src v, g] ⋅ (𝗋⇧-⇧1[v] ⋆ g) =
𝗋⇧-⇧1[v ⋆ g]"
by simp
thus ?thesis by simp
qed
thus ?thesis by simp
qed
also have "... = (𝗋[u] ⋅ 𝗋⇧-⇧1[u]) ⋅ μ"
using assms μ runit'_naturality [of μ] comp_assoc by auto
also have "... = μ"
using μ comp_cod_arr iso_runit inv_is_inverse comp_arr_inv by auto
finally show "trnr⇩ε u (trnr⇩η v μ) = μ" by simp
qed
show D: "⋀ν. «ν : v ⇒ u ⋆ f» ⟹ trnr⇩η v (trnr⇩ε u ν) = ν"
proof -
fix ν
assume ν: "«ν : v ⇒ u ⋆ f»"
have "trnr⇩η v (trnr⇩ε u ν) =
(𝗋[u] ⋅ (u ⋆ ε) ⋅ 𝖺[u, f, g] ⋅ (ν ⋆ g) ⋆ f) ⋅ 𝖺⇧-⇧1[v, g, f] ⋅ (v ⋆ η) ⋅ 𝗋⇧-⇧1[v]"
unfolding trnr⇩η_def trnr⇩ε_def by simp
also have "... = (𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅ (𝖺[u, f, g] ⋆ f) ⋅
(((ν ⋆ g) ⋆ f) ⋅ 𝖺⇧-⇧1[v, g, f]) ⋅ (v ⋆ η) ⋅ 𝗋⇧-⇧1[v]"
using assms ν antipar whisker_right comp_assoc by auto
also have "... = (𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅ (𝖺[u, f, g] ⋆ f) ⋅
(𝖺⇧-⇧1[u ⋆ f, g, f] ⋅ (ν ⋆ g ⋆ f)) ⋅ (v ⋆ η) ⋅ 𝗋⇧-⇧1[v]"
using assms ν antipar assoc'_naturality [of ν g f] by auto
also have "... = (𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅ (𝖺[u, f, g] ⋆ f) ⋅
𝖺⇧-⇧1[u ⋆ f, g, f] ⋅ ((ν ⋆ g ⋆ f) ⋅ (v ⋆ η)) ⋅ 𝗋⇧-⇧1[v]"
using comp_assoc by simp
also have "... = (𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅ (𝖺[u, f, g] ⋆ f) ⋅
𝖺⇧-⇧1[u ⋆ f, g, f] ⋅ (((u ⋆ f) ⋆ η) ⋅ (ν ⋆ src v)) ⋅ 𝗋⇧-⇧1[v]"
proof -
have "(ν ⋆ g ⋆ f) ⋅ (v ⋆ η) = ((u ⋆ f) ⋆ η) ⋅ (ν ⋆ src v)"
using assms ν antipar interchange [of "u ⋆ f" ν η "src v"]
interchange [of ν v "g ⋆ f" η] comp_arr_dom comp_cod_arr
by auto
thus ?thesis by simp
qed
also have "... = ((𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅
((𝖺[u, f, g] ⋆ f) ⋅ 𝖺⇧-⇧1[u ⋆ f, g, f]) ⋅
((u ⋆ f) ⋆ η)) ⋅ (ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using comp_assoc by simp
also have "... = ((𝗋[u] ⋆ f) ⋅ ((u ⋆ ε) ⋆ f) ⋅
(𝖺⇧-⇧1[u, f ⋆ g, f] ⋅ (u ⋆ 𝖺⇧-⇧1[f, g, f]) ⋅ 𝖺[u, f, g ⋆ f]) ⋅
((u ⋆ f) ⋆ η)) ⋅ (ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using assms antipar canI_associator_hcomp canI_associator_0 whisker_can_left_0
whisker_can_right_0
by simp
also have "... = ((𝗋[u] ⋆ f) ⋅ (((u ⋆ ε) ⋆ f) ⋅
𝖺⇧-⇧1[u, f ⋆ g, f]) ⋅ (u ⋆ 𝖺⇧-⇧1[f, g, f]) ⋅ (𝖺[u, f, g ⋆ f]) ⋅
((u ⋆ f) ⋆ η)) ⋅ (ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using comp_assoc by simp
also have "... = ((𝗋[u] ⋆ f) ⋅ (𝖺⇧-⇧1[u, src u, f] ⋅ (u ⋆ ε ⋆ f)) ⋅
(u ⋆ 𝖺⇧-⇧1[f, g, f]) ⋅ ((u ⋆ f ⋆ η) ⋅ 𝖺[u, f, src f])) ⋅
(ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using assms antipar assoc'_naturality [of u ε f] assoc_naturality [of u f η]
by auto
also have "... = (𝗋[u] ⋆ f) ⋅ 𝖺⇧-⇧1[u, src u, f] ⋅
((u ⋆ ε ⋆ f) ⋅ (u ⋆ 𝖺⇧-⇧1[f, g, f]) ⋅ (u ⋆ f ⋆ η)) ⋅ 𝖺[u, f, src f] ⋅
(ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using comp_assoc by simp
also have "... = (𝗋[u] ⋆ f) ⋅ 𝖺⇧-⇧1[u, src u, f] ⋅
(u ⋆ (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) ⋅ 𝖺[u, f, src f] ⋅
(ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using assms antipar whisker_left by auto
also have "... = ((𝗋[u] ⋆ f) ⋅ (𝖺⇧-⇧1[u, src u, f] ⋅ (u ⋆ 𝗅⇧-⇧1[f] ⋅ 𝗋[f]) ⋅ 𝖺[u, f, src f])) ⋅
(ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
using assms antipar triangle_left comp_assoc by simp
also have "... = 𝗋[u ⋆ f] ⋅ (ν ⋆ src v) ⋅ 𝗋⇧-⇧1[v]"
proof -
have "(𝗋[u] ⋆ f) ⋅ 𝖺⇧-⇧1[u, src u, f] ⋅ (u ⋆ 𝗅⇧-⇧1[f] ⋅ 𝗋[f]) ⋅ 𝖺[u, f, src f] =
((u ⋆ 𝗅[f]) ⋅ (𝖺[u, src u, f] ⋅ 𝖺⇧-⇧1[u, src u, f])) ⋅
(u ⋆ 𝗅⇧-⇧1[f] ⋅ 𝗋[f]) ⋅ 𝖺[u, f, src f]"
using assms ide_left ide_right antipar triangle comp_assoc by metis
also have "... = (u ⋆ 𝗋[f]) ⋅ 𝖺[u, f, src f]"
using assms antipar canI_associator_1 canI_unitor_0 whisker_can_left_0
whisker_can_right_0 canI_associator_1
by simp
also have "... = 𝗋[u ⋆ f]"
using assms antipar runit_hcomp by simp
finally show ?thesis by simp
qed
also have "... = (𝗋[u ⋆ f] ⋅ 𝗋⇧-⇧1[u ⋆ f]) ⋅ ν"
using assms ν runit'_naturality [of ν] comp_assoc by auto
also have "... = ν"
using assms ν comp_cod_arr comp_arr_inv inv_is_inverse iso_runit by auto
finally show "trnr⇩η v (trnr⇩ε u ν) = ν" by auto
qed
show "bij_betw (trnr⇩η v) (hom (v ⋆ g) u) (hom v (u ⋆ f))"
using A B C D by (intro bij_betwI, auto)
show "bij_betw (trnr⇩ε u) (hom v (u ⋆ f)) (hom (v ⋆ g) u)"
using A B C D by (intro bij_betwI, auto)
qed
lemma trnr⇩η_comp:
assumes "ide v" and "seq μ ν" and "src μ = trg f"
shows "trnr⇩η v (μ ⋅ ν) = (μ ⋆ f) ⋅ trnr⇩η v ν"
using assms trnr⇩η_def whisker_right comp_assoc by auto
end
text ‹
It is useful to have at hand the simpler versions of the preceding results that
hold in a normal bicategory and in a strict bicategory.
›
locale adjunction_in_normal_bicategory =
normal_bicategory +
adjunction_in_bicategory
begin
lemma triangle_left:
shows "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = f"
using triangle_left strict_lunit strict_runit by simp
lemma triangle_right:
shows "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = g"
using triangle_right strict_lunit strict_runit by simp
lemma trnr⇩η_eq:
assumes "ide u" and "ide v"
and "src v = trg g" and "src u = trg f"
and "μ ∈ hom (v ⋆ g) u"
shows "trnr⇩η v μ = (μ ⋆ f) ⋅ 𝖺⇧-⇧1[v, g, f] ⋅ (v ⋆ η)"
unfolding trnr⇩η_def
using assms antipar strict_runit' comp_arr_ide [of "𝗋⇧-⇧1[v]" "v ⋆ η"] hcomp_arr_obj
by auto
lemma trnr⇩ε_eq:
assumes "ide u" and "ide v"
and "src v = trg g" and "src u = trg f"
and "ν ∈ hom v (u ⋆ f)"
shows "trnr⇩ε u ν = (u ⋆ ε) ⋅ 𝖺[u, f, g] ⋅ (ν ⋆ g)"
unfolding trnr⇩ε_def
using assms antipar strict_runit comp_ide_arr hcomp_arr_obj by auto
lemma trnl⇩η_eq:
assumes "ide u" and "ide v"
and "src f = trg v" and "src g = trg u"
and "μ ∈ hom (f ⋆ v) u"
shows "trnl⇩η v μ = (g ⋆ μ) ⋅ 𝖺[g, f, v] ⋅ (η ⋆ v)"
using assms trnl⇩η_def antipar strict_lunit comp_arr_dom hcomp_obj_arr by auto
lemma trnl⇩ε_eq:
assumes "ide u" and "ide v"
and "src f = trg v" and "src g = trg u"
and "ν ∈ hom v (g ⋆ u)"
shows "trnl⇩ε u ν = (ε ⋆ u) ⋅ 𝖺⇧-⇧1[f, g, u] ⋅ (f ⋆ ν)"
using assms trnl⇩ε_def antipar strict_lunit comp_cod_arr hcomp_obj_arr by auto
end
locale adjunction_in_strict_bicategory =
strict_bicategory +
adjunction_in_normal_bicategory
begin
lemma triangle_left:
shows "(ε ⋆ f) ⋅ (f ⋆ η) = f"
using ide_left ide_right antipar triangle_left strict_assoc' comp_cod_arr
by (metis dom_eqI ideD(1) seqE)
lemma triangle_right:
shows "(g ⋆ ε) ⋅ (η ⋆ g) = g"
using ide_left ide_right antipar triangle_right strict_assoc comp_cod_arr
by (metis ideD(1) ideD(2) seqE)
lemma trnr⇩η_eq:
assumes "ide u" and "ide v"
and "src v = trg g" and "src u = trg f"
and "μ ∈ hom (v ⋆ g) u"
shows "trnr⇩η v μ = (μ ⋆ f) ⋅ (v ⋆ η)"
using assms antipar trnr⇩η_eq strict_assoc' comp_ide_arr [of "𝖺⇧-⇧1[v, g, f]" "v ⋆ η"]
by force
lemma trnr⇩ε_eq:
assumes "ide u" and "ide v"
and "src v = trg g" and "src u = trg f"
and "ν ∈ hom v (u ⋆ f)"
shows "trnr⇩ε u ν = (u ⋆ ε) ⋅ (ν ⋆ g)"
using assms antipar trnr⇩ε_eq strict_assoc comp_ide_arr [of "𝖺[u, f, g]" "ν ⋆ g"]
by force
lemma trnl⇩η_eq:
assumes "ide u" and "ide v"
and "src f = trg v" and "src g = trg u"
and "μ ∈ hom (f ⋆ v) u"
shows "trnl⇩η v μ = (g ⋆ μ) ⋅ (η ⋆ v)"
using assms antipar trnl⇩η_eq strict_assoc comp_ide_arr [of "𝖺[g, f, v]" "η ⋆ v"]
by force
lemma trnl⇩ε_eq:
assumes "ide u" and "ide v"
and "src f = trg v" and "src g = trg u"
and "ν ∈ hom v (g ⋆ u)"
shows "trnl⇩ε u ν = (ε ⋆ u) ⋅ (f ⋆ ν)"
using assms antipar trnl⇩ε_eq strict_assoc' comp_ide_arr [of "𝖺⇧-⇧1[f, g, u]" "f ⋆ ν"]
by fastforce
end
subsection "Preservation Properties for Adjunctions"
text ‹
Here we show that adjunctions are preserved under isomorphisms of the
left and right adjoints.
›
context bicategory
begin
interpretation E: self_evaluation_map V H 𝖺 𝗂 src trg ..
notation E.eval ("⦃_⦄")
definition adjoint_pair
where "adjoint_pair f g ≡ ∃η ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
abbreviation is_left_adjoint
where "is_left_adjoint f ≡ ∃g. adjoint_pair f g"
abbreviation is_right_adjoint
where "is_right_adjoint g ≡ ∃f. adjoint_pair f g"
lemma adjoint_pair_antipar:
assumes "adjoint_pair f g"
shows "ide f" and "ide g" and "src f = trg g" and "src g = trg f"
proof -
obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using A by auto
show "ide f" by simp
show "ide g" by simp
show "src f = trg g" using A.antipar by simp
show "src g = trg f" using A.antipar by simp
qed
lemma left_adjoint_is_ide:
assumes "is_left_adjoint f"
shows "ide f"
using assms adjoint_pair_antipar by auto
lemma right_adjoint_is_ide:
assumes "is_right_adjoint f"
shows "ide f"
using assms adjoint_pair_antipar by auto
lemma adjunction_preserved_by_iso_right:
assumes "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : g ⇒ g'»" and "iso φ"
shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' ((φ ⋆ f) ⋅ η) (ε ⋅ (f ⋆ inv φ))"
proof
interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by auto
show "ide f" by simp
show "ide g'"
using assms(2) isomorphic_def by auto
show "«(φ ⋆ f) ⋅ η : src f ⇒ g' ⋆ f»"
using assms A.antipar by fastforce
show "«ε ⋅ (f ⋆ inv φ) : f ⋆ g' ⇒ src g'»"
using assms A.antipar A.counit_in_hom by auto
show "(ε ⋅ (f ⋆ inv φ) ⋆ f) ⋅ 𝖺⇧-⇧1[f, g', f] ⋅ (f ⋆ (φ ⋆ f) ⋅ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
proof -
have "(ε ⋅ (f ⋆ inv φ) ⋆ f) ⋅ 𝖺⇧-⇧1[f, g', f] ⋅ (f ⋆ (φ ⋆ f) ⋅ η) =
(ε ⋆ f) ⋅ (((f ⋆ inv φ) ⋆ f) ⋅ 𝖺⇧-⇧1[f, g', f]) ⋅ (f ⋆ φ ⋆ f) ⋅ (f ⋆ η)"
using assms A.antipar whisker_right whisker_left comp_assoc by auto
also have "... = (ε ⋆ f) ⋅ (𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ inv φ ⋆ f)) ⋅ (f ⋆ φ ⋆ f) ⋅ (f ⋆ η)"
using assms A.antipar assoc'_naturality [of f "inv φ" f] by auto
also have "... = (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ ((f ⋆ inv φ ⋆ f) ⋅ (f ⋆ φ ⋆ f)) ⋅ (f ⋆ η)"
using comp_assoc by simp
also have "... = (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ g ⋆ f) ⋅ (f ⋆ η)"
using assms A.antipar comp_inv_arr inv_is_inverse whisker_left
whisker_right [of f "inv φ" φ]
by auto
also have "... = (ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)"
using assms A.antipar comp_cod_arr by simp
also have "... = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
using A.triangle_left by simp
finally show ?thesis by simp
qed
show "(g' ⋆ ε ⋅ (f ⋆ inv φ)) ⋅ 𝖺[g', f, g'] ⋅ ((φ ⋆ f) ⋅ η ⋆ g') = 𝗋⇧-⇧1[g'] ⋅ 𝗅[g']"
proof -
have "(g' ⋆ ε ⋅ (f ⋆ inv φ)) ⋅ 𝖺[g', f, g'] ⋅ ((φ ⋆ f) ⋅ η ⋆ g') =
(g' ⋆ ε) ⋅ ((g' ⋆ f ⋆ inv φ) ⋅ 𝖺[g', f, g']) ⋅ ((φ ⋆ f) ⋆ g') ⋅ (η ⋆ g')"
using assms A.antipar whisker_left whisker_right comp_assoc by auto
also have "... = (g' ⋆ ε) ⋅ (𝖺[g', f, g] ⋅ ((g' ⋆ f) ⋆ inv φ)) ⋅ ((φ ⋆ f) ⋆ g') ⋅ (η ⋆ g')"
using assms A.antipar assoc_naturality [of g' f "inv φ"] by auto
also have "... = (g' ⋆ ε) ⋅ 𝖺[g', f, g] ⋅ (((g' ⋆ f) ⋆ inv φ) ⋅ ((φ ⋆ f) ⋆ g')) ⋅ (η ⋆ g')"
using comp_assoc by simp
also have "... = (g' ⋆ ε) ⋅ (𝖺[g', f, g] ⋅ ((φ ⋆ f) ⋆ g)) ⋅ ((g ⋆ f) ⋆ inv φ) ⋅ (η ⋆ g')"
proof -
have "((g' ⋆ f) ⋆ inv φ) ⋅ ((φ ⋆ f) ⋆ g') = (φ ⋆ f) ⋆ inv φ"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of "g' ⋆ f" "φ ⋆ f" "inv φ" g']
by auto
also have "... = ((φ ⋆ f) ⋆ g) ⋅ ((g ⋆ f) ⋆ inv φ)"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of "φ ⋆ f" "g ⋆ f" g "inv φ"]
by auto
finally show ?thesis
using comp_assoc by simp
qed
also have "... = ((g' ⋆ ε) ⋅ (φ ⋆ f ⋆ g)) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ (trg g ⋆ inv φ)"
proof -
have "𝖺[g', f, g] ⋅ ((φ ⋆ f) ⋆ g) = (φ ⋆ f ⋆ g) ⋅ 𝖺[g, f, g]"
using assms A.antipar assoc_naturality [of φ f g] by auto
moreover have "((g ⋆ f) ⋆ inv φ) ⋅ (η ⋆ g') = (η ⋆ g) ⋅ (trg g ⋆ inv φ)"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of "g ⋆ f" η "inv φ" g'] interchange [of η "trg g" g "inv φ"]
by auto
ultimately show ?thesis
using comp_assoc by simp
qed
also have "... = ((φ ⋆ src g) ⋅ (g ⋆ ε)) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) ⋅ (trg g ⋆ inv φ)"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of g' φ ε "f ⋆ g"] interchange [of φ g "src g" ε]
by (metis A.counit_simps(1) A.counit_simps(2) A.counit_simps(3) in_homE)
also have "... = (φ ⋆ src g) ⋅ ((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)) ⋅ (trg g ⋆ inv φ)"
using comp_assoc by simp
also have "... = ((φ ⋆ src g) ⋅ 𝗋⇧-⇧1[g]) ⋅ 𝗅[g] ⋅ (trg g ⋆ inv φ)"
using assms A.antipar A.triangle_right comp_cod_arr comp_assoc
by simp
also have "... = (𝗋⇧-⇧1[g'] ⋅ φ) ⋅ inv φ ⋅ 𝗅[g']"
using assms A.antipar runit'_naturality [of φ] lunit_naturality [of "inv φ"]
by auto
also have "... = 𝗋⇧-⇧1[g'] ⋅ (φ ⋅ inv φ) ⋅ 𝗅[g']"
using comp_assoc by simp
also have "... = 𝗋⇧-⇧1[g'] ⋅ 𝗅[g']"
using assms comp_cod_arr comp_arr_inv' by auto
finally show ?thesis by simp
qed
qed
lemma adjunction_preserved_by_iso_left:
assumes "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : f ⇒ f'»" and "iso φ"
shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g ((g ⋆ φ) ⋅ η) (ε ⋅ (inv φ ⋆ g))"
proof
interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by auto
show "ide g" by simp
show "ide f'"
using assms(2) isomorphic_def by auto
show "«(g ⋆ φ) ⋅ η : src f' ⇒ g ⋆ f'»"
using assms A.antipar A.unit_in_hom by force
show "«ε ⋅ (inv φ ⋆ g) : f' ⋆ g ⇒ src g»"
using assms A.antipar by force
show "(g ⋆ ε ⋅ (inv φ ⋆ g)) ⋅ 𝖺[g, f', g] ⋅ ((g ⋆ φ) ⋅ η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
proof -
have "(g ⋆ ε ⋅ (inv φ ⋆ g)) ⋅ 𝖺[g, f', g] ⋅ ((g ⋆ φ) ⋅ η ⋆ g) =
(g ⋆ ε) ⋅ ((g ⋆ inv φ ⋆ g) ⋅ 𝖺[g, f', g]) ⋅ ((g ⋆ φ) ⋆ g) ⋅ (η ⋆ g)"
using assms A.antipar whisker_left whisker_right comp_assoc by auto
also have "... = (g ⋆ ε) ⋅ (𝖺[g, f, g] ⋅ ((g ⋆ inv φ) ⋆ g)) ⋅ ((g ⋆ φ) ⋆ g) ⋅ (η ⋆ g)"
using assms A.antipar assoc_naturality [of g "inv φ" g] by auto
also have "... = (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (((g ⋆ inv φ) ⋆ g) ⋅ ((g ⋆ φ) ⋆ g)) ⋅ (η ⋆ g)"
using comp_assoc by simp
also have "... = (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ ((g ⋆ f) ⋆ g) ⋅ (η ⋆ g)"
using assms A.antipar comp_inv_arr inv_is_inverse whisker_right
whisker_left [of g "inv φ" φ]
by auto
also have "... = (g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g)"
using assms A.antipar comp_cod_arr by simp
also have "... = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
using A.triangle_right by simp
finally show ?thesis by simp
qed
show "(ε ⋅ (inv φ ⋆ g) ⋆ f') ⋅ 𝖺⇧-⇧1[f', g, f'] ⋅ (f' ⋆ (g ⋆ φ) ⋅ η) = 𝗅⇧-⇧1[f'] ⋅ 𝗋[f']"
proof -
have "(ε ⋅ (inv φ ⋆ g) ⋆ f') ⋅ 𝖺⇧-⇧1[f', g, f'] ⋅ (f' ⋆ (g ⋆ φ) ⋅ η) =
(ε ⋆ f') ⋅ (((inv φ ⋆ g) ⋆ f') ⋅ 𝖺⇧-⇧1[f', g, f']) ⋅ (f' ⋆ g ⋆ φ) ⋅ (f' ⋆ η)"
using assms A.antipar whisker_right whisker_left comp_assoc
by auto
also have "... = (ε ⋆ f') ⋅ (𝖺⇧-⇧1[f, g, f'] ⋅ (inv φ ⋆ g ⋆ f')) ⋅ (f' ⋆ g ⋆ φ) ⋅ (f' ⋆ η)"
using assms A.antipar assoc'_naturality [of "inv φ" g f'] by auto
also have "... = (ε ⋆ f') ⋅ 𝖺⇧-⇧1[f, g, f'] ⋅ ((inv φ ⋆ g ⋆ f') ⋅ (f' ⋆ g ⋆ φ)) ⋅ (f' ⋆ η)"
using comp_assoc by simp
also have "... = (ε ⋆ f') ⋅ (𝖺⇧-⇧1[f, g, f'] ⋅ (f ⋆ g ⋆ φ)) ⋅ (inv φ ⋆ g ⋆ f) ⋅ (f' ⋆ η)"
proof -
have "(inv φ ⋆ g ⋆ f') ⋅ (f' ⋆ g ⋆ φ) = (f ⋆ g ⋆ φ) ⋅ (inv φ ⋆ g ⋆ f)"
using assms(2-3) A.antipar comp_arr_dom comp_cod_arr
interchange [of "inv φ" f' "g ⋆ f'" "g ⋆ φ"]
interchange [of f "inv φ" "g ⋆ φ" "g ⋆ f"]
by auto
thus ?thesis
using comp_assoc by simp
qed
also have "... = ((ε ⋆ f') ⋅ ((f ⋆ g) ⋆ φ)) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ (inv φ ⋆ src f)"
proof -
have "𝖺⇧-⇧1[f, g, f'] ⋅ (f ⋆ g ⋆ φ) = ((f ⋆ g) ⋆ φ) ⋅ 𝖺⇧-⇧1[f, g, f]"
using assms A.antipar assoc'_naturality [of f g φ] by auto
moreover have "(inv φ ⋆ g ⋆ f) ⋅ (f' ⋆ η) = (f ⋆ η) ⋅ (inv φ ⋆ src f)"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of "inv φ" f' "g ⋆ f" η] interchange [of f "inv φ" η "src f"]
by auto
ultimately show ?thesis
using comp_assoc by simp
qed
also have "... = ((trg f ⋆ φ) ⋅ (ε ⋆ f)) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) ⋅ (inv φ ⋆ src f)"
using assms A.antipar comp_arr_dom comp_cod_arr
interchange [of ε "f ⋆ g" f' φ] interchange [of "trg f" ε φ f]
by (metis A.counit_simps(1) A.counit_simps(2) A.counit_simps(3) in_homE)
also have "... = (trg f ⋆ φ) ⋅ ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) ⋅ (inv φ ⋆ src f)"
using comp_assoc by simp
also have "... = ((trg f ⋆ φ) ⋅ 𝗅⇧-⇧1[f]) ⋅ 𝗋[f] ⋅ (inv φ ⋆ src f)"
using assms A.antipar A.triangle_left comp_cod_arr comp_assoc
by simp
also have "... = (𝗅⇧-⇧1[f'] ⋅ φ) ⋅ inv φ ⋅ 𝗋[f']"
using assms A.antipar lunit'_naturality runit_naturality [of "inv φ"] by auto
also have "... = 𝗅⇧-⇧1[f'] ⋅ (φ ⋅ inv φ) ⋅ 𝗋[f']"
using comp_assoc by simp
also have "... = 𝗅⇧-⇧1[f'] ⋅ 𝗋[f']"
using assms comp_cod_arr comp_arr_inv inv_is_inverse by auto
finally show ?thesis by simp
qed
qed
lemma adjoint_pair_preserved_by_iso:
assumes "adjoint_pair f g"
and "«φ : f ⇒ f'»" and "iso φ"
and "«ψ : g ⇒ g'»" and "iso ψ"
shows "adjoint_pair f' g'"
using assms adjoint_pair_def adjunction_preserved_by_iso_left
adjunction_preserved_by_iso_right
by metis
lemma left_adjoint_preserved_by_iso:
assumes "is_left_adjoint f"
and "«φ : f ⇒ f'»" and "iso φ"
shows "is_left_adjoint f'"
proof -
obtain g where g: "adjoint_pair f g"
using assms by auto
have "adjoint_pair f' g"
using assms g adjoint_pair_preserved_by_iso [of f g φ f' g g]
adjoint_pair_antipar [of f g]
by auto
thus ?thesis by auto
qed
lemma right_adjoint_preserved_by_iso:
assumes "is_right_adjoint g"
and "«φ : g ⇒ g'»" and "iso φ"
shows "is_right_adjoint g'"
proof -
obtain f where f: "adjoint_pair f g"
using assms by auto
have "adjoint_pair f g'"
using assms f adjoint_pair_preserved_by_iso [of f g f f φ g']
adjoint_pair_antipar [of f g]
by auto
thus ?thesis by auto
qed
lemma left_adjoint_preserved_by_iso':
assumes "is_left_adjoint f" and "f ≅ f'"
shows "is_left_adjoint f'"
using assms isomorphic_def left_adjoint_preserved_by_iso by blast
lemma right_adjoint_preserved_by_iso':
assumes "is_right_adjoint g" and "g ≅ g'"
shows "is_right_adjoint g'"
using assms isomorphic_def right_adjoint_preserved_by_iso by blast
lemma obj_self_adjunction:
assumes "obj a"
shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg a a 𝗅⇧-⇧1[a] 𝗋[a]"
proof
show 1: "ide a"
using assms by auto
show "«𝗅⇧-⇧1[a] : src a ⇒ a ⋆ a»"
using assms 1 by auto
show "«𝗋[a] : a ⋆ a ⇒ src a»"
using assms 1 by fastforce
show "(𝗋[a] ⋆ a) ⋅ 𝖺⇧-⇧1[a, a, a] ⋅ (a ⋆ 𝗅⇧-⇧1[a]) = 𝗅⇧-⇧1[a] ⋅ 𝗋[a]"
using assms 1 canI_unitor_1 canI_associator_1(2) canI_associator_3
whisker_can_right_1 whisker_can_left_1 can_Ide_self obj_simps
by simp
show "(a ⋆ 𝗋[a]) ⋅ 𝖺[a, a, a] ⋅ (𝗅⇧-⇧1[a] ⋆ a) = 𝗋⇧-⇧1[a] ⋅ 𝗅[a]"
using assms 1 canI_unitor_1 canI_associator_1(2) canI_associator_3
whisker_can_right_1 whisker_can_left_1 can_Ide_self
by simp
qed
lemma obj_is_self_adjoint:
assumes "obj a"
shows "adjoint_pair a a" and "is_left_adjoint a" and "is_right_adjoint a"
using assms obj_self_adjunction adjoint_pair_def by auto
end
subsection "Pseudofunctors and Adjunctions"
context pseudofunctor
begin
lemma preserves_adjunction:
assumes "adjunction_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
shows "adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g)
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
proof -
interpret adjunction_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε
using assms by auto
interpret A: adjunction_data_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
‹F f› ‹F g› ‹D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)›
‹D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)›
using adjunction_data_in_bicategory_axioms preserves_adjunction_data by auto
show "adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g)
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
proof
show "(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)) =
D.lunit' (F f) ⋅⇩D 𝗋⇩D[F f]"
proof -
have 1: "D.iso (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)))"
using antipar C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C D.iso_is_arr FF_def
by (intro D.isos_compose D.seqI, simp_all)
have "(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)) =
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) ⋆⇩D F f) ⋅⇩D
(D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)) ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))"
proof -
have "𝖺⇩D⇧-⇧1[F f, F g, F f] =
(D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f))"
proof -
have "𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D D.inv (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f))) =
D.inv (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f))"
proof -
have "D.inv (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)) ⋅⇩D 𝖺⇩D[F f, F g, F f]) =
D.inv (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f))"
using antipar assoc_coherence by simp
moreover
have "D.inv (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)) ⋅⇩D 𝖺⇩D[F f, F g, F f]) =
𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D D.inv (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)))"
proof -
have "D.seq (Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f))) 𝖺⇩D[F f, F g, F f]"
using antipar by fastforce
thus ?thesis
using 1 antipar D.comp_assoc
D.inv_comp [of "𝖺⇩D[F f, F g, F f]" "Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f))"]
by auto
qed
ultimately show ?thesis by simp
qed
moreover have 2: "D.iso (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f))"
using antipar D.isos_compose C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C cmp_simps(4)
by simp
ultimately have "𝖺⇩D⇧-⇧1[F f, F g, F f] =
D.inv (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) ⋅⇩D
(Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)))"
using 1 2 antipar D.invert_side_of_triangle(2) D.inv_inv D.iso_inv_iso D.arr_inv
by metis
moreover have "D.inv (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) =
(D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f]"
proof -
have "D.inv (F 𝖺⇩C[f, g, f] ⋅⇩D Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) =
D.inv (Φ (f ⋆⇩C g, f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f]"
using antipar D.isos_compose C.VV.arr_char⇩S⇩b⇩C cmp_simps(4)
preserves_inv D.inv_comp C.VV.cod_char⇩S⇩b⇩C
by simp
also have "... = (D.inv (Φ (f, g) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f))) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f]"
using antipar D.inv_comp C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C cmp_simps(4)
by simp
also have "... = ((D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f))) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f]"
using antipar C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C by simp
also have "... = (D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f]"
using D.comp_assoc by simp
finally show ?thesis by simp
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D
(F f ⋆⇩D F η ⋅⇩D unit (src⇩C f))"
proof -
have "... = ((D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) ⋅⇩D
(D.inv (Φ (f, g)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D Φ (g, f)) ⋅⇩D
((F f ⋆⇩D D.inv (Φ (g, f))) ⋅⇩D (F f ⋆⇩D F η ⋅⇩D unit (src⇩C f)))"
proof -
have "D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) ⋆⇩D F f =
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)"
using ide_left ide_right antipar D.whisker_right unit_char(2)
by (metis A.counit_simps(1) A.ide_left D.comp_assoc)
moreover have "F f ⋆⇩D D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) =
(F f ⋆⇩D D.inv (Φ (g, f))) ⋅⇩D (F f ⋆⇩D F η ⋅⇩D unit (src⇩C f))"
using antipar unit_char(2) D.whisker_left by simp
ultimately show ?thesis by simp
qed
also have "... = (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D
(((Φ (f, g) ⋆⇩D F f) ⋅⇩D (D.inv (Φ (f, g)) ⋆⇩D F f)) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f))) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D Φ (f, g ⋆⇩C f) ⋅⇩D
(((F f ⋆⇩D Φ (g, f)) ⋅⇩D (F f ⋆⇩D D.inv (Φ (g, f)))) ⋅⇩D
(F f ⋆⇩D F η ⋅⇩D unit (src⇩C f)))"
using D.comp_assoc by simp
also have "... = (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D
(F f ⋆⇩D F η ⋅⇩D unit (src⇩C f))"
proof -
have "((F f ⋆⇩D Φ (g, f)) ⋅⇩D (F f ⋆⇩D D.inv (Φ (g, f)))) ⋅⇩D
(F f ⋆⇩D F η ⋅⇩D unit (src⇩C f)) =
F f ⋆⇩D F η ⋅⇩D unit (src⇩C f)"
proof -
have "(F f ⋆⇩D Φ (g, f)) ⋅⇩D (F f ⋆⇩D D.inv (Φ (g, f))) = F f ⋆⇩D F (g ⋆⇩C f)"
using antipar unit_char(2) D.comp_arr_inv D.inv_is_inverse
D.whisker_left [of "F f" "Φ (g, f)" "D.inv (Φ (g, f))"]
by simp
moreover have "D.seq (F f ⋆⇩D F (g ⋆⇩C f)) (F f ⋆⇩D F η ⋅⇩D unit (src⇩C f))"
using antipar by fastforce
ultimately show ?thesis
using D.comp_cod_arr by auto
qed
moreover have "((Φ (f, g) ⋆⇩D F f) ⋅⇩D (D.inv (Φ (f, g)) ⋆⇩D F f)) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f)) =
D.inv (Φ (f ⋆⇩C g, f))"
using antipar D.comp_arr_inv D.inv_is_inverse D.comp_cod_arr
D.whisker_right [of "F f" "Φ (f, g)" "D.inv (Φ (f, g))"]
by simp
ultimately show ?thesis by simp
qed
finally show ?thesis by simp
qed
also have "... = (D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D
D.inv (Φ (trg⇩C f, f)) ⋅⇩D F (ε ⋆⇩C f) ⋅⇩D
((Φ (f ⋆⇩C g, f) ⋅⇩D D.inv (Φ (f ⋆⇩C g, f))) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f]) ⋅⇩D
((Φ (f, g ⋆⇩C f) ⋅⇩D D.inv (Φ (f, g ⋆⇩C f))) ⋅⇩D F (f ⋆⇩C η)) ⋅⇩D
Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
proof -
have "(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋆⇩D F f) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D
(F f ⋆⇩D F η ⋅⇩D unit (src⇩C f)) =
((D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D (F ε ⋆⇩D F f)) ⋅⇩D
D.inv (Φ (f ⋆⇩C g, f)) ⋅⇩D
F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D
Φ (f, g ⋆⇩C f) ⋅⇩D
((F f ⋆⇩D F η) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)))"
using antipar D.comp_assoc D.whisker_left D.whisker_right unit_char(2)
by simp
moreover have "F ε ⋆⇩D F f = D.inv (Φ (trg⇩C f, f)) ⋅⇩D F (ε ⋆⇩C f) ⋅⇩D Φ (f ⋆⇩C g, f)"
using antipar Φ.naturality [of "(ε, f)"] C.VV.arr_char⇩S⇩b⇩C FF_def
D.invert_side_of_triangle(1) C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
moreover have "F f ⋆⇩D F η = D.inv (Φ (f, g ⋆⇩C f)) ⋅⇩D F (f ⋆⇩C η) ⋅⇩D Φ (f, src⇩C f)"
using antipar Φ.naturality [of "(f, η)"] C.VV.arr_char⇩S⇩b⇩C FF_def
D.invert_side_of_triangle(1) C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = ((D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f))) ⋅⇩D
(F (ε ⋆⇩C f) ⋅⇩D
(F ((f ⋆⇩C g) ⋆⇩C f) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D F (f ⋆⇩C g ⋆⇩C f)) ⋅⇩D
F (f ⋆⇩C η)) ⋅⇩D
Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
using antipar D.comp_arr_inv' D.comp_assoc by simp
also have "... = ((D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f))) ⋅⇩D
(F (ε ⋆⇩C f) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D F (f ⋆⇩C η)) ⋅⇩D
Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
proof -
have "F ((f ⋆⇩C g) ⋆⇩C f) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D F (f ⋆⇩C g ⋆⇩C f) = F 𝖺⇩C⇧-⇧1[f, g, f]"
using antipar D.comp_arr_dom D.comp_cod_arr by simp
thus ?thesis by simp
qed
also have "... = D.inv (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)) ⋅⇩D
F ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η)) ⋅⇩D
Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
proof -
have "(D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f)) =
D.inv (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f))"
proof -
have "D.iso (Φ (trg⇩C f, f))"
using antipar by simp
moreover have "D.iso (unit (trg⇩C f) ⋆⇩D F f)"
using antipar unit_char(2) by simp
moreover have "D.seq (Φ (trg⇩C f, f)) (unit (trg⇩C f) ⋆⇩D F f)"
using antipar D.iso_is_arr calculation(2)
apply (intro D.seqI D.hseqI) by auto
ultimately show ?thesis
using antipar D.inv_comp unit_char(2) by simp
qed
moreover have "F (ε ⋆⇩C f) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D F (f ⋆⇩C η) =
F ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η))"
using antipar by simp
ultimately show ?thesis by simp
qed
also have "... = (D.lunit' (F f) ⋅⇩D F 𝗅⇩C[f]) ⋅⇩D
F (C.lunit' f ⋅⇩C 𝗋⇩C[f]) ⋅⇩D
(D.inv (F 𝗋⇩C[f]) ⋅⇩D 𝗋⇩D[F f])"
proof -
have "F ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η)) = F (C.lunit' f ⋅⇩C 𝗋⇩C[f])"
using triangle_left by simp
moreover have "D.inv (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)) =
D.lunit' (F f) ⋅⇩D F 𝗅⇩C[f]"
proof -
have 0: "D.iso (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f))"
using unit_char(2)
apply (intro D.isos_compose D.seqI) by auto
show ?thesis
proof -
have 1: "D.iso (F 𝗅⇩C[f])"
using C.iso_lunit preserves_iso by auto
moreover have "D.iso (F 𝗅⇩C[f] ⋅⇩D Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f))"
by (metis (no_types) A.ide_left D.iso_lunit ide_left lunit_coherence)
moreover have "D.inv (D.inv (F 𝗅⇩C[f])) = F 𝗅⇩C[f]"
using 1 D.inv_inv by blast
ultimately show ?thesis
by (metis 0 D.inv_comp D.invert_side_of_triangle(2) D.iso_inv_iso
D.iso_is_arr ide_left lunit_coherence)
qed
qed
moreover have "Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)) = D.inv (F 𝗋⇩C[f]) ⋅⇩D 𝗋⇩D[F f]"
using ide_left runit_coherence preserves_iso C.iso_runit D.invert_side_of_triangle(1)
by (metis A.ide_left D.runit_simps(1))
ultimately show ?thesis by simp
qed
also have "... = D.lunit' (F f) ⋅⇩D
((F 𝗅⇩C[f] ⋅⇩D F (C.lunit' f)) ⋅⇩D (F 𝗋⇩C[f] ⋅⇩D D.inv (F 𝗋⇩C[f]))) ⋅⇩D
𝗋⇩D[F f]"
using D.comp_assoc by simp
also have "... = D.lunit' (F f) ⋅⇩D 𝗋⇩D[F f]"
using D.comp_cod_arr C.iso_runit C.iso_lunit preserves_iso D.comp_arr_inv'
preserves_inv
by force
finally show ?thesis by blast
qed
show "(F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g) =
D.runit' (F g) ⋅⇩D 𝗅⇩D[F g]"
proof -
have "𝖺⇩D[F g, F f, F g] =
D.inv (Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g))) ⋅⇩D
F 𝖺⇩C[g, f, g] ⋅⇩D Φ (g ⋆⇩C f, g) ⋅⇩D (Φ (g, f) ⋆⇩D F g)"
proof -
have "D.iso (Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g)))"
using antipar D.iso_is_arr
apply (intro D.isos_compose, auto)
by (metis C.iso_assoc D.comp_assoc D.seqE ide_left ide_right
preserves_assoc(1) preserves_iso)
moreover have "F 𝖺⇩C[g, f, g] ⋅⇩D Φ (g ⋆⇩C f, g) ⋅⇩D (Φ (g, f) ⋆⇩D F g) =
Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g)) ⋅⇩D 𝖺⇩D[F g, F f, F g]"
using antipar assoc_coherence by simp
moreover have "D.seq (F 𝖺⇩C[g, f, g]) (Φ (g ⋆⇩C f, g) ⋅⇩D (Φ (g, f) ⋆⇩D F g))"
using antipar C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C FF_def
by (intro D.seqI D.hseqI') auto
ultimately show ?thesis
using D.invert_side_of_triangle(1) D.comp_assoc by auto
qed
hence "(F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g) =
(F g ⋆⇩D (D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D Φ (f, g)) ⋅⇩D
D.inv (Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g))) ⋅⇩D
F 𝖺⇩C[g, f, g] ⋅⇩D
Φ (g ⋆⇩C f, g) ⋅⇩D (Φ (g, f) ⋆⇩D F g) ⋅⇩D
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g)"
using D.comp_assoc by simp
also have "... = ((F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D (F g ⋆⇩D Φ (f, g))) ⋅⇩D
D.inv (Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g))) ⋅⇩D
F 𝖺⇩C[g, f, g] ⋅⇩D Φ (g ⋆⇩C f, g) ⋅⇩D
(Φ (g, f) ⋆⇩D F g) ⋅⇩D ((D.inv (Φ (g, f)) ⋆⇩D F g) ⋅⇩D
(F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g))"
proof -
have "F g ⋆⇩D (D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D Φ (f, g) =
(F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D (F g ⋆⇩D Φ (f, g))"
proof -
have "D.seq (D.inv (unit (trg⇩C f)) ⋅⇩D F ε) (Φ (f, g))"
using antipar D.comp_assoc by simp
thus ?thesis
using antipar D.whisker_left by simp
qed
moreover have "D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g =
(D.inv (Φ (g, f)) ⋆⇩D F g) ⋅⇩D (F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g)"
using antipar D.whisker_right by simp
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = (F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D
(((F g ⋆⇩D Φ (f, g)) ⋅⇩D D.inv (F g ⋆⇩D Φ (f, g))) ⋅⇩D
D.inv (Φ (g, f ⋆⇩C g))) ⋅⇩D F 𝖺⇩C[g, f, g] ⋅⇩D Φ (g ⋆⇩C f, g) ⋅⇩D
((Φ (g, f) ⋆⇩D F g) ⋅⇩D (D.inv (Φ (g, f)) ⋆⇩D F g)) ⋅⇩D
(F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g)"
proof -
have "D.inv (Φ (g, f ⋆⇩C g) ⋅⇩D (F g ⋆⇩D Φ (f, g))) =
D.inv (F g ⋆⇩D Φ (f, g)) ⋅⇩D D.inv (Φ (g, f ⋆⇩C g))"
proof -
have "D.iso (Φ (g, f ⋆⇩C g))"
using antipar by simp
moreover have "D.iso (F g ⋆⇩D Φ (f, g))"
using antipar by simp
moreover have "D.seq (Φ (g, f ⋆⇩C g)) (F g ⋆⇩D Φ (f, g))"
using antipar cmp_in_hom A.ide_right D.iso_is_arr
by (intro D.seqI) auto
ultimately show ?thesis
using antipar D.inv_comp by simp
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (F g ⋆⇩D D.inv (unit (trg⇩C f)) ⋅⇩D F ε) ⋅⇩D
D.inv (Φ (g, f ⋆⇩C g)) ⋅⇩D F 𝖺⇩C[g, f, g] ⋅⇩D Φ (g ⋆⇩C f, g) ⋅⇩D
(F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g)"
proof -
have "((Φ (g, f) ⋆⇩D F g) ⋅⇩D (D.inv (Φ (g, f)) ⋆⇩D F g)) ⋅⇩D
(F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g) =
(F η ⋅⇩D unit (src⇩C f) ⋆⇩D F g)"
proof -
have "(Φ (g, f) ⋆⇩D F g) ⋅⇩D (D.inv (Φ (g, f)) ⋆⇩D F g) = F (g ⋆⇩C f) ⋆⇩D F g"
using antipar D.comp_arr_inv'
D.whisker_right [of "F g" "Φ (g, f)" "D.inv (Φ (g, f))"]
by simp
thus ?thesis
using antipar D.comp_cod_arr D.whisker_right by simp
qed
moreover have "((F g ⋆⇩D Φ (f, g)) ⋅⇩D D.inv (F g ⋆⇩D Φ (f, g))) ⋅⇩D
D.inv (Φ (g, f ⋆⇩C g)) =
D.inv (Φ (g, f ⋆⇩C g))"
using antipar D.comp_arr_inv' D.comp_cod_arr
D.whisker_left [of "F g" "Φ (f, g)" "D.inv (Φ (f, g))"]
by simp
ultimately show ?thesis by simp
qed
also have "... = (F g ⋆⇩D D.inv (unit (trg⇩C f))) ⋅⇩D
((F g ⋆⇩D F ε) ⋅⇩D D.inv (Φ (g, f ⋆⇩C g))) ⋅⇩D
F 𝖺⇩C[g, f, g] ⋅⇩D
(Φ (g ⋆⇩C f, g) ⋅⇩D (F η ⋆⇩D F g)) ⋅⇩D
(unit (src⇩C f) ⋆⇩D F g)"
using antipar D.whisker_left D.whisker_right unit_char(2) D.comp_assoc by simp
also have "... = (F g ⋆⇩D D.inv (unit (trg⇩C f))) ⋅⇩D D.inv (Φ (g, src⇩C g)) ⋅⇩D
(F (g ⋆⇩C ε) ⋅⇩D F 𝖺⇩C[g, f, g] ⋅⇩D F (η ⋆⇩C g)) ⋅⇩D
Φ (trg⇩C g, g) ⋅⇩D (unit (src⇩C f) ⋆⇩D F g)"
proof -
have "(F g ⋆⇩D F ε) ⋅⇩D D.inv (Φ (g, f ⋆⇩C g)) = D.inv (Φ (g, src⇩C g)) ⋅⇩D F (g ⋆⇩C ε)"
using antipar C.VV.arr_char⇩S⇩b⇩C Φ.naturality [of "(g, ε)"] FF_def
D.invert_opposite_sides_of_square C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
moreover have "Φ (g ⋆⇩C f, g) ⋅⇩D (F η ⋆⇩D F g) = F (η ⋆⇩C g) ⋅⇩D Φ (trg⇩C g, g)"
using antipar C.VV.arr_char⇩S⇩b⇩C Φ.naturality [of "(η, g)"] FF_def
C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = ((F g ⋆⇩D D.inv (unit (trg⇩C f))) ⋅⇩D D.inv (Φ (g, src⇩C g)) ⋅⇩D
F (C.runit' g)) ⋅⇩D (F 𝗅⇩C[g] ⋅⇩D Φ (trg⇩C g, g) ⋅⇩D (unit (src⇩C f) ⋆⇩D F g))"
proof -
have "F (g ⋆⇩C ε) ⋅⇩D F 𝖺⇩C[g, f, g] ⋅⇩D F (η ⋆⇩C g) = F (C.runit' g) ⋅⇩D F 𝗅⇩C[g]"
using ide_left ide_right antipar triangle_right
by (metis C.comp_in_homE C.seqI' preserves_comp triangle_in_hom(2))
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = D.runit' (F g) ⋅⇩D 𝗅⇩D[F g]"
proof -
have "D.inv 𝗋⇩D[F g] =
(F g ⋆⇩D D.inv (unit (trg⇩C f))) ⋅⇩D D.inv (Φ (g, src⇩C g)) ⋅⇩D F (C.runit' g)"
proof -
have "D.runit' (F g) = D.inv (F 𝗋⇩C[g] ⋅⇩D Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g)))"
using runit_coherence by simp
also have
"... = (F g ⋆⇩D D.inv (unit (trg⇩C f))) ⋅⇩D D.inv (Φ (g, src⇩C g)) ⋅⇩D F (C.runit' g)"
proof -
have "D.inv (F 𝗋⇩C[g] ⋅⇩D Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g))) =
D.inv (F g ⋆⇩D unit (src⇩C g)) ⋅⇩D D.inv (Φ (g, src⇩C g)) ⋅⇩D F (C.runit' g)"
proof -
have "D.iso (F 𝗋⇩C[g])"
using preserves_iso by simp
moreover have 1: "D.iso (Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g)))"
using preserves_iso unit_char(2) D.arrI D.seqE ide_right runit_coherence
by (intro D.isos_compose D.seqI, auto)
moreover have "D.seq (F 𝗋⇩C[g]) (Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g)))"
using ide_right A.ide_right D.runit_simps(1) runit_coherence by metis
ultimately have "D.inv (F 𝗋⇩C[g] ⋅⇩D Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g))) =
D.inv (Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g))) ⋅⇩D F (C.runit' g)"
using C.iso_runit preserves_inv D.inv_comp by simp
moreover have "D.inv (Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (src⇩C g))) =
D.inv (F g ⋆⇩D unit (src⇩C g)) ⋅⇩D D.inv (Φ (g, src⇩C g))"
proof -
have "D.seq (Φ (g, src⇩C g)) (F g ⋆⇩D unit (src⇩C g))"
using 1 antipar preserves_iso unit_char(2) by fast
thus ?thesis
using 1 antipar preserves_iso unit_char(2) D.inv_comp by auto
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
thus ?thesis
using antipar unit_char(2) preserves_iso by simp
qed
finally show ?thesis by simp
qed
thus ?thesis
using antipar lunit_coherence by simp
qed
finally show ?thesis by simp
qed
qed
qed
lemma preserves_adjoint_pair:
assumes "C.adjoint_pair f g"
shows "D.adjoint_pair (F f) (F g)"
using assms C.adjoint_pair_def D.adjoint_pair_def preserves_adjunction by blast
lemma preserves_left_adjoint:
assumes "C.is_left_adjoint f"
shows "D.is_left_adjoint (F f)"
using assms preserves_adjoint_pair by auto
lemma preserves_right_adjoint:
assumes "C.is_right_adjoint g"
shows "D.is_right_adjoint (F g)"
using assms preserves_adjoint_pair by auto
end
context equivalence_pseudofunctor
begin
lemma reflects_adjunction:
assumes "C.ide f" and "C.ide g"
and "«η : src⇩C f ⇒⇩C g ⋆⇩C f»" and "«ε : f ⋆⇩C g ⇒⇩C src⇩C g»"
and "adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g)
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
shows "adjunction_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
proof -
let ?η' = "D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)"
let ?ε' = "D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)"
interpret A': adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹F f› ‹F g› ?η' ?ε'
using assms(5) by auto
interpret A: adjunction_data_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε
using assms(1-4) by (unfold_locales, auto)
show ?thesis
proof
show "(ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η) = 𝗅⇩C⇧-⇧1[f] ⋅⇩C 𝗋⇩C[f]"
proof -
have 1: "C.par ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η)) (𝗅⇩C⇧-⇧1[f] ⋅⇩C 𝗋⇩C[f])"
using assms A.antipar by simp
moreover have "F ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η)) = F (𝗅⇩C⇧-⇧1[f] ⋅⇩C 𝗋⇩C[f])"
proof -
have "F ((ε ⋆⇩C f) ⋅⇩C 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩C (f ⋆⇩C η)) =
F (ε ⋆⇩C f) ⋅⇩D F 𝖺⇩C⇧-⇧1[f, g, f] ⋅⇩D F (f ⋆⇩C η)"
using 1 by (metis C.seqE preserves_comp)
also have "... =
(F (ε ⋆⇩C f) ⋅⇩D Φ (f ⋆⇩C g, f)) ⋅⇩D
(Φ (f, g) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D (F f ⋆⇩D D.inv (Φ (g, f))) ⋅⇩D
(D.inv (Φ (f, g ⋆⇩C f)) ⋅⇩D F (f ⋆⇩C η))"
using assms A.antipar preserves_assoc(2) D.comp_assoc by auto
also have "... = Φ (trg⇩C f, f) ⋅⇩D ((F ε ⋆⇩D F f) ⋅⇩D (Φ (f, g) ⋆⇩D F f)) ⋅⇩D
𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D
((F f ⋆⇩D D.inv (Φ (g, f))) ⋅⇩D (F f ⋆⇩D F η)) ⋅⇩D
D.inv (Φ (f, src⇩C f))"
proof -
have "F (ε ⋆⇩C f) ⋅⇩D Φ (f ⋆⇩C g, f) = Φ (trg⇩C f, f) ⋅⇩D (F ε ⋆⇩D F f)"
using assms Φ.naturality [of "(ε, f)"] FF_def C.VV.arr_char⇩S⇩b⇩C
C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
moreover have "D.inv (Φ (f, g ⋆⇩C f)) ⋅⇩D F (f ⋆⇩C η) =
(F f ⋆⇩D F η) ⋅⇩D D.inv (Φ (f, src⇩C f))"
proof -
have "F (f ⋆⇩C η) ⋅⇩D Φ (f, src⇩C f) = Φ (f, g ⋆⇩C f) ⋅⇩D (F f ⋆⇩D F η)"
using assms Φ.naturality [of "(f, η)"] FF_def C.VV.arr_char⇩S⇩b⇩C A.antipar
C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
by simp
thus ?thesis
using assms A.antipar cmp_components_are_iso C.VV.arr_char⇩S⇩b⇩C cmp_in_hom
FF_def C.VV.dom_simp C.VV.cod_simp
D.invert_opposite_sides_of_square
[of "Φ (f, g ⋆⇩C f)" "F f ⋆⇩D F η" "F (f ⋆⇩C η)" "Φ (f, src⇩C f)"]
by fastforce
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = Φ (trg⇩C f, f) ⋅⇩D (F ε ⋅⇩D Φ (f, g) ⋆⇩D F f) ⋅⇩D
𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, f)) ⋅⇩D F η) ⋅⇩D D.inv (Φ (f, src⇩C f))"
using assms A.antipar cmp_in_hom A.ide_left A.ide_right A'.ide_left A'.ide_right
D.whisker_left [of "F f" "D.inv (Φ (g, f))" "F η"]
D.whisker_right [of "F f" "F ε" "Φ (f, g)"]
by (metis A'.counit_in_vhom A'.unit_simps(1)D.arrI D.comp_assoc
D.src.preserves_reflects_arr D.src_vcomp D.vseq_implies_hpar(1) cmp_simps(2))
also have "... = Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋅⇩D ?ε' ⋆⇩D F f) ⋅⇩D
𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D
(F f ⋆⇩D ?η' ⋅⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
proof -
have "F ε ⋅⇩D Φ (f, g) = unit (trg⇩C f) ⋅⇩D ?ε'"
proof -
have "D.iso (unit (trg⇩C f))"
using A.ide_left C.ideD(1) unit_char(2) by blast
thus ?thesis
by (metis A'.counit_simps(1) D.comp_assoc D.comp_cod_arr D.inv_is_inverse
D.seqE D.comp_arr_inv)
qed
moreover have "D.inv (Φ (g, f)) ⋅⇩D F η = ?η' ⋅⇩D D.inv (unit (src⇩C f))"
using assms(2) unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
by (metis A'.unit_simps(1) A.antipar(1) C.ideD(1) C.obj_trg
D.invert_side_of_triangle(2))
ultimately show ?thesis by simp
qed
also have "... = Φ (trg⇩C f, f) ⋅⇩D ((unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D
(?ε' ⋆⇩D F f)) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D ((F f ⋆⇩D ?η') ⋅⇩D
(F f ⋆⇩D D.inv (unit (src⇩C f)))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
using assms A.antipar A'.antipar unit_char D.whisker_left D.whisker_right
by simp
also have "... = Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D
((?ε' ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F f] ⋅⇩D (F f ⋆⇩D ?η')) ⋅⇩D
(F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
using D.comp_assoc by simp
also have "... = (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f]) ⋅⇩D
𝗋⇩D[F f] ⋅⇩D (F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
using A'.triangle_left D.comp_assoc by simp
also have "... = F 𝗅⇩C⇧-⇧1[f] ⋅⇩D F 𝗋⇩C[f]"
using assms A.antipar preserves_lunit(2) preserves_runit(1) by simp
also have "... = F (𝗅⇩C⇧-⇧1[f] ⋅⇩C 𝗋⇩C[f])"
using assms by simp
finally show ?thesis by simp
qed
ultimately show ?thesis
using is_faithful by blast
qed
show "(g ⋆⇩C ε) ⋅⇩C 𝖺⇩C[g, f, g] ⋅⇩C (η ⋆⇩C g) = 𝗋⇩C⇧-⇧1[g] ⋅⇩C 𝗅⇩C[g]"
proof -
have 1: "C.par ((g ⋆⇩C ε) ⋅⇩C 𝖺⇩C g f g ⋅⇩C (η ⋆⇩C g)) (𝗋⇩C⇧-⇧1[g] ⋅⇩C 𝗅⇩C[g])"
using assms A.antipar by auto
moreover have "F ((g ⋆⇩C ε) ⋅⇩C 𝖺⇩C[g, f, g] ⋅⇩C (η ⋆⇩C g)) = F (𝗋⇩C⇧-⇧1[g] ⋅⇩C 𝗅⇩C[g])"
proof -
have "F ((g ⋆⇩C ε) ⋅⇩C 𝖺⇩C g f g ⋅⇩C (η ⋆⇩C g)) =
F (g ⋆⇩C ε) ⋅⇩D F 𝖺⇩C[g, f, g] ⋅⇩D F (η ⋆⇩C g)"
using 1 by auto
also have "... = (F (g ⋆⇩C ε) ⋅⇩D Φ (g, f ⋆⇩C g)) ⋅⇩D (F g ⋆⇩D Φ (f, g)) ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D
(D.inv (Φ (g, f)) ⋆⇩D F g) ⋅⇩D (D.inv (Φ (g ⋆⇩C f, g)) ⋅⇩D F (η ⋆⇩C g))"
using assms A.antipar preserves_assoc(1) [of g f g] D.comp_assoc by auto
also have "... = Φ (g, src⇩C g) ⋅⇩D ((F g ⋆⇩D F ε) ⋅⇩D (F g ⋆⇩D Φ (f, g))) ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D
((D.inv (Φ (g, f)) ⋆⇩D F g) ⋅⇩D (F η ⋆⇩D F g)) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
proof -
have "F (g ⋆⇩C ε) ⋅⇩D Φ (g, f ⋆⇩C g) = Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D F ε)"
using assms Φ.naturality [of "(g, ε)"] FF_def C.VV.arr_char⇩S⇩b⇩C
C.VV.dom_simp C.VV.cod_simp
by auto
moreover have "D.inv (Φ (g ⋆⇩C f, g)) ⋅⇩D F (η ⋆⇩C g) =
(F η ⋆⇩D F g) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
proof -
have "F (η ⋆⇩C g) ⋅⇩D Φ (trg⇩C g, g) = Φ (g ⋆⇩C f, g) ⋅⇩D (F η ⋆⇩D F g)"
using assms Φ.naturality [of "(η, g)"] FF_def C.VV.arr_char⇩S⇩b⇩C A.antipar
C.VV.dom_simp C.VV.cod_simp
by auto
thus ?thesis
using assms A.antipar cmp_components_are_iso C.VV.arr_char⇩S⇩b⇩C FF_def
C.VV.dom_simp C.VV.cod_simp
D.invert_opposite_sides_of_square
[of "Φ (g ⋆⇩C f, g)" "F η ⋆⇩D F g" "F (η ⋆⇩C g)" "Φ (trg⇩C g, g)"]
by fastforce
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have " ... = Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D
(D.inv (Φ (g, f)) ⋅⇩D F η ⋆⇩D F g) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
proof -
have "(F g ⋆⇩D F ε) ⋅⇩D (F g ⋆⇩D Φ (f, g)) = F g ⋆⇩D F ε ⋅⇩D Φ (f, g)"
using assms A.antipar D.whisker_left
by (metis A'.counit_simps(1) A'.ide_right D.seqE)
moreover have "(D.inv (Φ (g, f)) ⋆⇩D F g) ⋅⇩D (F η ⋆⇩D F g) =
D.inv (Φ (g, f)) ⋅⇩D F η ⋆⇩D F g"
using assms A.antipar D.whisker_right by simp
ultimately show ?thesis by simp
qed
also have "... = Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (trg⇩C f) ⋅⇩D ?ε') ⋅⇩D
𝖺⇩D[F g, F f, F g] ⋅⇩D
(?η' ⋅⇩D D.inv (unit (src⇩C f)) ⋆⇩D F g) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
proof -
have "F ε ⋅⇩D Φ (f, g) = unit (trg⇩C f) ⋅⇩D ?ε'"
using unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
by (metis A'.counit_simps(1) C.ideD(1) C.obj_trg D.seqE assms(1))
moreover have "D.inv (Φ (g, f)) ⋅⇩D F η = ?η' ⋅⇩D D.inv (unit (src⇩C f))"
using unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
by (metis A'.unit_simps(1) A.unit_simps(1) A.unit_simps(5)
C.obj_trg D.invert_side_of_triangle(2))
ultimately show ?thesis by simp
qed
also have "... = Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (trg⇩C f)) ⋅⇩D
((F g ⋆⇩D ?ε') ⋅⇩D 𝖺⇩D[F g, F f, F g] ⋅⇩D (?η' ⋆⇩D F g)) ⋅⇩D
(D.inv (unit (src⇩C f)) ⋆⇩D F g) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
using assms A.antipar unit_char D.whisker_left D.whisker_right D.comp_assoc
by simp
also have "... = Φ (g, src⇩C g) ⋅⇩D (F g ⋆⇩D unit (trg⇩C f)) ⋅⇩D 𝗋⇩D⇧-⇧1[F g] ⋅⇩D
𝗅⇩D[F g] ⋅⇩D (D.inv (unit (src⇩C f)) ⋆⇩D F g) ⋅⇩D D.inv (Φ (trg⇩C g, g))"
using A'.triangle_right D.comp_assoc by simp
also have "... = F 𝗋⇩C⇧-⇧1[g] ⋅⇩D F 𝗅⇩C[g]"
using assms A.antipar preserves_lunit(1) preserves_runit(2) D.comp_assoc
by simp
also have "... = F (𝗋⇩C⇧-⇧1[g] ⋅⇩C 𝗅⇩C[g])"
using assms by simp
finally show ?thesis by simp
qed
ultimately show ?thesis
using is_faithful by blast
qed
qed
qed
lemma reflects_adjoint_pair:
assumes "C.ide f" and "C.ide g"
and "src⇩C f = trg⇩C g" and "src⇩C g = trg⇩C f"
and "D.adjoint_pair (F f) (F g)"
shows "C.adjoint_pair f g"
proof -
obtain η' ε' where A': "adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g) η' ε'"
using assms D.adjoint_pair_def by auto
interpret A': adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹F f› ‹F g› η' ε'
using A' by auto
have 1: "«Φ (g, f) ⋅⇩D η' ⋅⇩D D.inv (unit (src⇩C f)) : F (src⇩C f) ⇒⇩D F (g ⋆⇩C f)»"
using assms unit_char [of "src⇩C f"] A'.unit_in_hom
by (intro D.comp_in_homI, auto)
have 2: "«unit (trg⇩C f) ⋅⇩D ε' ⋅⇩D D.inv (Φ (f, g)): F (f ⋆⇩C g) ⇒⇩D F (trg⇩C f)»"
using assms cmp_in_hom [of f g] unit_char [of "trg⇩C f"] A'.counit_in_hom
by (intro D.comp_in_homI, auto)
obtain η where η: "«η : src⇩C f ⇒⇩C g ⋆⇩C f» ∧
F η = Φ (g, f) ⋅⇩D η' ⋅⇩D D.inv (unit (src⇩C f))"
using assms 1 A'.unit_in_hom cmp_in_hom locally_full by fastforce
have η': "η' = D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)"
using assms 1 η cmp_in_hom D.iso_inv_iso cmp_components_are_iso unit_char(2)
D.invert_side_of_triangle(1) [of "F η" "Φ (g, f)" "η' ⋅⇩D D.inv (unit (src⇩C f))"]
D.invert_side_of_triangle(2) [of "D.inv (Φ (g, f)) ⋅⇩D F η" η' "D.inv (unit (src⇩C f))"]
by (metis (no_types, lifting) C.ideD(1) C.obj_trg D.arrI D.comp_assoc D.inv_inv)
obtain ε where ε: "«ε : f ⋆⇩C g ⇒⇩C trg⇩C f» ∧
F ε = unit (trg⇩C f) ⋅⇩D ε' ⋅⇩D D.inv (Φ (f, g))"
using assms 2 A'.counit_in_hom cmp_in_hom locally_full by fastforce
have ε': "ε' = D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)"
using assms 2 ε cmp_in_hom D.iso_inv_iso unit_char(2) D.comp_assoc
D.invert_side_of_triangle(1) [of "F ε" "unit (trg⇩C f)" "ε' ⋅⇩D D.inv (Φ (f, g))"]
D.invert_side_of_triangle(2) [of "D.inv (unit (trg⇩C f)) ⋅⇩D F ε" ε' "D.inv (Φ (f, g))"]
by (metis (no_types, lifting) C.arrI C.ideD(1) C.obj_trg D.inv_inv cmp_components_are_iso
preserves_arr)
have "adjunction_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g)
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
using A'.adjunction_in_bicategory_axioms η' ε' by simp
hence "adjunction_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
using assms η ε reflects_adjunction by simp
thus ?thesis
using C.adjoint_pair_def by auto
qed
lemma reflects_left_adjoint:
assumes "C.ide f" and "D.is_left_adjoint (F f)"
shows "C.is_left_adjoint f"
proof -
obtain g' where g': "D.adjoint_pair (F f) g'"
using assms D.adjoint_pair_def by auto
obtain g where g: "«g : trg⇩C f →⇩C src⇩C f» ∧ C.ide g ∧ D.isomorphic (F g) g'"
using assms g' locally_essentially_surjective [of "trg⇩C f" "src⇩C f" g']
D.adjoint_pair_antipar [of "F f" g']
by auto
obtain φ where φ: "«φ : g' ⇒⇩D F g» ∧ D.iso φ"
using g D.isomorphic_def D.isomorphic_symmetric by metis
have "D.adjoint_pair (F f) (F g)"
using assms g g' φ D.adjoint_pair_preserved_by_iso [of "F f" g' "F f" "F f" φ "F g"]
by auto
thus ?thesis
using assms g reflects_adjoint_pair [of f g] D.adjoint_pair_antipar C.in_hhom_def
by auto
qed
lemma reflects_right_adjoint:
assumes "C.ide g" and "D.is_right_adjoint (F g)"
shows "C.is_right_adjoint g"
proof -
obtain f' where f': "D.adjoint_pair f' (F g)"
using assms D.adjoint_pair_def by auto
obtain f where f: "«f : trg⇩C g →⇩C src⇩C g» ∧ C.ide f ∧ D.isomorphic (F f) f'"
using assms f' locally_essentially_surjective [of "trg⇩C g" "src⇩C g" f']
D.adjoint_pair_antipar [of f' "F g"]
by auto
obtain φ where φ: "«φ : f' ⇒⇩D F f» ∧ D.iso φ"
using f D.isomorphic_def D.isomorphic_symmetric by metis
have "D.adjoint_pair (F f) (F g)"
using assms f f' φ D.adjoint_pair_preserved_by_iso [of f' "F g" φ "F f" "F g" "F g"]
by auto
thus ?thesis
using assms f reflects_adjoint_pair [of f g] D.adjoint_pair_antipar C.in_hhom_def
by auto
qed
end
subsection "Composition of Adjunctions"
text ‹
We first consider the strict case, then extend to all bicategories using strictification.
›
locale composite_adjunction_in_strict_bicategory =
strict_bicategory V H 𝖺 𝗂 src trg +
fg: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g ζ ξ +
hk: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg h k σ τ
for V :: "'a ⇒ 'a ⇒ 'a" (infixr "⋅" 55)
and H :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and 𝗂 :: "'a ⇒ 'a" ("𝗂[_]")
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a"
and f :: "'a"
and g :: "'a"
and ζ :: "'a"
and ξ :: "'a"
and h :: "'a"
and k :: "'a"
and σ :: "'a"
and τ :: "'a" +
assumes composable: "src h = trg f"
begin
abbreviation η
where "η ≡ (g ⋆ σ ⋆ f) ⋅ ζ"
abbreviation ε
where "ε ≡ τ ⋅ (h ⋆ ξ ⋆ k)"
interpretation adjunction_data_in_bicategory V H 𝖺 𝗂 src trg ‹h ⋆ f› ‹g ⋆ k› η ε
proof
show "ide (h ⋆ f)"
using composable by simp
show "ide (g ⋆ k)"
using fg.antipar hk.antipar composable by simp
show "«η : src (h ⋆ f) ⇒ (g ⋆ k) ⋆ h ⋆ f»"
proof
show "«ζ : src (h ⋆ f) ⇒ g ⋆ f»"
using fg.antipar hk.antipar composable ‹ide (h ⋆ f)› by auto
show "«g ⋆ σ ⋆ f : g ⋆ f ⇒ (g ⋆ k) ⋆ h ⋆ f»"
proof -
have "«g ⋆ σ ⋆ f : g ⋆ trg f ⋆ f ⇒ g ⋆ (k ⋆ h) ⋆ f»"
using fg.antipar hk.antipar composable hk.unit_in_hom
apply (intro hcomp_in_vhom) by auto
thus ?thesis
using hcomp_obj_arr hcomp_assoc by fastforce
qed
qed
show "«ε : (h ⋆ f) ⋆ g ⋆ k ⇒ src (g ⋆ k)»"
proof
show "«h ⋆ ξ ⋆ k : (h ⋆ f) ⋆ g ⋆ k ⇒ h ⋆ k»"
proof -
have "«h ⋆ ξ ⋆ k : h ⋆ (f ⋆ g) ⋆ k ⇒ h ⋆ trg f ⋆ k»"
using composable fg.antipar(1-2) hk.antipar(1) by fastforce
thus ?thesis
using fg.antipar hk.antipar composable hk.unit_in_hom hcomp_obj_arr hcomp_assoc
by simp
qed
show "«τ : h ⋆ k ⇒ src (g ⋆ k)»"
using fg.antipar hk.antipar composable hk.unit_in_hom by auto
qed
qed
sublocale adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg ‹h ⋆ f› ‹g ⋆ k› η ε
proof
show "(ε ⋆ h ⋆ f) ⋅ 𝖺⇧-⇧1[h ⋆ f, g ⋆ k, h ⋆ f] ⋅ ((h ⋆ f) ⋆ η) = 𝗅⇧-⇧1[h ⋆ f] ⋅ 𝗋[h ⋆ f]"
proof -
have "(ε ⋆ h ⋆ f) ⋅ 𝖺⇧-⇧1[h ⋆ f, g ⋆ k, h ⋆ f] ⋅ ((h ⋆ f) ⋆ η) =
(τ ⋅ (h ⋆ ξ ⋆ k) ⋆ h ⋆ f) ⋅ ((h ⋆ f) ⋆ (g ⋆ σ ⋆ f) ⋅ ζ)"
using fg.antipar hk.antipar composable strict_assoc comp_ide_arr
ide_left ide_right antipar(1) antipar(2)
by (metis arrI seqE strict_assoc' triangle_in_hom(1))
also have "... = (τ ⋆ h ⋆ f) ⋅ ((h ⋆ ξ ⋆ (k ⋆ h) ⋆ f) ⋅ (h ⋆ (f ⋆ g) ⋆ σ ⋆ f)) ⋅ (h ⋆ f ⋆ ζ)"
using fg.antipar hk.antipar composable whisker_left [of "h ⋆ f"] whisker_right
comp_assoc hcomp_assoc
by simp
also have "... = (τ ⋆ h ⋆ f) ⋅ (h ⋆ (ξ ⋆ (k ⋆ h)) ⋅ ((f ⋆ g) ⋆ σ) ⋆ f) ⋅ (h ⋆ f ⋆ ζ)"
using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
by simp
also have "... = (τ ⋆ h ⋆ f) ⋅ (h ⋆ (trg f ⋆ σ) ⋅ (ξ ⋆ trg f) ⋆ f) ⋅ (h ⋆ f ⋆ ζ)"
using fg.antipar hk.antipar composable comp_arr_dom comp_cod_arr
interchange [of ξ "f ⋆ g" "k ⋆ h" σ] interchange [of "trg f" ξ σ "trg f"]
by (metis fg.counit_simps(1) fg.counit_simps(2) fg.counit_simps(3)
hk.unit_simps(1) hk.unit_simps(2) hk.unit_simps(3))
also have "... = (τ ⋆ h ⋆ f) ⋅ (h ⋆ σ ⋅ ξ ⋆ f) ⋅ (h ⋆ f ⋆ ζ)"
using fg.antipar hk.antipar composable hcomp_obj_arr hcomp_arr_obj
by (metis fg.counit_simps(1) fg.counit_simps(4) hk.unit_simps(1) hk.unit_simps(5)
obj_src)
also have "... = ((τ ⋆ h ⋆ f) ⋅ (h ⋆ σ ⋆ f)) ⋅ ((h ⋆ ξ ⋆ f) ⋅ (h ⋆ f ⋆ ζ))"
using fg.antipar hk.antipar composable whisker_left whisker_right comp_assoc
by simp
also have "... = ((τ ⋆ h) ⋅ (h ⋆ σ) ⋆ f) ⋅ (h ⋆ (ξ ⋆ f) ⋅ (f ⋆ ζ))"
using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
by simp
also have "... = h ⋆ f"
using fg.antipar hk.antipar composable fg.triangle_left hk.triangle_left
by simp
also have "... = 𝗅⇧-⇧1[h ⋆ f] ⋅ 𝗋[h ⋆ f]"
using fg.antipar hk.antipar composable strict_lunit' strict_runit by simp
finally show ?thesis by simp
qed
show "((g ⋆ k) ⋆ ε) ⋅ 𝖺[g ⋆ k, h ⋆ f, g ⋆ k] ⋅ (η ⋆ g ⋆ k) = 𝗋⇧-⇧1[g ⋆ k] ⋅ 𝗅[g ⋆ k]"
proof -
have "((g ⋆ k) ⋆ ε) ⋅ 𝖺[g ⋆ k, h ⋆ f, g ⋆ k] ⋅ (η ⋆ g ⋆ k) =
((g ⋆ k) ⋆ τ ⋅ (h ⋆ ξ ⋆ k)) ⋅ ((g ⋆ σ ⋆ f) ⋅ ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable strict_assoc comp_ide_arr
ide_left ide_right
by (metis antipar(1) antipar(2) arrI seqE triangle_in_hom(2))
also have "... = (g ⋆ k ⋆ τ) ⋅ ((g ⋆ (k ⋆ h) ⋆ ξ ⋆ k) ⋅ (g ⋆ σ ⋆ (f ⋆ g) ⋆ k)) ⋅ (ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable whisker_left [of "g ⋆ k"] whisker_right
comp_assoc hcomp_assoc
by simp
also have "... = (g ⋆ k ⋆ τ) ⋅ (g ⋆ ((k ⋆ h) ⋆ ξ) ⋅ (σ ⋆ f ⋆ g) ⋆ k) ⋅ (ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
by simp
also have "... = (g ⋆ k ⋆ τ) ⋅ (g ⋆ (σ ⋆ src g) ⋅ (src g ⋆ ξ) ⋆ k) ⋅ (ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable interchange [of "k ⋆ h" σ ξ "f ⋆ g"]
interchange [of σ "src g" "src g" ξ] comp_arr_dom comp_cod_arr
by (metis fg.counit_simps(1) fg.counit_simps(2) fg.counit_simps(3)
hk.unit_simps(1) hk.unit_simps(2) hk.unit_simps(3))
also have "... = (g ⋆ k ⋆ τ) ⋅ (g ⋆ σ ⋅ ξ ⋆ k) ⋅ (ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable hcomp_obj_arr [of "src g" ξ]
hcomp_arr_obj [of σ "src g"]
by simp
also have "... = ((g ⋆ k ⋆ τ) ⋅ (g ⋆ σ ⋆ k)) ⋅ (g ⋆ ξ ⋆ k) ⋅ (ζ ⋆ g ⋆ k)"
using fg.antipar hk.antipar composable whisker_left whisker_right comp_assoc
by simp
also have "... = (g ⋆ (k ⋆ τ) ⋅ (σ ⋆ k)) ⋅ ((g ⋆ ξ) ⋅ (ζ ⋆ g) ⋆ k)"
using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
by simp
also have "... = g ⋆ k"
using fg.antipar hk.antipar composable fg.triangle_right hk.triangle_right
by simp
also have "... = 𝗋⇧-⇧1[g ⋆ k] ⋅ 𝗅[g ⋆ k]"
using fg.antipar hk.antipar composable strict_lunit strict_runit' by simp
finally show ?thesis by simp
qed
qed
lemma is_adjunction_in_strict_bicategory:
shows "adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg (h ⋆ f) (g ⋆ k) η ε"
..
end
context strict_bicategory
begin
lemma left_adjoints_compose:
assumes "is_left_adjoint f" and "is_left_adjoint f'" and "src f' = trg f"
shows "is_left_adjoint (f' ⋆ f)"
proof -
obtain g η ε where fg: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret fg: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using fg by auto
obtain g' η' ε' where f'g': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'"
using assms adjoint_pair_def by auto
interpret f'g': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'
using f'g' by auto
interpret f'fgg': composite_adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg
f g η ε f' g' η' ε'
using assms apply unfold_locales by simp
have "adjoint_pair (f' ⋆ f) (g ⋆ g')"
using adjoint_pair_def f'fgg'.adjunction_in_bicategory_axioms by auto
thus ?thesis by auto
qed
lemma right_adjoints_compose:
assumes "is_right_adjoint g" and "is_right_adjoint g'" and "src g = trg g'"
shows "is_right_adjoint (g ⋆ g')"
proof -
obtain f η ε where fg: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret fg: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using fg by auto
obtain f' η' ε' where f'g': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'"
using assms adjoint_pair_def by auto
interpret f'g': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'
using f'g' by auto
interpret f'fgg': composite_adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg
f g η ε f' g' η' ε'
using assms fg.antipar f'g'.antipar apply unfold_locales by simp
have "adjoint_pair (f' ⋆ f) (g ⋆ g')"
using adjoint_pair_def f'fgg'.adjunction_in_bicategory_axioms by auto
thus ?thesis by auto
qed
end
text ‹
We now use strictification to extend the preceding results to an arbitrary bicategory.
We only prove that ``left adjoints compose'' and ``right adjoints compose'';
I did not work out formulas for the unit and counit of the composite adjunction in the
non-strict case.
›
context bicategory
begin
interpretation S: strictified_bicategory V H 𝖺 𝗂 src trg ..
notation S.vcomp (infixr "⋅⇩S" 55)
notation S.hcomp (infixr "⋆⇩S" 53)
notation S.in_hom ("«_ : _ ⇒⇩S _»")
notation S.in_hhom ("«_ : _ →⇩S _»")
interpretation UP: fully_faithful_functor V S.vcomp S.UP
using S.UP_is_fully_faithful_functor by auto
interpretation UP: equivalence_pseudofunctor V H 𝖺 𝗂 src trg
S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmp⇩U⇩P
using S.UP_is_equivalence_pseudofunctor by auto
lemma left_adjoints_compose:
assumes "is_left_adjoint f" and "is_left_adjoint f'" and "src f = trg f'"
shows "is_left_adjoint (f ⋆ f')"
proof -
have "S.is_left_adjoint (S.UP f) ∧ S.is_left_adjoint (S.UP f')"
using assms UP.preserves_left_adjoint by simp
moreover have "S.src (S.UP f) = S.trg (S.UP f')"
using assms left_adjoint_is_ide by simp
ultimately have "S.is_left_adjoint (S.hcomp (S.UP f) (S.UP f'))"
using S.left_adjoints_compose by simp
moreover have "S.isomorphic (S.hcomp (S.UP f) (S.UP f')) (S.UP (f ⋆ f'))"
proof -
have "«S.cmp⇩U⇩P (f, f') : S.hcomp (S.UP f) (S.UP f') ⇒⇩S S.UP (f ⋆ f')»"
using assms left_adjoint_is_ide UP.cmp_in_hom by simp
moreover have "S.iso (S.cmp⇩U⇩P (f, f'))"
using assms left_adjoint_is_ide by simp
ultimately show ?thesis
using S.isomorphic_def by blast
qed
ultimately have "S.is_left_adjoint (S.UP (f ⋆ f'))"
using S.left_adjoint_preserved_by_iso S.isomorphic_def by blast
thus "is_left_adjoint (f ⋆ f')"
using assms left_adjoint_is_ide UP.reflects_left_adjoint by simp
qed
lemma right_adjoints_compose:
assumes "is_right_adjoint g" and "is_right_adjoint g'" and "src g' = trg g"
shows "is_right_adjoint (g' ⋆ g)"
proof -
have "S.is_right_adjoint (S.UP g) ∧ S.is_right_adjoint (S.UP g')"
using assms UP.preserves_right_adjoint by simp
moreover have "S.src (S.UP g') = S.trg (S.UP g)"
using assms right_adjoint_is_ide by simp
ultimately have "S.is_right_adjoint (S.hcomp (S.UP g') (S.UP g))"
using S.right_adjoints_compose by simp
moreover have "S.isomorphic (S.hcomp (S.UP g') (S.UP g)) (S.UP (g' ⋆ g))"
proof -
have "«S.cmp⇩U⇩P (g', g) : S.hcomp (S.UP g') (S.UP g) ⇒⇩S S.UP (g' ⋆ g)»"
using assms right_adjoint_is_ide UP.cmp_in_hom by simp
moreover have "S.iso (S.cmp⇩U⇩P (g', g))"
using assms right_adjoint_is_ide by simp
ultimately show ?thesis
using S.isomorphic_def by blast
qed
ultimately have "S.is_right_adjoint (S.UP (g' ⋆ g))"
using S.right_adjoint_preserved_by_iso S.isomorphic_def by blast
thus "is_right_adjoint (g' ⋆ g)"
using assms right_adjoint_is_ide UP.reflects_right_adjoint by simp
qed
end
subsection "Choosing Right Adjoints"
text ‹
It will be useful in various situations to suppose that we have made a choice of
right adjoint for each left adjoint ({\it i.e.} each ``map'') in a bicategory.
›
locale chosen_right_adjoints =
bicategory
begin
no_notation Transitive_Closure.rtrancl ("(_⇧*)" [1000] 999)
definition some_right_adjoint ("_⇧*" [1000] 1000)
where "f⇧* ≡ SOME g. adjoint_pair f g"
definition some_unit
where "some_unit f ≡ SOME η. ∃ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f⇧* η ε"
definition some_counit
where "some_counit f ≡
SOME ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f⇧* (some_unit f) ε"
lemma left_adjoint_extends_to_adjunction:
assumes "is_left_adjoint f"
shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f f⇧* (some_unit f) (some_counit f)"
using assms some_right_adjoint_def adjoint_pair_def some_unit_def some_counit_def
someI_ex [of "λg. adjoint_pair f g"]
someI_ex [of "λη. ∃ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f⇧* η ε"]
someI_ex [of "λε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f⇧* (some_unit f) ε"]
by auto
lemma left_adjoint_extends_to_adjoint_pair:
assumes "is_left_adjoint f"
shows "adjoint_pair f f⇧*"
using assms adjoint_pair_def left_adjoint_extends_to_adjunction by blast
lemma right_adjoint_in_hom [intro]:
assumes "is_left_adjoint f"
shows "«f⇧* : trg f → src f»"
and "«f⇧* : f⇧* ⇒ f⇧*»"
using assms left_adjoint_extends_to_adjoint_pair adjoint_pair_antipar [of f "f⇧*"]
by auto
lemma right_adjoint_simps [simp]:
assumes "is_left_adjoint f"
shows "ide f⇧*"
and "src f⇧* = trg f" and "trg f⇧* = src f"
and "dom f⇧* = f⇧*" and "cod f⇧* = f⇧*"
using assms right_adjoint_in_hom left_adjoint_extends_to_adjoint_pair apply auto
using assms right_adjoint_is_ide [of "f⇧*"] by blast
end
locale map_in_bicategory =
bicategory + chosen_right_adjoints +
fixes f :: 'a
assumes is_map: "is_left_adjoint f"
begin
abbreviation η
where "η ≡ some_unit f"
abbreviation ε
where "ε ≡ some_counit f"
sublocale adjunction_in_bicategory V H 𝖺 𝗂 src trg f ‹f⇧*› η ε
using is_map left_adjoint_extends_to_adjunction by simp
end
subsection "Equivalences Refine to Adjoint Equivalences"
text ‹
In this section, we show that, just as an equivalence between categories can always
be refined to an adjoint equivalence, an internal equivalence in a bicategory can also
always be so refined.
The proof, which follows that of Theorem 3.3 from \<^cite>‹"nlab-adjoint-equivalence"›,
makes use of the fact that if an internal equivalence satisfies one of the triangle
identities, then it also satisfies the other.
›
locale adjoint_equivalence_in_bicategory =
equivalence_in_bicategory +
adjunction_in_bicategory
begin
lemma dual_adjoint_equivalence:
shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg g f (inv ε) (inv η)"
proof -
interpret gf: equivalence_in_bicategory V H 𝖺 𝗂 src trg g f ‹inv ε› ‹inv η›
using dual_equivalence by simp
show ?thesis
proof
show "(inv η ⋆ g) ⋅ 𝖺⇧-⇧1[g, f, g] ⋅ (g ⋆ inv ε) = 𝗅⇧-⇧1[g] ⋅ 𝗋[g]"
proof -
have "(inv η ⋆ g) ⋅ 𝖺⇧-⇧1[g, f, g] ⋅ (g ⋆ inv ε) =
inv ((g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g))"
using antipar inv_comp isos_compose comp_assoc by simp
also have "... = inv (𝗋⇧-⇧1[g] ⋅ 𝗅[g])"
using triangle_right by simp
also have "... = 𝗅⇧-⇧1[g] ⋅ 𝗋[g]"
using inv_comp by simp
finally show ?thesis
by blast
qed
show "(f ⋆ inv η) ⋅ 𝖺[f, g, f] ⋅ (inv ε ⋆ f) = 𝗋⇧-⇧1[f] ⋅ 𝗅[f]"
proof -
have "(f ⋆ inv η) ⋅ 𝖺[f, g, f] ⋅ (inv ε ⋆ f) =
inv ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η))"
using antipar inv_comp isos_compose comp_assoc by simp
also have "... = inv (𝗅⇧-⇧1[f] ⋅ 𝗋[f])"
using triangle_left by simp
also have "... = 𝗋⇧-⇧1[f] ⋅ 𝗅[f]"
using inv_comp by simp
finally show ?thesis by blast
qed
qed
qed
end
context bicategory
begin
lemma adjoint_equivalence_preserved_by_iso_right:
assumes "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : g ⇒ g'»" and "iso φ"
shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' ((φ ⋆ f) ⋅ η) (ε ⋅ (f ⋆ inv φ))"
proof -
interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by simp
interpret fg': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' ‹(φ ⋆ f) ⋅ η› ‹ε ⋅ (f ⋆ inv φ)›
using assms fg.adjunction_in_bicategory_axioms adjunction_preserved_by_iso_right
by simp
interpret fg': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' ‹(φ ⋆ f) ⋅ η› ‹ε ⋅ (f ⋆ inv φ)›
using assms fg.equivalence_in_bicategory_axioms equivalence_preserved_by_iso_right
by simp
show ?thesis ..
qed
lemma adjoint_equivalence_preserved_by_iso_left:
assumes "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
and "«φ : f ⇒ f'»" and "iso φ"
shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g ((g ⋆ φ) ⋅ η) (ε ⋅ (inv φ ⋆ g))"
proof -
interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms by simp
interpret fg': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g ‹(g ⋆ φ) ⋅ η› ‹ε ⋅ (inv φ ⋆ g)›
using assms fg.adjunction_in_bicategory_axioms adjunction_preserved_by_iso_left
by simp
interpret fg': equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g ‹(g ⋆ φ) ⋅ η› ‹ε ⋅ (inv φ ⋆ g)›
using assms fg.equivalence_in_bicategory_axioms equivalence_preserved_by_iso_left
by simp
show ?thesis ..
qed
end
context strict_bicategory
begin
notation isomorphic (infix "≅" 50)
lemma equivalence_refines_to_adjoint_equivalence:
assumes "equivalence_map f" and "«g : trg f → src f»" and "ide g"
and "«η : src f ⇒ g ⋆ f»" and "iso η"
shows "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
proof -
obtain g' η' ε' where E': "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'"
using assms equivalence_map_def by auto
interpret E': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'
using E' by auto
let ?a = "src f" and ?b = "trg f"
have f_in_hhom: "«f : ?a → ?b»" and ide_f: "ide f"
using assms equivalence_map_def by auto
have g_in_hhom: "«g : ?b → ?a»" and ide_g: "ide g"
using assms by auto
have g'_in_hhom: "«g' : ?b → ?a»" and ide_g': "ide g'"
using assms f_in_hhom E'.antipar by auto
have η_in_hom: "«η : ?a ⇒ g ⋆ f»" and iso_η: "iso η"
using assms by auto
have a: "obj ?a" and b: "obj ?b"
using f_in_hhom by auto
have η_in_hhom: "«η : ?a → ?a»"
using a η_in_hom
by (metis arrI in_hhom_def obj_simps(2-3) vconn_implies_hpar(1-2))
text ‹
The following is quoted from \<^cite>‹"nlab-adjoint-equivalence"›:
\begin{quotation}
``Since ‹g ≅ gfg' ≅ g'›, the isomorphism ‹fg' ≅ 1› also induces an isomorphism ‹fg ≅ 1›,
which we denote ‹ξ›. Now ‹η› and ‹ξ› may not satisfy the zigzag identities, but if we
define ‹ε› by ‹ξ ⋅ (f ⋆ η⇧-⇧1) ⋅ (f ⋆ g ⋆ ξ⇧-⇧1) : f ⋆ g ⇒ 1›, then we can verify,
using string diagram notation as above,
that ‹ε› satisfies one zigzag identity, and hence (by the previous lemma) also the other.
Finally, if ‹ε': fg ⇒ 1› is any other isomorphism satisfying the zigzag identities
with ‹η›, then we have:
\[
‹ε' = ε' ⋅ (ε f g) ⋅ (f η g) = ε ⋅ (f g ε') ⋅ (f η g) = ε›
\]
using the interchange law and two zigzag identities. This shows uniqueness.''
\end{quotation}
›
have 1: "g ≅ g'"
proof -
have "g ≅ g ⋆ ?b"
using assms hcomp_arr_obj isomorphic_reflexive by auto
also have "... ≅ g ⋆ f ⋆ g'"
using assms f_in_hhom g_in_hhom g'_in_hhom E'.counit_in_vhom E'.counit_is_iso
isomorphic_def hcomp_ide_isomorphic isomorphic_symmetric
by (metis E'.counit_simps(5) in_hhomE trg_trg)
also have "... ≅ ?a ⋆ g'"
using assms f_in_hhom g_in_hhom g'_in_hhom ide_g' E'.unit_in_vhom E'.unit_is_iso
isomorphic_def hcomp_isomorphic_ide isomorphic_symmetric
by (metis hcomp_assoc hcomp_isomorphic_ide in_hhomE src_src)
also have "... ≅ g'"
using assms
by (simp add: E'.antipar(1) hcomp_obj_arr isomorphic_reflexive)
finally show ?thesis by blast
qed
have "f ⋆ g' ≅ ?b"
using E'.counit_is_iso isomorphicI [of ε'] by auto
hence 2: "f ⋆ g ≅ ?b"
using assms 1 ide_f hcomp_ide_isomorphic [of f g g'] isomorphic_transitive
isomorphic_symmetric
by (metis in_hhomE)
obtain ξ where ξ: "«ξ : f ⋆ g ⇒ ?b» ∧ iso ξ"
using 2 by auto
have ξ_in_hom: "«ξ : f ⋆ g ⇒ ?b»" and iso_ξ: "iso ξ"
using ξ by auto
have ξ_in_hhom: "«ξ : ?b → ?b»"
using b ξ_in_hom
by (metis ξ in_hhom_def iso_is_arr obj_simps(2-3) vconn_implies_hpar(1-4))
text ‹
At the time of this writing, the definition of ‹ε› given on nLab
\<^cite>‹"nlab-adjoint-equivalence"› had an apparent typo:
the expression ‹f ⋆ g ⋆ ξ⇧-⇧1› should read ‹ξ⇧-⇧1 ⋆ f ⋆ g›, as we have used here.
›
let ?ε = "ξ ⋅ (f ⋆ inv η ⋆ g) ⋅ (inv ξ ⋆ f ⋆ g)"
have ε_in_hom: "«?ε : f ⋆ g ⇒ ?b»"
proof (intro comp_in_homI)
show "«f ⋆ inv η ⋆ g : f ⋆ g ⋆ f ⋆ g ⇒ f ⋆ g»"
proof -
have "«f ⋆ inv η ⋆ g : f ⋆ (g ⋆ f) ⋆ g ⇒ f ⋆ g»"
proof -
have "«f ⋆ inv η ⋆ g : f ⋆ (g ⋆ f) ⋆ g ⇒ f ⋆ ?a ⋆ g»"
using assms η_in_hom iso_η by (intro hcomp_in_vhom) auto
thus ?thesis
using assms f_in_hhom hcomp_obj_arr by (metis in_hhomE)
qed
moreover have "f ⋆ (g ⋆ f) ⋆ g = f ⋆ g ⋆ f ⋆ g"
using hcomp_assoc by simp
ultimately show ?thesis by simp
qed
show "«inv ξ ⋆ f ⋆ g : f ⋆ g ⇒ f ⋆ g ⋆ f ⋆ g»"
proof -
have "«inv ξ ⋆ f ⋆ g : ?b ⋆ f ⋆ g ⇒ (f ⋆ g) ⋆ f ⋆ g»"
using assms ξ_in_hom iso_ξ by (intro hcomp_in_vhom, auto)
thus ?thesis
using hcomp_assoc f_in_hhom g_in_hhom b hcomp_obj_arr [of ?b "f ⋆ g"]
by fastforce
qed
show "«ξ : f ⋆ g ⇒ ?b»"
using ξ_in_hom by blast
qed
have "iso ?ε"
using f_in_hhom g_in_hhom η_in_hhom ide_f ide_g η_in_hom iso_η ξ_in_hhom ξ_in_hom iso_ξ
iso_inv_iso isos_compose
by (metis ε_in_hom arrI hseqE ide_is_iso iso_hcomp seqE)
have 4: "«inv ξ ⋆ f : ?b ⋆ f ⇒ f ⋆ g ⋆ f»"
proof -
have "«inv ξ ⋆ f : ?b ⋆ f ⇒ (f ⋆ g) ⋆ f»"
using ξ_in_hom iso_ξ f_in_hhom
by (intro hcomp_in_vhom, auto)
thus ?thesis
using hcomp_assoc by simp
qed
text ‹
First show ‹?ε› and ‹η› satisfy the ``left'' triangle identity.
›
have triangle_left: "(?ε ⋆ f) ⋅ (f ⋆ η) = f"
proof -
have "(?ε ⋆ f) ⋅ (f ⋆ η) = (ξ ⋆ f) ⋅ (f ⋆ inv η ⋆ g ⋆ f) ⋅ (inv ξ ⋆ f ⋆ g ⋆ f) ⋅ (?b ⋆ f ⋆ η)"
proof -
have "f ⋆ η = ?b ⋆ f ⋆ η"
using b η_in_hhom hcomp_obj_arr [of ?b "f ⋆ η"] by fastforce
moreover have "ξ ⋅ (f ⋆ inv η ⋆ g) ⋅ (inv ξ ⋆ f ⋆ g) ⋆ f =
(ξ ⋆ f) ⋅ ((f ⋆ inv η ⋆ g) ⋆ f) ⋅ ((inv ξ ⋆ f ⋆ g) ⋆ f)"
using ide_f ide_g ξ_in_hhom ξ_in_hom iso_ξ η_in_hhom η_in_hom iso_η whisker_right
by (metis ε_in_hom arrI seqE)
moreover have "... = (ξ ⋆ f) ⋅ (f ⋆ inv η ⋆ g ⋆ f) ⋅ (inv ξ ⋆ f ⋆ g ⋆ f)"
using hcomp_assoc by simp
ultimately show ?thesis
using comp_assoc by simp
qed
also have "... = (ξ ⋆ f) ⋅ ((f ⋆ inv η ⋆ g ⋆ f) ⋅ (f ⋆ g ⋆ f ⋆ η)) ⋅ (inv ξ ⋆ f)"
proof -
have "(inv ξ ⋆ f ⋆ g ⋆ f) ⋅ (?b ⋆ f ⋆ η) = ((inv ξ ⋆ f) ⋆ (g ⋆ f)) ⋅ ((?b ⋆ f) ⋆ η)"
using hcomp_assoc by simp
also have "... = (inv ξ ⋆ f) ⋅ (?b ⋆ f) ⋆ (g ⋆ f) ⋅ η"
proof -
have "seq (inv ξ ⋆ f) (?b ⋆ f)"
using a b 4 ide_f ide_g ξ_in_hhom ξ_in_hom iso_ξ by blast
moreover have "seq (g ⋆ f) η"
using f_in_hhom g_in_hhom ide_g ide_f η_in_hom by fast
ultimately show ?thesis
using interchange [of "inv ξ ⋆ f" "?b ⋆ f" "g ⋆ f" η] by simp
qed
also have "... = inv ξ ⋆ f ⋆ η"
using 4 comp_arr_dom comp_cod_arr η_in_hom hcomp_assoc by (metis in_homE)
also have "... = (f ⋆ g) ⋅ inv ξ ⋆ (f ⋆ η) ⋅ (f ⋆ ?a)"
proof -
have "(f ⋆ g) ⋅ inv ξ = inv ξ"
using ξ_in_hom iso_ξ comp_cod_arr by auto
moreover have "(f ⋆ η) ⋅ (f ⋆ ?a) = f ⋆ η"
proof -
have "«f ⋆ η : f ⋆ ?a ⇒ f ⋆ g ⋆ f»"
using η_in_hom by fastforce
thus ?thesis
using comp_arr_dom by blast
qed
ultimately show ?thesis by argo
qed
also have "... = ((f ⋆ g) ⋆ (f ⋆ η)) ⋅ (inv ξ ⋆ (f ⋆ ?a))"
proof -
have "seq (f ⋆ g) (inv ξ)"
using ξ_in_hom iso_ξ comp_cod_arr by auto
moreover have "seq (f ⋆ η) (f ⋆ ?a)"
using f_in_hhom η_in_hom by force
ultimately show ?thesis
using interchange by simp
qed
also have "... = (f ⋆ g ⋆ f ⋆ η) ⋅ (inv ξ ⋆ f)"
using hcomp_arr_obj hcomp_assoc by auto
finally have "(inv ξ ⋆ f ⋆ g ⋆ f) ⋅ (?b ⋆ f ⋆ η) = (f ⋆ g ⋆ f ⋆ η) ⋅ (inv ξ ⋆ f)"
by simp
thus ?thesis
using comp_assoc by simp
qed
also have "... = (ξ ⋆ f) ⋅ ((f ⋆ ?a ⋆ η) ⋅ (f ⋆ inv η ⋆ ?a)) ⋅ (inv ξ ⋆ f)"
proof -
have "(f ⋆ inv η ⋆ g ⋆ f) ⋅ (f ⋆ (g ⋆ f) ⋆ η) = f ⋆ (inv η ⋆ g ⋆ f) ⋅ ((g ⋆ f) ⋆ η)"
proof -
have "(f ⋆ (inv η ⋆ g) ⋆ f) ⋅ (f ⋆ (g ⋆ f) ⋆ η) = f ⋆ ((inv η ⋆ g) ⋆ f) ⋅ ((g ⋆ f) ⋆ η)"
proof -
have "seq ((inv η ⋆ g) ⋆ f) ((g ⋆ f) ⋆ η)"
proof -
have "seq (inv η ⋆ g ⋆ f) ((g ⋆ f) ⋆ η)"
using f_in_hhom ide_f g_in_hhom ide_g η_in_hhom η_in_hom iso_η
apply (intro seqI hseqI')
apply auto
by fastforce+
thus ?thesis
using hcomp_assoc by simp
qed
thus ?thesis
using whisker_left by simp
qed
thus ?thesis
using hcomp_assoc by simp
qed
also have "... = f ⋆ (?a ⋆ η) ⋅ (inv η ⋆ ?a)"
proof -
have "(inv η ⋆ g ⋆ f) ⋅ ((g ⋆ f) ⋆ η) = (?a ⋆ η) ⋅ (inv η ⋆ ?a)"
proof -
have "(inv η ⋆ g ⋆ f) ⋅ ((g ⋆ f) ⋆ η) = inv η ⋅ (g ⋆ f) ⋆ (g ⋆ f) ⋅ η"
using g_in_hhom ide_g η_in_hom iso_η
interchange [of "inv η" "g ⋆ f" "g ⋆ f" η]
by force
also have "... = inv η ⋆ η"
using η_in_hom iso_η comp_arr_dom comp_cod_arr by auto
also have "... = ?a ⋅ inv η ⋆ η ⋅ ?a"
using η_in_hom iso_η comp_arr_dom comp_cod_arr by auto
also have "... = (?a ⋆ η) ⋅ (inv η ⋆ ?a)"
using a η_in_hom iso_η interchange [of ?a "inv η" η ?a] by blast
finally show ?thesis by simp
qed
thus ?thesis by argo
qed
also have "... = (f ⋆ ?a ⋆ η) ⋅ (f ⋆ inv η ⋆ ?a)"
proof -
have "seq (?a ⋆ η) (inv η ⋆ ?a)"
proof (intro seqI')
show "«inv η ⋆ ?a : (g ⋆ f) ⋆ ?a ⇒ ?a ⋆ ?a»"
using a g_in_hhom η_in_hom iso_η hseqI ide_f ide_g
by (intro hcomp_in_vhom) auto
show "«?a ⋆ η : ?a ⋆ ?a ⇒ ?a ⋆ g ⋆ f»"
using a η_in_hom hseqI by (intro hcomp_in_vhom) auto
qed
thus ?thesis
using whisker_left by simp
qed
finally show ?thesis
using hcomp_assoc by simp
qed
also have "... = (ξ ⋆ f) ⋅ ((f ⋆ η) ⋅ (f ⋆ inv η)) ⋅ (inv ξ ⋆ f)"
using a η_in_hhom iso_η hcomp_obj_arr [of ?a η] hcomp_arr_obj [of "inv η" ?a] by auto
also have "... = (ξ ⋆ f) ⋅ (inv ξ ⋆ f)"
proof -
have "((f ⋆ η) ⋅ (f ⋆ inv η)) ⋅ (inv ξ ⋆ f) = (f ⋆ η ⋅ inv η) ⋅ (inv ξ ⋆ f)"
using η_in_hhom iso_η whisker_left inv_in_hom by auto
also have "... = (f ⋆ g ⋆ f) ⋅ (inv ξ ⋆ f)"
using η_in_hom iso_η comp_arr_inv inv_is_inverse by auto
also have "... = inv ξ ⋆ f"
using 4 comp_cod_arr by blast
ultimately show ?thesis by simp
qed
also have "... = f"
proof -
have "(ξ ⋆ f) ⋅ (inv ξ ⋆ f) = ξ ⋅ inv ξ ⋆ f"
using ξ_in_hhom iso_ξ whisker_right by auto
also have "... = ?b ⋆ f"
using ξ_in_hom iso_ξ comp_arr_inv' by auto
also have "... = f"
using hcomp_obj_arr by auto
finally show ?thesis by blast
qed
finally show ?thesis by blast
qed
interpret E: equivalence_in_strict_bicategory V H 𝖺 𝗂 src trg f g η ?ε
using ide_g η_in_hom ε_in_hom g_in_hhom ‹iso η› ‹iso ?ε›
by (unfold_locales, auto)
text ‹
Apply ``triangle left if and only iff right'' to show the ``right'' triangle identity.
›
have triangle_right: "((g ⋆ ξ ⋅ (f ⋆ inv η ⋆ g) ⋅ (inv ξ ⋆ f ⋆ g)) ⋅ (η ⋆ g) = g)"
using triangle_left E.triangle_left_iff_right by simp
text ‹
Use the two triangle identities to establish an adjoint equivalence and show that
there is only one choice for the counit.
›
show "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
proof -
have "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ?ε"
proof
show "(?ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
proof -
have "(?ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = (?ε ⋆ f) ⋅ (f ⋆ η)"
proof -
have "seq 𝖺⇧-⇧1[f, g, f] (f ⋆ η)"
using E.antipar
by (intro seqI, auto)
hence "𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = f ⋆ η"
using ide_f ide_g E.antipar triangle_right strict_assoc' comp_ide_arr
by presburger
thus ?thesis by simp
qed
also have "... = f"
using triangle_left by simp
also have "... = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
using strict_lunit strict_runit by simp
finally show ?thesis by simp
qed
show "(g ⋆ ?ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
proof -
have "(g ⋆ ?ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = (g ⋆ ?ε) ⋅ (η ⋆ g)"
proof -
have "seq 𝖺[g, f, g] (η ⋆ g)"
using E.antipar
by (intro seqI, auto)
hence "𝖺[g, f, g] ⋅ (η ⋆ g) = η ⋆ g"
using ide_f ide_g E.antipar triangle_right strict_assoc comp_ide_arr
by presburger
thus ?thesis by simp
qed
also have "... = g"
using triangle_right by simp
also have "... = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
using strict_lunit strict_runit by simp
finally show ?thesis by blast
qed
qed
moreover have "⋀ε ε'. ⟦ adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε;
adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε' ⟧
⟹ ε = ε'"
using adjunction_unit_determines_counit
by (meson adjoint_equivalence_in_bicategory.axioms(2))
ultimately show ?thesis by auto
qed
qed
end
text ‹
We now apply strictification to generalize the preceding result to an arbitrary bicategory.
›
context bicategory
begin
interpretation S: strictified_bicategory V H 𝖺 𝗂 src trg ..
notation S.vcomp (infixr "⋅⇩S" 55)
notation S.hcomp (infixr "⋆⇩S" 53)
notation S.in_hom ("«_ : _ ⇒⇩S _»")
notation S.in_hhom ("«_ : _ →⇩S _»")
interpretation UP: fully_faithful_functor V S.vcomp S.UP
using S.UP_is_fully_faithful_functor by auto
interpretation UP: equivalence_pseudofunctor V H 𝖺 𝗂 src trg
S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmp⇩U⇩P
using S.UP_is_equivalence_pseudofunctor by auto
interpretation UP: pseudofunctor_into_strict_bicategory V H 𝖺 𝗂 src trg
S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmp⇩U⇩P
..
lemma equivalence_refines_to_adjoint_equivalence:
assumes "equivalence_map f" and "«g : trg f → src f»" and "ide g"
and "«η : src f ⇒ g ⋆ f»" and "iso η"
shows "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
proof -
text ‹
To unpack the consequences of the assumptions, we need to obtain an
interpretation of @{locale equivalence_in_bicategory}, even though we don't
need the associated data other than ‹f›, ‹a›, and ‹b›.
›
obtain g' φ ψ where E: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' φ ψ"
using assms equivalence_map_def by auto
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' φ ψ
using E by auto
let ?a = "src f" and ?b = "trg f"
have ide_f: "ide f" by simp
have f_in_hhom: "«f : ?a → ?b»" by simp
have a: "obj ?a" and b: "obj ?b" by auto
have 1: "S.equivalence_map (S.UP f)"
using assms UP.preserves_equivalence_maps by simp
let ?η' = "S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η ⋅⇩S UP.unit ?a"
have 2: "«S.UP η : S.UP ?a ⇒⇩S S.UP (g ⋆ f)»"
using assms UP.preserves_hom [of η "src f" "g ⋆ f"] by auto
have 3: "«?η' : UP.map⇩0 ?a ⇒⇩S S.UP g ⋆⇩S S.UP f» ∧ S.iso ?η'"
proof (intro S.comp_in_homI conjI)
show "«S.inv (S.cmp⇩U⇩P (g, f)) : S.UP (g ⋆ f) ⇒⇩S S.UP g ⋆⇩S S.UP f»"
using assms UP.cmp_in_hom(2) by auto
moreover show "«UP.unit ?a : UP.map⇩0 ?a ⇒⇩S S.UP ?a»" by auto
moreover show "«S.UP η : S.UP ?a ⇒⇩S S.UP (g ⋆ f)»"
using 2 by simp
ultimately show "S.iso (S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η ⋅⇩S UP.unit ?a)"
using assms UP.cmp_components_are_iso UP.unit_char(2)
by (intro S.isos_compose) auto
qed
have ex_un_ξ': "∃!ξ'. adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
(S.UP f) (S.UP g) ?η' ξ'"
proof -
have "«S.UP g : S.trg (S.UP f) →⇩S S.src (S.UP f)»"
using assms(2) by auto
moreover have "S.ide (S.UP g)"
by (simp add: assms(3))
ultimately show ?thesis
using 1 3 S.equivalence_refines_to_adjoint_equivalence S.UP_map⇩0_obj by simp
qed
obtain ξ' where ξ': "adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
(S.UP f) (S.UP g) ?η' ξ'"
using ex_un_ξ' by auto
interpret E': adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
‹S.UP f› ‹S.UP g› ?η' ξ'
using ξ' by auto
let ?ε' = "UP.unit ?b ⋅⇩S ξ' ⋅⇩S S.inv (S.cmp⇩U⇩P (f, g))"
have ε': "«?ε' : S.UP (f ⋆ g) ⇒⇩S S.UP ?b»"
using assms(2-3) by auto
have ex_un_ε: "∃!ε. «ε : f ⋆ g ⇒ ?b» ∧ S.UP ε = ?ε'"
proof -
have "∃ε. «ε : f ⋆ g ⇒ ?b» ∧ S.UP ε = ?ε'"
proof -
have "src (f ⋆ g) = src ?b ∧ trg (f ⋆ g) = trg ?b"
using assms(2) f_in_hhom by auto
moreover have "ide (f ⋆ g)"
using assms(2-3) by auto
ultimately show ?thesis
using ε' UP.locally_full by auto
qed
moreover have
"⋀μ ν. ⟦ «μ : f ⋆ g ⇒ ?b»; S.UP μ = ?ε'; «ν : f ⋆ g ⇒ ?b»; S.UP ν = ?ε' ⟧
⟹ μ = ν"
proof -
fix μ ν
assume μ: "«μ : f ⋆ g ⇒ ?b»" and ν: "«ν : f ⋆ g ⇒ ?b»"
and 1: "S.UP μ = ?ε'" and 2: "S.UP ν = ?ε'"
have "par μ ν"
using μ ν by fastforce
thus "μ = ν"
using 1 2 UP.is_faithful [of μ ν] by simp
qed
ultimately show ?thesis by auto
qed
have iso_ε': "S.iso ?ε'"
proof (intro S.isos_compose)
show "S.iso (S.inv (S.cmp⇩U⇩P (f, g)))"
using assms UP.cmp_components_are_iso by auto
show "S.iso ξ'"
using E'.counit_is_iso by blast
show "S.iso (UP.unit ?b)"
using b UP.unit_char(2) by simp
show "S.seq (UP.unit ?b) (ξ' ⋅⇩S S.inv (S.cmp⇩U⇩P (f, g)))"
proof (intro S.seqI')
show "«UP.unit ?b : UP.map⇩0 ?b ⇒⇩S S.UP ?b»"
using b UP.unit_char by simp
show "«ξ' ⋅⇩S S.inv (S.cmp⇩U⇩P (f, g)) : S.UP (f ⋆ g) ⇒⇩S UP.map⇩0 ?b»"
using assms by auto
qed
thus "S.seq ξ' (S.inv (S.cmp⇩U⇩P (f, g)))" by auto
qed
obtain ε where ε: "«ε : f ⋆ g ⇒ ?b» ∧ S.UP ε = ?ε'"
using ex_un_ε by auto
interpret E'': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using assms(1,3-5)
apply unfold_locales
apply simp_all
using assms(2) ε
apply auto[1]
using ε iso_ε' UP.reflects_iso [of ε]
by auto
interpret E'': adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
proof
show "(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) = 𝗅⇧-⇧1[f] ⋅ 𝗋[f]"
proof -
have "S.UP ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) =
S.cmp⇩U⇩P (trg f, f) ⋅⇩S (S.UP ε ⋅⇩S S.cmp⇩U⇩P (f, g) ⋆⇩S S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S S.inv (S.cmp⇩U⇩P (f, src f))"
using E''.UP_triangle(3) by simp
also have "... = S.cmp⇩U⇩P (trg f, f) ⋅⇩S
(UP.unit ?b ⋅⇩S ξ' ⋅⇩S S.inv (S.cmp⇩U⇩P (f, g)) ⋅⇩S S.cmp⇩U⇩P (f, g) ⋆⇩S S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S S.inv (S.cmp⇩U⇩P (f, src f))"
using ε S.comp_assoc by simp
also have "... = S.cmp⇩U⇩P (trg f, f) ⋅⇩S (UP.unit ?b ⋅⇩S ξ' ⋆⇩S S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S
S.inv (S.cmp⇩U⇩P (f, src f))"
proof -
have "ξ' ⋅⇩S S.inv (S.cmp⇩U⇩P (f, g)) ⋅⇩S S.cmp⇩U⇩P (f, g) = ξ'"
proof -
have "S.iso (S.cmp⇩U⇩P (f, g))"
using assms by auto
moreover have "S.dom (S.cmp⇩U⇩P (f, g)) = S.UP f ⋆⇩S S.UP g"
using assms by auto
ultimately have "S.inv (S.cmp⇩U⇩P (f, g)) ⋅⇩S S.cmp⇩U⇩P (f, g) = S.UP f ⋆⇩S S.UP g"
using S.comp_inv_arr' by simp
thus ?thesis
using S.comp_arr_dom E'.counit_in_hom(2) by simp
qed
thus ?thesis by argo
qed
also have
"... = S.cmp⇩U⇩P (trg f, f) ⋅⇩S (UP.unit ?b ⋆⇩S S.UP f) ⋅⇩S
((ξ' ⋆⇩S S.UP f) ⋅⇩S (S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f))) ⋅⇩S
(S.UP f ⋆⇩S S.UP η)) ⋅⇩S
S.inv (S.cmp⇩U⇩P (f, src f))"
proof -
have "UP.unit ?b ⋅⇩S ξ' ⋆⇩S S.UP f = (UP.unit ?b ⋆⇩S S.UP f) ⋅⇩S (ξ' ⋆⇩S S.UP f)"
using assms b UP.unit_char S.whisker_right S.UP_map⇩0_obj by auto
moreover have "S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η =
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f))) ⋅⇩S (S.UP f ⋆⇩S S.UP η)"
using assms S.whisker_left by auto
ultimately show ?thesis
using S.comp_assoc by simp
qed
also have "... = (S.cmp⇩U⇩P (trg f, f) ⋅⇩S (UP.unit ?b ⋆⇩S S.UP f)) ⋅⇩S
(S.UP f ⋆⇩S S.inv (UP.unit (src f))) ⋅⇩S S.inv (S.cmp⇩U⇩P (f, src f))"
proof -
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S (S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f))) ⋅⇩S (S.UP f ⋆⇩S S.UP η)
= (S.UP f ⋆⇩S S.inv (UP.unit (src f)))"
proof -
have "(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f))) ⋅⇩S (S.UP f ⋆⇩S S.UP η) =
S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η"
using assms S.whisker_left by auto
hence "((ξ' ⋆⇩S S.UP f) ⋅⇩S (S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f))) ⋅⇩S (S.UP f ⋆⇩S S.UP η))
= ((ξ' ⋆⇩S S.UP f) ⋅⇩S (S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η))"
by simp
also have "... = ((ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f)) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η)"
proof -
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) = ξ' ⋆⇩S S.UP f"
proof -
have "«ξ' ⋆⇩S S.UP f :
(S.UP f ⋆⇩S S.UP g) ⋆⇩S S.UP f ⇒⇩S S.trg (S.UP f) ⋆⇩S S.UP f»"
using assms by auto
moreover have "«S.𝖺' (S.UP f) (S.UP g) (S.UP f) :
S.UP f ⋆⇩S S.UP g ⋆⇩S S.UP f ⇒⇩S (S.UP f ⋆⇩S S.UP g) ⋆⇩S S.UP f»"
using assms S.assoc'_in_hom by auto
ultimately show ?thesis
using assms S.strict_assoc' S.iso_assoc S.hcomp_assoc E'.antipar
S.comp_arr_ide S.seqI'
by (metis (no_types, lifting) E'.ide_left E'.ide_right)
qed
thus ?thesis
using S.comp_assoc by simp
qed
also have "... = ((ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η))"
using S.comp_assoc by simp
also have "... = (S.UP f ⋆⇩S S.inv (UP.unit (src f)))"
proof -
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) =
(S.UP f ⋆⇩S S.inv (UP.unit (src f)))"
proof -
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S
(S.UP f ⋆⇩S UP.unit ?a) =
S.lunit' (S.UP f) ⋅⇩S S.runit (S.UP f)"
proof -
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S
(S.UP f ⋆⇩S UP.unit ?a) =
(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η ⋅⇩S UP.unit ?a)"
proof -
have "S.seq (S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) (UP.unit ?a)"
using assms UP.unit_char UP.cmp_components_are_iso
E'.unit_simps(1) S.comp_assoc
by presburger
hence "(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) ⋅⇩S
(S.UP f ⋆⇩S UP.unit ?a) =
S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η ⋅⇩S UP.unit ?a"
using assms UP.unit_char UP.cmp_components_are_iso S.comp_assoc
S.whisker_left [of "S.UP f" "S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η" "UP.unit ?a"]
by simp
thus ?thesis by simp
qed
thus ?thesis
using assms E'.triangle_left UP.cmp_components_are_iso UP.unit_char
by argo
qed
also have "... = S.UP f"
using S.strict_lunit' S.strict_runit by simp
finally have 1: "((ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η)) ⋅⇩S
(S.UP f ⋆⇩S UP.unit ?a) = S.UP f"
using S.comp_assoc by simp
have "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η) =
S.UP f ⋅⇩S (S.UP f ⋆⇩S S.inv (UP.unit ?a))"
proof -
have "S.arr (S.UP f)"
using assms by simp
moreover have "S.iso (S.UP f ⋆⇩S UP.unit ?a)"
using assms UP.unit_char S.UP_map⇩0_obj by auto
moreover have "S.inv (S.UP f ⋆⇩S UP.unit ?a) =
S.UP f ⋆⇩S S.inv (UP.unit ?a)"
using assms a UP.unit_char S.UP_map⇩0_obj by auto
ultimately show ?thesis
using assms 1 UP.unit_char UP.cmp_components_are_iso
S.invert_side_of_triangle(2)
[of "S.UP f" "(ξ' ⋆⇩S S.UP f) ⋅⇩S S.𝖺' (S.UP f) (S.UP g) (S.UP f) ⋅⇩S
(S.UP f ⋆⇩S S.inv (S.cmp⇩U⇩P (g, f)) ⋅⇩S S.UP η)"
"S.UP f ⋆⇩S UP.unit ?a"]
by presburger
qed
also have "... = S.UP f ⋆⇩S S.inv (UP.unit ?a)"
proof -
have "«S.UP f ⋆⇩S S.inv (UP.unit ?a) :
S.UP f ⋆⇩S S.UP ?a ⇒⇩S S.UP f ⋆⇩S UP.map⇩0 ?a»"
using assms ide_f f_in_hhom UP.unit_char [of ?a] S.inv_in_hom
apply (intro S.hcomp_in_vhom)
apply auto[1]
apply blast
by auto
moreover have "S.UP f ⋆⇩S UP.map⇩0 ?a = S.UP f"
using a S.hcomp_arr_obj S.UP_map⇩0_obj by auto
finally show ?thesis
using S.comp_cod_arr by blast
qed
finally show ?thesis by auto
qed
thus ?thesis
using S.comp_assoc by simp
qed
finally show ?thesis by simp
qed
thus ?thesis
using S.comp_assoc by simp
qed
also have "... = S.UP 𝗅⇧-⇧1[f] ⋅⇩S S.UP 𝗋[f]"
proof -
have "S.cmp⇩U⇩P (trg f, f) ⋅⇩S (UP.unit ?b ⋆⇩S S.UP f) = S.UP 𝗅⇧-⇧1[f]"
proof -
have "S.UP f = S.UP 𝗅[f] ⋅⇩S S.cmp⇩U⇩P (trg f, f) ⋅⇩S (UP.unit (trg f) ⋆⇩S S.UP f)"
using UP.lunit_coherence iso_lunit S.strict_lunit by simp
thus ?thesis
using UP.image_of_unitor(3) ide_f by presburger
qed
moreover have "(S.UP f ⋆⇩S S.inv (UP.unit (src f))) ⋅⇩S S.inv (S.cmp⇩U⇩P (f, src f))
= S.UP 𝗋[f]"
proof -
have "S.UP 𝗋[f] ⋅⇩S S.cmp⇩U⇩P (f, src f) ⋅⇩S (S.UP f ⋆⇩S UP.unit (src f)) = S.UP f"
using UP.runit_coherence [of f] S.strict_runit by simp
moreover have "S.iso (S.cmp⇩U⇩P (f, src f) ⋅⇩S (S.UP f ⋆⇩S UP.unit (src f)))"
using UP.unit_char UP.cmp_components_are_iso VV.arr_char⇩S⇩b⇩C S.UP_map⇩0_obj
by (intro S.isos_compose) auto
ultimately have
"S.UP 𝗋[f] = S.UP f ⋅⇩S S.inv (S.cmp⇩U⇩P (f, src f) ⋅⇩S (S.UP f ⋆⇩S UP.unit (src f)))"
using S.invert_side_of_triangle(2)
[of "S.UP f" "S.UP 𝗋[f]" "S.cmp⇩U⇩P (f, src f) ⋅⇩S (S.UP f ⋆⇩S UP.unit (src f))"]
ideD(1) ide_f by blast
thus ?thesis
using ide_f UP.image_of_unitor(2) [of f] by argo
qed
ultimately show ?thesis
using S.comp_assoc by simp
qed
also have "... = S.UP (𝗅⇧-⇧1[f] ⋅ 𝗋[f])"
by simp
finally have "S.UP ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) = S.UP (𝗅⇧-⇧1[f] ⋅ 𝗋[f])"
by simp
moreover have "par ((ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η)) (𝗅⇧-⇧1[f] ⋅ 𝗋[f])"
proof -
have "«(ε ⋆ f) ⋅ 𝖺⇧-⇧1[f, g, f] ⋅ (f ⋆ η) : f ⋆ src f ⇒ trg f ⋆ f»"
using E''.triangle_in_hom(1) by simp
moreover have "«𝗅⇧-⇧1[f] ⋅ 𝗋[f] : f ⋆ src f ⇒ trg f ⋆ f»" by auto
ultimately show ?thesis
by (metis in_homE)
qed
ultimately show ?thesis
using UP.is_faithful by blast
qed
thus "(g ⋆ ε) ⋅ 𝖺[g, f, g] ⋅ (η ⋆ g) = 𝗋⇧-⇧1[g] ⋅ 𝗅[g]"
using E''.triangle_left_implies_right by simp
qed
show ?thesis
using E''.adjoint_equivalence_in_bicategory_axioms E''.adjunction_in_bicategory_axioms
adjunction_unit_determines_counit adjoint_equivalence_in_bicategory_def
by metis
qed
lemma equivalence_map_extends_to_adjoint_equivalence:
assumes "equivalence_map f"
shows "∃g η ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
proof -
obtain g η ε' where E: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'"
using assms equivalence_map_def by auto
interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
using E by auto
obtain ε where A: "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms equivalence_refines_to_adjoint_equivalence [of f g η]
E.antipar E.unit_is_iso E.unit_in_hom by auto
show ?thesis
using E A by blast
qed
end
subsection "Uniqueness of Adjoints"
text ‹
Left and right adjoints determine each other up to isomorphism.
›
context strict_bicategory
begin
lemma left_adjoint_determines_right_up_to_iso:
assumes "adjoint_pair f g" and "adjoint_pair f g'"
shows "g ≅ g'"
proof -
obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using A by auto
interpret A: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g η ε ..
obtain η' ε' where A': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'"
using assms adjoint_pair_def by auto
interpret A': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'
using A' by auto
interpret A': adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g' η' ε' ..
let ?φ = "A'.trnl⇩η g ε"
have "«?φ: g ⇒ g'»"
using A'.trnl⇩η_eq A'.adjoint_transpose_left(1) [of "trg f" g] A.antipar A'.antipar
hcomp_arr_obj
by auto
moreover have "iso ?φ"
proof (intro isoI)
let ?ψ = "A.trnl⇩η g' ε'"
show "inverse_arrows ?φ ?ψ"
proof
show "ide (?φ ⋅ ?ψ)"
proof -
have 1: "ide (trg f) ∧ trg (trg f) = trg f"
by simp
have "?φ ⋅ ?ψ = (g' ⋆ ε) ⋅ ((η' ⋆ g) ⋅ (g ⋆ ε')) ⋅ (η ⋆ g')"
using 1 A.antipar A'.antipar A.trnl⇩η_eq [of "trg f" g' ε']
A'.trnl⇩η_eq [of "trg f" g ε] comp_assoc A.counit_in_hom A'.counit_in_hom
by simp
also have "... = ((g' ⋆ ε) ⋅ (g' ⋆ f ⋆ g ⋆ ε')) ⋅ ((η' ⋆ g ⋆ f ⋆ g') ⋅ (η ⋆ g'))"
proof -
have "(η' ⋆ g) ⋅ (g ⋆ ε') = (η' ⋆ g ⋆ trg f) ⋅ (src f ⋆ g ⋆ ε')"
using A.antipar A'.antipar hcomp_arr_obj hcomp_obj_arr [of "src f" "g ⋆ ε'"]
hseqI'
by (metis A'.counit_simps(1) A'.counit_simps(5) A.ide_right ideD(1)
obj_trg trg_hcomp)
also have "... = η' ⋆ g ⋆ ε'"
using A.antipar A'.antipar interchange [of η' "src f" "g ⋆ trg f" "g ⋆ ε'"]
whisker_left comp_arr_dom comp_cod_arr
by simp
also have "... = ((g' ⋆ f) ⋆ g ⋆ ε') ⋅ (η' ⋆ g ⋆ (f ⋆ g'))"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
A'.unit_in_hom A'.counit_in_hom interchange whisker_left
comp_arr_dom comp_cod_arr
by (metis A'.counit_simps(1-2,5) A'.unit_simps(1,3) hseqI' ide_char)
also have "... = (g' ⋆ f ⋆ g ⋆ ε') ⋅ (η' ⋆ g ⋆ f ⋆ g')"
using hcomp_assoc by simp
finally show ?thesis
using comp_assoc by simp
qed
also have "... = (g' ⋆ ε') ⋅ ((g' ⋆ (ε ⋆ f) ⋆ g') ⋅ (g' ⋆ (f ⋆ η) ⋆ g')) ⋅ (η' ⋆ g')"
proof -
have "(g' ⋆ ε) ⋅ (g' ⋆ f ⋆ g ⋆ ε') = (g' ⋆ ε') ⋅ (g' ⋆ ε ⋆ f ⋆ g')"
proof -
have "(g' ⋆ ε) ⋅ (g' ⋆ f ⋆ g ⋆ ε') = g' ⋆ ε ⋆ ε'"
proof -
have "ε ⋅ (f ⋆ g ⋆ ε') = ε ⋆ ε'"
using A.ide_left A.ide_right A.antipar A'.antipar hcomp_arr_obj comp_arr_dom
comp_cod_arr interchange obj_src trg_src
by (metis A'.counit_simps(1,3) A.counit_simps(1-2,4) hcomp_assoc)
thus ?thesis
using A.antipar A'.antipar whisker_left [of g' ε "f ⋆ g ⋆ ε'"]
by (simp add: hcomp_assoc)
qed
also have "... = (g' ⋆ ε') ⋅ (g' ⋆ ε ⋆ f ⋆ g')"
proof -
have "ε ⋆ ε' = ε' ⋅ (ε ⋆ f ⋆ g')"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
hcomp_obj_arr hcomp_arr_obj comp_arr_dom comp_cod_arr interchange
obj_src trg_src
by (metis A'.counit_simps(1-2,5) A.counit_simps(1,3-4) arr_cod
not_arr_null seq_if_composable)
thus ?thesis
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
whisker_left
by (metis A'.counit_simps(1,5) A.counit_simps(1,4) hseqI')
qed
finally show ?thesis by simp
qed
moreover have "(η' ⋆ g ⋆ f ⋆ g') ⋅ (η ⋆ g') = (g' ⋆ f ⋆ η ⋆ g') ⋅ (η' ⋆ g')"
proof -
have "(η' ⋆ g ⋆ f ⋆ g') ⋅ (η ⋆ g') = η' ⋆ η ⋆ g'"
proof -
have "(η' ⋆ g ⋆ f) ⋅ η = η' ⋆ η"
using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
interchange comp_arr_dom comp_cod_arr
by (metis A'.unit_simps(1-2,4) A.unit_simps(1,3,5) hcomp_obj_arr obj_trg)
thus ?thesis
using A.antipar A'.antipar whisker_right [of g' "η' ⋆ g ⋆ f" η]
by (simp add: hcomp_assoc)
qed
also have "... = (g' ⋆ f ⋆ η ⋆ g') ⋅ (η' ⋆ g')"
proof -
have "η' ⋆ η = (g' ⋆ f ⋆ η) ⋅ η'"
using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
comp_arr_dom comp_cod_arr hcomp_assoc interchange
by (metis A'.unit_simps(1,3-4) A.unit_simps(1-2) obj_src)
thus ?thesis
using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
whisker_right [of g' "g' ⋆ f ⋆ η" η']
by (metis A'.ide_right A'.unit_simps(1,4) A.unit_simps(1,5)
hseqI' hcomp_assoc)
qed
finally show ?thesis by simp
qed
ultimately show ?thesis
using comp_assoc hcomp_assoc by simp
qed
also have "... = (g' ⋆ ε') ⋅ ((g' ⋆ f) ⋆ g') ⋅ (η' ⋆ g')"
proof -
have "(g' ⋆ (ε ⋆ f) ⋆ g') ⋅ (g' ⋆ (f ⋆ η) ⋆ g') = g' ⋆ f ⋆ g'"
proof -
have "(g' ⋆ (ε ⋆ f) ⋆ g') ⋅ (g' ⋆ (f ⋆ η) ⋆ g') =
g' ⋆ ((ε ⋆ f) ⋆ g') ⋅ ((f ⋆ η) ⋆ g')"
using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom
A'.counit_in_hom whisker_left [of g' "(ε ⋆ f) ⋆ g'" "(f ⋆ η) ⋆ g'"]
by (metis A'.ide_right A.triangle_left hseqI' ideD(1) whisker_right)
also have "... = g' ⋆ (ε ⋆ f) ⋅ (f ⋆ η) ⋆ g'"
using A.antipar A'.antipar whisker_right [of g' "ε ⋆ f" "f ⋆ η"]
by (simp add: A.triangle_left)
also have "... = g' ⋆ f ⋆ g'"
using A.triangle_left by simp
finally show ?thesis by simp
qed
thus ?thesis
using hcomp_assoc by simp
qed
also have "... = (g' ⋆ ε') ⋅ (η' ⋆ g')"
using A.antipar A'.antipar A'.unit_in_hom A'.counit_in_hom comp_cod_arr
by (metis A'.ide_right A'.triangle_in_hom(2) A.ide_left arrI assoc_is_natural_2
ide_char seqE strict_assoc)
also have "... = g'"
using A'.triangle_right by simp
finally have "?φ ⋅ ?ψ = g'" by simp
thus ?thesis by simp
qed
show "ide (?ψ ⋅ ?φ)"
proof -
have 1: "ide (trg f) ∧ trg (trg f) = trg f"
by simp
have "?ψ ⋅ ?φ = (g ⋆ ε') ⋅ ((η ⋆ g') ⋅ (g' ⋆ ε)) ⋅ (η' ⋆ g)"
using A.antipar A'.antipar A'.trnl⇩η_eq [of "trg f" g ε]
A.trnl⇩η_eq [of "trg f" g' ε'] comp_assoc A.counit_in_hom A'.counit_in_hom
by simp
also have "... = ((g ⋆ ε') ⋅ (g ⋆ f ⋆ g' ⋆ ε)) ⋅ ((η ⋆ g' ⋆ f ⋆ g) ⋅ (η' ⋆ g))"
proof -
have "(η ⋆ g') ⋅ (g' ⋆ ε) = (η ⋆ g' ⋆ trg f) ⋅ (src f ⋆ g' ⋆ ε)"
using A.antipar A'.antipar hcomp_arr_obj hcomp_obj_arr hseqI'
by (metis A'.ide_right A.unit_simps(1,4) hcomp_assoc hcomp_obj_arr
ideD(1) obj_src)
also have "... = η ⋆ g' ⋆ ε"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
A.counit_in_hom interchange
by (metis "1" A.counit_simps(5) A.unit_simps(4) hseqI' ide_def ide_in_hom(2)
not_arr_null seqI' src.preserves_ide)
also have "... = ((g ⋆ f) ⋆ g' ⋆ ε) ⋅ (η ⋆ g' ⋆ (f ⋆ g))"
using A'.ide_right A'.antipar interchange ide_char comp_arr_dom comp_cod_arr hseqI'
by (metis A.counit_simps(1-2,5) A.unit_simps(1,3))
also have "... = (g ⋆ f ⋆ g' ⋆ ε) ⋅ (η ⋆ g' ⋆ f ⋆ g)"
using hcomp_assoc by simp
finally show ?thesis
using comp_assoc by simp
qed
also have "... = (g ⋆ ε) ⋅ ((g ⋆ (ε' ⋆ f) ⋆ g) ⋅ (g ⋆ (f ⋆ η') ⋆ g)) ⋅ (η ⋆ g)"
proof -
have "(g ⋆ ε') ⋅ (g ⋆ f ⋆ g' ⋆ ε) = (g ⋆ ε) ⋅ (g ⋆ ε' ⋆ f ⋆ g)"
proof -
have "(g ⋆ ε') ⋅ (g ⋆ f ⋆ g' ⋆ ε) = g ⋆ ε' ⋆ ε"
proof -
have "ε' ⋅ (f ⋆ g' ⋆ ε) = ε' ⋆ ε"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar hcomp_arr_obj
comp_arr_dom comp_cod_arr interchange obj_src trg_src hcomp_assoc
by (metis A.counit_simps(1,3) A'.counit_simps(1-2,4))
thus ?thesis
using A.antipar A'.antipar whisker_left [of g ε' "f ⋆ g' ⋆ ε"]
by (simp add: hcomp_assoc)
qed
also have "... = (g ⋆ ε) ⋅ (g ⋆ ε' ⋆ f ⋆ g)"
proof -
have "ε' ⋆ ε = ε ⋅ (ε' ⋆ f ⋆ g)"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar hcomp_obj_arr
hcomp_arr_obj comp_arr_dom comp_cod_arr interchange obj_src trg_src
by (metis A.counit_simps(1-2,5) A'.counit_simps(1,3-4)
arr_cod not_arr_null seq_if_composable)
thus ?thesis
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
whisker_left
by (metis A.counit_simps(1,5) A'.counit_simps(1,4) hseqI')
qed
finally show ?thesis by simp
qed
moreover have "(η ⋆ g' ⋆ f ⋆ g) ⋅ (η' ⋆ g) = (g ⋆ f ⋆ η' ⋆ g) ⋅ (η ⋆ g)"
proof -
have "(η ⋆ g' ⋆ f ⋆ g) ⋅ (η' ⋆ g) = η ⋆ η' ⋆ g"
proof -
have "(η ⋆ g' ⋆ f) ⋅ η' = η ⋆ η'"
using A.antipar A'.antipar A.unit_in_hom hcomp_arr_obj
comp_arr_dom comp_cod_arr hcomp_obj_arr interchange
by (metis A'.unit_simps(1,3,5) A.unit_simps(1-2,4) obj_trg)
thus ?thesis
using A.antipar A'.antipar whisker_right [of g "η ⋆ g' ⋆ f" η']
by (simp add: hcomp_assoc)
qed
also have "... = ((g ⋆ f) ⋆ η' ⋆ g) ⋅ (η ⋆ src f ⋆ g)"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
A'.unit_in_hom comp_arr_dom comp_cod_arr interchange
by (metis A'.unit_simps(1-2,4) A.unit_simps(1,3) hseqI' ide_char)
also have "... = (g ⋆ f ⋆ η' ⋆ g) ⋅ (η ⋆ g)"
using A.antipar A'.antipar hcomp_assoc
by (simp add: hcomp_obj_arr)
finally show ?thesis by simp
qed
ultimately show ?thesis
using comp_assoc hcomp_assoc by simp
qed
also have "... = (g ⋆ ε) ⋅ ((g ⋆ f) ⋆ g) ⋅ (η ⋆ g)"
proof -
have "(g ⋆ (ε' ⋆ f) ⋆ g) ⋅ (g ⋆ (f ⋆ η') ⋆ g) = g ⋆ f ⋆ g"
proof -
have "(g ⋆ (ε' ⋆ f) ⋆ g) ⋅ (g ⋆ (f ⋆ η') ⋆ g) =
g ⋆ ((ε' ⋆ f) ⋆ g) ⋅ ((f ⋆ η') ⋆ g)"
using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
A.counit_in_hom whisker_left
by (metis A'.triangle_left hseqI' ideD(1) whisker_right)
also have "... = g ⋆ (ε' ⋆ f) ⋅ (f ⋆ η') ⋆ g"
using A.antipar A'.antipar whisker_right [of g "ε' ⋆ f" "f ⋆ η'"]
by (simp add: A'.triangle_left)
also have "... = g ⋆ f ⋆ g"
using A'.triangle_left by simp
finally show ?thesis by simp
qed
thus ?thesis
using hcomp_assoc by simp
qed
also have "... = (g ⋆ ε) ⋅ (η ⋆ g)"
using A.antipar A'.antipar A.unit_in_hom A.counit_in_hom comp_cod_arr
by (metis A.ide_left A.ide_right A.triangle_in_hom(2) arrI assoc_is_natural_2
ide_char seqE strict_assoc)
also have "... = g"
using A.triangle_right by simp
finally have "?ψ ⋅ ?φ = g" by simp
moreover have "ide g"
by simp
ultimately show ?thesis by simp
qed
qed
qed
ultimately show ?thesis
using isomorphic_def by auto
qed
end
text ‹
We now use strictification to extend to arbitrary bicategories.
›
context bicategory
begin
interpretation S: strictified_bicategory V H 𝖺 𝗂 src trg ..
notation S.vcomp (infixr "⋅⇩S" 55)
notation S.hcomp (infixr "⋆⇩S" 53)
notation S.in_hom ("«_ : _ ⇒⇩S _»")
notation S.in_hhom ("«_ : _ →⇩S _»")
interpretation UP: equivalence_pseudofunctor V H 𝖺 𝗂 src trg
S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmp⇩U⇩P
using S.UP_is_equivalence_pseudofunctor by auto
interpretation UP: pseudofunctor_into_strict_bicategory V H 𝖺 𝗂 src trg
S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmp⇩U⇩P
..
interpretation UP: fully_faithful_functor V S.vcomp S.UP
using S.UP_is_fully_faithful_functor by auto
lemma left_adjoint_determines_right_up_to_iso:
assumes "adjoint_pair f g" and "adjoint_pair f g'"
shows "g ≅ g'"
proof -
have 0: "ide g ∧ ide g'"
using assms adjoint_pair_def adjunction_in_bicategory_def
adjunction_data_in_bicategory_def adjunction_data_in_bicategory_axioms_def
by metis
have 1: "S.adjoint_pair (S.UP f) (S.UP g) ∧ S.adjoint_pair (S.UP f) (S.UP g')"
using assms UP.preserves_adjoint_pair by simp
obtain ν where ν: "«ν : S.UP g ⇒⇩S S.UP g'» ∧ S.iso ν"
using 1 S.left_adjoint_determines_right_up_to_iso S.isomorphic_def by blast
obtain μ where μ: "«μ : g ⇒ g'» ∧ S.UP μ = ν"
using 0 ν UP.is_full [of g' g ν] by auto
have "«μ : g ⇒ g'» ∧ iso μ"
using μ ν UP.reflects_iso by auto
thus ?thesis
using isomorphic_def by auto
qed
lemma right_adjoint_determines_left_up_to_iso:
assumes "adjoint_pair f g" and "adjoint_pair f' g"
shows "f ≅ f'"
proof -
obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using A by auto
obtain η' ε' where A': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g η' ε'"
using assms adjoint_pair_def by auto
interpret A': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g η' ε'
using A' by auto
interpret Cop: op_bicategory V H 𝖺 𝗂 src trg ..
interpret Aop: adjunction_in_bicategory V Cop.H Cop.𝖺 𝗂 Cop.src Cop.trg g f η ε
using A.antipar A.triangle_left A.triangle_right Cop.assoc_ide_simp
Cop.lunit_ide_simp Cop.runit_ide_simp
by (unfold_locales, auto)
interpret Aop': adjunction_in_bicategory V Cop.H Cop.𝖺 𝗂 Cop.src Cop.trg g f' η' ε'
using A'.antipar A'.triangle_left A'.triangle_right Cop.assoc_ide_simp
Cop.lunit_ide_simp Cop.runit_ide_simp
by (unfold_locales, auto)
show ?thesis
using Aop.adjunction_in_bicategory_axioms Aop'.adjunction_in_bicategory_axioms
Cop.left_adjoint_determines_right_up_to_iso Cop.adjoint_pair_def
by blast
qed
end
context chosen_right_adjoints
begin
lemma isomorphic_to_left_adjoint_implies_isomorphic_right_adjoint:
assumes "is_left_adjoint f" and "f ≅ h"
shows "f⇧* ≅ h⇧*"
proof -
have 1: "adjoint_pair f f⇧*"
using assms left_adjoint_extends_to_adjoint_pair by blast
moreover have "adjoint_pair h f⇧*"
using assms 1 adjoint_pair_preserved_by_iso isomorphic_symmetric isomorphic_reflexive
by (meson isomorphic_def right_adjoint_simps(1))
thus ?thesis
using left_adjoint_determines_right_up_to_iso left_adjoint_extends_to_adjoint_pair
by blast
qed
end
context bicategory
begin
lemma equivalence_is_adjoint:
assumes "equivalence_map f"
shows equivalence_is_left_adjoint: "is_left_adjoint f"
and equivalence_is_right_adjoint: "is_right_adjoint f"
proof -
obtain g η ε where fg: "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms equivalence_map_extends_to_adjoint_equivalence by blast
interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using fg by simp
interpret gf: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg g f ‹inv ε› ‹inv η›
using fg.dual_adjoint_equivalence by simp
show "is_left_adjoint f"
using fg.adjunction_in_bicategory_axioms adjoint_pair_def by auto
show "is_right_adjoint f"
using gf.adjunction_in_bicategory_axioms adjoint_pair_def by auto
qed
lemma right_adjoint_to_equivalence_is_equivalence:
assumes "equivalence_map f" and "adjoint_pair f g"
shows "equivalence_map g"
proof -
obtain η ε where fg: "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε"
using assms adjoint_pair_def by auto
interpret fg: adjunction_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg f g η ε
using fg by simp
obtain g' φ ψ where fg': "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ"
using assms equivalence_map_def by auto
interpret fg': equivalence_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg f g' φ ψ
using fg' by auto
obtain ψ' where ψ': "adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ'"
using assms equivalence_refines_to_adjoint_equivalence [of f g' φ]
fg'.antipar fg'.unit_in_hom fg'.unit_is_iso
by auto
interpret ψ': adjoint_equivalence_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg f g' φ ψ'
using ψ' by simp
have 1: "g ≅ g'"
using fg.adjunction_in_bicategory_axioms ψ'.adjunction_in_bicategory_axioms
left_adjoint_determines_right_up_to_iso adjoint_pair_def
by blast
obtain γ where γ: "«γ : g' ⇒ g» ∧ iso γ"
using 1 isomorphic_def isomorphic_symmetric by metis
have "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g ((γ ⋆ f) ⋅ φ) (ψ' ⋅ (f ⋆ inv γ))"
using γ equivalence_preserved_by_iso_right ψ'.equivalence_in_bicategory_axioms by simp
hence "quasi_inverses f g"
using quasi_inverses_def by blast
thus ?thesis
using equivalence_mapI quasi_inverses_symmetric by blast
qed
lemma left_adjoint_to_equivalence_is_equivalence:
assumes "equivalence_map f" and "adjoint_pair g f"
shows "equivalence_map g"
proof -
obtain η ε where gf: "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g f η ε"
using assms adjoint_pair_def by auto
interpret gf: adjunction_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg g f η ε
using gf by simp
obtain g' where 1: "quasi_inverses g' f"
using assms equivalence_mapE quasi_inverses_symmetric by blast
obtain φ ψ where g'f: "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ"
using assms 1 quasi_inverses_def by auto
interpret g'f: equivalence_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg g' f φ ψ
using g'f by auto
obtain ψ' where ψ': "adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ'"
using assms 1 equivalence_refines_to_adjoint_equivalence [of g' f φ]
g'f.antipar g'f.unit_in_hom g'f.unit_is_iso quasi_inverses_def
equivalence_map_def
by auto
interpret ψ': adjoint_equivalence_in_bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg g' f φ ψ'
using ψ' by simp
have 1: "g ≅ g'"
using gf.adjunction_in_bicategory_axioms ψ'.adjunction_in_bicategory_axioms
right_adjoint_determines_left_up_to_iso adjoint_pair_def
by blast
obtain γ where γ: "«γ : g' ⇒ g» ∧ iso γ"
using 1 isomorphic_def isomorphic_symmetric by metis
have "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g f ((f ⋆ γ) ⋅ φ) (ψ' ⋅ (inv γ ⋆ f))"
using γ equivalence_preserved_by_iso_left ψ'.equivalence_in_bicategory_axioms by simp
hence "quasi_inverses g f"
using quasi_inverses_def by auto
thus ?thesis
using quasi_inverses_symmetric quasi_inverses_def equivalence_map_def by blast
qed
lemma quasi_inverses_are_adjoint_pair:
assumes "quasi_inverses f g"
shows "adjoint_pair f g"
proof -
obtain η ε where ηε: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
using assms quasi_inverses_def by auto
interpret ηε: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
using ηε by auto
obtain ε' where ηε': "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'"
using ηε equivalence_map_def ηε.antipar ηε.unit_in_hom ηε.unit_is_iso
ηε.ide_right equivalence_refines_to_adjoint_equivalence [of f g η]
by force
interpret ηε': adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
using ηε' by auto
show ?thesis
using ηε' adjoint_pair_def ηε'.adjunction_in_bicategory_axioms by auto
qed
lemma quasi_inverses_isomorphic_right:
assumes "quasi_inverses f g"
shows "quasi_inverses f g' ⟷ g ≅ g'"
proof
show "g ≅ g' ⟹ quasi_inverses f g'"
using assms quasi_inverses_def isomorphic_def equivalence_preserved_by_iso_right
by metis
assume g': "quasi_inverses f g'"
show "g ≅ g'"
using assms g' quasi_inverses_are_adjoint_pair left_adjoint_determines_right_up_to_iso
by blast
qed
lemma quasi_inverses_isomorphic_left:
assumes "quasi_inverses f g"
shows "quasi_inverses f' g ⟷ f ≅ f'"
proof
show "f ≅ f' ⟹ quasi_inverses f' g"
using assms quasi_inverses_def isomorphic_def equivalence_preserved_by_iso_left
by metis
assume f': "quasi_inverses f' g"
show "f ≅ f'"
using assms f' quasi_inverses_are_adjoint_pair right_adjoint_determines_left_up_to_iso
by blast
qed
end
end