Theory EnrichedCategoryBasics.EnrichedCategory
text ‹
The notion of an enriched category \<^cite>‹"kelly-enriched-category"›
generalizes the concept of category by replacing the hom-sets of an ordinary category by
objects of an arbitrary monoidal category ‹M›.
The choice, for each object ‹a›, of a distinguished element ‹id a : a → a› as an identity,
is replaced by an arrow ‹Id a : ℐ → Hom a a› of ‹M›. The composition operation is similarly
replaced by a family of arrows ‹Comp a b c : Hom B C ⊗ Hom A B → Hom A C› of ‹M›.
The identity and composition are required to satisfy unit and associativity laws which are
expressed as commutative diagrams in ‹M›.
›
theory EnrichedCategory
imports ClosedMonoidalCategory
begin
context monoidal_category
begin
abbreviation ι' ("ι⇧-⇧1")
where "ι' ≡ inv ι"
end
context elementary_symmetric_monoidal_category
begin
lemma sym_unit:
shows "ι ⋅ 𝗌[ℐ, ℐ] = ι"
by (simp add: ι_def unitor_coherence unitor_coincidence(2))
lemma sym_inv_unit:
shows "𝗌[ℐ, ℐ] ⋅ inv ι = inv ι"
using sym_unit
by (metis MC.unit_is_iso arr_inv cod_inv comp_arr_dom comp_cod_arr
iso_cancel_left iso_is_arr)
end
section "Basic Definitions"
locale enriched_category =
monoidal_category +
fixes Obj :: "'o set"
and Hom :: "'o ⇒ 'o ⇒ 'a"
and Id :: "'o ⇒ 'a"
and Comp :: "'o ⇒ 'o ⇒ 'o ⇒ 'a"
assumes ide_Hom [intro, simp]: "⟦a ∈ Obj; b ∈ Obj⟧ ⟹ ide (Hom a b)"
and Id_in_hom [intro]: "a ∈ Obj ⟹ «Id a : ℐ → Hom a a»"
and Comp_in_hom [intro]: "⟦a ∈ Obj; b ∈ Obj; c ∈ Obj⟧ ⟹
«Comp a b c : Hom b c ⊗ Hom a b → Hom a c»"
and Comp_Hom_Id: "⟦a ∈ Obj; b ∈ Obj⟧ ⟹
Comp a a b ⋅ (Hom a b ⊗ Id a) = 𝗋[Hom a b]"
and Comp_Id_Hom: "⟦a ∈ Obj; b ∈ Obj⟧ ⟹
Comp a b b ⋅ (Id b ⊗ Hom a b) = 𝗅[Hom a b]"
and Comp_assoc: "⟦a ∈ Obj; b ∈ Obj; c ∈ Obj; d ∈ Obj⟧ ⟹
Comp a b d ⋅ (Comp b c d ⊗ Hom a b) =
Comp a c d ⋅ (Hom c d ⊗ Comp a b c) ⋅
𝖺[Hom c d, Hom b c, Hom a b]"
text‹
A functor from an enriched category ‹A› to an enriched category ‹B› consists of
an object map ‹F⇩o : Obj⇩A → Obj⇩B› and a map ‹F⇩a› that assigns to each pair of objects
‹a› ‹b› in ‹Obj⇩A› an arrow ‹F⇩a a b : Hom⇩A a b → Hom⇩B (F⇩o a) (F⇩o b)› of the underlying
monoidal category, subject to equations expressing that identities and composition
are preserved.
›
locale enriched_functor =
monoidal_category C T α ι +
A: enriched_category C T α ι Obj⇩A Hom⇩A Id⇩A Comp⇩A +
B: enriched_category C T α ι Obj⇩B Hom⇩B Id⇩B Comp⇩B
for C :: "'m ⇒ 'm ⇒ 'm" (infixr ‹⋅› 55)
and T :: "'m × 'm ⇒ 'm"
and α :: "'m × 'm × 'm ⇒ 'm"
and ι :: "'m"
and Obj⇩A :: "'a set"
and Hom⇩A :: "'a ⇒ 'a ⇒ 'm"
and Id⇩A :: "'a ⇒ 'm"
and Comp⇩A :: "'a ⇒ 'a ⇒ 'a ⇒ 'm"
and Obj⇩B :: "'b set"
and Hom⇩B :: "'b ⇒ 'b ⇒ 'm"
and Id⇩B :: "'b ⇒ 'm"
and Comp⇩B :: "'b ⇒ 'b ⇒ 'b ⇒ 'm"
and F⇩o :: "'a ⇒ 'b"
and F⇩a :: "'a ⇒ 'a ⇒ 'm" +
assumes extensionality: "a ∉ Obj⇩A ∨ b ∉ Obj⇩A ⟹ F⇩a a b = null"
assumes preserves_Obj [intro]: "a ∈ Obj⇩A ⟹ F⇩o a ∈ Obj⇩B"
and preserves_Hom: "⟦a ∈ Obj⇩A; b ∈ Obj⇩A⟧ ⟹
«F⇩a a b : Hom⇩A a b → Hom⇩B (F⇩o a) (F⇩o b)»"
and preserves_Id: "a ∈ Obj⇩A ⟹ F⇩a a a ⋅ Id⇩A a = Id⇩B (F⇩o a)"
and preserves_Comp: "⟦a ∈ Obj⇩A; b ∈ Obj⇩A; c ∈ Obj⇩A⟧ ⟹
Comp⇩B (F⇩o a) (F⇩o b) (F⇩o c) ⋅ T (F⇩a b c, F⇩a a b) =
F⇩a a c ⋅ Comp⇩A a b c"
locale fully_faithful_enriched_functor =
enriched_functor +
assumes locally_iso: "⟦a ∈ Obj⇩A; b ∈ Obj⇩A⟧ ⟹ iso (F⇩a a b)"
text‹
A natural transformation from an an enriched functor ‹F = (F⇩o, F⇩a)› to an
enriched functor ‹G = (G⇩o, G⇩a)› consists of a map ‹τ› that assigns to each
object ‹a ∈ Obj⇩A› a ``component at ‹a›'', which is an arrow ‹τ a : ℐ → Hom⇩B (F⇩o a) (G⇩o a)›,
subject to an equation that expresses the naturality condition.
›
locale enriched_natural_transformation =
monoidal_category C T α ι +
A: enriched_category C T α ι Obj⇩A Hom⇩A Id⇩A Comp⇩A +
B: enriched_category C T α ι Obj⇩B Hom⇩B Id⇩B Comp⇩B +
F: enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A Obj⇩B Hom⇩B Id⇩B Comp⇩B F⇩o F⇩a +
G: enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A Obj⇩B Hom⇩B Id⇩B Comp⇩B G⇩o G⇩a
for C :: "'m ⇒ 'm ⇒ 'm" (infixr ‹⋅› 55)
and T :: "'m × 'm ⇒ 'm"
and α :: "'m × 'm × 'm ⇒ 'm"
and ι :: "'m"
and Obj⇩A :: "'a set"
and Hom⇩A :: "'a ⇒ 'a ⇒ 'm"
and Id⇩A :: "'a ⇒ 'm"
and Comp⇩A :: "'a ⇒ 'a ⇒ 'a ⇒ 'm"
and Obj⇩B :: "'b set"
and Hom⇩B :: "'b ⇒ 'b ⇒ 'm"
and Id⇩B :: "'b ⇒ 'm"
and Comp⇩B :: "'b ⇒ 'b ⇒ 'b ⇒ 'm"
and F⇩o :: "'a ⇒ 'b"
and F⇩a :: "'a ⇒ 'a ⇒ 'm"
and G⇩o :: "'a ⇒ 'b"
and G⇩a :: "'a ⇒ 'a ⇒ 'm"
and τ :: "'a ⇒ 'm" +
assumes extensionality: "a ∉ Obj⇩A ⟹ τ a = null"
and component_in_hom [intro]: "a ∈ Obj⇩A ⟹ «τ a : ℐ → Hom⇩B (F⇩o a) (G⇩o a)»"
and naturality: "⟦a ∈ Obj⇩A; b ∈ Obj⇩A⟧ ⟹
Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅ (τ b ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b] =
Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ τ a) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]"
subsection "Self-Enrichment"
context elementary_closed_monoidal_category
begin
text ‹
Every closed monoidal category ‹M› admits a structure of enriched category,
where the exponentials in ‹M› itself serve as the ``hom-objects''
(\emph{cf.}~\<^cite>‹"kelly-enriched-category"› Section 1.6).
Essentially all the work in proving this theorem has already been done in
@{theory EnrichedCategoryBasics.ClosedMonoidalCategory}.
›
interpretation closed_monoidal_category
using is_closed_monoidal_category by blast
interpretation EC: enriched_category C T α ι ‹Collect ide› exp Id Comp
using Id_in_hom Comp_in_hom Comp_unit_right Comp_unit_left Comp_assoc⇩E⇩C⇩M⇩C(2)
by unfold_locales auto
theorem is_enriched_in_itself:
shows "enriched_category C T α ι (Collect ide) exp Id Comp"
..
text‹
The following mappings define a bijection between ‹hom a b› and ‹hom ℐ (exp a b)›.
These have functorial properties which are encountered repeatedly.
›
definition UP ("_⇧↑" [100] 100)
where "t⇧↑ ≡ if arr t then Curry[ℐ, dom t, cod t] (t ⋅ 𝗅[dom t]) else null"
definition DN
where "DN a b t ≡ if arr t then Uncurry[a, b] t ⋅ 𝗅⇧-⇧1[a] else null"
abbreviation DN' ("_⇧↓[_, _]" [100] 99)
where "t⇧↓[a, b] ≡ DN a b t"
lemma UP_DN:
shows [intro]: "arr t ⟹ «t⇧↑ : ℐ → exp (dom t) (cod t)»"
and [intro]: "⟦ide a; ide b; «t : ℐ → exp a b»⟧ ⟹ «t⇧↓[a, b]: a → b»"
and [simp]: "arr t ⟹ (t⇧↑)⇧↓[dom t, cod t] = t"
and [simp]: "⟦ide a; ide b; «t : ℐ → exp a b»⟧ ⟹ (t⇧↓[a, b])⇧↑ = t"
using UP_def DN_def Uncurry_Curry Curry_Uncurry [of ℐ a b t]
comp_assoc comp_arr_dom
by auto
lemma UP_simps [simp]:
assumes "arr t"
shows "arr (t⇧↑)" and "dom (t⇧↑) = ℐ" and "cod (t⇧↑) = exp (dom t) (cod t)"
using assms UP_DN by auto
lemma DN_simps [simp]:
assumes "ide a" and "ide b" and "arr t" and "dom t = ℐ" and "cod t = exp a b"
shows "arr (t⇧↓[a, b])" and "dom (t⇧↓[a, b]) = a" and "cod (t⇧↓[a, b]) = b"
using assms UP_DN DN_def by auto
lemma UP_ide:
assumes "ide a"
shows "a⇧↑ = Id a"
using assms Id_def comp_cod_arr UP_def by auto
lemma DN_Id:
assumes "ide a"
shows "(Id a)⇧↓[a, a] = a"
using assms Uncurry_Curry lunit_in_hom Id_def DN_def by auto
lemma UP_comp:
assumes "seq t u"
shows "(t ⋅ u)⇧↑ = Comp (dom u) (cod u) (cod t) ⋅ (t⇧↑ ⊗ u⇧↑) ⋅ ι⇧-⇧1"
proof -
have "Comp (dom u) (cod u) (cod t) ⋅ (t⇧↑ ⊗ u⇧↑) ⋅ ι⇧-⇧1 =
(Curry[exp (cod u) (cod t) ⊗ exp (dom u) (cod u), dom u, cod t]
(eval (cod u) (cod t) ⋅
(exp (cod u) (cod t) ⊗ eval (dom u) (cod u)) ⋅
𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]) ⋅
(t⇧↑ ⊗ u⇧↑)) ⋅ ι⇧-⇧1"
unfolding Comp_def
using assms comp_assoc by simp
also have "... =
(Curry[ℐ ⊗ ℐ, dom u, cod t]
((eval (cod u) (cod t) ⋅
(exp (cod u) (cod t) ⊗ eval (dom u) (cod u)) ⋅
𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]) ⋅
((t⇧↑ ⊗ u⇧↑) ⊗ dom u))) ⋅ ι⇧-⇧1"
using assms
comp_Curry_arr
[of "dom u" "t⇧↑ ⊗ u⇧↑"
"ℐ ⊗ ℐ" "exp (cod u) (cod t) ⊗ exp (dom u) (cod u)"
"eval (cod u) (cod t) ⋅
(exp (cod u) (cod t) ⊗ eval (dom u) (cod u)) ⋅
𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]"
"cod t"]
by fastforce
also have "... =
Curry[ℐ ⊗ ℐ, dom u, cod t]
(eval (cod u) (cod t) ⋅
((exp (cod u) (cod t) ⊗ eval (dom u) (cod u)) ⋅
(t⇧↑ ⊗ u⇧↑ ⊗ dom u)) ⋅ 𝖺[ℐ, ℐ, dom u]) ⋅ ι⇧-⇧1"
using assms assoc_naturality [of "t⇧↑" "u⇧↑" "dom u"] comp_assoc by auto
also have "... =
Curry[ℐ ⊗ ℐ, dom u, cod t]
(eval (cod u) (cod t) ⋅
(exp (cod u) (cod t) ⋅ t⇧↑ ⊗ Uncurry[dom u, cod u] (u⇧↑)) ⋅
𝖺[ℐ, ℐ, dom u]) ⋅ ι⇧-⇧1"
using assms comp_cod_arr UP_DN interchange by auto
also have "... =
Curry[ℐ ⊗ ℐ, dom u, cod t]
(eval (cod u) (cod t) ⋅
(exp (cod u) (cod t) ⋅ t⇧↑ ⊗ u ⋅ 𝗅[dom u]) ⋅
𝖺[ℐ, ℐ, dom u]) ⋅ ι⇧-⇧1"
using assms Uncurry_Curry UP_def by auto
also have "... =
Curry[ℐ ⊗ ℐ, dom u, cod t]
(eval (cod u) (cod t) ⋅
(t⇧↑ ⊗ u ⋅ 𝗅[dom u]) ⋅ 𝖺[ℐ, ℐ, dom u]) ⋅ ι⇧-⇧1"
using assms comp_cod_arr by auto
also have "... =
Curry[ℐ ⊗ ℐ, dom u, cod t]
(eval (cod u) (cod t) ⋅
((t⇧↑ ⊗ cod u) ⋅ (ℐ ⊗ u ⋅ 𝗅[dom u])) ⋅
𝖺[ℐ, ℐ, dom u]) ⋅ ι⇧-⇧1"
using assms comp_arr_dom [of "t⇧↑" ℐ] comp_cod_arr [of "u ⋅ 𝗅[dom u]" "cod u"]
interchange [of "t⇧↑" ℐ "cod u" "u ⋅ 𝗅[dom u]"]
by auto
also have "... =
Curry[ℐ, dom u, cod t]
((eval (cod u) (cod t) ⋅
((t⇧↑ ⊗ cod u) ⋅ (ℐ ⊗ u ⋅ 𝗅[dom u])) ⋅
𝖺[ℐ, ℐ, dom u]) ⋅ (ι⇧-⇧1 ⊗ dom u))"
proof -
have "«ι⇧-⇧1 : ℐ → ℐ ⊗ ℐ»"
using inv_in_hom unit_is_iso by blast
thus ?thesis
using assms comp_Curry_arr by fastforce
qed
also have "... =
Curry[ℐ, dom u, cod t]
((Uncurry[cod u, cod t] (t⇧↑)) ⋅ (ℐ ⊗ u ⋅ 𝗅[dom u]) ⋅
𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u))"
using comp_assoc by simp
also have "... = Curry[ℐ, dom u, cod t] (Uncurry[cod u, cod t] (t⇧↑) ⋅ (ℐ ⊗ u))"
proof -
have "(ℐ ⊗ u ⋅ 𝗅[dom u]) ⋅ 𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u) =
((ℐ ⊗ u) ⋅ (ℐ ⊗ 𝗅[dom u])) ⋅ 𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u)"
using assms by auto
also have "... = (ℐ ⊗ u) ⋅ (ℐ ⊗ 𝗅[dom u]) ⋅ 𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u)"
using comp_assoc by simp
also have "... = (ℐ ⊗ u) ⋅ (ℐ ⊗ 𝗅[dom u]) ⋅ (ℐ ⊗ 𝗅⇧-⇧1[dom u])"
proof -
have "𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u) = ℐ ⊗ 𝗅⇧-⇧1[dom u]"
proof -
have "𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u) =
inv ((ι ⊗ dom u) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, dom u])"
using assms inv_inv inv_comp [of "𝖺⇧-⇧1[ℐ, ℐ, dom u]" "ι ⊗ dom u"]
inv_tensor [of ι "dom u"]
by (metis ide_dom ide_is_iso ide_unity inv_ide iso_assoc iso_inv_iso
iso_is_arr lunit_char(2) seqE tensor_preserves_iso triangle
unit_is_iso unitor_coincidence(2))
also have "... = inv (ℐ ⊗ 𝗅[dom u])"
using assms lunit_char [of "dom u"] by auto
also have "... = ℐ ⊗ 𝗅⇧-⇧1[dom u]"
using assms inv_tensor by auto
finally show ?thesis by blast
qed
thus ?thesis by simp
qed
also have "... = (ℐ ⊗ u) ⋅ (ℐ ⊗ dom u)"
using assms
by (metis comp_ide_self comp_lunit_lunit'(1) dom_comp ideD(1)
ide_dom ide_unity interchange)
also have "... = ℐ ⊗ u"
using assms by blast
finally have "(ℐ ⊗ u ⋅ 𝗅[dom u]) ⋅ 𝖺[ℐ, ℐ, dom u] ⋅ (ι⇧-⇧1 ⊗ dom u) = ℐ ⊗ u"
by blast
thus ?thesis by argo
qed
also have "... = Curry[ℐ, dom u, cod t] ((t ⋅ 𝗅[cod u]) ⋅ (ℐ ⊗ u))"
using assms Uncurry_Curry UP_def by auto
also have "... = Curry[ℐ, dom u, cod t] (t ⋅ u ⋅ 𝗅[dom u])"
using assms comp_assoc lunit_naturality by auto
also have "... = (t ⋅ u)⇧↑"
using assms comp_assoc UP_def by simp
finally show ?thesis by simp
qed
end
section "Underlying Category, Functor, and Natural Transformation"
subsection "Underlying Category"
text‹
The underlying category (\emph{cf.}~\<^cite>‹"kelly-enriched-category"› Section 1.3)
of an enriched category has as its arrows from ‹a› to ‹b› the arrows ‹ℐ → Hom a b› of ‹M›
(\emph{i.e.}~the points of ‹Hom a b›). The identity at ‹a› is ‹Id a›. The composition of
arrows ‹f› and ‹g› is given by the formula: ‹Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1›.
›
locale underlying_category =
M: monoidal_category +
A: enriched_category
begin
sublocale concrete_category Obj ‹λa b. M.hom ℐ (Hom a b)› ‹Id›
‹λc b a g f. Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1›
proof
show "⋀a. a ∈ Obj ⟹ Id a ∈ M.hom ℐ (Hom a a)"
using A.Id_in_hom by blast
show 1: "⋀a b c f g.
⟦a ∈ Obj; b ∈ Obj; c ∈ Obj;
f ∈ M.hom ℐ (Hom a b); g ∈ M.hom ℐ (Hom b c)⟧
⟹ Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1 ∈ M.hom ℐ (Hom a c)"
using A.Comp_in_hom M.inv_in_hom M.unit_is_iso M.comp_in_homI
M.unit_in_hom
apply auto[1]
apply (intro M.comp_in_homI)
by auto
show "⋀a b f. ⟦a ∈ Obj; b ∈ Obj; f ∈ M.hom ℐ (Hom a b)⟧
⟹ Comp a a b ⋅ (f ⊗ Id a) ⋅ ι⇧-⇧1 = f"
proof -
fix a b f
assume a: "a ∈ Obj" and b: "b ∈ Obj" and f: "f ∈ M.hom ℐ (Hom a b)"
show "Comp a a b ⋅ (f ⊗ Id a) ⋅ ι⇧-⇧1 = f"
proof -
have "Comp a a b ⋅ (f ⊗ Id a) ⋅ ι⇧-⇧1 = (Comp a a b ⋅ (f ⊗ Id a)) ⋅ ι⇧-⇧1"
using M.comp_assoc by simp
also have "... = (Comp a a b ⋅ (Hom a b ⊗ Id a) ⋅ (f ⊗ ℐ)) ⋅ ι⇧-⇧1"
using a f M.comp_arr_dom M.comp_cod_arr A.Id_in_hom
M.in_homE M.interchange mem_Collect_eq
by metis
also have "... = (𝗋[Hom a b] ⋅ (f ⊗ ℐ)) ⋅ ι⇧-⇧1"
using a b f A.Comp_Hom_Id M.comp_assoc by metis
also have "... = (f ⋅ 𝗋[ℐ]) ⋅ ι⇧-⇧1"
using f M.runit_naturality by fastforce
also have "... = f ⋅ ι ⋅ ι⇧-⇧1"
by (simp add: M.unitor_coincidence(2) M.comp_assoc)
also have "... = f"
using f M.comp_arr_dom M.comp_arr_inv' M.unit_is_iso by auto
finally show "Comp a a b ⋅ (f ⊗ Id a) ⋅ ι⇧-⇧1 = f" by blast
qed
qed
show "⋀a b f. ⟦a ∈ Obj; b ∈ Obj; f ∈ M.hom ℐ (Hom a b)⟧
⟹ Comp a b b ⋅ (Id b ⊗ f) ⋅ ι⇧-⇧1 = f"
proof -
fix a b f
assume a: "a ∈ Obj" and b: "b ∈ Obj" and f: "f ∈ M.hom ℐ (Hom a b)"
show "Comp a b b ⋅ (Id b ⊗ f) ⋅ ι⇧-⇧1 = f"
proof -
have "Comp a b b ⋅ (Id b ⊗ f) ⋅ ι⇧-⇧1 = (Comp a b b ⋅ (Id b ⊗ f)) ⋅ ι⇧-⇧1"
using M.comp_assoc by simp
also have "... = (Comp a b b ⋅ (Id b ⊗ Hom a b) ⋅ (ℐ ⊗ f)) ⋅ ι⇧-⇧1"
using a b f M.comp_arr_dom M.comp_cod_arr A.Id_in_hom
M.in_homE M.interchange mem_Collect_eq
by metis
also have "... = (𝗅[Hom a b] ⋅ (ℐ ⊗ f)) ⋅ ι⇧-⇧1"
using a b A.Comp_Id_Hom M.comp_assoc by metis
also have "... = (f ⋅ 𝗅[ℐ]) ⋅ ι⇧-⇧1"
using a b f M.lunit_naturality [of f] by auto
also have "... = f ⋅ ι ⋅ ι⇧-⇧1"
by (simp add: M.unitor_coincidence(1) M.comp_assoc)
also have "... = f"
using M.comp_arr_dom M.comp_arr_inv' M.unit_is_iso f by auto
finally show "Comp a b b ⋅ (Id b ⊗ f) ⋅ ι⇧-⇧1 = f" by blast
qed
qed
show "⋀a b c d f g h.
⟦a ∈ Obj; b ∈ Obj; c ∈ Obj; d ∈ Obj;
f ∈ M.hom ℐ (Hom a b); g ∈ M.hom ℐ (Hom b c);
h ∈ M.hom ℐ (Hom c d)⟧
⟹ Comp a c d ⋅ (h ⊗ Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1) ⋅ ι⇧-⇧1 =
Comp a b d ⋅ (Comp b c d ⋅ (h ⊗ g) ⋅ ι⇧-⇧1 ⊗ f) ⋅ ι⇧-⇧1"
proof -
fix a b c d f g h
assume a: "a ∈ Obj" and b: "b ∈ Obj" and c: "c ∈ Obj" and d: "d ∈ Obj"
assume f: "f ∈ M.hom ℐ (Hom a b)" and g: "g ∈ M.hom ℐ (Hom b c)"
and h: "h ∈ M.hom ℐ (Hom c d)"
have "Comp a c d ⋅ (h ⊗ Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1) ⋅ ι⇧-⇧1 =
Comp a c d ⋅
((Hom c d ⊗ Comp a b c) ⋅ (h ⊗ (g ⊗ f) ⋅ ι⇧-⇧1)) ⋅ ι⇧-⇧1"
using a b c d f g h 1 M.interchange A.ide_Hom M.comp_ide_arr M.comp_cod_arr
M.in_homE mem_Collect_eq
by metis
also have "... = Comp a c d ⋅
((Hom c d ⊗ Comp a b c) ⋅
(𝖺[Hom c d, Hom b c, Hom a b] ⋅
𝖺⇧-⇧1[Hom c d, Hom b c, Hom a b])) ⋅
(h ⊗ (g ⊗ f) ⋅ ι⇧-⇧1) ⋅ ι⇧-⇧1"
proof -
have "(Hom c d ⊗ Comp a b c) ⋅
(𝖺[Hom c d, Hom b c, Hom a b] ⋅
𝖺⇧-⇧1[Hom c d, Hom b c, Hom a b]) =
Hom c d ⊗ Comp a b c"
using a b c d
by (metis A.Comp_in_hom A.ide_Hom M.comp_arr_ide
M.comp_assoc_assoc'(1) M.ide_in_hom M.interchange M.seqI'
M.tensor_preserves_ide)
thus ?thesis
using M.comp_assoc by force
qed
also have "... = (Comp a c d ⋅ (Hom c d ⊗ Comp a b c) ⋅
𝖺[Hom c d, Hom b c, Hom a b]) ⋅
(𝖺⇧-⇧1[Hom c d, Hom b c, Hom a b] ⋅
(h ⊗ (g ⊗ f) ⋅ ι⇧-⇧1)) ⋅
ι⇧-⇧1"
using M.comp_assoc by auto
also have "... = (Comp a b d ⋅ (Comp b c d ⊗ Hom a b)) ⋅
(𝖺⇧-⇧1[Hom c d, Hom b c, Hom a b] ⋅ (h ⊗ (g ⊗ f) ⋅ ι⇧-⇧1)) ⋅ ι⇧-⇧1"
using a b c d A.Comp_assoc by auto
also have "... = (Comp a b d ⋅ (Comp b c d ⊗ Hom a b)) ⋅
(𝖺⇧-⇧1[Hom c d, Hom b c, Hom a b] ⋅ (h ⊗ (g ⊗ f))) ⋅
(ℐ ⊗ ι⇧-⇧1) ⋅ ι⇧-⇧1"
proof -
have "h ⊗ (g ⊗ f) ⋅ ι⇧-⇧1 = (h ⊗ (g ⊗ f)) ⋅ (ℐ ⊗ ι⇧-⇧1)"
proof -
have "M.seq h ℐ"
using h by auto
moreover have "M.seq (g ⊗ f) ι⇧-⇧1"
using f g M.inv_in_hom M.unit_is_iso by blast
ultimately show ?thesis
using a b c d f g h M.interchange M.comp_arr_ide M.ide_unity by metis
qed
thus ?thesis
using M.comp_assoc by simp
qed
also have "... = (Comp a b d ⋅ (Comp b c d ⊗ Hom a b)) ⋅
((h ⊗ g) ⊗ f) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ] ⋅ (ℐ ⊗ ι⇧-⇧1) ⋅ ι⇧-⇧1"
using f g h M.assoc'_naturality
by (metis M.comp_assoc M.in_homE mem_Collect_eq)
also have "... = (Comp a b d ⋅ (Comp b c d ⊗ Hom a b)) ⋅
(((h ⊗ g) ⊗ f) ⋅ (ι⇧-⇧1 ⊗ ℐ)) ⋅ ι⇧-⇧1"
proof -
have "𝖺⇧-⇧1[ℐ, ℐ, ℐ] ⋅ (ℐ ⊗ ι⇧-⇧1) ⋅ ι⇧-⇧1 = (ι⇧-⇧1 ⊗ ℐ) ⋅ ι⇧-⇧1"
using M.unitor_coincidence
by (metis (full_types) M.L.preserves_inv M.L.preserves_iso
M.R.preserves_inv M.arrI M.arr_tensor M.comp_assoc M.ideD(1)
M.ide_unity M.inv_comp M.iso_assoc M.unit_in_hom_ax
M.unit_is_iso M.unit_triangle(1))
thus ?thesis
using M.comp_assoc by simp
qed
also have "... = Comp a b d ⋅
((Comp b c d ⊗ Hom a b) ⋅ ((h ⊗ g) ⋅ ι⇧-⇧1 ⊗ f)) ⋅ ι⇧-⇧1"
proof -
have "((h ⊗ g) ⊗ f) ⋅ (ι⇧-⇧1 ⊗ ℐ) = (h ⊗ g) ⋅ ι⇧-⇧1 ⊗ f"
proof -
have "M.seq (h ⊗ g) ι⇧-⇧1"
using g h M.inv_in_hom M.unit_is_iso by blast
moreover have "M.seq f ℐ"
using M.ide_in_hom M.ide_unity f by blast
ultimately show ?thesis
using f g h M.interchange M.comp_arr_ide M.ide_unity by metis
qed
thus ?thesis
using M.comp_assoc by auto
qed
also have "... = Comp a b d ⋅ (Comp b c d ⋅ (h ⊗ g) ⋅ ι⇧-⇧1 ⊗ f) ⋅ ι⇧-⇧1"
using b c d f g h 1 M.in_homE mem_Collect_eq M.comp_cod_arr
M.interchange A.ide_Hom M.comp_ide_arr
by metis
finally show "Comp a c d ⋅ (h ⊗ Comp a b c ⋅ (g ⊗ f) ⋅ ι⇧-⇧1) ⋅ ι⇧-⇧1 =
Comp a b d ⋅ (Comp b c d ⋅ (h ⊗ g) ⋅ ι⇧-⇧1 ⊗ f) ⋅ ι⇧-⇧1"
by blast
qed
qed
abbreviation comp (infixr "⋅⇩0" 55)
where "comp ≡ COMP"
lemma hom_char:
assumes "a ∈ Obj" and "b ∈ Obj"
shows "hom (MkIde a) (MkIde b) = MkArr a b ` M.hom ℐ (Hom a b)"
proof
show "hom (MkIde a) (MkIde b) ⊆ MkArr a b ` M.hom ℐ (Hom a b)"
proof
fix t
assume t: "t ∈ hom (MkIde a) (MkIde b)"
have "t = MkArr a b (Map t)"
using t MkArr_Map dom_char cod_char by fastforce
moreover have "Map t ∈ M.hom ℐ (Hom a b)"
using t arr_char dom_char cod_char by fastforce
ultimately show "t ∈ MkArr a b ` M.hom ℐ (Hom a b)" by simp
qed
show "MkArr a b ` M.hom ℐ (Hom a b) ⊆ hom (MkIde a) (MkIde b)"
using assms MkArr_in_hom by blast
qed
end
subsection "Underlying Functor"
text‹
The underlying functor of an enriched functor ‹F : A ⟶ B›
takes an arrow ‹«f : a → a'»› of the underlying category ‹A⇩0›
(\emph{i.e.}~an arrow ‹«ℐ → Hom a a'»› of ‹M›)
to the arrow ‹«F⇩a a a' ⋅ f : F⇩o a → F⇩o a'»› of ‹B⇩0›
(\emph{i.e.} the arrow ‹«F⇩a a a' ⋅ f : ℐ → Hom (F⇩o a) (F⇩o a')»› of ‹M›).
›
locale underlying_functor =
enriched_functor
begin
sublocale A⇩0: underlying_category C T α ι Obj⇩A Hom⇩A Id⇩A Comp⇩A ..
sublocale B⇩0: underlying_category C T α ι Obj⇩B Hom⇩B Id⇩B Comp⇩B ..
notation A⇩0.comp (infixr "⋅⇩A⇩0" 55)
notation B⇩0.comp (infixr "⋅⇩B⇩0" 55)
definition map⇩0
where "map⇩0 f = (if A⇩0.arr f
then B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f))
(F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f)
else B⇩0.null)"
sublocale "functor" A⇩0.comp B⇩0.comp map⇩0
proof
fix f
show "¬ A⇩0.arr f ⟹ map⇩0 f = B⇩0.null"
using map⇩0_def by simp
show 1: "⋀f. A⇩0.arr f ⟹ B⇩0.arr (map⇩0 f)"
proof -
fix f
assume f: "A⇩0.arr f"
have "B⇩0.arr (B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f))
(F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f))"
using f preserves_Hom A⇩0.Dom_in_Obj A⇩0.Cod_in_Obj A⇩0.arrE
by (metis (mono_tags, lifting) B⇩0.arr_MkArr comp_in_homI
mem_Collect_eq preserves_Obj)
thus "B⇩0.arr (map⇩0 f)"
using f map⇩0_def by simp
qed
show "A⇩0.arr f ⟹ B⇩0.dom (map⇩0 f) = map⇩0 (A⇩0.dom f)"
using 1 A⇩0.dom_char B⇩0.dom_char preserves_Id A⇩0.arr_dom_iff_arr
map⇩0_def A⇩0.Dom_in_Obj
by auto
show "A⇩0.arr f ⟹ B⇩0.cod (map⇩0 f) = map⇩0 (A⇩0.cod f)"
using 1 A⇩0.cod_char B⇩0.cod_char preserves_Id A⇩0.arr_cod_iff_arr
map⇩0_def A⇩0.Cod_in_Obj
by auto
fix g
assume fg: "A⇩0.seq g f"
show "map⇩0 (g ⋅⇩A⇩0 f) = map⇩0 g ⋅⇩B⇩0 map⇩0 f"
proof -
have "B⇩0.MkArr (F⇩o (A⇩0.Dom (g ⋅⇩A⇩0 f))) (F⇩o (B⇩0.Cod (g ⋅⇩A⇩0 f)))
(F⇩a (A⇩0.Dom (g ⋅⇩A⇩0 f))
(B⇩0.Cod (g ⋅⇩A⇩0 f)) ⋅ B⇩0.Map (g ⋅⇩A⇩0 f)) =
B⇩0.MkArr (F⇩o (A⇩0.Dom g)) (F⇩o (B⇩0.Cod g))
(F⇩a (A⇩0.Dom g) (B⇩0.Cod g) ⋅ B⇩0.Map g) ⋅⇩B⇩0
B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (B⇩0.Cod f))
(F⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⋅ B⇩0.Map f)"
proof -
have 2: "B⇩0.arr (B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g))
(F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f))"
using fg 1 A⇩0.seq_char map⇩0_def by auto
have 3: "B⇩0.arr (B⇩0.MkArr (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g))
(F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⋅ A⇩0.Map g))"
using fg 1 A⇩0.seq_char map⇩0_def by metis
have "B⇩0.MkArr (F⇩o (A⇩0.Dom g)) (F⇩o (B⇩0.Cod g))
(F⇩a (A⇩0.Dom g) (B⇩0.Cod g) ⋅ B⇩0.Map g) ⋅⇩B⇩0
B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (B⇩0.Cod f))
(F⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⋅ B⇩0.Map f) =
B⇩0.MkArr (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod g))
(Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g)) ⋅
(F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⋅ A⇩0.Map g ⊗
F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f) ⋅
ι⇧-⇧1)"
using fg 2 3 A⇩0.seq_char B⇩0.comp_MkArr by simp
moreover
have "Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g)) ⋅
(F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⋅ A⇩0.Map g ⊗
F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f) ⋅ ι⇧-⇧1 =
F⇩a (A⇩0.Dom (g ⋅⇩A⇩0 f)) (B⇩0.Cod (g ⋅⇩A⇩0 f)) ⋅ B⇩0.Map (g ⋅⇩A⇩0 f)"
proof -
have "Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g)) ⋅
(F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⋅ A⇩0.Map g ⊗
F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f) ⋅ ι⇧-⇧1 =
Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g)) ⋅
((F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f)) ⋅
(A⇩0.Map g ⊗ A⇩0.Map f)) ⋅ ι⇧-⇧1"
using fg preserves_Hom
interchange [of "F⇩a (A⇩0.Dom g) (A⇩0.Cod g)" "A⇩0.Map g"
"F⇩a (A⇩0.Dom f) (A⇩0.Cod f)" "A⇩0.Map f"]
by (metis A⇩0.arrE A⇩0.seqE seqI' mem_Collect_eq)
also have "... =
(Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Dom g)) (F⇩o (A⇩0.Cod g)) ⋅
(F⇩a (A⇩0.Dom g) (A⇩0.Cod g) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f))) ⋅
(A⇩0.Map g ⊗ A⇩0.Map f) ⋅ ι⇧-⇧1"
using comp_assoc by auto
also have "... = (F⇩a (A⇩0.Dom f) (B⇩0.Cod g) ⋅
Comp⇩A (A⇩0.Dom f) (A⇩0.Dom g) (B⇩0.Cod g)) ⋅
(A⇩0.Map g ⊗ A⇩0.Map f) ⋅ ι⇧-⇧1"
using fg A⇩0.seq_char preserves_Comp A⇩0.Dom_in_Obj A⇩0.Cod_in_Obj
by auto
also have "... = F⇩a (A⇩0.Dom (g ⋅⇩A⇩0 f)) (B⇩0.Cod (g ⋅⇩A⇩0 f)) ⋅
Comp⇩A (A⇩0.Dom f) (A⇩0.Dom g) (B⇩0.Cod g) ⋅
(A⇩0.Map g ⊗ A⇩0.Map f) ⋅ ι⇧-⇧1"
using fg comp_assoc A⇩0.seq_char by simp
also have "... = F⇩a (A⇩0.Dom (g ⋅⇩A⇩0 f)) (B⇩0.Cod (g ⋅⇩A⇩0 f)) ⋅
B⇩0.Map (g ⋅⇩A⇩0 f)"
using A⇩0.Map_comp A⇩0.seq_char fg by presburger
finally show ?thesis by blast
qed
ultimately show ?thesis
using A⇩0.seq_char fg by auto
qed
thus ?thesis
using fg map⇩0_def B⇩0.comp_MkArr by auto
qed
qed
proposition is_functor:
shows "functor A⇩0.comp B⇩0.comp map⇩0"
..
end
subsection "Underlying Natural Transformation"
text‹
The natural transformation underlying an enriched natural transformation ‹τ›
has components that are essentially those of ‹τ›, except that we have to bother
ourselves about coercions between types.
›
locale underlying_natural_transformation =
enriched_natural_transformation
begin
sublocale A⇩0: underlying_category C T α ι Obj⇩A Hom⇩A Id⇩A Comp⇩A ..
sublocale B⇩0: underlying_category C T α ι Obj⇩B Hom⇩B Id⇩B Comp⇩B ..
sublocale F⇩0: underlying_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A Obj⇩B Hom⇩B Id⇩B Comp⇩B F⇩o F⇩a ..
sublocale G⇩0: underlying_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A Obj⇩B Hom⇩B Id⇩B Comp⇩B G⇩o G⇩a ..
definition map⇩o⇩b⇩j
where "map⇩o⇩b⇩j a ≡
B⇩0.MkArr (B⇩0.Dom (F⇩0.map⇩0 a)) (B⇩0.Dom (G⇩0.map⇩0 a))
(τ (A⇩0.Dom a))"
sublocale τ: NaturalTransformation.transformation_by_components
A⇩0.comp B⇩0.comp F⇩0.map⇩0 G⇩0.map⇩0 map⇩o⇩b⇩j
proof
show "⋀a. A⇩0.ide a ⟹ B⇩0.in_hom (map⇩o⇩b⇩j a) (F⇩0.map⇩0 a) (G⇩0.map⇩0 a)"
unfolding map⇩o⇩b⇩j_def
using A⇩0.Dom_in_Obj B⇩0.ide_char⇩C⇩C F⇩0.map⇩0_def G⇩0.map⇩0_def
F⇩0.preserves_ide G⇩0.preserves_ide component_in_hom
by auto
show "⋀f. A⇩0.arr f ⟹
map⇩o⇩b⇩j (A⇩0.cod f) ⋅⇩B⇩0 F⇩0.map⇩0 f =
G⇩0.map⇩0 f ⋅⇩B⇩0 map⇩o⇩b⇩j (A⇩0.dom f)"
proof -
fix f
assume f: "A⇩0.arr f"
show "map⇩o⇩b⇩j (A⇩0.cod f) ⋅⇩B⇩0 F⇩0.map⇩0 f =
G⇩0.map⇩0 f ⋅⇩B⇩0 map⇩o⇩b⇩j (A⇩0.dom f)"
proof (intro B⇩0.arr_eqI)
show 1: "B⇩0.seq (map⇩o⇩b⇩j (A⇩0.cod f)) (F⇩0.map⇩0 f)"
using A⇩0.ide_cod
‹⋀a. A⇩0.ide a ⟹
B⇩0.in_hom (map⇩o⇩b⇩j a) (F⇩0.map⇩0 a) (G⇩0.map⇩0 a)› f
by blast
show 2: "B⇩0.seq (G⇩0.map⇩0 f) (map⇩o⇩b⇩j (A⇩0.dom f))"
using A⇩0.ide_dom
‹⋀a. A⇩0.ide a ⟹
B⇩0.in_hom (map⇩o⇩b⇩j a) (F⇩0.map⇩0 a) (G⇩0.map⇩0 a)› f
by blast
show "B⇩0.Dom (map⇩o⇩b⇩j (A⇩0.cod f) ⋅⇩B⇩0 F⇩0.map⇩0 f) =
B⇩0.Dom (G⇩0.map⇩0 f ⋅⇩B⇩0 map⇩o⇩b⇩j (A⇩0.dom f))"
using f 1 2 B⇩0.comp_char [of "map⇩o⇩b⇩j (A⇩0.cod f)" "F⇩0.map⇩0 f"]
B⇩0.comp_char [of "G⇩0.map⇩0 f" "map⇩o⇩b⇩j (A⇩0.dom f)"]
F⇩0.map⇩0_def G⇩0.map⇩0_def map⇩o⇩b⇩j_def
by simp
show "B⇩0.Cod (map⇩o⇩b⇩j (A⇩0.cod f) ⋅⇩B⇩0 F⇩0.map⇩0 f) =
B⇩0.Cod (G⇩0.map⇩0 f ⋅⇩B⇩0 map⇩o⇩b⇩j (A⇩0.dom f))"
using f 1 2 B⇩0.comp_char [of "map⇩o⇩b⇩j (A⇩0.cod f)" "F⇩0.map⇩0 f"]
B⇩0.comp_char [of "G⇩0.map⇩0 f" "map⇩o⇩b⇩j (A⇩0.dom f)"]
F⇩0.map⇩0_def G⇩0.map⇩0_def map⇩o⇩b⇩j_def
by simp
show "B⇩0.Map (map⇩o⇩b⇩j (A⇩0.cod f) ⋅⇩B⇩0 F⇩0.map⇩0 f) =
B⇩0.Map (G⇩0.map⇩0 f ⋅⇩B⇩0 map⇩o⇩b⇩j (A⇩0.dom f))"
proof -
have "Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f)) (G⇩o (A⇩0.Cod f)) ⋅
(τ (A⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f) ⋅ ι⇧-⇧1 =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f ⊗ τ (A⇩0.Dom f)) ⋅ ι⇧-⇧1"
proof -
have "Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f)) (G⇩o (A⇩0.Cod f)) ⋅
(τ (A⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f) ⋅ ι⇧-⇧1 =
Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f)) (G⇩o (A⇩0.Cod f)) ⋅
((τ (A⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f)) ⋅ (ℐ ⊗ A⇩0.Map f)) ⋅
ι⇧-⇧1"
proof -
have "τ (A⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f) ⋅ A⇩0.Map f =
(τ (A⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (A⇩0.Cod f)) ⋅ (ℐ ⊗ A⇩0.Map f)"
proof -
have "seq (τ (A⇩0.Cod f)) ℐ"
using f seqI component_in_hom
by (metis (no_types, lifting) A⇩0.Cod_in_Obj ide_char
ide_unity in_homE)
moreover have "seq (F⇩a (A⇩0.Dom f) (B⇩0.Cod f)) (B⇩0.Map f)"
using f A⇩0.Map_in_Hom A⇩0.Cod_in_Obj A⇩0.Dom_in_Obj
F.preserves_Hom in_homE
by blast
ultimately show ?thesis
using f component_in_hom interchange comp_arr_dom by auto
qed
thus ?thesis by simp
qed
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (A⇩0.Cod f)) (G⇩o (A⇩0.Cod f)) ⋅
((τ (B⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (B⇩0.Cod f)) ⋅
(𝗅⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅
𝗅[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)]) ⋅
(ℐ ⊗ B⇩0.Map f)) ⋅ ι⇧-⇧1"
proof -
have "(𝗅⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅
𝗅[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)]) ⋅
(ℐ ⊗ B⇩0.Map f) =
ℐ ⊗ B⇩0.Map f"
using f comp_lunit_lunit'(2)
by (metis (no_types, lifting) A.ide_Hom A⇩0.arrE comp_cod_arr
comp_ide_self ideD(1) ide_unity interchange in_homE
mem_Collect_eq)
thus ?thesis by simp
qed
also have "... =
(Comp⇩B (F⇩o (A⇩0.Dom f)) (F⇩o (B⇩0.Cod f)) (G⇩o (B⇩0.Cod f)) ⋅
(τ (B⇩0.Cod f) ⊗ F⇩a (A⇩0.Dom f) (B⇩0.Cod f)) ⋅
𝗅⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)]) ⋅
𝗅[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅ (ℐ ⊗ B⇩0.Map f) ⋅ ι⇧-⇧1"
using comp_assoc by simp
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⊗ τ (A⇩0.Dom f)) ⋅
𝗋⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅
(𝗅[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅ (ℐ ⊗ B⇩0.Map f)) ⋅ ι⇧-⇧1"
using f A⇩0.Cod_in_Obj A⇩0.Dom_in_Obj naturality comp_assoc by simp
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⊗ τ (A⇩0.Dom f)) ⋅
𝗋⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅ (B⇩0.Map f ⋅ 𝗅[ℐ]) ⋅ ι⇧-⇧1"
using f lunit_naturality A⇩0.Map_in_Hom by force
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⊗ τ (A⇩0.Dom f)) ⋅
𝗋⇧-⇧1[Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)] ⋅ B⇩0.Map f"
proof -
have "ι ⋅ ι⇧-⇧1 = ℐ"
using comp_arr_inv' unit_is_iso by blast
moreover have "«B⇩0.Map f : ℐ → Hom⇩A (A⇩0.Dom f) (B⇩0.Cod f)»"
using f A⇩0.Map_in_Hom by blast
ultimately show ?thesis
using f comp_arr_dom unitor_coincidence(1) comp_assoc by auto
qed
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⊗ τ (A⇩0.Dom f)) ⋅
(B⇩0.Map f ⊗ ℐ) ⋅ 𝗋⇧-⇧1[ℐ]"
using f runit'_naturality A⇩0.Map_in_Hom by force
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
((G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⊗ τ (A⇩0.Dom f)) ⋅
(B⇩0.Map f ⊗ ℐ)) ⋅ ι⇧-⇧1"
using unitor_coincidence comp_assoc by simp
also have "... =
Comp⇩B (F⇩o (A⇩0.Dom f)) (G⇩o (A⇩0.Dom f)) (G⇩o (B⇩0.Cod f)) ⋅
(G⇩a (A⇩0.Dom f) (B⇩0.Cod f) ⋅ A⇩0.Map f ⊗ τ (A⇩0.Dom f)) ⋅ ι⇧-⇧1"
proof -
have "seq (G⇩a (A⇩0.Dom f) (B⇩0.Cod f)) (B⇩0.Map f)"
using f A⇩0.Map_in_Hom A⇩0.Cod_in_Obj A⇩0.Dom_in_Obj G.preserves_Hom
by fast
moreover have "seq (τ (A⇩0.Dom f)) ℐ"
using f seqI component_in_hom
by (metis (no_types, lifting) A⇩0.Dom_in_Obj ide_char
ide_unity in_homE)
ultimately show ?thesis
using f comp_arr_dom interchange by auto
qed
finally show ?thesis by simp
qed
thus ?thesis
using f 1 2 B⇩0.comp_char [of "map⇩o⇩b⇩j (A⇩0.cod f)" "F⇩0.map⇩0 f"]
B⇩0.comp_char [of "G⇩0.map⇩0 f" "map⇩o⇩b⇩j (A⇩0.dom f)"]
F⇩0.map⇩0_def G⇩0.map⇩0_def map⇩o⇩b⇩j_def
by simp
qed
qed
qed
qed
proposition is_natural_transformation:
shows "natural_transformation A⇩0.comp B⇩0.comp F⇩0.map⇩0 G⇩0.map⇩0 τ.map"
..
end
subsection "Self-Enriched Case"
text‹
Here we show that a closed monoidal category ‹C›, regarded as a category enriched
in itself, it is isomorphic to its own underlying category. This is useful,
because it is somewhat less cumbersome to work directly in the category ‹C›
than in the higher-type version that results from the underlying category construction.
Kelly often regards these two categories as identical.
›
locale self_enriched_category =
elementary_closed_monoidal_category +
enriched_category C T α ι ‹Collect ide› exp Id Comp
begin
sublocale UC: underlying_category C T α ι ‹Collect ide› exp Id Comp ..
abbreviation toUC
where "toUC g ≡ if arr g
then UC.MkArr (dom g) (cod g) (g⇧↑)
else UC.null"
lemma toUC_simps [simp]:
assumes "arr f"
shows "UC.arr (toUC f)"
and "UC.dom (toUC f) = toUC (dom f)"
and "UC.cod (toUC f) = toUC (cod f)"
using assms UC.arr_char UC.dom_char UC.cod_char UP_def
comp_cod_arr Id_def
by auto
lemma toUC_in_hom [intro]:
assumes "arr f"
shows "UC.in_hom (toUC f) (UC.MkIde (dom f)) (UC.MkIde (cod f))"
using assms toUC_simps by fastforce
sublocale toUC: "functor" C UC.comp toUC
using toUC_simps UP_comp UC.COMP_def
by unfold_locales auto
abbreviation frmUC
where "frmUC g ≡ if UC.arr g
then (UC.Map g)⇧↓[UC.Dom g, UC.Cod g]
else null"
lemma frmUC_simps [simp]:
assumes "UC.arr f"
shows "arr (frmUC f)"
and "dom (frmUC f) = frmUC (UC.dom f)"
and "cod (frmUC f) = frmUC (UC.cod f)"
using assms UC.arr_char UC.dom_char UC.cod_char Uncurry_Curry
Id_def lunit_in_hom DN_def
by auto
lemma frmUC_in_hom [intro]:
assumes "UC.in_hom f a b"
shows "«frmUC f : frmUC a → frmUC b»"
using assms frmUC_simps by blast
lemma DN_Map_comp:
assumes "UC.seq g f"
shows "(UC.Map (UC.comp g f))⇧↓[UC.Dom f, UC.Cod g] =
(UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f]"
proof -
have "(UC.Map (UC.comp g f))⇧↓[UC.Dom f, UC.Cod g] =
((UC.Map (UC.comp g f))⇧↓[UC.Dom f, UC.Cod g])⇧↑
⇧↓[UC.Dom f, UC.Cod g]"
using assms UC.arr_char UC.seq_char [of g f] by fastforce
also have "... = ((UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f])⇧↑
⇧↓[UC.Dom f, UC.Cod g]"
proof -
have "((UC.Map (UC.comp g f))⇧↓[UC.Dom f, UC.Cod g])⇧↑ =
UC.Map (UC.comp g f)"
using assms UC.arr_char UC.seq_char [of g f] by fastforce
also have "... = Comp (UC.Dom f) (UC.Dom g) (UC.Cod g) ⋅
(UC.Map g ⊗ UC.Map f) ⋅ ι⇧-⇧1"
using assms UC.Map_comp UC.seq_char by blast
also have "... = Comp (UC.Dom f) (UC.Dom g) (UC.Cod g) ⋅
(((UC.Map g)⇧↓[UC.Dom g, UC.Cod g])⇧↑ ⊗
((UC.Map f)⇧↓[UC.Dom f, UC.Cod f])⇧↑) ⋅ ι⇧-⇧1"
using assms UC.seq_char UC.arr_char by auto
also have "... = ((UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f])⇧↑"
proof -
have "dom ((UC.Map f)⇧↓[UC.Dom f, UC.Cod f]) = UC.Dom f"
using assms DN_Id UC.Dom_in_Obj frmUC_simps(2) by auto
moreover have "cod ((UC.Map f)⇧↓[UC.Dom f, UC.Cod f]) = UC.Cod f"
using assms DN_Id UC.Cod_in_Obj frmUC_simps(3) by auto
moreover have "seq ((UC.Map g)⇧↓[UC.Cod f, UC.Cod g])
((UC.Map f)⇧↓[UC.Dom f, UC.Cod f])"
using assms frmUC_simps(1-3) UC.seq_char
apply (intro seqI)
apply auto[3]
by metis+
ultimately show ?thesis
using assms UP_comp UP_DN(2) UC.arr_char UC.seq_char
in_homE seqI
by auto
qed
finally show ?thesis by simp
qed
also have "... = (UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f]"
proof -
have 2: "seq ((UC.Map g)⇧↓[UC.Dom g, UC.Cod g])
((UC.Map f)⇧↓[UC.Dom f, UC.Cod f])"
using assms frmUC_simps(1-3) UC.seq_char
apply (elim UC.seqE, intro seqI)
apply auto[3]
by metis+
moreover have "dom ((UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f]) =
UC.Dom f"
using assms 2 UC.Dom_comp UC.arr_char [of f] by auto
moreover have "cod ((UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f]) =
UC.Cod g"
using assms 2 UC.Cod_comp UC.arr_char [of g] by auto
ultimately show ?thesis
using assms
UP_DN(3) [of "(UC.Map g)⇧↓[UC.Dom g, UC.Cod g] ⋅
(UC.Map f)⇧↓[UC.Dom f, UC.Cod f]"]
by simp
qed
finally show ?thesis by blast
qed
sublocale frmUC: "functor" UC.comp C frmUC
proof
show "⋀f. ¬ UC.arr f ⟹ frmUC f = null"
by simp
show "⋀f. UC.arr f ⟹ arr (frmUC f)"
using UC.arr_char frmUC_simps(1) by blast
show "⋀f. UC.arr f ⟹ dom (frmUC f) = frmUC (UC.dom f)"
using frmUC_simps(2) by blast
show "⋀f. UC.arr f ⟹ cod (frmUC f) = frmUC (UC.cod f)"
using frmUC_simps(3) by blast
fix f g
assume fg: "UC.seq g f"
show "frmUC (UC.comp g f) = frmUC g ⋅ frmUC f"
using fg UC.seq_char DN_Map_comp by auto
qed
sublocale inverse_functors UC.comp C toUC frmUC
proof
show "frmUC ∘ toUC = map"
using is_extensional comp_arr_dom comp_assoc Uncurry_Curry by auto
interpret to_frm: composite_functor UC.comp C UC.comp frmUC toUC ..
show "toUC ∘ frmUC = UC.map"
proof
fix f
show "(toUC ∘ frmUC) f = UC.map f"
proof (cases "UC.arr f")
show "¬ UC.arr f ⟹ ?thesis"
using UC.is_extensional by auto
assume f: "UC.arr f"
show ?thesis
proof (intro UC.arr_eqI)
show "UC.arr ((toUC ∘ frmUC) f)"
using f by blast
show "UC.arr (UC.map f)"
using f by blast
show "UC.Dom ((toUC ∘ frmUC) f) = UC.Dom (UC.map f)"
using f UC.Dom_in_Obj frmUC.preserves_arr UC.arr_char [of f]
by auto
show "UC.Cod (to_frm.map f) = UC.Cod (UC.map f)"
using f UC.arr_char [of f] by auto
show "UC.Map (to_frm.map f) = UC.Map (UC.map f)"
using f UP_DN UC.arr_char [of f] by auto
qed
qed
qed
qed
lemma inverse_functors_toUC_frmUC:
shows "inverse_functors UC.comp C toUC frmUC"
..
corollary enriched_category_isomorphic_to_underlying_category:
shows "isomorphic_categories UC.comp C"
using inverse_functors_toUC_frmUC
by unfold_locales blast
end
section "Opposite of an Enriched Category"
text‹
Construction of the opposite of an enriched category
(\emph{cf.}~\<^cite>‹"kelly-enriched-category"› (1.19)) requires that the underlying monoidal
category be symmetric, in order to introduce the required ``twist'' in the definition
of composition.
›
locale opposite_enriched_category =
symmetric_monoidal_category +
EC: enriched_category
begin
interpretation elementary_symmetric_monoidal_category
C tensor unity lunit runit assoc sym
using induces_elementary_symmetric_monoidal_category⇩C⇩M⇩C by blast
abbreviation (input) Hom⇩o⇩p
where "Hom⇩o⇩p a b ≡ Hom b a"
abbreviation Comp⇩o⇩p
where "Comp⇩o⇩p a b c ≡ Comp c b a ⋅ 𝗌[Hom c b, Hom b a]"
sublocale enriched_category C T α ι Obj Hom⇩o⇩p Id Comp⇩o⇩p
proof
show *: "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹ ide (Hom b a)"
using EC.ide_Hom by blast
show "⋀a. a ∈ Obj ⟹ «Id a : ℐ → Hom a a»"
using EC.Id_in_hom by blast
show **: "⋀a b c. ⟦a ∈ Obj; b ∈ Obj; c ∈ Obj⟧ ⟹
«Comp⇩o⇩p a b c : Hom c b ⊗ Hom b a → Hom c a»"
using sym_in_hom EC.ide_Hom EC.Comp_in_hom by auto
show "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹
Comp⇩o⇩p a a b ⋅ (Hom b a ⊗ Id a) = 𝗋[Hom b a]"
proof -
fix a b
assume a: "a ∈ Obj" and b: "b ∈ Obj"
have "Comp⇩o⇩p a a b ⋅ (Hom b a ⊗ Id a) =
Comp b a a ⋅ 𝗌[Hom b a, Hom a a] ⋅ (Hom b a ⊗ Id a)"
using comp_assoc by simp
also have "... = Comp b a a ⋅ (Id a ⊗ Hom b a) ⋅ 𝗌[Hom b a, ℐ]"
using a b sym_naturality [of "Hom b a" "Id a"] sym_in_hom
EC.Id_in_hom EC.ide_Hom
by fastforce
also have "... = (Comp b a a ⋅ (Id a ⊗ Hom b a)) ⋅ 𝗌[Hom b a, ℐ]"
using comp_assoc by simp
also have "... = 𝗅[Hom b a] ⋅ 𝗌[Hom b a, ℐ]"
using a b EC.Comp_Id_Hom by simp
also have "... = 𝗋[Hom b a] "
using a b unitor_coherence EC.ide_Hom by presburger
finally show "Comp⇩o⇩p a a b ⋅ (Hom b a ⊗ Id a) = 𝗋[Hom b a]"
by blast
qed
show "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹
Comp⇩o⇩p a b b ⋅ (Id b ⊗ Hom b a) = 𝗅[Hom b a]"
proof -
fix a b
assume a: "a ∈ Obj" and b: "b ∈ Obj"
have "Comp⇩o⇩p a b b ⋅ (Id b ⊗ Hom b a) =
Comp b b a ⋅ 𝗌[Hom b b, Hom b a] ⋅ (Id b ⊗ Hom b a)"
using comp_assoc by simp
also have "... = Comp b b a ⋅ (Hom b a ⊗ Id b) ⋅ 𝗌[ℐ, Hom b a]"
using a b sym_naturality [of "Id b" "Hom b a"] sym_in_hom
EC.Id_in_hom EC.ide_Hom
by force
also have "... = (Comp b b a ⋅ (Hom b a ⊗ Id b)) ⋅ 𝗌[ℐ, Hom b a]"
using comp_assoc by simp
also have "... = 𝗋[Hom b a] ⋅ 𝗌[ℐ, Hom b a]"
using a b EC.Comp_Hom_Id by simp
also have "... = 𝗅[Hom b a]"
proof -
have "𝗋[Hom b a] ⋅ 𝗌[ℐ, Hom b a] =
(𝗅[Hom b a] ⋅ 𝗌[Hom b a, ℐ]) ⋅ 𝗌[ℐ, Hom b a]"
using a b unitor_coherence EC.ide_Hom by simp
also have "... = 𝗅[Hom b a] ⋅ 𝗌[Hom b a, ℐ] ⋅ 𝗌[ℐ, Hom b a]"
using comp_assoc by simp
also have "... = 𝗅[Hom b a]"
using a b comp_arr_dom comp_arr_inv sym_inverse by simp
finally show ?thesis by blast
qed
finally show "Comp⇩o⇩p a b b ⋅ (Id b ⊗ Hom b a) = 𝗅[Hom b a]"
by blast
qed
show "⋀a b c d. ⟦a ∈ Obj; b ∈ Obj; c ∈ Obj; d ∈ Obj⟧ ⟹
Comp⇩o⇩p a b d ⋅ (Comp⇩o⇩p b c d ⊗ Hom b a) =
Comp⇩o⇩p a c d ⋅ (Hom d c ⊗ Comp⇩o⇩p a b c) ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
proof -
fix a b c d
assume a: "a ∈ Obj" and b: "b ∈ Obj" and c: "c ∈ Obj" and d: "d ∈ Obj"
have "Comp⇩o⇩p a b d ⋅ (Comp⇩o⇩p b c d ⊗ Hom b a) =
Comp⇩o⇩p a b d ⋅ (Comp d c b ⊗ Hom b a) ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using a b c d ** interchange comp_ide_arr ide_in_hom seqI'
EC.ide_Hom
by metis
also have "... = (Comp d b a ⋅
(𝗌[Hom d b, Hom b a] ⋅ (Comp d c b ⊗ Hom b a)) ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
using comp_assoc by simp
also have "... = (Comp d b a ⋅
((Hom b a ⊗ Comp d c b) ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a]) ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
using a b c d sym_naturality EC.Comp_in_hom ide_char
in_homE EC.ide_Hom
by metis
also have "... = (Comp d b a ⋅ (Hom b a ⊗ Comp d c b)) ⋅
(𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
using comp_assoc by simp
also have "... = (Comp d c a ⋅ (Comp c b a ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]) ⋅
(𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
proof -
have "Comp d b a ⋅ (Hom b a ⊗ Comp d c b) =
(Comp d b a ⋅ (Hom b a ⊗ Comp d c b)) ⋅
(Hom b a ⊗ Hom c b ⊗ Hom d c)"
using a b c d EC.Comp_in_hom arrI comp_in_homI ide_in_hom
tensor_in_hom EC.ide_Hom
proof -
have "seq (Comp d b a) (Hom b a ⊗ Comp d c b)"
using a b c d EC.Comp_in_hom arrI comp_in_homI ide_in_hom
tensor_in_hom EC.ide_Hom
by meson
moreover have "dom (Comp d b a ⋅ (Hom b a ⊗ Comp d c b)) =
(Hom b a ⊗ Hom c b ⊗ Hom d c)"
using a b c d EC.Comp_in_hom dom_comp dom_tensor ideD(1-2)
in_homE calculation EC.ide_Hom
by metis
ultimately show ?thesis
using a b c d EC.Comp_in_hom comp_arr_dom by metis
qed
also have "... =
(Comp d b a ⋅ (Hom b a ⊗ Comp d c b)) ⋅
𝖺[Hom b a, Hom c b, Hom d c] ⋅ 𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]"
using a b c d comp_assoc_assoc'(1) EC.ide_Hom by simp
also have "... = (Comp d b a ⋅ (Hom b a ⊗ Comp d c b) ⋅
𝖺[Hom b a, Hom c b, Hom d c]) ⋅
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]"
using comp_assoc by simp
also have "... = (Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]"
using a b c d EC.Comp_assoc by simp
also have "... = Comp d c a ⋅ (Comp c b a ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]"
using comp_assoc by simp
finally have "Comp d b a ⋅ (Hom b a ⊗ Comp d c b) =
Comp d c a ⋅ (Comp c b a ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c]"
by blast
thus ?thesis by simp
qed
also have "... = (Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
(𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
using comp_assoc by simp
finally have LHS: "(Comp d b a ⋅ 𝗌[Hom d b, Hom b a]) ⋅
(Comp d c b ⋅ 𝗌[Hom d c, Hom c b] ⊗ Hom b a) =
(Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
(𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
by blast
have "Comp⇩o⇩p a c d ⋅ (Hom d c ⊗ Comp⇩o⇩p a b c) ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
Comp d c a ⋅
(𝗌[Hom d c, Hom c a] ⋅
(Hom d c ⊗ Comp c b a ⋅ 𝗌[Hom c b, Hom b a])) ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using comp_assoc by simp
also have "... =
Comp d c a ⋅
((Comp c b a ⋅ 𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a]) ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using a b c d ** sym_naturality ide_char in_homE EC.ide_Hom
by metis
also have "... =
Comp d c a ⋅
(((Comp c b a ⊗ Hom d c) ⋅ (𝗌[Hom c b, Hom b a] ⊗ Hom d c)) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a]) ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using a b c d ** interchange comp_arr_dom ideD(1-2)
in_homE EC.ide_Hom
by metis
also have "... = (Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
((𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a])"
using comp_assoc by simp
also have "... = (Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
(𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
proof -
have "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
proof -
have 1: "𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
proof -
have "𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
(𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
𝖺[Hom c b, Hom b a, Hom d c]) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using a b c d comp_assoc_assoc'(2) comp_cod_arr by simp
also have "... =
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
𝖺[Hom c b, Hom b a, Hom d c] ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using comp_assoc by simp
also have "... =
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using a b c d assoc_coherence EC.ide_Hom by auto
finally show ?thesis by blast
qed
have 2: "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
inv 𝖺[Hom c b, Hom d c, Hom b a]"
proof -
have "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) =
inv ((Hom c b ⊗ 𝗌[Hom b a, Hom d c]) ⋅
𝖺[Hom c b, Hom b a, Hom d c] ⋅
(𝗌[Hom b a, Hom c b] ⊗ Hom d c))"
proof -
have "inv ((Hom c b ⊗ 𝗌[Hom b a, Hom d c]) ⋅
𝖺[Hom c b, Hom b a, Hom d c] ⋅
(𝗌[Hom b a, Hom c b] ⊗ Hom d c)) =
inv (𝖺[Hom c b, Hom b a, Hom d c] ⋅
(𝗌[Hom b a, Hom c b] ⊗ Hom d c)) ⋅
inv (Hom c b ⊗ 𝗌[Hom b a, Hom d c])"
using a b c d EC.ide_Hom
inv_comp [of "𝖺[Hom c b, Hom b a, Hom d c] ⋅
(𝗌[Hom b a, Hom c b] ⊗ Hom d c)"
"Hom c b ⊗ 𝗌[Hom b a, Hom d c]"]
by fastforce
also have "... =
(inv (𝗌[Hom b a, Hom c b] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c]) ⋅
inv (Hom c b ⊗ 𝗌[Hom b a, Hom d c])"
using a b c d EC.ide_Hom inv_comp by simp
also have "... =
((𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c]) ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a])"
using a b c d sym_inverse inverse_unique
apply auto[1]
by (metis *)
finally show ?thesis
using comp_assoc by simp
qed
also have "... =
inv (𝖺[Hom c b, Hom d c, Hom b a] ⋅
𝗌[Hom b a, Hom c b ⊗ Hom d c] ⋅
𝖺[Hom b a, Hom c b, Hom d c])"
using a b c d assoc_coherence EC.ide_Hom by auto
also have "... =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
inv 𝗌[Hom b a, Hom c b ⊗ Hom d c] ⋅
𝖺⇧-⇧1[Hom c b, Hom d c, Hom b a]"
using a b c d EC.ide_Hom inv_comp inv_tensor comp_assoc
isos_compose
by auto
also have "... =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
𝖺⇧-⇧1[Hom c b, Hom d c, Hom b a]"
using a b c d sym_inverse inv_is_inverse inverse_unique
by (metis tensor_preserves_ide EC.ide_Hom)
finally show ?thesis by blast
qed
hence "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a] =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
inv 𝖺[Hom c b, Hom d c, Hom b a] ⋅
𝖺[Hom c b, Hom d c, Hom b a]"
by (metis comp_assoc)
hence 3: "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a] =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a]"
using a b c comp_arr_dom d by fastforce
have "(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝗌[Hom d c, Hom c b ⊗ Hom b a] ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
(𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using 1 by simp
also have "... =
((𝗌[Hom c b, Hom b a] ⊗ Hom d c) ⋅
𝖺⇧-⇧1[Hom c b, Hom b a, Hom d c] ⋅
(Hom c b ⊗ 𝗌[Hom d c, Hom b a]) ⋅
𝖺[Hom c b, Hom d c, Hom b a]) ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using comp_assoc by simp
also have "... =
(𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a]) ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using 3 by simp
also have "... =
𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a)"
using comp_assoc by simp
finally show ?thesis by simp
qed
thus ?thesis by auto
qed
finally have RHS: "Comp⇩o⇩p a c d ⋅
(Hom d c ⊗ Comp⇩o⇩p a b c) ⋅
𝖺[Hom d c, Hom c b, Hom b a] =
(Comp d c a ⋅ (Comp c b a ⊗ Hom d c)) ⋅
(𝖺⇧-⇧1[Hom b a, Hom c b, Hom d c] ⋅
𝗌[Hom c b ⊗ Hom d c, Hom b a] ⋅
(𝗌[Hom d c, Hom c b] ⊗ Hom b a))"
by blast
show "Comp⇩o⇩p a b d ⋅ (Comp⇩o⇩p b c d ⊗ Hom b a) =
Comp⇩o⇩p a c d ⋅ (Hom d c ⊗ Comp⇩o⇩p a b c) ⋅
𝖺[Hom d c, Hom c b, Hom b a]"
using LHS RHS by simp
qed
qed
end
subsection "Relation between ‹(-⇧o⇧p)⇩0› and ‹(-⇩0)⇧o⇧p›"
text‹
Kelly (comment before (1.22)) claims, for a category ‹A› enriched in a symmetric
monoidal category, that we have ‹(A⇧o⇧p)⇩0 = (A⇩0)⇧o⇧p›. This point becomes somewhat
confusing, as it depends on the particular formalization one adopts for the
notion of ``category''.
\sloppypar
As we can see from the next two facts (‹Op_UC_hom_char› and ‹UC_Op_hom_char›),
the hom-sets ‹Op.UC.hom a b› and ‹UC.Op.hom a b› are both obtained by using ‹UC.MkArr›
to ``tag'' elements of ‹hom ℐ (Hom (UC.Dom b) (UC.Dom a))› with ‹UC.Dom a› and ‹UC.Dom b›.
These two hom-sets are formally distinct if (as is the case for us), the arrows of a
category are regarded as containing information about their domain and codomain,
so that the hom-sets are disjoint. On the other hand, if one regards a category
as a collection of mappings that assign to each pair of objects ‹a› and ‹b›
a corresponding set ‹hom a b›, then the hom-sets ‹Op.UC.hom a b› and ‹UC.Op.hom a b›
could be arranged to be equal, as Kelly suggests.
›
locale category_enriched_in_symmetric_monoidal_category =
symmetric_monoidal_category +
enriched_category
begin
interpretation elementary_symmetric_monoidal_category
C tensor unity lunit runit assoc sym
using induces_elementary_symmetric_monoidal_category⇩C⇩M⇩C by blast
interpretation Op: opposite_enriched_category C T α ι σ Obj Hom Id Comp ..
interpretation Op⇩0: underlying_category C T α ι Obj Op.Hom⇩o⇩p Id Op.Comp⇩o⇩p
..
interpretation UC: underlying_category C T α ι Obj Hom Id Comp ..
interpretation UC.Op: dual_category UC.comp ..
lemma Op_UC_hom_char:
assumes "UC.ide a" and "UC.ide b"
shows "Op⇩0.hom a b =
UC.MkArr (UC.Dom a) (UC.Dom b) `
hom ℐ (Hom (UC.Dom b) (UC.Dom a))"
using assms Op⇩0.hom_char [of "UC.Dom a" "UC.Dom b"]
UC.ide_char [of a] UC.ide_char [of b] UC.arr_char
by force
lemma UC_Op_hom_char:
assumes "UC.ide a" and "UC.ide b"
shows "UC.Op.hom a b =
UC.MkArr (UC.Dom b) (UC.Dom a) `
hom ℐ (Hom (UC.Dom b) (UC.Dom a))"
using assms UC.Op.hom_char UC.hom_char [of "UC.Dom b" "UC.Dom a"]
UC.ide_char⇩C⇩C
by simp
abbreviation toUCOp
where "toUCOp f ≡ if Op⇩0.arr f
then UC.MkArr (Op⇩0.Cod f) (Op⇩0.Dom f) (Op⇩0.Map f)
else UC.Op.null"
sublocale toUCOp: "functor" Op⇩0.comp UC.Op.comp toUCOp
proof
show "⋀f. ¬ Op⇩0.arr f ⟹ toUCOp f = UC.Op.null"
by simp
show 1: "⋀f. Op⇩0.arr f ⟹ UC.Op.arr (toUCOp f)"
using Op⇩0.arr_char by auto
show "⋀f. Op⇩0.arr f ⟹ UC.Op.dom (toUCOp f) = toUCOp (Op⇩0.dom f)"
using 1 by simp
show "⋀f. Op⇩0.arr f ⟹ UC.Op.cod (toUCOp f) = toUCOp (Op⇩0.cod f)"
using 1 by simp
show "⋀g f. Op⇩0.seq g f ⟹
toUCOp (Op⇩0.comp g f) = UC.Op.comp (toUCOp g) (toUCOp f)"
proof -
fix f g
assume fg: "Op⇩0.seq g f"
show "toUCOp (Op⇩0.comp g f) = UC.Op.comp (toUCOp g) (toUCOp f)"
proof (intro UC.arr_eqI)
show "UC.arr (toUCOp (Op⇩0.comp g f))"
using 1 fg UC.Op.arr_char by blast
show 2: "UC.arr (UC.Op.comp (toUCOp g) (toUCOp f))"
using 1 Op⇩0.seq_char UC.seq_char fg by force
show "Op⇩0.Dom (toUCOp (Op⇩0.comp g f)) =
Op⇩0.Dom (UC.Op.comp (toUCOp g) (toUCOp f))"
using 1 2 fg Op⇩0.seq_char by fastforce
show "Op⇩0.Cod (toUCOp (Op⇩0.comp g f)) =
Op⇩0.Cod (UC.Op.comp (toUCOp g) (toUCOp f))"
using 1 2 fg Op⇩0.seq_char by fastforce
show "Op⇩0.Map (toUCOp (Op⇩0.comp g f)) =
Op⇩0.Map (UC.Op.comp (toUCOp g) (toUCOp f))"
proof -
have "Op⇩0.Map (toUCOp (Op⇩0.comp g f)) =
Op.Comp⇩o⇩p (UC.Dom f) (UC.Dom g) (UC.Cod g) ⋅
(UC.Map g ⊗ UC.Map f) ⋅ ι⇧-⇧1"
using 1 2 fg Op⇩0.seq_char by auto
also have "... = Comp (Op⇩0.Cod g) (Op⇩0.Dom g) (Op⇩0.Dom f) ⋅
(𝗌[Hom (Op⇩0.Cod g) (Op⇩0.Dom g),
Hom (Op⇩0.Dom g) (Op⇩0.Dom f)] ⋅
(Op⇩0.Map g ⊗ Op⇩0.Map f)) ⋅ ι⇧-⇧1"
using comp_assoc by simp
also have "... = Comp (Op⇩0.Cod g) (Op⇩0.Dom g) (Op⇩0.Dom f) ⋅
((Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ 𝗌[ℐ, ℐ]) ⋅ ι⇧-⇧1"
using fg Op⇩0.seq_char Op⇩0.arr_char sym_naturality
by (metis (no_types, lifting) in_homE mem_Collect_eq)
also have "... = Comp (Op⇩0.Cod g) (Op⇩0.Dom g) (Op⇩0.Dom f) ⋅
(Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ 𝗌[ℐ, ℐ] ⋅ ι⇧-⇧1"
using comp_assoc by simp
also have "... = Comp (Op⇩0.Cod g) (Op⇩0.Dom g) (Op⇩0.Dom f) ⋅
(Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ ι⇧-⇧1"
using sym_inv_unit ι_def monoidal_category_axioms
by (simp add: monoidal_category.unitor_coincidence(1))
finally have "Op⇩0.Map (toUCOp (Op⇩0.comp g f)) =
Comp (Op⇩0.Cod g) (Op⇩0.Dom g) (Op⇩0.Dom f) ⋅
(Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ ι⇧-⇧1"
by blast
also have "... = Op⇩0.Map (UC.Op.comp (toUCOp g) (toUCOp f))"
using fg 2 by auto
finally show ?thesis by blast
qed
qed
qed
qed
lemma functor_toUCOp:
shows "functor Op⇩0.comp UC.Op.comp toUCOp"
..
abbreviation toOp⇩0
where "toOp⇩0 f ≡ if UC.Op.arr f
then Op⇩0.MkArr (UC.Cod f) (UC.Dom f) (UC.Map f)
else Op⇩0.null"
sublocale toOp⇩0: "functor" UC.Op.comp Op⇩0.comp toOp⇩0
proof
show "⋀f. ¬ UC.Op.arr f ⟹ toOp⇩0 f = Op⇩0.null"
by simp
show 1: "⋀f. UC.Op.arr f ⟹ Op⇩0.arr (toOp⇩0 f)"
using UC.arr_char by simp
show "⋀f. UC.Op.arr f ⟹ Op⇩0.dom (toOp⇩0 f) = toOp⇩0 (UC.Op.dom f)"
using 1 by auto
show "⋀f. UC.Op.arr f ⟹ Op⇩0.cod (toOp⇩0 f) = toOp⇩0 (UC.Op.cod f)"
using 1 by auto
show "⋀g f. UC.Op.seq g f ⟹
toOp⇩0 (UC.Op.comp g f) = Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f)"
proof -
fix f g
assume fg: "UC.Op.seq g f"
show "toOp⇩0 (UC.Op.comp g f) = Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f)"
proof (intro Op⇩0.arr_eqI)
show "Op⇩0.arr (toOp⇩0 (UC.Op.comp g f))"
using fg 1 by blast
show 2: "Op⇩0.seq (toOp⇩0 g) (toOp⇩0 f)"
using fg 1 UC.seq_char UC.arr_char Op⇩0.seq_char by fastforce
show "Op⇩0.Dom (toOp⇩0 (UC.Op.comp g f)) =
Op⇩0.Dom (Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f))"
using fg 1 2 Op⇩0.dom_char Op⇩0.cod_char UC.seq_char Op⇩0.seq_char
by auto
show "Op⇩0.Cod (toOp⇩0 (UC.Op.comp g f)) =
Op⇩0.Cod (Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f))"
using fg 1 2 Op⇩0.dom_char Op⇩0.cod_char UC.seq_char Op⇩0.seq_char
by auto
show "Op⇩0.Map (toOp⇩0 (UC.Op.comp g f)) =
Op⇩0.Map (Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f))"
proof -
have "Op⇩0.Map (Op⇩0.comp (toOp⇩0 g) (toOp⇩0 f)) =
Op.Comp⇩o⇩p (Op⇩0.Dom (toOp⇩0 f)) (Op⇩0.Dom (toOp⇩0 g))
(Op⇩0.Cod (toOp⇩0 g)) ⋅
(Op⇩0.Map (toOp⇩0 g) ⊗ Op⇩0.Map (toOp⇩0 f)) ⋅ inv ι"
using fg 1 2 UC.seq_char by auto
also have "... =
Comp (Op⇩0.Dom g) (Op⇩0.Cod g) (Op⇩0.Cod f) ⋅
(𝗌[Hom (Op⇩0.Dom g) (Op⇩0.Cod g),
Hom (Op⇩0.Cod g) (Op⇩0.Cod f)] ⋅
(Op⇩0.Map g ⊗ Op⇩0.Map f)) ⋅ inv ι"
using fg comp_assoc by auto
also have "... =
Comp (Op⇩0.Dom g) (Op⇩0.Cod g) (Op⇩0.Cod f) ⋅
((Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ 𝗌[unity, unity]) ⋅ inv ι"
using fg UC.seq_char UC.arr_char sym_naturality
by (metis (no_types, lifting) in_homE UC.Op.arr_char
UC.Op.comp_def mem_Collect_eq)
also have "... =
Comp (Op⇩0.Dom g) (Op⇩0.Cod g) (Op⇩0.Cod f) ⋅
(Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ 𝗌[unity, unity] ⋅ inv ι"
using comp_assoc by simp
also have "... =
Comp (Op⇩0.Dom g) (Op⇩0.Cod g) (Op⇩0.Cod f) ⋅
(Op⇩0.Map f ⊗ Op⇩0.Map g) ⋅ inv ι"
using sym_inv_unit ι_def monoidal_category_axioms
by (simp add: monoidal_category.unitor_coincidence(1))
also have "... = Op⇩0.Map (toOp⇩0 (UC.Op.comp g f))"
using fg UC.seq_char by simp
finally show ?thesis by argo
qed
qed
qed
qed
lemma functor_toOp⇩0:
shows "functor UC.Op.comp Op⇩0.comp toOp⇩0"
..
sublocale inverse_functors UC.Op.comp Op⇩0.comp toUCOp toOp⇩0
using Op⇩0.MkArr_Map toUCOp.preserves_reflects_arr Op⇩0.is_extensional
UC.MkArr_Map toOp⇩0.preserves_reflects_arr UC.Op.is_extensional
by unfold_locales auto
lemma inverse_functors_toUCOp_toOp⇩0:
shows "inverse_functors UC.Op.comp Op⇩0.comp toUCOp toOp⇩0"
..
end
section "Enriched Hom Functors"
text‹
Here we exhibit covariant and contravariant hom functors as enriched functors,
as in \<^cite>‹"kelly-enriched-category"› Section 1.6. We don't bother to exhibit
them as partial functors of a single two-argument functor, as to do so would
require us to define the tensor product of enriched categories; something that would
require more technology for proving coherence conditions than we have developed
at present.
›
subsection "Covariant Case"
locale covariant_Hom =
monoidal_category +
C: elementary_closed_monoidal_category +
enriched_category +
fixes x :: 'o
assumes x: "x ∈ Obj"
begin
interpretation C: enriched_category C T α ι ‹Collect ide› exp C.Id C.Comp
using C.is_enriched_in_itself by simp
interpretation C: self_enriched_category C T α ι exp eval Curry ..
abbreviation hom⇩o
where "hom⇩o ≡ Hom x"
abbreviation hom⇩a
where "hom⇩a ≡ λb c. if b ∈ Obj ∧ c ∈ Obj
then Curry[Hom b c, Hom x b, Hom x c] (Comp x b c)
else null"
sublocale enriched_functor C T α ι
Obj Hom Id Comp
‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a
proof
show "⋀a b. a ∉ Obj ∨ b ∉ Obj ⟹ hom⇩a a b = null"
by auto
show "⋀y. y ∈ Obj ⟹ hom⇩o y ∈ Collect ide"
using x ide_Hom by auto
show *: "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹
«hom⇩a a b : Hom a b → exp (hom⇩o a) (hom⇩o b)»"
using x by auto
show "⋀a. a ∈ Obj ⟹ hom⇩a a a ⋅ Id a = C.Id (hom⇩o a)"
using x Comp_Id_Hom Comp_in_hom Id_in_hom C.Id_def C.comp_Curry_arr
apply auto[1]
by (metis ide_Hom)
show "⋀a b c. ⟦a ∈ Obj; b ∈ Obj; c ∈ Obj⟧ ⟹
C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅
(hom⇩a b c ⊗ hom⇩a a b) =
hom⇩a a c ⋅ Comp a b c"
proof -
fix a b c
assume a: "a ∈ Obj" and b: "b ∈ Obj" and c: "c ∈ Obj"
have "Uncurry[hom⇩o a, hom⇩o c]
(C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b)) =
Uncurry[hom⇩o a, hom⇩o c] (hom⇩a a c ⋅ Comp a b c)"
proof -
have "Uncurry[hom⇩o a, hom⇩o c]
(C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b)) =
Uncurry[hom⇩o a, hom⇩o c]
(Curry[exp (hom⇩o b) (hom⇩o c) ⊗ exp (hom⇩o a) (hom⇩o b), hom⇩o a,
hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b),
hom⇩o a]) ⋅
(hom⇩a b c ⊗ hom⇩a a b))"
using C.Comp_def by simp
also have "... =
Uncurry[hom⇩o a, hom⇩o c]
(Curry[Hom b c ⊗ Hom a b, hom⇩o a, hom⇩o c]
((eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b),
hom⇩o a]) ⋅
((hom⇩a b c ⊗ hom⇩a a b) ⊗ hom⇩o a)))"
proof -
have "«hom⇩a b c ⊗ hom⇩a a b :
Hom b c ⊗ Hom a b →
exp (hom⇩o b) (hom⇩o c) ⊗ exp (hom⇩o a) (hom⇩o b)»"
using x a b c * by force
moreover have "«eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a]
: (exp (hom⇩o b) (hom⇩o c) ⊗ exp (hom⇩o a) (hom⇩o b))
⊗ hom⇩o a
→ hom⇩o c»"
using x a b c by simp
ultimately show ?thesis
using x a b c C.comp_Curry_arr by simp
qed
also have "... =
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a]) ⋅
((hom⇩a b c ⊗ hom⇩a a b) ⊗ hom⇩o a)"
using x a b c
C.Uncurry_Curry
[of "Hom b c ⊗ Hom a b" "hom⇩o a" "hom⇩o c"
"(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a]) ⋅
((Curry[Hom b c, hom⇩o b, hom⇩o c] (Comp x b c) ⊗
Curry[Hom a b, hom⇩o a, hom⇩o b] (Comp x a b))
⊗ hom⇩o a)"]
by fastforce
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a] ⋅
((hom⇩a b c ⊗ hom⇩a a b) ⊗ hom⇩o a)"
by (simp add: comp_assoc)
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅
((exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
(hom⇩a b c ⊗ hom⇩a a b ⊗ hom⇩o a)) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
using x a b c Comp_in_hom
assoc_naturality
[of "Curry[Hom b c, hom⇩o b, hom⇩o c] (Comp x b c)"
"Curry[Hom a b, hom⇩o a, hom⇩o b] (Comp x a b)"
"hom⇩o a"]
using comp_assoc by auto
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⋅
hom⇩a b c ⊗ Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b)) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
using x a b c Comp_in_hom interchange by simp
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⋅ hom⇩a b c ⊗ Comp x a b) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
using x a b c C.Uncurry_Curry Comp_in_hom by auto
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ Comp x a b) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
using x a b c
by (simp add: Comp_in_hom comp_ide_arr)
also have "... =
eval (hom⇩o b) (hom⇩o c) ⋅
((hom⇩a b c ⊗ hom⇩o b) ⋅ (Hom b c ⊗ Comp x a b)) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
proof -
have "seq (hom⇩a b c) (Hom b c)"
using x a b c Comp_in_hom C.Curry_in_hom ide_Hom by simp
moreover have "seq (hom⇩o b) (Comp x a b)"
using x a b c Comp_in_hom by fastforce
ultimately show ?thesis
using x a b c Comp_in_hom C.Curry_in_hom comp_arr_ide
comp_ide_arr ide_Hom interchange
by metis
qed
also have "... =
Uncurry[hom⇩o b, hom⇩o c] (hom⇩a b c) ⋅
(Hom b c ⊗ Comp x a b) ⋅
𝖺[Hom b c, Hom a b, hom⇩o a]"
using comp_assoc by simp
also have "... = Comp x a c ⋅ (Comp a b c ⊗ hom⇩o a)"
using x a b c C.Uncurry_Curry Comp_in_hom Comp_assoc by auto
also have "... = Uncurry[hom⇩o a, hom⇩o c]
(Curry[Hom b c ⊗ Hom a b, hom⇩o a, hom⇩o c]
(Comp x a c ⋅ (Comp a b c ⊗ hom⇩o a)))"
using x a b c Comp_in_hom comp_assoc
C.Uncurry_Curry
[of "Hom b c ⊗ Hom a b" "hom⇩o a" "hom⇩o c"
"Comp x a c ⋅ (Comp a b c ⊗ hom⇩o a)"]
by fastforce
also have "... = Uncurry[hom⇩o a, hom⇩o c] (hom⇩a a c ⋅ Comp a b c)"
using x a b c Comp_in_hom
C.comp_Curry_arr
[of "hom⇩o a" "Comp a b c" "Hom b c ⊗ Hom a b"
"Hom a c" "Comp x a c" "hom⇩o c"]
by auto
finally show ?thesis by blast
qed
hence "Curry[Hom b c ⊗ Hom a b, hom⇩o a, hom⇩o c]
(Uncurry[hom⇩o a, hom⇩o c]
(C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅
(hom⇩a b c ⊗ hom⇩a a b))) =
Curry[Hom b c ⊗ Hom a b, hom⇩o a, hom⇩o c]
(Uncurry[hom⇩o a, hom⇩o c] (hom⇩a a c ⋅ Comp a b c))"
by simp
thus "C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b) =
hom⇩a a c ⋅ Comp a b c"
using x a b c Comp_in_hom
C.Curry_Uncurry
[of "Hom b c ⊗ Hom a b" "hom⇩o a" "hom⇩o c" "hom⇩a a c ⋅ Comp a b c"]
C.Curry_Uncurry
[of "Hom b c ⊗ Hom a b" "hom⇩o a" "hom⇩o c"
"C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b)"]
by auto
qed
qed
lemma is_enriched_functor:
shows "enriched_functor C T α ι
Obj Hom Id Comp
(Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a"
..
sublocale C⇩0: underlying_category C T α ι ‹Collect ide› exp C.Id C.Comp ..
sublocale UC: underlying_category C T α ι Obj Hom Id Comp ..
sublocale UF: underlying_functor C T α ι
Obj Hom Id Comp
‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a
..
text‹
The following is Kelly's formula (1.31), for the result of applying the ordinary
functor underlying the covariant hom functor, to an arrow ‹g : ℐ → Hom b c› of ‹C⇩0›,
resulting in an arrow ‹Hom⇧→ x g : Hom x b → Hom x c› of ‹C›. The point of the result
is that this can be expressed explicitly as ‹Comp x b c ⋅ (g ⊗ hom⇩o b) ⋅ 𝗅⇧-⇧1[hom⇩o b]›.
This is all very confusing at first, because Kelly identifies ‹C› with the
underlying category ‹C⇩0› of ‹C› regarded as a self-enriched category, whereas here we
cannot ignore the fact that they are merely isomorphic via ‹C.frmUC: UC.comp → C⇩0.comp›.
There is also the bother that, for an arrow ‹g : ℐ → Hom b c› of ‹C›,
the corresponding arrow of the underlying category ‹UC› has to be formally
constructed using ‹UC.MkArr›, \emph{i.e.}~as ‹UC.MkArr b c g›.
›
lemma Kelly_1_31:
assumes "b ∈ Obj" and "c ∈ Obj" and "«g : ℐ → Hom b c»"
shows "C.frmUC (UF.map⇩0 (UC.MkArr b c g)) =
Comp x b c ⋅ (g ⊗ hom⇩o b) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
proof -
have "C.frmUC (UF.map⇩0 (UC.MkArr b c g)) =
(Curry[Hom b c, hom⇩o b, hom⇩o c] (Comp x b c) ⋅ g) ⇧↓[hom⇩o b, hom⇩o c]"
using assms x ide_Hom UF.map⇩0_def
C.UC.arr_MkArr
[of "Hom x b" "Hom x c"
"Curry[Hom b c, Hom x b, Hom x c] (Comp x b c) ⋅ g"]
by fastforce
also have "... = C.Uncurry (Hom x b) (Hom x c)
(Curry[ℐ, Hom x b, Hom x c]
(Comp x b c ⋅ (g ⊗ Hom x b))) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using assms x C.comp_Curry_arr C.DN_def
by (metis Comp_in_hom C.Curry_simps(1-2) in_homE seqI ide_Hom)
also have "... = (Comp x b c ⋅ (g ⊗ Hom x b)) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using assms x ide_Hom ide_unity
C.Uncurry_Curry
[of ℐ "Hom x b" "Hom x c" "Comp x b c ⋅ (g ⊗ Hom x b)"]
by fastforce
also have "... = Comp x b c ⋅ (g ⊗ Hom x b) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using comp_assoc by simp
finally show ?thesis by blast
qed
abbreviation map⇩0
where "map⇩0 b c g ≡ Comp x b c ⋅ (g ⊗ Hom x b) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
end
context elementary_closed_monoidal_category
begin
lemma cov_Exp_DN:
assumes "«g : ℐ → exp a b»"
and "ide a" and "ide b" and "ide x"
shows "Exp⇧→ x (g ⇧↓[a, b]) =
(Curry[exp a b, exp x a, exp x b] (Comp x a b) ⋅ g) ⇧↓[exp x a, exp x b]"
proof -
have "(Curry[exp a b, exp x a, exp x b] (Comp x a b) ⋅ g) ⇧↓[exp x a, exp x b] =
Uncurry[exp x a, exp x b]
(Curry[ℐ, exp x a, exp x b] (Comp x a b ⋅ (g ⊗ exp x a))) ⋅ 𝗅⇧-⇧1[exp x a]"
using assms DN_def
comp_Curry_arr
[of "exp x a" g ℐ "exp a b" "Comp x a b" "exp x b"]
by force
also have "... = (Comp x a b ⋅ (g ⊗ exp x a)) ⋅ 𝗅⇧-⇧1[exp x a]"
using assms Uncurry_Curry by auto
also have "... = Curry[exp a b ⊗ exp x a, x, b]
(eval a b ⋅ (exp a b ⊗ eval x a) ⋅ 𝖺[exp a b, exp x a, x]) ⋅
(g ⊗ exp x a) ⋅ 𝗅⇧-⇧1[exp x a]"
unfolding Comp_def
using assms comp_assoc by auto
also have "... = Curry[exp x a, x, b]
((eval a b ⋅ (exp a b ⊗ eval x a) ⋅ 𝖺[exp a b, exp x a, x]) ⋅
((g ⊗ exp x a) ⋅ 𝗅⇧-⇧1[exp x a] ⊗ x))"
using assms comp_Curry_arr by auto
also have "... = Curry[exp x a, x, b]
(eval a b ⋅ (exp a b ⊗ eval x a) ⋅
(𝖺[exp a b, exp x a, x] ⋅ ((g ⊗ exp x a) ⊗ x)) ⋅
(𝗅⇧-⇧1[exp x a] ⊗ x))"
using assms comp_arr_dom comp_cod_arr interchange comp_assoc by fastforce
also have "... = Curry[exp x a, x, b]
(eval a b ⋅ (exp a b ⊗ eval x a) ⋅
((g ⊗ exp x a ⊗ x) ⋅ 𝖺[ℐ, exp x a, x]) ⋅
(𝗅⇧-⇧1[exp x a] ⊗ x))"
using assms assoc_naturality [of g "exp x a" x] by auto
also have "... = Curry[exp x a, x, b]
(eval a b ⋅ ((exp a b ⊗ eval x a) ⋅ (g ⊗ exp x a ⊗ x)) ⋅
𝖺[ℐ, exp x a, x] ⋅ (𝗅⇧-⇧1[exp x a] ⊗ x))"
using assms comp_assoc by simp
also have "... = Curry[exp x a, x, b]
(eval a b ⋅ ((g ⊗ a) ⋅ (ℐ ⊗ eval x a)) ⋅
𝖺[ℐ, exp x a, x] ⋅ (𝗅⇧-⇧1[exp x a] ⊗ x))"
using assms comp_arr_dom comp_cod_arr interchange by auto
also have "... = Curry[exp x a, x, b]
(Uncurry[a, b] g ⋅ (ℐ ⊗ eval x a) ⋅ 𝗅⇧-⇧1[exp x a ⊗ x])"
using assms lunit_tensor inv_comp comp_assoc by simp
also have "... = Exp⇧→ x (g ⇧↓[a, b])"
using assms lunit'_naturality [of "eval x a"] comp_assoc DN_def by auto
finally show ?thesis by simp
qed
end
subsection "Contravariant Case"
locale contravariant_Hom =
symmetric_monoidal_category +
C: elementary_closed_symmetric_monoidal_category +
enriched_category +
fixes y :: 'o
assumes y: "y ∈ Obj"
begin
interpretation C: enriched_category C T α ι ‹Collect ide› exp C.Id C.Comp
using C.is_enriched_in_itself by simp
interpretation C: self_enriched_category C T α ι exp eval Curry ..
sublocale Op: opposite_enriched_category C T α ι σ Obj Hom Id Comp ..
abbreviation hom⇩o
where "hom⇩o ≡ λa. Hom a y"
abbreviation hom⇩a
where "hom⇩a ≡ λb c. if b ∈ Obj ∧ c ∈ Obj
then Curry[Hom c b, Hom b y, Hom c y] (Op.Comp⇩o⇩p y b c)
else null"
sublocale enriched_functor C T α ι
Obj Op.Hom⇩o⇩p Id Op.Comp⇩o⇩p
‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a
proof
show "⋀a b. a ∉ Obj ∨ b ∉ Obj ⟹ hom⇩a a b = null"
by auto
show "⋀x. x ∈ Obj ⟹ hom⇩o x ∈ Collect ide"
using y by auto
show *: "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹
«hom⇩a a b : Hom b a → exp (hom⇩o a) (hom⇩o b)»"
using y C.cnt_Exp_ide C.Curry_in_hom Op.Comp_in_hom [of y] by simp
show "⋀a. a ∈ Obj ⟹ hom⇩a a a ⋅ Id a = C.Id (hom⇩o a)"
using y Id_in_hom C.Id_def C.comp_Curry_arr Op.Comp_Id_Hom Op.Comp_in_hom
by fastforce
show "⋀a b c. ⟦a ∈ Obj; b ∈ Obj; c ∈ Obj⟧ ⟹
C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅
(hom⇩a b c ⊗ hom⇩a a b) =
hom⇩a a c ⋅ Op.Comp⇩o⇩p a b c "
proof -
fix a b c
assume a: "a ∈ Obj" and b: "b ∈ Obj" and c: "c ∈ Obj"
have "C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b) =
Curry[exp (hom⇩o b) (hom⇩o c) ⊗ exp (hom⇩o a) (hom⇩o b),
hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a]) ⋅
(hom⇩a b c ⊗ hom⇩a a b)"
using y a b c comp_assoc C.Comp_def by simp
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
((eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b),
hom⇩o a]) ⋅
((hom⇩a b c ⊗ hom⇩a a b) ⊗ hom⇩o a))"
using y a b c
C.comp_Curry_arr
[of "Hom a y" "hom⇩a b c ⊗ hom⇩a a b" "Hom c b ⊗ Hom b a"
"exp (hom⇩o b) (hom⇩o c) ⊗ exp (hom⇩o a) (hom⇩o b)"
"eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
𝖺[exp (hom⇩o b) (hom⇩o c), exp (hom⇩o a) (hom⇩o b), hom⇩o a]"
"hom⇩o c"]
by fastforce
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⊗ eval (hom⇩o a) (hom⇩o b)) ⋅
(hom⇩a b c ⊗ hom⇩a a b ⊗ hom⇩o a) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c Op.Comp_in_hom comp_assoc
C.assoc_naturality
[of "Curry[Hom c b, hom⇩o b, hom⇩o c] (Op.Comp⇩o⇩p y b c)"
"Curry[Hom b a, hom⇩o a, hom⇩o b] (Op.Comp⇩o⇩p y a b)"
"hom⇩o a"]
by auto
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⋅ hom⇩a b c ⊗
Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b)) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
proof -
have "seq (exp (hom⇩o b) (hom⇩o c)) (hom⇩a b c)"
using y a b c by force
moreover have "seq (eval (hom⇩o a) (hom⇩o b)) (hom⇩a a b ⊗ hom⇩o a)"
using y a b c by fastforce
ultimately show ?thesis
using y a b c comp_assoc
C.interchange
[of "exp (Hom b y) (Hom c y)" "hom⇩a b c"
"eval (Hom a y) (Hom b y)" "hom⇩a a b ⊗ hom⇩o a"]
by metis
qed
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(exp (hom⇩o b) (hom⇩o c) ⋅ hom⇩a b c ⊗ Op.Comp⇩o⇩p y a b) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c C.Uncurry_Curry Op.Comp_in_hom by auto
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(hom⇩a b c ⊗ Op.Comp⇩o⇩p y a b) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c
by (simp add: comp_ide_arr Op.Comp_in_hom)
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
(hom⇩a b c ⋅ Hom c b ⊗ hom⇩o b ⋅ Op.Comp⇩o⇩p y a b) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c *
by (metis Op.Comp_in_hom comp_cod_arr comp_arr_dom in_homE)
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(eval (hom⇩o b) (hom⇩o c) ⋅
((hom⇩a b c ⊗ hom⇩o b) ⋅ (Hom c b ⊗ Op.Comp⇩o⇩p y a b)) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c *
C.interchange [of "hom⇩a b c" "Hom c b" "hom⇩o b" "Op.Comp⇩o⇩p y a b"]
by (metis Op.Comp_in_hom ide_Hom ide_char in_homE seqI)
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(Uncurry[hom⇩o b, hom⇩o c] (hom⇩a b c) ⋅
(Hom c b ⊗ Op.Comp⇩o⇩p y a b) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using comp_assoc by simp
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(Op.Comp⇩o⇩p y b c ⋅
(Hom c b ⊗ Op.Comp⇩o⇩p y a b) ⋅
𝖺[Hom c b, Hom b a, hom⇩o a])"
using y a b c C.Uncurry_Curry
by (simp add: Op.Comp_in_hom)
also have "... = Curry[Hom c b ⊗ Hom b a, hom⇩o a, hom⇩o c]
(Op.Comp⇩o⇩p y a c ⋅ (Op.Comp⇩o⇩p a b c ⊗ hom⇩o a))"
using y a b c Op.Comp_assoc [of y a b c] by simp
also have "... = hom⇩a a c ⋅ Op.Comp⇩o⇩p a b c"
using y a b c C.comp_Curry_arr [of "Hom a y" "Op.Comp⇩o⇩p a b c"]
ide_Hom Op.Comp_in_hom
by fastforce
finally
show "C.Comp (hom⇩o a) (hom⇩o b) (hom⇩o c) ⋅ (hom⇩a b c ⊗ hom⇩a a b) =
hom⇩a a c ⋅ Op.Comp⇩o⇩p a b c"
by blast
qed
qed
lemma is_enriched_functor:
shows "enriched_functor C T α ι
Obj Op.Hom⇩o⇩p Id Op.Comp⇩o⇩p
(Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a"
..
sublocale C⇩0: underlying_category C T α ι ‹Collect ide› exp C.Id C.Comp ..
sublocale Op⇩0: underlying_category C T α ι Obj Op.Hom⇩o⇩p Id Op.Comp⇩o⇩p ..
sublocale UF: underlying_functor C T α ι
Obj Op.Hom⇩o⇩p Id Op.Comp⇩o⇩p
‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a
..
text‹
The following is Kelly's formula (1.32) for ‹Hom⇧← f y : Hom b y → Hom a y›.
›
lemma Kelly_1_32:
assumes "a ∈ Obj" and "b ∈ Obj" and "«f : ℐ → Hom a b»"
shows "C.frmUC (UF.map⇩0 (Op⇩0.MkArr b a f)) =
Comp a b y ⋅ (Hom b y ⊗ f) ⋅ 𝗋⇧-⇧1[hom⇩o b]"
proof -
have "C.frmUC (UF.map⇩0 (Op⇩0.MkArr b a f)) =
(Curry[Hom a b, hom⇩o b, hom⇩o a] (Op.Comp⇩o⇩p y b a) ⋅ f)
⇧↓[hom⇩o b, hom⇩o a]"
proof -
have "C.UC.arr (Op⇩0.MkArr (Hom b y) (Hom a y)
(Curry[Hom a b, Hom b y, Hom a y] (Op.Comp⇩o⇩p y b a) ⋅ f))"
using assms y ide_Hom
apply auto[1]
using C.UC.arr_MkArr
[of "Hom b y" "Hom a y"
"Curry[Hom a b, hom⇩o b, hom⇩o a] (Op.Comp⇩o⇩p y b a) ⋅ f"]
by blast
thus ?thesis
using assms UF.map⇩0_def Op⇩0.arr_MkArr UF.preserves_arr by auto
qed
also have 1: "... = Curry[ℐ, hom⇩o b, hom⇩o a]
(Op.Comp⇩o⇩p y b a ⋅ (f ⊗ hom⇩o b)) ⇧↓[hom⇩o b, hom⇩o a]"
proof -
have "Curry[Hom a b, Hom b y, Hom a y] (Op.Comp⇩o⇩p y b a) ⋅ f =
Curry[ℐ, Hom b y, Hom a y] (Op.Comp⇩o⇩p y b a ⋅ (f ⊗ Hom b y))"
using assms y C.comp_Curry_arr by blast
thus ?thesis by simp
qed
also have "... = (Op.Comp⇩o⇩p y b a ⋅ (f ⊗ Hom b y)) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
proof -
have "arr (Curry[ℐ, Hom b y, Hom a y]
(Op.Comp⇩o⇩p y b a ⋅ (f ⊗ Hom b y)))"
using assms y ide_Hom C.ide_unity
by (metis 1 C.Curry_simps(1-3) C.DN_def C.DN_simps(1) cod_comp
dom_comp in_homE not_arr_null seqI Op.Comp_in_hom)
thus ?thesis
unfolding C.DN_def
using assms y ide_Hom C.ide_unity
C.Uncurry_Curry
[of ℐ "Hom b y" "Hom a y" "Op.Comp⇩o⇩p y b a ⋅ (f ⊗ Hom b y)"]
apply auto[1]
by fastforce
qed
also have "... =
Comp a b y ⋅ (𝗌[Hom a b, Hom b y] ⋅ (f ⊗ Hom b y)) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using comp_assoc by simp
also have "... = Comp a b y ⋅ ((Hom b y ⊗ f) ⋅ 𝗌[ℐ, Hom b y]) ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using assms y C.sym_naturality [of f "Hom b y"] by auto
also have "... = Comp a b y ⋅ (Hom b y ⊗ f) ⋅ 𝗌[ℐ, Hom b y] ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using comp_assoc by simp
also have "... = Comp a b y ⋅ (Hom b y ⊗ f) ⋅ 𝗋⇧-⇧1[hom⇩o b]"
proof -
have "𝗋⇧-⇧1[hom⇩o b] = inv (𝗅[hom⇩o b] ⋅ 𝗌[Hom b y, ℐ])"
using assms y unitor_coherence by simp
also have "... = 𝗌[ℐ, Hom b y] ⋅ 𝗅⇧-⇧1[hom⇩o b]"
using assms y
by (metis C.ide_unity inv_comp_left(1) inverse_unique
C.iso_lunit C.iso_runit C.sym_inverse C.unitor_coherence
Op.ide_Hom)
finally show ?thesis by simp
qed
finally show ?thesis by blast
qed
abbreviation map⇩0
where "map⇩0 a b f ≡ Comp a b y ⋅ (Hom b y ⊗ f) ⋅ 𝗋⇧-⇧1[hom⇩o b]"
end
context elementary_closed_symmetric_monoidal_category
begin
interpretation enriched_category C T α ι ‹Collect ide› exp Id Comp
using is_enriched_in_itself by simp
interpretation self_enriched_category C T α ι exp eval Curry ..
sublocale Op: opposite_enriched_category C T α ι σ ‹Collect ide› exp Id Comp
..
lemma cnt_Exp_DN:
assumes "«f : ℐ → exp a b»"
and "ide a" and "ide b" and "ide y"
shows "Exp⇧← (f ⇧↓[a, b]) y =
(Curry[exp a b, exp b y, exp a y] (Op.Comp⇩o⇩p y b a) ⋅ f)
⇧↓[exp b y, exp a y]"
proof -
have "(Curry[exp a b, exp b y, exp a y] (Op.Comp⇩o⇩p y b a) ⋅ f)
⇧↓[exp b y, exp a y] =
Uncurry[exp b y, exp a y]
(Curry[ℐ, exp b y, exp a y] (Op.Comp⇩o⇩p y b a ⋅ (f ⊗ exp b y))) ⋅
𝗅⇧-⇧1[exp b y]"
using assms Op.Comp_in_hom DN_def comp_Curry_arr by force
also have "... = (Op.Comp⇩o⇩p y b a ⋅ (f ⊗ exp b y)) ⋅ 𝗅⇧-⇧1[exp b y]"
using assms Uncurry_Curry by auto
also have "... = Comp a b y ⋅ (𝗌[exp a b, exp b y] ⋅ (f ⊗ exp b y)) ⋅
𝗅⇧-⇧1[exp b y]"
using comp_assoc by simp
also have "... = Comp a b y ⋅ ((exp b y ⊗ f) ⋅ 𝗌[ℐ, exp b y]) ⋅ 𝗅⇧-⇧1[exp b y]"
using assms sym_naturality [of f "exp b y"] by auto
also have "... = Comp a b y ⋅ (exp b y ⊗ f) ⋅ 𝗌[ℐ, exp b y] ⋅ 𝗅⇧-⇧1[exp b y]"
using comp_assoc by simp
also have "... = Comp a b y ⋅ (exp b y ⊗ f) ⋅ 𝗋⇧-⇧1[exp b y]"
proof -
have "𝗋⇧-⇧1[exp b y] = inv (𝗅[exp b y] ⋅ 𝗌[exp b y, ℐ])"
using assms unitor_coherence by auto
also have "... = inv 𝗌[exp b y, ℐ] ⋅ 𝗅⇧-⇧1[exp b y]"
using assms inv_comp by simp
also have "... = 𝗌[ℐ, exp b y] ⋅ 𝗅⇧-⇧1[exp b y]"
using assms
by (metis ide_exp ide_unity inverse_unique sym_inverse)
finally show ?thesis by simp
qed
also have "... = Curry[exp b y ⊗ exp a b, a, y]
(eval b y ⋅ (exp b y ⊗ eval a b) ⋅ 𝖺[exp b y, exp a b, a]) ⋅
(exp b y ⊗ f) ⋅ 𝗋⇧-⇧1[exp b y]"
unfolding Comp_def by simp
also have "... = Curry[exp b y, a, y]
((eval b y ⋅ (exp b y ⊗ eval a b) ⋅ 𝖺[exp b y, exp a b, a]) ⋅
((exp b y ⊗ f) ⋅ 𝗋⇧-⇧1[exp b y] ⊗ a))"
using assms
comp_Curry_arr
[of a "(exp b y ⊗ f) ⋅ 𝗋⇧-⇧1[exp b y]" "exp b y" "exp b y ⊗ exp a b"
"eval b y ⋅ (exp b y ⊗ eval a b) ⋅ 𝖺[exp b y, exp a b, a]" y]
by auto
also have "... = Curry[exp b y, a, y]
((eval b y ⋅ (exp b y ⊗ eval a b) ⋅ 𝖺[exp b y, exp a b, a]) ⋅
(((exp b y ⊗ f) ⊗ a) ⋅ (𝗋⇧-⇧1[exp b y] ⊗ a)))"
using assms comp_arr_dom comp_cod_arr interchange by auto
also have "... = Curry[exp b y, a, y]
(eval b y ⋅ (exp b y ⊗ eval a b) ⋅
(𝖺[exp b y, exp a b, a] ⋅ ((exp b y ⊗ f) ⊗ a)) ⋅
(𝗋⇧-⇧1[exp b y] ⊗ a))"
using comp_assoc by simp
also have "... = Curry[exp b y, a, y]
(eval b y ⋅ (exp b y ⊗ eval a b) ⋅
((exp b y ⊗ f ⊗ a) ⋅ 𝖺[exp b y, ℐ, a]) ⋅
(𝗋⇧-⇧1[exp b y] ⊗ a))"
using assms assoc_naturality [of "exp b y" f a] by auto
also have "... = Curry[exp b y, a, y]
(eval b y ⋅
((exp b y ⊗ eval a b) ⋅ (exp b y ⊗ f ⊗ a)) ⋅
𝖺[exp b y, ℐ, a] ⋅ (𝗋⇧-⇧1[exp b y] ⊗ a))"
using comp_assoc by simp
also have "... = Curry[exp b y, a, y]
(eval b y ⋅ (exp b y ⊗ Uncurry[a, b] f) ⋅
𝖺[exp b y, ℐ, a] ⋅ (𝗋⇧-⇧1[exp b y] ⊗ a))"
using assms comp_arr_dom comp_cod_arr interchange by simp
also have "... = Curry[exp b y, a, y]
(eval b y ⋅ (exp b y ⊗ Uncurry[a, b] f) ⋅ (exp b y ⊗ 𝗅⇧-⇧1[a]))"
proof -
have "exp b y ⊗ 𝗅⇧-⇧1[a] = inv ((𝗋[exp b y] ⊗ a) ⋅ 𝖺⇧-⇧1[exp b y, ℐ, a])"
using assms triangle' inv_inv iso_inv_iso
by (metis ide_exp ide_is_iso inv_ide inv_tensor iso_lunit)
also have "... = 𝖺[exp b y, ℐ, a] ⋅ (𝗋⇧-⇧1[exp b y] ⊗ a)"
using assms inv_comp by simp
finally show ?thesis by simp
qed
also have "... = Curry[exp b y, a, y]
(eval b y ⋅ (exp b y ⊗ Uncurry[a, b] f ⋅ 𝗅⇧-⇧1[a]))"
using assms comp_arr_dom comp_cod_arr interchange by fastforce
also have "... = Exp⇧← (f ⇧↓[a, b]) y"
using assms DN_def by auto
finally show ?thesis by simp
qed
end
section "Enriched Yoneda Lemma"
text‹
In this section we prove the (weak) Yoneda lemma for enriched categories,
as in Kelly, Section 1.9. The weakness is due to the fact that the lemma
asserts only a bijection between sets, rather than an isomorphism of objects of
the underlying base category.
›
subsection "Preliminaries"
text‹
The following gives conditions under which ‹τ› defined as ‹τ x = (𝒯 x)⇧↑›
yields an enriched natural transformation between enriched functors ‹F› and ‹G›
to the self-enriched base category.
›
context elementary_closed_monoidal_category
begin
lemma transformation_lam_UP:
assumes "enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A (Collect ide) exp Id Comp F⇩o F⇩a"
assumes "enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A (Collect ide) exp Id Comp G⇩o G⇩a"
and "⋀x. x ∉ Obj⇩A ⟹ 𝒯 x = null"
and "⋀x. x ∈ Obj⇩A ⟹ «𝒯 x : F⇩o x → G⇩o x»"
and "⋀a b. ⟦a ∈ Obj⇩A; b ∈ Obj⇩A⟧ ⟹
𝒯 b ⋅ Uncurry[F⇩o a, F⇩o b] (F⇩a a b) =
eval (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ 𝒯 a)"
shows "enriched_natural_transformation C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A (Collect ide) exp Id Comp
F⇩o F⇩a G⇩o G⇩a (λx. (𝒯 x)⇧↑)"
proof -
interpret F: enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A ‹Collect ide› exp Id Comp F⇩o F⇩a
using assms(1) by blast
interpret G: enriched_functor C T α ι
Obj⇩A Hom⇩A Id⇩A Comp⇩A ‹Collect ide› exp Id Comp G⇩o G⇩a
using assms(2) by blast
show ?thesis
proof
show "⋀x. x ∉ Obj⇩A ⟹ (𝒯 x)⇧↑ = null"
unfolding UP_def
using assms(3) by auto
show "⋀x. x ∈ Obj⇩A ⟹ «(𝒯 x)⇧↑ : ℐ → exp (F⇩o x) (G⇩o x)»"
unfolding UP_def
using assms(4)
apply auto[1]
by force
fix a b
assume a: "a ∈ Obj⇩A" and b: "b ∈ Obj⇩A"
have 1: "«((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (F⇩o b) (G⇩o b) ⊗ exp (F⇩o a) (F⇩o b)»"
using assms(4) [of b] a b UP_DN F.preserves_Hom
apply (intro comp_in_homI tensor_in_homI)
apply auto[5]
by fastforce
have 2: "«(G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (G⇩o a) (G⇩o b) ⊗ exp (F⇩o a) (G⇩o a)»"
using assms(4) [of a] a b UP_DN F.preserves_Obj G.preserves_Hom
apply (intro comp_in_homI tensor_in_homI)
apply auto[5]
by fastforce
have 3: "«Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅ ((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (F⇩o a) (G⇩o b)»"
using a b 1 F.preserves_Obj G.preserves_Obj by blast
have 4: "«Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (F⇩o a) (G⇩o b)»"
using a b 2 F.preserves_Obj G.preserves_Obj by blast
have "Uncurry[F⇩o a, G⇩o b]
(Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅
((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]) =
Uncurry[F⇩o a, G⇩o b]
(Curry[exp (F⇩o b) (G⇩o b) ⊗ exp (F⇩o a) (F⇩o b), F⇩o a, G⇩o b]
(eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
𝖺[exp (F⇩o b) (G⇩o b), exp (F⇩o a) (F⇩o b), F⇩o a]) ⋅
((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b])"
using a b Comp_def comp_assoc by auto
also have "... =
Uncurry[F⇩o a, G⇩o b]
(Curry[Hom⇩A a b, F⇩o a, G⇩o b]
((eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
𝖺[exp (F⇩o b) (G⇩o b), exp (F⇩o a) (F⇩o b), F⇩o a]) ⋅
(((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)))"
using a b 1 F.preserves_Obj G.preserves_Obj comp_Curry_arr by auto
also have "... =
(eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
𝖺[exp (F⇩o b) (G⇩o b), exp (F⇩o a) (F⇩o b), F⇩o a]) ⋅
(((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using a b 1 F.preserves_Obj G.preserves_Obj Uncurry_Curry by auto
also have "... =
(eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
𝖺[exp (F⇩o b) (G⇩o b), exp (F⇩o a) (F⇩o b), F⇩o a]) ⋅
((((𝒯 b)⇧↑ ⊗ F⇩a a b) ⊗ F⇩o a) ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a))"
proof -
have "seq ((𝒯 b)⇧↑ ⊗ F⇩a a b) 𝗅⇧-⇧1[Hom⇩A a b]"
using assms(4) a b 1 F.preserves_Hom [of a b] UP_DN
apply (intro seqI)
apply auto[2]
by (metis F.A.ide_Hom arrI cod_inv dom_lunit iso_lunit seqE)
thus ?thesis
using assms(3) a b F.preserves_Obj F.preserves_Hom interchange
by simp
qed
also have "... =
eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
(𝖺[exp (F⇩o b) (G⇩o b), exp (F⇩o a) (F⇩o b), F⇩o a] ⋅
(((𝒯 b)⇧↑ ⊗ F⇩a a b) ⊗ F⇩o a)) ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... =
eval (F⇩o b) (G⇩o b) ⋅
(exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
(((𝒯 b)⇧↑ ⊗ F⇩a a b ⊗ F⇩o a) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a]) ⋅
(𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) a b F.preserves_Obj F.preserves_Hom
assoc_naturality [of "(𝒯 b)⇧↑" "F⇩a a b" "F⇩o a"]
by force
also have "... =
eval (F⇩o b) (G⇩o b) ⋅
((exp (F⇩o b) (G⇩o b) ⊗ eval (F⇩o a) (F⇩o b)) ⋅
((𝒯 b)⇧↑ ⊗ F⇩a a b ⊗ F⇩o a)) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... =
eval (F⇩o b) (G⇩o b) ⋅
((𝒯 b)⇧↑ ⊗ Uncurry[F⇩o a, F⇩o b] (F⇩a a b)) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
proof -
have "seq (exp (F⇩o b) (G⇩o b)) (UP (𝒯 b))"
using assms(4) b F.preserves_Obj G.preserves_Obj by fastforce
moreover have "seq (eval (F⇩o a) (F⇩o b)) (F⇩a a b ⊗ F⇩o a)"
using a b F.preserves_Obj F.preserves_Hom by force
ultimately show ?thesis
using assms(4) [of b] a b UP_DN(1) comp_cod_arr interchange by auto
qed
also have "... =
eval (F⇩o b) (G⇩o b) ⋅
(((𝒯 b)⇧↑ ⊗ F⇩o b) ⋅ (ℐ ⊗ Uncurry[F⇩o a, F⇩o b] (F⇩a a b))) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) [of b] a b F.preserves_Obj F.preserves_Hom [of a b]
comp_arr_dom comp_cod_arr [of "Uncurry[F⇩o a, F⇩o b] (F⇩a a b)"]
interchange [of "(𝒯 b)⇧↑" ℐ "F⇩o b" "Uncurry[F⇩o a, F⇩o b] (F⇩a a b)"]
by auto
also have "... =
Uncurry[F⇩o b, G⇩o b] ((𝒯 b)⇧↑) ⋅
(ℐ ⊗ Uncurry[F⇩o a, F⇩o b] (F⇩a a b)) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... = (𝒯 b ⋅ 𝗅[F⇩o b]) ⋅
(ℐ ⊗ Uncurry[F⇩o a, F⇩o b] (F⇩a a b)) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
proof -
have "Uncurry[F⇩o b, G⇩o b] ((𝒯 b)⇧↑) = 𝒯 b ⋅ 𝗅[F⇩o b]"
unfolding UP_def
using assms(4) a b Uncurry_Curry
apply simp
by (metis F.preserves_Obj arr_lunit cod_lunit comp_in_homI' dom_lunit
ide_cod ide_unity in_homE mem_Collect_eq)
thus ?thesis by simp
qed
also have "... = 𝒯 b ⋅ (𝗅[F⇩o b] ⋅ (ℐ ⊗ Uncurry[F⇩o a, F⇩o b] (F⇩a a b))) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... = 𝒯 b ⋅ (Uncurry[F⇩o a, F⇩o b] (F⇩a a b) ⋅ 𝗅[Hom⇩A a b ⊗ F⇩o a]) ⋅
𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using a b lunit_naturality [of "Uncurry[F⇩o a, F⇩o b] (F⇩a a b)"]
F.preserves_Obj F.preserves_Hom [of a b]
by auto
also have "... = 𝒯 b ⋅ Uncurry[F⇩o a, F⇩o b] (F⇩a a b) ⋅
𝗅[Hom⇩A a b ⊗ F⇩o a] ⋅ 𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅
(𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... = 𝒯 b ⋅ Uncurry[F⇩o a, F⇩o b] (F⇩a a b)"
proof -
have "𝗅[Hom⇩A a b ⊗ F⇩o a] ⋅ 𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅
(𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a) =
Hom⇩A a b ⊗ F⇩o a"
proof -
have "𝗅[Hom⇩A a b ⊗ F⇩o a] ⋅ 𝖺[ℐ, Hom⇩A a b, F⇩o a] ⋅
(𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a) =
(𝗅[Hom⇩A a b] ⊗ F⇩o a) ⋅ (𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using a b lunit_tensor' [of "Hom⇩A a b" "F⇩o a"]
by (metis F.A.ide_Hom F.preserves_Obj comp_assoc mem_Collect_eq)
also have "... = 𝗅[Hom⇩A a b] ⋅ 𝗅⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a ⋅ F⇩o a"
using a b interchange F.preserves_Obj by force
also have "... = Hom⇩A a b ⊗ F⇩o a"
using a b F.preserves_Obj by auto
finally show ?thesis by blast
qed
thus ?thesis
using a b F.preserves_Obj F.preserves_Hom [of a b] comp_arr_dom
by auto
qed
finally have LHS: "Uncurry[F⇩o a, G⇩o b]
(Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅ ((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅
𝗅⇧-⇧1[Hom⇩A a b]) =
𝒯 b ⋅ Uncurry[F⇩o a, F⇩o b] (F⇩a a b)"
by blast
have "Uncurry[F⇩o a, G⇩o b] (Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅
(G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]) =
Uncurry[F⇩o a, G⇩o b]
(Curry[exp (G⇩o a) (G⇩o b) ⊗ exp (F⇩o a) (G⇩o a), F⇩o a, G⇩o b]
(eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
𝖺[exp (G⇩o a) (G⇩o b), exp (F⇩o a) (G⇩o a), F⇩o a]) ⋅
(G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b])"
using a b Comp_def comp_assoc by auto
also have "... =
Uncurry[F⇩o a, G⇩o b]
(Curry[Hom⇩A a b, F⇩o a, G⇩o b]
((eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
𝖺[exp (G⇩o a) (G⇩o b), exp (F⇩o a) (G⇩o a), F⇩o a]) ⋅
((G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)))"
using assms(3) a b 2 F.preserves_Obj G.preserves_Obj comp_Curry_arr
by auto
also have "... =
(eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
𝖺[exp (G⇩o a) (G⇩o b), exp (F⇩o a) (G⇩o a), F⇩o a]) ⋅
((G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(3) a b 2 F.preserves_Obj G.preserves_Obj Uncurry_Curry
by auto
also have "... =
(eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
𝖺[exp (G⇩o a) (G⇩o b), exp (F⇩o a) (G⇩o a), F⇩o a]) ⋅
(((G⇩a a b ⊗ (𝒯 a)⇧↑) ⊗ F⇩o a) ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a))"
using assms(4) a b F.preserves_Obj G.preserves_Hom
interchange [of "G⇩a a b ⊗ (𝒯 a)⇧↑" "𝗋⇧-⇧1[Hom⇩A a b]" "F⇩o a" "F⇩o a"]
by fastforce
also have "... =
eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
(𝖺[exp (G⇩o a) (G⇩o b), exp (F⇩o a) (G⇩o a), F⇩o a] ⋅
((G⇩a a b ⊗ (𝒯 a)⇧↑) ⊗ F⇩o a)) ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... =
eval (G⇩o a) (G⇩o b) ⋅
(exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
((G⇩a a b ⊗ (𝒯 a)⇧↑ ⊗ F⇩o a) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a]) ⋅
(𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) a b F.preserves_Obj G.preserves_Hom
assoc_naturality [of "G⇩a a b" "(𝒯 a)⇧↑" "F⇩o a"]
by fastforce
also have "... =
eval (G⇩o a) (G⇩o b) ⋅
((exp (G⇩o a) (G⇩o b) ⊗ eval (F⇩o a) (G⇩o a)) ⋅
(G⇩a a b ⊗ (𝒯 a)⇧↑ ⊗ F⇩o a)) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... =
eval (G⇩o a) (G⇩o b) ⋅
(G⇩a a b ⊗ Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑)) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) a b F.preserves_Obj G.preserves_Obj
G.preserves_Hom [of a b] comp_cod_arr interchange
by fastforce
also have "... =
eval (G⇩o a) (G⇩o b) ⋅
((G⇩a a b ⊗ G⇩o a) ⋅ (Hom⇩A a b ⊗ Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑))) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
proof -
have "seq (G⇩o a) (Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑))"
using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj by auto
moreover have "G⇩o a ⋅ Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑) =
Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑)"
using a b F.preserves_Obj G.preserves_Obj calculation(1)
comp_ide_arr
by blast
ultimately show ?thesis
using assms(3) a b G.preserves_Hom [of a b] interchange
comp_arr_dom
by auto
qed
also have "... =
Uncurry[G⇩o a, G⇩o b] (G⇩a a b) ⋅
(Hom⇩A a b ⊗ Uncurry[F⇩o a, G⇩o a] ((𝒯 a)⇧↑)) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... =
Uncurry[G⇩o a, G⇩o b] (G⇩a a b) ⋅
(Hom⇩A a b ⊗ 𝒯 a ⋅ 𝗅[F⇩o a]) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj UP_def
Uncurry_Curry
by auto
also have "... =
Uncurry[G⇩o a, G⇩o b] (G⇩a a b) ⋅
((Hom⇩A a b ⊗ 𝒯 a) ⋅ (Hom⇩A a b ⊗ 𝗅[F⇩o a])) ⋅
𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj interchange
by auto
also have "... =
Uncurry[G⇩o a, G⇩o b] (G⇩a a b) ⋅ (Hom⇩A a b ⊗ 𝒯 a) ⋅
(Hom⇩A a b ⊗ 𝗅[F⇩o a]) ⋅ 𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅
(𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using comp_assoc by simp
also have "... = Uncurry[G⇩o a, G⇩o b] (G⇩a a b) ⋅ (Hom⇩A a b ⊗ 𝒯 a)"
proof -
have "(Hom⇩A a b ⊗ 𝗅[F⇩o a]) ⋅ 𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅
(𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a) =
Hom⇩A a b ⊗ F⇩o a"
proof -
have "(Hom⇩A a b ⊗ 𝗅[F⇩o a]) ⋅ 𝖺[Hom⇩A a b, ℐ, F⇩o a] ⋅
(𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a) =
(𝗋[Hom⇩A a b] ⊗ F⇩o a) ⋅ (𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a)"
using a b triangle [of "Hom⇩A a b" "F⇩o a"]
by (metis F.A.ide_Hom F.preserves_Obj comp_assoc mem_Collect_eq)
also have "... = 𝗋[Hom⇩A a b] ⋅ 𝗋⇧-⇧1[Hom⇩A a b] ⊗ F⇩o a ⋅ F⇩o a"
using a b interchange F.preserves_Obj by force
also have "... = Hom⇩A a b ⊗ F⇩o a"
using a b F.preserves_Obj by auto
finally show ?thesis by blast
qed
thus ?thesis
using assms(4) [of a] a b comp_arr_dom by auto
qed
also have "... = eval (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ G⇩o a) ⋅ (Hom⇩A a b ⊗ 𝒯 a)"
using comp_assoc by auto
also have "... = eval (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ 𝒯 a)"
using assms(4) a b G.preserves_Hom comp_arr_dom comp_cod_arr
interchange
by (metis in_homE)
finally have RHS: "Uncurry[F⇩o a, G⇩o b]
(Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅
𝗋⇧-⇧1[Hom⇩A a b]) =
eval (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ 𝒯 a)"
by blast
have "Uncurry[F⇩o a, G⇩o b]
(Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅ ((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]) =
Uncurry[F⇩o a, G⇩o b]
(Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b])"
using a b assms(5) LHS RHS by simp
moreover have "«Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅
((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (F⇩o a) (G⇩o b)»"
using assms(4) a b 1 F.preserves_Obj G.preserves_Obj
F.preserves_Hom G.preserves_Hom
apply (intro comp_in_homI' seqI)
apply auto[1]
by fastforce+
moreover have "«Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅
(G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]
: Hom⇩A a b → exp (F⇩o a) (G⇩o b)»"
using assms(4) a b 2 UP_DN(1) F.preserves_Obj G.preserves_Obj
F.preserves_Hom G.preserves_Hom [of a b]
apply (intro comp_in_homI' seqI)
apply auto[7]
by fastforce
ultimately show "Comp (F⇩o a) (F⇩o b) (G⇩o b) ⋅
((𝒯 b)⇧↑ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b] =
Comp (F⇩o a) (G⇩o a) (G⇩o b) ⋅
(G⇩a a b ⊗ (𝒯 a)⇧↑) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]"
using a b Curry_Uncurry F.A.ide_Hom F.preserves_Obj
G.preserves_Obj mem_Collect_eq
by metis
qed
qed
end
text‹
Kelly (1.39) expresses enriched naturality in an alternate form, using the underlying
functors of the covariant and contravariant enriched hom functors.
›
locale Kelly_1_39 =
symmetric_monoidal_category +
elementary_closed_monoidal_category +
enriched_natural_transformation
for a :: 'a
and b :: 'a +
assumes a: "a ∈ Obj⇩A"
and b: "b ∈ Obj⇩A"
begin
interpretation enriched_category C T α ι ‹Collect ide› exp Id Comp
using is_enriched_in_itself by blast
interpretation self_enriched_category C T α ι exp eval Curry
..
sublocale cov_Hom: covariant_Hom C T α ι
exp eval Curry Obj⇩B Hom⇩B Id⇩B Comp⇩B ‹F⇩o a›
using a F.preserves_Obj by unfold_locales
sublocale cnt_Hom: contravariant_Hom C T α ι σ
exp eval Curry Obj⇩B Hom⇩B Id⇩B Comp⇩B ‹G⇩o b›
using b G.preserves_Obj by unfold_locales
lemma Kelly_1_39:
shows "cov_Hom.map⇩0 (F⇩o b) (G⇩o b) (τ b) ⋅ F⇩a a b =
cnt_Hom.map⇩0 (F⇩o a) (G⇩o a) (τ a) ⋅ G⇩a a b"
proof -
have "cov_Hom.map⇩0 (F⇩o b) (G⇩o b) (τ b) ⋅ F⇩a a b =
Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅ (τ b ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]"
proof -
have "cov_Hom.map⇩0 (F⇩o b) (G⇩o b) (τ b) ⋅ F⇩a a b =
Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅
(τ b ⊗ Hom⇩B (F⇩o a) (F⇩o b)) ⋅ 𝗅⇧-⇧1[Hom⇩B (F⇩o a) (F⇩o b)] ⋅ F⇩a a b"
using comp_assoc by simp
also have "... = Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅
(τ b ⊗ Hom⇩B (F⇩o a) (F⇩o b)) ⋅ (ℐ ⊗ F⇩a a b) ⋅ 𝗅⇧-⇧1[Hom⇩A a b]"
using a b lunit'_naturality F.preserves_Hom [of a b] by fastforce
also have "... = Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅
((τ b ⊗ Hom⇩B (F⇩o a) (F⇩o b)) ⋅ (ℐ ⊗ F⇩a a b)) ⋅
𝗅⇧-⇧1[Hom⇩A a b]"
using comp_assoc by simp
also have "... = Comp⇩B (F⇩o a) (F⇩o b) (G⇩o b) ⋅ (τ b ⊗ F⇩a a b) ⋅
𝗅⇧-⇧1[Hom⇩A a b]"
using a b component_in_hom [of b] F.preserves_Hom [of a b]
comp_arr_dom comp_cod_arr [of "F⇩a a b" "Hom⇩B (F⇩o a) (F⇩o b)"]
interchange
by fastforce
finally show ?thesis by blast
qed
moreover have "cnt_Hom.map⇩0 (F⇩o a) (G⇩o a) (τ a) ⋅ G⇩a a b =
Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ τ a) ⋅ 𝗋⇧-⇧1[Hom⇩A a b]"
proof -
have "cnt_Hom.map⇩0 (F⇩o a) (G⇩o a) (τ a) ⋅ G⇩a a b =
Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (Hom⇩B (G⇩o a) (G⇩o b) ⊗ τ a) ⋅
𝗋⇧-⇧1[Hom⇩B (G⇩o a) (G⇩o b)] ⋅ G⇩a a b"
using comp_assoc by simp
also have "... = Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅
(Hom⇩B (G⇩o a) (G⇩o b) ⊗ τ a) ⋅ (G⇩a a b ⊗ ℐ) ⋅
𝗋⇧-⇧1[Hom⇩A a b]"
using a b runit'_naturality G.preserves_Hom [of a b] by fastforce
also have "... = Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅
((Hom⇩B (G⇩o a) (G⇩o b) ⊗ τ a) ⋅ (G⇩a a b ⊗ ℐ)) ⋅
𝗋⇧-⇧1[Hom⇩A a b]"
using comp_assoc by simp
also have "... = Comp⇩B (F⇩o a) (G⇩o a) (G⇩o b) ⋅ (G⇩a a b ⊗ τ a) ⋅
𝗋⇧-⇧1[Hom⇩A a b]"
using a b interchange component_in_hom [of a] G.preserves_Hom [of a b]
comp_arr_dom comp_cod_arr [of "G⇩a a b" "Hom⇩B (G⇩o a) (G⇩o b)"]
by fastforce
finally show ?thesis by blast
qed
ultimately show ?thesis
using a b naturality by simp
qed
end
subsection "Covariant Case"
locale covariant_yoneda_lemma =
symmetric_monoidal_category +
C: closed_symmetric_monoidal_category +
covariant_Hom +
F: enriched_functor C T α ι Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
begin
interpretation C: elementary_closed_symmetric_monoidal_category C T α ι σ exp eval Curry ..
interpretation C: self_enriched_category C T α ι exp eval Curry ..
text‹
Every element ‹e : ℐ → F⇩o x› of ‹F⇩o x› determines an enriched natural transformation
‹τ⇩e: hom x - → F›. The formula here is Kelly (1.47): ‹τ⇩e y: hom x y → F y›
is obtained as the composite:
\[
‹hom x y› \labarrow{‹F⇩a x y›} ‹exp (F x) (F y)›
\labarrow{‹Exp⇧← e (F y)›} ‹exp ℐ (F y)› \labarrow{} ‹F y›
\]
where the third component is a canonical isomorphism.
This basically amounts to evaluating ‹F⇩a x y› on element ‹e› of ‹F⇩o x› to obtain
an element of ‹F⇩o y›.
Note that the above composite gives an arrow ‹τ⇩e y: hom x y → F y›, whereas the
definition of enriched natural transformation formally requires
‹τ⇩e y: ℐ → exp (hom x y) (F y)›.
So we need to transform the composite to achieve that.
›
abbreviation generated_transformation
where "generated_transformation e ≡
λy. (eval ℐ (F⇩o y) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o y)] ⋅ Exp⇧← e (F⇩o y) ⋅ F⇩a x y)⇧↑"
lemma enriched_natural_transformation_generated_transformation:
assumes "«e : ℐ → F⇩o x»"
shows "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a (generated_transformation e)"
proof (intro C.transformation_lam_UP)
show "⋀y. y ∉ Obj ⟹
eval ℐ (F⇩o y) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o y)] ⋅ Exp⇧← e (F⇩o y) ⋅ F⇩a x y = null"
by (simp add: F.extensionality)
show "enriched_functor (⋅) T α ι Obj Hom Id Comp
(Collect ide) exp C.Id C.Comp hom⇩o hom⇩a"
..
show "enriched_functor (⋅) T α ι Obj Hom Id Comp
(Collect ide) exp C.Id C.Comp F⇩o F⇩a"
..
show *: "⋀y. y ∈ Obj ⟹
«eval ℐ (F⇩o y) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o y)] ⋅ Exp⇧← e (F⇩o y) ⋅ F⇩a x y
: hom⇩o y → F⇩o y»"
using assms x F.preserves_Obj F.preserves_Hom
apply (intro in_homI seqI)
apply auto[6]
by fastforce+
show "⋀a b. ⟦a ∈ Obj; b ∈ Obj⟧ ⟹
(eval ℐ (F⇩o b) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅
Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅
Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b) =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← e (F⇩o a) ⋅ F⇩a x a)"
proof -
fix a b
assume a: "a ∈ Obj" and b: "b ∈ Obj"
have "(eval ℐ (F⇩o b) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅
Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅ Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b) =
eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⋅ Comp x a b ⊗ e) ⋅
𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
proof -
have "(eval ℐ (F⇩o b) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅
Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅ Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b) =
eval ℐ (F⇩o b) ⋅
(𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅ Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅
Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b)"
using comp_assoc by simp
also have "... = eval ℐ (F⇩o b) ⋅
(𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅ Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅
Comp x a b"
using a b x C.Uncurry_Curry [of _ "hom⇩o a" "hom⇩o b"] Comp_in_hom
by auto
also have "... = eval ℐ (F⇩o b) ⋅
((Exp⇧← e (F⇩o b) ⋅ F⇩a x b ⊗ ℐ) ⋅
𝗋⇧-⇧1[hom⇩o b]) ⋅ Comp x a b"
proof -
have "«Exp⇧← e (F⇩o b) ⋅ F⇩a x b : hom⇩o b → exp ℐ (F⇩o b)»"
using assms a b x F.preserves_Obj F.preserves_Hom [of x b] by force
thus ?thesis
using a b F.preserves_Obj F.preserves_Hom
runit'_naturality [of "Exp⇧← e (F⇩o b) ⋅ F⇩a x b"]
by auto
qed
also have "... = eval ℐ (F⇩o b) ⋅
(((Exp⇧← e (F⇩o b) ⊗ ℐ) ⋅ (F⇩a x b ⊗ ℐ)) ⋅
𝗋⇧-⇧1[hom⇩o b]) ⋅
Comp x a b"
using assms a b x F.preserves_Obj F.preserves_Hom [of x b]
interchange [of "Exp⇧← e (F⇩o b)" "F⇩a x b" ℐ ℐ]
by fastforce
also have "... = Uncurry[ℐ, F⇩o b] (Exp⇧← e (F⇩o b)) ⋅ (F⇩a x b ⊗ ℐ) ⋅
𝗋⇧-⇧1[hom⇩o b] ⋅ Comp x a b"
using comp_assoc by simp
also have "... = (eval (F⇩o x) (F⇩o b) ⋅ (exp (F⇩o x) (F⇩o b) ⊗ e)) ⋅
(F⇩a x b ⊗ ℐ) ⋅ 𝗋⇧-⇧1[hom⇩o b] ⋅ Comp x a b"
using assms a b x F.preserves_Obj C.Uncurry_Curry by auto
also have "... = eval (F⇩o x) (F⇩o b) ⋅
((exp (F⇩o x) (F⇩o b) ⊗ e) ⋅ (F⇩a x b ⊗ ℐ)) ⋅
𝗋⇧-⇧1[hom⇩o b] ⋅ Comp x a b"
using comp_assoc by simp
also have "... = eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⊗ e) ⋅ 𝗋⇧-⇧1[hom⇩o b] ⋅
Comp x a b"
using assms a b x F.preserves_Hom [of x b]
comp_cod_arr [of "F⇩a x b" "exp (F⇩o x) (F⇩o b)"] comp_arr_dom
interchange
by fastforce
also have "... = eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⊗ e) ⋅
(Comp x a b ⊗ ℐ) ⋅ 𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
using assms a b x runit'_naturality [of "Comp x a b"]
Comp_in_hom [of x a b]
by auto
also have "... = eval (F⇩o x) (F⇩o b) ⋅ ((F⇩a x b ⊗ e) ⋅ (Comp x a b ⊗ ℐ)) ⋅
𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
using comp_assoc by simp
also have "... = eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⋅ Comp x a b ⊗ e) ⋅
𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
using assms a b x F.preserves_Hom [of x b] Comp_in_hom comp_arr_dom
interchange [of "F⇩a x b" "Comp x a b" e ℐ]
by fastforce
finally show ?thesis by blast
qed
also have "... = eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← e (F⇩o a) ⋅ F⇩a x a)"
proof -
have "eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← e (F⇩o a) ⋅ F⇩a x a) =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅ (𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← e (F⇩o a)) ⋅ F⇩a x a)"
using comp_assoc by simp
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅
((Exp⇧← e (F⇩o a) ⊗ ℐ) ⋅ 𝗋⇧-⇧1[exp (F⇩o x) (F⇩o a)]) ⋅
F⇩a x a)"
using assms a b x F.preserves_Obj F.preserves_Hom
runit'_naturality [of "Exp⇧← e (F⇩o a)"]
by auto
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗
Uncurry[ℐ, F⇩o a] (Exp⇧← e (F⇩o a)) ⋅ 𝗋⇧-⇧1[exp (F⇩o x) (F⇩o a)] ⋅
F⇩a x a)"
using comp_assoc by simp
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗
(eval (F⇩o x) (F⇩o a) ⋅ (exp (F⇩o x) (F⇩o a) ⊗ e)) ⋅
𝗋⇧-⇧1[exp (F⇩o x) (F⇩o a)] ⋅ F⇩a x a)"
using assms a b x F.preserves_Obj C.Uncurry_Curry by auto
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗
(eval (F⇩o x) (F⇩o a) ⋅ (exp (F⇩o x) (F⇩o a) ⊗ e)) ⋅
(F⇩a x a ⊗ ℐ) ⋅ 𝗋⇧-⇧1[hom⇩o a])"
using a b x F.preserves_Hom [of x a] runit'_naturality by fastforce
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗
eval (F⇩o x) (F⇩o a) ⋅ (exp (F⇩o x) (F⇩o a) ⊗ e) ⋅
(F⇩a x a ⊗ ℐ) ⋅ 𝗋⇧-⇧1[hom⇩o a])"
using comp_assoc by simp
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(F⇩a a b ⊗ eval (F⇩o x) (F⇩o a) ⋅ (F⇩a x a ⊗ e) ⋅ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom F.preserves_Hom
comp_arr_dom [of e ℐ]
comp_cod_arr [of "F⇩a x a" "exp (F⇩o x) (F⇩o a)"]
interchange [of "exp (F⇩o x) (F⇩o a)" "F⇩a x a" e ℐ] comp_assoc
by (metis in_homE)
also have "... =
eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a)) ⋅
(F⇩a a b ⊗ (F⇩a x a ⊗ e) ⋅ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom [of x a]
F.preserves_Hom [of a b]
comp_cod_arr [of "F⇩a a b" "exp (F⇩o a) (F⇩o b)"]
interchange
[of "exp (F⇩o a) (F⇩o b)" "F⇩a a b"
"eval (F⇩o x) (F⇩o a)" "(F⇩a x a ⊗ e) ⋅ 𝗋⇧-⇧1[hom⇩o a]"]
by fastforce
also have "... = (eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a))) ⋅
(F⇩a a b ⊗ (F⇩a x a ⊗ e) ⋅ 𝗋⇧-⇧1[hom⇩o a])"
using comp_assoc by simp
also have "... = (eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a))) ⋅
(F⇩a a b ⊗ (F⇩a x a ⊗ e)) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
F.preserves_Hom [of x a] comp_arr_dom [of "F⇩a a b" "Hom a b"]
interchange [of "F⇩a a b" "Hom a b" "F⇩a x a ⊗ e" "𝗋⇧-⇧1[hom⇩o a]"]
by fastforce
also have "... = (eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a))) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ exp (F⇩o x) (F⇩o a) ⊗ F⇩o x) ⋅
(F⇩a a b ⊗ F⇩a x a ⊗ e) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
F.preserves_Hom [of x a]
comp_cod_arr [of "(F⇩a a b ⊗ F⇩a x a ⊗ e) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
"exp (F⇩o a) (F⇩o b) ⊗ exp (F⇩o x) (F⇩o a) ⊗ F⇩o x"]
by fastforce
also have "... = (eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a))) ⋅
(𝖺[exp (F⇩o a) (F⇩o b), exp (F⇩o x) (F⇩o a), F⇩o x] ⋅
𝖺⇧-⇧1[exp (F⇩o a) (F⇩o b), exp (F⇩o x) (F⇩o a), F⇩o x]) ⋅
(F⇩a a b ⊗ (F⇩a x a ⊗ e)) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj comp_assoc_assoc' by simp
also have "... = (eval (F⇩o a) (F⇩o b) ⋅
(exp (F⇩o a) (F⇩o b) ⊗ eval (F⇩o x) (F⇩o a)) ⋅
𝖺[exp (F⇩o a) (F⇩o b), exp (F⇩o x) (F⇩o a), F⇩o x]) ⋅
(𝖺⇧-⇧1[exp (F⇩o a) (F⇩o b), exp (F⇩o x) (F⇩o a), F⇩o x] ⋅
(F⇩a a b ⊗ F⇩a x a ⊗ e)) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using comp_assoc by simp
also have "... = Uncurry[F⇩o x, F⇩o b] (C.Comp (F⇩o x) (F⇩o a) (F⇩o b)) ⋅
(𝖺⇧-⇧1[exp (F⇩o a) (F⇩o b), exp (F⇩o x) (F⇩o a), F⇩o x] ⋅
(F⇩a a b ⊗ F⇩a x a ⊗ e)) ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj C.Uncurry_Curry C.Comp_def
by auto
also have "... = Uncurry[F⇩o x, F⇩o b] (C.Comp (F⇩o x) (F⇩o a) (F⇩o b)) ⋅
(((F⇩a a b ⊗ F⇩a x a) ⊗ e) ⋅ 𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ]) ⋅
(Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Hom [of a b] F.preserves_Hom [of x a]
assoc'_naturality [of "F⇩a a b" "F⇩a x a" e]
by fastforce
also have "... = eval (F⇩o x) (F⇩o b) ⋅
((C.Comp (F⇩o x) (F⇩o a) (F⇩o b) ⊗ F⇩o x) ⋅
((F⇩a a b ⊗ F⇩a x a) ⊗ e)) ⋅
𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ] ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using comp_assoc by simp
also have "... = eval (F⇩o x) (F⇩o b) ⋅
(C.Comp (F⇩o x) (F⇩o a) (F⇩o b) ⋅ (F⇩a a b ⊗ F⇩a x a) ⊗ e) ⋅
𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ] ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
F.preserves_Hom [of x a] comp_cod_arr [of e "F⇩o x"]
interchange
[of "C.Comp (F⇩o x) (F⇩o a) (F⇩o b)" "F⇩a a b ⊗ F⇩a x a" "F⇩o x" e]
by fastforce
also have "... = eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⋅ Comp x a b ⊗ e) ⋅
𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ] ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a])"
using assms a b x F.preserves_Obj F.preserves_Hom F.preserves_Comp
by simp
also have "... = eval (F⇩o x) (F⇩o b) ⋅ (F⇩a x b ⋅ Comp x a b ⊗ e) ⋅
𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
proof -
have "𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ] ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a]) =
𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
proof -
have "𝖺⇧-⇧1[Hom a b, hom⇩o a, ℐ] ⋅ (Hom a b ⊗ 𝗋⇧-⇧1[hom⇩o a]) =
inv ((Hom a b ⊗ 𝗋[hom⇩o a]) ⋅ 𝖺[Hom a b, hom⇩o a, ℐ])"
using assms a b x inv_comp by auto
also have "... = 𝗋⇧-⇧1[Hom a b ⊗ hom⇩o a]"
using assms a b x runit_tensor by auto
finally show ?thesis by blast
qed
thus ?thesis by simp
qed
finally show ?thesis by simp
qed
finally show "(eval ℐ (F⇩o b) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o b)] ⋅ Exp⇧← e (F⇩o b) ⋅ F⇩a x b) ⋅
Uncurry[hom⇩o a, hom⇩o b] (hom⇩a a b) =
eval (F⇩o a) (F⇩o b) ⋅ (F⇩a a b ⊗ eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← e (F⇩o a) ⋅ F⇩a x a)"
by argo
qed
qed
text‹
If ‹τ: hom x - → F› is an enriched natural transformation, then there exists an
element ‹e⇩τ : ℐ → F x› that generates ‹τ› via the preceding formula.
The idea (Kelly 1.46) is to take:
\[
‹e⇩τ› = ‹ℐ›\;\labarrow{‹Id x›}\;‹hom⇩o x›\;\labarrow{‹τ x›}\; ‹F x›
\]
This amounts to the ``evaluation of ‹τ x› at the identity on ‹x›''.
However, note once again that, according to the formal definition of enriched
natural transformation, we have ‹τ x : ℐ → exp (hom⇩o x) (F⇩o x)›, so it is
necessary to transform this to an arrow: ‹(τ x) ⇧↓[hom⇩o x, F⇩o x]: hom⇩o x → F x›.
›
abbreviation generating_elem
where "generating_elem τ ≡ (τ x) ⇧↓[hom⇩o x, F⇩o x] ⋅ Id x"
lemma generating_elem_in_hom:
assumes "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ"
shows "«generating_elem τ : ℐ → F⇩o x»"
proof -
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using assms by blast
show "«generating_elem τ : ℐ → F⇩o x»"
using x Id_in_hom τ.component_in_hom [of x] F.preserves_Obj C.DN_def
by auto fastforce
qed
text‹
Now we have to verify the elements of the diagram after Kelly (1.47):
$$\xymatrix{
‹hom⇩o a›
\xuppertwocell[rrrrr]{}^{‹hom⇩o a›}<15>{\omit{}}
\ar[rr] _{‹hom⇩a x a›}
\ar[d] _{‹F⇩a a›}
&&
‹[hom⇩o x, hom⇩o a]›
\ar[rr] _{‹[Id x, hom⇩o a]›}
\ar[d] ^{‹[hom⇩o x, τ a]›}
&&
‹[ℐ, hom⇩o a]›
\ar[r] _{\textrm{iso}}
\ar[d] ^{‹[ℐ, τ a]›}
&
‹hom⇩o a›
\ar[d] ^{‹τ a›}
\\
‹[F⇩o x, F⇩o a]›
\ar[rr] ^{‹[τ⇩e x, F⇩o a]›}
\xlowertwocell[rrrr]{}_{‹[τ⇩e x ⋅ Id x, F⇩o a]›}<-15>{\omit{}}
&&
‹[hom⇩o x, F⇩o a]›
\ar[rr] ^{‹[Id x, F⇩o a]›}
&&
‹[ℐ, F⇩o a]›
\ar[r] ^{\textrm{iso}}
&
‹F⇩o a›
}$$
›
text‹
The left square is enriched naturality of ‹τ› (Kelly (1.39)).
The middle square commutes trivially.
The right square commutes by the naturality of the canonical isomorphismm
from ‹[ℐ, hom⇩o a]› to ‹hom⇩o a›.
The top edge composes to ‹hom⇩o a› (an identity).
The commutativity of the entire diagram shows that ‹τ a› is recovered from ‹e⇩τ›.
Note that where ‹τ a› appears, what is actually meant formally is ‹(τ a) ⇧↓[hom⇩o a, F⇩o a]›.
›
lemma center_square:
assumes "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ"
and "a ∈ Obj"
shows "C.Exp ℐ (τ a ⇧↓[hom⇩o a, F⇩o a]) ⋅ C.Exp (Id x) (hom⇩o a) =
C.Exp (Id x) (F⇩o a) ⋅ C.Exp (hom⇩o x) (τ a ⇧↓[hom⇩o a, F⇩o a])"
proof -
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using assms by blast
let ?τ⇩a = "τ a ⇧↓[hom⇩o a, F⇩o a]"
show "C.Exp ℐ ?τ⇩a ⋅ C.Exp (Id x) (hom⇩o a) =
C.Exp (Id x) (F⇩o a) ⋅ C.Exp (hom⇩o x) ?τ⇩a"
by (metis assms(2) x C.Exp_comp F.preserves_Obj Id_in_hom
C.DN_simps(1-3) comp_arr_dom comp_cod_arr in_homE τ.component_in_hom
ide_Hom mem_Collect_eq)
qed
lemma right_square:
assumes "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ"
and "a ∈ Obj"
shows "τ a ⇧↓[hom⇩o a, F⇩o a] ⋅ C.Dn (hom⇩o a) =
C.Dn (F⇩o a) ⋅ C.Exp ℐ (τ a ⇧↓[hom⇩o a, F⇩o a])"
proof -
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using assms by blast
show ?thesis
using assms(2) C.Up_Dn_naturality C.DN_simps τ.component_in_hom
apply auto[1]
by (metis C.Exp_ide_y C.UP_DN(2) F.preserves_Obj ide_Hom ide_unity
in_homE mem_Collect_eq x)
qed
lemma top_path:
assumes "a ∈ Obj"
shows "eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅ C.Exp (Id x) (hom⇩o a) ⋅
hom⇩a x a =
hom⇩o a"
proof -
have "eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅ C.Exp (Id x) (hom⇩o a) ⋅
hom⇩a x a =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
(Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (hom⇩o a ⋅ eval ℐ (hom⇩o a)) ⋅
Curry[exp (hom⇩o x) (hom⇩o a), ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (exp (hom⇩o x) (hom⇩o a) ⊗ Id x))) ⋅
hom⇩a x a"
using assms x C.Exp_def Id_in_hom [of x] by auto
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (hom⇩o a ⋅ eval ℐ (hom⇩o a)) ⋅
Curry[exp (hom⇩o x) (hom⇩o a), ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (exp (hom⇩o x) (hom⇩o a) ⊗ Id x)) ⋅
hom⇩a x a"
using comp_assoc by simp
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (hom⇩o a ⋅ eval ℐ (hom⇩o a)) ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
((eval (hom⇩o x) (hom⇩o a) ⋅ (exp (hom⇩o x) (hom⇩o a) ⊗ Id x)) ⋅
(hom⇩a x a ⊗ ℐ))"
proof -
have "«eval (hom⇩o x) (hom⇩o a) ⋅ (exp (hom⇩o x) (hom⇩o a) ⊗ Id x)
: exp (hom⇩o x) (hom⇩o a) ⊗ ℐ → hom⇩o a»"
using assms x
by (meson Id_in_hom comp_in_homI C.eval_in_hom_ax C.ide_exp
ide_in_hom tensor_in_hom ide_Hom)
thus ?thesis
using assms x preserves_Hom [of x a] C.comp_Curry_arr by simp
qed
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (hom⇩o a ⋅ eval ℐ (hom⇩o a)) ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅
(exp (hom⇩o x) (hom⇩o a) ⊗ Id x) ⋅ (hom⇩a x a ⊗ ℐ))"
using comp_assoc by simp
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (hom⇩o a ⋅ eval ℐ (hom⇩o a)) ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x))"
proof -
have "seq (Id x) ℐ ∧ seq (hom⇩o x) (Id x)"
using x Id_in_hom ide_in_hom ide_unity by blast
thus ?thesis
using assms x preserves_Hom comp_arr_dom [of "Id x" ℐ]
interchange [of "exp (hom⇩o x) (hom⇩o a)" "hom⇩a x a" "Id x" ℐ]
by (metis comp_cod_arr comp_ide_arr dom_eqI ide_unity
in_homE ide_Hom)
qed
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[exp ℐ (hom⇩o a), ℐ, hom⇩o a] (eval ℐ (hom⇩o a)) ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(Uncurry[hom⇩o x, hom⇩o a] (hom⇩a x a) ⋅ (hom⇩o a ⊗ Id x))"
proof -
have "eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x) =
eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⋅ hom⇩o a ⊗ hom⇩o x ⋅ Id x)"
using assms x Id_in_hom comp_cod_arr comp_arr_dom Comp_in_hom
by (metis in_homE preserves_Hom)
also have "... = eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ hom⇩o x) ⋅
(hom⇩o a ⊗ Id x)"
using assms x Id_in_hom Comp_in_hom
interchange [of "hom⇩a x a" "hom⇩o a" "hom⇩o x" "Id x"]
by (metis comp_arr_dom comp_cod_arr in_homE preserves_Hom)
also have "... = Uncurry[hom⇩o x, hom⇩o a] (hom⇩a x a) ⋅ (hom⇩o a ⊗ Id x)"
using comp_assoc by simp
finally show ?thesis
using assms x comp_cod_arr ide_Hom ide_unity C.eval_simps(1,3) by metis
qed
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(Uncurry[ℐ, hom⇩o a]
(Curry[hom⇩o a, ℐ, hom⇩o a]
(Uncurry[hom⇩o x, hom⇩o a] (hom⇩a x a) ⋅ (hom⇩o a ⊗ Id x))))"
using assms x
C.comp_Curry_arr
[of ℐ
"Curry[hom⇩o a, ℐ, hom⇩o a]
(Uncurry[hom⇩o x, hom⇩o a] (hom⇩a x a) ⋅ (hom⇩o a ⊗ Id x))"
"hom⇩o a" "exp ℐ (hom⇩o a)"
"eval ℐ (hom⇩o a)" "hom⇩o a"]
apply auto[1]
by (metis Comp_Hom_Id Comp_in_hom C.Uncurry_Curry C.eval_in_hom_ax
ide_unity C.isomorphic_exp_unity(1) ide_Hom)
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(Uncurry[hom⇩o x, hom⇩o a] (hom⇩a x a) ⋅ (hom⇩o a ⊗ Id x))"
using assms x C.Uncurry_Curry
by (simp add: Comp_Hom_Id Comp_in_hom C.Curry_Uncurry
C.isomorphic_exp_unity(1))
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ hom⇩o x) ⋅ (hom⇩o a ⊗ Id x))"
using comp_assoc by simp
also have "... =
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅
Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x))"
using assms x comp_cod_arr [of "Id x" "hom⇩o x"] comp_arr_dom
interchange [of "hom⇩a x a" "hom⇩o a" "hom⇩o x" "Id x"]
preserves_Hom [of x a] Id_in_hom
apply auto[1]
by fastforce
also have "... =
eval ℐ (hom⇩o a) ⋅
(Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x)) ⊗ ℐ) ⋅
𝗋⇧-⇧1[hom⇩o a]"
proof -
have "«Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x))
: hom⇩o a → exp ℐ (hom⇩o a)»"
using assms x preserves_Hom [of x a] Id_in_hom [of x] by force
thus ?thesis
using assms x runit'_naturality by fastforce
qed
also have "... =
Uncurry[ℐ, hom⇩o a]
(Curry[hom⇩o a, ℐ, hom⇩o a]
(eval (hom⇩o x) (hom⇩o a) ⋅ (hom⇩a x a ⊗ Id x))) ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using comp_assoc by simp
also have "... = (eval (hom⇩o x) (hom⇩o a) ⋅
(Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a) ⊗ Id x)) ⋅
𝗋⇧-⇧1[hom⇩o a]"
using assms x C.Uncurry_Curry preserves_Hom [of x a] Id_in_hom [of x]
by fastforce
also have "... = (eval (hom⇩o x) (hom⇩o a) ⋅
((Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a) ⊗ hom⇩o x) ⋅
(hom⇩o a ⊗ Id x))) ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using assms x Id_in_hom [of x] Comp_in_hom comp_arr_dom comp_cod_arr
interchange
by auto
also have "... = Uncurry[hom⇩o x, hom⇩o a]
(Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)) ⋅
(hom⇩o a ⊗ Id x) ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using comp_assoc by simp
also have "... = Comp x x a ⋅ (hom⇩o a ⊗ Id x) ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using assms x C.Uncurry_Curry Comp_in_hom by simp
also have "... = (Comp x x a ⋅ (hom⇩o a ⊗ Id x)) ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using comp_assoc by simp
also have "... = 𝗋[hom⇩o a] ⋅ 𝗋⇧-⇧1[hom⇩o a]"
using assms x Comp_Hom_Id by auto
also have "... = hom⇩o a"
using assms x comp_runit_runit' by blast
finally show ?thesis by blast
qed
text‹
The left square is an instance of Kelly (1.39), so we can get that by
instantiating that result. The confusing business is that the target
enriched category is the base category C.
›
lemma left_square:
assumes "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ"
and "a ∈ Obj"
shows "Exp⇧→ (hom⇩o x) ((τ a) ⇧↓[hom⇩o a, F⇩o a]) ⋅ hom⇩a x a =
Exp⇧← ((τ x) ⇧↓[hom⇩o x, F⇩o x]) (F⇩o a) ⋅ F⇩a x a"
proof -
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using assms(1) by blast
interpret cov_Hom: covariant_Hom C T α ι exp eval Curry
‹Collect ide› exp C.Id C.Comp ‹hom⇩o x›
using x by unfold_locales auto
interpret cnt_Hom: contravariant_Hom C T α ι σ exp eval Curry
‹Collect ide› exp C.Id C.Comp ‹F⇩o a›
using assms(2) F.preserves_Obj by unfold_locales
interpret Kelly: Kelly_1_39 C T α ι σ exp eval Curry
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ x a
using assms(2) x
by unfold_locales
text‹
The following is the enriched naturality of ‹τ›, expressed in the alternate form
involving the underlying ordinary functors of the enriched hom functors.
›
have 1: "cov_Hom.map⇩0 (hom⇩o a) (F⇩o a) (τ a) ⋅ hom⇩a x a =
cnt_Hom.map⇩0 (hom⇩o x) (F⇩o x) (τ x) ⋅ F⇩a x a"
using Kelly.Kelly_1_39 by simp
text‹
Here we have the underlying ordinary functor of the enriched covariant hom,
expressed in terms of the covariant endofunctor ‹Exp⇧→ (hom⇩o x)› on the base
category.
›
have 2: "cov_Hom.map⇩0 (hom⇩o a) (F⇩o a) (τ a) =
Exp⇧→ (hom⇩o x) ((τ a) ⇧↓[hom⇩o a, F⇩o a])"
proof -
have "cov_Hom.map⇩0 (hom⇩o a) (F⇩o a) (τ a) =
(Curry[cnt_Hom.hom⇩o (hom⇩o a), cov_Hom.hom⇩o (hom⇩o a),
cnt_Hom.hom⇩o (hom⇩o x)]
(C.Comp (hom⇩o x) (hom⇩o a) (F⇩o a)) ⋅ τ a)
⇧↓[cov_Hom.hom⇩o (hom⇩o a), cnt_Hom.hom⇩o (hom⇩o x)]"
proof -
have "cov_Hom.map⇩0 (hom⇩o a) (F⇩o a) (τ a) =
cnt_Hom.Op⇩0.Map
(cov_Hom.UF.map⇩0 (cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a)))
⇧↓[cnt_Hom.Op⇩0.Dom
(cov_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a))),
cnt_Hom.Op⇩0.Cod
(cov_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a)))]"
using assms x preserves_Obj F.preserves_Obj τ.component_in_hom
cov_Hom.Kelly_1_31 cov_Hom.UF.preserves_arr
by force
moreover
have "cnt_Hom.Op⇩0.Dom
(cov_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a))) =
exp (hom⇩o x) (hom⇩o a)"
using assms x cov_Hom.UF.map⇩0_def
apply auto[1]
using cnt_Hom.y τ.component_in_hom by force
moreover
have "cnt_Hom.Op⇩0.Cod
(cov_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a))) =
exp (hom⇩o x) (F⇩o a)"
using assms x cov_Hom.UF.map⇩0_def
apply auto[1]
using cnt_Hom.y τ.component_in_hom by fastforce
moreover
have "cnt_Hom.Op⇩0.Map
(cov_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (hom⇩o a) (F⇩o a) (τ a))) =
cov_Hom.hom⇩a (hom⇩o a) (F⇩o a) ⋅ τ a"
using assms x cov_Hom.UF.map⇩0_def
apply auto[1]
using cnt_Hom.y τ.component_in_hom by auto
ultimately show ?thesis
using assms x ide_Hom F.preserves_Obj by simp
qed
also have "... = Exp⇧→ (hom⇩o x) ((τ a) ⇧↓[hom⇩o a, F⇩o a])"
using assms(2) x C.cov_Exp_DN τ.component_in_hom F.preserves_Obj
by simp
finally show ?thesis by blast
qed
text‹
Here we have the underlying ordinary functor of the enriched contravariant hom,
expressed in terms of the contravariant endofunctor ‹λf. Exp⇧← f (F⇩o a)› on the base
category.
›
have 3: "cnt_Hom.map⇩0 (hom⇩o x) (F⇩o x) (τ x) =
Exp⇧← (τ x ⇧↓[hom⇩o x, F⇩o x]) (F⇩o a)"
proof -
have "cnt_Hom.map⇩0 (hom⇩o x) (F⇩o x) (τ x) =
Uncurry[exp (F⇩o x) (F⇩o a), exp (hom⇩o x) (F⇩o a)]
(cnt_Hom.hom⇩a (F⇩o x) (hom⇩o x) ⋅ τ x) ⋅
𝗅⇧-⇧1[exp (F⇩o x) (F⇩o a)]"
proof -
have "cnt_Hom.map⇩0 (hom⇩o x) (F⇩o x) (τ x) =
Uncurry[cnt_Hom.Op⇩0.Dom
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x))),
cnt_Hom.Op⇩0.Cod
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x)))]
(cnt_Hom.Op⇩0.Map
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (Hom x x) (τ x)))) ⋅
𝗅⇧-⇧1[cnt_Hom.Op⇩0.Dom
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x)))]"
using assms x 1 2 cnt_Hom.Kelly_1_32 [of "hom⇩o x" "F⇩o x" "τ x"]
C.Curry_simps(1-3) C.DN_def C.UP_DN(2) C.eval_simps(1-3)
C.ide_exp Comp_in_hom F.preserves_Obj comp_in_homI'
not_arr_null preserves_Obj τ.component_in_hom in_homE
mem_Collect_eq seqE
by (smt (verit))
moreover have "cnt_Hom.Op⇩0.Dom
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x))) =
exp (F⇩o x) (F⇩o a)"
using assms x cnt_Hom.UF.map⇩0_def
apply auto[1]
using F.preserves_Obj cnt_Hom.Op⇩0.arr_MkArr τ.component_in_hom
by blast
moreover have "cnt_Hom.Op⇩0.Cod
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x))) =
exp (hom⇩o x) (F⇩o a)"
using assms x cnt_Hom.UF.map⇩0_def
apply auto[1]
using F.preserves_Obj cnt_Hom.Op⇩0.arr_MkArr τ.component_in_hom
by blast
moreover have "cnt_Hom.Op⇩0.Map
(cnt_Hom.UF.map⇩0
(cnt_Hom.Op⇩0.MkArr (F⇩o x) (hom⇩o x) (τ x))) =
cnt_Hom.hom⇩a (F⇩o x) (hom⇩o x) ⋅ τ x"
using assms x cnt_Hom.UF.map⇩0_def F.preserves_Obj
by (simp add: τ.component_in_hom)
ultimately show ?thesis by argo
qed
also have "... = Exp⇧← (τ x ⇧↓[hom⇩o x, F⇩o x]) (F⇩o a)"
using assms(2) x τ.component_in_hom [of x] F.preserves_Obj
C.DN_def C.cnt_Exp_DN
by fastforce
finally show ?thesis by simp
qed
show ?thesis
using 1 2 3 by auto
qed
lemma transformation_generated_by_element:
assumes "enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ"
and "a ∈ Obj"
shows "τ a = generated_transformation (generating_elem τ) a"
proof -
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using assms(1) by blast
have "τ a ⇧↓[hom⇩o a, F⇩o a] =
τ a ⇧↓[hom⇩o a, F⇩o a] ⋅
eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)] ⋅ C.Exp (Id x) (hom⇩o a) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using assms(2) x top_path τ.component_in_hom [of a] F.preserves_Obj
comp_arr_dom C.UP_DN(2)
by auto
also have "... =
(τ a ⇧↓[hom⇩o a, F⇩o a] ⋅ eval ℐ (hom⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (hom⇩o a)]) ⋅
C.Exp (Id x) (hom⇩o a) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using comp_assoc by simp
also have "... =
(eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
C.Exp ℐ (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a])) ⋅
C.Exp (Id x) (hom⇩o a) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using assms right_square C.DN_def τ.component_in_hom comp_assoc
by auto blast
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
(C.Exp ℐ (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a]) ⋅
C.Exp (Id x) (hom⇩o a)) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using comp_assoc by simp
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
(C.Exp (Id x) (F⇩o a) ⋅
C.Exp (hom⇩o x) (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a])) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using assms center_square C.DN_def
enriched_natural_transformation.component_in_hom
by fastforce
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
C.Exp (hom⇩o x) (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a]) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a)"
using comp_assoc by simp
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
Exp⇧← (Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) (F⇩o a) ⋅ F⇩a x a"
proof -
have "eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
C.Exp (hom⇩o x) (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a]) ⋅
Curry[hom⇩o a, hom⇩o x, hom⇩o a] (Comp x x a) =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
C.Exp (hom⇩o x) (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a]) ⋅
hom⇩a x a"
using assms(2) x by force
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
Exp⇧→ (hom⇩o x) (Uncurry[hom⇩o a, F⇩o a] (τ a) ⋅ 𝗅⇧-⇧1[hom⇩o a]) ⋅
hom⇩a x a"
using assms x C.Exp_def C.cnt_Exp_ide comp_arr_dom by auto
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
Exp⇧→ (hom⇩o x) (τ a⇧↓[hom⇩o a, F⇩o a]) ⋅ hom⇩a x a"
using assms x C.DN_def by fastforce
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
Exp⇧← (τ x⇧↓[hom⇩o x, F⇩o x]) (F⇩o a) ⋅ F⇩a x a"
using assms(2) left_square τ.enriched_natural_transformation_axioms
by fastforce
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅ C.Exp (Id x) (F⇩o a) ⋅
Exp⇧← (Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) (F⇩o a) ⋅ F⇩a x a"
using C.DN_def by fastforce
finally show ?thesis by blast
qed
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
(C.Exp (Id x) (F⇩o a) ⋅
Exp⇧← (Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) (F⇩o a)) ⋅
F⇩a x a"
using comp_assoc by simp
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
(Exp⇧← (Id x) (F⇩o a) ⋅
Exp⇧← (Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) (F⇩o a)) ⋅
F⇩a x a"
using assms x F.preserves_Obj C.Exp_def C.cov_Exp_ide
comp_cod_arr [of "Exp⇧← (Id x) (dom (F⇩o a))"]
by auto
also have "... =
eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← ((Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) ⋅ Id x) (F⇩o a) ⋅
F⇩a x a"
proof -
have "seq (Uncurry[hom⇩o x, F⇩o x] (τ x) ⋅ 𝗅⇧-⇧1[hom⇩o x]) (Id x)"
using assms x F.preserves_Obj Id_in_hom τ.component_in_hom
apply (intro seqI)
apply auto[1]
by force+
thus ?thesis
using assms x F.preserves_Obj C.cnt_Exp_comp by simp
qed
also have "... = eval ℐ (F⇩o a) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o a)] ⋅
Exp⇧← (generating_elem τ) (F⇩o a) ⋅ F⇩a x a"
using x C.DN_def comp_assoc τ.component_in_hom by fastforce
also have 1: "... =
(generated_transformation (generating_elem τ) a) ⇧↓[hom⇩o a, F⇩o a]"
using assms x F.preserves_Obj C.UP_DN(4) τ.component_in_hom calculation
ide_Hom
by (metis (no_types, lifting) mem_Collect_eq)
finally have *: "(τ a) ⇧↓[hom⇩o a, F⇩o a] =
(generated_transformation (generating_elem τ) a)
⇧↓[hom⇩o a, F⇩o a]"
by blast
have "τ a = ((τ a) ⇧↓[hom⇩o a, F⇩o a])⇧↑"
using assms x τ.component_in_hom ide_Hom F.preserves_Obj by auto
also have "... = ((generated_transformation (generating_elem τ) a)
⇧↓[hom⇩o a, F⇩o a])⇧↑"
using * by argo
also have "... = generated_transformation (generating_elem τ) a"
using assms x 1 ide_Hom by presburger
finally show "τ a = generated_transformation (generating_elem τ) a" by blast
qed
lemma element_of_generated_transformation:
assumes "e ∈ hom ℐ (F⇩o x)"
shows "generating_elem (generated_transformation e) = e"
proof -
have "generating_elem (generated_transformation e) =
Uncurry[hom⇩o x, F⇩o x]
((eval ℐ (F⇩o x) ⋅ 𝗋⇧-⇧1[exp ℐ (F⇩o x)] ⋅
Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e)) ⋅ F⇩a x x)⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
proof -
have "arr ((eval ℐ (F⇩o x) ⋅
𝗋⇧-⇧1[exp ℐ (F⇩o x)] ⋅
Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e)) ⋅ F⇩a x x)⇧↑)"
using assms x F.preserves_Hom F.preserves_Obj
apply (intro C.UP_simps seqI)
apply auto[1]
by fastforce+
thus ?thesis
using assms x C.DN_def comp_assoc by auto
qed
also have "... =
Uncurry[hom⇩o x, F⇩o x]
((eval ℐ (F⇩o x) ⋅
(𝗋⇧-⇧1[exp ℐ (F⇩o x)] ⋅
Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e))) ⋅ F⇩a x x)⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using comp_assoc by simp
also have "... =
Uncurry[hom⇩o x, F⇩o x]
((eval ℐ (F⇩o x) ⋅
((Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e)) ⊗ ℐ) ⋅
𝗋⇧-⇧1[exp (F⇩o x) (F⇩o x)]) ⋅
F⇩a x x)⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
proof -
have "«Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e))
: exp (F⇩o x) (F⇩o x) → exp ℐ (F⇩o x)»"
using assms x F.preserves_Obj C.ide_exp
by (intro C.Curry_in_hom) auto
thus ?thesis
using assms
runit'_naturality
[of "Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e))"]
by force
qed
also have "... =
Uncurry[hom⇩o x, F⇩o x]
((Uncurry[ℐ, F⇩o x]
(Curry[exp (F⇩o x) (F⇩o x), ℐ, F⇩o x]
(eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e))) ⋅
𝗋⇧-⇧1[exp (F⇩o x) (F⇩o x)] ⋅ F⇩a x x)⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using comp_assoc by simp
also have "... =
Uncurry[hom⇩o x, F⇩o x]
(((eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e)) ⋅
𝗋⇧-⇧1[exp (F⇩o x) (F⇩o x)] ⋅ F⇩a x x)⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using assms x F.preserves_Obj C.Uncurry_Curry by auto
also have "... =
Uncurry[hom⇩o x, F⇩o x]
(((eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e)) ⋅
(F⇩a x x ⊗ ℐ) ⋅ 𝗋⇧-⇧1[hom⇩o x])⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using assms x runit'_naturality F.preserves_Hom [of x x] by fastforce
also have "... =
Uncurry[hom⇩o x, F⇩o x]
(((eval (F⇩o x) (F⇩o x) ⋅ (exp (F⇩o x) (F⇩o x) ⊗ e) ⋅ (F⇩a x x ⊗ ℐ)) ⋅
𝗋⇧-⇧1[hom⇩o x])⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using comp_assoc by simp
also have "... =
Uncurry[hom⇩o x, F⇩o x]
(((eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e)) ⋅ 𝗋⇧-⇧1[hom⇩o x])⇧↑) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
using assms x F.preserves_Hom [of x x] comp_arr_dom [of e ℐ] comp_cod_arr
interchange
by fastforce
also have "... =
Uncurry[hom⇩o x, F⇩o x]
(Curry[ℐ, hom⇩o x, F⇩o x]
(((eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e)) ⋅ 𝗋⇧-⇧1[hom⇩o x]) ⋅ 𝗅[hom⇩o x])) ⋅
𝗅⇧-⇧1[hom⇩o x] ⋅ Id x"
proof -
have "seq (eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e)) 𝗋⇧-⇧1[Hom x x]"
using assms x F.preserves_Obj F.preserves_Hom by blast
thus ?thesis
using assms x C.UP_def F.preserves_Obj by auto
qed
also have "... =
(((eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e)) ⋅ 𝗋⇧-⇧1[Hom x x]) ⋅ 𝗅[Hom x x]) ⋅
𝗅⇧-⇧1[Hom x x] ⋅ Id x"
using assms x C.Uncurry_Curry F.preserves_Obj F.preserves_Hom by force
also have "... =
eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e) ⋅ 𝗋⇧-⇧1[Hom x x] ⋅
(𝗅[Hom x x] ⋅ 𝗅⇧-⇧1[Hom x x]) ⋅ Id x"
using comp_assoc by simp
also have "... = eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e) ⋅ 𝗋⇧-⇧1[Hom x x] ⋅ Id x"
using assms x ide_Hom Id_in_hom comp_lunit_lunit'(1) comp_cod_arr
by fastforce
also have "... = eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⊗ e) ⋅ (Id x ⊗ ℐ) ⋅ 𝗋⇧-⇧1[ℐ]"
using x Id_in_hom runit'_naturality by fastforce
also have "... = eval (F⇩o x) (F⇩o x) ⋅ ((F⇩a x x ⊗ e) ⋅ (Id x ⊗ ℐ)) ⋅ 𝗋⇧-⇧1[ℐ]"
using comp_assoc by simp
also have "... = eval (F⇩o x) (F⇩o x) ⋅ (F⇩a x x ⋅ Id x ⊗ e) ⋅ 𝗋⇧-⇧1[ℐ]"
using assms x interchange [of "F⇩a x x" "Id x" e ℐ] F.preserves_Hom
comp_arr_dom Id_in_hom
by fastforce
also have "... = eval (F⇩o x) (F⇩o x) ⋅ (C.Id (F⇩o x) ⊗ e) ⋅ 𝗋⇧-⇧1[ℐ]"
using x F.preserves_Id by auto
also have "... =
eval (F⇩o x) (F⇩o x) ⋅ ((C.Id (F⇩o x) ⊗ F⇩o x) ⋅ (ℐ ⊗ e)) ⋅ 𝗋⇧-⇧1[ℐ]"
using assms x interchange C.Id_in_hom F.preserves_Obj comp_arr_dom
comp_cod_arr
by (metis in_homE mem_Collect_eq)
also have "... = Uncurry[F⇩o x, F⇩o x] (C.Id (F⇩o x)) ⋅ (ℐ ⊗ e) ⋅ 𝗋⇧-⇧1[ℐ]"
using comp_assoc by simp
also have "... = 𝗅[F⇩o x] ⋅ (ℐ ⊗ e) ⋅ 𝗋⇧-⇧1[ℐ]"
using x F.preserves_Obj C.Id_def C.Uncurry_Curry by fastforce
also have "... = 𝗅[F⇩o x] ⋅ (ℐ ⊗ e) ⋅ 𝗅⇧-⇧1[ℐ]"
using unitor_coincidence by simp
also have "... = 𝗅[F⇩o x] ⋅ 𝗅⇧-⇧1[F⇩o x] ⋅ e"
using assms lunit'_naturality by fastforce
also have "... = (𝗅[F⇩o x] ⋅ 𝗅⇧-⇧1[F⇩o x]) ⋅ e"
using comp_assoc by simp
also have "... = e"
using assms x comp_lunit_lunit' F.preserves_Obj comp_cod_arr by auto
finally show "generating_elem (generated_transformation e) = e"
by blast
qed
text‹
We can now state and prove the (weak) covariant Yoneda lemma (Kelly, Section 1.9)
for enriched categories.
›
theorem covariant_yoneda:
shows "bij_betw generated_transformation
(hom ℐ (F⇩o x))
(Collect (enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a))"
proof (intro bij_betwI)
show "generated_transformation ∈
hom ℐ (F⇩o x) → Collect
(enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a)"
using enriched_natural_transformation_generated_transformation by blast
show "generating_elem ∈
Collect (enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a)
→ hom ℐ (F⇩o x)"
using generating_elem_in_hom by blast
show "⋀e. e ∈ hom ℐ (F⇩o x) ⟹
generating_elem (generated_transformation e) = e"
using element_of_generated_transformation by blast
show "⋀τ. τ ∈ Collect (enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a)
⟹ generated_transformation (generating_elem τ) = τ"
proof -
fix τ
assume τ: "τ ∈ Collect (enriched_natural_transformation C T α ι
Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a)"
interpret τ: enriched_natural_transformation C T α ι
Obj Hom Id Comp ‹Collect ide› exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a τ
using τ by blast
show "generated_transformation (generating_elem τ) = τ"
proof
fix a
show "generated_transformation (generating_elem τ) a = τ a"
using τ transformation_generated_by_element τ.extensionality
F.extensionality C.UP_def not_arr_null null_is_zero(2)
by (cases "a ∈ Obj") auto
qed
qed
qed
end
subsection "Contravariant Case"
text‹
The (weak) contravariant Yoneda lemma is obtained by just replacing the enriched category
by its opposite in the covariant version.
›
locale contravariant_yoneda_lemma =
opposite_enriched_category C T α ι σ Obj Hom Id Comp +
covariant_yoneda_lemma C T α ι σ exp eval Curry Obj Hom⇩o⇩p Id Comp⇩o⇩p y F⇩o F⇩a
for C :: "'a ⇒ 'a ⇒ 'a" (infixr ‹⋅› 55)
and T :: "'a × 'a ⇒ 'a"
and α :: "'a × 'a × 'a ⇒ 'a"
and ι :: "'a"
and σ :: "'a × 'a ⇒ 'a"
and exp :: "'a ⇒ 'a ⇒ 'a"
and eval :: "'a ⇒ 'a ⇒ 'a"
and Curry :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
and Obj :: "'b set"
and Hom :: "'b ⇒ 'b ⇒ 'a"
and Id :: "'b ⇒ 'a"
and Comp :: "'b ⇒ 'b ⇒ 'b ⇒ 'a"
and y :: 'b
and F⇩o :: "'b ⇒ 'a"
and F⇩a :: "'b ⇒ 'b ⇒ 'a"
begin
corollary contravariant_yoneda:
shows "bij_betw generated_transformation
(hom ℐ (F⇩o y))
(Collect
(enriched_natural_transformation
C T α ι Obj Hom⇩o⇩p Id Comp⇩o⇩p (Collect ide) exp C.Id C.Comp
hom⇩o hom⇩a F⇩o F⇩a))"
using covariant_yoneda by blast
end
end