Theory FreeMonoidalCategory
chapter "The Free Monoidal Category"
text_raw‹
\label{fmc-chap}
›
theory FreeMonoidalCategory
imports Category3.Subcategory MonoidalFunctor
begin
text ‹
In this theory, we use the monoidal language of a category @{term C} defined in
@{theory MonoidalCategory.MonoidalCategory} to give a construction of the free monoidal category
‹ℱC› generated by @{term C}.
The arrows of ‹ℱC› are the equivalence classes of formal arrows obtained
by declaring two formal arrows to be equivalent if they are parallel and have the
same diagonalization.
Composition, tensor, and the components of the associator and unitors are all
defined in terms of the corresponding syntactic constructs.
After defining ‹ℱC› and showing that it does indeed have the structure of
a monoidal category, we prove the freeness: every functor from @{term C} to a
monoidal category @{term D} extends uniquely to a strict monoidal functor from
‹ℱC› to @{term D}.
We then consider the full subcategory ‹ℱ⇩SC› of ‹ℱC› whose objects
are the equivalence classes of diagonal identity terms
({\em i.e.}~equivalence classes of lists of identity arrows of @{term C}),
and we show that this category is monoidally equivalent to ‹ℱC›.
In addition, we show that ‹ℱ⇩SC› is the free strict monoidal category,
as any functor from ‹C› to a strict monoidal category @{term D} extends uniquely
to a strict monoidal functor from ‹ℱ⇩SC› to @{term D}.
›
section "Syntactic Construction"
locale free_monoidal_category =
monoidal_language C
for C :: "'c comp"
begin
no_notation C.in_hom (‹«_ : _ → _»›)
notation C.in_hom (‹«_ : _ →⇩C _»›)
text ‹
Two terms of the monoidal language of @{term C} are defined to be equivalent if
they are parallel formal arrows with the same diagonalization.
›
abbreviation equiv
where "equiv t u ≡ Par t u ∧ ❙⌊t❙⌋ = ❙⌊u❙⌋"
text ‹
Arrows of ‹ℱC› will be the equivalence classes of formal arrows
determined by the relation @{term equiv}. We define here the property of being an
equivalence class of the relation @{term equiv}. Later we show that this property
coincides with that of being an arrow of the category that we will construct.
›
type_synonym 'a arr = "'a term set"
definition ARR where "ARR f ≡ f ≠ {} ∧ (∀t. t ∈ f ⟶ f = Collect (equiv t))"
lemma not_ARR_empty:
shows "¬ARR {}"
using ARR_def by simp
lemma ARR_eqI:
assumes "ARR f" and "ARR g" and "f ∩ g ≠ {}"
shows "f = g"
using assms ARR_def by fastforce
text ‹
We will need to choose a representative of each equivalence class as a normal form.
The requirements we have of these representatives are: (1) the normal form of an
arrow @{term t} is equivalent to @{term t}; (2) equivalent arrows have identical
normal forms; (3) a normal form is a canonical term if and only if its diagonalization
is an identity. It follows from these properties and coherence that a term and its
normal form have the same evaluation in any monoidal category. We choose here as a
normal form for an arrow @{term t} the particular term @{term "Inv (Cod t❙↓) ❙⋅ ❙⌊t❙⌋ ❙⋅ Dom t❙↓"}.
However, the only specific properties of this definition we actually use are the
three we have just stated.
›
definition norm (‹❙∥_❙∥›)
where "❙∥t❙∥ = Inv (Cod t❙↓) ❙⋅ ❙⌊t❙⌋ ❙⋅ Dom t❙↓"
text ‹
If @{term t} is a formal arrow, then @{term t} is equivalent to its normal form.
›
lemma equiv_norm_Arr:
assumes "Arr t"
shows "equiv ❙∥t❙∥ t"
proof -
have "Par t (Inv (Cod t❙↓) ❙⋅ ❙⌊t❙⌋ ❙⋅ Dom t❙↓)"
using assms Diagonalize_in_Hom red_in_Hom Inv_in_Hom Arr_implies_Ide_Dom
Arr_implies_Ide_Cod Ide_implies_Arr Can_red
by auto
moreover have "❙⌊(Inv (Cod t❙↓) ❙⋅ ❙⌊t❙⌋ ❙⋅ Dom t❙↓)❙⌋ = ❙⌊t❙⌋"
using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diagonalize_preserves_Ide
Diagonalize_in_Hom Diagonalize_Inv [of "Cod t❙↓"] Diag_Diagonalize
CompDiag_Diag_Dom [of "❙⌊t❙⌋"] CompDiag_Cod_Diag [of "❙⌊t❙⌋"]
by (simp add: Diagonalize_red [of "Cod t"] Can_red(1))
ultimately show ?thesis using norm_def by simp
qed
text ‹
Equivalent arrows have identical normal forms.
›
lemma norm_respects_equiv:
assumes "equiv t u"
shows "❙∥t❙∥ = ❙∥u❙∥"
using assms norm_def by simp
text ‹
The normal form of an arrow is canonical if and only if its diagonalization
is an identity term.
›
lemma Can_norm_iff_Ide_Diagonalize:
assumes "Arr t"
shows "Can ❙∥t❙∥ ⟷ Ide ❙⌊t❙⌋"
using assms norm_def Can_implies_Arr Arr_implies_Ide_Dom Arr_implies_Ide_Cod Can_red
Inv_preserves_Can Diagonalize_preserves_Can red_in_Hom Diagonalize_in_Hom
Ide_Diagonalize_Can
by fastforce
text ‹
We now establish various additional properties of normal forms that are consequences
of the three already proved. The definition ‹norm_def› is not used subsequently.
›
lemma norm_preserves_Can:
assumes "Can t"
shows "Can ❙∥t❙∥"
using assms Can_implies_Arr Can_norm_iff_Ide_Diagonalize Ide_Diagonalize_Can by simp
lemma Par_Arr_norm:
assumes "Arr t"
shows "Par ❙∥t❙∥ t"
using assms equiv_norm_Arr by auto
lemma Diagonalize_norm [simp]:
assumes "Arr t"
shows " ❙⌊❙∥t❙∥❙⌋ = ❙⌊t❙⌋"
using assms equiv_norm_Arr by auto
lemma unique_norm:
assumes "ARR f"
shows "∃!t. ∀u. u ∈ f ⟶ ❙∥u❙∥ = t"
proof
have 1: "(SOME t. t ∈ f) ∈ f"
using assms ARR_def someI_ex [of "λt. t ∈ f"] by auto
show "⋀t. ∀u. u ∈ f ⟶ ❙∥u❙∥ = t ⟹ t = ❙∥SOME t. t ∈ f❙∥"
using assms ARR_def 1 by auto
show "∀u. u ∈ f ⟶ ❙∥u❙∥ = ❙∥SOME t. t ∈ f❙∥"
using assms ARR_def 1 norm_respects_equiv by blast
qed
lemma Dom_norm:
assumes "Arr t"
shows "Dom ❙∥t❙∥ = Dom t"
using assms Par_Arr_norm by metis
lemma Cod_norm:
assumes "Arr t"
shows "Cod ❙∥t❙∥ = Cod t"
using assms Par_Arr_norm by metis
lemma norm_in_Hom:
assumes "Arr t"
shows "❙∥t❙∥ ∈ Hom (Dom t) (Cod t)"
using assms Par_Arr_norm [of t] by simp
text ‹
As all the elements of an equivalence class have the same normal form, we can
use the normal form of an arbitrarily chosen element as a canonical representative.
›
definition rep where "rep f ≡ ❙∥SOME t. t ∈ f❙∥"
lemma rep_in_ARR:
assumes "ARR f"
shows "rep f ∈ f"
using assms ARR_def someI_ex [of "λt. t ∈ f"] equiv_norm_Arr rep_def ARR_def
by fastforce
lemma Arr_rep_ARR:
assumes "ARR f"
shows "Arr (rep f)"
using assms ARR_def rep_in_ARR by auto
text ‹
We next define a function ‹mkarr› that maps formal arrows to their equivalence classes.
For terms that are not formal arrows, the function yields the empty set.
›
definition mkarr where "mkarr t = Collect (equiv t)"
lemma mkarr_extensionality:
assumes "¬Arr t"
shows "mkarr t = {}"
using assms mkarr_def by simp
lemma ARR_mkarr:
assumes "Arr t"
shows "ARR (mkarr t)"
using assms ARR_def mkarr_def by auto
lemma mkarr_memb_ARR:
assumes "ARR f" and "t ∈ f"
shows "mkarr t = f"
using assms ARR_def mkarr_def by simp
lemma mkarr_rep_ARR [simp]:
assumes "ARR f"
shows "mkarr (rep f) = f"
using assms rep_in_ARR mkarr_memb_ARR by auto
lemma Arr_in_mkarr:
assumes "Arr t"
shows "t ∈ mkarr t"
using assms mkarr_def by simp
text ‹
Two terms are related by @{term equiv} iff they are both formal arrows
and have identical normal forms.
›
lemma equiv_iff_eq_norm:
shows "equiv t u ⟷ Arr t ∧ Arr u ∧ ❙∥t❙∥ = ❙∥u❙∥"
proof
show "equiv t u ⟹ Arr t ∧ Arr u ∧ ❙∥t❙∥ = ❙∥u❙∥"
using mkarr_def Arr_in_mkarr ARR_mkarr unique_norm by blast
show "Arr t ∧ Arr u ∧ ❙∥t❙∥ = ❙∥u❙∥ ⟹ equiv t u"
using Par_Arr_norm Diagonalize_norm by metis
qed
lemma norm_norm [simp]:
assumes "Arr t"
shows "❙∥❙∥t❙∥❙∥ = ❙∥t❙∥"
proof -
have "t ∈ mkarr t"
using assms Arr_in_mkarr by blast
moreover have "❙∥t❙∥ ∈ mkarr t"
using assms equiv_norm_Arr mkarr_def by simp
ultimately show ?thesis using assms ARR_mkarr unique_norm by auto
qed
lemma norm_in_ARR:
assumes "ARR f" and "t ∈ f"
shows "❙∥t❙∥ ∈ f"
using assms ARR_def equiv_iff_eq_norm norm_norm Par_Arr_norm by fastforce
lemma norm_rep_ARR [simp]:
assumes "ARR f"
shows "❙∥rep f❙∥ = rep f"
using assms ARR_def someI_ex [of "λt. t ∈ f"] rep_def norm_norm by fastforce
lemma norm_memb_eq_rep_ARR:
assumes "ARR f" and "t ∈ f"
shows "norm t = rep f"
using assms ARR_def someI_ex [of "λt. t ∈ f"] unique_norm rep_def by metis
lemma rep_mkarr:
assumes "Arr f"
shows "rep (mkarr f) = ❙∥f❙∥"
using assms ARR_mkarr Arr_in_mkarr norm_memb_eq_rep_ARR by fastforce
text ‹
To prove that two terms determine the same equivalence class,
it suffices to show that they are parallel formal arrows with
identical diagonalizations.
›
lemma mkarr_eqI [intro]:
assumes "Par f g" and "❙⌊f❙⌋ = ❙⌊g❙⌋"
shows "mkarr f = mkarr g"
using assms by (metis ARR_mkarr equiv_iff_eq_norm rep_mkarr mkarr_rep_ARR)
text ‹
We use canonical representatives to lift the formal domain and codomain functions
from terms to equivalence classes.
›
abbreviation DOM where "DOM f ≡ Dom (rep f)"
abbreviation COD where "COD f ≡ Cod (rep f)"
lemma DOM_mkarr:
assumes "Arr t"
shows "DOM (mkarr t) = Dom t"
using assms rep_mkarr by (metis Par_Arr_norm)
lemma COD_mkarr:
assumes "Arr t"
shows "COD (mkarr t) = Cod t"
using assms rep_mkarr by (metis Par_Arr_norm)
text ‹
A composition operation can now be defined on equivalence classes
using the syntactic constructor ‹Comp›.
›
definition comp (infixr ‹⋅› 55)
where "comp f g ≡ (if ARR f ∧ ARR g ∧ DOM f = COD g
then mkarr ((rep f) ❙⋅ (rep g)) else {})"
text ‹
We commence the task of showing that the composition ‹comp› so defined
determines a category.
›
interpretation partial_composition comp
apply unfold_locales
using comp_def not_ARR_empty by metis
notation in_hom (‹«_ : _ → _»›)
text ‹
The empty set serves as the null for the composition.
›
lemma null_char:
shows "null = {}"
proof -
let ?P = "λn. ∀f. f ⋅ n = n ∧ n ⋅ f = n"
have "?P {}" using comp_def not_ARR_empty by simp
moreover have "∃!n. ?P n" using ex_un_null by metis
ultimately show ?thesis using null_def theI_unique [of ?P "{}"]
by (metis null_is_zero(2))
qed
lemma ARR_comp:
assumes "ARR f" and "ARR g" and "DOM f = COD g"
shows "ARR (f ⋅ g)"
using assms comp_def Arr_rep_ARR ARR_mkarr(1) by simp
lemma DOM_comp [simp]:
assumes "ARR f" and "ARR g" and "DOM f = COD g"
shows "DOM (f ⋅ g) = DOM g"
using assms comp_def ARR_comp Arr_rep_ARR DOM_mkarr by simp
lemma COD_comp [simp]:
assumes "ARR f" and "ARR g" and "DOM f = COD g"
shows "COD (f ⋅ g) = COD f"
using assms comp_def ARR_comp Arr_rep_ARR COD_mkarr by simp
lemma comp_assoc:
assumes "g ⋅ f ≠ null" and "h ⋅ g ≠ null"
shows "h ⋅ (g ⋅ f) = (h ⋅ g) ⋅ f"
proof -
have 1: "ARR f ∧ ARR g ∧ ARR h ∧ DOM h = COD g ∧ DOM g = COD f"
using assms comp_def not_ARR_empty null_char by metis
hence 2: "Arr (rep f) ∧ Arr (rep g) ∧ Arr (rep h) ∧
Dom (rep h) = Cod (rep g) ∧ Dom (rep g) = Cod (rep f)"
using Arr_rep_ARR by simp
have 3: "h ⋅ g ⋅ f = mkarr (rep h ❙⋅ rep (mkarr (rep g ❙⋅ rep f)))"
using 1 comp_def ARR_comp COD_comp by simp
also have "... = mkarr (rep h ❙⋅ rep g ❙⋅ rep f)"
proof -
have "equiv (rep h ❙⋅ rep (mkarr (rep g ❙⋅ rep f))) (rep h ❙⋅ rep g ❙⋅ rep f)"
proof -
have "Par (rep h ❙⋅ rep (mkarr (rep g ❙⋅ rep f))) (rep h ❙⋅ rep g ❙⋅ rep f)"
using 1 2 3 DOM_mkarr ARR_comp COD_comp mkarr_extensionality not_ARR_empty
by (metis Arr.simps(4) Cod.simps(4) Dom.simps(4) snd_map_prod)
moreover have "❙⌊rep h ❙⋅ rep (mkarr (rep g ❙⋅ rep f))❙⌋ = ❙⌊rep h ❙⋅ rep g ❙⋅ rep f❙⌋"
using 1 2 Arr_rep_ARR rep_mkarr rep_in_ARR assms(1) ARR_comp mkarr_extensionality
comp_def equiv_iff_eq_norm norm_memb_eq_rep_ARR null_char
by auto
ultimately show ?thesis using equiv_iff_eq_norm by blast
qed
thus ?thesis
using mkarr_def by force
qed
also have "... = mkarr ((rep h ❙⋅ rep g) ❙⋅ rep f)"
proof -
have "Par (rep h ❙⋅ rep g ❙⋅ rep f) ((rep h ❙⋅ rep g) ❙⋅ rep f)"
using 2 by simp
moreover have "❙⌊rep h ❙⋅ rep g ❙⋅ rep f❙⌋ = ❙⌊(rep h ❙⋅ rep g) ❙⋅ rep f❙⌋"
using 2 Diag_Diagonalize by (simp add: CompDiag_assoc)
ultimately show ?thesis
using equiv_iff_eq_norm by (simp add: mkarr_def)
qed
also have "... = mkarr (rep (mkarr (rep h ❙⋅ rep g)) ❙⋅ rep f)"
proof -
have "equiv (rep (mkarr (rep h ❙⋅ rep g)) ❙⋅ rep f) ((rep h ❙⋅ rep g) ❙⋅ rep f)"
proof -
have "Par (rep (mkarr (rep h ❙⋅ rep g)) ❙⋅ rep f) ((rep h ❙⋅ rep g) ❙⋅ rep f)"
using 1 2 Arr_rep_ARR DOM_comp ARR_comp COD_comp comp_def by auto
moreover have "❙⌊rep (mkarr (rep h ❙⋅ rep g)) ❙⋅ rep f❙⌋ = ❙⌊(rep h ❙⋅ rep g) ❙⋅ rep f❙⌋"
using assms(2) 1 2 ARR_comp Arr_rep_ARR mkarr_extensionality rep_mkarr rep_in_ARR
equiv_iff_eq_norm norm_memb_eq_rep_ARR comp_def null_char
by simp
ultimately show ?thesis using equiv_iff_eq_norm by blast
qed
thus ?thesis
using mkarr_def by auto
qed
also have "... = (h ⋅ g) ⋅ f"
using 1 comp_def ARR_comp DOM_comp by simp
finally show ?thesis by blast
qed
lemma Comp_in_comp_ARR:
assumes "ARR f" and "ARR g" and "DOM f = COD g"
and "t ∈ f" and "u ∈ g"
shows "t ❙⋅ u ∈ f ⋅ g"
proof -
have "equiv (t ❙⋅ u) (rep f ❙⋅ rep g)"
proof -
have 1: "Par (t ❙⋅ u) (rep f ❙⋅ rep g)"
using assms ARR_def Arr_rep_ARR COD_mkarr DOM_mkarr mkarr_memb_ARR
mkarr_extensionality
by (metis (no_types, lifting) Arr.simps(4) Cod.simps(4) Dom.simps(4) snd_map_prod)
moreover have "❙⌊t ❙⋅ u❙⌋ = ❙⌊rep f ❙⋅ rep g❙⌋"
using assms 1 rep_in_ARR equiv_iff_eq_norm norm_memb_eq_rep_ARR
by (metis (no_types, lifting) Arr.simps(4) Diagonalize.simps(4))
ultimately show ?thesis by simp
qed
thus ?thesis
using assms comp_def mkarr_def by simp
qed
text ‹
Ultimately, we will show that that the identities of the category are those
equivalence classes, all of whose members diagonalize to formal identity arrows,
having the further property that their canonical representative is a formal
endo-arrow.
›
definition IDE where "IDE f ≡ ARR f ∧ (∀t. t ∈ f ⟶ Ide ❙⌊t❙⌋) ∧ DOM f = COD f"
lemma IDE_implies_ARR:
assumes "IDE f"
shows "ARR f"
using assms IDE_def ARR_def by auto
lemma IDE_mkarr_Ide:
assumes "Ide a"
shows "IDE (mkarr a)"
proof -
have "DOM (mkarr a) = COD (mkarr a)"
using assms mkarr_def equiv_iff_eq_norm Par_Arr_norm COD_mkarr DOM_mkarr Ide_in_Hom
by (metis Ide_implies_Can Inv_Ide Ide_implies_Arr Inv_preserves_Can(2))
moreover have "ARR (mkarr a) ∧ (∀t. t ∈ mkarr a ⟶ Ide ❙⌊t❙⌋)"
proof -
have "ARR (mkarr a)" using assms ARR_mkarr Ide_implies_Arr by simp
moreover have "∀t. t ∈ mkarr a ⟶ Ide ❙⌊t❙⌋"
using assms mkarr_def Diagonalize_preserves_Ide by fastforce
ultimately show ?thesis by blast
qed
ultimately show ?thesis using IDE_def by blast
qed
lemma IDE_implies_ide:
assumes "IDE a"
shows "ide a"
proof (unfold ide_def)
have "a ⋅ a ≠ null"
proof -
have "rep a ❙⋅ rep a ∈ a ⋅ a"
using assms IDE_def comp_def Arr_rep_ARR Arr_in_mkarr by simp
thus ?thesis
using null_char by auto
qed
moreover have "⋀f. (f ⋅ a ≠ null ⟶ f ⋅ a = f) ∧ (a ⋅ f ≠ null ⟶ a ⋅ f = f)"
proof
fix f :: "'c arr"
show "a ⋅ f ≠ null ⟶ a ⋅ f = f"
proof
assume f: "a ⋅ f ≠ null"
hence "ARR f"
using comp_def null_char by auto
have "rep a ❙⋅ rep f ∈ a ⋅ f"
using assms f Comp_in_comp_ARR comp_def rep_in_ARR null_char by metis
moreover have "rep a ❙⋅ rep f ∈ f"
proof -
have "rep f ∈ f"
using ‹ARR f› rep_in_ARR by auto
moreover have "equiv (rep a ❙⋅ rep f) (rep f)"
proof -
have 1: "Par (rep a ❙⋅ rep f) (rep f)"
using assms f comp_def mkarr_extensionality Arr_rep_ARR IDE_def null_char
by (metis Cod.simps(4) Dom.simps(4))
moreover have "❙⌊rep a ❙⋅ rep f❙⌋ = ❙⌊rep f❙⌋"
using assms f 1 comp_def IDE_def CompDiag_Ide_Diag Diag_Diagonalize(1)
Diag_Diagonalize(2) Diag_Diagonalize(3) rep_in_ARR
by auto
ultimately show ?thesis by auto
qed
ultimately show ?thesis
using ‹ARR f› ARR_def by auto
qed
ultimately show "a ⋅ f = f"
using mkarr_memb_ARR comp_def by auto
qed
show "f ⋅ a ≠ null ⟶ f ⋅ a = f"
proof
assume f: "f ⋅ a ≠ null"
hence "ARR f"
using comp_def null_char by auto
have "rep f ❙⋅ rep a ∈ f ⋅ a"
using assms f Comp_in_comp_ARR comp_def rep_in_ARR null_char by metis
moreover have "rep f ❙⋅ rep a ∈ f"
proof -
have "rep f ∈ f"
using ‹ARR f› rep_in_ARR by auto
moreover have "equiv (rep f ❙⋅ rep a) (rep f)"
proof -
have 1: "Par (rep f ❙⋅ rep a) (rep f)"
using assms f comp_def mkarr_extensionality Arr_rep_ARR IDE_def null_char
by (metis Cod.simps(4) Dom.simps(4))
moreover have "❙⌊rep f ❙⋅ rep a❙⌋ = ❙⌊rep f❙⌋"
using assms f 1 comp_def IDE_def CompDiag_Diag_Ide
Diag_Diagonalize(1) Diag_Diagonalize(2) Diag_Diagonalize(3)
rep_in_ARR
by force
ultimately show ?thesis by auto
qed
ultimately show ?thesis
using ‹ARR f› ARR_def by auto
qed
ultimately show "f ⋅ a = f"
using mkarr_memb_ARR comp_def by auto
qed
qed
ultimately show "a ⋅ a ≠ null ∧
(∀f. (f ⋅ a ≠ null ⟶ f ⋅ a = f) ∧ (a ⋅ f ≠ null ⟶ a ⋅ f = f))"
by blast
qed
lemma ARR_iff_has_domain:
shows "ARR f ⟷ domains f ≠ {}"
proof
assume f: "domains f ≠ {}"
show "ARR f" using f domains_def comp_def null_char by auto
next
assume f: "ARR f"
have "Ide (DOM f)"
using f ARR_def by (simp add: Arr_implies_Ide_Dom Arr_rep_ARR)
hence "IDE (mkarr (DOM f))" using IDE_mkarr_Ide by metis
hence "ide (mkarr (DOM f))" using IDE_implies_ide by simp
moreover have "f ⋅ mkarr (DOM f) = f"
proof -
have 1: "rep f ❙⋅ DOM f ∈ f ⋅ mkarr (DOM f)"
using f Comp_in_comp_ARR
using IDE_implies_ARR Ide_in_Hom rep_in_ARR ‹IDE (mkarr (DOM f))›
‹Ide (DOM f)› Arr_in_mkarr COD_mkarr
by fastforce
moreover have "rep f ❙⋅ DOM f ∈ f"
proof -
have 2: "rep f ∈ f" using f rep_in_ARR by simp
moreover have "equiv (rep f ❙⋅ DOM f) (rep f)"
by (metis 1 Arr.simps(4) Arr_rep_ARR COD_mkarr Cod.simps(4)
Diagonalize_Comp_Arr_Dom Dom.simps(4) IDE_def Ide_implies_Arr
‹IDE (mkarr (DOM f))› ‹Ide (DOM f)› all_not_in_conv DOM_mkarr comp_def)
ultimately show ?thesis
using f ARR_eqI 1 ‹ide (mkarr (DOM f))› null_char ide_def by auto
qed
ultimately show ?thesis
using f ARR_eqI ‹ide (mkarr (DOM f))› null_char ide_def by auto
qed
ultimately show "domains f ≠ {}"
using f domains_def not_ARR_empty null_char by auto
qed
lemma ARR_iff_has_codomain:
shows "ARR f ⟷ codomains f ≠ {}"
proof
assume f: "codomains f ≠ {}"
show "ARR f" using f codomains_def comp_def null_char by auto
next
assume f: "ARR f"
have "Ide (COD f)"
using f ARR_def by (simp add: Arr_rep_ARR Arr_implies_Ide_Cod)
hence "IDE (mkarr (COD f))" using IDE_mkarr_Ide by metis
hence "ide (mkarr (COD f))" using IDE_implies_ide by simp
moreover have "mkarr (COD f) ⋅ f = f"
proof -
have 1: "COD f ❙⋅ rep f ∈ mkarr (COD f) ⋅ f"
using f Comp_in_comp_ARR
using IDE_implies_ARR Ide_in_Hom rep_in_ARR ‹IDE (mkarr (COD f))›
‹Ide (COD f)› Arr_in_mkarr DOM_mkarr
by fastforce
moreover have "COD f ❙⋅ rep f ∈ f"
using 1 null_char norm_rep_ARR norm_memb_eq_rep_ARR mkarr_memb_ARR
‹ide (mkarr (COD f))› emptyE equiv_iff_eq_norm mkarr_extensionality ide_def
by metis
ultimately show ?thesis
using f ARR_eqI ‹ide (mkarr (COD f))› null_char ide_def by auto
qed
ultimately show "codomains f ≠ {}"
using codomains_def f not_ARR_empty null_char by auto
qed
lemma arr_iff_ARR:
shows "arr f ⟷ ARR f"
using arr_def ARR_iff_has_domain ARR_iff_has_codomain by simp
text ‹
The arrows of the category are the equivalence classes of formal arrows.
›
lemma arr_char:
shows "arr f ⟷ f ≠ {} ∧ (∀t. t ∈ f ⟶ f = mkarr t)"
using arr_iff_ARR ARR_def mkarr_def by simp
lemma seq_char:
shows "seq g f ⟷ g ⋅ f ≠ null"
proof
show "g ⋅ f ≠ null ⟹ seq g f"
using comp_def null_char Comp_in_comp_ARR rep_in_ARR ARR_mkarr
Arr_rep_ARR arr_iff_ARR
by auto
show "seq g f ⟹ g ⋅ f ≠ null"
by auto
qed
lemma seq_char':
shows "seq g f ⟷ ARR f ∧ ARR g ∧ DOM g = COD f"
proof
show "ARR f ∧ ARR g ∧ DOM g = COD f ⟹ seq g f"
using comp_def null_char Comp_in_comp_ARR rep_in_ARR ARR_mkarr
Arr_rep_ARR arr_iff_ARR
by auto
have "¬ (ARR f ∧ ARR g ∧ DOM g = COD f) ⟹ g ⋅ f = null"
using comp_def null_char by auto
thus "seq g f ⟹ ARR f ∧ ARR g ∧ DOM g = COD f"
using ext by fastforce
qed
text ‹
Finally, we can show that the composition ‹comp› determines a category.
›
interpretation category comp
proof
show "⋀f. domains f ≠ {} ⟷ codomains f ≠ {}"
using ARR_iff_has_domain ARR_iff_has_codomain by simp
show 1: "⋀f g. g ⋅ f ≠ null ⟹ seq g f"
using comp_def ARR_comp null_char arr_iff_ARR by metis
fix f g h
show "seq h g ⟹ seq (h ⋅ g) f ⟹ seq g f"
using seq_char' by auto
show "seq h (g ⋅ f) ⟹ seq g f ⟹ seq h g"
using seq_char' by auto
show "seq g f ⟹ seq h g ⟹ seq (h ⋅ g) f"
using seq_char' ARR_comp arr_iff_ARR by auto
show "seq g f ⟹ seq h g ⟹ (h ⋅ g) ⋅ f = h ⋅ g ⋅ f"
using seq_char comp_assoc by auto
qed
lemma mkarr_rep [simp]:
assumes "arr f"
shows "mkarr (rep f) = f"
using assms arr_iff_ARR by simp
lemma arr_mkarr [simp]:
assumes "Arr t"
shows "arr (mkarr t)"
using assms by (simp add: ARR_mkarr arr_iff_ARR)
lemma mkarr_memb:
assumes "t ∈ f" and "arr f"
shows "Arr t" and "mkarr t = f"
using assms arr_char mkarr_extensionality by auto
lemma rep_in_arr [simp]:
assumes "arr f"
shows "rep f ∈ f"
using assms by (simp add: rep_in_ARR arr_iff_ARR)
lemma Arr_rep [simp]:
assumes "arr f"
shows "Arr (rep f)"
using assms mkarr_memb rep_in_arr by blast
lemma rep_in_Hom:
assumes "arr f"
shows "rep f ∈ Hom (DOM f) (COD f)"
using assms by simp
lemma norm_memb_eq_rep:
assumes "arr f" and "t ∈ f"
shows "❙∥t❙∥ = rep f"
using assms arr_iff_ARR norm_memb_eq_rep_ARR by auto
lemma norm_rep:
assumes "arr f"
shows "❙∥rep f❙∥ = rep f"
using assms norm_memb_eq_rep by simp
text ‹
Composition, domain, and codomain on arrows reduce to the corresponding
syntactic operations on their representative terms.
›
lemma comp_mkarr [simp]:
assumes "Arr t" and "Arr u" and "Dom t = Cod u"
shows "mkarr t ⋅ mkarr u = mkarr (t ❙⋅ u)"
using assms
by (metis (no_types, lifting) ARR_mkarr ARR_comp ARR_def Arr_in_mkarr COD_mkarr
Comp_in_comp_ARR DOM_mkarr mkarr_def)
lemma dom_char:
shows "dom f = (if arr f then mkarr (DOM f) else null)"
proof -
have "¬arr f ⟹ ?thesis"
using dom_def by (simp add: arr_def)
moreover have "arr f ⟹ ?thesis"
proof -
assume f: "arr f"
have "dom f = mkarr (DOM f)"
proof (intro dom_eqI)
have 1: "Ide (DOM f)"
using f arr_char by (metis Arr_rep Arr_implies_Ide_Dom)
hence 2: "IDE (mkarr (DOM f))"
using IDE_mkarr_Ide by metis
thus "ide (mkarr (DOM f))" using IDE_implies_ide by simp
moreover show "seq f (mkarr (DOM f))"
proof -
have "f ⋅ mkarr (DOM f) ≠ null"
using f 1 2 ARR_def DOM_mkarr IDE_implies_ARR Ide_in_Hom ARR_comp IDE_def
ARR_iff_has_codomain ARR_iff_has_domain null_char arr_def
by (metis (mono_tags, lifting) mem_Collect_eq)
thus ?thesis using seq_char by simp
qed
qed
thus ?thesis using f by simp
qed
ultimately show ?thesis by blast
qed
lemma dom_simp:
assumes "arr f"
shows "dom f = mkarr (DOM f)"
using assms dom_char by simp
lemma cod_char:
shows "cod f = (if arr f then mkarr (COD f) else null)"
proof -
have "¬arr f ⟹ ?thesis"
using cod_def by (simp add: arr_def)
moreover have "arr f ⟹ ?thesis"
proof -
assume f: "arr f"
have "cod f = mkarr (COD f)"
proof (intro cod_eqI)
have 1: "Ide (COD f)"
using f arr_char by (metis Arr_rep Arr_implies_Ide_Cod)
hence 2: "IDE (mkarr (COD f))"
using IDE_mkarr_Ide by metis
thus "ide (mkarr (COD f))" using IDE_implies_ide by simp
moreover show "seq (mkarr (COD f)) f"
proof -
have "mkarr (COD f) ⋅ f ≠ null"
using f 1 2 ARR_def DOM_mkarr IDE_implies_ARR Ide_in_Hom ARR_comp IDE_def
ARR_iff_has_codomain ARR_iff_has_domain null_char arr_def
by (metis (mono_tags, lifting) mem_Collect_eq)
thus ?thesis using seq_char by simp
qed
qed
thus ?thesis using f by simp
qed
ultimately show ?thesis by blast
qed
lemma cod_simp:
assumes "arr f"
shows "cod f = mkarr (COD f)"
using assms cod_char by simp
lemma Dom_memb:
assumes "arr f" and "t ∈ f"
shows "Dom t = DOM f"
using assms DOM_mkarr mkarr_extensionality arr_char by fastforce
lemma Cod_memb:
assumes "arr f" and "t ∈ f"
shows "Cod t = COD f"
using assms COD_mkarr mkarr_extensionality arr_char by fastforce
lemma dom_mkarr [simp]:
assumes "Arr t"
shows "dom (mkarr t) = mkarr (Dom t)"
using assms dom_char DOM_mkarr arr_mkarr by auto
lemma cod_mkarr [simp]:
assumes "Arr t"
shows "cod (mkarr t) = mkarr (Cod t)"
using assms cod_char COD_mkarr arr_mkarr by auto
lemma mkarr_in_hom:
assumes "Arr t"
shows "«mkarr t : mkarr (Dom t) → mkarr (Cod t)»"
using assms arr_mkarr dom_mkarr cod_mkarr by auto
lemma DOM_in_dom [intro]:
assumes "arr f"
shows "DOM f ∈ dom f"
using assms dom_char
by (metis Arr_in_mkarr mkarr_extensionality ideD(1) ide_dom not_arr_null null_char)
lemma COD_in_cod [intro]:
assumes "arr f"
shows "COD f ∈ cod f"
using assms cod_char
by (metis Arr_in_mkarr mkarr_extensionality ideD(1) ide_cod not_arr_null null_char)
lemma DOM_dom:
assumes "arr f"
shows "DOM (dom f) = DOM f"
using assms Arr_rep Arr_implies_Ide_Dom Ide_implies_Arr dom_char rep_mkarr Par_Arr_norm
Ide_in_Hom
by simp
lemma DOM_cod:
assumes "arr f"
shows "DOM (cod f) = COD f"
using assms Arr_rep Arr_implies_Ide_Cod Ide_implies_Arr cod_char rep_mkarr Par_Arr_norm
Ide_in_Hom
by simp
lemma memb_equiv:
assumes "arr f" and "t ∈ f" and "u ∈ f"
shows "Par t u" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
proof -
show "Par t u"
using assms Cod_memb Dom_memb mkarr_memb(1) by metis
show "❙⌊t❙⌋ = ❙⌊u❙⌋"
using assms arr_iff_ARR ARR_def by auto
qed
text ‹
Two arrows can be proved equal by showing that they are parallel and
have representatives with identical diagonalizations.
›
lemma arr_eqI:
assumes "par f g" and "t ∈ f" and "u ∈ g" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
shows "f = g"
proof -
have "Arr t ∧ Arr u" using assms mkarr_memb(1) by blast
moreover have "Dom t = Dom u ∧ Cod t = Cod u"
using assms Dom_memb Cod_memb comp_def arr_char comp_arr_dom comp_cod_arr
by (metis (full_types))
ultimately have "Par t u" by simp
thus ?thesis
using assms arr_char by (metis rep_mkarr rep_in_arr equiv_iff_eq_norm)
qed
lemma comp_char:
shows "f ⋅ g = (if seq f g then mkarr (rep f ❙⋅ rep g) else null)"
using comp_def seq_char arr_char by meson
text ‹
The mapping that takes identity terms to their equivalence classes is injective.
›
lemma mkarr_inj_on_Ide:
assumes "Ide t" and "Ide u" and "mkarr t = mkarr u"
shows "t = u"
using assms
by (metis (mono_tags, lifting) COD_mkarr Ide_in_Hom mem_Collect_eq)
lemma Comp_in_comp [intro]:
assumes "arr f" and "g ∈ hom (dom g) (dom f)" and "t ∈ f" and "u ∈ g"
shows "t ❙⋅ u ∈ f ⋅ g"
proof -
have "ARR f" using assms arr_iff_ARR by simp
moreover have "ARR g" using assms arr_iff_ARR by auto
moreover have "DOM f = COD g"
using assms dom_char cod_char mkarr_inj_on_Ide Arr_implies_Ide_Cod Arr_implies_Ide_Dom
by force
ultimately show ?thesis using assms Comp_in_comp_ARR by simp
qed
text ‹
An arrow is defined to be ``canonical'' if some (equivalently, all) its representatives
diagonalize to an identity term.
›
definition can
where "can f ≡ arr f ∧ (∃t. t ∈ f ∧ Ide ❙⌊t❙⌋)"
lemma can_def_alt:
shows "can f ⟷ arr f ∧ (∀t. t ∈ f ⟶ Ide ❙⌊t❙⌋)"
proof
assume "arr f ∧ (∀t. t ∈ f ⟶ Ide ❙⌊t❙⌋)"
thus "can f" using can_def arr_char by fastforce
next
assume f: "can f"
show "arr f ∧ (∀t. t ∈ f ⟶ Ide ❙⌊t❙⌋)"
proof -
obtain t where t: "t ∈ f ∧ Ide ❙⌊t❙⌋" using f can_def by auto
have "ARR f" using f can_def arr_char ARR_def mkarr_def by simp
hence "∀u. u ∈ f ⟶ ❙∥u❙∥ = ❙∥t❙∥" using t unique_norm by auto
hence "∀u. u ∈ f ⟶ ❙⌊t❙⌋ = ❙⌊u❙⌋"
using t by (metis ‹ARR f› equiv_iff_eq_norm arr_iff_ARR mkarr_memb(1))
hence "∀u. u ∈ f ⟶ Ide ❙⌊u❙⌋"
using t by metis
thus ?thesis using f can_def by blast
qed
qed
lemma can_implies_arr:
assumes "can f"
shows "arr f"
using assms can_def by auto
text ‹
The identities of the category are precisely the canonical endo-arrows.
›
lemma ide_char:
shows "ide f ⟷ can f ∧ dom f = cod f"
proof
assume f: "ide f"
show "can f ∧ dom f = cod f"
using f can_def arr_char dom_char cod_char IDE_def Arr_implies_Ide_Cod can_def_alt
Arr_rep IDE_mkarr_Ide
by (metis ideD(1) ideD(3))
next
assume f: "can f ∧ dom f = cod f"
show "ide f"
proof -
have "f = dom f"
proof (intro arr_eqI)
show "par f (dom f)" using f can_def by simp
show "rep f ∈ f" using f can_def by simp
show "DOM f ∈ dom f" using f can_def by auto
show "❙⌊rep f❙⌋ = ❙⌊DOM f❙⌋"
proof -
have "❙⌊rep f❙⌋ ∈ Hom ❙⌊DOM f❙⌋ ❙⌊COD f❙⌋"
using f can_def Diagonalize_in_Hom by simp
moreover have "Ide ❙⌊rep f❙⌋" using f can_def_alt rep_in_arr by simp
ultimately show ?thesis
using f can_def Ide_in_Hom by simp
qed
qed
thus ?thesis using f can_implies_arr ide_dom [of f] by auto
qed
qed
lemma ide_iff_IDE:
shows "ide a ⟷ IDE a"
using ide_char IDE_def can_def_alt arr_iff_ARR dom_char cod_char mkarr_inj_on_Ide
Arr_implies_Ide_Cod Arr_implies_Ide_Dom Arr_rep
by auto
lemma ide_mkarr_Ide:
assumes "Ide a"
shows "ide (mkarr a)"
using assms IDE_mkarr_Ide ide_iff_IDE by simp
lemma rep_dom:
assumes "arr f"
shows "rep (dom f) = ❙∥DOM f❙∥"
using assms dom_simp rep_mkarr Arr_rep Arr_implies_Ide_Dom by simp
lemma rep_cod:
assumes "arr f"
shows "rep (cod f) = ❙∥COD f❙∥"
using assms cod_simp rep_mkarr Arr_rep Arr_implies_Ide_Cod by simp
lemma rep_preserves_seq:
assumes "seq g f"
shows "Seq (rep g) (rep f)"
using assms Arr_rep dom_char cod_char mkarr_inj_on_Ide Arr_implies_Ide_Dom
Arr_implies_Ide_Cod
by auto
lemma rep_comp:
assumes "seq g f"
shows "rep (g ⋅ f) = ❙∥rep g ❙⋅ rep f❙∥"
proof -
have "rep (g ⋅ f) = rep (mkarr (rep g ❙⋅ rep f))"
using assms comp_char by metis
also have "... = ❙∥rep g ❙⋅ rep f❙∥"
using assms rep_preserves_seq rep_mkarr by simp
finally show ?thesis by blast
qed
text ‹
The equivalence classes of canonical terms are canonical arrows.
›
lemma can_mkarr_Can:
assumes "Can t"
shows "can (mkarr t)"
using assms Arr_in_mkarr Can_implies_Arr Ide_Diagonalize_Can arr_mkarr can_def by blast
lemma ide_implies_can:
assumes "ide a"
shows "can a"
using assms ide_char by blast
lemma Can_rep_can:
assumes "can f"
shows "Can (rep f)"
proof -
have "Can ❙∥rep f❙∥"
using assms can_def_alt Can_norm_iff_Ide_Diagonalize by auto
moreover have "rep f = ❙∥rep f❙∥"
using assms can_implies_arr norm_rep by simp
ultimately show ?thesis by simp
qed
text ‹
Parallel canonical arrows are identical.
›
lemma can_coherence:
assumes "par f g" and "can f" and "can g"
shows "f = g"
proof -
have "❙⌊rep f❙⌋ = ❙⌊rep g❙⌋"
proof -
have "❙⌊rep f❙⌋ = ❙⌊DOM f❙⌋"
using assms Ide_Diagonalize_Can Can_rep_can Diagonalize_in_Hom Ide_in_Hom by force
also have "... = ❙⌊DOM g❙⌋"
using assms dom_char equiv_iff_eq_norm
by (metis DOM_in_dom mkarr_memb(1) rep_mkarr arr_dom_iff_arr)
also have "... = ❙⌊rep g❙⌋"
using assms Ide_Diagonalize_Can Can_rep_can Diagonalize_in_Hom Ide_in_Hom by force
finally show ?thesis by blast
qed
hence "rep f = rep g"
using assms rep_in_arr norm_memb_eq_rep equiv_iff_eq_norm
by (metis (no_types, lifting) arr_eqI)
thus ?thesis
using assms arr_eqI [of f g] rep_in_arr [of f] rep_in_arr [of g] by metis
qed
text ‹
Canonical arrows are invertible, and their inverses can be obtained syntactically.
›
lemma inverse_arrows_can:
assumes "can f"
shows "inverse_arrows f (mkarr (Inv (DOM f❙↓) ❙⋅ ❙⌊rep f❙⌋ ❙⋅ COD f❙↓))"
proof
let ?t = "(Inv (DOM f❙↓) ❙⋅ ❙⌊rep f❙⌋ ❙⋅ COD f❙↓)"
have 1: "rep f ∈ f ∧ Arr (rep f) ∧ Can (rep f) ∧ Ide ❙⌊rep f❙⌋"
using assms can_def_alt rep_in_arr rep_in_arr(1) Can_rep_can by simp
hence 2: "❙⌊DOM f❙⌋ = ❙⌊COD f❙⌋"
using Diagonalize_in_Hom [of "rep f"] Ide_in_Hom by auto
have 3: "Can ?t"
using assms 1 2 Can_red Ide_implies_Can Diagonalize_in_Hom Inv_preserves_Can
Arr_implies_Ide_Cod Arr_implies_Ide_Dom Diag_Diagonalize
by simp
have 4: "DOM f = Cod ?t"
using assms can_def Can_red
by (simp add: Arr_implies_Ide_Dom Inv_preserves_Can(3))
have 5: "COD f = Dom ?t"
using assms can_def Can_red Arr_rep Arr_implies_Ide_Cod by simp
have 6: "antipar f (mkarr ?t)"
using assms 3 4 5 dom_char cod_char can_def cod_mkarr dom_mkarr Can_implies_Arr
by simp
show "ide (f ⋅ mkarr ?t)"
proof -
have 7: "par (f ⋅ mkarr ?t) (dom (f ⋅ mkarr ?t))"
using assms 6 by auto
moreover have "can (f ⋅ mkarr ?t)"
proof -
have 8: "Comp (rep f) ?t ∈ (f ⋅ mkarr ?t)"
using assms 1 3 4 6 can_implies_arr Arr_in_mkarr COD_mkarr Comp_in_comp_ARR
Can_implies_Arr arr_iff_ARR seq_char'
by meson
moreover have "Can (rep f ❙⋅ ?t)"
using 1 3 7 8 mkarr_memb(1) by (metis Arr.simps(4) Can.simps(4))
ultimately show ?thesis
using can_mkarr_Can 7 mkarr_memb(2) by metis
qed
moreover have "can (dom (f ⋅ mkarr ?t))"
using 7 ide_implies_can by force
ultimately have "f ⋅ mkarr ?t = dom (f ⋅ mkarr ?t)"
using can_coherence by meson
thus ?thesis
using 7 ide_dom by metis
qed
show "ide (mkarr ?t ⋅ f)"
proof -
have 7: "par (mkarr ?t ⋅ f) (cod (mkarr ?t ⋅ f))"
using assms 6 by auto
moreover have "can (mkarr ?t ⋅ f)"
proof -
have 8: "Comp ?t (rep f) ∈ mkarr ?t ⋅ f"
using assms 1 3 6 7 Arr_in_mkarr Comp_in_comp_ARR Can_implies_Arr arr_char
comp_def
by meson
moreover have "Can (?t ❙⋅ rep f)"
using 1 3 7 8 mkarr_memb(1) by (metis Arr.simps(4) Can.simps(4))
ultimately show ?thesis
using can_mkarr_Can 7 mkarr_memb(2) by metis
qed
moreover have "can (cod (mkarr ?t ⋅ f))"
using 7 ide_implies_can by force
ultimately have "mkarr ?t ⋅ f = cod (mkarr ?t ⋅ f)"
using can_coherence by meson
thus ?thesis
using 7 can_implies_arr ide_cod by metis
qed
qed
lemma inv_mkarr [simp]:
assumes "Can t"
shows "inv (mkarr t) = mkarr (Inv t)"
proof -
have t: "Can t ∧ Arr t ∧ Can (Inv t) ∧ Arr (Inv t) ∧ Ide (Dom t) ∧ Ide (Cod t)"
using assms Can_implies_Arr Arr_implies_Ide_Dom Arr_implies_Ide_Cod
Inv_preserves_Can
by simp
have "inverse_arrows (mkarr t) (mkarr (Inv t))"
proof
show "ide (mkarr t ⋅ mkarr (Inv t))"
proof -
have "mkarr (Cod t) = mkarr (Comp t (Inv t))"
using t Inv_in_Hom Ide_in_Hom Diagonalize_Inv Diag_Diagonalize Diagonalize_preserves_Can
by (intro mkarr_eqI, auto)
also have "... = mkarr t ⋅ mkarr (Inv t)"
using t comp_mkarr Inv_in_Hom by simp
finally have "mkarr (Cod t) = mkarr t ⋅ mkarr (Inv t)"
by blast
thus ?thesis using t ide_mkarr_Ide [of "Cod t"] by simp
qed
show "ide (mkarr (Inv t) ⋅ mkarr t)"
proof -
have "mkarr (Dom t) = mkarr (Inv t ❙⋅ t)"
using t Inv_in_Hom Ide_in_Hom Diagonalize_Inv Diag_Diagonalize Diagonalize_preserves_Can
by (intro mkarr_eqI, auto)
also have "... = mkarr (Inv t) ⋅ mkarr t"
using t comp_mkarr Inv_in_Hom by simp
finally have "mkarr (Dom t) = mkarr (Inv t) ⋅ mkarr t"
by blast
thus ?thesis using t ide_mkarr_Ide [of "Dom t"] by simp
qed
qed
thus ?thesis using inverse_unique by auto
qed
lemma iso_can:
assumes "can f"
shows "iso f"
using assms inverse_arrows_can by auto
text ‹
The following function produces the unique canonical arrow between two given objects,
if such an arrow exists.
›
definition mkcan
where "mkcan a b = mkarr (Inv (COD b❙↓) ❙⋅ (DOM a❙↓))"
lemma can_mkcan:
assumes "ide a" and "ide b" and "❙⌊DOM a❙⌋ = ❙⌊COD b❙⌋"
shows "can (mkcan a b)" and "«mkcan a b : a → b»"
proof -
show "can (mkcan a b)"
using assms mkcan_def Arr_rep Arr_implies_Ide_Dom Arr_implies_Ide_Cod Can_red
Inv_preserves_Can can_mkarr_Can
by simp
show "«mkcan a b : a → b»"
using assms mkcan_def Arr_rep Arr_implies_Ide_Dom Arr_implies_Ide_Cod Can_red Inv_in_Hom
dom_char [of a] cod_char [of b] mkarr_rep mkarr_in_hom can_implies_arr
by auto
qed
lemma dom_mkcan:
assumes "ide a" and "ide b" and "❙⌊DOM a❙⌋ = ❙⌊COD b❙⌋"
shows "dom (mkcan a b) = a"
using assms can_mkcan by blast
lemma cod_mkcan:
assumes "ide a" and "ide b" and "❙⌊DOM a❙⌋ = ❙⌊COD b❙⌋"
shows "cod (mkcan a b) = b"
using assms can_mkcan by blast
lemma can_coherence':
assumes "can f"
shows "mkcan (dom f) (cod f) = f"
proof -
have "Ide ❙⌊rep f❙⌋"
using assms Ide_Diagonalize_Can Can_rep_can by simp
hence "Dom ❙⌊rep f❙⌋ = Cod ❙⌊rep f❙⌋"
using Ide_in_Hom by simp
hence "❙⌊DOM f❙⌋ = ❙⌊COD f❙⌋"
using assms can_implies_arr Arr_rep Diagonalize_in_Hom by simp
moreover have "DOM f = DOM (dom f)"
using assms can_implies_arr dom_char rep_mkarr Arr_implies_Ide_Dom Ide_implies_Arr
Par_Arr_norm [of "DOM f"] Ide_in_Hom
by auto
moreover have "COD f = COD (cod f)"
using assms can_implies_arr cod_char rep_mkarr Arr_implies_Ide_Cod Ide_implies_Arr
Par_Arr_norm [of "COD f"] Ide_in_Hom
by auto
ultimately have "can (mkcan (dom f) (cod f)) ∧ par f (mkcan (dom f) (cod f))"
using assms can_implies_arr can_mkcan dom_mkcan cod_mkcan by simp
thus ?thesis using assms can_coherence by blast
qed
lemma Ide_Diagonalize_rep_ide:
assumes "ide a"
shows "Ide ❙⌊rep a❙⌋"
using assms ide_implies_can can_def_alt rep_in_arr by simp
lemma Diagonalize_DOM:
assumes "arr f"
shows "❙⌊DOM f❙⌋ = Dom ❙⌊rep f❙⌋"
using assms Diag_Diagonalize by simp
lemma Diagonalize_COD:
assumes "arr f"
shows "❙⌊COD f❙⌋ = Cod ❙⌊rep f❙⌋"
using assms Diag_Diagonalize by simp
lemma Diagonalize_rep_preserves_seq:
assumes "seq g f"
shows "Seq ❙⌊rep g❙⌋ ❙⌊rep f❙⌋"
using assms Diagonalize_DOM Diagonalize_COD Diag_implies_Arr Diag_Diagonalize(1)
rep_preserves_seq
by force
lemma Dom_Diagonalize_rep:
assumes "arr f"
shows "Dom ❙⌊rep f❙⌋ = ❙⌊rep (dom f)❙⌋"
using assms Diagonalize_rep_preserves_seq [of f "dom f"] Ide_Diagonalize_rep_ide Ide_in_Hom
by simp
lemma Cod_Diagonalize_rep:
assumes "arr f"
shows "Cod ❙⌊rep f❙⌋ = ❙⌊rep (cod f)❙⌋"
using assms Diagonalize_rep_preserves_seq [of "cod f" f] Ide_Diagonalize_rep_ide Ide_in_Hom
by simp
lemma mkarr_Diagonalize_rep:
assumes "arr f" and "Diag (DOM f)" and "Diag (COD f)"
shows "mkarr ❙⌊rep f❙⌋ = f"
proof -
have "mkarr (rep f) = mkarr ❙⌊rep f❙⌋"
using assms rep_in_Hom Diagonalize_in_Hom Diag_Diagonalize Diagonalize_Diag
by (intro mkarr_eqI, simp_all)
thus ?thesis using assms mkarr_rep by auto
qed
text ‹
We define tensor product of arrows via the constructor @{term Tensor} on terms.
›
definition tensor⇩F⇩M⇩C (infixr ‹⊗› 53)
where "f ⊗ g ≡ (if arr f ∧ arr g then mkarr (rep f ❙⊗ rep g) else null)"
lemma arr_tensor [simp]:
assumes "arr f" and "arr g"
shows "arr (f ⊗ g)"
using assms tensor⇩F⇩M⇩C_def arr_mkarr by simp
lemma rep_tensor:
assumes "arr f" and "arr g"
shows "rep (f ⊗ g) = ❙∥rep f ❙⊗ rep g❙∥"
using assms tensor⇩F⇩M⇩C_def rep_mkarr by simp
lemma Par_memb_rep:
assumes "arr f" and "t ∈ f"
shows "Par t (rep f)"
using assms mkarr_memb apply simp
using rep_in_Hom Dom_memb Cod_memb by metis
lemma Tensor_in_tensor [intro]:
assumes "arr f" and "arr g" and "t ∈ f" and "u ∈ g"
shows "t ❙⊗ u ∈ f ⊗ g"
proof -
have "equiv (t ❙⊗ u) (rep f ❙⊗ rep g)"
proof -
have 1: "Par (t ❙⊗ u) (rep f ❙⊗ rep g)"
proof -
have "Par t (rep f) ∧ Par u (rep g)" using assms Par_memb_rep by blast
thus ?thesis by simp
qed
moreover have "❙⌊t ❙⊗ u❙⌋ = ❙⌊rep f ❙⊗ rep g❙⌋"
using assms 1 equiv_iff_eq_norm rep_mkarr norm_norm mkarr_memb(2)
by (metis Arr.simps(3) Diagonalize.simps(3))
ultimately show ?thesis by simp
qed
thus ?thesis
using assms tensor⇩F⇩M⇩C_def mkarr_def by simp
qed
lemma DOM_tensor [simp]:
assumes "arr f" and "arr g"
shows "DOM (f ⊗ g) = DOM f ❙⊗ DOM g"
by (metis (no_types, lifting) DOM_mkarr Dom.simps(3) mkarr_extensionality arr_char
arr_tensor assms(1) assms(2) tensor⇩F⇩M⇩C_def)
lemma COD_tensor [simp]:
assumes "arr f" and "arr g"
shows "COD (f ⊗ g) = COD f ❙⊗ COD g"
by (metis (no_types, lifting) COD_mkarr Cod.simps(3) mkarr_extensionality arr_char
arr_tensor assms(1) assms(2) tensor⇩F⇩M⇩C_def)
lemma tensor_in_hom [simp]:
assumes "«f : a → b»" and "«g : c → d»"
shows "«f ⊗ g : a ⊗ c → b ⊗ d»"
proof -
have f: "arr f ∧ dom f = a ∧ cod f = b" using assms(1) by auto
have g: "arr g ∧ dom g = c ∧ cod g = d" using assms(2) by auto
have "dom (f ⊗ g) = dom f ⊗ dom g"
using f g arr_tensor dom_char Tensor_in_tensor [of "dom f" "dom g" "DOM f" "DOM g"]
DOM_in_dom mkarr_memb(2) DOM_tensor arr_dom_iff_arr
by metis
moreover have "cod (f ⊗ g) = cod f ⊗ cod g"
using f g arr_tensor cod_char Tensor_in_tensor [of "cod f" "cod g" "COD f" "COD g"]
COD_in_cod mkarr_memb(2) COD_tensor arr_cod_iff_arr
by metis
ultimately show ?thesis using assms arr_tensor by blast
qed
lemma dom_tensor [simp]:
assumes "arr f" and "arr g"
shows "dom (f ⊗ g) = dom f ⊗ dom g"
using assms tensor_in_hom [of f] by blast
lemma cod_tensor [simp]:
assumes "arr f" and "arr g"
shows "cod (f ⊗ g) = cod f ⊗ cod g"
using assms tensor_in_hom [of f] by blast
lemma tensor_mkarr [simp]:
assumes "Arr t" and "Arr u"
shows "mkarr t ⊗ mkarr u = mkarr (t ❙⊗ u)"
using assms by (meson Tensor_in_tensor arr_char Arr_in_mkarr arr_mkarr arr_tensor)
lemma tensor_preserves_ide:
assumes "ide a" and "ide b"
shows "ide (a ⊗ b)"
proof -
have "can (a ⊗ b)"
using assms tensor⇩F⇩M⇩C_def Can_rep_can ide_implies_can can_mkarr_Can by simp
moreover have "dom (a ⊗ b) = cod (a ⊗ b)"
using assms tensor_in_hom by simp
ultimately show ?thesis using ide_char by metis
qed
lemma tensor_preserves_can:
assumes "can f" and "can g"
shows "can (f ⊗ g)"
using assms can_implies_arr Can_rep_can tensor⇩F⇩M⇩C_def can_mkarr_Can by simp
lemma comp_preserves_can:
assumes "can f" and "can g" and "dom f = cod g"
shows "can (f ⋅ g)"
proof -
have 1: "ARR f ∧ ARR g ∧ DOM f = COD g"
using assms can_implies_arr arr_iff_ARR Arr_implies_Ide_Cod Arr_implies_Ide_Dom
mkarr_inj_on_Ide cod_char dom_char
by simp
hence "Can (rep f ❙⋅ rep g)"
using assms can_implies_arr Can_rep_can by force
thus ?thesis
using assms 1 can_implies_arr comp_char can_mkarr_Can seq_char' by simp
qed
text ‹
The remaining structure required of a monoidal category is also defined syntactically.
›
definition unity⇩F⇩M⇩C :: "'c arr" (‹ℐ›)
where "ℐ = mkarr ❙ℐ"
definition lunit⇩F⇩M⇩C :: "'c arr ⇒ 'c arr" (‹𝗅[_]›)
where "𝗅[a] = mkarr ❙𝗅❙[rep a❙]"
definition runit⇩F⇩M⇩C :: "'c arr ⇒ 'c arr" (‹𝗋[_]›)
where "𝗋[a] = mkarr ❙𝗋❙[rep a❙]"
definition assoc⇩F⇩M⇩C :: "'c arr ⇒ 'c arr ⇒ 'c arr ⇒ 'c arr" (‹𝖺[_, _, _]›)
where "𝖺[a, b, c] = mkarr ❙𝖺❙[rep a, rep b, rep c❙]"
lemma can_lunit:
assumes "ide a"
shows "can 𝗅[a]"
using assms lunit⇩F⇩M⇩C_def can_mkarr_Can
by (simp add: Can_rep_can ide_implies_can)
lemma lunit_in_hom:
assumes "ide a"
shows "«𝗅[a] : ℐ ⊗ a → a»"
proof -
have "dom 𝗅[a] = ℐ ⊗ a"
using assms lunit⇩F⇩M⇩C_def unity⇩F⇩M⇩C_def Ide_implies_Arr dom_mkarr dom_char tensor_mkarr
Arr_rep
by (metis Arr.simps(2) Arr.simps(5) Arr_implies_Ide_Dom Dom.simps(5)
ideD(1) ideD(2))
moreover have "cod 𝗅[a] = a"
using assms lunit⇩F⇩M⇩C_def rep_in_arr(1) cod_mkarr cod_char ideD(3) by auto
ultimately show ?thesis
using assms arr_cod_iff_arr by (intro in_homI, fastforce)
qed
lemma arr_lunit [simp]:
assumes "ide a"
shows "arr 𝗅[a]"
using assms can_lunit can_implies_arr by simp
lemma dom_lunit [simp]:
assumes "ide a"
shows "dom 𝗅[a] = ℐ ⊗ a"
using assms lunit_in_hom by auto
lemma cod_lunit [simp]:
assumes "ide a"
shows "cod 𝗅[a] = a"
using assms lunit_in_hom by auto
lemma can_runit:
assumes "ide a"
shows "can 𝗋[a]"
using assms runit⇩F⇩M⇩C_def can_mkarr_Can
by (simp add: Can_rep_can ide_implies_can)
lemma runit_in_hom [simp]:
assumes "ide a"
shows "«𝗋[a] : a ⊗ ℐ → a»"
proof -
have "dom 𝗋[a] = a ⊗ ℐ"
using assms Arr_rep Arr.simps(2) Arr.simps(7) Arr_implies_Ide_Dom Dom.simps(7)
Ide_implies_Arr dom_mkarr dom_char ideD(1) ideD(2) runit⇩F⇩M⇩C_def tensor_mkarr
unity⇩F⇩M⇩C_def
by metis
moreover have "cod 𝗋[a] = a"
using assms runit⇩F⇩M⇩C_def rep_in_arr(1) cod_mkarr cod_char ideD(3) by auto
ultimately show ?thesis
using assms arr_cod_iff_arr by (intro in_homI, fastforce)
qed
lemma arr_runit [simp]:
assumes "ide a"
shows "arr 𝗋[a]"
using assms can_runit can_implies_arr by simp
lemma dom_runit [simp]:
assumes "ide a"
shows "dom 𝗋[a] = a ⊗ ℐ"
using assms runit_in_hom by blast
lemma cod_runit [simp]:
assumes "ide a"
shows "cod 𝗋[a] = a"
using assms runit_in_hom by blast
lemma can_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "can 𝖺[a, b, c]"
using assms assoc⇩F⇩M⇩C_def can_mkarr_Can
by (simp add: Can_rep_can ide_implies_can)
lemma assoc_in_hom:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ b ⊗ c»"
proof -
have "dom 𝖺[a, b, c] = (a ⊗ b) ⊗ c"
proof -
have "dom 𝖺[a, b, c] = mkarr (Dom ❙𝖺❙[rep a, rep b, rep c❙])"
using assms assoc⇩F⇩M⇩C_def rep_in_arr(1) by simp
also have "... = mkarr ((DOM a ❙⊗ DOM b) ❙⊗ DOM c)"
by simp
also have "... = (a ⊗ b) ⊗ c"
by (metis mkarr_extensionality arr_tensor assms dom_char
ideD(1) ideD(2) not_arr_null null_char tensor_mkarr)
finally show ?thesis by blast
qed
moreover have "cod 𝖺[a, b, c] = a ⊗ b ⊗ c"
proof -
have "cod 𝖺[a, b, c] = mkarr (Cod ❙𝖺❙[rep a, rep b, rep c❙])"
using assms assoc⇩F⇩M⇩C_def rep_in_arr(1) by simp
also have "... = mkarr (COD a ❙⊗ COD b ❙⊗ COD c)"
by simp
also have "... = a ⊗ b ⊗ c"
by (metis mkarr_extensionality arr_tensor assms(1) assms(2) assms(3) cod_char
ideD(1) ideD(3) not_arr_null null_char tensor_mkarr)
finally show ?thesis by blast
qed
moreover have "arr 𝖺[a, b, c]"
using assms assoc⇩F⇩M⇩C_def rep_in_arr(1) arr_mkarr by simp
ultimately show ?thesis by auto
qed
lemma arr_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺[a, b, c]"
using assms can_assoc can_implies_arr by simp
lemma dom_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "dom 𝖺[a, b, c] = (a ⊗ b) ⊗ c"
using assms assoc_in_hom by blast
lemma cod_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "cod 𝖺[a, b, c] = a ⊗ b ⊗ c"
using assms assoc_in_hom by blast
lemma ide_unity [simp]:
shows "ide ℐ"
using unity⇩F⇩M⇩C_def Arr.simps(2) Dom.simps(2) arr_mkarr dom_mkarr ide_dom
by metis
lemma Unity_in_unity [simp]:
shows "❙ℐ ∈ ℐ"
using unity⇩F⇩M⇩C_def Arr_in_mkarr by simp
lemma rep_unity [simp]:
shows "rep ℐ = ❙∥❙ℐ❙∥"
using unity⇩F⇩M⇩C_def rep_mkarr by simp
lemma Lunit_in_lunit [intro]:
assumes "arr f" and "t ∈ f"
shows "❙𝗅❙[t❙] ∈ 𝗅[f]"
proof -
have "Arr t ∧ Arr (rep f) ∧ Dom t = DOM f ∧ Cod t = COD f ∧ ❙⌊t❙⌋ = ❙⌊rep f❙⌋"
using assms
by (metis mkarr_memb(1) mkarr_memb(2) rep_mkarr rep_in_arr(1) equiv_iff_eq_norm
norm_rep)
thus ?thesis
by (simp add: mkarr_def lunit⇩F⇩M⇩C_def)
qed
lemma Runit_in_runit [intro]:
assumes "arr f" and "t ∈ f"
shows "❙𝗋❙[t❙] ∈ 𝗋[f]"
proof -
have "Arr t ∧ Arr (rep f) ∧ Dom t = DOM f ∧ Cod t = COD f ∧ ❙⌊t❙⌋ = ❙⌊rep f❙⌋"
using assms
by (metis mkarr_memb(1) mkarr_memb(2) rep_mkarr rep_in_arr(1) equiv_iff_eq_norm
norm_rep)
thus ?thesis
by (simp add: mkarr_def runit⇩F⇩M⇩C_def)
qed
lemma Assoc_in_assoc [intro]:
assumes "arr f" and "arr g" and "arr h"
and "t ∈ f" and "u ∈ g" and "v ∈ h"
shows "❙𝖺❙[t, u, v❙] ∈ 𝖺[f, g, h]"
proof -
have "Arr t ∧ Arr (rep f) ∧ Dom t = DOM f ∧ Cod t = COD f ∧ ❙⌊t❙⌋ = ❙⌊rep f❙⌋"
using assms
by (metis mkarr_memb(1) rep_mkarr rep_in_arr(1) equiv_iff_eq_norm mkarr_memb(2)
norm_rep)
moreover have "Arr u ∧ Arr (rep g) ∧ Dom u = DOM g ∧ Cod u = COD g ∧
❙⌊u❙⌋ = ❙⌊rep g❙⌋"
using assms
by (metis mkarr_memb(1) rep_mkarr rep_in_arr(1) equiv_iff_eq_norm mkarr_memb(2)
norm_rep)
moreover have "Arr v ∧ Arr (rep h) ∧ Dom v = DOM h ∧ Cod v = COD h ∧
❙⌊v❙⌋ = ❙⌊rep h❙⌋"
using assms
by (metis mkarr_memb(1) rep_mkarr rep_in_arr(1) equiv_iff_eq_norm mkarr_memb(2)
norm_rep)
ultimately show ?thesis
using assoc⇩F⇩M⇩C_def mkarr_def by simp
qed
text ‹
At last, we can show that we've constructed a monoidal category.
›
interpretation EMC: elementary_monoidal_category
comp tensor⇩F⇩M⇩C unity⇩F⇩M⇩C lunit⇩F⇩M⇩C runit⇩F⇩M⇩C assoc⇩F⇩M⇩C
proof
show "ide ℐ" using ide_unity by auto
show "⋀a. ide a ⟹ «𝗅[a] : ℐ ⊗ a → a»" by auto
show "⋀a. ide a ⟹ «𝗋[a] : a ⊗ ℐ → a»" by auto
show "⋀a. ide a ⟹ iso 𝗅[a]" using can_lunit iso_can by auto
show "⋀a. ide a ⟹ iso 𝗋[a]" using can_runit iso_can by auto
show "⋀a b c. ⟦ ide a; ide b; ide c ⟧ ⟹ «𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ b ⊗ c»" by auto
show "⋀a b c. ⟦ ide a; ide b; ide c ⟧ ⟹ iso 𝖺[a, b, c]" using can_assoc iso_can by auto
show "⋀a b. ⟦ ide a; ide b ⟧ ⟹ ide (a ⊗ b)" using tensor_preserves_ide by auto
fix f a b g c d
show "⟦ «f : a → b»; «g : c → d» ⟧ ⟹ «f ⊗ g : a ⊗ c → b ⊗ d»"
using tensor_in_hom by auto
next
text ‹Naturality of left unitor.›
fix f
assume f: "arr f"
show "𝗅[cod f] ⋅ (ℐ ⊗ f) = f ⋅ 𝗅[dom f]"
proof (intro arr_eqI)
show "par (𝗅[cod f] ⋅ (ℐ ⊗ f)) (f ⋅ 𝗅[dom f])"
using f by simp
show "❙𝗅❙[COD f❙] ❙⋅ (❙ℐ ❙⊗ rep f) ∈ 𝗅[cod f] ⋅ (ℐ ⊗ f)"
using f by fastforce
show "rep f ❙⋅ ❙𝗅❙[DOM f❙] ∈ f ⋅ 𝗅[dom f]"
using f by fastforce
show "❙⌊❙𝗅❙[COD f❙] ❙⋅ (❙ℐ ❙⊗ rep f)❙⌋ = ❙⌊rep f ❙⋅ ❙𝗅❙[DOM f❙]❙⌋"
using f by (simp add: Diag_Diagonalize(1) Diagonalize_DOM Diagonalize_COD)
qed
text ‹Naturality of right unitor.›
show "𝗋[cod f] ⋅ (f ⊗ ℐ) = f ⋅ 𝗋[dom f]"
proof (intro arr_eqI)
show "par (𝗋[cod f] ⋅ (f ⊗ ℐ)) (f ⋅ 𝗋[dom f])"
using f by simp
show "❙𝗋❙[COD f❙] ❙⋅ (rep f ❙⊗ ❙ℐ) ∈ 𝗋[cod f] ⋅ (f ⊗ ℐ)"
using f by fastforce
show "rep f ❙⋅ ❙𝗋❙[DOM f❙] ∈ f ⋅ 𝗋[dom f]"
using f by fastforce
show "❙⌊❙𝗋❙[COD f❙] ❙⋅ (rep f ❙⊗ ❙ℐ)❙⌋ = ❙⌊rep f ❙⋅ ❙𝗋❙[DOM f❙]❙⌋"
using f by (simp add: Diag_Diagonalize(1) Diagonalize_DOM Diagonalize_COD)
qed
next
text ‹Naturality of associator.›
fix f0 :: "'c arr" and f1 f2
assume f0: "arr f0" and f1: "arr f1" and f2: "arr f2"
show "𝖺[cod f0, cod f1, cod f2] ⋅ ((f0 ⊗ f1) ⊗ f2)
= (f0 ⊗ f1 ⊗ f2) ⋅ 𝖺[dom f0, dom f1, dom f2]"
proof (intro arr_eqI)
show 1: "par (𝖺[cod f0, cod f1, cod f2] ⋅ ((f0 ⊗ f1) ⊗ f2))
((f0 ⊗ f1 ⊗ f2) ⋅ 𝖺[dom f0, dom f1, dom f2])"
using f0 f1 f2 by force
show "❙𝖺❙[rep (cod f0), rep (cod f1), rep (cod f2)❙] ❙⋅ ((rep f0 ❙⊗ rep f1) ❙⊗ rep f2)
∈ 𝖺[cod f0, cod f1, cod f2] ⋅ ((f0 ⊗ f1) ⊗ f2)"
using f0 f1 f2 by fastforce
show "(rep f0 ❙⊗ rep f1 ❙⊗ rep f2) ❙⋅ ❙𝖺❙[rep (dom f0), rep (dom f1), rep (dom f2)❙]
∈ (f0 ⊗ f1 ⊗ f2) ⋅ 𝖺[dom f0, dom f1, dom f2]"
using f0 f1 f2 by fastforce
show "❙⌊❙𝖺❙[rep (cod f0), rep (cod f1), rep (cod f2)❙] ❙⋅ ((rep f0 ❙⊗ rep f1) ❙⊗ rep f2)❙⌋
= ❙⌊(rep f0 ❙⊗ rep f1 ❙⊗ rep f2) ❙⋅ ❙𝖺❙[rep (dom f0), rep (dom f1), rep (dom f2)❙]❙⌋"
proof -
have "❙⌊❙𝖺❙[rep (cod f0), rep (cod f1), rep (cod f2)❙] ❙⋅ ((rep f0 ❙⊗ rep f1) ❙⊗ rep f2)❙⌋
= ❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f2❙⌋"
proof -
have b0: "❙⌊rep (cod f0)❙⌋ = Cod ❙⌊rep f0❙⌋"
using f0 Cod_Diagonalize_rep by simp
have b1: "❙⌊rep (cod f1)❙⌋ = Cod ❙⌊rep f1❙⌋"
using f1 Cod_Diagonalize_rep by simp
have b2: "❙⌊rep (cod f2)❙⌋ = Cod ❙⌊rep f2❙⌋"
using f2 Cod_Diagonalize_rep by simp
have "❙⌊❙𝖺❙[rep (cod f0), rep (cod f1), rep (cod f2)❙] ❙⋅ ((rep f0 ❙⊗ rep f1) ❙⊗ rep f2)❙⌋
= (❙⌊rep (cod f0)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep (cod f1)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep (cod f2)❙⌋) ❙⌊❙⋅❙⌋
(❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f2❙⌋)"
using f0 f1 f2 using Diag_Diagonalize(1) TensorDiag_assoc by auto
also have "... = ❙⌊rep (cod f0)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋
❙⌊rep (cod f1)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep (cod f2)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f2❙⌋"
proof -
have "Seq ❙⌊rep (cod f0)❙⌋ ❙⌊rep f0❙⌋ ∧ Seq ❙⌊rep (cod f1)❙⌋ ❙⌊rep f1❙⌋ ∧
Seq ❙⌊rep (cod f2)❙⌋ ❙⌊rep f2❙⌋"
using f0 f1 f2 rep_in_Hom Diagonalize_in_Hom Dom_Diagonalize_rep Cod_Diagonalize_rep
by auto
thus ?thesis
using f0 f1 f2 b0 b1 b2 TensorDiag_in_Hom TensorDiag_preserves_Diag
Diag_Diagonalize Arr_implies_Ide_Dom Arr_implies_Ide_Cod
CompDiag_TensorDiag
by simp
qed
also have "... = ❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f2❙⌋"
proof -
have "❙⌊rep (cod f0)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f0❙⌋ = ❙⌊rep f0❙⌋"
using f0 b0 CompDiag_Cod_Diag [of "❙⌊rep f0❙⌋"] Diag_Diagonalize
by simp
moreover have "❙⌊rep (cod f1)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f1❙⌋ = ❙⌊rep f1❙⌋"
using f1 b1 CompDiag_Cod_Diag [of "❙⌊rep f1❙⌋"] Diag_Diagonalize
by simp
moreover have "❙⌊rep (cod f2)❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f2❙⌋ = ❙⌊rep f2❙⌋"
using f2 b2 CompDiag_Cod_Diag [of "❙⌊rep f2❙⌋"] Diag_Diagonalize
by simp
ultimately show ?thesis by argo
qed
finally show ?thesis by blast
qed
also have "... = ❙⌊(rep f0 ❙⊗ rep f1 ❙⊗ rep f2) ❙⋅
❙𝖺❙[rep (dom f0), rep (dom f1), rep (dom f2)❙]❙⌋"
proof -
have a0: "❙⌊rep (dom f0)❙⌋ = Dom ❙⌊rep f0❙⌋"
using f0 Dom_Diagonalize_rep by simp
have a1: "❙⌊rep (dom f1)❙⌋ = Dom ❙⌊rep f1❙⌋"
using f1 Dom_Diagonalize_rep by simp
have a2: "❙⌊rep (dom f2)❙⌋ = Dom ❙⌊rep f2❙⌋"
using f2 Dom_Diagonalize_rep by simp
have "❙⌊(rep f0 ❙⊗ rep f1 ❙⊗ rep f2) ❙⋅ ❙𝖺❙[rep (dom f0), rep (dom f1), rep (dom f2)❙]❙⌋
= (❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f2❙⌋) ❙⌊❙⋅❙⌋
(❙⌊rep (dom f0)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep (dom f1)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep (dom f2)❙⌋)"
using f0 f1 f2 using Diag_Diagonalize(1) TensorDiag_assoc by auto
also have "... = ❙⌊rep f0❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f0)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f1)❙⌋ ❙⌊❙⊗❙⌋
❙⌊rep f2❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f2)❙⌋"
proof -
have "Seq ❙⌊rep f0❙⌋ ❙⌊rep (dom f0)❙⌋ ∧ Seq ❙⌊rep f1❙⌋ ❙⌊rep (dom f1)❙⌋ ∧
Seq ❙⌊rep f2❙⌋ ❙⌊rep (dom f2)❙⌋"
using f0 f1 f2 rep_in_Hom Diagonalize_in_Hom Dom_Diagonalize_rep Cod_Diagonalize_rep
by auto
thus ?thesis
using f0 f1 f2 a0 a1 a2 TensorDiag_in_Hom TensorDiag_preserves_Diag
Diag_Diagonalize Arr_implies_Ide_Dom Arr_implies_Ide_Cod
CompDiag_TensorDiag
by force
qed
also have "... = ❙⌊rep f0❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f1❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f2❙⌋"
proof -
have "❙⌊rep f0❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f0)❙⌋ = ❙⌊rep f0❙⌋"
using f0 a0 CompDiag_Diag_Dom [of "Diagonalize (rep f0)"] Diag_Diagonalize
by simp
moreover have "❙⌊rep f1❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f1)❙⌋ = ❙⌊rep f1❙⌋"
using f1 a1 CompDiag_Diag_Dom [of "Diagonalize (rep f1)"] Diag_Diagonalize
by simp
moreover have "❙⌊rep f2❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep (dom f2)❙⌋ = ❙⌊rep f2❙⌋"
using f2 a2 CompDiag_Diag_Dom [of "Diagonalize (rep f2)"] Diag_Diagonalize
by simp
ultimately show ?thesis by argo
qed
finally show ?thesis by argo
qed
finally show ?thesis by blast
qed
qed
next
text ‹Tensor preserves composition (interchange).›
fix f g f' g'
show "⟦ seq g f; seq g' f' ⟧ ⟹ (g ⊗ g') ⋅ (f ⊗ f') = g ⋅ f ⊗ g' ⋅ f'"
proof -
assume gf: "seq g f"
assume gf': "seq g' f'"
show ?thesis
proof (intro arr_eqI)
show "par ((g ⊗ g') ⋅ (f ⊗ f')) (g ⋅ f ⊗ g' ⋅ f')"
using gf gf' by fastforce
show "(rep g ❙⊗ rep g') ❙⋅ (rep f ❙⊗ rep f') ∈ (g ⊗ g') ⋅ (f ⊗ f')"
using gf gf' by force
show "rep g ❙⋅ rep f ❙⊗ rep g' ❙⋅ rep f' ∈ g ⋅ f ⊗ g' ⋅ f'"
using gf gf'
by (meson Comp_in_comp_ARR Tensor_in_tensor rep_in_arr seqE seq_char')
show "❙⌊(rep g ❙⊗ rep g') ❙⋅ (rep f ❙⊗ rep f')❙⌋ = ❙⌊rep g ❙⋅ rep f ❙⊗ rep g' ❙⋅ rep f'❙⌋"
proof -
have "❙⌊(rep g ❙⊗ rep g') ❙⋅ (rep f ❙⊗ rep f')❙⌋
= (❙⌊rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep g'❙⌋) ❙⌊❙⋅❙⌋ (❙⌊rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep f'❙⌋)"
by auto
also have "... = ❙⌊rep g❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊rep g'❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f'❙⌋"
using gf gf' Arr_rep Diagonalize_rep_preserves_seq
CompDiag_TensorDiag [of "❙⌊rep g❙⌋" " ❙⌊rep g'❙⌋" "❙⌊rep f❙⌋" "❙⌊rep f'❙⌋"]
Diag_Diagonalize Diagonalize_DOM Diagonalize_COD
by force
also have "... = ❙⌊rep g ❙⋅ rep f ❙⊗ rep g' ❙⋅ rep f'❙⌋"
by auto
finally show ?thesis by blast
qed
qed
qed
next
text ‹The triangle.›
fix a b
assume a: "ide a"
assume b: "ide b"
show "(a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b] = 𝗋[a] ⊗ b"
proof -
have "par ((a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b]) (𝗋[a] ⊗ b)"
using a b by simp
moreover have "can ((a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b])"
using a b ide_implies_can comp_preserves_can tensor_preserves_can can_assoc can_lunit
by simp
moreover have "can (𝗋[a] ⊗ b)"
using a b ide_implies_can can_runit tensor_preserves_can by simp
ultimately show ?thesis using can_coherence by blast
qed
next
text ‹The pentagon.›
fix a b c d
assume a: "ide a"
assume b: "ide b"
assume c: "ide c"
assume d: "ide d"
show "(a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)
= 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof -
let ?LHS = "(a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)"
let ?RHS = "𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
have "par ?LHS ?RHS"
using a b c d can_assoc tensor_preserves_ide by auto
moreover have "can ?LHS"
using a b c d ide_implies_can comp_preserves_can tensor_preserves_can can_assoc
tensor_preserves_ide
by simp
moreover have "can ?RHS"
using a b c d comp_preserves_can tensor_preserves_can can_assoc tensor_in_hom
tensor_preserves_ide
by simp
ultimately show ?thesis using can_coherence by blast
qed
qed
lemma is_elementary_monoidal_category:
shows "elementary_monoidal_category
comp tensor⇩F⇩M⇩C unity⇩F⇩M⇩C lunit⇩F⇩M⇩C runit⇩F⇩M⇩C assoc⇩F⇩M⇩C"
..
abbreviation T⇩F⇩M⇩C where "T⇩F⇩M⇩C ≡ EMC.T"
abbreviation α⇩F⇩M⇩C where "α⇩F⇩M⇩C ≡ EMC.α"
abbreviation ι⇩F⇩M⇩C where "ι⇩F⇩M⇩C ≡ EMC.ι"
interpretation MC: monoidal_category comp T⇩F⇩M⇩C α⇩F⇩M⇩C ι⇩F⇩M⇩C
using EMC.induces_monoidal_category by auto
lemma induces_monoidal_category:
shows "monoidal_category comp T⇩F⇩M⇩C α⇩F⇩M⇩C ι⇩F⇩M⇩C"
..
end
sublocale free_monoidal_category ⊆
elementary_monoidal_category
comp tensor⇩F⇩M⇩C unity⇩F⇩M⇩C lunit⇩F⇩M⇩C runit⇩F⇩M⇩C assoc⇩F⇩M⇩C
using is_elementary_monoidal_category by auto
sublocale free_monoidal_category ⊆ monoidal_category comp T⇩F⇩M⇩C α⇩F⇩M⇩C ι⇩F⇩M⇩C
using induces_monoidal_category by auto
section "Proof of Freeness"
text ‹
Now we proceed on to establish the freeness of ‹ℱC›: each functor
from @{term C} to a monoidal category @{term D} extends uniquely
to a strict monoidal functor from ‹ℱC› to D.
›
context free_monoidal_category
begin
lemma rep_lunit:
assumes "ide a"
shows "rep 𝗅[a] = ❙∥❙𝗅❙[rep a❙]❙∥"
using assms Lunit_in_lunit [of a "rep a"] rep_in_arr norm_memb_eq_rep [of "𝗅[a]"]
by simp
lemma rep_runit:
assumes "ide a"
shows "rep 𝗋[a] = ❙∥❙𝗋❙[rep a❙]❙∥"
using assms Runit_in_runit [of a "rep a"] rep_in_arr norm_memb_eq_rep [of "𝗋[a]"]
by simp
lemma rep_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "rep 𝖺[a, b, c] = ❙∥❙𝖺❙[rep a, rep b, rep c❙]❙∥"
using assms Assoc_in_assoc [of a b c "rep a" "rep b" "rep c"] rep_in_arr
norm_memb_eq_rep [of "𝖺[a, b, c]"]
by simp
lemma mkarr_Unity:
shows "mkarr ❙ℐ = ℐ"
using unity⇩F⇩M⇩C_def by simp
text ‹
The unitors and associator were given syntactic definitions in terms of
corresponding terms, but these were only for the special case of identity
arguments (\emph{i.e.}~the components of the natural transformations).
We need to show that @{term mkarr} gives the correct result for \emph{all}
terms.
›
lemma mkarr_Lunit:
assumes "Arr t"
shows "mkarr ❙𝗅❙[t❙] = 𝔩 (mkarr t)"
proof -
have "mkarr ❙𝗅❙[t❙] = mkarr (t ❙⋅ ❙𝗅❙[❙∥Dom t❙∥❙])"
using assms Arr_implies_Ide_Dom Ide_in_Hom Diagonalize_preserves_Ide
Diag_Diagonalize Par_Arr_norm
by (intro mkarr_eqI) simp_all
also have "... = mkarr t ⋅ mkarr ❙𝗅❙[❙∥Dom t❙∥❙]"
using assms Arr_implies_Ide_Dom Par_Arr_norm Ide_in_Hom by simp
also have "... = mkarr t ⋅ 𝗅[dom (mkarr t)]"
proof -
have "arr 𝗅[mkarr (Dom t)]"
using assms Arr_implies_Ide_Dom ide_mkarr_Ide by simp
moreover have "❙𝗅❙[❙∥Dom t❙∥❙] ∈ 𝗅[mkarr (Dom t)]"
using assms Arr_implies_Ide_Dom Lunit_in_lunit rep_mkarr
rep_in_arr [of "mkarr (Dom t)"]
by simp
ultimately show ?thesis
using assms mkarr_memb(2) by simp
qed
also have "... = 𝔩 (mkarr t)"
using assms Arr_implies_Ide_Dom ide_mkarr_Ide lunit_agreement by simp
finally show ?thesis by blast
qed
lemma mkarr_Lunit':
assumes "Arr t"
shows "mkarr ❙𝗅⇧-⇧1❙[t❙] = 𝔩' (mkarr t)"
proof -
have "mkarr ❙𝗅⇧-⇧1❙[t❙] = mkarr (❙𝗅⇧-⇧1❙[❙∥Cod t❙∥❙] ❙⋅ t)"
using assms Arr_implies_Ide_Cod Ide_in_Hom Diagonalize_preserves_Ide
Diag_Diagonalize Par_Arr_norm
by (intro mkarr_eqI) simp_all
also have "... = mkarr ❙𝗅⇧-⇧1❙[❙∥Cod t❙∥❙] ⋅ mkarr t"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm by simp
also have "... = mkarr (Inv ❙𝗅❙[❙∥Cod t❙∥❙]) ⋅ mkarr t"
proof -
have "mkarr ❙𝗅⇧-⇧1❙[❙∥Cod t❙∥❙] = mkarr (Inv ❙𝗅❙[❙∥Cod t❙∥❙])"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm Inv_in_Hom
Ide_implies_Can norm_preserves_Can Diagonalize_Inv Diagonalize_preserves_Ide
by (intro mkarr_eqI, simp_all)
thus ?thesis by argo
qed
also have "... = 𝔩' (cod (mkarr t)) ⋅ mkarr t"
proof -
have "mkarr (Inv ❙𝗅❙[❙∥Cod t❙∥❙]) ⋅ mkarr t = lunit' (cod (mkarr t)) ⋅ mkarr t"
using assms Arr_implies_Ide_Cod rep_mkarr Par_Arr_norm inv_mkarr
norm_preserves_Can Ide_implies_Can lunit_agreement 𝔩'_ide_simp
Can_implies_Arr arr_mkarr cod_mkarr ide_cod lunit⇩F⇩M⇩C_def
by (metis (no_types, lifting) Can.simps(5))
also have "... = 𝔩' (cod (mkarr t)) ⋅ mkarr t"
using assms 𝔩'_ide_simp arr_mkarr ide_cod by presburger
finally show ?thesis by blast
qed
also have "... = 𝔩' (mkarr t)"
using assms 𝔩'.is_natural_2 [of "mkarr t"] by simp
finally show ?thesis by blast
qed
lemma mkarr_Runit:
assumes "Arr t"
shows "mkarr ❙𝗋❙[t❙] = ρ (mkarr t)"
proof -
have "mkarr ❙𝗋❙[t❙] = mkarr (t ❙⋅ ❙𝗋❙[❙∥Dom t❙∥❙])"
proof -
have "¬ Diag (Dom t ❙⊗ ❙ℐ)" by (cases "Dom t") simp_all
thus ?thesis
using assms Par_Arr_norm Arr_implies_Ide_Dom Ide_in_Hom Diag_Diagonalize
Diagonalize_preserves_Ide
by (intro mkarr_eqI) simp_all
qed
also have "... = mkarr t ⋅ mkarr ❙𝗋❙[❙∥Dom t❙∥❙]"
using assms Arr_implies_Ide_Dom Par_Arr_norm Ide_in_Hom by simp
also have "... = mkarr t ⋅ 𝗋[dom (mkarr t)]"
proof -
have "arr 𝗋[mkarr (Dom t)]"
using assms Arr_implies_Ide_Dom ide_mkarr_Ide by simp
moreover have "❙𝗋❙[❙∥Dom t❙∥❙] ∈ 𝗋[mkarr (Dom t)]"
using assms Arr_implies_Ide_Dom Runit_in_runit rep_mkarr
rep_in_arr [of "mkarr (Dom t)"]
by simp
moreover have "mkarr (Dom t) = mkarr ❙∥Dom t❙∥"
using assms mkarr_rep rep_mkarr arr_mkarr Ide_implies_Arr Arr_implies_Ide_Dom
by metis
ultimately show ?thesis
using assms mkarr_memb(2) by simp
qed
also have "... = ρ (mkarr t)"
using assms Arr_implies_Ide_Dom ide_mkarr_Ide runit_agreement by simp
finally show ?thesis by blast
qed
lemma mkarr_Runit':
assumes "Arr t"
shows "mkarr ❙𝗋⇧-⇧1❙[t❙] = ρ' (mkarr t)"
proof -
have "mkarr ❙𝗋⇧-⇧1❙[t❙] = mkarr (❙𝗋⇧-⇧1❙[❙∥Cod t❙∥❙] ❙⋅ t)"
proof -
have "¬ Diag (Cod t ❙⊗ ❙ℐ)" by (cases "Cod t") simp_all
thus ?thesis
using assms Par_Arr_norm Arr_implies_Ide_Cod Ide_in_Hom
Diagonalize_preserves_Ide Diag_Diagonalize
by (intro mkarr_eqI) simp_all
qed
also have "... = mkarr ❙𝗋⇧-⇧1❙[❙∥Cod t❙∥❙] ⋅ mkarr t"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm by simp
also have "... = mkarr (Inv ❙𝗋❙[❙∥Cod t❙∥❙]) ⋅ mkarr t"
proof -
have "mkarr (Runit' (norm (Cod t))) = mkarr (Inv (Runit (norm (Cod t))))"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm Inv_in_Hom
Ide_implies_Can norm_preserves_Can Diagonalize_Inv Diagonalize_preserves_Ide
by (intro mkarr_eqI) simp_all
thus ?thesis by argo
qed
also have "... = ρ' (cod (mkarr t)) ⋅ mkarr t"
proof -
have "mkarr (Inv ❙𝗋❙[❙∥Cod t❙∥❙]) ⋅ mkarr t = runit' (cod (mkarr t)) ⋅ mkarr t"
using assms Arr_implies_Ide_Cod rep_mkarr inv_mkarr norm_preserves_Can
Ide_implies_Can runit_agreement Can_implies_Arr arr_mkarr cod_mkarr
ide_cod runit⇩F⇩M⇩C_def
by (metis (no_types, lifting) Can.simps(7))
also have "... = ρ' (cod (mkarr t)) ⋅ mkarr t"
proof -
have "runit' (cod (mkarr t)) = ρ' (cod (mkarr t))"
using assms ρ'_ide_simp arr_mkarr ide_cod by blast
thus ?thesis by argo
qed
finally show ?thesis by blast
qed
also have "... = ρ' (mkarr t)"
using assms ρ'.is_natural_2 [of "mkarr t"] by simp
finally show ?thesis by blast
qed
lemma mkarr_Assoc:
assumes "Arr t" and "Arr u" and "Arr v"
shows "mkarr ❙𝖺❙[t, u, v❙] = α (mkarr t, mkarr u, mkarr v)"
proof -
have "mkarr ❙𝖺❙[t, u, v❙] = mkarr ((t ❙⊗ u ❙⊗ v) ❙⋅ ❙𝖺❙[❙∥Dom t❙∥, ❙∥Dom u❙∥, ❙∥Dom v❙∥❙])"
using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Ide_in_Hom
Diag_Diagonalize Diagonalize_preserves_Ide TensorDiag_preserves_Ide
TensorDiag_preserves_Diag TensorDiag_assoc Par_Arr_norm
by (intro mkarr_eqI, simp_all)
also have "... = α (mkarr t, mkarr u, mkarr v)"
using assms Arr_implies_Ide_Dom rep_mkarr Ide_in_Hom assoc⇩F⇩M⇩C_def
Par_Arr_norm [of "Dom t"] Par_Arr_norm [of "Dom u"] Par_Arr_norm [of "Dom v"]
α_simp
by simp
finally show ?thesis by blast
qed
lemma mkarr_Assoc':
assumes "Arr t" and "Arr u" and "Arr v"
shows "mkarr ❙𝖺⇧-⇧1❙[t, u, v❙] = α' (mkarr t, mkarr u, mkarr v)"
proof -
have "mkarr ❙𝖺⇧-⇧1❙[t, u, v❙] = mkarr (❙𝖺⇧-⇧1❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙] ❙⋅ (t ❙⊗ u ❙⊗ v))"
using assms Par_Arr_norm Arr_implies_Ide_Cod Ide_in_Hom Diag_Diagonalize
TensorDiag_preserves_Diag CompDiag_Cod_Diag [of "❙⌊t❙⌋ ❙⌊❙⊗❙⌋ ❙⌊u❙⌋ ❙⌊❙⊗❙⌋ ❙⌊v❙⌋"]
by (intro mkarr_eqI, simp_all)
also have "... = mkarr ❙𝖺⇧-⇧1❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙] ⋅ mkarr (t ❙⊗ u ❙⊗ v)"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm by simp
also have "... = mkarr (Inv ❙𝖺❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙]) ⋅ mkarr (t ❙⊗ u ❙⊗ v)"
proof -
have "mkarr ❙𝖺⇧-⇧1❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙] =
mkarr (Inv ❙𝖺❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙])"
using assms Arr_implies_Ide_Cod Ide_in_Hom Par_Arr_norm Inv_in_Hom Ide_implies_Can
norm_preserves_Can Diagonalize_Inv Diagonalize_preserves_Ide
by (intro mkarr_eqI, simp_all)
thus ?thesis by argo
qed
also have "... = inv (mkarr ❙𝖺❙[❙∥Cod t❙∥, ❙∥Cod u❙∥, ❙∥Cod v❙∥❙]) ⋅ mkarr (t ❙⊗ u ❙⊗ v)"
using assms Arr_implies_Ide_Cod Ide_implies_Can norm_preserves_Can by simp
also have "... = α' (mkarr t, mkarr u, mkarr v)"
proof -
have "mkarr (❙𝖺⇧-⇧1❙[Inv ❙∥Cod t❙∥, Inv ❙∥Cod u❙∥, Inv ❙∥Cod v❙∥❙] ❙⋅ (Cod t ❙⊗ Cod u ❙⊗ Cod v))
= mkarr ❙𝖺⇧-⇧1❙[Inv ❙∥Cod t❙∥, Inv ❙∥Cod u❙∥, Inv ❙∥Cod v❙∥❙]"
using assms Arr_implies_Ide_Cod Inv_in_Hom norm_preserves_Can Diagonalize_Inv
Ide_implies_Can Diag_Diagonalize Ide_in_Hom Diagonalize_preserves_Ide
Par_Arr_norm TensorDiag_preserves_Diag
CompDiag_Cod_Diag [of "❙⌊Cod t❙⌋ ❙⌊❙⊗❙⌋ ❙⌊Cod u❙⌋ ❙⌊❙⊗❙⌋ ❙⌊Cod v❙⌋"]
by (intro mkarr_eqI) simp_all
thus ?thesis
using assms Arr_implies_Ide_Cod rep_mkarr assoc⇩F⇩M⇩C_def α'.map_simp by simp
qed
finally show ?thesis by blast
qed
text ‹
Next, we define the ``inclusion of generators'' functor from @{term C} to ‹ℱC›.
›
definition inclusion_of_generators
where "inclusion_of_generators ≡ λf. if C.arr f then mkarr ❙⟨f❙⟩ else null"
lemma inclusion_is_functor:
shows "functor C comp inclusion_of_generators"
unfolding inclusion_of_generators_def
apply unfold_locales
apply auto[4]
by (elim C.seqE, simp, intro mkarr_eqI, auto)
end
text ‹
We now show that, given a functor @{term V} from @{term C} to a
a monoidal category @{term D}, the evaluation map that takes formal arrows
of the monoidal language of @{term C} to arrows of @{term D}
induces a strict monoidal functor from ‹ℱC› to @{term D}.
›
locale evaluation_functor =
C: category C +
D: monoidal_category D T⇩D α⇩D ι⇩D +
evaluation_map C D T⇩D α⇩D ι⇩D V +
ℱC: free_monoidal_category C
for C :: "'c comp" (infixr ‹⋅⇩C› 55)
and D :: "'d comp" (infixr ‹⋅⇩D› 55)
and T⇩D :: "'d * 'd ⇒ 'd"
and α⇩D :: "'d * 'd * 'd ⇒ 'd"
and ι⇩D :: "'d"
and V :: "'c ⇒ 'd"
begin
notation eval (‹⦃_⦄›)
definition map
where "map f ≡ if ℱC.arr f then ⦃ℱC.rep f⦄ else D.null"
text ‹
It follows from the coherence theorem that a formal arrow and its normal
form always have the same evaluation.
›
lemma eval_norm:
assumes "Arr t"
shows "⦃❙∥t❙∥⦄ = ⦃t⦄"
using assms ℱC.Par_Arr_norm ℱC.Diagonalize_norm coherence canonical_factorization
by simp
interpretation "functor" ℱC.comp D map
proof
fix f
show "¬ℱC.arr f ⟹ map f = D.null" using map_def by simp
assume f: "ℱC.arr f"
show "D.arr (map f)" using f map_def ℱC.arr_char by simp
show "D.dom (map f) = map (ℱC.dom f)"
using f map_def eval_norm ℱC.rep_dom Arr_implies_Ide_Dom by auto
show "D.cod (map f) = map (ℱC.cod f)"
using f map_def eval_norm ℱC.rep_cod Arr_implies_Ide_Cod by auto
next
fix f g
assume fg: "ℱC.seq g f"
show "map (ℱC.comp g f) = D (map g) (map f)"
using fg map_def ℱC.rep_comp ℱC.rep_preserves_seq eval_norm by auto
qed
lemma is_functor:
shows "functor ℱC.comp D map" ..
interpretation FF: product_functor ℱC.comp ℱC.comp D D map map ..
interpretation FoT: composite_functor ℱC.CC.comp ℱC.comp D ℱC.T⇩F⇩M⇩C map ..
interpretation ToFF: composite_functor ℱC.CC.comp D.CC.comp D FF.map T⇩D ..
interpretation strict_monoidal_functor
ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D map
proof
show "map ℱC.ι = ι⇩D"
using ℱC.ι_def ℱC.lunit_agreement map_def ℱC.rep_lunit ℱC.Arr_rep [of ℐ]
eval_norm ℱC.lunit_agreement D.unitor_coincidence D.comp_cod_arr D.unit_in_hom
by auto
show "⋀f g. ⟦ ℱC.arr f; ℱC.arr g ⟧ ⟹
map (ℱC.tensor f g) = D.tensor (map f) (map g)"
using map_def ℱC.rep_tensor ℱC.Arr_rep eval_norm by simp
show "⋀a b c. ⟦ ℱC.ide a; ℱC.ide b; ℱC.ide c ⟧ ⟹
map (ℱC.assoc a b c) = D.assoc (map a) (map b) (map c)"
using map_def ℱC.assoc⇩F⇩M⇩C_def ℱC.rep_mkarr eval_norm by auto
qed
lemma is_strict_monoidal_functor:
shows "strict_monoidal_functor ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D map"
..
end
sublocale evaluation_functor ⊆ strict_monoidal_functor
ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C D T⇩D α⇩D ι⇩D map
using is_strict_monoidal_functor by auto
text ‹
The final step in proving freeness is to show that the evaluation functor
is the \emph{unique} strict monoidal extension of the functor @{term V}
to ‹ℱC›. This is done by induction, exploiting the syntactic construction
of ‹ℱC›.
›
text ‹
To ease the statement and proof of the result, we define a locale that
expresses that @{term F} is a strict monoidal extension to monoidal
category @{term C}, of a functor @{term "V"} from @{term "C⇩0"} to a
monoidal category @{term D}, along a functor @{term I} from
@{term "C⇩0"} to @{term C}.
›
locale strict_monoidal_extension =
C⇩0: category C⇩0 +
C: monoidal_category C T⇩C α⇩C ι⇩C +
D: monoidal_category D T⇩D α⇩D ι⇩D +
I: "functor" C⇩0 C I +
V: "functor" C⇩0 D V +
strict_monoidal_functor C T⇩C α⇩C ι⇩C D T⇩D α⇩D ι⇩D F
for C⇩0 :: "'c⇩0 comp"
and C :: "'c comp" (infixr ‹⋅⇩C› 55)
and T⇩C :: "'c * 'c ⇒ 'c"
and α⇩C :: "'c * 'c * 'c ⇒ 'c"
and ι⇩C :: "'c"
and D :: "'d comp" (infixr ‹⋅⇩D› 55)
and T⇩D :: "'d * 'd ⇒ 'd"
and α⇩D :: "'d * 'd * 'd ⇒ 'd"
and ι⇩D :: "'d"
and I :: "'c⇩0 ⇒ 'c"
and V :: "'c⇩0 ⇒ 'd"
and F :: "'c ⇒ 'd" +
assumes is_extension: "∀f. C⇩0.arr f ⟶ F (I f) = V f"
sublocale evaluation_functor ⊆
strict_monoidal_extension C ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D
ℱC.inclusion_of_generators V map
proof -
interpret inclusion: "functor" C ℱC.comp ℱC.inclusion_of_generators
using ℱC.inclusion_is_functor by auto
show "strict_monoidal_extension C ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D
ℱC.inclusion_of_generators V map"
apply unfold_locales
using map_def ℱC.rep_mkarr eval_norm ℱC.inclusion_of_generators_def by simp
qed
text ‹
A special case of interest is a strict monoidal extension to ‹ℱC›,
of a functor @{term V} from a category @{term C} to a monoidal category @{term D},
along the inclusion of generators from @{term C} to ‹ℱC›.
The evaluation functor induced by @{term V} is such an extension.
›
locale strict_monoidal_extension_to_free_monoidal_category =
C: category C +
monoidal_language C +
ℱC: free_monoidal_category C +
strict_monoidal_extension C ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D
ℱC.inclusion_of_generators V F
for C :: "'c comp" (infixr ‹⋅⇩C› 55)
and D :: "'d comp" (infixr ‹⋅⇩D› 55)
and T⇩D :: "'d * 'd ⇒ 'd"
and α⇩D :: "'d * 'd * 'd ⇒ 'd"
and ι⇩D :: "'d"
and V :: "'c ⇒ 'd"
and F :: "'c free_monoidal_category.arr ⇒ 'd"
begin
lemma strictly_preserves_everything:
shows "C.arr f ⟹ F (ℱC.mkarr ❙⟨f❙⟩) = V f"
and "F (ℱC.mkarr ❙ℐ) = ℐ⇩D"
and "⟦ Arr t; Arr u ⟧ ⟹ F (ℱC.mkarr (t ❙⊗ u)) = F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u)"
and "⟦ Arr t; Arr u; Dom t = Cod u ⟧ ⟹
F (ℱC.mkarr (t ❙⋅ u)) = F (ℱC.mkarr t) ⋅⇩D F (ℱC.mkarr u)"
and "Arr t ⟹ F (ℱC.mkarr ❙𝗅❙[t❙]) = D.𝔩 (F (ℱC.mkarr t))"
and "Arr t ⟹ F (ℱC.mkarr ❙𝗅⇧-⇧1❙[t❙]) = D.𝔩'.map (F (ℱC.mkarr t))"
and "Arr t ⟹ F (ℱC.mkarr ❙𝗋❙[t❙]) = D.ρ (F (ℱC.mkarr t))"
and "Arr t ⟹ F (ℱC.mkarr ❙𝗋⇧-⇧1❙[t❙]) = D.ρ'.map (F (ℱC.mkarr t))"
and "⟦ Arr t; Arr u; Arr v ⟧ ⟹
F (ℱC.mkarr ❙𝖺❙[t, u, v❙]) = α⇩D (F (ℱC.mkarr t), F (ℱC.mkarr u), F (ℱC.mkarr v))"
and "⟦ Arr t; Arr u; Arr v ⟧ ⟹
F (ℱC.mkarr ❙𝖺⇧-⇧1❙[t, u, v❙])
= D.α' (F (ℱC.mkarr t), F (ℱC.mkarr u), F (ℱC.mkarr v))"
proof -
show "C.arr f ⟹ F (ℱC.mkarr ❙⟨f❙⟩) = V f"
using is_extension ℱC.inclusion_of_generators_def by simp
show "F (ℱC.mkarr ❙ℐ) = ℐ⇩D"
using ℱC.mkarr_Unity ℱC.ι_def strictly_preserves_unity ℱC.ℐ_agreement by auto
show tensor_case:
"⋀t u.⟦ Arr t; Arr u ⟧ ⟹
F (ℱC.mkarr (t ❙⊗ u)) = F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u)"
proof -
fix t u
assume t: "Arr t" and u: "Arr u"
have "F (ℱC.mkarr (t ❙⊗ u)) = F (ℱC.tensor (ℱC.mkarr t) (ℱC.mkarr u))"
using t u ℱC.tensor_mkarr ℱC.arr_mkarr by simp
also have "... = F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u)"
using t u ℱC.arr_mkarr strictly_preserves_tensor by blast
finally show "F (ℱC.mkarr (t ❙⊗ u)) = F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u)"
by fast
qed
show "⟦ Arr t; Arr u; Dom t = Cod u ⟧ ⟹
F (ℱC.mkarr (t ❙⋅ u)) = F (ℱC.mkarr t) ⋅⇩D F (ℱC.mkarr u)"
proof -
fix t u
assume t: "Arr t" and u: "Arr u" and tu: "Dom t = Cod u"
show "F (ℱC.mkarr (t ❙⋅ u)) = F (ℱC.mkarr t) ⋅⇩D F (ℱC.mkarr u)"
proof -
have "F (ℱC.mkarr (t ❙⋅ u)) = F (ℱC.mkarr t ⋅ ℱC.mkarr u)"
using t u tu ℱC.comp_mkarr by simp
also have "... = F (ℱC.mkarr t) ⋅⇩D F (ℱC.mkarr u)"
using t u tu ℱC.arr_mkarr by fastforce
finally show ?thesis by blast
qed
qed
show "Arr t ⟹ F (ℱC.mkarr ❙𝗅❙[t❙]) = D.𝔩 (F (ℱC.mkarr t))"
using ℱC.mkarr_Lunit Arr_implies_Ide_Dom ℱC.ide_mkarr_Ide strictly_preserves_lunit
by simp
show "Arr t ⟹ F (ℱC.mkarr ❙𝗋❙[t❙]) = D.ρ (F (ℱC.mkarr t))"
using ℱC.mkarr_Runit Arr_implies_Ide_Dom ℱC.ide_mkarr_Ide strictly_preserves_runit
by simp
show "⟦ Arr t; Arr u; Arr v ⟧ ⟹
F (ℱC.mkarr ❙𝖺❙[t, u, v❙])
= α⇩D (F (ℱC.mkarr t), F (ℱC.mkarr u), F (ℱC.mkarr v))"
using ℱC.mkarr_Assoc strictly_preserves_assoc ℱC.ide_mkarr_Ide tensor_case
by simp
show "Arr t ⟹ F (ℱC.mkarr ❙𝗅⇧-⇧1❙[t❙]) = D.𝔩'.map (F (ℱC.mkarr t))"
proof -
assume t: "Arr t"
have "F (ℱC.mkarr ❙𝗅⇧-⇧1❙[t❙]) = F (ℱC.lunit' (ℱC.mkarr (Cod t))) ⋅⇩D F (ℱC.mkarr t)"
using t ℱC.mkarr_Lunit' Arr_implies_Ide_Cod ℱC.ide_mkarr_Ide ℱC.𝔩'.map_simp
ℱC.comp_cod_arr
by simp
also have "... = D.lunit' (D.cod (F (ℱC.mkarr t))) ⋅⇩D F (ℱC.mkarr t)"
using t Arr_implies_Ide_Cod ℱC.ide_mkarr_Ide strictly_preserves_lunit
preserves_inv
by simp
also have "... = D.𝔩'.map (F (ℱC.mkarr t))"
using t D.𝔩'.map_simp D.comp_cod_arr by simp
finally show ?thesis by blast
qed
show "Arr t ⟹ F (ℱC.mkarr ❙𝗋⇧-⇧1❙[t❙]) = D.ρ'.map (F (ℱC.mkarr t))"
proof -
assume t: "Arr t"
have "F (ℱC.mkarr ❙𝗋⇧-⇧1❙[t❙]) = F (ℱC.runit' (ℱC.mkarr (Cod t))) ⋅⇩D F (ℱC.mkarr t)"
using t ℱC.mkarr_Runit' Arr_implies_Ide_Cod ℱC.ide_mkarr_Ide ℱC.ρ'.map_simp
ℱC.comp_cod_arr
by simp
also have "... = D.runit' (D.cod (F (ℱC.mkarr t))) ⋅⇩D F (ℱC.mkarr t)"
using t Arr_implies_Ide_Cod ℱC.ide_mkarr_Ide strictly_preserves_runit
preserves_inv
by simp
also have "... = D.ρ'.map (F (ℱC.mkarr t))"
using t D.ρ'.map_simp D.comp_cod_arr by simp
finally show ?thesis by blast
qed
show "⟦ Arr t; Arr u; Arr v ⟧ ⟹
F (ℱC.mkarr ❙𝖺⇧-⇧1❙[t, u, v❙])
= D.α'.map (F (ℱC.mkarr t), F (ℱC.mkarr u), F (ℱC.mkarr v))"
proof -
assume t: "Arr t" and u: "Arr u" and v: "Arr v"
have "F (ℱC.mkarr ❙𝖺⇧-⇧1❙[t, u, v❙]) =
F (ℱC.assoc' (ℱC.mkarr (Cod t)) (ℱC.mkarr (Cod u)) (ℱC.mkarr (Cod v))) ⋅⇩D
(F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u) ⊗⇩D F (ℱC.mkarr v))"
using t u v ℱC.mkarr_Assoc' Arr_implies_Ide_Cod ℱC.ide_mkarr_Ide ℱC.α'.map_simp
tensor_case ℱC.iso_assoc
by simp
also have "... = D.assoc' (D.cod (F (ℱC.mkarr t))) (D.cod (F (ℱC.mkarr u)))
(D.cod (F (ℱC.mkarr v))) ⋅⇩D
(F (ℱC.mkarr t) ⊗⇩D F (ℱC.mkarr u) ⊗⇩D F (ℱC.mkarr v))"
using t u v ℱC.ide_mkarr_Ide Arr_implies_Ide_Cod preserves_inv ℱC.iso_assoc
strictly_preserves_assoc
[of "ℱC.mkarr (Cod t)" "ℱC.mkarr (Cod u)" "ℱC.mkarr (Cod v)"]
by simp
also have "... = D.α'.map (F (ℱC.mkarr t), F (ℱC.mkarr u), F (ℱC.mkarr v))"
using t u v D.α'.map_simp by simp
finally show ?thesis by blast
qed
qed
end
sublocale evaluation_functor ⊆ strict_monoidal_extension_to_free_monoidal_category
C D T⇩D α⇩D ι⇩D V map
..
context free_monoidal_category
begin
text ‹
The evaluation functor induced by @{term V} is the unique strict monoidal
extension of @{term V} to ‹ℱC›.
›
theorem is_free:
assumes "strict_monoidal_extension_to_free_monoidal_category C D T⇩D α⇩D ι⇩D V F"
shows "F = evaluation_functor.map C D T⇩D α⇩D ι⇩D V"
proof -
interpret F: strict_monoidal_extension_to_free_monoidal_category C D T⇩D α⇩D ι⇩D V F
using assms by auto
interpret E: evaluation_functor C D T⇩D α⇩D ι⇩D V ..
have Ide_case: "⋀a. Ide a ⟹ F (mkarr a) = E.map (mkarr a)"
proof -
fix a
show "Ide a ⟹ F (mkarr a) = E.map (mkarr a)"
using E.strictly_preserves_everything F.strictly_preserves_everything Ide_implies_Arr
by (induct a) auto
qed
show ?thesis
proof
fix f
have "¬arr f ⟹ F f = E.map f"
using E.is_extensional F.is_extensional by simp
moreover have "arr f ⟹ F f = E.map f"
proof -
assume f: "arr f"
have "Arr (rep f) ∧ f = mkarr (rep f)" using f mkarr_rep by simp
moreover have "⋀t. Arr t ⟹ F (mkarr t) = E.map (mkarr t)"
proof -
fix t
show "Arr t ⟹ F (mkarr t) = E.map (mkarr t)"
using Ide_case E.strictly_preserves_everything F.strictly_preserves_everything
Arr_implies_Ide_Dom Arr_implies_Ide_Cod
by (induct t) auto
qed
ultimately show "F f = E.map f" by metis
qed
ultimately show "F f = E.map f" by blast
qed
qed
end
section "Strict Subcategory"
context free_monoidal_category
begin
text ‹
In this section we show that ‹ℱC› is monoidally equivalent to its full subcategory
‹ℱ⇩SC› whose objects are the equivalence classes of diagonal identity terms,
and that this subcategory is the free strict monoidal category generated by @{term C}.
›
interpretation ℱ⇩SC: full_subcategory comp ‹λf. ide f ∧ Diag (DOM f)›
by (unfold_locales) auto
text ‹
The mapping defined on equivalence classes by diagonalizing their representatives
is a functor from the free monoidal category to the subcategory @{term "ℱ⇩SC"}.
›
definition D
where "D ≡ λf. if arr f then mkarr ❙⌊rep f❙⌋ else ℱ⇩SC.null"
text ‹
The arrows of ‹ℱ⇩SC› are those equivalence classes whose canonical representative
term has diagonal formal domain and codomain.
›
lemma strict_arr_char:
shows "ℱ⇩SC.arr f ⟷ arr f ∧ Diag (DOM f) ∧ Diag (COD f)"
proof
show "arr f ∧ Diag (DOM f) ∧ Diag (COD f) ⟹ ℱ⇩SC.arr f"
using ℱ⇩SC.arr_char⇩S⇩b⇩C DOM_dom DOM_cod by simp
show "ℱ⇩SC.arr f ⟹ arr f ∧ Diag (DOM f) ∧ Diag (COD f)"
using ℱ⇩SC.arr_char⇩S⇩b⇩C Arr_rep Arr_implies_Ide_Cod Ide_implies_Arr DOM_dom DOM_cod
by force
qed
text ‹
Alternatively, the arrows of ‹ℱ⇩SC› are those equivalence classes
that are preserved by diagonalization of representatives.
›
lemma strict_arr_char':
shows "ℱ⇩SC.arr f ⟷ arr f ∧ D f = f"
proof
fix f
assume f: "ℱ⇩SC.arr f"
show "arr f ∧ D f = f"
proof
show "arr f" using f ℱ⇩SC.arr_char⇩S⇩b⇩C by blast
show "D f = f"
using f strict_arr_char mkarr_Diagonalize_rep D_def by simp
qed
next
assume f: "arr f ∧ D f = f"
show "ℱ⇩SC.arr f"
proof -
have "arr f" using f by simp
moreover have "Diag (DOM f)"
proof -
have "DOM f = DOM (mkarr ❙⌊rep f❙⌋)" using f D_def by auto
also have "... = Dom ❙∥❙⌊rep f❙⌋❙∥"
using f Arr_rep Diagonalize_in_Hom rep_mkarr by simp
also have "... = Dom ❙⌊rep f❙⌋"
using f Arr_rep Diagonalize_in_Hom Par_Arr_norm [of "❙⌊rep f❙⌋"] by force
finally have "DOM f = Dom ❙⌊rep f❙⌋" by blast
thus ?thesis using f Arr_rep Diag_Diagonalize Dom_preserves_Diag by metis
qed
moreover have "Diag (COD f)"
proof -
have "COD f = COD (mkarr ❙⌊rep f❙⌋)" using f D_def by auto
also have "... = Cod ❙∥❙⌊rep f❙⌋❙∥"
using f Arr_rep Diagonalize_in_Hom rep_mkarr by simp
also have "... = Cod ❙⌊rep f❙⌋"
using f Arr_rep Diagonalize_in_Hom Par_Arr_norm [of "❙⌊rep f❙⌋"] by force
finally have "COD f = Cod ❙⌊rep f❙⌋" by blast
thus ?thesis using f Arr_rep Diag_Diagonalize Cod_preserves_Diag by metis
qed
ultimately show ?thesis using strict_arr_char by auto
qed
qed
interpretation D: "functor" comp ℱ⇩SC.comp D
proof -
have 1: "⋀f. arr f ⟹ ℱ⇩SC.arr (D f)"
unfolding strict_arr_char D_def
using arr_mkarr Diagonalize_in_Hom Arr_rep rep_mkarr Par_Arr_norm
Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diag_Diagonalize
by force
show "functor comp ℱ⇩SC.comp D"
proof
show "⋀f. ¬ arr f ⟹ D f = ℱ⇩SC.null" using D_def by simp
show "⋀f. arr f ⟹ ℱ⇩SC.arr (D f)" by fact
show "⋀f. arr f ⟹ ℱ⇩SC.dom (D f) = D (dom f)"
using D_def Diagonalize_in_Hom ℱ⇩SC.dom_char⇩S⇩b⇩C ℱ⇩SC.arr_char⇩S⇩b⇩C
rep_mkarr rep_dom Arr_implies_Ide_Dom Arr_implies_Ide_Cod
Diagonalize_preserves_Ide ide_mkarr_Ide Diag_Diagonalize Dom_norm
by simp
show 2: "⋀f. arr f ⟹ ℱ⇩SC.cod (D f) = D (cod f)"
using D_def Diagonalize_in_Hom ℱ⇩SC.cod_char⇩S⇩b⇩C ℱ⇩SC.arr_char⇩S⇩b⇩C
rep_mkarr rep_cod Arr_implies_Ide_Dom Arr_implies_Ide_Cod
Diagonalize_preserves_Ide ide_mkarr_Ide Diag_Diagonalize Dom_norm
by simp
fix f g
assume fg: "seq g f"
hence fg': "arr f ∧ arr g ∧ dom g = cod f" by blast
show "D (g ⋅ f) = ℱ⇩SC.comp (D g) (D f)"
proof -
have seq: "ℱ⇩SC.seq (mkarr ❙⌊rep g❙⌋) (mkarr ❙⌊rep f❙⌋)"
proof -
have 3: "ℱ⇩SC.arr (mkarr ❙⌊rep g❙⌋) ∧ ℱ⇩SC.arr (mkarr ❙⌊rep f❙⌋)"
using fg' 1 arr_char D_def by force
moreover have "ℱ⇩SC.dom (mkarr ❙⌊rep g❙⌋) = ℱ⇩SC.cod (mkarr ❙⌊rep f❙⌋)"
using fg' 2 3 ℱ⇩SC.dom_char⇩S⇩b⇩C rep_in_Hom mkarr_in_hom D_def
Dom_Diagonalize_rep Diag_implies_Arr Diag_Diagonalize(1) ℱ⇩SC.arr_char⇩S⇩b⇩C
by force
ultimately show ?thesis using ℱ⇩SC.seqI by auto
qed
have "mkarr ❙⌊rep (g ⋅ f)❙⌋ = ℱ⇩SC.comp (mkarr ❙⌊rep g❙⌋) (mkarr ❙⌊rep f❙⌋)"
proof -
have Seq: "Seq ❙⌊rep g❙⌋ ❙⌊rep f❙⌋"
using fg rep_preserves_seq Diagonalize_in_Hom by force
hence 4: "❙⌊rep g❙⌋ ❙⋅ ❙⌊rep f❙⌋ ∈ Hom ❙⌊DOM f❙⌋ ❙⌊COD g❙⌋"
using fg' Seq Diagonalize_in_Hom by auto
have "ℱ⇩SC.comp (mkarr ❙⌊rep g❙⌋) (mkarr ❙⌊rep f❙⌋) = mkarr ❙⌊rep g❙⌋ ⋅ mkarr ❙⌊rep f❙⌋"
using seq ℱ⇩SC.comp_char ℱ⇩SC.seq_char⇩S⇩b⇩C by meson
also have "... = mkarr (❙⌊rep g❙⌋ ❙⋅ ❙⌊rep f❙⌋)"
using Seq comp_mkarr by fastforce
also have "... = mkarr ❙⌊rep (g ⋅ f)❙⌋"
proof (intro mkarr_eqI)
show "Par (❙⌊rep g❙⌋ ❙⋅ ❙⌊rep f❙⌋) ❙⌊rep (g ⋅ f)❙⌋"
using fg 4 rep_in_Hom rep_preserves_seq rep_in_Hom Diagonalize_in_Hom
Par_Arr_norm
apply (elim seqE, auto)
by (simp_all add: rep_comp)
show "❙⌊❙⌊rep g❙⌋ ❙⋅ ❙⌊rep f❙⌋❙⌋ = ❙⌊❙⌊rep (g ⋅ f)❙⌋❙⌋"
using fg rep_preserves_seq norm_in_Hom Diag_Diagonalize Diagonalize_Diag
apply auto
by (simp add: rep_comp)
qed
finally show ?thesis by blast
qed
thus ?thesis using fg D_def by auto
qed
qed
qed
lemma diagonalize_is_functor:
shows "functor comp ℱ⇩SC.comp D" ..
lemma diagonalize_strict_arr:
assumes "ℱ⇩SC.arr f"
shows "D f = f"
using assms arr_char D_def strict_arr_char Arr_rep Arr_implies_Ide_Dom Ide_implies_Arr
mkarr_Diagonalize_rep [of f]
by auto
lemma diagonalize_is_idempotent:
shows "D o D = D"
unfolding D_def
using D.is_extensional ℱ⇩SC.null_char Arr_rep Diagonalize_in_Hom mkarr_Diagonalize_rep
strict_arr_char rep_mkarr
by fastforce
lemma diagonalize_tensor:
assumes "arr f" and "arr g"
shows "D (f ⊗ g) = D (D f ⊗ D g)"
unfolding D_def
using assms strict_arr_char rep_in_Hom Diagonalize_in_Hom tensor_mkarr rep_tensor
Diagonalize_in_Hom rep_mkarr Diagonalize_norm Diagonalize_Tensor
by force
lemma ide_diagonalize_can:
assumes "can f"
shows "ide (D f)"
using assms D_def Can_rep_can Ide_Diagonalize_Can ide_mkarr_Ide can_implies_arr
by simp
text ‹
We next show that the diagonalization functor and the inclusion of the full subcategory
‹ℱ⇩SC› underlie an equivalence of categories. The arrows @{term "mkarr (DOM a❙↓)"},
determined by reductions of canonical representatives, are the components of a
natural isomorphism.
›
interpretation S: full_inclusion_functor comp ‹λf. ide f ∧ Diag (DOM f)› ..
interpretation DoS: composite_functor ℱ⇩SC.comp comp ℱ⇩SC.comp ℱ⇩SC.map D
..
interpretation SoD: composite_functor comp ℱ⇩SC.comp comp D ℱ⇩SC.map ..
interpretation ν: transformation_by_components
comp comp map SoD.map ‹λa. mkarr (DOM a❙↓)›
proof
fix a
assume a: "ide a"
show "«mkarr (DOM a❙↓) : map a → SoD.map a»"
proof -
have "«mkarr (DOM a❙↓) : a → mkarr ❙⌊DOM a❙⌋»"
using a Arr_implies_Ide_Dom red_in_Hom dom_char [of a] by auto
moreover have "map a = a"
using a map_simp by simp
moreover have "SoD.map a = mkarr ❙⌊DOM a❙⌋"
using a D.preserves_ide ℱ⇩SC.ideD ℱ⇩SC.map_simp D_def Ide_Diagonalize_rep_ide
Ide_in_Hom Diagonalize_in_Hom
by force
ultimately show ?thesis by simp
qed
next
fix f
assume f: "arr f"
show "mkarr (DOM (cod f)❙↓) ⋅ map f = SoD.map f ⋅ mkarr (DOM (dom f)❙↓)"
proof -
have "SoD.map f ⋅ mkarr (DOM (dom f)❙↓) = mkarr ❙⌊rep f❙⌋ ⋅ mkarr (DOM f❙↓)"
using f DOM_dom D.preserves_arr ℱ⇩SC.map_simp D_def by simp
also have "... = mkarr (❙⌊rep f❙⌋ ❙⋅ DOM f❙↓)"
using f Diagonalize_in_Hom red_in_Hom comp_mkarr Arr_implies_Ide_Dom
by simp
also have "... = mkarr (COD f❙↓ ❙⋅ rep f)"
proof (intro mkarr_eqI)
show "Par (❙⌊rep f❙⌋ ❙⋅ DOM f❙↓) (COD f❙↓ ❙⋅ rep f)"
using f Diagonalize_in_Hom red_in_Hom Arr_implies_Ide_Dom Arr_implies_Ide_Cod
by simp
show "❙⌊❙⌊rep f❙⌋ ❙⋅ DOM f❙↓❙⌋ = ❙⌊COD f❙↓ ❙⋅ rep f❙⌋"
proof -
have "❙⌊❙⌊rep f❙⌋ ❙⋅ DOM f❙↓❙⌋ = ❙⌊rep f❙⌋ ❙⌊❙⋅❙⌋ ❙⌊DOM f❙↓❙⌋"
using f by simp
also have "... = ❙⌊rep f❙⌋"
using f Arr_implies_Ide_Dom Can_red Ide_Diagonalize_Can [of "DOM f❙↓"]
Diag_Diagonalize CompDiag_Diag_Ide
by force
also have "... = ❙⌊COD f❙↓❙⌋ ❙⌊❙⋅❙⌋ ❙⌊rep f❙⌋"
using f Arr_implies_Ide_Cod Can_red Ide_Diagonalize_Can [of "COD f❙↓"]
Diag_Diagonalize CompDiag_Diag_Ide
by force
also have "... = ❙⌊COD f❙↓ ❙⋅ rep f❙⌋"
by simp
finally show ?thesis by blast
qed
qed
also have "... = mkarr (COD f❙↓) ⋅ mkarr (rep f)"
using f comp_mkarr rep_in_Hom red_in_Hom Arr_implies_Ide_Cod by blast
also have "... = mkarr (DOM (cod f)❙↓) ⋅ map f"
using f DOM_cod by simp
finally show ?thesis by blast
qed
qed
interpretation ν: natural_isomorphism comp comp map SoD.map ν.map
apply unfold_locales
using ν.map_simp_ide rep_in_Hom Arr_implies_Ide_Dom Can_red can_mkarr_Can iso_can
by simp
text ‹
The restriction of the diagonalization functor to the subcategory ‹ℱ⇩SC›
is the identity.
›
lemma DoS_eq_ℱ⇩SC:
shows "DoS.map = ℱ⇩SC.map"
proof
fix f
have "¬ ℱ⇩SC.arr f ⟹ DoS.map f = ℱ⇩SC.map f"
using DoS.is_extensional ℱ⇩SC.map_def by simp
moreover have "ℱ⇩SC.arr f ⟹ DoS.map f = ℱ⇩SC.map f"
using ℱ⇩SC.map_simp strict_arr_char Diagonalize_Diag D_def mkarr_Diagonalize_rep
by simp
ultimately show "DoS.map f = ℱ⇩SC.map f" by blast
qed
interpretation μ: transformation_by_components
ℱ⇩SC.comp ℱ⇩SC.comp DoS.map ℱ⇩SC.map ‹λa. a›
using ℱ⇩SC.ideD ℱ⇩SC.map_simp DoS_eq_ℱ⇩SC ℱ⇩SC.map_simp ℱ⇩SC.comp_cod_arr ℱ⇩SC.comp_arr_dom
apply unfold_locales
by (intro ℱ⇩SC.in_homI) auto
interpretation μ: natural_isomorphism ℱ⇩SC.comp ℱ⇩SC.comp DoS.map ℱ⇩SC.map μ.map
apply unfold_locales using μ.map_simp_ide ℱ⇩SC.ide_is_iso by simp
interpretation equivalence_of_categories ℱ⇩SC.comp comp D ℱ⇩SC.map ν.map μ.map ..
text ‹
We defined the natural isomorphisms @{term μ} and @{term ν} by giving their
components (\emph{i.e.}~their values at objects). However, it is helpful
in exporting these facts to have simple characterizations of their values
for all arrows.
›
definition μ
where "μ ≡ λf. if ℱ⇩SC.arr f then f else ℱ⇩SC.null"
definition ν
where "ν ≡ λf. if arr f then mkarr (COD f❙↓) ⋅ f else null"
lemma μ_char:
shows "μ.map = μ"
proof (intro NaturalTransformation.eqI)
show "natural_transformation ℱ⇩SC.comp ℱ⇩SC.comp DoS.map ℱ⇩SC.map μ.map" ..
have "natural_transformation ℱ⇩SC.comp ℱ⇩SC.comp ℱ⇩SC.map ℱ⇩SC.map ℱ⇩SC.map"
using DoS.as_nat_trans.natural_transformation_axioms DoS_eq_ℱ⇩SC by simp
moreover have "ℱ⇩SC.map = μ" unfolding μ_def using ℱ⇩SC.map_def by blast
ultimately show "natural_transformation ℱ⇩SC.comp ℱ⇩SC.comp DoS.map ℱ⇩SC.map μ"
using ℱ⇩SC.as_nat_trans.natural_transformation_axioms DoS_eq_ℱ⇩SC by simp
show "⋀a. ℱ⇩SC.ide a ⟹ μ.map a = μ a"
using μ.map_simp_ide ℱ⇩SC.ideD μ_def by simp
qed
lemma ν_char:
shows "ν.map = ν"
unfolding ν.map_def ν_def using map_simp DOM_cod by fastforce
lemma is_equivalent_to_strict_subcategory:
shows "equivalence_of_categories ℱ⇩SC.comp comp D ℱ⇩SC.map ν μ"
proof -
have "equivalence_of_categories ℱ⇩SC.comp comp D ℱ⇩SC.map ν.map μ.map" ..
thus "equivalence_of_categories ℱ⇩SC.comp comp D ℱ⇩SC.map ν μ"
using ν_char μ_char by simp
qed
text ‹
The inclusion of generators functor from @{term C} to ‹ℱC›
corestricts to a functor from @{term C} to ‹ℱ⇩SC›.
›
interpretation I: "functor" C comp inclusion_of_generators
using inclusion_is_functor by auto
interpretation DoI: composite_functor C comp ℱ⇩SC.comp inclusion_of_generators D ..
lemma DoI_eq_I:
shows "DoI.map = inclusion_of_generators"
proof
fix f
have "¬ C.arr f ⟹ DoI.map f = inclusion_of_generators f"
using DoI.is_extensional I.is_extensional ℱ⇩SC.null_char by blast
moreover have "C.arr f ⟹ DoI.map f = inclusion_of_generators f"
proof -
assume f: "C.arr f"
have "DoI.map f = D (inclusion_of_generators f)" using f by simp
also have "... = inclusion_of_generators f"
proof -
have "ℱ⇩SC.arr (inclusion_of_generators f)"
using f arr_mkarr rep_mkarr Par_Arr_norm [of "❙⟨f❙⟩"] strict_arr_char
inclusion_of_generators_def
by simp
thus ?thesis using f strict_arr_char' by blast
qed
finally show "DoI.map f = inclusion_of_generators f" by blast
qed
ultimately show "DoI.map f = inclusion_of_generators f" by blast
qed
end
text ‹
Next, we show that the subcategory ‹ℱ⇩SC› inherits monoidal structure from
the ambient category ‹ℱC›, and that this monoidal structure is strict.
›
locale free_strict_monoidal_category =
monoidal_language C +
ℱC: free_monoidal_category C +
full_subcategory ℱC.comp "λf. ℱC.ide f ∧ Diag (ℱC.DOM f)"
for C :: "'c comp"
begin
interpretation D: "functor" ℱC.comp comp ℱC.D
using ℱC.diagonalize_is_functor by auto
notation comp (infixr ‹⋅⇩S› 55)
definition tensor⇩S (infixr ‹⊗⇩S› 53)
where "f ⊗⇩S g ≡ ℱC.D (ℱC.tensor f g)"
definition assoc⇩S (‹𝖺⇩S[_, _, _]›)
where "assoc⇩S a b c ≡ a ⊗⇩S b ⊗⇩S c"
lemma tensor_char:
assumes "arr f" and "arr g"
shows "f ⊗⇩S g = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋)"
unfolding ℱC.D_def tensor⇩S_def
using assms arr_char⇩S⇩b⇩C ℱC.rep_tensor by simp
lemma tensor_in_hom [simp]:
assumes "«f : a → b»" and "«g : c → d»"
shows "«f ⊗⇩S g : a ⊗⇩S c → b ⊗⇩S d»"
unfolding tensor⇩S_def
using assms D.preserves_hom arr_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C
by (metis (no_types, lifting) ℱC.T_simp ℱC.tensor_in_hom in_homE)
lemma arr_tensor [simp]:
assumes "arr f" and "arr g"
shows "arr (f ⊗⇩S g)"
using assms arr_iff_in_hom [of f] arr_iff_in_hom [of g] tensor_in_hom by blast
lemma dom_tensor [simp]:
assumes "arr f" and "arr g"
shows "dom (f ⊗⇩S g) = dom f ⊗⇩S dom g"
using assms arr_iff_in_hom [of f] arr_iff_in_hom [of g] tensor_in_hom by blast
lemma cod_tensor [simp]:
assumes "arr f" and "arr g"
shows "cod (f ⊗⇩S g) = cod f ⊗⇩S cod g"
using assms arr_iff_in_hom [of f] arr_iff_in_hom [of g] tensor_in_hom by blast
lemma tensor_preserves_ide:
assumes "ide a" and "ide b"
shows "ide (a ⊗⇩S b)"
using assms tensor⇩S_def D.preserves_ide ℱC.tensor_preserves_ide ide_char⇩S⇩b⇩C
by fastforce
lemma tensor_tensor:
assumes "arr f" and "arr g" and "arr h"
shows "(f ⊗⇩S g) ⊗⇩S h = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
and "f ⊗⇩S g ⊗⇩S h = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
proof -
show "(f ⊗⇩S g) ⊗⇩S h = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
proof -
have "(f ⊗⇩S g) ⊗⇩S h = ℱC.mkarr (❙⌊ℱC.rep (f ⊗⇩S g)❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
using assms Diag_Diagonalize TensorDiag_preserves_Diag Diag_implies_Arr
ℱC.COD_mkarr ℱC.DOM_mkarr ℱC.strict_arr_char tensor_char
by simp
also have
"... = ℱC.mkarr (❙⌊ℱC.rep (ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋))❙⌋ ❙⌊❙⊗❙⌋
❙⌊ℱC.rep h❙⌋)"
using assms arr_char⇩S⇩b⇩C tensor_char by simp
also have "... = ℱC.mkarr (❙⌊❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
using assms ℱC.rep_mkarr TensorDiag_in_Hom Diag_Diagonalize
TensorDiag_preserves_Diag arr_char⇩S⇩b⇩C
by force
also have "... = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
using assms Diag_Diagonalize TensorDiag_preserves_Diag TensorDiag_assoc arr_char⇩S⇩b⇩C
by force
finally show ?thesis by blast
qed
show "f ⊗⇩S g ⊗⇩S h = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋)"
proof -
have "... = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋❙⌋)"
using assms Diag_Diagonalize TensorDiag_preserves_Diag arr_char⇩S⇩b⇩C by force
also have "... = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋
(❙⌊ℱC.rep (ℱC.mkarr (❙⌊ℱC.rep g❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep h❙⌋))❙⌋))"
using assms ℱC.rep_mkarr TensorDiag_in_Hom Diag_Diagonalize arr_char⇩S⇩b⇩C by force
also have "... = ℱC.mkarr (❙⌊ℱC.rep f❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep (g ⊗⇩S h)❙⌋)"
using assms tensor_char by simp
also have "... = f ⊗⇩S g ⊗⇩S h"
using assms Diag_Diagonalize TensorDiag_preserves_Diag Diag_implies_Arr
ℱC.COD_mkarr ℱC.DOM_mkarr ℱC.strict_arr_char tensor_char
by simp
finally show ?thesis by blast
qed
qed
lemma tensor_assoc:
assumes "arr f" and "arr g" and "arr h"
shows "(f ⊗⇩S g) ⊗⇩S h = f ⊗⇩S g ⊗⇩S h"
using assms tensor_tensor by presburger
lemma arr_unity:
shows "arr ℐ"
using ℱC.rep_unity ℱC.Par_Arr_norm ℱC.ℐ_agreement ℱC.strict_arr_char by force
lemma tensor_unity_arr:
assumes "arr f"
shows "ℐ ⊗⇩S f = f"
using assms arr_unity tensor_char ℱC.strict_arr_char ℱC.mkarr_Diagonalize_rep
by simp
lemma tensor_arr_unity:
assumes "arr f"
shows "f ⊗⇩S ℐ = f"
using assms arr_unity tensor_char ℱC.strict_arr_char ℱC.mkarr_Diagonalize_rep
by simp
lemma assoc_char:
assumes "ide a" and "ide b" and "ide c"
shows "𝖺⇩S[a, b, c] = ℱC.mkarr (❙⌊ℱC.rep a❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep b❙⌋ ❙⌊❙⊗❙⌋ ❙⌊ℱC.rep c❙⌋)"
using assms tensor_tensor(2) assoc⇩S_def ideD(1) by simp
lemma assoc_in_hom:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺⇩S[a, b, c] : (a ⊗⇩S b) ⊗⇩S c → a ⊗⇩S b ⊗⇩S c»"
using assms tensor_preserves_ide ideD tensor_assoc assoc⇩S_def
by (metis (no_types, lifting) ide_in_hom)
text ‹The category ‹ℱ⇩SC› is a monoidal category.›
interpretation EMC: elementary_monoidal_category comp tensor⇩S ℐ ‹λa. a› ‹λa. a› assoc⇩S
proof
show "ide ℐ"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C ℱC.rep_mkarr ℱC.Dom_norm ℱC.Cod_norm ℱC.ℐ_agreement
by auto
show "⋀a. ide a ⟹ iso a"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C iso_char⇩S⇩b⇩C by auto
show "⋀f a b g c d. ⟦ in_hom a b f; in_hom c d g ⟧ ⟹ in_hom (a ⊗⇩S c) (b ⊗⇩S d) (f ⊗⇩S g)"
using tensor_in_hom by blast
show "⋀a b. ⟦ ide a; ide b ⟧ ⟹ ide (a ⊗⇩S b)"
using tensor_preserves_ide by blast
show "⋀a b c. ⟦ ide a; ide b; ide c⟧ ⟹ iso 𝖺⇩S[a, b, c]"
using tensor_preserves_ide ide_is_iso assoc⇩S_def by presburger
show "⋀a b c. ⟦ ide a; ide b; ide c⟧ ⟹ «𝖺⇩S[a, b, c] : (a ⊗⇩S b) ⊗⇩S c → a ⊗⇩S b ⊗⇩S c»"
using assoc_in_hom by blast
show "⋀a b. ⟦ ide a; ide b ⟧ ⟹ (a ⊗⇩S b) ⋅⇩S 𝖺⇩S[a, ℐ, b] = a ⊗⇩S b"
using ide_def tensor_unity_arr assoc⇩S_def ideD(1) tensor_preserves_ide comp_ide_self
by simp
show "⋀f. arr f ⟹ cod f ⋅⇩S (ℐ ⊗⇩S f) = f ⋅⇩S dom f"
using tensor_unity_arr comp_arr_dom comp_cod_arr by presburger
show "⋀f. arr f ⟹ cod f ⋅⇩S (f ⊗⇩S ℐ) = f ⋅⇩S dom f"
using tensor_arr_unity comp_arr_dom comp_cod_arr by presburger
next
fix a
assume a: "ide a"
show "«a : ℐ ⊗⇩S a → a»"
using a tensor_unity_arr ide_in_hom [of a] by fast
show "«a : a ⊗⇩S ℐ → a»"
using a tensor_arr_unity ide_in_hom [of a] by fast
next
fix f g f' g'
assume fg: "seq g f"
assume fg': "seq g' f'"
show "(g ⊗⇩S g') ⋅⇩S (f ⊗⇩S f') = g ⋅⇩S f ⊗⇩S g' ⋅⇩S f'"
proof -
have A: "ℱC.seq g f" and B: "ℱC.seq g' f'"
using fg fg' seq_char⇩S⇩b⇩C by auto
have "(g ⊗⇩S g') ⋅⇩S (f ⊗⇩S f') = ℱC.D ((g ⊗ g') ⋅ (f ⊗ f'))"
using A B tensor⇩S_def by fastforce
also have "... = ℱC.D (g ⋅ f ⊗ g' ⋅ f')"
using A B ℱC.interchange ℱC.T_simp ℱC.seqE by metis
also have "... = ℱC.D (g ⋅ f) ⊗⇩S ℱC.D (g' ⋅ f')"
using A B tensor⇩S_def ℱC.T_simp ℱC.seqE ℱC.diagonalize_tensor arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) D.preserves_reflects_arr)
also have "... = ℱC.D g ⋅⇩S ℱC.D f ⊗⇩S ℱC.D g' ⋅⇩S ℱC.D f'"
using A B by simp
also have "... = g ⋅⇩S f ⊗⇩S g' ⋅⇩S f'"
using fg fg' ℱC.diagonalize_strict_arr by (elim seqE, simp)
finally show ?thesis by blast
qed
next
fix f0 f1 f2
assume f0: "arr f0" and f1: "arr f1" and f2: "arr f2"
show "𝖺⇩S[cod f0, cod f1, cod f2] ⋅⇩S ((f0 ⊗⇩S f1) ⊗⇩S f2)
= (f0 ⊗⇩S f1 ⊗⇩S f2) ⋅⇩S 𝖺⇩S[dom f0, dom f1, dom f2]"
using f0 f1 f2 assoc⇩S_def tensor_assoc dom_tensor cod_tensor arr_tensor
comp_cod_arr [of "f0 ⊗⇩S f1 ⊗⇩S f2" "cod f0 ⊗⇩S cod f1 ⊗⇩S cod f2"]
comp_arr_dom [of "f0 ⊗⇩S f1 ⊗⇩S f2" "dom f0 ⊗⇩S dom f1 ⊗⇩S dom f2"]
by presburger
next
fix a b c d
assume a: "ide a" and b: "ide b" and c: "ide c" and d: "ide d"
show "(a ⊗⇩S 𝖺⇩S[b, c, d]) ⋅⇩S 𝖺⇩S[a, b ⊗⇩S c, d] ⋅⇩S (𝖺⇩S[a, b, c] ⊗⇩S d)
= 𝖺⇩S[a, b, c ⊗⇩S d] ⋅⇩S 𝖺⇩S[a ⊗⇩S b, c, d]"
unfolding assoc⇩S_def
using a b c d tensor_assoc tensor_preserves_ide ideD tensor_in_hom
comp_arr_dom [of "a ⊗⇩S b ⊗⇩S c ⊗⇩S d"]
by simp
qed
lemma is_elementary_monoidal_category:
shows "elementary_monoidal_category comp tensor⇩S ℐ (λa. a) (λa. a) assoc⇩S" ..
abbreviation T⇩F⇩S⇩M⇩C where "T⇩F⇩S⇩M⇩C ≡ EMC.T"
abbreviation α⇩F⇩S⇩M⇩C where "α⇩F⇩S⇩M⇩C ≡ EMC.α"
abbreviation ι⇩F⇩S⇩M⇩C where "ι⇩F⇩S⇩M⇩C ≡ EMC.ι"
lemma is_monoidal_category:
shows "monoidal_category comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C"
using EMC.induces_monoidal_category by auto
end
sublocale free_strict_monoidal_category ⊆
elementary_monoidal_category comp tensor⇩S ℐ "λa. a" "λa. a" assoc⇩S
using is_elementary_monoidal_category by auto
sublocale free_strict_monoidal_category ⊆ monoidal_category comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
using is_monoidal_category by auto
sublocale free_strict_monoidal_category ⊆
strict_monoidal_category comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
using tensor_preserves_ide lunit_agreement runit_agreement α_ide_simp assoc⇩S_def
by unfold_locales auto
context free_strict_monoidal_category
begin
text ‹
The inclusion of generators functor from @{term C} to ‹ℱ⇩SC› is the composition
of the inclusion of generators from @{term C} to ‹ℱC› and the diagonalization
functor, which projects ‹ℱC› to ‹ℱ⇩SC›. As the diagonalization functor
is the identity map on the image of @{term C}, the composite functor amounts to the
corestriction to ‹ℱ⇩SC› of the inclusion of generators of ‹ℱC›.
›
interpretation D: "functor" ℱC.comp comp ℱC.D
using ℱC.diagonalize_is_functor by auto
interpretation I: composite_functor C ℱC.comp comp ℱC.inclusion_of_generators ℱC.D
proof -
interpret "functor" C ℱC.comp ℱC.inclusion_of_generators
using ℱC.inclusion_is_functor by blast
show "composite_functor C ℱC.comp comp ℱC.inclusion_of_generators ℱC.D" ..
qed
definition inclusion_of_generators
where "inclusion_of_generators ≡ ℱC.inclusion_of_generators"
lemma inclusion_is_functor:
shows "functor C comp inclusion_of_generators"
using ℱC.DoI_eq_I I.functor_axioms inclusion_of_generators_def
by auto
text ‹
The diagonalization functor is strict monoidal.
›
interpretation D: strict_monoidal_functor ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C
comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
ℱC.D
proof
show "ℱC.D ℱC.ι = ι"
proof -
have "ℱC.D ℱC.ι = ℱC.mkarr ❙⌊ℱC.rep ℱC.ι❙⌋"
unfolding ℱC.D_def using ℱC.ι_in_hom by auto
also have "... = ℱC.mkarr ❙⌊❙𝗅❙[❙∥❙ℐ❙∥❙]❙⌋"
using ℱC.ι_def ℱC.rep_unity ℱC.rep_lunit ℱC.Par_Arr_norm ℱC.Diagonalize_norm
by auto
also have "... = ι"
using ℱC.unity⇩F⇩M⇩C_def ℱC.ℐ_agreement ι_def by simp
finally show ?thesis by blast
qed
show "⋀f g. ⟦ ℱC.arr f; ℱC.arr g ⟧ ⟹
ℱC.D (ℱC.tensor f g) = tensor (ℱC.D f) (ℱC.D g)"
proof -
fix f g
assume f: "ℱC.arr f" and g: "ℱC.arr g"
have fg: "arr (ℱC.D f) ∧ arr (ℱC.D g)"
using f g D.preserves_arr by blast
have "ℱC.D (ℱC.tensor f g) = f ⊗⇩S g"
using tensor⇩S_def by simp
also have "f ⊗⇩S g = ℱC.D (f ⊗ g)"
using f g tensor⇩S_def by simp
also have "... = ℱC.D f ⊗⇩S ℱC.D g"
using f g fg tensor⇩S_def ℱC.T_simp ℱC.diagonalize_tensor arr_char⇩S⇩b⇩C
by (metis (no_types, lifting))
also have "... = tensor (ℱC.D f) (ℱC.D g)"
using fg T_simp by simp
finally show "ℱC.D (ℱC.tensor f g) = tensor (ℱC.D f) (ℱC.D g)"
by blast
qed
show "⋀a b c. ⟦ ℱC.ide a; ℱC.ide b; ℱC.ide c ⟧ ⟹
ℱC.D (ℱC.assoc a b c) = assoc (ℱC.D a) (ℱC.D b) (ℱC.D c)"
proof -
fix a b c
assume a: "ℱC.ide a" and b: "ℱC.ide b" and c: "ℱC.ide c"
have abc: "ide (ℱC.D a) ∧ ide (ℱC.D b) ∧ ide (ℱC.D c)"
using a b c D.preserves_ide by blast
have abc': "ℱC.ide (ℱC.D a) ∧ ℱC.ide (ℱC.D b) ∧ ℱC.ide (ℱC.D c)"
using a b c D.preserves_ide ide_char⇩S⇩b⇩C by simp
have 1: "⋀f g. ℱC.arr f ⟹ ℱC.arr g ⟹ f ⊗⇩S g = ℱC.D (f ⊗ g)"
using tensor⇩S_def by simp
have 2: "⋀f. ide f ⟹ ℱC.ide f" using ide_char⇩S⇩b⇩C by blast
have "assoc (ℱC.D a) (ℱC.D b) (ℱC.D c) = ℱC.D a ⊗⇩S ℱC.D b ⊗⇩S ℱC.D c"
using abc α_ide_simp assoc⇩S_def by simp
also have "... = ℱC.D a ⊗⇩S ℱC.D (ℱC.D b ⊗ ℱC.D c)"
using abc' 1 by auto
also have "... = ℱC.D a ⊗⇩S ℱC.D (b ⊗ c)"
using b c ℱC.diagonalize_tensor by force
also have "... = ℱC.D (ℱC.D a ⊗ ℱC.D (b ⊗ c))"
using 1 b c abc D.preserves_ide ℱC.tensor_preserves_ide ide_char⇩S⇩b⇩C
by simp
also have "... = ℱC.D (a ⊗ b ⊗ c)"
using a b c ℱC.diagonalize_tensor by force
also have "... = ℱC.D 𝖺[a, b, c]"
proof -
have "ℱC.can 𝖺[a, b, c]" using a b c ℱC.can_assoc by simp
hence "ℱC.ide (ℱC.D 𝖺[a, b, c])"
using a b c ℱC.ide_diagonalize_can by simp
moreover have "ℱC.cod (ℱC.D 𝖺[a, b, c]) = ℱC.D (a ⊗ b ⊗ c)"
using a b c ℱC.assoc_in_hom D.preserves_hom
by (metis (no_types, lifting) cod_char⇩S⇩b⇩C in_homE)
ultimately show ?thesis by simp
qed
also have "... = ℱC.D (ℱC.assoc a b c)"
using a b c by simp
finally show "ℱC.D (ℱC.assoc a b c) = assoc (ℱC.D a) (ℱC.D b) (ℱC.D c)"
by blast
qed
qed
lemma diagonalize_is_strict_monoidal_functor:
shows "strict_monoidal_functor ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C
comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
ℱC.D"
..
interpretation φ: natural_isomorphism
ℱC.CC.comp comp D.T⇩DoFF.map D.FoT⇩C.map D.φ
using D.structure_is_natural_isomorphism by simp
text ‹
The diagonalization functor is part of a monoidal equivalence between the
free monoidal category and the subcategory @{term "ℱ⇩SC"}.
›
interpretation E: equivalence_of_categories comp ℱC.comp ℱC.D map ℱC.ν ℱC.μ
using ℱC.is_equivalent_to_strict_subcategory by auto
interpretation D: monoidal_functor ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C
comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
ℱC.D D.φ
using D.monoidal_functor_axioms by metis
interpretation equivalence_of_monoidal_categories comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C
ℱC.D D.φ ℐ
map ℱC.ν ℱC.μ
..
text ‹
The category @{term "ℱC"} is monoidally equivalent to its subcategory @{term "ℱ⇩SC"}.
›
theorem monoidally_equivalent_to_free_monoidal_category:
shows "equivalence_of_monoidal_categories comp T⇩F⇩S⇩M⇩C α⇩F⇩S⇩M⇩C ι⇩F⇩S⇩M⇩C
ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α⇩F⇩M⇩C ℱC.ι⇩F⇩M⇩C
ℱC.D D.φ
map ℱC.ν ℱC.μ"
..
end
text ‹
We next show that the evaluation functor induced on the free monoidal category
generated by @{term C} by a functor @{term V} from @{term C} to a strict monoidal
category @{term D} restricts to a strict monoidal functor on the subcategory @{term "ℱ⇩SC"}.
›
locale strict_evaluation_functor =
D: strict_monoidal_category D T⇩D α⇩D ι⇩D +
evaluation_map C D T⇩D α⇩D ι⇩D V +
ℱC: free_monoidal_category C +
E: evaluation_functor C D T⇩D α⇩D ι⇩D V +
ℱ⇩SC: free_strict_monoidal_category C
for C :: "'c comp" (infixr ‹⋅⇩C› 55)
and D :: "'d comp" (infixr ‹⋅⇩D› 55)
and T⇩D :: "'d * 'd ⇒ 'd"
and α⇩D :: "'d * 'd * 'd ⇒ 'd"
and ι⇩D :: "'d"
and V :: "'c ⇒ 'd"
begin
notation ℱC.in_hom (‹«_ : _ → _»›)
notation ℱ⇩SC.in_hom (‹«_ : _ →⇩S _»›)
definition map
where "map ≡ λf. if ℱ⇩SC.arr f then E.map f else D.null"
interpretation "functor" ℱ⇩SC.comp D map
unfolding map_def
apply unfold_locales
apply simp
using ℱ⇩SC.arr_char⇩S⇩b⇩C E.preserves_arr
apply simp
using ℱ⇩SC.arr_char⇩S⇩b⇩C ℱ⇩SC.dom_char⇩S⇩b⇩C E.preserves_dom
apply simp
using ℱ⇩SC.arr_char⇩S⇩b⇩C ℱ⇩SC.cod_char⇩S⇩b⇩C E.preserves_cod
apply simp
using ℱ⇩SC.arr_char⇩S⇩b⇩C ℱ⇩SC.dom_char⇩S⇩b⇩C ℱ⇩SC.cod_char⇩S⇩b⇩C ℱ⇩SC.comp_char E.preserves_comp
by (elim ℱ⇩SC.seqE, auto)
lemma is_functor:
shows "functor ℱ⇩SC.comp D map" ..
text ‹
Every canonical arrow is an equivalence class of canonical terms.
The evaluations in ‹D› of all such terms are identities,
due to the strictness of ‹D›.
›
lemma ide_eval_Can:
shows "Can t ⟹ D.ide ⦃t⦄"
proof (induct t)
show "⋀x. Can ❙⟨x❙⟩ ⟹ D.ide ⦃❙⟨x❙⟩⦄" by simp
show "Can ❙ℐ ⟹ D.ide ⦃❙ℐ⦄" by simp
show "⋀t1 t2. ⟦ Can t1 ⟹ D.ide ⦃t1⦄; Can t2 ⟹ D.ide ⦃t2⦄; Can (t1 ❙⊗ t2) ⟧ ⟹
D.ide ⦃t1 ❙⊗ t2⦄"
by simp
show "⋀t1 t2. ⟦ Can t1 ⟹ D.ide ⦃t1⦄; Can t2 ⟹ D.ide ⦃t2⦄; Can (t1 ❙⋅ t2) ⟧ ⟹
D.ide ⦃t1 ❙⋅ t2⦄"
proof -
fix t1 t2
assume t1: "Can t1 ⟹ D.ide ⦃t1⦄"
and t2: "Can t2 ⟹ D.ide ⦃t2⦄"
and t12: "Can (t1 ❙⋅ t2)"
show "D.ide ⦃t1 ❙⋅ t2⦄"
using t1 t2 t12 Can_implies_Arr eval_in_hom [of t1] eval_in_hom [of t2] D.comp_ide_arr
by fastforce
qed
show "⋀t. (Can t ⟹ D.ide ⦃t⦄) ⟹ Can ❙𝗅❙[t❙] ⟹ D.ide ⦃❙𝗅❙[t❙]⦄"
using D.strict_lunit by simp
show "⋀t. (Can t ⟹ D.ide ⦃t⦄) ⟹ Can ❙𝗅⇧-⇧1❙[t❙] ⟹ D.ide ⦃❙𝗅⇧-⇧1❙[t❙]⦄"
using D.strict_lunit by simp
show "⋀t. (Can t ⟹ D.ide ⦃t⦄) ⟹ Can ❙𝗋❙[t❙] ⟹ D.ide ⦃❙𝗋❙[t❙]⦄"
using D.strict_runit by simp
show "⋀t. (Can t ⟹ D.ide ⦃t⦄) ⟹ Can ❙𝗋⇧-⇧1❙[t❙] ⟹ D.ide ⦃❙𝗋⇧-⇧1❙[t❙]⦄"
using D.strict_runit by simp
fix t1 t2 t3
assume t1: "Can t1 ⟹ D.ide ⦃t1⦄"
and t2: "Can t2 ⟹ D.ide ⦃t2⦄"
and t3: "Can t3 ⟹ D.ide ⦃t3⦄"
show "Can ❙𝖺❙[t1, t2, t3❙] ⟹ D.ide ⦃❙𝖺❙[t1, t2, t3❙]⦄"
proof -
assume "Can ❙𝖺❙[t1, t2, t3❙]"
hence t123: "D.ide ⦃t1⦄ ∧ D.ide ⦃t2⦄ ∧ D.ide ⦃t3⦄"
using t1 t2 t3 by simp
have "⦃❙𝖺❙[t1, t2, t3❙]⦄ = ⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄"
using t123 D.strict_assoc D.assoc_in_hom [of "⦃t1⦄" "⦃t2⦄" "⦃t3⦄"] apply simp
by (elim D.in_homE, simp)
thus ?thesis using t123 by simp
qed
show "Can ❙𝖺⇧-⇧1❙[t1, t2, t3❙] ⟹ D.ide ⦃❙𝖺⇧-⇧1❙[t1, t2, t3❙]⦄"
proof -
assume "Can ❙𝖺⇧-⇧1❙[t1, t2, t3❙]"
hence t123: "Can t1 ∧ Can t2 ∧ Can t3 ∧ D.ide ⦃t1⦄ ∧ D.ide ⦃t2⦄ ∧ D.ide ⦃t3⦄"
using t1 t2 t3 by simp
have "⦃❙𝖺⇧-⇧1❙[t1, t2, t3❙]⦄
= D.inv 𝖺⇩D[D.cod ⦃t1⦄, D.cod ⦃t2⦄, D.cod ⦃t3⦄] ⋅⇩D (⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄)"
using t123 eval_Assoc' [of t1 t2 t3] Can_implies_Arr by simp
also have "... = ⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄"
proof -
have "D.dom 𝖺⇩D[⦃t1⦄, ⦃t2⦄, ⦃t3⦄] = ⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄"
proof -
have "D.dom 𝖺⇩D[⦃t1⦄, ⦃t2⦄, ⦃t3⦄] = D.cod 𝖺⇩D[⦃t1⦄, ⦃t2⦄, ⦃t3⦄]"
using t123 D.strict_assoc by simp
also have "... = ⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄"
using t123 by simp
finally show ?thesis by blast
qed
thus ?thesis
using t123 D.strict_assoc D.comp_arr_dom by auto
qed
finally have "⦃❙𝖺⇧-⇧1❙[t1, t2, t3❙]⦄ = ⦃t1⦄ ⊗⇩D ⦃t2⦄ ⊗⇩D ⦃t3⦄" by blast
thus ?thesis using t123 by auto
qed
qed
lemma ide_eval_can:
assumes "ℱC.can f"
shows "D.ide (E.map f)"
proof -
have "f = ℱC.mkarr (ℱC.rep f)"
using assms ℱC.can_implies_arr ℱC.mkarr_rep by blast
moreover have 1: "Can (ℱC.rep f)"
using assms ℱC.Can_rep_can by simp
moreover have "D.ide ⦃ℱC.rep f⦄"
using assms ide_eval_Can by (simp add: 1)
ultimately show ?thesis using assms ℱC.can_implies_arr E.map_def by force
qed
text ‹
Diagonalization transports formal arrows naturally along reductions,
which are canonical terms and therefore evaluate to identities of ‹D›.
It follows that the evaluation in ‹D› of a formal arrow is equal to the
evaluation of its diagonalization.
›
lemma map_diagonalize:
assumes f: "ℱC.arr f"
shows "E.map (ℱC.D f) = E.map f"
proof -
interpret EQ: equivalence_of_categories
ℱ⇩SC.comp ℱC.comp ℱC.D ℱ⇩SC.map ℱC.ν ℱC.μ
using ℱC.is_equivalent_to_strict_subcategory by auto
have 1: "ℱC.seq (ℱ⇩SC.map (ℱC.D f)) (ℱC.ν (ℱC.dom f))"
proof
show "«ℱC.ν (ℱC.dom f) : ℱC.dom f → ℱC.D (ℱC.dom f)»"
using f ℱ⇩SC.map_simp EQ.F.preserves_arr
by (intro ℱC.in_homI, simp_all)
show "«ℱ⇩SC.map (ℱC.D f) : ℱC.D (ℱC.dom f) → ℱC.cod (ℱC.D f)»"
by (metis (no_types, lifting) EQ.F.preserves_dom EQ.F.preserves_reflects_arr
ℱ⇩SC.arr_iff_in_hom ℱ⇩SC.cod_simp ℱ⇩SC.in_hom_char⇩S⇩b⇩C ℱ⇩SC.map_simp f)
qed
have "E.map (ℱC.ν (ℱC.cod f)) ⋅⇩D E.map f =
E.map (ℱC.D f) ⋅⇩D E.map (ℱC.ν (ℱC.dom f))"
proof -
have "E.map (ℱC.ν (ℱC.cod f)) ⋅⇩D E.map f = E.map (ℱC.ν (ℱC.cod f) ⋅ f)"
using f by simp
also have "... = E.map (ℱC.D f ⋅ ℱC.ν (ℱC.dom f))"
using f EQ.η.naturality ℱ⇩SC.map_simp EQ.F.preserves_arr by simp
also have "... = E.map (ℱ⇩SC.map (ℱC.D f)) ⋅⇩D E.map (ℱC.ν (ℱC.dom f))"
using f 1 E.as_nat_trans.preserves_comp_2 EQ.F.preserves_arr ℱ⇩SC.map_simp
by (metis (no_types, lifting))
also have "... = E.map (ℱC.D f) ⋅⇩D E.map (ℱC.ν (ℱC.dom f))"
using f EQ.F.preserves_arr ℱ⇩SC.map_simp by simp
finally show ?thesis by blast
qed
moreover have "⋀a. ℱC.ide a ⟹ D.ide (E.map (ℱC.ν a))"
using ℱC.ν_def ℱC.Arr_rep Arr_implies_Ide_Cod Can_red ℱC.can_mkarr_Can
ide_eval_can
by (metis (no_types, lifting) EQ.η.preserves_reflects_arr ℱC.seqE
ℱC.comp_preserves_can ℱC.ideD(1) ℱC.ide_implies_can)
moreover have "D.cod (E.map f) = D.dom (E.map (ℱC.ν (ℱC.cod f)))"
using f E.preserves_hom EQ.η.preserves_hom by simp
moreover have "D.dom (E.map (ℱC.D f)) = D.cod (E.map (ℱC.ν (ℱC.dom f)))"
using f 1 E.preserves_seq EQ.F.preserves_arr ℱ⇩SC.map_simp by auto
ultimately show ?thesis
using f D.comp_arr_dom D.ideD D.arr_dom_iff_arr E.as_nat_trans.is_natural_2
by (metis E.preserves_cod ℱC.ide_cod ℱC.ide_dom)
qed
lemma strictly_preserves_tensor:
assumes "ℱ⇩SC.arr f" and "ℱ⇩SC.arr g"
shows "map (ℱ⇩SC.tensor f g) = map f ⊗⇩D map g"
proof -
have 1: "ℱC.arr (f ⊗ g)"
using assms ℱ⇩SC.arr_char⇩S⇩b⇩C ℱC.tensor_in_hom by auto
have 2: "ℱ⇩SC.arr (ℱ⇩SC.tensor f g)"
using assms ℱ⇩SC.tensor_in_hom [of f g] ℱ⇩SC.T_simp by fastforce
have "map (ℱ⇩SC.tensor f g) = E.map (f ⊗ g)"
proof -
have "map (ℱ⇩SC.tensor f g) = map (f ⊗⇩S g)"
using assms ℱ⇩SC.T_simp by simp
also have "... = map (ℱC.D (f ⊗ g))"
using assms ℱC.tensor⇩F⇩M⇩C_def ℱ⇩SC.tensor⇩S_def ℱ⇩SC.arr_char⇩S⇩b⇩C by force
also have "... = E.map (f ⊗ g)"
proof -
interpret Diag: "functor" ℱC.comp ℱ⇩SC.comp ℱC.D
using ℱC.diagonalize_is_functor by auto
show ?thesis
using assms 1 map_diagonalize [of "f ⊗ g"] Diag.preserves_arr map_def by simp
qed
finally show ?thesis by blast
qed
thus ?thesis
using assms ℱ⇩SC.arr_char⇩S⇩b⇩C E.strictly_preserves_tensor map_def by simp
qed
lemma is_strict_monoidal_functor:
shows "strict_monoidal_functor ℱ⇩SC.comp ℱ⇩SC.T⇩F⇩S⇩M⇩C ℱ⇩SC.α ℱ⇩SC.ι D T⇩D α⇩D ι⇩D map"
proof
show "⋀f g. ℱ⇩SC.arr f ⟹ ℱ⇩SC.arr g ⟹ map (ℱ⇩SC.tensor f g) = map f ⊗⇩D map g"
using strictly_preserves_tensor by fast
show "map ℱ⇩SC.ι = ι⇩D"
using ℱ⇩SC.arr_unity ℱ⇩SC.ι_def map_def E.map_def ℱC.rep_mkarr E.eval_norm D.strict_unit
by auto
fix a b c
assume a: "ℱ⇩SC.ide a" and b: "ℱ⇩SC.ide b" and c: "ℱ⇩SC.ide c"
show "map (ℱ⇩SC.assoc a b c) = 𝖺⇩D[map a, map b, map c]"
proof -
have "map (ℱ⇩SC.assoc a b c) = map a ⊗⇩D map b ⊗⇩D map c"
using a b c ℱ⇩SC.α_def ℱ⇩SC.assoc⇩S_def ℱ⇩SC.arr_tensor ℱ⇩SC.T_simp ℱ⇩SC.ideD(1)
strictly_preserves_tensor ℱ⇩SC.α_ide_simp
by presburger
also have "... = 𝖺⇩D[map a, map b, map c]"
using a b c D.strict_assoc D.assoc_in_hom [of "map a" "map b" "map c"] by auto
finally show ?thesis by blast
qed
qed
end
sublocale strict_evaluation_functor ⊆
strict_monoidal_functor ℱ⇩SC.comp ℱ⇩SC.T⇩F⇩S⇩M⇩C ℱ⇩SC.α ℱ⇩SC.ι D T⇩D α⇩D ι⇩D map
using is_strict_monoidal_functor by auto
locale strict_monoidal_extension_to_free_strict_monoidal_category =
C: category C +
monoidal_language C +
ℱ⇩SC: free_strict_monoidal_category C +
strict_monoidal_extension C ℱ⇩SC.comp ℱ⇩SC.T⇩F⇩S⇩M⇩C ℱ⇩SC.α ℱ⇩SC.ι D T⇩D α⇩D ι⇩D
ℱ⇩SC.inclusion_of_generators V F
for C :: "'c comp" (infixr ‹⋅⇩C› 55)
and D :: "'d comp" (infixr ‹⋅⇩D› 55)
and T⇩D :: "'d * 'd ⇒ 'd"
and α⇩D :: "'d * 'd * 'd ⇒ 'd"
and ι⇩D :: "'d"
and V :: "'c ⇒ 'd"
and F :: "'c free_monoidal_category.arr ⇒ 'd"
sublocale strict_evaluation_functor ⊆
strict_monoidal_extension C ℱ⇩SC.comp ℱ⇩SC.T⇩F⇩S⇩M⇩C ℱ⇩SC.α ℱ⇩SC.ι D T⇩D α⇩D ι⇩D
ℱ⇩SC.inclusion_of_generators V map
proof -
interpret V: "functor" C ℱ⇩SC.comp ℱ⇩SC.inclusion_of_generators
using ℱ⇩SC.inclusion_is_functor by auto
show "strict_monoidal_extension C ℱ⇩SC.comp ℱ⇩SC.T⇩F⇩S⇩M⇩C ℱ⇩SC.α ℱ⇩SC.ι D T⇩D α⇩D ι⇩D
ℱ⇩SC.inclusion_of_generators V map"
proof
show "∀f. C.arr f ⟶ map (ℱ⇩SC.inclusion_of_generators f) = V f"
using V.preserves_arr E.is_extension map_def ℱ⇩SC.inclusion_of_generators_def by simp
qed
qed
context free_strict_monoidal_category
begin
text ‹
We now have the main result of this section: the evaluation functor on ‹ℱ⇩SC›
induced by a functor @{term V} from @{term C} to a strict monoidal category @{term D}
is the unique strict monoidal extension of @{term V} to ‹ℱ⇩SC›.
›
theorem is_free:
assumes "strict_monoidal_category D T⇩D α⇩D ι⇩D"
and "strict_monoidal_extension_to_free_strict_monoidal_category C D T⇩D α⇩D ι⇩D V F"
shows "F = strict_evaluation_functor.map C D T⇩D α⇩D ι⇩D V"
proof -
interpret D: strict_monoidal_category D T⇩D α⇩D ι⇩D
using assms(1) by auto
text ‹
Let @{term F} be a given extension of V to a strict monoidal functor defined on
‹ℱ⇩SC›.
›
interpret F: strict_monoidal_extension_to_free_strict_monoidal_category
C D T⇩D α⇩D ι⇩D V F
using assms(2) by auto
text ‹
Let @{term E⇩S} be the evaluation functor from ‹ℱ⇩SC› to @{term D}
induced by @{term V}. Then @{term E⇩S} is also a strict monoidal extension of @{term V}.
›
interpret E⇩S: strict_evaluation_functor C D T⇩D α⇩D ι⇩D V ..
text ‹
Let @{term D} be the strict monoidal functor @{term "ℱC.D"} that projects
‹ℱC› to the subcategory ‹ℱ⇩SC›.
›
interpret D: "functor" ℱC.comp comp ℱC.D
using ℱC.diagonalize_is_functor by auto
interpret D: strict_monoidal_functor ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι
comp T⇩F⇩S⇩M⇩C α ι
ℱC.D
using diagonalize_is_strict_monoidal_functor by blast
text ‹
The composite functor ‹F o D› is also an extension of @{term V}
to a strict monoidal functor on ‹ℱC›.
›
interpret FoD: composite_functor ℱC.comp comp D ℱC.D F ..
interpret FoD: strict_monoidal_functor
ℱC.comp ℱC.T⇩F⇩M⇩C ℱC.α ℱC.ι D T⇩D α⇩D ι⇩D ‹F o ℱC.D›
using D.strict_monoidal_functor_axioms F.strict_monoidal_functor_axioms
strict_monoidal_functors_compose
by fast
interpret FoD: strict_monoidal_extension_to_free_monoidal_category
C D T⇩D α⇩D ι⇩D V FoD.map
proof
show "∀f. C.arr f ⟶ FoD.map (ℱC.inclusion_of_generators f) = V f"
proof -
have "⋀f. C.arr f ⟹ FoD.map (ℱC.inclusion_of_generators f) = V f"
proof -
fix f
assume f: "C.arr f"
have "FoD.map (ℱC.inclusion_of_generators f)
= F (ℱC.D (ℱC.inclusion_of_generators f))"
using f by simp
also have "... = F (inclusion_of_generators f)"
using f ℱC.strict_arr_char' F.I.preserves_arr inclusion_of_generators_def by simp
also have "... = V f"
using f F.is_extension by simp
finally show "FoD.map (ℱC.inclusion_of_generators f) = V f"
by blast
qed
thus ?thesis by blast
qed
qed
text ‹
By the freeness of ‹ℱC›, we have that ‹F o D›
is equal to the evaluation functor @{term "E⇩S.E.map"} induced by @{term V}
on ‹ℱC›. Moreover, @{term E⇩S.map} coincides with @{term "E⇩S.E.map"} on
‹ℱ⇩SC› and ‹F o D› coincides with @{term F} on
‹ℱ⇩SC›. Therefore, @{term F} coincides with @{term E} on their common
domain ‹ℱ⇩SC›, showing @{term "F = E⇩S.map"}.
›
have "⋀f. arr f ⟹ F f = E⇩S.map f"
using ℱC.strict_arr_char' ℱC.is_free [of D] E⇩S.E.evaluation_functor_axioms
FoD.strict_monoidal_extension_to_free_monoidal_category_axioms E⇩S.map_def
by simp
moreover have "⋀f. ¬arr f ⟹ F f = E⇩S.map f"
using F.is_extensional E⇩S.is_extensional arr_char⇩S⇩b⇩C by auto
ultimately show "F = E⇩S.map" by blast
qed
end
end