Theory 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