Theory MonoidalCategory
chapter "Monoidal Category"
text_raw‹
\label{monoidal-category-chap}
›
text ‹
In this theory, we define the notion ``monoidal category,'' and develop consequences of
the definition. The main result is a proof of MacLane's coherence theorem.
›
theory MonoidalCategory
imports Category3.EquivalenceOfCategories
begin
section "Monoidal Category"
text ‹
A typical textbook presentation defines a monoidal category to be a category @{term C}
equipped with (among other things) a binary ``tensor product'' functor ‹⊗: C × C → C›
and an ``associativity'' natural isomorphism ‹α›, whose components are isomorphisms
‹α (a, b, c): (a ⊗ b) ⊗ c → a ⊗ (b ⊗ c)› for objects ‹a›, ‹b›,
and ‹c› of ‹C›. This way of saying things avoids an explicit definition of
the functors that are the domain and codomain of ‹α› and, in particular, what category
serves as the domain of these functors. The domain category is in fact the product
category ‹C × C × C› and the domain and codomain of ‹α› are the functors
‹T o (T × C): C × C × C → C› and ‹T o (C × T): C × C × C → C›.
In a formal development, though, we can't gloss over the fact that
‹C × C × C› has to mean either ‹C × (C × C)› or ‹(C × C) × C›,
which are not formally identical, and that associativities are somehow involved in the
definitions of the functors ‹T o (T × C)› and ‹T o (C × T)›.
Here we use the @{locale binary_endofunctor} locale to codify our choices about what
‹C × C × C›, ‹T o (T × C)›, and ‹T o (C × T)› actually mean.
In particular, we choose ‹C × C × C› to be ‹C × (C × C)› and define the
functors ‹T o (T × C)›, and ‹T o (C × T)› accordingly.
›
text ‹
Our primary definition for ``monoidal category'' follows the somewhat non-traditional
development in \<^cite>‹"Etingof15"›. There a monoidal category is defined to be a category
‹C› equipped with a binary \emph{tensor product} functor ‹T: C × C → C›,
an \emph{associativity isomorphism}, which is a natural isomorphism
‹α: T o (T × C) → T o (C × T)›, a \emph{unit object} ‹ℐ› of ‹C›,
and an isomorphism ‹ι: T (ℐ, ℐ) → ℐ›, subject to two axioms:
the \emph{pentagon axiom}, which expresses the commutativity of certain pentagonal diagrams
involving components of ‹α›, and the left and right \emph{unit axioms}, which state
that the endofunctors ‹T (ℐ, -)› and ‹T (-, ℐ)› are equivalences of categories.
This definition is formalized in the ‹monoidal_category› locale.
In more traditional developments, the definition of monoidal category involves additional
left and right \emph{unitor} isomorphisms ‹λ› and ‹ρ› and associated axioms
involving their components.
However, as is shown in \<^cite>‹"Etingof15"› and formalized here, the unitors are uniquely
determined by ‹α› and their values ‹λ(ℐ)› and ‹ρ(ℐ)› at ‹ℐ›,
which coincide. Treating ‹λ› and ‹ρ› as defined notions results in a more
economical basic definition of monoidal category that requires less data to be given,
and has a similar effect on the definition of ``monoidal functor.''
Moreover, in the context of the formalization of categories that we use here,
the unit object ‹ℐ› also need not be given separately, as it can be obtained as the
codomain of the isomorphism ‹ι›.
›
locale monoidal_category =
category C +
CC: product_category C C +
CCC: product_category C CC.comp +
T: binary_endofunctor C T +
α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α +
L: equivalence_functor C C "λf. T (cod ι, f)" +
R: equivalence_functor C C "λf. T (f, cod ι)"
for C :: "'a comp" (infixr ‹⋅› 55)
and T :: "'a * 'a ⇒ 'a"
and α :: "'a * 'a * 'a ⇒ 'a"
and ι :: 'a +
assumes unit_in_hom_ax: "«ι : T (cod ι, cod ι) → cod ι»"
and unit_is_iso: "iso ι"
and pentagon: "⟦ ide a; ide b; ide c; ide d ⟧ ⟹
T (a, α (b, c, d)) ⋅ α (a, T (b, c), d) ⋅ T (α (a, b, c), d) =
α (a, b, T (c, d)) ⋅ α (T (a, b), c, d)"
begin
text‹
We now define helpful notation and abbreviations to improve readability.
We did not define and use the notation ‹⊗› for the tensor product
in the definition of the locale because to define ‹⊗› as a binary
operator requires that it be in curried form, whereas for ‹T›
to be a binary functor requires that it take a pair as its argument.
›
abbreviation unity :: 'a (‹ℐ›)
where "unity ≡ cod ι"
abbreviation L :: "'a ⇒ 'a"
where "L f ≡ T (ℐ, f)"
abbreviation R :: "'a ⇒ 'a"
where "R f ≡ T (f, ℐ)"
abbreviation tensor (infixr ‹⊗› 53)
where "f ⊗ g ≡ T (f, g)"
abbreviation assoc (‹𝖺[_, _, _]›)
where "𝖺[a, b, c] ≡ α (a, b, c)"
text‹
In HOL we can just give the definitions of the left and right unitors ``up front''
without any preliminary work. Later we will have to show that these definitions
have the right properties. The next two definitions define the values of the
unitors when applied to identities; that is, their components as natural transformations.
›
definition lunit (‹𝗅[_]›)
where "lunit a ≡ THE f. «f : ℐ ⊗ a → a» ∧ ℐ ⊗ f = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
definition runit (‹𝗋[_]›)
where "runit a ≡ THE f. «f : a ⊗ ℐ → a» ∧ f ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
text‹
We now embark upon a development of the consequences of the monoidal category axioms.
One of our objectives is to be able to show that an interpretation of the
‹monoidal_category› locale induces an interpretation of a locale corresponding
to a more traditional definition of monoidal category.
Another is to obtain the facts we need to prove the coherence theorem.
›
lemma unit_in_hom [intro]:
shows "«ι : ℐ ⊗ ℐ → ℐ»"
using unit_in_hom_ax by force
lemma ide_unity [simp]:
shows "ide ℐ"
using unit_in_hom by auto
lemma tensor_in_hom [simp]:
assumes "«f : a → b»" and "«g : c → d»"
shows "«f ⊗ g : a ⊗ c → b ⊗ d»"
using assms T.preserves_hom CC.arr_char by simp
lemma tensor_in_homI [intro]:
assumes "«f : a → b»" and "«g : c → d»" and "x = a ⊗ c" and "y = b ⊗ d"
shows "«f ⊗ g : x → y»"
using assms tensor_in_hom
by force
lemma arr_tensor [simp]:
assumes "arr f" and "arr g"
shows "arr (f ⊗ g)"
using assms by simp
lemma dom_tensor [simp]:
assumes "«f : a → b»" and "«g : c → d»"
shows "dom (f ⊗ g) = a ⊗ c"
using assms by fastforce
lemma cod_tensor [simp]:
assumes "«f : a → b»" and "«g : c → d»"
shows "cod (f ⊗ g) = b ⊗ d"
using assms by fastforce
lemma tensor_preserves_ide [simp]:
assumes "ide a" and "ide b"
shows "ide (a ⊗ b)"
using assms T.preserves_ide CC.ide_char by simp
lemma tensor_preserves_iso [simp]:
assumes "iso f" and "iso g"
shows "iso (f ⊗ g)"
using assms by simp
lemma inv_tensor [simp]:
assumes "iso f" and "iso g"
shows "inv (f ⊗ g) = inv f ⊗ inv g"
using assms T.preserves_inv by auto
lemma interchange:
assumes "seq h g" and "seq h' g'"
shows "(h ⊗ h') ⋅ (g ⊗ g') = h ⋅ g ⊗ h' ⋅ g'"
using assms T.preserves_comp [of "(h, h')" "(g, g')"] by simp
lemma α_simp:
assumes "arr f" and "arr g" and "arr h"
shows "α (f, g, h) = (f ⊗ g ⊗ h) ⋅ 𝖺[dom f, dom g, dom h]"
using assms α.is_natural_1 [of "(f, g, h)"] by simp
lemma assoc_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ b ⊗ c»"
using assms CCC.in_homE by auto
lemma arr_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺[a, b, c]"
using assms assoc_in_hom 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 simp
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 simp
lemma assoc_naturality:
assumes "arr f0" and "arr f1" and "arr f2"
shows "𝖺[cod f0, cod f1, cod f2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
(f0 ⊗ f1 ⊗ f2) ⋅ 𝖺[dom f0, dom f1, dom f2]"
using assms α.naturality by auto
lemma iso_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "iso 𝖺[a, b, c]"
using assms α.preserves_iso by simp
text‹
The next result uses the fact that the functor ‹L› is an equivalence
(and hence faithful) to show the existence of a unique solution to the characteristic
equation used in the definition of a component @{term "𝗅[a]"} of the left unitor.
It follows that @{term "𝗅[a]"}, as given by our definition using definite description,
satisfies this characteristic equation and is therefore uniquely determined by
by ‹⊗›, @{term α}, and ‹ι›.
›
lemma lunit_char:
assumes "ide a"
shows "«𝗅[a] : ℐ ⊗ a → a»" and "ℐ ⊗ 𝗅[a] = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
and "∃!f. «f : ℐ ⊗ a → a» ∧ ℐ ⊗ f = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
proof -
obtain F η ε where L: "equivalence_of_categories C C F (λf. ℐ ⊗ f) η ε"
using L.induces_equivalence by auto
interpret L: equivalence_of_categories C C F ‹λf. ℐ ⊗ f› η ε
using L by auto
let ?P = "λf. «f : ℐ ⊗ a → a» ∧ ℐ ⊗ f = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
show "∃!f. ?P f"
proof -
have "∃f. ?P f"
proof -
have "«(ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a] : ℐ ⊗ ℐ ⊗ a → ℐ ⊗ a»"
proof
show "«ι ⊗ a : (ℐ ⊗ ℐ) ⊗ a → ℐ ⊗ a»"
using assms ide_in_hom by blast
show "«inv 𝖺[ℐ, ℐ, a] : ℐ ⊗ ℐ ⊗ a → (ℐ ⊗ ℐ) ⊗ a»"
using assms by auto
qed
moreover have "ide (ℐ ⊗ a)" using assms by simp
ultimately show ?thesis
using assms L.is_full by blast
qed
moreover have "⋀f f'. ?P f ⟹ ?P f' ⟹ f = f'"
by (metis L.is_faithful in_homE)
ultimately show ?thesis by blast
qed
hence 1: "?P 𝗅[a]"
unfolding lunit_def using theI' [of ?P] by auto
show "«𝗅[a] : ℐ ⊗ a → a»" using 1 by fast
show "ℐ ⊗ 𝗅[a] = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]" using 1 by fast
qed
lemma lunit_in_hom [intro]:
assumes "ide a"
shows "«𝗅[a] : ℐ ⊗ a → a»"
using assms lunit_char(1) by blast
lemma arr_lunit [simp]:
assumes "ide a"
shows "arr 𝗅[a]"
using assms lunit_in_hom by auto
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
text‹
As the right-hand side of the characteristic equation for @{term "ℐ ⊗ 𝗅[a]"}
is an isomorphism, and the equivalence functor ‹L› reflects isomorphisms,
it follows that @{term "𝗅[a]"} is an isomorphism.
›
lemma iso_lunit [simp]:
assumes "ide a"
shows "iso 𝗅[a]"
using assms lunit_char(2) unit_is_iso ide_unity isos_compose iso_assoc iso_inv_iso
unit_in_hom L.reflects_iso arr_lunit arr_tensor ideD(1) ide_is_iso lunit_in_hom
tensor_preserves_iso
by metis
text‹
To prove that an arrow @{term f} is equal to @{term "𝗅[a]"} we need only show
that it is parallel to @{term "𝗅[a]"} and that @{term "ℐ ⊗ f"} satisfies the same
characteristic equation as @{term "ℐ ⊗ 𝗅[a]"} does.
›
lemma lunit_eqI:
assumes "«f : ℐ ⊗ a → a»" and "ℐ ⊗ f = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
shows "f = 𝗅[a]"
proof -
have "ide a" using assms(1) by auto
thus ?thesis
using assms lunit_char the1_equality by blast
qed
text‹
The next facts establish the corresponding results for the components of the
right unitor.
›
lemma runit_char:
assumes "ide a"
shows "«𝗋[a] : a ⊗ ℐ → a»" and "𝗋[a] ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
and "∃!f. «f : a ⊗ ℐ → a» ∧ f ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
proof -
obtain F η ε where R: "equivalence_of_categories C C F (λf. f ⊗ ℐ) η ε"
using R.induces_equivalence by auto
interpret R: equivalence_of_categories C C F ‹λf. f ⊗ ℐ› η ε
using R by auto
let ?P = "λf. «f : a ⊗ ℐ → a» ∧ f ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
show "∃!f. ?P f"
proof -
have "∃f. ?P f"
proof -
have "«(a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ] : (a ⊗ ℐ) ⊗ ℐ → a ⊗ ℐ»"
using assms by fastforce
moreover have "ide (a ⊗ ℐ)" using assms by simp
ultimately show ?thesis
using assms R.is_full [of a "a ⊗ ℐ" "(a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"] by blast
qed
moreover have "⋀f f'. ?P f ⟹ ?P f' ⟹ f = f'"
by (metis R.is_faithful in_homE)
ultimately show ?thesis by blast
qed
hence 1: "?P 𝗋[a]" unfolding runit_def using theI' [of ?P] by fast
show "«𝗋[a] : a ⊗ ℐ → a»" using 1 by fast
show "𝗋[a] ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]" using 1 by fast
qed
lemma runit_in_hom [intro]:
assumes "ide a"
shows "«𝗋[a] : a ⊗ ℐ → a»"
using assms runit_char(1) by blast
lemma arr_runit [simp]:
assumes "ide a"
shows "arr 𝗋[a]"
using assms runit_in_hom by blast
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 runit_eqI:
assumes "«f : a ⊗ ℐ → a»" and "f ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
shows "f = 𝗋[a]"
proof -
have "ide a" using assms(1) by auto
thus ?thesis
using assms runit_char the1_equality by blast
qed
lemma iso_runit [simp]:
assumes "ide a"
shows "iso 𝗋[a]"
using assms unit_is_iso iso_inv_iso isos_compose ide_is_iso R.preserves_reflects_arr
arrI ide_unity iso_assoc runit_char tensor_preserves_iso R.reflects_iso
by metis
text‹
We can now show that the components of the left and right unitors have the
naturality properties required of a natural transformation.
›
lemma lunit_naturality:
assumes "arr f"
shows "𝗅[cod f] ⋅ (ℐ ⊗ f) = f ⋅ 𝗅[dom f]"
proof -
interpret α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..
have par: "par (𝗅[cod f] ⋅ (ℐ ⊗ f)) (f ⋅ 𝗅[dom f])"
using assms by simp
moreover have "ℐ ⊗ 𝗅[cod f] ⋅ (ℐ ⊗ f) = ℐ ⊗ f ⋅ 𝗅[dom f]"
proof -
have "ℐ ⊗ 𝗅[cod f] ⋅ (ℐ ⊗ f) = ((ι ⊗ cod f) ⋅ ((ℐ ⊗ ℐ) ⊗ f)) ⋅ inv 𝖺[ℐ, ℐ, dom f]"
using assms interchange [of ℐ ℐ "ℐ ⊗ f" "𝗅[cod f]"] lunit_char(2)
α'.naturality [of "(ℐ, ℐ, f)"] comp_assoc
by auto
also have "... = ((ℐ ⊗ f) ⋅ (ι ⊗ dom f)) ⋅ inv 𝖺[ℐ, ℐ, dom f]"
using assms interchange comp_arr_dom comp_cod_arr unit_in_hom by auto
also have "... = (ℐ ⊗ f) ⋅ (ℐ ⊗ 𝗅[dom f])"
using assms lunit_char(2) comp_assoc by auto
also have "... = ℐ ⊗ f ⋅ 𝗅[dom f]"
using assms interchange L.preserves_comp par by metis
finally show ?thesis by blast
qed
ultimately show "𝗅[cod f] ⋅ (ℐ ⊗ f) = f ⋅ 𝗅[dom f]"
using L.is_faithful by metis
qed
lemma runit_naturality:
assumes "arr f"
shows "𝗋[cod f] ⋅ (f ⊗ ℐ) = f ⋅ 𝗋[dom f]"
proof -
have par: "par (𝗋[cod f] ⋅ (f ⊗ ℐ)) (f ⋅ 𝗋[dom f])"
using assms by force
moreover have "𝗋[cod f] ⋅ (f ⊗ ℐ) ⊗ ℐ = f ⋅ 𝗋[dom f] ⊗ ℐ"
proof -
have "𝗋[cod f] ⋅ (f ⊗ ℐ) ⊗ ℐ = (cod f ⊗ ι) ⋅ 𝖺[cod f, ℐ, ℐ] ⋅ ((f ⊗ ℐ) ⊗ ℐ)"
using assms interchange [of ℐ ℐ "ℐ ⊗ f" "𝗋[cod f]"] runit_char(2)
comp_assoc
by auto
also have "... = (cod f ⊗ ι) ⋅ (f ⊗ ℐ ⊗ ℐ) ⋅ 𝖺[dom f, ℐ, ℐ]"
using assms α.naturality [of "(f, ℐ, ℐ)"] by auto
also have "... = ((cod f ⊗ ι) ⋅ (f ⊗ ℐ ⊗ ℐ)) ⋅ 𝖺[dom f, ℐ, ℐ]"
using comp_assoc by simp
also have "... = ((f ⊗ ℐ) ⋅ (dom f ⊗ ι)) ⋅ 𝖺[dom f, ℐ, ℐ]"
using assms unit_in_hom interchange comp_arr_dom comp_cod_arr by auto
also have "... = (f ⊗ ℐ) ⋅ (𝗋[dom f] ⊗ ℐ)"
using assms runit_char comp_assoc by auto
also have "... = f ⋅ 𝗋[dom f] ⊗ ℐ"
using assms interchange R.preserves_comp par by metis
finally show ?thesis by blast
qed
ultimately show "𝗋[cod f] ⋅ (f ⊗ ℐ) = f ⋅ 𝗋[dom f]"
using R.is_faithful by metis
qed
text‹
The next two definitions extend the unitors to all arrows, not just identities.
Unfortunately, the traditional symbol ‹λ› for the left unitor is already
reserved for a higher purpose, so we have to make do with a poor substitute.
›
abbreviation 𝔩
where "𝔩 f ≡ if arr f then f ⋅ 𝗅[dom f] else null"
abbreviation ρ
where "ρ f ≡ if arr f then f ⋅ 𝗋[dom f] else null"
lemma 𝔩_ide_simp:
assumes "ide a"
shows "𝔩 a = 𝗅[a]"
using assms lunit_char comp_cod_arr ide_in_hom by (metis in_homE)
lemma ρ_ide_simp:
assumes "ide a"
shows "ρ a = 𝗋[a]"
using assms runit_char [of a] comp_cod_arr by auto
end
context monoidal_category
begin
sublocale 𝔩: natural_transformation C C L map 𝔩
proof -
interpret 𝔩: transformation_by_components C C L map ‹λa. 𝗅[a]›
using lunit_in_hom lunit_naturality unit_in_hom_ax L.is_extensional
by (unfold_locales, auto)
have "𝔩.map = 𝔩"
using 𝔩.is_natural_1 𝔩.is_extensional by auto
thus "natural_transformation C C L map 𝔩"
using 𝔩.natural_transformation_axioms by auto
qed
sublocale 𝔩: natural_isomorphism C C L map 𝔩
apply unfold_locales
using iso_lunit 𝔩_ide_simp by simp
sublocale ρ: natural_transformation C C R map ρ
proof -
interpret ρ: transformation_by_components C C R map ‹λa. 𝗋[a]›
using runit_naturality unit_in_hom_ax R.is_extensional
by (unfold_locales, auto)
have "ρ.map = ρ"
using ρ.is_natural_1 ρ.is_extensional by auto
thus "natural_transformation C C R map ρ"
using ρ.natural_transformation_axioms by auto
qed
sublocale ρ: natural_isomorphism C C R map ρ
apply unfold_locales
using ρ_ide_simp by simp
sublocale 𝔩': inverse_transformation C C L map 𝔩 ..
sublocale ρ': inverse_transformation C C R map ρ ..
sublocale α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..
abbreviation α'
where "α' ≡ α'.map"
abbreviation assoc' (‹𝖺⇧-⇧1[_, _, _]›)
where "𝖺⇧-⇧1[a, b, c] ≡ inv 𝖺[a, b, c]"
lemma α'_ide_simp:
assumes "ide a" and "ide b" and "ide c"
shows "α' (a, b, c) = 𝖺⇧-⇧1[a, b, c]"
using assms α'.inverts_components inverse_unique by force
lemma α'_simp:
assumes "arr f" and "arr g" and "arr h"
shows "α' (f, g, h) = ((f ⊗ g) ⊗ h) ⋅ 𝖺⇧-⇧1[dom f, dom g, dom h]"
using assms T.ToTC_simp α'.is_natural_1 α'_ide_simp by force
lemma assoc_inv:
assumes "ide a" and "ide b" and "ide c"
shows "inverse_arrows 𝖺[a, b, c] 𝖺⇧-⇧1[a, b, c]"
using assms inv_is_inverse by simp
lemma assoc'_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺⇧-⇧1[a, b, c] : a ⊗ b ⊗ c → (a ⊗ b) ⊗ c»"
using assms by auto
lemma arr_assoc' [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺⇧-⇧1[a, b, c]"
using assms by simp
lemma dom_assoc' [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "dom 𝖺⇧-⇧1[a, b, c] = a ⊗ b ⊗ c"
using assms by simp
lemma cod_assoc' [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "cod 𝖺⇧-⇧1[a, b, c] = (a ⊗ b) ⊗ c"
using assms by simp
lemma comp_assoc_assoc' [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "𝖺[a, b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = a ⊗ (b ⊗ c)"
and "𝖺⇧-⇧1[a, b, c] ⋅ 𝖺[a, b, c] = (a ⊗ b) ⊗ c"
using assms assoc_inv comp_arr_inv comp_inv_arr by auto
lemma assoc'_naturality:
assumes "arr f0" and "arr f1" and "arr f2"
shows "((f0 ⊗ f1) ⊗ f2) ⋅ 𝖺⇧-⇧1[dom f0, dom f1, dom f2] =
𝖺⇧-⇧1[cod f0, cod f1, cod f2] ⋅ (f0 ⊗ f1 ⊗ f2)"
using assms α'.naturality by auto
abbreviation 𝔩'
where "𝔩' ≡ 𝔩'.map"
abbreviation lunit' (‹𝗅⇧-⇧1[_]›)
where "𝗅⇧-⇧1[a] ≡ inv 𝗅[a]"
lemma 𝔩'_ide_simp:
assumes "ide a"
shows "𝔩'.map a = 𝗅⇧-⇧1[a]"
using assms 𝔩'.inverts_components 𝔩_ide_simp inverse_unique by force
lemma lunit_inv:
assumes "ide a"
shows "inverse_arrows 𝗅[a] 𝗅⇧-⇧1[a]"
using assms inv_is_inverse by simp
lemma lunit'_in_hom [intro]:
assumes "ide a"
shows "«𝗅⇧-⇧1[a] : a → ℐ ⊗ a»"
using assms by auto
lemma comp_lunit_lunit' [simp]:
assumes "ide a"
shows "𝗅[a] ⋅ 𝗅⇧-⇧1[a] = a"
and "𝗅⇧-⇧1[a] ⋅ 𝗅[a] = ℐ ⊗ a"
proof -
show "𝗅[a] ⋅ 𝗅⇧-⇧1[a] = a"
using assms comp_arr_inv lunit_inv by fastforce
show "𝗅⇧-⇧1[a] ⋅ 𝗅[a] = ℐ ⊗ a"
using assms comp_arr_inv lunit_inv by fastforce
qed
lemma lunit'_naturality:
assumes "arr f"
shows "(ℐ ⊗ f) ⋅ 𝗅⇧-⇧1[dom f] = 𝗅⇧-⇧1[cod f] ⋅ f"
using assms 𝔩'.naturality 𝔩'_ide_simp by simp
abbreviation ρ'
where "ρ' ≡ ρ'.map"
abbreviation runit' (‹𝗋⇧-⇧1[_]›)
where "𝗋⇧-⇧1[a] ≡ inv 𝗋[a]"
lemma ρ'_ide_simp:
assumes "ide a"
shows "ρ'.map a = 𝗋⇧-⇧1[a]"
using assms ρ'.inverts_components ρ_ide_simp inverse_unique by auto
lemma runit_inv:
assumes "ide a"
shows "inverse_arrows 𝗋[a] 𝗋⇧-⇧1[a]"
using assms inv_is_inverse by simp
lemma runit'_in_hom [intro]:
assumes "ide a"
shows "«𝗋⇧-⇧1[a] : a → a ⊗ ℐ»"
using assms by auto
lemma comp_runit_runit' [simp]:
assumes "ide a"
shows "𝗋[a] ⋅ 𝗋⇧-⇧1[a] = a"
and "𝗋⇧-⇧1[a] ⋅ 𝗋[a] = a ⊗ ℐ"
proof -
show "𝗋[a] ⋅ 𝗋⇧-⇧1[a] = a"
using assms runit_inv by fastforce
show "𝗋⇧-⇧1[a] ⋅ 𝗋[a] = a ⊗ ℐ"
using assms runit_inv by fastforce
qed
lemma runit'_naturality:
assumes "arr f"
shows "(f ⊗ ℐ) ⋅ 𝗋⇧-⇧1[dom f] = 𝗋⇧-⇧1[cod f] ⋅ f"
using assms ρ'.naturality ρ'_ide_simp by simp
lemma lunit_commutes_with_L:
assumes "ide a"
shows "𝗅[ℐ ⊗ a] = ℐ ⊗ 𝗅[a]"
using assms lunit_naturality lunit_in_hom iso_lunit iso_is_section
section_is_mono monoE L.preserves_ide arrI cod_lunit dom_lunit seqI
by metis
lemma runit_commutes_with_R:
assumes "ide a"
shows "𝗋[a ⊗ ℐ] = 𝗋[a] ⊗ ℐ"
using assms runit_naturality runit_in_hom iso_runit iso_is_section
section_is_mono monoE R.preserves_ide arrI cod_runit dom_runit seqI
by metis
text‹
The components of the left and right unitors are related via a ``triangle''
diagram that also involves the associator.
The proof follows \<^cite>‹"Etingof15"›, Proposition 2.2.3.
›
lemma triangle:
assumes "ide a" and "ide b"
shows "(a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b] = 𝗋[a] ⊗ b"
proof -
text‹
We show that the lower left triangle in the following diagram commutes.
›
text‹
$$\xymatrix{
{@{term "((a ⊗ ℐ) ⊗ ℐ) ⊗ b"}}
\ar[rrrr]^{\scriptsize @{term "𝖺[a, ℐ, ℐ] ⊗ b"}}
\ar[ddd]_{\scriptsize @{term "𝖺[a ⊗ ℐ, ℐ, b]"}}
\ar[drr]_{\scriptsize @{term "(𝗋[a] ⊗ ℐ) ⊗ b"}}
&& &&
{@{term "(a ⊗ (ℐ ⊗ ℐ)) ⊗ b"}}
\ar[dll]^{\scriptsize @{term "(a ⊗ ι) ⊗ b"}}
\ar[ddd]^{\scriptsize @{term "𝖺[a, ℐ ⊗ ℐ, b]"}} \\
&& {@{term "(a ⊗ ℐ) ⊗ b"}}
\ar[d]^{\scriptsize @{term "𝖺[a, ℐ, b]"}} \\
&& {@{term "a ⊗ ℐ ⊗ b"}} \\
{@{term "(a ⊗ ℐ) ⊗ ℐ ⊗ b"}}
\ar[urr]^{\scriptsize @{term "𝗋[a] ⊗ ℐ ⊗ b"}}
\ar[drr]_{\scriptsize @{term "𝖺[a, ℐ, ℐ ⊗ b]"}}
&& &&
{@{term "a ⊗ (ℐ ⊗ ℐ) ⊗ b"}}
\ar[ull]_{\scriptsize @{term "a ⊗ ι ⊗ b"}}
\ar[dll]^{\scriptsize @{term "a ⊗ 𝖺[ℐ, ℐ, b]"}} \\
&& {@{term "a ⊗ ℐ ⊗ ℐ ⊗ b"}}
\ar[uu]^{\scriptsize @{term "a ⊗ 𝗅[ℐ ⊗ b]"}}
}$$
›
have *: "(a ⊗ 𝗅[ℐ ⊗ b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b] = 𝗋[a] ⊗ ℐ ⊗ b"
proof -
have 1: "((a ⊗ 𝗅[ℐ ⊗ b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b]) ⋅ 𝖺[a ⊗ ℐ, ℐ, b]
= (𝗋[a] ⊗ ℐ ⊗ b) ⋅ 𝖺[a ⊗ ℐ, ℐ, b]"
proof -
have "((a ⊗ 𝗅[ℐ ⊗ b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b]) ⋅ 𝖺[a ⊗ ℐ, ℐ, b] =
((a ⊗ 𝗅[ℐ ⊗ b]) ⋅ (a ⊗ 𝖺[ℐ, ℐ, b])) ⋅ 𝖺[a, ℐ ⊗ ℐ, b] ⋅ (𝖺[a, ℐ, ℐ] ⊗ b)"
using assms pentagon comp_assoc by auto
also have "... = (a ⊗ ((ℐ ⊗ 𝗅[b]) ⋅ 𝖺[ℐ, ℐ, b])) ⋅ 𝖺[a, ℐ ⊗ ℐ, b] ⋅ (𝖺[a, ℐ, ℐ] ⊗ b)"
using assms interchange lunit_commutes_with_L by simp
also have "... = ((a ⊗ (ι ⊗ b)) ⋅ 𝖺[a, ℐ ⊗ ℐ, b]) ⋅ (𝖺[a, ℐ, ℐ] ⊗ b)"
using assms lunit_char unit_in_hom comp_arr_dom comp_assoc by auto
also have "... = (𝖺[a, ℐ, b] ⋅ ((a ⊗ ι) ⊗ b)) ⋅ (𝖺[a, ℐ, ℐ] ⊗ b)"
using assms unit_in_hom assoc_naturality [of a ι b] by fastforce
also have "... = 𝖺[a, ℐ, b] ⋅ ((𝗋[a] ⊗ ℐ) ⊗ b)"
using assms unit_in_hom interchange runit_char(2) comp_assoc by auto
also have "... = (𝗋[a] ⊗ ℐ ⊗ b) ⋅ 𝖺[a ⊗ ℐ, ℐ, b]"
using assms assoc_naturality [of "𝗋[a]" ℐ b] by simp
finally show ?thesis by blast
qed
show ?thesis
proof -
have "epi 𝖺[a ⊗ ℐ, ℐ, b]"
using assms iso_assoc iso_is_retraction retraction_is_epi by simp
thus ?thesis
using 1 assms epiE [of "𝖺[a ⊗ ℐ, ℐ, b]" "(a ⊗ 𝗅[ℐ ⊗ b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b]"]
by fastforce
qed
qed
text‹
In \<^cite>‹"Etingof15"› it merely states that the preceding result suffices
``because any object of ‹C› is isomorphic to one of the form @{term "ℐ ⊗ b"}.''
However, it seems a little bit more involved than that to formally transport the
equation ‹(*)› along the isomorphism @{term "𝗅[b]"} from @{term "ℐ ⊗ b"}
to @{term b}.
›
have "(a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b] = ((a ⊗ 𝗅[b]) ⋅ (a ⊗ 𝗅[ℐ ⊗ b]) ⋅ (a ⊗ ℐ ⊗ 𝗅⇧-⇧1[b])) ⋅
(a ⊗ ℐ ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b] ⋅ ((a ⊗ ℐ) ⊗ 𝗅⇧-⇧1[b])"
proof -
have "𝖺[a, ℐ, b] = (a ⊗ ℐ ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b] ⋅ ((a ⊗ ℐ) ⊗ 𝗅⇧-⇧1[b])"
proof -
have "(a ⊗ ℐ ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b] ⋅ ((a ⊗ ℐ) ⊗ 𝗅⇧-⇧1[b])
= ((a ⊗ ℐ ⊗ 𝗅[b]) ⋅ (a ⊗ ℐ ⊗ 𝗅⇧-⇧1[b])) ⋅ 𝖺[a, ℐ, b]"
using assms assoc_naturality [of a ℐ "𝗅⇧-⇧1[b]"] comp_assoc by simp
also have "... = 𝖺[a, ℐ, b]"
using assms inv_is_inverse interchange comp_cod_arr by simp
finally show ?thesis by auto
qed
moreover have "a ⊗ 𝗅[b] = (a ⊗ 𝗅[b]) ⋅ (a ⊗ 𝗅[ℐ ⊗ b]) ⋅ (a ⊗ ℐ ⊗ 𝗅⇧-⇧1[b])"
using assms lunit_commutes_with_L comp_arr_dom interchange by auto
ultimately show ?thesis by argo
qed
also have "... = (a ⊗ 𝗅[b]) ⋅ (a ⊗ 𝗅[ℐ ⊗ b]) ⋅ ((a ⊗ ℐ ⊗ 𝗅⇧-⇧1[b]) ⋅ (a ⊗ ℐ ⊗ 𝗅[b])) ⋅
𝖺[a, ℐ, ℐ ⊗ b] ⋅ ((a ⊗ ℐ) ⊗ 𝗅⇧-⇧1[b])"
using assms comp_assoc by auto
also have "... = (a ⊗ 𝗅[b]) ⋅ ((a ⊗ 𝗅[ℐ ⊗ b]) ⋅ 𝖺[a, ℐ, ℐ ⊗ b]) ⋅ ((a ⊗ ℐ) ⊗ 𝗅⇧-⇧1[b])"
using assms interchange comp_cod_arr comp_assoc by auto
also have "... = 𝗋[a] ⊗ b"
using assms * interchange runit_char(1) comp_arr_dom comp_cod_arr by auto
finally show ?thesis by blast
qed
lemma lunit_tensor_gen:
assumes "ide a" and "ide b" and "ide c"
shows "(a ⊗ 𝗅[b ⊗ c]) ⋅ (a ⊗ 𝖺[ℐ, b, c]) = a ⊗ 𝗅[b] ⊗ c"
proof -
text‹
We show that the lower right triangle in the following diagram commutes.
›
text‹
$$\xymatrix{
{@{term "((a ⊗ ℐ) ⊗ b) ⊗ c"}}
\ar[rrrr]^{\scriptsize @{term "𝖺[a, ℐ, b] ⊗ c"}}
\ar[ddd]_{\scriptsize @{term "𝖺[a ⊗ ℐ, b, c]"}}
\ar[drr]_{\scriptsize @{term "𝗋[a] ⊗ b ⊗ c"}}
&& &&
{@{term "(a ⊗ (ℐ ⊗ b)) ⊗ c"}}
\ar[dll]^{\scriptsize @{term "(a ⊗ 𝗅[b]) ⊗ c"}}
\ar[ddd]^{\scriptsize @{term "𝖺[a, ℐ ⊗ b, c]"}} \\
&& {@{term "(a ⊗ b) ⊗ c"}}
\ar[d]^{\scriptsize @{term "𝖺[a, b, c]"}} \\
&& {@{term "a ⊗ b ⊗ c"}} \\
{@{term "(a ⊗ ℐ) ⊗ b ⊗ c"}}
\ar[urr]^{\scriptsize @{term "𝗋[a] ⊗ b ⊗ c"}}
\ar[drr]_{\scriptsize @{term "𝖺[a, ℐ, b ⊗ c]"}}
&& &&
{@{term "a ⊗ (ℐ ⊗ b) ⊗ c"}}
\ar[ull]_{\scriptsize @{term "a ⊗ 𝗅[b] ⊗ c"}}
\ar[dll]^{\scriptsize @{term "a ⊗ 𝖺[ℐ, b, c]"}} \\
&& {@{term "a ⊗ ℐ ⊗ b ⊗ c"}}
\ar[uu]^{\scriptsize @{term "a ⊗ 𝗅[b ⊗ c]"}}
}$$
›
have "((a ⊗ 𝗅[b ⊗ c]) ⋅ (a ⊗ 𝖺[ℐ, b, c])) ⋅ (𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c)) =
((a ⊗ 𝗅[b ⊗ c]) ⋅ 𝖺[a, ℐ, b ⊗ c]) ⋅ 𝖺[a ⊗ ℐ, b, c]"
using assms pentagon comp_assoc by simp
also have "... = (𝗋[a] ⊗ (b ⊗ c)) ⋅ 𝖺[a ⊗ ℐ, b, c]"
using assms triangle by auto
also have "... = 𝖺[a, b, c] ⋅ ((𝗋[a] ⊗ b) ⊗ c)"
using assms assoc_naturality [of "𝗋[a]" b c] by auto
also have "... = (𝖺[a, b, c] ⋅ ((a ⊗ 𝗅[b]) ⊗ c)) ⋅ (𝖺[a, ℐ, b] ⊗ c)"
using assms triangle interchange comp_assoc by auto
also have "... = (a ⊗ (𝗅[b] ⊗ c)) ⋅ (𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c))"
using assms assoc_naturality [of a "𝗅[b]" c] comp_assoc by auto
finally have 1: "((a ⊗ 𝗅[b ⊗ c]) ⋅ (a ⊗ 𝖺[ℐ, b, c])) ⋅ 𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c)
= (a ⊗ (𝗅[b] ⊗ c)) ⋅ 𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c)"
by blast
text‹
The result follows by cancelling the isomorphism
@{term "𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c)"}
›
have 2: "iso (𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c))"
using assms isos_compose by simp
moreover have
"seq ((a ⊗ 𝗅[b ⊗ c]) ⋅ (a ⊗ 𝖺[ℐ, b, c])) (𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c))"
using assms by auto
moreover have "seq (a ⊗ (𝗅[b] ⊗ c)) (𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c))"
using assms by auto
ultimately show ?thesis
using 1 2 assms iso_is_retraction retraction_is_epi
epiE [of "𝖺[a, ℐ ⊗ b, c] ⋅ (𝖺[a, ℐ, b] ⊗ c)"
"(a ⊗ 𝗅[b ⊗ c]) ⋅ (a ⊗ 𝖺[ℐ, b, c])" "a ⊗ 𝗅[b] ⊗ c"]
by auto
qed
text‹
The following result is quoted without proof as Theorem 7 of \<^cite>‹"Kelly64"› where it is
attributed to MacLane \<^cite>‹"MacLane63"›. It also appears as \<^cite>‹"MacLane71"›,
Exercise 1, page 161. I did not succeed within a few hours to construct a proof following
MacLane's hint. The proof below is based on \<^cite>‹"Etingof15"›, Proposition 2.2.4.
›
lemma lunit_tensor':
assumes "ide a" and "ide b"
shows "𝗅[a ⊗ b] ⋅ 𝖺[ℐ, a, b] = 𝗅[a] ⊗ b"
proof -
have "ℐ ⊗ (𝗅[a ⊗ b] ⋅ 𝖺[ℐ, a, b]) = ℐ ⊗ (𝗅[a] ⊗ b)"
using assms interchange [of ℐ ℐ] lunit_tensor_gen by simp
moreover have "par (𝗅[a ⊗ b] ⋅ 𝖺[ℐ, a, b]) (𝗅[a] ⊗ b)"
using assms by simp
ultimately show ?thesis
using assms L.is_faithful [of "𝗅[a ⊗ b] ⋅ 𝖺[ℐ, a, b]" "𝗅[a] ⊗ b"] by simp
qed
lemma lunit_tensor:
assumes "ide a" and "ide b"
shows "𝗅[a ⊗ b] = (𝗅[a] ⊗ b) ⋅ 𝖺⇧-⇧1[ℐ, a, b]"
using assms lunit_tensor' invert_side_of_triangle by simp
text‹
We next show the corresponding result for the right unitor.
›
lemma runit_tensor_gen:
assumes "ide a" and "ide b" and "ide c"
shows "𝗋[a ⊗ b] ⊗ c = ((a ⊗ 𝗋[b]) ⊗ c) ⋅ (𝖺[a, b, ℐ] ⊗ c)"
proof -
text‹
We show that the upper right triangle in the following diagram commutes.
›
text‹
$$\xymatrix{
&& {@{term "((a ⊗ b) ⊗ ℐ) ⊗ c"}}
\ar[dll]_{\scriptsize @{term "𝖺[a ⊗ b, ℐ, c]"}}
\ar[dd]^{\scriptsize @{term "𝗋[a ⊗ b] ⊗ c"}}
\ar[drr]^{\scriptsize @{term "𝖺[a, b, ℐ] ⊗ c"}} \\
{@{term "(a ⊗ b) ⊗ ℐ ⊗ c"}}
\ar[ddd]_{\scriptsize @{term "𝖺[a, b, ℐ ⊗ c]"}}
\ar[drr]_{\scriptsize @{term "(a ⊗ b) ⊗ 𝗅[c]"}}
&& &&
{@{term "(a ⊗ b ⊗ ℐ) ⊗ c"}}
\ar[dll]^{\scriptsize @{term "(a ⊗ 𝗋[b]) ⊗ c"}}
\ar[ddd]^{\scriptsize @{term "𝖺[a, b ⊗ ℐ, c]"}} \\
&& {@{term "(a ⊗ b) ⊗ c"}}
\ar[d]^{\scriptsize @{term "𝖺[a, b, c]"}} \\
&& {@{term "a ⊗ b ⊗ c"}} \\
{@{term "a ⊗ b ⊗ ℐ ⊗ c"}}
\ar[urr]^{\scriptsize @{term "a ⊗ b ⊗ 𝗅[c]"}}
&& &&
{@{term "a ⊗ (b ⊗ ℐ) ⊗ c"}}
\ar[llll]^{\scriptsize @{term "a ⊗ 𝖺[b, ℐ, c]"}}
\ar[ull]_{\scriptsize @{term "a ⊗ 𝗋[b] ⊗ c"}}
}$$
›
have "𝗋[a ⊗ b] ⊗ c = ((a ⊗ b) ⊗ 𝗅[c]) ⋅ 𝖺[a ⊗ b, ℐ, c]"
using assms triangle by simp
also have "... = (𝖺⇧-⇧1[a, b, c] ⋅ (a ⊗ b ⊗ 𝗅[c]) ⋅ 𝖺[a, b, ℐ ⊗ c]) ⋅ 𝖺[a ⊗ b, ℐ, c]"
using assms assoc_naturality [of a b "𝗅[c]"] comp_arr_dom comp_cod_arr
invert_side_of_triangle(1)
by force
also have "... = 𝖺⇧-⇧1[a, b, c] ⋅ (a ⊗ b ⊗ 𝗅[c]) ⋅ 𝖺[a, b, ℐ ⊗ c] ⋅ 𝖺[a ⊗ b, ℐ, c]"
using comp_assoc by force
also have "... = 𝖺⇧-⇧1[a, b, c] ⋅ ((a ⊗ (𝗋[b] ⊗ c)) ⋅ (a ⊗ 𝖺⇧-⇧1[b, ℐ, c])) ⋅
𝖺[a, b, ℐ ⊗ c] ⋅ 𝖺[a ⊗ b, ℐ, c]"
using assms triangle [of b c] interchange invert_side_of_triangle(2) by force
also have "... = (((a ⊗ 𝗋[b]) ⊗ c) ⋅ 𝖺⇧-⇧1[a, b ⊗ ℐ, c]) ⋅ (a ⊗ 𝖺⇧-⇧1[b, ℐ, c]) ⋅
𝖺[a, b, ℐ ⊗ c] ⋅ 𝖺[a ⊗ b, ℐ, c]"
using assms assoc'_naturality [of a "𝗋[b]" c] comp_assoc by force
also have "... = ((a ⊗ 𝗋[b]) ⊗ c) ⋅ 𝖺⇧-⇧1[a, b ⊗ ℐ, c] ⋅ (a ⊗ 𝖺⇧-⇧1[b, ℐ, c]) ⋅
𝖺[a, b, ℐ ⊗ c] ⋅ 𝖺[a ⊗ b, ℐ, c]"
using comp_assoc by simp
also have "... = ((a ⊗ 𝗋[b]) ⊗ c) ⋅ (𝖺[a, b, ℐ] ⊗ c)"
using assms pentagon invert_side_of_triangle(1)
invert_side_of_triangle(1)
[of "𝖺[a, b, ℐ ⊗ c] ⋅ 𝖺[a ⊗ b, ℐ, c]" "a ⊗ 𝖺[b, ℐ, c]"
"𝖺[a, b ⊗ ℐ, c] ⋅ (𝖺[a, b, ℐ] ⊗ c)"]
by force
finally show ?thesis by blast
qed
lemma runit_tensor:
assumes "ide a" and "ide b"
shows "𝗋[a ⊗ b] = (a ⊗ 𝗋[b]) ⋅ 𝖺[a, b, ℐ]"
proof -
have "((a ⊗ 𝗋[b]) ⋅ 𝖺[a, b, ℐ]) ⊗ ℐ = 𝗋[a ⊗ b] ⊗ ℐ"
using assms interchange [of ℐ ℐ] runit_tensor_gen by simp
moreover have "par ((a ⊗ 𝗋[b]) ⋅ 𝖺[a, b, ℐ]) 𝗋[a ⊗ b]"
using assms by simp
ultimately show ?thesis
using assms R.is_faithful [of "(a ⊗ 𝗋[b]) ⋅ (𝖺[a, b, ℐ])" "𝗋[a ⊗ b]"]
by fastforce
qed
lemma runit_tensor':
assumes "ide a" and "ide b"
shows "𝗋[a ⊗ b] ⋅ 𝖺⇧-⇧1[a, b, ℐ] = a ⊗ 𝗋[b]"
using assms runit_tensor invert_side_of_triangle by force
text ‹
Sometimes inverted forms of the triangle and pentagon axioms are useful.
›
lemma triangle':
assumes "ide a" and "ide b"
shows "(a ⊗ 𝗅[b]) = (𝗋[a] ⊗ b) ⋅ 𝖺⇧-⇧1[a, ℐ, b]"
proof -
have "(𝗋[a] ⊗ b) ⋅ 𝖺⇧-⇧1[a, ℐ, b] = ((a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b]) ⋅ 𝖺⇧-⇧1[a, ℐ, b]"
using assms triangle by auto
also have "... = (a ⊗ 𝗅[b])"
using assms comp_arr_dom comp_assoc by auto
finally show ?thesis by auto
qed
lemma pentagon':
assumes "ide a" and "ide b" and "ide c" and "ide d"
shows "((𝖺⇧-⇧1[a, b, c] ⊗ d) ⋅ 𝖺⇧-⇧1[a, b ⊗ c, d]) ⋅ (a ⊗ 𝖺⇧-⇧1[b, c, d])
= 𝖺⇧-⇧1[a ⊗ b, c, d] ⋅ 𝖺⇧-⇧1[a, b, c ⊗ d]"
proof -
have "((𝖺⇧-⇧1[a, b, c] ⊗ d) ⋅ 𝖺⇧-⇧1[a, b ⊗ c, d]) ⋅ (a ⊗ 𝖺⇧-⇧1[b, c, d])
= inv ((a ⊗ 𝖺[b, c, d]) ⋅ (𝖺[a, b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)))"
using assms isos_compose inv_comp by simp
also have "... = inv (𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d])"
using assms pentagon by auto
also have "... = 𝖺⇧-⇧1[a ⊗ b, c, d] ⋅ 𝖺⇧-⇧1[a, b, c ⊗ d]"
using assms inv_comp by simp
finally show ?thesis by auto
qed
text‹
The following non-obvious fact is Corollary 2.2.5 from \<^cite>‹"Etingof15"›.
The statement that @{term "𝗅[ℐ] = 𝗋[ℐ]"} is Theorem 6 from \<^cite>‹"Kelly64"›.
MacLane \<^cite>‹"MacLane71"› does not show this, but assumes it as an axiom.
›
lemma unitor_coincidence:
shows "𝗅[ℐ] = ι" and "𝗋[ℐ] = ι"
proof -
have "𝗅[ℐ] ⊗ ℐ = (ℐ ⊗ 𝗅[ℐ]) ⋅ 𝖺[ℐ, ℐ, ℐ]"
using lunit_tensor' [of ℐ ℐ] lunit_commutes_with_L [of ℐ] by simp
moreover have "𝗋[ℐ] ⊗ ℐ = (ℐ ⊗ 𝗅[ℐ]) ⋅ 𝖺[ℐ, ℐ, ℐ]"
using triangle [of ℐ ℐ] by simp
moreover have "ι ⊗ ℐ = (ℐ ⊗ 𝗅[ℐ]) ⋅ 𝖺[ℐ, ℐ, ℐ]"
using lunit_char comp_arr_dom unit_in_hom comp_assoc by auto
ultimately have "𝗅[ℐ] ⊗ ℐ = ι ⊗ ℐ ∧ 𝗋[ℐ] ⊗ ℐ = ι ⊗ ℐ"
by argo
moreover have "par 𝗅[ℐ] ι ∧ par 𝗋[ℐ] ι"
using unit_in_hom by force
ultimately have 1: "𝗅[ℐ] = ι ∧ 𝗋[ℐ] = ι"
using R.is_faithful by metis
show "𝗅[ℐ] = ι" using 1 by auto
show "𝗋[ℐ] = ι" using 1 by auto
qed
lemma unit_triangle:
shows "ι ⊗ ℐ = (ℐ ⊗ ι) ⋅ 𝖺[ℐ, ℐ, ℐ]"
and "(ι ⊗ ℐ) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ] = ℐ ⊗ ι"
using triangle [of ℐ ℐ] triangle' [of ℐ ℐ] unitor_coincidence by auto
text‹
The only isomorphism that commutes with @{term ι} is @{term ℐ}.
›
lemma iso_commuting_with_unit_equals_unity:
assumes "«f : ℐ → ℐ»" and "iso f" and "f ⋅ ι = ι ⋅ (f ⊗ f)"
shows "f = ℐ"
proof -
have "ℐ ⊗ f = ℐ ⊗ ℐ"
proof -
have "f ⊗ f = f ⊗ ℐ"
by (metis assms(1,3) iso_cancel_left runit_naturality seqE seqI' unit_in_hom_ax
unit_is_iso unitor_coincidence(2))
thus ?thesis
by (metis assms(1-2) R.preserves_comp comp_cod_arr comp_inv_arr' ideD(1) ide_unity
in_homE interchange)
qed
moreover have "par f ℐ"
using assms by auto
ultimately show "f = ℐ"
using L.is_faithful by metis
qed
end
text‹
We now show that the unit ‹ι› of a monoidal category is unique up to a unique
isomorphism (Proposition 2.2.6 of \<^cite>‹"Etingof15"›).
›
locale monoidal_category_with_alternate_unit =
monoidal_category C T α ι +
C⇩1: monoidal_category C T α ι⇩1
for C :: "'a comp" (infixr ‹⋅› 55)
and T :: "'a * 'a ⇒ 'a"
and α :: "'a * 'a * 'a ⇒ 'a"
and ι :: 'a
and ι⇩1 :: 'a
begin
no_notation C⇩1.tensor (infixr ‹⊗› 53)
no_notation C⇩1.unity (‹ℐ›)
no_notation C⇩1.lunit (‹𝗅[_]›)
no_notation C⇩1.runit (‹𝗋[_]›)
no_notation C⇩1.assoc (‹𝖺[_, _, _]›)
no_notation C⇩1.assoc' (‹𝖺⇧-⇧1[_, _, _]›)
notation C⇩1.tensor (infixr ‹⊗⇩1› 53)
notation C⇩1.unity (‹ℐ⇩1›)
notation C⇩1.lunit (‹𝗅⇩1[_]›)
notation C⇩1.runit (‹𝗋⇩1[_]›)
notation C⇩1.assoc (‹𝖺⇩1[_, _, _]›)
notation C⇩1.assoc' (‹𝖺⇩1⇧-⇧1[_, _, _]›)
definition i
where "i ≡ 𝗅[ℐ⇩1] ⋅ inv 𝗋⇩1[ℐ]"
lemma iso_i:
shows "«i : ℐ → ℐ⇩1»" and "iso i"
proof -
show "«i : ℐ → ℐ⇩1»"
using C⇩1.iso_runit inv_in_hom i_def by auto
show "iso i"
using iso_lunit C⇩1.iso_runit isos_compose i_def by simp
qed
text‹
The following is Exercise 2.2.7 of \<^cite>‹"Etingof15"›.
›
lemma i_maps_ι_to_ι⇩1:
shows "i ⋅ ι = ι⇩1 ⋅ (i ⊗ i)"
proof -
have 1: "inv 𝗋⇩1[ℐ] ⋅ ι = (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]) ⋅ (inv 𝗋⇩1[ℐ] ⊗ inv 𝗋⇩1[ℐ])"
proof -
have "ι ⋅ (𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ]) = 𝗋⇩1[ℐ] ⋅ (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1])"
proof -
text ‹
$$\xymatrix{
&& {@{term[source=true] "(ℐ ⊗ ℐ⇩1) ⊗ ℐ ⊗ ℐ⇩1"}}
\ar[dddll]_{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ]"}}
\ar[dd]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1"}}
\ar[dddrr]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]"}}
\\
\\
&& {@{term[source=true] "ℐ ⊗ ℐ ⊗ ℐ⇩1"}}
\ar[dll]^{\scriptsize @{term[source=true] "ℐ ⊗ 𝗋⇩1[ℐ]"}}
\ar[drr]_{\scriptsize @{term[source=true] "ℐ ⊗ 𝗅[ℐ⇩1]"}}
\ar[dd]^{\scriptsize @{term[source=true] "𝖺⇧-⇧1[ℐ, ℐ, ℐ⇩1]"}}
\\
{@{term[source=true] "ℐ ⊗ ℐ"}}
\ar[dddrr]_{\scriptsize @{term[source=true] "ι"}}
&&
&&
{@{term[source=true] "ℐ ⊗ ℐ⇩1"}}
\ar[dddll]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ]"}}
\\
&& {@{ term[source=true] "(ℐ ⊗ ℐ) ⊗ ℐ⇩1"}}
\ar[ull]_{\scriptsize @{term[source=true] "𝗋⇩1[ℐ ⊗ ℐ]"}}
\ar[urr]^{\scriptsize @{term[source=true] "ι ⊗ ℐ"}}
\\
\\
&& {@{term[source=true] "ℐ"}}
}$$
›
have "ι ⋅ (𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ]) = ι ⋅ (ℐ ⊗ 𝗋⇩1[ℐ]) ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using interchange comp_cod_arr comp_arr_dom by simp
also have "... = ι ⋅ (𝗋⇩1[ℐ ⊗ ℐ] ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ⇩1]) ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using C⇩1.runit_tensor' by auto
also have "... = (ι ⋅ 𝗋⇩1[ℐ ⊗ ℐ]) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using comp_assoc by auto
also have "... = (𝗋⇩1[ℐ] ⋅ (ι ⊗ ℐ⇩1)) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using C⇩1.runit_naturality [of ι] unit_in_hom by fastforce
also have "... = 𝗋⇩1[ℐ] ⋅ ((ι ⊗ ℐ⇩1) ⋅ 𝖺⇧-⇧1[ℐ, ℐ, ℐ⇩1]) ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using comp_assoc by auto
also have "... = 𝗋⇩1[ℐ] ⋅ (ℐ ⊗ 𝗅[ℐ⇩1]) ⋅ (𝗋⇩1[ℐ] ⊗ ℐ ⊗ ℐ⇩1)"
using lunit_tensor lunit_commutes_with_L unitor_coincidence by simp
also have "... = 𝗋⇩1[ℐ] ⋅ (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1])"
using interchange comp_arr_dom comp_cod_arr by simp
finally show ?thesis by blast
qed
moreover have "seq ι (𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ]) ∧ seq 𝗋⇩1[ℐ] (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1])"
using unit_in_hom by fastforce
moreover have "iso 𝗋⇩1[ℐ] ∧ iso (𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ])"
using C⇩1.iso_runit tensor_preserves_iso by force
ultimately show ?thesis
using invert_opposite_sides_of_square inv_tensor by metis
qed
have 2: "𝗅[ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]) = ι⇩1 ⋅ (𝗅[ℐ⇩1] ⊗ 𝗅[ℐ⇩1])"
proof -
text ‹
$$\xymatrix{
&& {@{term[source=true] "(ℐ ⊗ ℐ⇩1) ⊗ (ℐ ⊗ ℐ⇩1)"}}
\ar[dddll]_{\scriptsize @{term[source=true] "𝗅[ℐ⇩1] ⊗ 𝗅[ℐ⇩1]"}}
\ar[dd]^{\scriptsize @{term[source=true] "(ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1]"}}
\ar[dddrr]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]"}}
\\
\\
&& {@{term[source=true] "(ℐ ⊗ ℐ⇩1) ⊗ ℐ⇩1"}}
\ar[dll]^{\scriptsize @{term[source=true] "𝗅[ℐ⇩1] ⊗ ℐ⇩1"}}
\ar[drr]_{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ ℐ⇩1"}}
\ar[dd]^{\scriptsize @{term[source=true] "𝖺[ℐ, ℐ⇩1, ℐ⇩1]"}}
\\
{@{term[source=true] "ℐ⇩1 ⊗ ℐ⇩1"}}
\ar[dddrr]_{\scriptsize @{term[source=true] "ι⇩1"}}
&&
&&
{@{term[source=true] "ℐ ⊗ ℐ⇩1"}}
\ar[dddll]^{\scriptsize @{term[source=true] "𝗅[ℐ⇩1]"}}
\\
&& {@{term[source=true] "ℐ ⊗ ℐ⇩1 ⊗ ℐ⇩1"}}
\ar[ull]_{\scriptsize @{term[source=true] "𝗅[ℐ⇩1 ⊗ ℐ⇩1]"}}
\ar[urr]^{\scriptsize @{term[source=true] "ℐ ⊗ ι⇩1"}}
\\
\\
&& {@{term[source=true] "ℐ⇩1"}}
}$$
›
have "𝗅[ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]) = 𝗅[ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ ℐ⇩1) ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using interchange comp_arr_dom comp_cod_arr by force
also have "... = 𝗅[ℐ⇩1] ⋅ ((ℐ ⊗ ι⇩1) ⋅ 𝖺[ℐ, ℐ⇩1, ℐ⇩1]) ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using C⇩1.runit_tensor C⇩1.unitor_coincidence C⇩1.runit_commutes_with_R by simp
also have "... = (𝗅[ℐ⇩1] ⋅ (ℐ ⊗ ι⇩1)) ⋅ 𝖺[ℐ, ℐ⇩1, ℐ⇩1] ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using comp_assoc by fastforce
also have "... = (ι⇩1 ⋅ 𝗅[ℐ⇩1 ⊗ ℐ⇩1]) ⋅ 𝖺[ℐ, ℐ⇩1, ℐ⇩1] ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using lunit_naturality [of ι⇩1] C⇩1.unit_in_hom lunit_commutes_with_L by fastforce
also have "... = ι⇩1 ⋅ (𝗅[ℐ⇩1 ⊗ ℐ⇩1] ⋅ 𝖺[ℐ, ℐ⇩1, ℐ⇩1]) ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using comp_assoc by force
also have "... = ι⇩1 ⋅ (𝗅[ℐ⇩1] ⊗ ℐ⇩1) ⋅ ((ℐ ⊗ ℐ⇩1) ⊗ 𝗅[ℐ⇩1])"
using lunit_tensor' by auto
also have "... = ι⇩1 ⋅ (𝗅[ℐ⇩1] ⊗ 𝗅[ℐ⇩1])"
using interchange comp_arr_dom comp_cod_arr by simp
finally show ?thesis by blast
qed
show ?thesis
proof -
text ‹
$$\xymatrix{
{@{term[source=true] "ℐ⇩1 ⊗ ℐ⇩1"}}
\ar[dd]_{\scriptsize @{term "ι⇩1"}}
&&
{@{term[source=true] "(ℐ ⊗ ℐ⇩1) ⊗ (ℐ ⊗ ℐ⇩1)"}}
\ar[ll]_{\scriptsize @{term[source=true] "𝗅[ℐ⇩1] ⊗ 𝗅[ℐ⇩1]"}}
\ar[dd]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1]"}}
\ar[rr]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ] ⊗ 𝗋⇩1[ℐ]"}}
&&
{@{term[source=true] "ℐ⇩1 ⊗ ℐ⇩1"}}
\ar[dd]^{\scriptsize @{term[source=true] "ι"}}
\\
\\
{@{term[source=true] "ℐ⇩1"}}
&&
{@{term[source=true] "ℐ ⊗ ℐ⇩1"}}
\ar[ll]_{\scriptsize @{term[source=true] "𝗅[ℐ⇩1]"}}
\ar[rr]^{\scriptsize @{term[source=true] "𝗋⇩1[ℐ]"}}
&&
{@{term[source=true] "ℐ"}}
}$$
›
have "i ⋅ ι = 𝗅[ℐ⇩1] ⋅ inv 𝗋⇩1[ℐ] ⋅ ι"
using i_def comp_assoc by auto
also have "... = (𝗅[ℐ⇩1] ⋅ (𝗋⇩1[ℐ] ⊗ 𝗅[ℐ⇩1])) ⋅ (inv 𝗋⇩1[ℐ] ⊗ inv 𝗋⇩1[ℐ])"
using 1 comp_assoc by simp
also have "... = ι⇩1 ⋅ (𝗅[ℐ⇩1] ⊗ 𝗅[ℐ⇩1]) ⋅ (inv 𝗋⇩1[ℐ] ⊗ inv 𝗋⇩1[ℐ])"
using 2 comp_assoc by fastforce
also have "... = ι⇩1 ⋅ (i ⊗ i)"
using interchange i_def by simp
finally show ?thesis by blast
qed
qed
lemma inv_i_iso_ι:
assumes "«f : ℐ → ℐ⇩1»" and "iso f" and "f ⋅ ι = ι⇩1 ⋅ (f ⊗ f)"
shows "«inv i ⋅ f : ℐ → ℐ»" and "iso (inv i ⋅ f)"
and "(inv i ⋅ f) ⋅ ι = ι ⋅ (inv i ⋅ f ⊗ inv i ⋅ f)"
proof -
show 1: "«inv i ⋅ f : ℐ → ℐ»"
using assms iso_i inv_in_hom by blast
show "iso (inv i ⋅ f)"
using assms 1 iso_i inv_in_hom
by (intro isos_compose, auto)
show "(inv i ⋅ f) ⋅ ι = ι ⋅ (inv i ⋅ f ⊗ inv i ⋅ f)"
proof -
have "(inv i ⋅ f) ⋅ ι = (inv i ⋅ ι⇩1) ⋅ (f ⊗ f)"
using assms iso_i comp_assoc by auto
also have "... = (ι ⋅ (inv i ⊗ inv i)) ⋅ (f ⊗ f)"
by (metis unit_in_hom_ax i_maps_ι_to_ι⇩1 invert_opposite_sides_of_square iso_i
inv_tensor tensor_preserves_iso seqI')
also have "... = ι ⋅ (inv i ⋅ f ⊗ inv i ⋅ f)"
using assms 1 iso_i interchange comp_assoc by fastforce
finally show ?thesis by blast
qed
qed
lemma unit_unique_upto_unique_iso:
shows "∃!f. «f : ℐ → ℐ⇩1» ∧ iso f ∧ f ⋅ ι = ι⇩1 ⋅ (f ⊗ f)"
proof
show "«i : ℐ → ℐ⇩1» ∧ iso i ∧ i ⋅ ι = ι⇩1 ⋅ (i ⊗ i)"
using iso_i i_maps_ι_to_ι⇩1 by auto
show "⋀f. «f : ℐ → ℐ⇩1» ∧ iso f ∧ f ⋅ ι = ι⇩1 ⋅ (f ⊗ f) ⟹ f = i"
proof -
fix f
assume f: "«f : ℐ → ℐ⇩1» ∧ iso f ∧ f ⋅ ι = ι⇩1 ⋅ (f ⊗ f)"
have "inv i ⋅ f = ℐ"
using f inv_i_iso_ι iso_commuting_with_unit_equals_unity by blast
hence "ide (C (inv i) f)"
using iso_i by simp
thus "f = i"
using section_retraction_of_iso(2) [of "inv i" f] inverse_arrow_unique inv_is_inverse
iso_i
by blast
qed
qed
end
section "Elementary Monoidal Category"
text‹
Although the economy of data assumed by @{locale monoidal_category} is useful for general
results, to establish interpretations it is more convenient to work with a traditional
definition of monoidal category. The following locale provides such a definition.
It permits a monoidal category to be specified by giving the tensor product and the
components of the associator and unitors, which are required only to satisfy elementary
conditions that imply functoriality and naturality, without having to worry about
extensionality or formal interpretations for the various functors and natural transformations.
›
locale elementary_monoidal_category =
category C
for C :: "'a comp" (infixr ‹⋅› 55)
and tensor :: "'a ⇒ 'a ⇒ 'a" (infixr ‹⊗› 53)
and unity :: 'a (‹ℐ›)
and lunit :: "'a ⇒ 'a" (‹𝗅[_]›)
and runit :: "'a ⇒ 'a" (‹𝗋[_]›)
and assoc :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹𝖺[_, _, _]›) +
assumes ide_unity [simp]: "ide ℐ"
and iso_lunit: "ide a ⟹ iso 𝗅[a]"
and iso_runit: "ide a ⟹ iso 𝗋[a]"
and iso_assoc: "⟦ ide a; ide b; ide c ⟧ ⟹ iso 𝖺[a, b, c]"
and tensor_in_hom [simp]: "⟦ «f : a → b»; «g : c → d» ⟧ ⟹ «f ⊗ g : a ⊗ c → b ⊗ d»"
and tensor_preserves_ide: "⟦ ide a; ide b ⟧ ⟹ ide (a ⊗ b)"
and interchange: "⟦ seq g f; seq g' f' ⟧ ⟹ (g ⊗ g') ⋅ (f ⊗ f') = g ⋅ f ⊗ g' ⋅ f'"
and lunit_in_hom [simp]: "ide a ⟹ «𝗅[a] : ℐ ⊗ a → a»"
and lunit_naturality: "arr f ⟹ 𝗅[cod f] ⋅ (ℐ ⊗ f) = f ⋅ 𝗅[dom f]"
and runit_in_hom [simp]: "ide a ⟹ «𝗋[a] : a ⊗ ℐ → a»"
and runit_naturality: "arr f ⟹ 𝗋[cod f] ⋅ (f ⊗ ℐ) = f ⋅ 𝗋[dom f]"
and assoc_in_hom [simp]:
"⟦ ide a; ide b; ide c ⟧ ⟹ «𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ b ⊗ c»"
and assoc_naturality:
"⟦ arr f0; arr f1; arr f2 ⟧ ⟹ 𝖺[cod f0, cod f1, cod f2] ⋅ ((f0 ⊗ f1) ⊗ f2)
= (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[dom f0, dom f1, dom f2]"
and triangle: "⟦ ide a; ide b ⟧ ⟹ (a ⊗ 𝗅[b]) ⋅ 𝖺[a, ℐ, b] = 𝗋[a] ⊗ b"
and pentagon: "⟦ ide a; ide b; ide c; ide d ⟧ ⟹
(a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)
= 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
text‹
An interpretation for the ‹monoidal_category› locale readily induces an
interpretation for the ‹elementary_monoidal_category› locale.
›
context monoidal_category
begin
lemma induces_elementary_monoidal_category:
shows "elementary_monoidal_category C tensor ℐ lunit runit assoc"
using iso_assoc tensor_preserves_ide assoc_in_hom tensor_in_hom
assoc_naturality lunit_naturality runit_naturality lunit_in_hom runit_in_hom
iso_lunit iso_runit interchange pentagon triangle
by unfold_locales auto
end
context elementary_monoidal_category
begin
interpretation CC: product_category C C ..
interpretation CCC: product_category C CC.comp ..
definition T :: "'a * 'a ⇒ 'a"
where "T f ≡ if CC.arr f then (fst f ⊗ snd f) else null"
lemma T_simp [simp]:
assumes "arr f" and "arr g"
shows "T (f, g) = f ⊗ g"
using assms T_def by simp
lemma arr_tensor [simp]:
assumes "arr f" and "arr g"
shows "arr (f ⊗ g)"
using assms tensor_in_hom by blast
lemma dom_tensor [simp]:
assumes "arr f" and "arr g"
shows "dom (f ⊗ g) = dom f ⊗ dom g"
using assms tensor_in_hom 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 by blast
interpretation T: binary_endofunctor C T
using interchange T_def
apply unfold_locales
apply auto[4]
by (elim CC.seqE, auto)
lemma binary_endofunctor_T:
shows "binary_endofunctor C T" ..
interpretation ToTC: "functor" CCC.comp C T.ToTC
using T.functor_ToTC by auto
interpretation ToCT: "functor" CCC.comp C T.ToCT
using T.functor_ToCT by auto
definition α
where "α f ≡ if CCC.arr f
then (fst f ⊗ (fst (snd f) ⊗ snd (snd f))) ⋅
𝖺[dom (fst f), dom (fst (snd f)), dom (snd (snd f))]
else null"
lemma α_ide_simp [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "α (a, b, c) = 𝖺[a, b, c]"
unfolding α_def using assms assoc_in_hom comp_cod_arr
by (metis CC.arrI⇩P⇩C CCC.arrI⇩P⇩C fst_conv ide_char in_homE snd_conv)
lemma arr_assoc [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺[a, b, c]"
using assms assoc_in_hom by blast
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
interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
proof -
interpret α: transformation_by_components CCC.comp C T.ToTC T.ToCT α
apply unfold_locales
unfolding α_def T.ToTC_def T.ToCT_def T_def
using comp_arr_dom comp_cod_arr assoc_naturality
by simp_all
interpret α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α.map
using iso_assoc α.map_simp_ide assoc_in_hom tensor_preserves_ide α_def
by (unfold_locales, auto)
have "α = α.map"
using assoc_naturality α_def comp_cod_arr T.ToTC_def T_def α.map_def by auto
thus "natural_isomorphism CCC.comp C T.ToTC T.ToCT α"
using α.natural_isomorphism_axioms by simp
qed
interpretation α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..
interpretation L: "functor" C C ‹λf. T (ℐ, f)›
using T.fixing_ide_gives_functor_1 by auto
interpretation R: "functor" C C ‹λf. T (f, ℐ)›
using T.fixing_ide_gives_functor_2 by auto
interpretation 𝔩: natural_isomorphism C C ‹λf. T (ℐ, f)› map
‹λf. if arr f then f ⋅ 𝗅[dom f] else null›
proof -
interpret 𝔩: transformation_by_components C C ‹λf. T (ℐ, f)› map ‹λa. 𝗅[a]›
using lunit_naturality by (unfold_locales, auto)
interpret 𝔩: natural_isomorphism C C ‹λf. T (ℐ, f)› map 𝔩.map
using iso_lunit by (unfold_locales, simp)
have "𝔩.map = (λf. if arr f then f ⋅ 𝗅[dom f] else null)"
using 𝔩.map_def lunit_naturality by fastforce
thus "natural_isomorphism C C (λf. T (ℐ, f)) map (λf. if arr f then f ⋅ 𝗅[dom f] else null)"
using 𝔩.natural_isomorphism_axioms by force
qed
interpretation ρ: natural_isomorphism C C ‹λf. T (f, ℐ)› map
‹λf. if arr f then f ⋅ 𝗋[dom f] else null›
proof -
interpret ρ: transformation_by_components C C ‹λf. T (f, ℐ)› map ‹λa. 𝗋[a]›
using runit_naturality by (unfold_locales, auto)
interpret ρ: natural_isomorphism C C ‹λf. T (f, ℐ)› map ρ.map
using iso_runit ρ.map_simp_ide by (unfold_locales, simp)
have "(λf. if arr f then f ⋅ 𝗋[dom f] else null) = ρ.map"
using ρ.map_def runit_naturality T_simp by fastforce
thus "natural_isomorphism C C (λf. T (f, ℐ)) map (λf. if arr f then f ⋅ 𝗋[dom f] else null)"
using ρ.natural_isomorphism_axioms by force
qed
text‹
The endofunctors ‹λf. T (ℐ, f)› and ‹λf. T (f, ℐ)› are equivalence functors,
due to the existence of the unitors.
›
interpretation L: equivalence_functor C C ‹λf. T (ℐ, f)›
proof -
interpret endofunctor C ‹λf. T (ℐ, f)› ..
show "equivalence_functor C C (λf. T (ℐ, f))"
using isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp
qed
interpretation R: equivalence_functor C C ‹λf. T (f, ℐ)›
proof -
interpret endofunctor C ‹λf. T (f, ℐ)› ..
show "equivalence_functor C C (λf. T (f, ℐ))"
using isomorphic_to_identity_is_equivalence ρ.natural_isomorphism_axioms by simp
qed
text‹
To complete an interpretation of the @{locale "monoidal_category"} locale,
we define @{term "ι ≡ 𝗅[ℐ]"}.
We could also have chosen @{term "ι ≡ ρ[ℐ]"} as the two are equal, though to prove
that requires some work yet.
›
definition ι
where "ι ≡ 𝗅[ℐ]"
lemma ι_in_hom:
shows "«ι : ℐ ⊗ ℐ → ℐ»"
using lunit_in_hom ι_def by simp
lemma induces_monoidal_category:
shows "monoidal_category C T α ι"
proof -
have 1: "«ι : ℐ ⊗ ℐ → ℐ»"
using lunit_in_hom ι_def by simp
interpret L: equivalence_functor C C ‹λf. T (cod ι, f)›
proof -
have "(λf. T (ℐ, f)) = (λf. T (cod ι, f))" using 1 by fastforce
thus "equivalence_functor C C (λf. T (cod ι, f))"
using L.equivalence_functor_axioms T_def by simp
qed
interpret R: equivalence_functor C C ‹λf. T (f, cod ι)›
proof -
have "(λf. T (f, ℐ)) = (λf. T (f, cod ι))" using 1 by fastforce
thus "equivalence_functor C C (λf. T (f, cod ι))"
using R.equivalence_functor_axioms T_def by simp
qed
show ?thesis
proof
show "«ι : T (cod ι, cod ι) → cod ι»" using 1 by fastforce
show "iso ι" using iso_lunit ι_def by simp
show "⋀a b c d. ⟦ ide a; ide b; ide c; ide d ⟧ ⟹
T (a, α (b, c, d)) ⋅ α (a, T (b, c), d) ⋅ T (α (a, b, c), d)
= α (a, b, T (c, d)) ⋅ α (T (a, b), c, d)"
using pentagon tensor_preserves_ide by simp
qed
qed
interpretation MC: monoidal_category C T α ι
using induces_monoidal_category by auto
text‹
We now show that the notions defined in the interpretation ‹MC› agree with their
counterparts in the present locale. These facts are needed if we define an
interpretation for the @{locale elementary_monoidal_category} locale, use it to
obtain the induced interpretation for @{locale monoidal_category}, and then want to
transfer facts obtained in the induced interpretation back to the original one.
›
lemma ℐ_agreement:
shows "MC.unity = ℐ"
by (metis ι_def ide_unity in_homE lunit_in_hom)
lemma L_agreement:
shows "MC.L = (λf. T (ℐ, f))"
using ι_in_hom by auto
lemma R_agreement:
shows "MC.R = (λf. T (f, ℐ))"
using ι_in_hom by auto
text‹
We wish to show that the components of the unitors @{term MC.𝔩} and @{term MC.ρ}
defined in the induced interpretation ‹MC› agree with those given by the
parameters @{term lunit} and @{term runit} to the present locale. To avoid a lengthy
development that repeats work already done in the @{locale monoidal_category} locale,
we establish the agreement in a special case and then use the properties already
shown for ‹MC› to prove the general case. In particular, we first show that
@{term "𝗅[ℐ] = MC.lunit MC.unity"} and @{term "𝗋[ℐ] = MC.runit MC.unity"},
from which it follows by facts already proved for @{term MC} that both are equal to @{term ι}.
We then show that for an arbitrary identity @{term a} the arrows @{term "𝗅[a]"}
and @{term "𝗋[a]"} satisfy the equations that uniquely characterize the components
@{term "MC.lunit a"} and @{term "MC.runit a"}, respectively, and are therefore equal
to those components.
›
lemma unitor_coincidence:
shows "𝗅[ℐ] = ι" and "𝗋[ℐ] = ι"
proof -
have "𝗋[ℐ] = MC.runit MC.unity"
by (metis (no_types, lifting) MC.arr_runit MC.runit_eqI MC.unitor_coincidence(2)
T_simp ℐ_agreement ι_def α_ide_simp ideD(1) ide_unity iso_is_arr iso_runit
runit_in_hom triangle)
moreover have "𝗅[ℐ] = MC.lunit MC.unity"
using MC.unitor_coincidence(1) ι_def by force
ultimately have 1: "𝗅[ℐ] = ι ∧ 𝗋[ℐ] = ι"
using MC.unitor_coincidence by simp
show "𝗅[ℐ] = ι" using 1 by simp
show "𝗋[ℐ] = ι" using 1 by simp
qed
lemma lunit_char:
assumes "ide a"
shows "ℐ ⊗ 𝗅[a] = (ι ⊗ a) ⋅ inv 𝖺[ℐ, ℐ, a]"
by (metis MC.iso_assoc α_ide_simp ι_in_hom arrI arr_tensor assms ideD(1)
ide_unity invert_side_of_triangle(2) triangle unitor_coincidence(2))
lemma runit_char:
assumes "ide a"
shows "𝗋[a] ⊗ ℐ = (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ]"
using assms triangle ι_def by simp
lemma 𝔩_agreement:
shows "MC.𝔩 = (λf. if arr f then f ⋅ 𝗅[dom f] else null)"
proof
fix f
have "¬ arr f ⟹ MC.𝔩 f = null" by simp
moreover have "arr f ⟹ MC.𝔩 f = f ⋅ 𝗅[dom f]"
proof -
have "⋀a. ide a ⟹ 𝗅[a] = MC.lunit a"
using ℐ_agreement T_def lunit_char ι_in_hom iso_lunit
apply (intro MC.lunit_eqI)
apply auto
by blast
thus ?thesis
by (metis ide_dom ext seqE)
qed
ultimately show "MC.𝔩 f = (if arr f then f ⋅ 𝗅[dom f] else null)" by simp
qed
lemma ρ_agreement:
shows "MC.ρ = (λf. if arr f then f ⋅ 𝗋[dom f] else null)"
proof
fix f
have "¬ arr f ⟹ MC.ρ f = null" by simp
moreover have "arr f ⟹ MC.ρ f = f ⋅ 𝗋[dom f]"
proof -
have "⋀a. ide a ⟹ 𝗋[a] = MC.runit a"
using ℐ_agreement T_def runit_char ι_in_hom iso_runit
apply (intro MC.runit_eqI)
apply auto
by blast
thus ?thesis
by (metis ide_dom local.ext seqE)
qed
ultimately show "MC.ρ f = (if arr f then f ⋅ 𝗋[dom f] else null)" by simp
qed
lemma lunit_agreement:
assumes "ide a"
shows "MC.lunit a = 𝗅[a]"
using assms comp_cod_arr 𝔩_agreement
by (metis (no_types, lifting) MC.𝔩_ide_simp ide_char in_homE lunit_in_hom)
lemma runit_agreement:
assumes "ide a"
shows "MC.runit a = 𝗋[a]"
using assms comp_cod_arr ρ_agreement
by (metis (no_types, lifting) MC.ρ_ide_simp ide_char in_homE runit_in_hom)
end
section "Strict Monoidal Category"
text‹
A monoidal category is \emph{strict} if the components of the associator and unitors
are all identities.
›
locale strict_monoidal_category =
monoidal_category +
assumes strict_assoc: "⟦ ide a0; ide a1; ide a2 ⟧ ⟹ ide 𝖺[a0, a1, a2]"
and strict_lunit: "ide a ⟹ 𝗅[a] = a"
and strict_runit: "ide a ⟹ 𝗋[a] = a"
begin
lemma strict_unit:
shows "ι = ℐ"
using strict_lunit unitor_coincidence(1) by auto
lemma tensor_assoc [simp]:
assumes "arr f0" and "arr f1" and "arr f2"
shows "(f0 ⊗ f1) ⊗ f2 = f0 ⊗ f1 ⊗ f2"
by (metis CC.arrI⇩P⇩C CCC.arrI⇩P⇩C α'.preserves_reflects_arr α'_simp assms(1-3)
assoc'_naturality ide_cod ide_dom inv_ide comp_arr_ide comp_ide_arr strict_assoc)
end
section "Opposite Monoidal Category"
text‹
The \emph{opposite} of a monoidal category has the same underlying category, but the
arguments to the tensor product are reversed and the associator is inverted and its
arguments reversed.
›
locale opposite_monoidal_category =
C: monoidal_category C T⇩C α⇩C ι
for C :: "'a comp" (infixr ‹⋅› 55)
and T⇩C :: "'a * 'a ⇒ 'a"
and α⇩C :: "'a * 'a * 'a ⇒ 'a"
and ι :: 'a
begin
abbreviation T
where "T f ≡ T⇩C (snd f, fst f)"
abbreviation α
where "α f ≡ C.α' (snd (snd f), fst (snd f), fst f)"
end
sublocale opposite_monoidal_category ⊆ monoidal_category C T α ι
proof -
interpret T: binary_endofunctor C T
using C.T.is_extensional C.CC.seq_char C.interchange by (unfold_locales, auto)
interpret ToTC: "functor" C.CCC.comp C T.ToTC
using T.functor_ToTC by auto
interpret ToCT: "functor" C.CCC.comp C T.ToCT
using T.functor_ToCT by auto
interpret α: natural_transformation C.CCC.comp C T.ToTC T.ToCT α
using C.α'.is_extensional C.CCC.dom_char C.CCC.cod_char T.ToTC_def T.ToCT_def
C.α'_simp C.α'.naturality
by (unfold_locales) auto
interpret α: natural_isomorphism C.CCC.comp C T.ToTC T.ToCT α
using C.α'.components_are_iso by (unfold_locales, simp)
interpret L: equivalence_functor C C ‹λf. T (C.cod ι, f)›
using C.R.equivalence_functor_axioms by simp
interpret R: equivalence_functor C C ‹λf. T (f, C.cod ι)›
using C.L.equivalence_functor_axioms by simp
show "monoidal_category C T α ι"
using C.unit_is_iso C.pentagon' C.comp_assoc
by (unfold_locales) auto
qed
context opposite_monoidal_category
begin
lemma lunit_simp:
assumes "C.ide a"
shows "lunit a = C.runit a"
using assms lunit_char C.iso_assoc by (intro C.runit_eqI, auto)
lemma runit_simp:
assumes "C.ide a"
shows "runit a = C.lunit a"
using assms runit_char C.iso_assoc by (intro C.lunit_eqI, auto)
end
section "Dual Monoidal Category"
text‹
The \emph{dual} of a monoidal category is obtained by reversing the arrows of the
underlying category. The tensor product remains the same, but the associators and
unitors are inverted.
›
locale dual_monoidal_category =
M: monoidal_category
begin
sublocale dual_category C ..
sublocale MM: product_category comp comp ..
interpretation T: binary_functor comp comp comp T
using M.T.is_extensional M.interchange MM.comp_char
by unfold_locales auto
interpretation T: binary_endofunctor comp ..
interpretation ToTC: "functor" T.CCC.comp comp T.ToTC
using T.functor_ToTC by blast
interpretation ToCT: "functor" T.CCC.comp comp T.ToCT
using T.functor_ToCT by blast
interpretation α: natural_transformation T.CCC.comp comp T.ToTC T.ToCT M.α'
using M.α'.is_extensional M.α'.is_natural_1 M.α'.is_natural_2
by unfold_locales auto
interpretation α: natural_isomorphism T.CCC.comp comp T.ToTC T.ToCT M.α'
by unfold_locales auto
interpretation L: equivalence_functor comp comp ‹M.tensor (cod (M.inv ι))›
proof -
interpret L: dual_equivalence_functor C C ‹M.tensor ℐ› ..
show "equivalence_functor comp comp (M.tensor (cod (M.inv ι)))"
using L.equivalence_functor_axioms
by (simp add: M.unit_is_iso)
qed
interpretation R: equivalence_functor comp comp ‹λf. M.tensor f (cod (M.inv ι))›
proof -
interpret R: dual_equivalence_functor C C ‹λf. M.tensor f ℐ› ..
show "equivalence_functor comp comp (λf. M.tensor f (cod (M.inv ι)))"
using R.equivalence_functor_axioms
by (simp add: M.unit_is_iso)
qed
sublocale monoidal_category comp T M.α' ‹M.inv ι›
using T.is_extensional M.unit_in_hom M.inv_in_hom M.unit_is_iso M.pentagon'
equivalence_functor_def category_axioms
by unfold_locales auto
lemma is_monoidal_category:
shows "monoidal_category comp T M.α' (M.inv ι)"
..
no_notation comp (infixr ‹⋅› 55)
lemma assoc_char:
assumes "ide a" and "ide b" and "ide c"
shows "assoc a b c = M.assoc' a b c" and "assoc' a b c = M.assoc a b c"
using assms M.inv_inv M.iso_inv_iso
apply force
by (metis assms M.α'_ide_simp M.comp_assoc_assoc'(2) M.ideD(1) M.iso_assoc
M.iso_cancel_left M.iso_inv_iso comp_assoc_assoc'(2) ide_char comp_def
tensor_preserves_ide)
lemma lunit_char:
assumes "ide a"
shows "lunit a = M.lunit' a"
proof -
have "M.lunit' a = lunit a"
proof (intro lunit_eqI)
show "in_hom (M.lunit' a) (tensor unity a) a"
using assms
by (simp add: M.lunit'_in_hom M.unit_is_iso)
show "tensor unity (M.lunit' a) = comp (tensor (M.inv ι) a) (assoc' unity unity a)"
proof -
have "M.inv (tensor ℐ (M.lunit a) ⋅ M.assoc ℐ ℐ a) = M.inv (tensor ι a)"
using assms M.triangle M.unitor_coincidence by auto
hence "M.assoc' ℐ ℐ a ⋅ tensor ℐ (M.lunit' a) = tensor (M.inv ι) a"
using assms M.inv_comp M.unit_is_iso by fastforce
thus ?thesis
using assms M.unit_is_iso assoc_char
M.invert_side_of_triangle(1)
[of "tensor (M.inv ι) a" "M.assoc' unity unity a" "tensor ℐ 𝗅⇧-⇧1[a]"]
by auto
qed
qed
thus ?thesis by simp
qed
lemma runit_char:
assumes "ide a"
shows "runit a = M.runit' a"
proof -
have "M.runit' a = runit a"
proof (intro runit_eqI)
show "in_hom (M.runit' a) (tensor a unity) a"
using assms
by (simp add: M.runit'_in_hom M.unit_is_iso)
show "tensor (M.runit' a) unity = comp (tensor a (M.inv ι)) (assoc a unity unity)"
proof -
have "M.inv (tensor a ι ⋅ M.assoc a ℐ ℐ) = M.inv (tensor (M.runit a) ℐ)"
using assms M.triangle [of a ℐ] M.unitor_coincidence by auto
hence "M.assoc' a ℐ ℐ ⋅ tensor a (M.inv ι) = tensor (M.runit' a) ℐ"
using assms M.inv_comp M.unit_in_hom M.unit_is_iso by auto
thus ?thesis
using assms M.unit_is_iso assoc_char by auto
qed
qed
thus ?thesis by simp
qed
end
section "Monoidal Language"
text‹
In this section we assume that a category @{term C} is given, and we define a
formal syntax of terms constructed from arrows of @{term C} using function symbols
that correspond to unity, composition, tensor, the associator and its formal inverse,
and the left and right unitors and their formal inverses.
We will use this syntax to state and prove the coherence theorem and then to construct
the free monoidal category generated by @{term C}.
›
locale monoidal_language =
C: category C
for C :: "'a comp" (infixr ‹⋅› 55)
begin