Theory EnrichedCategoryBasics.CartesianClosedMonoidalCategory
section "Cartesian Closed Monoidal Categories"
text‹
A \emph{cartesian closed monoidal category} is a cartesian monoidal category that is a
closed monoidal category with respect to a chosen product. This is not quite the same
thing as a cartesian closed category, because a cartesian monoidal category
(being a monoidal category) has chosen structure (the tensor, associators, and unitors),
whereas we have defined a cartesian closed category to be an abstract category satisfying
certain properties that are expressed without assuming any chosen structure.
›
theory CartesianClosedMonoidalCategory
imports Category3.CartesianClosedCategory MonoidalCategory.CartesianMonoidalCategory
ClosedMonoidalCategory
begin
locale cartesian_closed_monoidal_category =
cartesian_monoidal_category +
closed_monoidal_category
locale elementary_cartesian_closed_monoidal_category =
cartesian_monoidal_category +
elementary_closed_monoidal_category
begin
lemmas prod_eq_tensor [simp]
end
text‹
The following is the main purpose for the current theory: to show that a
cartesian closed category with chosen structure determines a cartesian closed
monoidal category.
›
context elementary_cartesian_closed_category
begin
interpretation CMC: cartesian_monoidal_category C Prod α ι
using extends_to_cartesian_monoidal_category⇩E⇩C⇩C by blast
interpretation CMC: closed_monoidal_category C Prod α ι
using CMC.T.extensionality interchange left_adjoint_prod
by unfold_locales
(auto simp add: left_adjoint_functor.ex_terminal_arrow)
lemma extends_to_closed_monoidal_category⇩E⇩C⇩C⇩C:
shows "closed_monoidal_category C Prod α ι"
..
lemma extends_to_cartesian_closed_monoidal_category⇩E⇩C⇩C⇩C:
shows "cartesian_closed_monoidal_category C Prod α ι"
..
interpretation CMC: elementary_monoidal_category
C CMC.tensor CMC.unity CMC.lunit CMC.runit CMC.assoc
using CMC.induces_elementary_monoidal_category by blast
interpretation CMC: elementary_closed_monoidal_category
C Prod α ι exp eval curry
using eval_in_hom_ax curry_in_hom uncurry_curry_ax curry_uncurry_ax
by unfold_locales auto
lemma extends_to_elementary_closed_monoidal_category⇩E⇩C⇩C⇩C:
shows "elementary_closed_monoidal_category C Prod α ι exp eval curry"
..
lemma extends_to_elementary_cartesian_closed_monoidal_category⇩E⇩C⇩C⇩C:
shows "elementary_cartesian_closed_monoidal_category C Prod α ι exp eval curry"
..
end
context elementary_cartesian_closed_monoidal_category
begin
interpretation elementary_monoidal_category C tensor unity lunit runit assoc
using induces_elementary_monoidal_category by blast
text ‹
The following fact is not used in the present article, but it is a natural
and likely useful lemma for which I constructed a proof at one point.
The proof requires cartesianness; I suspect this is essential, but I am not
absolutely certain of it.
›
lemma isomorphic_exp_prod:
assumes "ide a" and "ide b" and "ide x"
shows "«⟨Curry[exp x (a ⊗ b), x, a] (𝔭⇩1[a, b] ⋅ eval x (a ⊗ b)),
Curry[exp x (a ⊗ b), x, b] (𝔭⇩0[a, b] ⋅ eval x (a ⊗ b))⟩
: exp x (a ⊗ b) → exp x a ⊗ exp x b»"
(is "«⟨?C, ?D⟩ : exp x (a ⊗ b) → exp x a ⊗ exp x b»")
and "«Curry[exp x a ⊗ exp x b, x, a ⊗ b]
⟨eval x a ⋅ ⟨𝔭⇩1[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩,
eval x b ⋅ ⟨𝔭⇩0[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩⟩
: exp x a ⊗ exp x b → exp x (a ⊗ b)»"
(is "«Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩
: exp x a ⊗ exp x b → exp x (a ⊗ b)»")
and "inverse_arrows
(Curry[exp x a ⊗ exp x b, x, a ⊗ b]
⟨eval x a ⋅ ⟨𝔭⇩1[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩,
eval x b ⋅ ⟨𝔭⇩0[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩⟩)
⟨Curry[exp x (a ⊗ b), x, a] (𝔭⇩1[a, b] ⋅ eval x (a ⊗ b)),
Curry[exp x (a ⊗ b), x, b] (𝔭⇩0[a, b] ⋅ eval x (a ⊗ b))⟩"
and "isomorphic (exp x (a ⊗ b)) (exp x a ⊗ exp x b)"
proof -
have A: "«?A : (exp x a ⊗ exp x b) ⊗ x → a»"
using assms by auto
have B: "«?B : (exp x a ⊗ exp x b) ⊗ x → b»"
using assms by auto
have AB: "«⟨?A, ?B⟩ : (exp x a ⊗ exp x b) ⊗ x → a ⊗ b»"
by (metis A B ECC.tuple_in_hom prod_eq_tensor)
have C: "«?C : exp x (a ⊗ b) → exp x a»"
using assms by auto
have D: "«?D : exp x (a ⊗ b) → exp x b»"
using assms by auto
show CD: "«⟨?C, ?D⟩ : exp x (a ⊗ b) → exp x a ⊗ exp x b»"
using C D by fastforce
show 1: "«Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩
: (exp x a ⊗ exp x b) → exp x (a ⊗ b)»"
by (simp add: AB assms(1-3) Curry_in_hom)
show "inverse_arrows (Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩) ⟨?C, ?D⟩"
proof
show "ide (Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⋅ ⟨?C, ?D⟩)"
proof -
have "Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⋅ ⟨?C, ?D⟩ =
Curry[exp x (a ⊗ b), x, a ⊗ b] (⟨?A, ?B⟩ ⋅ (⟨?C, ?D⟩ ⊗ x))"
using assms AB CD comp_Curry_arr by presburger
also have "... = Curry[exp x (a ⊗ b), x, a ⊗ b]
⟨?A ⋅ (⟨?C, ?D⟩ ⊗ x), ?B ⋅ (⟨?C, ?D⟩ ⊗ x)⟩"
proof -
have "span ?A ?B"
using A B by fastforce
moreover have "arr (⟨?C, ?D⟩ ⊗ x)"
using assms CD by auto
moreover have "dom ?A = cod (⟨?C, ?D⟩ ⊗ x)"
by (metis A CD assms(3) cod_tensor ide_char in_homE)
ultimately show ?thesis
using assms ECC.comp_tuple_arr by metis
qed
also have "... = Curry[exp x (a ⊗ b), x, a ⊗ b]
⟨Uncurry[x, a] ?C, eval x b ⋅ (?D ⊗ x)⟩"
proof -
have "?A ⋅ (⟨?C, ?D⟩ ⊗ x) = Uncurry[x, a] ?C"
proof -
have "?A ⋅ (⟨?C, ?D⟩ ⊗ x) =
eval x a ⋅
⟨𝔭⇩1[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x] ⋅ (⟨?C, ?D⟩ ⊗ x),
𝔭⇩0[exp x a ⊗ exp x b, x] ⋅ (⟨?C, ?D⟩ ⊗ x)⟩"
using assms ECC.comp_tuple_arr comp_assoc by simp
also have "... = eval x a ⋅
⟨?C ⋅ 𝔭⇩1[exp x (a ⊗ b), x], x ⋅ 𝔭⇩0[exp x (a ⊗ b), x]⟩"
using assms ECC.pr_naturality(1-2) by auto
also have "... = eval x a ⋅ (?C ⊗ x) ⋅
⟨𝔭⇩1[exp x (a ⊗ b), x], 𝔭⇩0[exp x (a ⊗ b), x]⟩"
using assms
ECC.prod_tuple
[of "𝔭⇩1[exp x (a ⊗ b), x]" "𝔭⇩0[exp x (a ⊗ b), x]" ?C x]
by simp
also have "... = Uncurry[x, a] ?C"
using assms C ECC.tuple_pr comp_arr_ide comp_arr_dom by auto
finally show ?thesis by blast
qed
moreover have "?B ⋅ (⟨?C, ?D⟩ ⊗ x) = Uncurry[x, b] ?D"
proof -
have "?B ⋅ (⟨?C, ?D⟩ ⊗ x) =
eval x b ⋅
⟨𝔭⇩0[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x] ⋅ (⟨?C, ?D⟩ ⊗ x),
𝔭⇩0[exp x a ⊗ exp x b, x] ⋅ (⟨?C, ?D⟩ ⊗ x)⟩"
using assms ECC.comp_tuple_arr comp_assoc by simp
also have "... = eval x b ⋅
⟨?D ⋅ 𝔭⇩1[exp x (a ⊗ b), x], x ⋅ 𝔭⇩0[exp x (a ⊗ b), x]⟩"
using assms C ECC.pr_naturality(1-2) by auto
also have "... = eval x b ⋅ (?D ⊗ x) ⋅
⟨𝔭⇩1[exp x (a ⊗ b), x], 𝔭⇩0[exp x (a ⊗ b), x]⟩"
using assms
ECC.prod_tuple
[of "𝔭⇩1[exp x (a ⊗ b), x]" "𝔭⇩0[exp x (a ⊗ b), x]" ?D x]
by simp
also have "... = Uncurry[x, b] ?D"
using assms C ECC.tuple_pr comp_arr_ide comp_arr_dom by auto
finally show ?thesis by blast
qed
ultimately show ?thesis by simp
qed
also have "... = Curry[exp x (a ⊗ b), x, a ⊗ b]
(⟨𝔭⇩1[a, b] ⋅ eval x (a ⊗ b), 𝔭⇩0[a, b] ⋅ eval x (a ⊗ b)⟩)"
using assms Uncurry_Curry by auto
also have "... = Curry[exp x (a ⊗ b), x, a ⊗ b]
(⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ ⋅ eval x (a ⊗ b))"
using assms ECC.comp_tuple_arr [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]" "eval x (a ⊗ b)"]
by simp
also have "... = Curry[exp x (a ⊗ b), x, a ⊗ b] (eval x (a ⊗ b))"
using assms comp_cod_arr by simp
also have "... = exp x (a ⊗ b)"
using assms Curry_Uncurry ide_exp ide_in_hom tensor_preserves_ide
Uncurry_exp
by metis
finally have "Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⋅ ⟨?C, ?D⟩ =
exp x (a ⊗ b)"
by blast
thus ?thesis
using assms ide_exp tensor_preserves_ide by presburger
qed
show "ide (⟨?C, ?D⟩ ⋅ Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩)"
proof -
have 2: "span 𝔭⇩1[exp x a ⊗ exp x b, x] 𝔭⇩0[exp x a ⊗ exp x b, x]"
using assms by simp
have 3: "seq x 𝔭⇩0[exp x a ⊗ exp x b, x]"
using assms by simp
have "⟨?C, ?D⟩ ⋅ Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
⟨?C ⋅ Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩,
?D ⋅ Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩⟩"
using assms C D 1 ECC.comp_tuple_arr by (metis in_homE)
also have "... = ⟨𝔭⇩1[exp x a, exp x b], 𝔭⇩0[exp x a, exp x b]⟩"
proof -
have "Curry[exp x (a ⊗ b), x, a] (𝔭⇩1[a, b] ⋅ eval x (a ⊗ b)) ⋅
Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
𝔭⇩1[exp x a, exp x b]"
proof -
have "Curry[exp x (a ⊗ b), x, a] (𝔭⇩1[a, b] ⋅ eval x (a ⊗ b)) ⋅
Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
Curry[exp x a ⊗ exp x b, x, a]
((𝔭⇩1[a, b] ⋅ eval x (a ⊗ b)) ⋅
(Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⊗ x))"
using assms 1 comp_Curry_arr by auto
also have "... = Curry[exp x a ⊗ exp x b, x, a]
(𝔭⇩1[a, b] ⋅ eval x (a ⊗ b) ⋅
(Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⊗ x))"
using comp_assoc by simp
also have "... = Curry[exp x a ⊗ exp x b, x, a] (𝔭⇩1[a, b] ⋅ ⟨?A, ?B⟩)"
using assms AB Uncurry_Curry ide_exp tensor_preserves_ide by simp
also have "... = Curry[exp x a ⊗ exp x b, x, a]
(eval x a ⋅
⟨𝔭⇩1[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩)"
using assms A B ECC.pr_tuple(1) by fastforce
also have "... = Curry[exp x a ⊗ exp x b, x, a]
(eval x a ⋅ (𝔭⇩1[exp x a, exp x b] ⊗ x) ⋅
⟨𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩)"
proof -
have "seq 𝔭⇩1[exp x a, exp x b] 𝔭⇩1[exp x a ⊗ exp x b, x]"
using assms by auto
thus ?thesis
using assms 2 3 prod_eq_tensor comp_ide_arr ECC.prod_tuple
by metis
qed
also have "... = Curry (exp x a ⊗ exp x b) x a
(eval x a ⋅ (𝔭⇩1[exp x a, exp x b] ⊗ x))"
using assms comp_arr_dom by simp
also have "... = 𝔭⇩1[exp x a, exp x b]"
using assms Curry_Uncurry by simp
finally show ?thesis by blast
qed
moreover have "Curry[exp x (a ⊗ b), x, b] (𝔭⇩0[a, b] ⋅ eval x (a ⊗ b)) ⋅
Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
𝔭⇩0[exp x a, exp x b]"
proof -
have "Curry[exp x (a ⊗ b), x, b] (𝔭⇩0[a, b] ⋅ eval x (a ⊗ b)) ⋅
Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
Curry[exp x a ⊗ exp x b, x, b]
((𝔭⇩0[a, b] ⋅ eval x (a ⊗ b)) ⋅
(Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ ⊗ x))"
proof -
have "«Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩
: exp x a ⊗ exp x b → exp x (a ⊗ b)»"
using 1 by blast
moreover have "«𝔭⇩0[a, b] ⋅ eval x (a ⊗ b) : exp x (a ⊗ b) ⊗ x → b»"
using assms
by (metis (no_types, lifting) ECC.pr0_in_hom' ECC.pr_simps(2)
comp_in_homI eval_in_hom⇩E⇩C⇩M⇩C prod_eq_tensor tensor_preserves_ide)
ultimately show ?thesis
using assms comp_Curry_arr by simp
qed
also have "... = Curry[exp x a ⊗ exp x b, x, b]
(𝔭⇩0[a, b] ⋅
Uncurry[x, a ⊗ b]
(Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩))"
using comp_assoc by simp
also have "... = Curry (exp x a ⊗ exp x b) x b (𝔭⇩0[a, b] ⋅ ⟨?A, ?B⟩)"
using assms AB Uncurry_Curry ide_exp tensor_preserves_ide by simp
also have "... = Curry[exp x a ⊗ exp x b, x, b]
(eval x b ⋅
⟨𝔭⇩0[exp x a, exp x b] ⋅ 𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩)"
using assms A B by fastforce
also have "... = Curry[exp x a ⊗ exp x b, x, b]
(eval x b ⋅ (𝔭⇩0[exp x a, exp x b] ⊗ x) ⋅
⟨𝔭⇩1[exp x a ⊗ exp x b, x],
𝔭⇩0[exp x a ⊗ exp x b, x]⟩)"
proof -
have "seq 𝔭⇩0[exp x a, exp x b] 𝔭⇩1[exp x a ⊗ exp x b, x]"
using assms by auto
thus ?thesis
using assms 2 3 prod_eq_tensor comp_ide_arr ECC.prod_tuple
by metis
qed
also have "... = Curry (exp x a ⊗ exp x b) x b
(Uncurry[x, b] 𝔭⇩0[exp x a, exp x b])"
proof -
have "(𝔭⇩0[exp x a, exp x b] ⊗ x) ⋅
⟨𝔭⇩1[exp x a ⊗ exp x b, x], 𝔭⇩0[exp x a ⊗ exp x b, x]⟩ =
𝔭⇩0[exp x a, exp x b] ⊗ x"
using assms comp_arr_ide ECC.tuple_pr by auto
thus ?thesis by simp
qed
also have "... = 𝔭⇩0[exp x a, exp x b]"
using assms Curry_Uncurry by simp
finally show ?thesis by blast
qed
ultimately show ?thesis by simp
qed
also have "... = exp x a ⊗ exp x b"
using assms ECC.tuple_pr by simp
finally have "⟨?C, ?D⟩ ⋅ Curry[exp x a ⊗ exp x b, x, a ⊗ b] ⟨?A, ?B⟩ =
exp x a ⊗ exp x b"
by blast
thus ?thesis
using assms tensor_preserves_ide by simp
qed
qed
thus "isomorphic (exp x (a ⊗ b)) (exp x a ⊗ exp x b)"
unfolding isomorphic_def
using CD by blast
qed
end
end