Theory CartesianMonoidalCategory
chapter "Cartesian Monoidal Category"
theory CartesianMonoidalCategory
imports MonoidalCategory Category3.CartesianCategory
begin
section "Symmetric Monoidal Category"
locale symmetric_monoidal_category =
monoidal_category C T α ι +
S: symmetry_functor C C +
ToS: composite_functor CC.comp CC.comp C S.map T +
σ: natural_isomorphism CC.comp C T ToS.map σ
for C :: "'a comp" (infixr ‹⋅› 55)
and T :: "'a * 'a ⇒ 'a"
and α :: "'a * 'a * 'a ⇒ 'a"
and ι :: 'a
and σ :: "'a * 'a ⇒ 'a" +
assumes sym_inverse: "⟦ ide a; ide b ⟧ ⟹ inverse_arrows (σ (a, b)) (σ (b, a))"
and unitor_coherence: "ide a ⟹ 𝗅[a] ⋅ σ (a, ℐ) = 𝗋[a]"
and assoc_coherence: "⟦ ide a; ide b; ide c ⟧ ⟹
α (b, c, a) ⋅ σ (a, b ⊗ c) ⋅ α (a, b, c)
= (b ⊗ σ (a, c)) ⋅ α (b, a, c) ⋅ (σ (a, b) ⊗ c)"
begin
abbreviation sym (‹𝗌[_, _]›)
where "sym a b ≡ σ (a, b)"
end
locale elementary_symmetric_monoidal_category =
elementary_monoidal_category C tensor unity lunit runit assoc
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" (‹𝖺[_, _, _]›)
and sym :: "'a ⇒ 'a ⇒ 'a" (‹𝗌[_, _]›) +
assumes sym_in_hom: "⟦ ide a; ide b ⟧ ⟹ «𝗌[a, b] : a ⊗ b → b ⊗ a»"
and sym_naturality: "⟦ arr f; arr g ⟧ ⟹ 𝗌[cod f, cod g] ⋅ (f ⊗ g) = (g ⊗ f) ⋅ 𝗌[dom f, dom g]"
and sym_inverse: "⟦ ide a; ide b ⟧ ⟹ inverse_arrows 𝗌[a, b] 𝗌[b, a]"
and unitor_coherence: "ide a ⟹ 𝗅[a] ⋅ 𝗌[a, ℐ] = 𝗋[a]"
and assoc_coherence: "⟦ ide a; ide b; ide c ⟧ ⟹
𝖺[b, c, a] ⋅ 𝗌[a, b ⊗ c] ⋅ 𝖺[a, b, c]
= (b ⊗ 𝗌[a, c]) ⋅ 𝖺[b, a, c] ⋅ (𝗌[a, b] ⊗ c)"
begin
lemma sym_simps [simp]:
assumes "ide a" and "ide b"
shows "arr 𝗌[a, b]"
and "dom 𝗌[a, b] = a ⊗ b"
and "cod 𝗌[a, b] = b ⊗ a"
using assms sym_in_hom by auto
interpretation CC: product_category C C ..
sublocale MC: monoidal_category C T α ι
using induces_monoidal_category by simp
interpretation S: symmetry_functor C C ..
interpretation ToS: composite_functor CC.comp CC.comp C S.map T ..
definition σ :: "'a * 'a ⇒ 'a"
where "σ f ≡ if CC.arr f then 𝗌[cod (fst f), cod (snd f)] ⋅ (fst f ⊗ snd f) else null"
interpretation σ: natural_isomorphism CC.comp C T ToS.map σ
proof -
interpret σ: transformation_by_components CC.comp C T ToS.map "λa. 𝗌[fst a, snd a]"
using sym_in_hom sym_naturality
by unfold_locales auto
interpret σ: natural_isomorphism CC.comp C T ToS.map σ.map
using sym_inverse σ.map_simp_ide
by unfold_locales auto
have "σ = σ.map"
using σ_def σ.map_def sym_naturality by fastforce
thus "natural_isomorphism CC.comp C T ToS.map σ"
using σ.natural_isomorphism_axioms by presburger
qed
interpretation symmetric_monoidal_category C T α ι σ
proof
show "⋀a b. ⟦ ide a; ide b ⟧ ⟹ inverse_arrows (σ (a, b)) (σ (b, a))"
using sym_inverse comp_arr_dom σ_def by auto
show "⋀a. ide a ⟹ MC.lunit a ⋅ σ (a, MC.unity) = MC.runit a"
using lunit_agreement ℐ_agreement sym_in_hom comp_arr_dom
unitor_coherence runit_agreement σ_def
by simp
show "⋀a b c. ⟦ ide a; ide b; ide c ⟧ ⟹
MC.assoc b c a ⋅ σ (a, MC.tensor b c) ⋅ MC.assoc a b c =
MC.tensor b (σ (a, c)) ⋅ MC.assoc b a c ⋅ MC.tensor (σ (a, b)) c"
using sym_in_hom tensor_preserves_ide σ_def assoc_coherence
comp_arr_dom comp_cod_arr
by simp
qed
lemma induces_symmetric_monoidal_category⇩C⇩M⇩C:
shows "symmetric_monoidal_category C T α ι σ"
..
end
context symmetric_monoidal_category
begin
interpretation EMC: elementary_monoidal_category C tensor unity lunit runit assoc
using induces_elementary_monoidal_category by auto
lemma induces_elementary_symmetric_monoidal_category⇩C⇩M⇩C:
shows "elementary_symmetric_monoidal_category
C tensor unity lunit runit assoc (λa b. σ (a, b))"
using σ.naturality unitor_coherence assoc_coherence sym_inverse
by unfold_locales auto
end
locale dual_symmetric_monoidal_category =
M: symmetric_monoidal_category
begin
sublocale dual_monoidal_category C T α ι ..
interpretation S: symmetry_functor comp comp ..
interpretation ToS: composite_functor MM.comp MM.comp comp S.map T ..
sublocale σ': inverse_transformation M.CC.comp C T M.ToS.map σ ..
interpretation σ: natural_transformation MM.comp comp T ToS.map σ'.map
using σ'.extensionality σ'.naturality1 σ'.naturality2
by unfold_locales auto
interpretation σ: natural_isomorphism MM.comp comp T ToS.map σ'.map
by unfold_locales auto
sublocale symmetric_monoidal_category comp T M.α' ‹M.inv ι› σ'.map
proof
show "⋀a b. ⟦ide a; ide b⟧ ⟹ inverse_arrows (σ'.map (a, b)) (σ'.map (b, a))"
apply auto
by (metis M.inverse_arrowsE M.inverse_unique M.isoI M.sym_inverse ide_char
iso_char comp_def section_retraction_of_iso(1))
show "⋀a. ide a ⟹ lunit a ⋅⇧o⇧p σ'.map (a, unity) = runit a"
using M.unitor_coherence M.unit_in_hom M.unit_is_iso lunit_char runit_char
apply auto
by (metis M.inv_comp_left(1) M.iso_lunit M.iso_runit)
show "⋀a b c.
⟦ide a; ide b; ide c⟧
⟹ assoc b c a ⋅⇧o⇧p σ'.map (a, tensor b c) ⋅⇧o⇧p assoc a b c =
(tensor b (σ'.map (a, c))) ⋅⇧o⇧p assoc b a c ⋅⇧o⇧p (tensor (σ'.map (a, b)) c)"
proof -
fix a b c
assume a: "ide a" and b: "ide b" and c: "ide c"
show "assoc b c a ⋅⇧o⇧p σ'.map (a, tensor b c) ⋅⇧o⇧p assoc a b c =
(tensor b (σ'.map (a, c))) ⋅⇧o⇧p assoc b a c ⋅⇧o⇧p (tensor (σ'.map (a, b)) c)"
proof -
have "assoc b c a ⋅⇧o⇧p σ'.map (a, tensor b c) ⋅⇧o⇧p assoc a b c =
(𝖺⇧-⇧1[a, b, c] ⋅ M.inv 𝗌[a, tensor b c]) ⋅ 𝖺⇧-⇧1[b, c, a]"
using a b c by auto
also have "... = M.inv (𝗌[a, tensor b c] ⋅ M.assoc a b c) ⋅ M.inv (M.assoc b c a)"
using a b c M.iso_assoc M.inv_comp by auto
also have "... = M.inv (M.assoc b c a ⋅ 𝗌[a, tensor b c] ⋅ M.assoc a b c)"
using a b c M.iso_assoc
M.inv_comp [of "𝗌[a, tensor b c] ⋅ M.assoc a b c" "M.assoc b c a"]
by fastforce
also have "... = M.inv (tensor b 𝗌[a, c] ⋅ 𝖺[b, a, c] ⋅ (tensor 𝗌[a, b] c))"
using a b c M.assoc_coherence by simp
also have "... = M.inv (𝖺[b, a, c] ⋅ (tensor 𝗌[a, b] c)) ⋅ M.inv (tensor b 𝗌[a, c])"
using a b c M.iso_assoc
M.inv_comp [of "𝖺[b, a, c] ⋅ (tensor 𝗌[a, b] c)"]
by fastforce
also have "... =
(tensor (M.inv 𝗌[a, b]) c ⋅ M.inv 𝖺[b, a, c]) ⋅ tensor b (M.inv 𝗌[a, c])"
using a b c M.iso_assoc M.inv_comp by simp
also have "... =
(tensor b (σ'.map (a, c))) ⋅⇧o⇧p assoc b a c ⋅⇧o⇧p (tensor (σ'.map (a, b)) c)"
using a b c by auto
finally show ?thesis by simp
qed
qed
qed
lemma is_symmetric_monoidal_category:
shows "symmetric_monoidal_category comp T M.α' (M.inv ι) σ'.map"
..
end
section "Cartesian Monoidal Category"
text ‹
Here we define ``cartesian monoidal category'' by imposing additional properties,
but not additional structure, on top of ``monoidal category''. The additional properties
are that the unit is a terminal object and that the tensor is a categorical product,
with projections defined in terms of unitors, terminators, and tensor. It then follows
that the associators are induced by the product structure.
›
locale cartesian_monoidal_category =
monoidal_category C T α ι
for C :: "'a comp" (infixr ‹⋅› 55)
and T :: "'a * 'a ⇒ 'a"
and α :: "'a * 'a * 'a ⇒ 'a"
and ι :: 'a +
assumes terminal_unity: "terminal ℐ"
and tensor_is_product:
"⟦ide a; ide b; «t⇩a : a → ℐ»; «t⇩b : b → ℐ»⟧ ⟹
has_as_binary_product a b (𝗋[a] ⋅ (a ⊗ t⇩b)) (𝗅[b] ⋅ (t⇩a ⊗ b))"
begin
sublocale category_with_terminal_object
using terminal_unity by unfold_locales blast
lemma is_category_with_terminal_object:
shows "category_with_terminal_object C"
..
definition the_trm (‹𝗍[_]›)
where "the_trm ≡ λf. THE t. «t : dom f → ℐ»"
lemma trm_in_hom [intro]:
assumes "ide a"
shows "«𝗍[a] : a → ℐ»"
unfolding the_trm_def
using assms theI [of "λt. «t : dom a → ℐ»"] terminal_unity terminal_arr_unique
by (metis ideD(2) terminalE)
lemma trm_simps [simp]:
assumes "ide a"
shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = ℐ"
using assms trm_in_hom by auto
interpretation elementary_category_with_terminal_object C ℐ the_trm
proof
show "ide ℐ"
using ide_unity by blast
fix a
show "ide a ⟹ «the_trm a : a → ℐ»"
using the_trm_def theI [of "λt. «t : dom a → ℐ»"] terminalE terminal_unity by auto
thus "⋀f. ⟦ide a; «f : a → ℐ»⟧ ⟹ f = the_trm a"
using theI [of "λt. «t : dom a → ℐ»"]
by (metis terminalE terminal_unity)
qed
lemma extends_to_elementary_category_with_terminal_object⇩C⇩M⇩C:
shows "elementary_category_with_terminal_object C ℐ the_trm"
..
definition pr⇩0 (‹𝔭⇩0[_, _]›)
where "pr⇩0 a b ≡ 𝗅[b] ⋅ (𝗍[a] ⊗ b)"
definition pr⇩1 (‹𝔭⇩1[_, _]›)
where "pr⇩1 a b ≡ 𝗋[a] ⋅ (a ⊗ 𝗍[b])"
sublocale ECC: elementary_category_with_binary_products C pr⇩0 pr⇩1
proof
fix f g
assume fg: "span f g"
have "has_as_binary_product (cod f) (cod g) 𝔭⇩1[cod f, cod g] 𝔭⇩0[cod f, cod g]"
using fg tensor_is_product pr⇩0_def pr⇩1_def by auto
thus "∃!l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
using fg
by (elim has_as_binary_productE) blast
qed (unfold pr⇩0_def pr⇩1_def, auto)
lemma induces_elementary_category_with_binary_products⇩C⇩M⇩C:
shows "elementary_category_with_binary_products C pr⇩0 pr⇩1"
..
lemma is_category_with_binary_products:
shows "category_with_binary_products C"
using ECC.is_category_with_binary_products by blast
sublocale category_with_binary_products C
using is_category_with_binary_products by blast
sublocale ECC: elementary_cartesian_category C pr⇩0 pr⇩1 ℐ the_trm ..
lemma extends_to_elementary_cartesian_category⇩C⇩M⇩C:
shows "elementary_cartesian_category C pr⇩0 pr⇩1 ℐ the_trm"
..
lemma is_cartesian_category:
shows "cartesian_category C"
using ECC.is_cartesian_category by simp
sublocale cartesian_category C
using is_cartesian_category by blast
abbreviation dup (‹𝖽[_]›)
where "dup ≡ ECC.dup"
abbreviation tuple (‹⟨_, _⟩›)
where "⟨f, g⟩ ≡ ECC.tuple f g"
lemma prod_eq_tensor:
shows "ECC.prod = tensor"
proof -
have "⋀f g. ECC.prod f g = f ⊗ g"
proof -
fix f g
show "ECC.prod f g = f ⊗ g"
proof (cases "arr f ∧ arr g")
show "¬ (arr f ∧ arr g) ⟹ ?thesis"
by (metis CC.arrE ECC.prod_def ECC.tuple_ext T.extensionality fst_conv seqE snd_conv)
assume 0: "arr f ∧ arr g"
have 1: "span (f ⋅ 𝔭⇩1[dom f, dom g]) (g ⋅ 𝔭⇩0[dom f, dom g])"
using 0 by simp
have "𝔭⇩1[cod f, cod g] ⋅ ECC.prod f g = 𝔭⇩1[cod f, cod g] ⋅ (f ⊗ g)"
proof -
have "𝔭⇩1[cod f, cod g] ⋅ ECC.prod f g =
𝔭⇩1[cod f, cod g] ⋅ ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
unfolding ECC.prod_def by simp
also have "... = f ⋅ 𝔭⇩1[dom f, dom g]"
using 0 1 ECC.pr_tuple(1) by fastforce
also have "... = (f ⋅ 𝗋[dom f]) ⋅ (dom f ⊗ 𝗍[dom g])"
unfolding pr⇩1_def
using comp_assoc by simp
also have "... = (𝗋[cod f] ⋅ (f ⊗ ℐ)) ⋅ (dom f ⊗ 𝗍[dom g])"
using 0 runit_naturality by auto
also have "... = 𝗋[cod f] ⋅ (f ⊗ ℐ) ⋅ (dom f ⊗ 𝗍[dom g])"
using comp_assoc by simp
also have "... = 𝗋[cod f] ⋅ (cod f ⊗ 𝗍[cod g]) ⋅ (f ⊗ g)"
using 0 interchange comp_arr_dom comp_cod_arr trm_naturality trm_simps(1)
by force
also have "... = (𝗋[cod f] ⋅ (cod f ⊗ 𝗍[cod g])) ⋅ (f ⊗ g)"
using comp_assoc by simp
also have "... = 𝔭⇩1[cod f, cod g] ⋅ (f ⊗ g)"
unfolding pr⇩1_def by simp
finally show ?thesis by blast
qed
moreover have "𝔭⇩0[cod f, cod g] ⋅ ECC.prod f g = 𝔭⇩0[cod f, cod g] ⋅ (f ⊗ g)"
proof -
have "𝔭⇩0[cod f, cod g] ⋅ ECC.prod f g =
𝔭⇩0[cod f, cod g] ⋅ ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
unfolding ECC.prod_def by simp
also have "... = g ⋅ 𝔭⇩0[dom f, dom g]"
using 0 1 ECC.pr_tuple by fastforce
also have "... = (g ⋅ 𝗅[dom g]) ⋅ (𝗍[dom f] ⊗ dom g)"
unfolding pr⇩0_def
using comp_assoc by simp
also have "... = (𝗅[cod g] ⋅ (ℐ ⊗ g)) ⋅ (𝗍[dom f] ⊗ dom g)"
using 0 lunit_naturality by auto
also have "... = 𝗅[cod g] ⋅ (ℐ ⊗ g) ⋅ (𝗍[dom f] ⊗ dom g)"
using comp_assoc by simp
also have "... = 𝗅[cod g] ⋅ (𝗍[cod f] ⊗ cod g) ⋅ (f ⊗ g)"
using 0 interchange comp_arr_dom comp_cod_arr trm_naturality trm_simps(1)
by force
also have "... = (𝗅[cod g] ⋅ (𝗍[cod f] ⊗ cod g)) ⋅ (f ⊗ g)"
using comp_assoc by simp
also have "... = 𝔭⇩0[cod f, cod g] ⋅ (f ⊗ g)"
unfolding pr⇩0_def by simp
finally show ?thesis by blast
qed
ultimately show ?thesis
by (metis 0 1 ECC.pr_naturality(1-2) ECC.tuple_pr_arr ide_cod)
qed
qed
thus ?thesis by blast
qed
lemma Prod_eq_T:
shows "ECC.Prod = T"
proof
fix fg
show "ECC.Prod fg = T fg"
using prod_eq_tensor
by (cases "CC.arr fg") auto
qed
lemma tuple_pr [simp]:
assumes "ide a" and "ide b"
shows "⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ = a ⊗ b"
using assms prod_eq_tensor by simp
lemma tensor_expansion:
assumes "arr f" and "arr g"
shows "f ⊗ g = ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"
using assms
by (metis ECC.prod_def prod_eq_tensor)
text ‹
It is somewhat amazing that once the tensor product has been assumed to be a
categorical product with the indicated projections, then the associators are
forced to be those induced by the categorical product.
›
lemma pr_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
and "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
and "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a ⊗ b, c]"
proof -
show "𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
proof -
have "𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c] = (𝗋[a] ⋅ (a ⊗ ι ⋅ (𝗍[b] ⊗ 𝗍[c]))) ⋅ 𝖺[a, b, c]"
by (metis ECC.trm_tensor ECC.unit_eq_trm arr_cod_iff_arr assms(2-3) comp_cod_arr
dom_lunit ide_unity pr⇩1_def prod_eq_tensor trm_naturality trm_one trm_simps(1)
unitor_coincidence(1))
also have "... = (𝗋[a] ⋅ (a ⊗ ι) ⋅ (a ⊗ 𝗍[b] ⊗ 𝗍[c])) ⋅ 𝖺[a, b, c]"
using assms interchange unit_in_hom_ax by auto
also have "... = 𝗋[a] ⋅ (a ⊗ ι) ⋅ (a ⊗ 𝗍[b] ⊗ 𝗍[c]) ⋅ 𝖺[a, b, c]"
using comp_assoc by simp
also have "... = 𝗋[a] ⋅ (a ⊗ ι) ⋅ 𝖺[a, ℐ, ℐ] ⋅ ((a ⊗ 𝗍[b]) ⊗ 𝗍[c])"
using assms assoc_naturality [of a "𝗍[b]" "𝗍[c]"] by force
also have "... = 𝗋[a] ⋅ (𝗋[a] ⊗ ℐ) ⋅ ((a ⊗ 𝗍[b]) ⊗ 𝗍[c])"
using assms runit_char comp_assoc by simp
also have "... = 𝗋[a] ⋅ (𝔭⇩1[a, b] ⊗ 𝗍[c])"
using assms comp_arr_dom comp_cod_arr interchange [of "𝗋[a]" "a ⊗ 𝗍[b]" ℐ "𝗍[c]"]
by (metis ECC.pr_simps(4) pr⇩1_def trm_simps(1) trm_simps(3))
also have "... = 𝗋[a] ⋅ (𝔭⇩1[a, b] ⋅ (a ⊗ b) ⊗ ℐ ⋅ 𝗍[c])"
using assms comp_arr_dom comp_cod_arr
by (metis (no_types, lifting) ECC.pr_simps(4-5) prod_eq_tensor trm_simps(1,3))
also have "... = 𝗋[a] ⋅ (𝔭⇩1[a, b] ⊗ ℐ) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using assms interchange [of "𝔭⇩1[a, b]" "a ⊗ b" ℐ " 𝗍[c]"]
by (metis (no_types, lifting) ECC.pr_simps(4-5) Prod_eq_T comp_arr_dom comp_cod_arr
fst_conv snd_conv trm_simps(1,3))
also have "... = (𝗋[a] ⋅ (𝔭⇩1[a, b] ⊗ ℐ)) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using comp_assoc by simp
also have "... = (𝔭⇩1[a, b] ⋅ 𝗋[a ⊗ b]) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using assms runit_naturality
by (metis (no_types, lifting) ECC.cod_pr1 ECC.pr_simps(4,5) prod_eq_tensor)
also have "... = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
using pr⇩1_def comp_assoc by simp
finally show ?thesis by blast
qed
show "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
proof -
have "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] =
𝗋[b] ⋅ (b ⊗ 𝗍[c]) ⋅ 𝗅[b ⊗ c] ⋅ 𝖺[ℐ, b, c] ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms pr⇩0_def pr⇩1_def assoc_naturality [of "𝗍[a]" b c] comp_assoc by auto
also have "... = 𝗋[b] ⋅ ((b ⊗ 𝗍[c]) ⋅ 𝗅[b ⊗ c]) ⋅ 𝖺[ℐ, b, c] ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using comp_assoc by simp
also have "... = 𝗋[b] ⋅ (𝗅[b ⊗ ℐ] ⋅ (ℐ ⊗ b ⊗ 𝗍[c])) ⋅ 𝖺[ℐ, b, c] ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms lunit_naturality [of "b ⊗ 𝗍[c]"] by auto
also have "... = 𝗋[b] ⋅ 𝗅[b ⊗ ℐ] ⋅ ((ℐ ⊗ b ⊗ 𝗍[c]) ⋅ 𝖺[ℐ, b, c]) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using comp_assoc by simp
also have "... = 𝗋[b] ⋅ 𝗅[b ⊗ ℐ] ⋅ (𝖺[ℐ, b, ℐ] ⋅ ((ℐ ⊗ b) ⊗ 𝗍[c])) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms assoc_naturality [of ℐ b "𝗍[c]"] by auto
also have "... = 𝗋[b] ⋅ (𝗅[b] ⊗ ℐ) ⋅ ((ℐ ⊗ b) ⊗ 𝗍[c]) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms lunit_tensor [of b ℐ] comp_assoc
by (metis ide_unity lunit_tensor')
also have "... = 𝗋[b] ⋅ (𝗅[b] ⊗ ℐ) ⋅ ((𝗍[a] ⊗ b) ⊗ ℐ) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using assms comp_arr_dom comp_cod_arr interchange by simp
also have "... = (𝗋[b] ⋅ (𝔭⇩0[a, b] ⊗ ℐ)) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using assms pr⇩0_def ECC.pr_simps(1) R.preserves_comp comp_assoc by simp
also have "... = (𝔭⇩0[a, b] ⋅ 𝗋[a ⊗ b]) ⋅ ((a ⊗ b) ⊗ 𝗍[c])"
using assms pr⇩0_def runit_naturality [of "𝔭⇩0[a, b]"] comp_assoc by simp
also have "... = 𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
using pr⇩0_def pr⇩1_def comp_assoc by simp
finally show ?thesis by blast
qed
show "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a ⊗ b, c]"
proof -
have "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] =
𝗅[c] ⋅ (𝗍[b] ⊗ c) ⋅ 𝗅[b ⊗ c] ⋅ (𝗍[a] ⊗ b ⊗ c) ⋅ 𝖺[a, b, c]"
using pr⇩0_def comp_assoc by simp
also have "... = 𝗅[c] ⋅ ((𝗍[b] ⊗ c) ⋅ 𝗅[b ⊗ c]) ⋅ 𝖺[ℐ, b, c] ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms assoc_naturality [of "𝗍[a]" b c] comp_assoc by simp
also have "... = 𝗅[c] ⋅ (𝗅[ℐ ⊗ c] ⋅ (ℐ ⊗ 𝗍[b] ⊗ c)) ⋅ 𝖺[ℐ, b, c] ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms lunit_naturality [of "𝗍[b] ⊗ c"] by simp
also have "... = 𝗅[c] ⋅ 𝗅[ℐ ⊗ c] ⋅ (𝖺[ℐ, ℐ, c] ⋅ ((ℐ ⊗ 𝗍[b]) ⊗ c)) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms assoc_naturality [of ℐ "𝗍[b]" c] comp_assoc by simp
also have "... = 𝗅[c] ⋅ (𝗅[ℐ ⊗ c] ⋅ 𝖺[ℐ, ℐ, c]) ⋅ ((ℐ ⊗ 𝗍[b]) ⊗ c) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using comp_assoc by simp
also have "... = 𝗅[c] ⋅ (ι ⊗ c) ⋅ ((ℐ ⊗ 𝗍[b]) ⊗ c) ⋅ ((𝗍[a] ⊗ b) ⊗ c)"
using assms lunit_tensor' unitor_coincidence(1) by simp
also have "... = 𝗅[c] ⋅ (ι ⊗ c) ⋅ ((ℐ ⊗ 𝗍[b]) ⋅ (𝗍[a] ⊗ b) ⊗ c)"
using assms comp_arr_dom comp_cod_arr
by (metis arr_tensor ide_char interchange trm_simps(1-3))
also have "... = 𝗅[c] ⋅ (ι ⊗ c) ⋅ ((𝗍[a] ⊗ 𝗍[b]) ⊗ c)"
using assms comp_arr_dom comp_cod_arr interchange by simp
also have "... = 𝗅[c] ⋅ (ι ⋅ (𝗍[a] ⊗ 𝗍[b]) ⊗ c)"
using assms interchange unit_in_hom_ax by auto
also have "... = 𝔭⇩0[a ⊗ b, c]"
using assms pr⇩0_def ECC.trm_tensor category.comp_arr_dom category_axioms prod_eq_tensor
trm_one unit_in_hom_ax unitor_coincidence(1)
by fastforce
finally show ?thesis by blast
qed
qed
lemma assoc_agreement:
assumes "ide a" and "ide b" and "ide c"
shows "ECC.assoc a b c = 𝖺[a, b, c]"
proof -
have "𝔭⇩1[a, b ⊗ c] ⋅ ECC.assoc a b c = 𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c]"
using assms ECC.pr_assoc(3) pr_assoc(1) prod_eq_tensor by force
moreover have "𝔭⇩0[a, b ⊗ c] ⋅ ECC.assoc a b c = 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c]"
proof -
have "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ ECC.assoc a b c = 𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c]"
using assms ECC.pr_assoc(2) pr_assoc(2) prod_eq_tensor by force
moreover have "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ ECC.assoc a b c =
𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c]"
using assms prod_eq_tensor ECC.pr_assoc(1) pr_assoc(3) by force
ultimately show ?thesis
using assms prod_eq_tensor
ECC.pr_joint_monic
[of b c "𝔭⇩0[a, b ⊗ c] ⋅ ECC.assoc a b c " "𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c]"]
by fastforce
qed
ultimately show ?thesis
using assms prod_eq_tensor
ECC.pr_joint_monic [of a "b ⊗ c" "ECC.assoc a b c" "𝖺[a, b, c]"]
by fastforce
qed
lemma lunit_eq:
assumes "ide a"
shows "𝔭⇩0[ℐ, a] = 𝗅[a]"
by (simp add: assms comp_arr_dom pr⇩0_def trm_one)
lemma runit_eq:
assumes "ide a"
shows "𝔭⇩1[a, ℐ] = 𝗋[a]"
by (simp add: assms comp_arr_dom pr⇩1_def trm_one)
lemma lunit'_as_tuple:
assumes "ide a"
shows "tuple 𝗍[a] a = lunit' a"
using ECC.inverse_arrows_lunit assms inverse_unique lunit_eq by fastforce
lemma runit'_as_tuple:
assumes "ide a"
shows "tuple a 𝗍[a] = runit' a"
using ECC.inverse_arrows_runit assms inverse_unique runit_eq by fastforce
interpretation S: symmetry_functor C C ..
interpretation ToS: composite_functor CC.comp CC.comp C S.map T ..
interpretation σ: natural_transformation CC.comp C T ToS.map ECC.σ
proof -
have "ECC.Prod' = ToS.map"
proof
fix fg
show "ECC.Prod' fg = ToS.map fg"
using prod_eq_tensor
by (metis CC.arr_char ECC.prod_def ECC.tuple_ext S.map_def ToS.extensionality o_apply seqE)
qed
thus "natural_transformation CC.comp C T ToS.map ECC.σ"
using Prod_eq_T ECC.σ_naturalitytransformation by simp
qed
interpretation σ: natural_isomorphism CC.comp C T ToS.map ECC.σ
using ECC.sym_inverse_arrows comp_arr_dom
by unfold_locales auto
sublocale SMC: symmetric_monoidal_category C T α ι ECC.σ
proof
show "⋀a b. ⟦ide a; ide b⟧ ⟹ inverse_arrows (ECC.σ (a, b)) (ECC.σ (b, a))"
using comp_arr_dom by auto
show "⋀a. ide a ⟹ 𝗅[a] ⋅ ECC.σ (a, ℐ) = 𝗋[a]"
using σ.naturality prod_eq_tensor
by (metis (no_types, lifting) CC.arr_char ECC.prj_sym(1) R.preserves_ide
𝔩_ide_simp ρ_ide_simp σ.preserves_reflects_arr comp_arr_ide fst_conv
ideD(1) ideD(3) ide_unity lunit_naturality pr⇩0_def pr⇩1_def runit_naturality
snd_conv trm_one)
show "⋀a b c. ⟦ide a; ide b; ide c⟧ ⟹
𝖺[b, c, a] ⋅ ECC.σ (a, b ⊗ c) ⋅ 𝖺[a, b, c] =
(b ⊗ ECC.σ (a, c)) ⋅ 𝖺[b, a, c] ⋅ (ECC.σ (a, b) ⊗ c)"
proof -
fix a b c
assume a: "ide a" and b: "ide b" and c: "ide c"
show "𝖺[b, c, a] ⋅ ECC.σ (a, b ⊗ c) ⋅ 𝖺[a, b, c] =
(b ⊗ ECC.σ (a, c)) ⋅ 𝖺[b, a, c] ⋅ (ECC.σ (a, b) ⊗ c)"
using a b c prod_eq_tensor assoc_agreement comp_arr_dom ECC.sym_assoc_coherence [of a b c]
by simp
qed
qed
end
section "Elementary Cartesian Monoidal Category"
locale elementary_cartesian_monoidal_category =
elementary_monoidal_category C tensor unity lunit runit assoc
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" (‹𝖺[_, _, _]›)
and trm :: "'a ⇒ 'a" (‹𝗍[_]›)
and dup :: "'a ⇒ 'a" (‹𝖽[_]›) +
assumes trm_in_hom: "ide a ⟹ «𝗍[a] : a → ℐ»"
and trm_unity: "𝗍[ℐ] = ℐ"
and trm_naturality: "arr f ⟹ 𝗍[cod f] ⋅ f = 𝗍[dom f]"
and dup_in_hom [intro]: "ide a ⟹ «𝖽[a] : a → a ⊗ a»"
and dup_naturality: "arr f ⟹ 𝖽[cod f] ⋅ f = (f ⊗ f) ⋅ 𝖽[dom f]"
and prj0_dup: "ide a ⟹ 𝗋[a] ⋅ (a ⊗ 𝗍[a]) ⋅ 𝖽[a] = a"
and prj1_dup: "ide a ⟹ 𝗅[a] ⋅ (𝗍[a] ⊗ a) ⋅ 𝖽[a] = a"
and tuple_prj: "⟦ ide a; ide b ⟧ ⟹ (𝗋[a] ⋅ (a ⊗ 𝗍[b]) ⊗ 𝗅[b] ⋅ (𝗍[a] ⊗ b)) ⋅ 𝖽[a ⊗ b] = a ⊗ b"
context cartesian_monoidal_category
begin
interpretation elementary_category_with_terminal_object C ℐ the_trm
using extends_to_elementary_category_with_terminal_object⇩C⇩M⇩C by blast
interpretation elementary_monoidal_category C tensor unity lunit runit assoc
using induces_elementary_monoidal_category by simp
interpretation elementary_cartesian_monoidal_category C
tensor unity lunit runit assoc the_trm dup
using ECC.trm_one ECC.trm_naturality ECC.tuple_in_hom' prod_eq_tensor ECC.dup_naturality in_homI
ECC.comp_runit_term_dup runit_eq ECC.comp_lunit_term_dup lunit_eq ECC.tuple_expansion
comp_cod_arr
apply unfold_locales
apply auto
proof -
fix a b
assume a: "ide a" and b: "ide b"
show "(𝗋[a] ⋅ (a ⊗ 𝗍[b]) ⊗ 𝗅[b] ⋅ (𝗍[a] ⊗ b)) ⋅ 𝖽[a ⊗ b] = a ⊗ b"
using a b ECC.tuple_pr pr⇩0_def pr⇩1_def prod_eq_tensor
by (metis ECC.pr_simps(5) ECC.span_pr ECC.tuple_expansion)
qed
lemma induces_elementary_cartesian_monoidal_category⇩C⇩M⇩C:
shows "elementary_cartesian_monoidal_category C tensor ℐ lunit runit assoc the_trm dup"
..
end
context elementary_cartesian_monoidal_category
begin
lemma trm_simps [simp]:
assumes "ide a"
shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = ℐ"
using assms trm_in_hom by auto
lemma dup_simps [simp]:
assumes "ide a"
shows "arr 𝖽[a]" and "dom 𝖽[a] = a" and "cod 𝖽[a] = a ⊗ a"
using assms dup_in_hom by auto
interpretation elementary_category_with_terminal_object C ℐ trm
apply unfold_locales
apply auto
by (metis comp_cod_arr in_homE trm_naturality trm_unity)
lemma is_elementary_category_with_terminal_object:
shows "elementary_category_with_terminal_object C ℐ trm"
..
interpretation MC: monoidal_category C T α ι
using induces_monoidal_category by auto
interpretation ECBP: elementary_category_with_binary_products C
‹λa b. 𝗅[b] ⋅ (𝗍[a] ⊗ b)› ‹λa b. 𝗋[a] ⋅ (a ⊗ 𝗍[b])›
proof -
let ?pr⇩0 = "λa b. 𝗅[b] ⋅ (𝗍[a] ⊗ b)"
let ?pr⇩1 = "λa b. 𝗋[a] ⋅ (a ⊗ 𝗍[b])"
show "elementary_category_with_binary_products C ?pr⇩0 ?pr⇩1"
proof
fix a b
assume a: "ide a" and b: "ide b"
show 0: "cod (?pr⇩0 a b) = b"
by (metis a arr_tensor b cod_comp cod_tensor ide_char in_homE lunit_in_hom
seqI trm_simps(1,3))
show 1: "cod (?pr⇩1 a b) = a"
by (metis a arr_tensor b cod_comp cod_tensor ideD(1,3) in_homE runit_in_hom
seqI trm_simps(1,3))
show "span (?pr⇩1 a b) (?pr⇩0 a b)"
by (metis 0 1 a arr_cod_iff_arr b dom_cod dom_comp dom_tensor ideD(1) trm_simps(1-2))
next
fix f g
assume fg: "span f g"
show "∃!l. ?pr⇩1 (cod f) (cod g) ⋅ l = f ∧ ?pr⇩0 (cod f) (cod g) ⋅ l = g"
proof
show 1: "?pr⇩1 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] = f ∧
?pr⇩0 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] = g"
proof
show "?pr⇩1 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] = f"
proof -
have "?pr⇩1 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] =
MC.runit (cod f) ⋅ (MC.tensor (cod f) 𝗍[cod g] ⋅ (f ⊗ g)) ⋅ 𝖽[dom f]"
by (simp add: fg comp_assoc runit_agreement)
also have "... = MC.runit (cod f) ⋅ (MC.tensor f ℐ ⋅ (dom f ⊗ 𝗍[dom g])) ⋅ 𝖽[dom f]"
using fg
by (simp add: comp_arr_dom comp_cod_arr interchange trm_naturality)
also have "... = (MC.runit (cod f) ⋅ MC.tensor f ℐ ) ⋅ (dom f ⊗ 𝗍[dom g]) ⋅ 𝖽[dom f]"
using comp_assoc by simp
also have "... = f ⋅ ?pr⇩1 (dom f) (dom g) ⋅ 𝖽[dom f]"
using MC.runit_naturality ℐ_agreement fg comp_assoc runit_agreement by force
also have "... = f"
using fg comp_arr_dom comp_assoc prj0_dup runit_agreement by fastforce
finally show ?thesis by blast
qed
show "?pr⇩0 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] = g"
proof -
have "?pr⇩0 (cod f) (cod g) ⋅ (f ⊗ g) ⋅ 𝖽[dom f] =
MC.lunit (cod g) ⋅ (MC.tensor 𝗍[cod f] (cod g) ⋅ (f ⊗ g)) ⋅ 𝖽[dom f]"
by (simp add: fg comp_assoc lunit_agreement)
also have "... = MC.lunit (cod g) ⋅ (MC.tensor ℐ g ⋅ (𝗍[dom f] ⊗ dom g)) ⋅ 𝖽[dom f]"
using fg
by (simp add: comp_arr_dom comp_cod_arr interchange trm_naturality)
also have "... = (MC.lunit (cod g) ⋅ MC.tensor ℐ g) ⋅ (𝗍[dom f] ⊗ dom g) ⋅ 𝖽[dom f]"
using comp_assoc by simp
also have "... = g ⋅ ?pr⇩0 (dom f) (dom g) ⋅ 𝖽[dom f]"
using MC.lunit_naturality ℐ_agreement fg comp_assoc lunit_agreement by force
also have "... = g"
using fg comp_arr_dom comp_assoc prj1_dup lunit_agreement by fastforce
finally show ?thesis by blast
qed
qed
fix l
assume l: "?pr⇩1 (cod f) (cod g) ⋅ l = f ∧ ?pr⇩0 (cod f) (cod g) ⋅ l = g"
show "l = (f ⊗ g) ⋅ 𝖽[dom f]"
proof -
have 2: "«l : dom f → cod f ⊗ cod g»"
by (metis 1 arr_iff_in_hom cod_comp cod_tensor dom_comp fg l seqE)
have "l = ((?pr⇩1 (cod f) (cod g) ⊗ ?pr⇩0 (cod f) (cod g)) ⋅ 𝖽[cod f ⊗ cod g]) ⋅ l"
using fg 2 tuple_prj [of "cod f" "cod g"] lunit_agreement runit_agreement comp_cod_arr
by auto
also have "... = (?pr⇩1 (cod f) (cod g) ⊗ ?pr⇩0 (cod f) (cod g)) ⋅ 𝖽[cod f ⊗ cod g] ⋅ l"
using comp_assoc by simp
also have "... = ((?pr⇩1 (cod f) (cod g) ⊗ ?pr⇩0 (cod f) (cod g)) ⋅ (l ⊗ l)) ⋅ 𝖽[dom f]"
using 2 dup_naturality [of l] comp_assoc by auto
also have "... = (f ⊗ g) ⋅ 𝖽[dom f]"
using fg l interchange [of "?pr⇩1 (cod f) (cod g)" l "?pr⇩0 (cod f) (cod g)" l] by simp
finally show ?thesis by blast
qed
qed
qed
qed
lemma induces_elementary_category_with_binary_products⇩E⇩C⇩M⇩C:
shows "elementary_category_with_binary_products C
(λa b. 𝗅[b] ⋅ (𝗍[a] ⊗ b)) (λa b. 𝗋[a] ⋅ (a ⊗ 𝗍[b]))"
..
sublocale cartesian_monoidal_category C T α ι
proof
show "terminal MC.unity"
by (simp add: ℐ_agreement terminal_one)
show "⋀a b t⇩a t⇩b. ⟦ide a; ide b; «t⇩a : a → MC.unity»; «t⇩b : b → MC.unity»⟧ ⟹
has_as_binary_product a b
(MC.runit a ⋅ MC.tensor a t⇩b) (MC.lunit b ⋅ MC.tensor t⇩a b)"
by (metis ECBP.has_as_binary_product T_simp ℐ_agreement arrI ideD(1)
lunit_agreement runit_agreement trm_eqI)
qed
lemma induces_cartesian_monoidal_category⇩E⇩C⇩M⇩C:
shows "cartesian_monoidal_category C T α ι"
..
end
locale diagonal_functor =
C: category C +
CC: product_category C C
for C :: "'a comp"
begin
abbreviation map
where "map f ≡ if C.arr f then (f, f) else CC.null"
lemma is_functor:
shows "functor C CC.comp map"
using map_def by unfold_locales auto
sublocale "functor" C CC.comp map
using is_functor by simp
end
context cartesian_monoidal_category
begin
sublocale Δ: diagonal_functor C ..
interpretation ToΔ: composite_functor C CC.comp C Δ.map T ..
sublocale δ: natural_transformation C C map ‹T o Δ.map› dup
proof
show "⋀f. ¬ arr f ⟹ 𝖽[f] = null"
using ECC.tuple_ext by blast
show "⋀f. arr f ⟹ arr 𝖽[f]"
using dup_def by simp
show "⋀f. arr f ⟹ ToΔ.map f ⋅ 𝖽[dom f] = 𝖽[f]"
using ECC.tuple_expansion prod_eq_tensor by force
show "⋀f. arr f ⟹ 𝖽[cod f] ⋅ map f = 𝖽[f]"
by (simp add: comp_cod_arr dup_def)
qed
end
section "Cartesian Monoidal Category from Cartesian Category"
text ‹
A cartesian category extends to a cartesian monoidal category by using the product
structure to obtain the various canonical maps.
›
context elementary_cartesian_category
begin
interpretation CC: product_category C C ..
interpretation CCC: product_category C CC.comp ..
interpretation T: binary_functor C C C Prod
using binary_functor_Prod by simp
interpretation T: binary_endofunctor C Prod ..
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
interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
using α_naturalityisomorphism by blast
interpretation L: "functor" C C ‹λf. Prod (cod ι, f)›
using unit_is_terminal_arr T.fixing_ide_gives_functor_1 by simp
interpretation L: endofunctor C ‹λf. Prod (cod ι, f)› ..
interpretation 𝗅: transformation_by_components C C
‹λf. Prod (cod ι, f)› map ‹λa. pr0 (cod ι) a›
using unit_is_terminal_arr
by unfold_locales auto
interpretation 𝗅: natural_isomorphism C C ‹λf. Prod (cod ι, f)› map 𝗅.map
using 𝗅.map_simp_ide inverse_arrows_lunit ide_one
by unfold_locales auto
interpretation L: equivalence_functor C C ‹λf. Prod (cod ι, f)›
using 𝗅.natural_isomorphism_axioms naturally_isomorphic_def
L.isomorphic_to_identity_is_equivalence
by blast
interpretation R: "functor" C C ‹λf. Prod (f, cod ι)›
using unit_is_terminal_arr T.fixing_ide_gives_functor_2 by simp
interpretation R: endofunctor C‹λf. Prod (f, cod ι)› ..
interpretation ρ: transformation_by_components C C
‹λf. Prod (f, cod ι)› map ‹λa. 𝔭⇩1[a, cod ι]›
using unit_is_terminal_arr
by unfold_locales auto
interpretation ρ: natural_isomorphism C C ‹λf. Prod (f, cod ι)› map ρ.map
using ρ.map_simp_ide inverse_arrows_runit ide_one
by unfold_locales auto
interpretation R: equivalence_functor C C ‹λf. Prod (f, cod ι)›
using ρ.natural_isomorphism_axioms naturally_isomorphic_def
R.isomorphic_to_identity_is_equivalence
by blast
interpretation MC: monoidal_category C Prod α ι
using ide_one ι_is_iso pentagon comp_assoc α_simp_ide comp_cod_arr
by unfold_locales auto
lemma induces_monoidal_category⇩E⇩C⇩C:
shows "monoidal_category C Prod α ι"
..
lemma unity_agreement:
shows "MC.unity = 𝟭"
using ide_one by simp
lemma assoc_agreement:
assumes "ide a" and "ide b" and "ide c"
shows "MC.assoc a b c = 𝖺[a, b, c]"
using assms assoc_def α_simp_ide by auto
lemma assoc'_agreement:
assumes "ide a" and "ide b" and "ide c"
shows "MC.assoc' a b c = 𝖺⇧-⇧1[a, b, c]"
using assms inverse_arrows_assoc inverse_unique α_simp_ide by auto
lemma runit_char_eqn:
assumes "ide a"
shows "𝗋[a] ⊗ 𝟭 = (a ⊗ ι) ⋅ 𝖺[a, 𝟭, 𝟭]"
using assms ide_one assoc_def comp_assoc prod_tuple comp_cod_arr
by (intro pr_joint_monic [of a "𝟭" "𝗋[a] ⊗ 𝟭" "(a ⊗ ι) ⋅ 𝖺[a, 𝟭, 𝟭]"]) auto
lemma runit_agreement:
assumes "ide a"
shows "MC.runit a = 𝗋[a]"
using assms unity_agreement assoc_agreement MC.runit_char(2) runit_char_eqn ide_one
by (metis (no_types, lifting) MC.runit_eqI fst_conv runit_in_hom snd_conv)
lemma lunit_char_eqn:
assumes "ide a"
shows "𝟭 ⊗ 𝗅[a] = (ι ⊗ a) ⋅ 𝖺⇧-⇧1[𝟭, 𝟭, a]"
proof (intro pr_joint_monic [of "𝟭" a "𝟭 ⊗ 𝗅[a]" "(ι ⊗ a) ⋅ 𝖺⇧-⇧1[𝟭, 𝟭, a]"])
show "ide a" by fact
show "ide 𝟭"
using ide_one by simp
show "seq 𝗅[a] (𝟭 ⊗ 𝗅[a])"
using assms ide_one by simp
show "𝗅[a] ⋅ (𝟭 ⊗ 𝗅[a]) = 𝗅[a] ⋅ (ι ⊗ a) ⋅ 𝖺⇧-⇧1[𝟭, 𝟭, a]"
using assms ide_one assoc'_def comp_assoc prod_tuple comp_cod_arr by simp
show "𝔭⇩1[𝟭, a] ⋅ prod 𝟭 (lunit a) = 𝔭⇩1[𝟭, a] ⋅ prod ι a ⋅ assoc' 𝟭 𝟭 a"
using assms ide_one assoc'_def comp_cod_arr prod_tuple pr_naturality
apply simp
by (metis (full_types) cod_pr0 cod_pr1 elementary_category_with_binary_products.ide_prod
elementary_category_with_binary_products_axioms pr_simps(1-2,4-5) trm_naturality
trm_one)
qed
lemma lunit_agreement:
assumes "ide a"
shows "MC.lunit a = 𝗅[a]"
by (metis (no_types, lifting) MC.lunit_eqI assms assoc'_agreement fst_conv ide_one
lunit_char_eqn lunit_in_hom snd_conv unity_agreement)
interpretation CMC: cartesian_monoidal_category C Prod α ι
proof
show "terminal MC.unity"
by (simp add: terminal_one unity_agreement)
fix a b t⇩a t⇩b
assume a: "ide a" and b: "ide b"
and t⇩a: "«t⇩a : a → MC.unity»" and t⇩b: "«t⇩b : b → MC.unity»"
have 0: "𝔭⇩0[a, b] = MC.lunit b ⋅ MC.tensor 𝗍[a] b"
by (metis (no_types, lifting) a b ide_char cod_pr0 comp_cod_arr lunit_agreement
pr_naturality(1) pr_simps(1) prod.sel(1-2) trm_simps(1-3))
have 1: "𝔭⇩1[a, b] = MC.runit a ⋅ MC.tensor a 𝗍[b]"
by (metis (no_types, lifting) a b cod_pr1 comp_cod_arr ide_char pr_naturality(2)
pr_simps(4) prod.sel(1-2) runit_agreement trm_simps(1-3))
have 2: "𝗍[a] = t⇩a ∧ 𝗍[b] = t⇩b"
using a b t⇩a t⇩b terminal_arr_unique trm_eqI unity_agreement by metis
show "has_as_binary_product a b (MC.runit a ⋅ MC.tensor a t⇩b) (MC.lunit b ⋅ MC.tensor t⇩a b)"
using a b 0 1 2 has_as_binary_product by force
qed
lemma extends_to_cartesian_monoidal_category⇩E⇩C⇩C:
shows "cartesian_monoidal_category C Prod α ι"
..
lemma trm_agreement:
assumes "ide a"
shows "CMC.the_trm a = 𝗍[a]"
by (metis assms CMC.extends_to_elementary_category_with_terminal_object⇩C⇩M⇩C
elementary_category_with_terminal_object.trm_eqI trm_in_hom unity_agreement)
lemma pr_agreement:
assumes "ide a" and "ide b"
shows "CMC.pr⇩0 a b = 𝔭⇩0[a, b]" and "CMC.pr⇩1 a b = 𝔭⇩1[a, b]"
proof -
show "CMC.pr⇩0 a b = 𝔭⇩0[a, b]"
unfolding CMC.pr⇩0_def
using assms(1-2) lunit_agreement pr_expansion(1) trm_agreement by auto
show "CMC.pr⇩1 a b = 𝔭⇩1[a, b]"
unfolding CMC.pr⇩1_def
using assms(1-2) pr_expansion(2) runit_agreement trm_agreement by force
qed
lemma dup_agreement:
assumes "ide a"
shows "CMC.dup a = 𝖽[a]"
by (metis (no_types, lifting) CMC.ECC.tuple_eqI assms ideD(1) pr_agreement(1-2) pr_dup(1-2))
end
section "Cartesian Monoidal Category from Elementary Cartesian Category"
context elementary_cartesian_category
begin
interpretation MC: monoidal_category C Prod α ι
using induces_monoidal_category⇩E⇩C⇩C by blast
lemma triangle:
assumes "ide a" and "ide b"
shows "(a ⊗ 𝗅[b]) ⋅ 𝖺[a, 𝟭, b] = 𝗋[a] ⊗ b"
using assms MC.triangle [of a b] assoc_agreement ide_one lunit_agreement
runit_agreement unity_agreement fst_conv snd_conv
by (metis (no_types, lifting))
lemma induces_elementary_cartesian_monoidal_category⇩E⇩C⇩C:
shows "elementary_cartesian_monoidal_category (⋅) prod 𝟭 lunit runit assoc trm dup"
using ide_one inverse_arrows_lunit inverse_arrows_runit inverse_arrows_assoc
interchange lunit_naturality runit_naturality assoc_naturality
triangle pentagon comp_assoc trm_one trm_naturality
in_homI prod_tuple isoI arr_dom MC.tensor_in_homI comp_arr_dom comp_cod_arr
apply unfold_locales
apply simp_all
apply blast
apply blast
by meson
end
context cartesian_category
begin
interpretation ECC: elementary_cartesian_category C
some_pr0 some_pr1 some_terminal some_terminator
using extends_to_elementary_cartesian_category by simp
lemma extends_to_cartesian_monoidal_category⇩C⇩C:
shows "cartesian_monoidal_category C ECC.Prod ECC.α ECC.ι"
using ECC.extends_to_cartesian_monoidal_category⇩E⇩C⇩C by blast
end
end