# Theory CZH_ECAT_PCategory

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Product category›
theory CZH_ECAT_PCategory
imports
CZH_ECAT_NTCF
CZH_ECAT_Small_Category
CZH_Foundations.CZH_SMC_PSemicategory
begin

subsection‹Background›

text‹See Chapter II-3 in \<^cite>‹"mac_lane_categories_2010"›.›

named_theorems cat_prod_cs_simps
named_theorems cat_prod_cs_intros

subsection‹Product category: definition and elementary properties›

definition cat_prod :: "V ⇒ (V ⇒ V) ⇒ V"
where "cat_prod I 𝔄 =
[
(∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈),
(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈),
(λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). (λi∈⇩∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈)),
(λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). (λi∈⇩∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈)),
(
λgf∈⇩∘composable_arrs (dg_prod I 𝔄).
(λi∈⇩∘I. vpfst gf⦇i⦈ ∘⇩A⇘𝔄 i⇙ vpsnd gf⦇i⦈)
),
(λa∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈). (λi∈⇩∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈))
]⇩∘"

syntax "_PCATEGORY" :: "pttrn ⇒ V ⇒ (V ⇒ V) ⇒ V"
("(3∏⇩C_∈⇩∘_./ _)" [0, 0, 10] 10)
translations "∏⇩Ci∈⇩∘I. 𝔄" ⇌ "CONST cat_prod I (λi. 𝔄)"

text‹Components.›

lemma cat_prod_components:
shows "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈ = (∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈)"
and "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈ = (∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈)"
and "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇Dom⦈ =
(λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). (λi∈⇩∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈))"
and "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇Cod⦈ =
(λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). (λi∈⇩∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈))"
and "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇Comp⦈ =
(
λgf∈⇩∘composable_arrs (dg_prod I 𝔄).
(λi∈⇩∘I. vpfst gf⦇i⦈ ∘⇩A⇘𝔄 i⇙ vpsnd gf⦇i⦈)
)"
and "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈ =
(λa∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈). (λi∈⇩∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈))"
unfolding cat_prod_def dg_field_simps by (simp_all add: nat_omega_simps)

text‹Slicing.›

lemma cat_smc_cat_prod[slicing_commute]:
"smc_prod I (λi. cat_smc (𝔄 i)) = cat_smc (∏⇩Ci∈⇩∘I. 𝔄 i)"
unfolding dg_prod_def cat_smc_def cat_prod_def smc_prod_def dg_field_simps

context
fixes 𝔄 φ :: "V ⇒ V"
and ℭ :: V
begin

lemmas_with [
where 𝔄=‹λi. cat_smc (𝔄 i)›, unfolded slicing_simps slicing_commute
]:
cat_prod_ObjI = smc_prod_ObjI
and cat_prod_ObjD = smc_prod_ObjD
and cat_prod_ObjE = smc_prod_ObjE
and cat_prod_Obj_cong = smc_prod_Obj_cong
and cat_prod_ArrI = smc_prod_ArrI
and cat_prod_ArrD = smc_prod_ArrD
and cat_prod_ArrE = smc_prod_ArrE
and cat_prod_Arr_cong = smc_prod_Arr_cong
and cat_prod_Dom_vsv[cat_cs_intros] = smc_prod_Dom_vsv
and cat_prod_Dom_vdomain[cat_cs_simps] = smc_prod_Dom_vdomain
and cat_prod_Dom_app = smc_prod_Dom_app
and cat_prod_Dom_app_component_app[cat_cs_simps] =
smc_prod_Dom_app_component_app
and cat_prod_Cod_vsv[cat_cs_intros] = smc_prod_Cod_vsv
and cat_prod_Cod_app = smc_prod_Cod_app
and cat_prod_Cod_vdomain[cat_cs_simps] = smc_prod_Cod_vdomain
and cat_prod_Cod_app_component_app[cat_cs_simps] =
smc_prod_Cod_app_component_app
and cat_prod_Comp = smc_prod_Comp
and cat_prod_Comp_vdomain[cat_cs_simps] = smc_prod_Comp_vdomain
and cat_prod_Comp_app = smc_prod_Comp_app
and cat_prod_Comp_app_component[cat_cs_simps] =
smc_prod_Comp_app_component
and cat_prod_Comp_app_vdomain = smc_prod_Comp_app_vdomain
and cat_prod_vunion_Obj_in_Obj = smc_prod_vunion_Obj_in_Obj
and cat_prod_vdiff_vunion_Obj_in_Obj = smc_prod_vdiff_vunion_Obj_in_Obj
and cat_prod_vunion_Arr_in_Arr = smc_prod_vunion_Arr_in_Arr
and cat_prod_vdiff_vunion_Arr_in_Arr = smc_prod_vdiff_vunion_Arr_in_Arr

end

subsection‹Local assumptions for a product category›

locale pcategory_base = 𝒵 α for α I 𝔄 +
assumes pcat_categories: "i ∈⇩∘ I ⟹ category α (𝔄 i)"
and pcat_index_in_Vset[cat_cs_intros]: "I ∈⇩∘ Vset α"

lemma (in pcategory_base) pcat_categories'[cat_prod_cs_intros]:
assumes "i ∈⇩∘ I" and "α' = α"
shows "category α' (𝔄 i)"
using assms(1) unfolding assms(2) by (rule pcat_categories)

text‹Rules.›

lemma (in pcategory_base) pcategory_base_axioms'[cat_prod_cs_intros]:
assumes "α' = α" and "I' = I"
shows "pcategory_base α' I' 𝔄"
unfolding assms by (rule pcategory_base_axioms)

mk_ide rf pcategory_base_def[unfolded pcategory_base_axioms_def]
|intro pcategory_baseI|
|dest pcategory_baseD[dest]|
|elim pcategory_baseE[elim]|

lemma pcategory_base_psemicategory_baseI:
assumes "psemicategory_base α I (λi. cat_smc (𝔄 i))"
and "⋀i. i ∈⇩∘ I ⟹ category α (𝔄 i)"
shows "pcategory_base α I 𝔄"
proof-
interpret psemicategory_base α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
show ?thesis
by (intro pcategory_baseI)
(auto simp: assms(2) psmc_index_in_Vset psmc_Obj_in_Vset psmc_Arr_in_Vset)
qed

text‹Product category is a product semicategory.›

context pcategory_base
begin

lemma pcat_psemicategory_base: "psemicategory_base α I (λi. cat_smc (𝔄 i))"
proof(intro psemicategory_baseI)
from pcat_index_in_Vset show "I ∈⇩∘ Vset α" by auto
qed (auto simp: category.cat_semicategory cat_prod_cs_intros)

interpretation psmc: psemicategory_base α I ‹λi. cat_smc (𝔄 i)›
by (rule pcat_psemicategory_base)

lemmas_with [unfolded slicing_simps slicing_commute]:
pcat_Obj_in_Vset = psmc.psmc_Obj_in_Vset
and pcat_Arr_in_Vset = psmc.psmc_Arr_in_Vset
and pcat_smc_prod_Obj_in_Vset = psmc.psmc_smc_prod_Obj_in_Vset
and pcat_smc_prod_Arr_in_Vset = psmc.psmc_smc_prod_Arr_in_Vset
and cat_prod_Dom_app_in_Obj[cat_cs_intros] = psmc.smc_prod_Dom_app_in_Obj
and cat_prod_Cod_app_in_Obj[cat_cs_intros] = psmc.smc_prod_Cod_app_in_Obj
and cat_prod_is_arrI = psmc.smc_prod_is_arrI
and cat_prod_is_arrD[dest] = psmc.smc_prod_is_arrD
and cat_prod_is_arrE[elim] = psmc.smc_prod_is_arrE

end

lemma cat_prod_dg_prod_is_arr:
"g : b ↦⇘dg_prod I 𝔄⇙ c ⟷ g : b ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ c"
unfolding is_arr_def cat_prod_def smc_prod_def dg_prod_def dg_field_simps

lemma smc_prod_composable_arrs_dg_prod:
"composable_arrs (dg_prod I 𝔄) = composable_arrs (∏⇩Ci∈⇩∘I. 𝔄 i)"
unfolding composable_arrs_def cat_prod_dg_prod_is_arr by simp

text‹Elementary properties.›

lemma (in pcategory_base) pcat_vsubset_index_pcategory_base:
assumes "J ⊆⇩∘ I"
shows "pcategory_base α J 𝔄"
proof(intro pcategory_baseI)
show "category α (𝔄 i)" if "i ∈⇩∘ J" for i
using that assms by (auto intro: cat_prod_cs_intros)
from assms show "J ∈⇩∘ Vset α" by (simp add: vsubset_in_VsetI cat_cs_intros)
qed auto

subsubsection‹Identity›

lemma cat_prod_CId_vsv[cat_cs_intros]: "vsv ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈)"
unfolding cat_prod_components by auto

lemma cat_prod_CId_vdomain[cat_cs_simps]:
"𝒟⇩∘ ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈) = (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈"
unfolding cat_prod_components by simp

lemma cat_prod_CId_app:
assumes "a ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈"
shows "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇a⦈ = (λi∈⇩∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈)"
using assms unfolding cat_prod_components by simp

lemma cat_prod_CId_app_component[cat_cs_simps]:
assumes "a ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈" and "i ∈⇩∘ I"
shows "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇a⦈⦇i⦈ = 𝔄 i⦇CId⦈⦇a⦇i⦈⦈"
using assms unfolding cat_prod_components by simp

lemma (in pcategory_base) cat_prod_CId_vrange:
"ℛ⇩∘ ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈) ⊆⇩∘ (∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈)"
proof(intro vsubsetI)
interpret CId: vsv ‹((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈)› by (rule cat_prod_CId_vsv)
fix f assume "f ∈⇩∘ ℛ⇩∘ ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈)"
then obtain a where f_def: "f = ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈)⦇a⦈"
and "a ∈⇩∘ 𝒟⇩∘ ((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈)"
by (blast dest: CId.vrange_atD)
then have a: "a ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈"
unfolding cat_prod_components by simp
show "f ∈⇩∘ (∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈)"
unfolding f_def cat_prod_CId_app[OF a]
proof(rule VLambda_in_vproduct)
fix i assume prems: "i ∈⇩∘ I"
interpret 𝔄: category α ‹𝔄 i›
by (simp add: ‹i ∈⇩∘ I› cat_cs_intros cat_prod_cs_intros)
from prems a have "a⦇i⦈ ∈⇩∘ 𝔄 i⦇Obj⦈" unfolding cat_prod_components by auto
with is_arrD(1) show "𝔄 i⦇CId⦈⦇a⦇i⦈⦈ ∈⇩∘ 𝔄 i⦇Arr⦈"
by (auto intro: cat_cs_intros)
qed
qed

subsubsection‹A product ‹α›-category is a tiny ‹β›-category›

lemma (in pcategory_base) pcat_tiny_category_cat_prod:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "tiny_category β (∏⇩Ci∈⇩∘I. 𝔄 i)"
proof-

interpret β: 𝒵 β by (rule assms(1))

show ?thesis
proof(intro tiny_categoryI, (unfold slicing_simps)?)

show Π: "tiny_semicategory β (cat_smc (∏⇩Ci∈⇩∘I. 𝔄 i))"
unfolding slicing_commute[symmetric]
by
(
intro psemicategory_base.psmc_tiny_semicategory_smc_prod;
(rule assms pcat_psemicategory_base)?
)
interpret Π: tiny_semicategory β ‹cat_smc (∏⇩Ci∈⇩∘I. 𝔄 i)› by (rule Π)

show "vfsequence (∏⇩Ci∈⇩∘I. 𝔄 i)" unfolding cat_prod_def by auto
show "vcard (∏⇩Ci∈⇩∘I. 𝔄 i) = 6⇩ℕ"
unfolding cat_prod_def by (simp add: nat_omega_simps)

show CId: "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇a⦈ : a ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ a"
if a: "a ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈" for a
proof(rule cat_prod_is_arrI)
have [cat_cs_intros]: "a⦇i⦈ ∈⇩∘ 𝔄 i⦇Obj⦈" if i: "i ∈⇩∘ I" for i
by (rule cat_prod_ObjD(3)[OF a i])
from that show "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇a⦈⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ a⦇i⦈"
if "i ∈⇩∘ I" for i
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_prod_cs_intros that
)
qed (use that in ‹auto simp: cat_prod_components cat_prod_CId_app that›)

show "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ f = f"
if "f : a ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ b" for f a b
proof(rule cat_prod_Arr_cong)
note f = Π.smc_is_arrD[unfolded slicing_simps, OF that]
note a = f(2) and b = f(3) and f = f(1)
from CId[OF b] have CId_b:
"(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ : b ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ b"
by simp
from Π.smc_Comp_is_arr[unfolded slicing_simps, OF this that] show
"(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ f ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
from that show "f ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈" by auto
fix i assume prems: "i ∈⇩∘ I"
interpret 𝔄i: category α ‹𝔄 i› by (simp add: prems cat_prod_cs_intros)
from prems cat_prod_is_arrD(7)[OF that] have fi:
"f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
by auto
from prems show "((∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ f)⦇i⦈ = f⦇i⦈"
unfolding cat_prod_Comp_app_component[OF CId_b that prems]
unfolding cat_prod_CId_app[OF b]
by (auto intro: 𝔄i.cat_CId_left_left[OF fi])
qed

show "f ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ = f"
if "f : b ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ c" for f b c
proof(rule cat_prod_Arr_cong)
note f = Π.smc_is_arrD[unfolded slicing_simps, OF that]
note b = f(2) and c = f(3) and f = f(1)
from CId[OF b] have CId_b:
"(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ : b ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ b"
by simp
from Π.smc_Comp_is_arr[unfolded slicing_simps, OF that this] show
"f ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
from that show "f ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈" by auto
fix i assume prems: "i ∈⇩∘ I"
interpret 𝔄i: category α ‹𝔄 i› by (simp add: prems cat_prod_cs_intros)
from prems cat_prod_is_arrD[OF that] have fi: "f⦇i⦈ : b⦇i⦈ ↦⇘𝔄 i⇙ c⦇i⦈"
by simp
from prems show "(f ∘⇩A⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇b⦈)⦇i⦈ = f⦇i⦈"
unfolding cat_prod_Comp_app_component[OF that CId_b prems]
unfolding cat_prod_CId_app[OF b]
by (auto intro: 𝔄i.cat_CId_right_left[OF fi])
qed

qed (auto simp: cat_cs_intros cat_cs_simps intro: cat_cs_intros)

qed

subsection‹Further local assumptions for product categories›

subsubsection‹Definition and elementary properties›

locale pcategory = pcategory_base α I 𝔄 for α I 𝔄 +
assumes pcat_Obj_vsubset_Vset: "J ⊆⇩∘ I ⟹ (∏⇩Ci∈⇩∘J. 𝔄 i)⦇Obj⦈ ⊆⇩∘ Vset α"
and pcat_Hom_vifunion_in_Vset:
"⟦
J ⊆⇩∘ I;
A ⊆⇩∘ (∏⇩Ci∈⇩∘J. 𝔄 i)⦇Obj⦈;
B ⊆⇩∘ (∏⇩Ci∈⇩∘J. 𝔄 i)⦇Obj⦈;
A ∈⇩∘ Vset α;
B ∈⇩∘ Vset α
⟧ ⟹ (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (∏⇩Ci∈⇩∘J. 𝔄 i) a b) ∈⇩∘ Vset α"

text‹Rules.›

lemma (in pcategory) pcategory_axioms'[cat_prod_cs_intros]:
assumes "α' = α" and "I' = I"
shows "pcategory α' I' 𝔄"
unfolding assms by (rule pcategory_axioms)

mk_ide rf pcategory_def[unfolded pcategory_axioms_def]
|intro pcategoryI|
|dest pcategoryD[dest]|
|elim pcategoryE[elim]|

lemmas [cat_prod_cs_intros] = pcategoryD(1)

lemma pcategory_psemicategoryI:
assumes "psemicategory α I (λi. cat_smc (𝔄 i))"
and "⋀i. i ∈⇩∘ I ⟹ category α (𝔄 i)"
shows "pcategory α I 𝔄"
proof-
interpret psemicategory α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
note [unfolded slicing_simps slicing_commute, cat_cs_intros] =
psmc_Obj_vsubset_Vset
psmc_Hom_vifunion_in_Vset
show ?thesis
by (intro pcategoryI pcategory_base_psemicategory_baseI)
(auto simp: assms(2) smc_prod_cs_intros intro!: cat_cs_intros)
qed

text‹Product category is a product semicategory.›

context pcategory
begin

lemma pcat_psemicategory: "psemicategory α I (λi. cat_smc (𝔄 i))"
proof(intro psemicategoryI, unfold slicing_simps slicing_commute)
show "psemicategory_base α I (λi. cat_smc (𝔄 i))"
by (rule pcat_psemicategory_base)
qed (auto intro!: pcat_Obj_vsubset_Vset pcat_Hom_vifunion_in_Vset)

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)›
by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
pcat_Obj_vsubset_Vset' = psmc.psmc_Obj_vsubset_Vset'
and pcat_Hom_vifunion_in_Vset' = psmc.psmc_Hom_vifunion_in_Vset'
and pcat_cat_prod_vunion_is_arr = psmc.psmc_smc_prod_vunion_is_arr
and pcat_cat_prod_vdiff_vunion_is_arr = psmc.psmc_smc_prod_vdiff_vunion_is_arr

lemmas_with [unfolded slicing_simps slicing_commute]:
pcat_cat_prod_vunion_Comp = psmc.psmc_smc_prod_vunion_Comp
and pcat_cat_prod_vdiff_vunion_Comp = psmc.psmc_smc_prod_vdiff_vunion_Comp

end

text‹Elementary properties.›

lemma (in pcategory) pcat_vsubset_index_pcategory:
assumes "J ⊆⇩∘ I"
shows "pcategory α J 𝔄"
proof(intro pcategoryI pcategory_psemicategoryI)
show "cat_prod J' 𝔄⦇Obj⦈ ⊆⇩∘ Vset α" if ‹J' ⊆⇩∘ J› for J'
proof-
from that assms have "J' ⊆⇩∘ I" by simp
then show "cat_prod J' 𝔄⦇Obj⦈ ⊆⇩∘ Vset α" by (rule pcat_Obj_vsubset_Vset)
qed
fix A B J' assume prems:
"J' ⊆⇩∘ J"
"A ⊆⇩∘ (∏⇩Ci∈⇩∘J'. 𝔄 i)⦇Obj⦈"
"B ⊆⇩∘ (∏⇩Ci∈⇩∘J'. 𝔄 i)⦇Obj⦈"
"A ∈⇩∘ Vset α"
"B ∈⇩∘ Vset α"
show "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (∏⇩Ci∈⇩∘J'. 𝔄 i) a b) ∈⇩∘ Vset α"
proof-
from prems(1) assms have "J' ⊆⇩∘ I" by simp
from pcat_Hom_vifunion_in_Vset[OF this prems(2-5)] show ?thesis.
qed

qed (rule pcat_vsubset_index_pcategory_base[OF assms])

subsubsection‹A product ‹α›-category is an ‹α›-category›

lemma (in pcategory) pcat_category_cat_prod: "category α (∏⇩Ci∈⇩∘I. 𝔄 i)"
proof-
interpret tiny_category ‹α + ω› ‹∏⇩Ci∈⇩∘I. 𝔄 i›
by (intro pcat_tiny_category_cat_prod)
(auto simp: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω)
show ?thesis
by (rule category_if_category)
(
auto
intro!: pcat_Hom_vifunion_in_Vset pcat_Obj_vsubset_Vset
intro: cat_cs_intros
)
qed

subsection‹Local assumptions for a finite product category›

subsubsection‹Definition and elementary properties›

locale finite_pcategory = pcategory_base α I 𝔄 for α I 𝔄 +
assumes fin_pcat_index_vfinite: "vfinite I"

text‹Rules.›

lemma (in finite_pcategory) finite_pcategory_axioms[cat_prod_cs_intros]:
assumes "α' = α" and "I' = I"
shows "finite_pcategory α' I' 𝔄"
unfolding assms by (rule finite_pcategory_axioms)

mk_ide rf finite_pcategory_def[unfolded finite_pcategory_axioms_def]
|intro finite_pcategoryI|
|dest finite_pcategoryD[dest]|
|elim finite_pcategoryE[elim]|

lemmas [cat_prod_cs_intros] = finite_pcategoryD(1)

lemma finite_pcategory_finite_psemicategoryI:
assumes "finite_psemicategory α I (λi. cat_smc (𝔄 i))"
and "⋀i. i ∈⇩∘ I ⟹ category α (𝔄 i)"
shows "finite_pcategory α I 𝔄"
proof-
interpret finite_psemicategory α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
show ?thesis
by
(
intro
assms
finite_pcategoryI
pcategory_base_psemicategory_baseI
finite_psemicategoryD(1)[OF assms(1)]
fin_psmc_index_vfinite
)
qed

subsubsection‹
Local assumptions for a finite product semicategory and local
assumptions for an arbitrary product semicategory
›

sublocale finite_pcategory ⊆ pcategory α I 𝔄
proof-
interpret finite_psemicategory α I ‹λi. cat_smc (𝔄 i)›
proof(intro finite_psemicategoryI psemicategory_baseI)
fix i assume "i ∈⇩∘ I"
then interpret 𝔄i: category α ‹𝔄 i› by (simp add: pcat_categories)
show "semicategory α (cat_smc (𝔄 i))" by (simp add: 𝔄i.cat_semicategory)
qed (auto intro!: cat_cs_intros fin_pcat_index_vfinite)
show "pcategory α I 𝔄"
by (intro pcategory_psemicategoryI)
qed

subsection‹Binary union and complement›

lemma (in pcategory) pcat_cat_prod_vunion_CId:
assumes "vdisjnt J K"
and "J ⊆⇩∘ I"
and "K ⊆⇩∘ I"
and "a ∈⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇Obj⦈"
and "b ∈⇩∘ (∏⇩Cj∈⇩∘K. 𝔄 j)⦇Obj⦈"
shows
"(∏⇩Cj∈⇩∘J. 𝔄 j)⦇CId⦈⦇a⦈ ∪⇩∘ (∏⇩Cj∈⇩∘K. 𝔄 j)⦇CId⦈⦇b⦈ =
(∏⇩Ci∈⇩∘J ∪⇩∘ K. 𝔄 i)⦇CId⦈⦇a ∪⇩∘ b⦈"
proof-

interpret J𝔄: pcategory α J 𝔄
using assms(2) by (simp add: pcat_vsubset_index_pcategory)
interpret K𝔄: pcategory α K 𝔄
using assms(3) by (simp add: pcat_vsubset_index_pcategory)
interpret JK𝔄: pcategory α ‹J ∪⇩∘ K› 𝔄
using assms(2,3) by (simp add: pcat_vsubset_index_pcategory)

interpret J𝔄': category α ‹cat_prod J 𝔄›
by (rule J𝔄.pcat_category_cat_prod)
interpret K𝔄': category α ‹cat_prod K 𝔄›
by (rule K𝔄.pcat_category_cat_prod)
interpret JK𝔄': category α ‹cat_prod (J ∪⇩∘ K) 𝔄›
by (rule JK𝔄.pcat_category_cat_prod)

from assms(4) have CId_a: "cat_prod J 𝔄⦇CId⦈⦇a⦈ : a ↦⇘(∏⇩Cj∈⇩∘J. 𝔄 j)⇙ a"
by (auto intro: cat_cs_intros)
from assms(5) have CId_b: "cat_prod K 𝔄⦇CId⦈⦇b⦈ : b ↦⇘(∏⇩Ck∈⇩∘K. 𝔄 k)⇙ b"
by (auto intro: cat_cs_intros)
have CId_a_CId_b: "cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪⇩∘ cat_prod K 𝔄⦇CId⦈⦇b⦈ :
a ∪⇩∘ b ↦⇘cat_prod (J ∪⇩∘ K) 𝔄⇙ a ∪⇩∘ b"
by (rule pcat_cat_prod_vunion_is_arr[OF assms(1-3) CId_a CId_b])
from CId_a have a: "a ∈⇩∘ cat_prod J 𝔄⦇Obj⦈" by (auto intro: cat_cs_intros)
from CId_b have b: "b ∈⇩∘ cat_prod K 𝔄⦇Obj⦈" by (auto intro: cat_cs_intros)
from CId_a_CId_b have ab: "a ∪⇩∘ b ∈⇩∘ cat_prod (J ∪⇩∘ K) 𝔄⦇Obj⦈"
by (auto intro: cat_cs_intros)

and CId_bD = K𝔄.cat_prod_is_arrD[OF CId_b]

show ?thesis
proof(rule cat_prod_Arr_cong[of _ ‹J ∪⇩∘ K› 𝔄])
from CId_a_CId_b show
"cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪⇩∘ cat_prod K 𝔄⦇CId⦈⦇b⦈ ∈⇩∘ cat_prod (J ∪⇩∘ K) 𝔄⦇Arr⦈"
by auto
from ab show "cat_prod (J ∪⇩∘ K) 𝔄⦇CId⦈⦇a ∪⇩∘ b⦈ ∈⇩∘ cat_prod (J ∪⇩∘ K) 𝔄⦇Arr⦈"
by (auto intro: JK𝔄'.cat_is_arrD(1) cat_cs_intros)
fix i assume "i ∈⇩∘ J ∪⇩∘ K"
then consider (iJ) ‹i ∈⇩∘ J› | (iK) ‹i ∈⇩∘ K› by auto
then show "(cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪⇩∘ cat_prod K 𝔄⦇CId⦈⦇b⦈)⦇i⦈ =
cat_prod (J ∪⇩∘ K) 𝔄⦇CId⦈⦇a ∪⇩∘ b⦈⦇i⦈"
by cases
(
auto simp:
assms(1)
CId_bD(1-4)
cat_prod_CId_app[OF ab]
cat_prod_CId_app[OF a]
cat_prod_CId_app[OF b]
)
qed

qed

lemma (in pcategory) pcat_cat_prod_vdiff_vunion_CId:
assumes "J ⊆⇩∘ I"
and "a ∈⇩∘ (∏⇩Cj∈⇩∘I -⇩∘ J. 𝔄 j)⦇Obj⦈"
and "b ∈⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇Obj⦈"
shows
"(∏⇩Cj∈⇩∘I -⇩∘ J. 𝔄 j)⦇CId⦈⦇a⦈ ∪⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇CId⦈⦇b⦈ =
(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇a ∪⇩∘ b⦈"
by
(
vdiff_of_vunion'
rule: pcat_cat_prod_vunion_CId assms: assms(2-3) subset: assms(1)
)

subsection‹Projection›

subsubsection‹Definition and elementary properties›

text‹See Chapter II-3 in \<^cite>‹"mac_lane_categories_2010"›.›

definition cf_proj :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V" (‹π⇩C›)
where "π⇩C I 𝔄 i =
[
(λa∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈). a⦇i⦈),
(λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). f⦇i⦈),
(∏⇩Ci∈⇩∘I. 𝔄 i),
𝔄 i
]⇩∘"

text‹Components.›

lemma cf_proj_components:
shows "π⇩C I 𝔄 i⦇ObjMap⦈ = (λa∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈). a⦇i⦈)"
and "π⇩C I 𝔄 i⦇ArrMap⦈ = (λf∈⇩∘(∏⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈). f⦇i⦈)"
and "π⇩C I 𝔄 i⦇HomDom⦈ = (∏⇩Ci∈⇩∘I. 𝔄 i)"
and "π⇩C I 𝔄 i⦇HomCod⦈ = 𝔄 i"
unfolding cf_proj_def dghm_field_simps by (simp_all add: nat_omega_simps)

text‹Slicing›

lemma cf_smcf_cf_proj[slicing_commute]:
"π⇩S⇩M⇩C I (λi. cat_smc (𝔄 i)) i = cf_smcf (π⇩C I 𝔄 i)"
unfolding
cat_smc_def
cf_smcf_def
smcf_proj_def
cf_proj_def
cat_prod_def
smc_prod_def
dg_prod_def
dg_field_simps
dghm_field_simps

context pcategory
begin

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)›
by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
pcat_cf_proj_is_semifunctor = psmc.psmc_smcf_proj_is_semifunctor

end

subsubsection‹Projection functor is a functor›

lemma (in pcategory) pcat_cf_proj_is_functor:
assumes "i ∈⇩∘ I"
shows "π⇩C I 𝔄 i : (∏⇩Ci∈⇩∘I. 𝔄 i) ↦↦⇩C⇘α⇙ 𝔄 i"
proof(intro is_functorI)
interpret 𝔄: category α ‹(∏⇩Ci∈⇩∘I. 𝔄 i)›
show "vfsequence (π⇩C I 𝔄 i)" unfolding cf_proj_def by simp
show "category α (∏⇩Ci∈⇩∘I. 𝔄 i)" by (simp add: 𝔄.category_axioms)
show "vcard (π⇩C I 𝔄 i) = 4⇩ℕ"
unfolding cf_proj_def by (simp add: nat_omega_simps)
show "π⇩C I 𝔄 i⦇ArrMap⦈⦇(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = 𝔄 i⦇CId⦈⦇π⇩C I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈" for c
proof-
interpret 𝔄i: category α ‹𝔄 i›
by (auto intro: assms cat_prod_cs_intros)
from that have "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈ : c ↦⇘(∏⇩Ci∈⇩∘I. 𝔄 i)⇙ c"
then have "(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈ ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
by (auto intro: cat_cs_intros)
with assms have
"π⇩C I 𝔄 i⦇ArrMap⦈⦇(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = (∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈⦇i⦈"
unfolding cf_proj_components cat_prod_components by simp
also from assms have "… = 𝔄 i⦇CId⦈⦇c⦇i⦈⦈"
unfolding cat_prod_CId_app[OF that] by simp
also from that have "… = 𝔄 i⦇CId⦈⦇π⇩C I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
unfolding cf_proj_components cat_prod_components by simp
finally show
"π⇩C I 𝔄 i⦇ArrMap⦈⦇(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = 𝔄 i⦇CId⦈⦇π⇩C I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
by simp
qed
qed
(
auto simp:
assms cf_proj_components pcat_cf_proj_is_semifunctor cat_prod_cs_intros
)

lemma (in pcategory) pcat_cf_proj_is_functor':
assumes "i ∈⇩∘ I" and "ℭ = (∏⇩Ci∈⇩∘I. 𝔄 i)" and "𝔇 = 𝔄 i"
shows "π⇩C I 𝔄 i : ℭ ↦↦⇩C⇘α⇙ 𝔇"
using assms(1) unfolding assms(2,3) by (rule pcat_cf_proj_is_functor)

lemmas [cat_cs_intros] = pcategory.pcat_cf_proj_is_functor'

subsection‹Category product universal property functor›

subsubsection‹Definition and elementary properties›

text‹
The functor that is presented in this section is used in the proof of
the universal property of the product category later in this work.
›

definition cf_up :: "V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
where "cf_up I 𝔄 ℭ φ =
[
(λa∈⇩∘ℭ⦇Obj⦈. (λi∈⇩∘I. φ i⦇ObjMap⦈⦇a⦈)),
(λf∈⇩∘ℭ⦇Arr⦈. (λi∈⇩∘I. φ i⦇ArrMap⦈⦇f⦈)),
ℭ,
(∏⇩Ci∈⇩∘I. 𝔄 i)
]⇩∘"

text‹Components.›

lemma cf_up_components:
shows "cf_up I 𝔄 ℭ φ⦇ObjMap⦈ = (λa∈⇩∘ℭ⦇Obj⦈. (λi∈⇩∘I. φ i⦇ObjMap⦈⦇a⦈))"
and "cf_up I 𝔄 ℭ φ⦇ArrMap⦈ = (λf∈⇩∘ℭ⦇Arr⦈. (λi∈⇩∘I. φ i⦇ArrMap⦈⦇f⦈))"
and "cf_up I 𝔄 ℭ φ⦇HomDom⦈ = ℭ"
and "cf_up I 𝔄 ℭ φ⦇HomCod⦈ = (∏⇩Ci∈⇩∘I. 𝔄 i)"
unfolding cf_up_def dghm_field_simps by (simp_all add: nat_omega_simps)

text‹Slicing.›

lemma smcf_dghm_cf_up[slicing_commute]:
"smcf_up I (λi. cat_smc (𝔄 i)) (cat_smc ℭ) (λi. cf_smcf (φ i)) =
cf_smcf (cf_up I 𝔄 ℭ φ)"
unfolding
cat_smc_def
cf_smcf_def
cf_up_def
smcf_up_def
cat_prod_def
smc_prod_def
dg_prod_def
dg_field_simps
dghm_field_simps

context
fixes 𝔄 φ :: "V ⇒ V"
and ℭ :: V
begin

lemmas_with
[
where 𝔄=‹λi. cat_smc (𝔄 i)› and φ=‹λi. cf_smcf (φ i)› and ℭ = ‹cat_smc ℭ›,
unfolded slicing_simps slicing_commute
]:
cf_up_ObjMap_vdomain[simp] = smcf_up_ObjMap_vdomain
and cf_up_ObjMap_app = smcf_up_ObjMap_app
and cf_up_ObjMap_app_vdomain[simp] = smcf_up_ObjMap_app_vdomain
and cf_up_ObjMap_app_component = smcf_up_ObjMap_app_component
and cf_up_ArrMap_vdomain[simp] = smcf_up_ArrMap_vdomain
and cf_up_ArrMap_app = smcf_up_ArrMap_app
and cf_up_ArrMap_app_vdomain[simp] = smcf_up_ArrMap_app_vdomain
and cf_up_ArrMap_app_component = smcf_up_ArrMap_app_component

lemma cf_up_ObjMap_vrange:
assumes "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
shows "ℛ⇩∘ (cf_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈"
proof
(
rule smcf_up_ObjMap_vrange[
where 𝔄=‹λi. cat_smc (𝔄 i)›
and φ=‹λi. cf_smcf (φ i)›
and ℭ=‹cat_smc ℭ›,
unfolded slicing_simps slicing_commute
]
)
fix i assume "i ∈⇩∘ I"
then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
show "cf_smcf (φ i) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (𝔄 i)"
by (rule cf_is_semifunctor)
qed

lemma cf_up_ObjMap_app_vrange:
assumes "a ∈⇩∘ ℭ⦇Obj⦈" and "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
shows " ℛ⇩∘ (cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈) ⊆⇩∘ (⋃⇩∘i∈⇩∘I. 𝔄 i⦇Obj⦈)"
proof
(
rule smcf_up_ObjMap_app_vrange[
where 𝔄=‹λi. cat_smc (𝔄 i)›
and φ=‹λi. cf_smcf (φ i)›
and ℭ=‹cat_smc ℭ›,
unfolded slicing_simps slicing_commute
]
)
show "a ∈⇩∘ ℭ⦇Obj⦈" by (rule assms)
fix i assume "i ∈⇩∘ I"
then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
show "cf_smcf (φ i) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (𝔄 i)"
by (rule cf_is_semifunctor)
qed

lemma cf_up_ArrMap_vrange:
assumes "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
shows "ℛ⇩∘ (cf_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
proof
(
rule smcf_up_ArrMap_vrange[
where 𝔄=‹λi. cat_smc (𝔄 i)›
and φ=‹λi. cf_smcf (φ i)›
and ℭ=‹cat_smc ℭ›,
unfolded slicing_simps slicing_commute
]
)
fix i assume "i ∈⇩∘ I"
then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
show "cf_smcf (φ i) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (𝔄 i)"
by (rule cf_is_semifunctor)
qed

lemma cf_up_ArrMap_app_vrange:
assumes "a ∈⇩∘ ℭ⦇Arr⦈" and "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
shows " ℛ⇩∘ (cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈) ⊆⇩∘ (⋃⇩∘i∈⇩∘I. 𝔄 i⦇Arr⦈)"
proof
(
rule smcf_up_ArrMap_app_vrange
[
where 𝔄=‹λi. cat_smc (𝔄 i)›
and φ=‹λi. cf_smcf (φ i)›
and ℭ=‹cat_smc ℭ›,
unfolded slicing_simps slicing_commute
]
)
fix i assume "i ∈⇩∘ I"
then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
show "cf_smcf (φ i) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (𝔄 i)"
by (rule cf_is_semifunctor)
qed (rule assms)

end

context pcategory
begin

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)›
by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
pcat_smcf_comp_smcf_proj_smcf_up = psmc.psmc_Comp_smcf_proj_smcf_up
and pcat_smcf_up_eq_smcf_proj = psmc.psmc_smcf_up_eq_smcf_proj

end

subsubsection‹Category product universal property functor is a functor›

lemma (in pcategory) pcat_cf_up_is_functor:
assumes "category α ℭ" and "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
shows "cf_up I 𝔄 ℭ φ : ℭ ↦↦⇩C⇘α⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)"
proof-
interpret ℭ: category α ℭ by (simp add: assms(1))
interpret 𝔄: category α ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› by (rule pcat_category_cat_prod)
show ?thesis
proof(intro is_functorI)
show "vfsequence (cf_up I 𝔄 ℭ φ)" unfolding cf_up_def by simp
show "vcard (cf_up I 𝔄 ℭ φ) = 4⇩ℕ"
unfolding cf_up_def by (simp add: nat_omega_simps)
show "cf_smcf (cf_up I 𝔄 ℭ φ) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (∏⇩Ci∈⇩∘I. 𝔄 i)"
unfolding slicing_commute[symmetric]
by (rule psemicategory.psmc_smcf_up_is_semifunctor)
(
auto simp:
assms(2)
pcat_psemicategory
is_functor.cf_is_semifunctor
slicing_intros
)
show "cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ =
(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ ℭ⦇Obj⦈" for c
proof(rule cat_prod_Arr_cong)
from that is_arrD(1) have CId_c: "ℭ⦇CId⦈⦇c⦈ ∈⇩∘ ℭ⦇Arr⦈"
by (auto intro: cat_cs_intros)
from CId_c cf_up_ArrMap_vrange[OF assms(2), simplified]
show "cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
unfolding cf_up_components by force
have cf_up_φ_c: "cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈ ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Obj⦈"
unfolding cat_prod_components
proof(intro vproductI ballI)
fix i assume prems: "i ∈⇩∘ I"
interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (simp add: prems assms(2))
from that show  "cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦇i⦈ ∈⇩∘ 𝔄 i⦇Obj⦈"
unfolding cf_up_ObjMap_app_component[OF that prems]
by (auto intro: cat_cs_intros)
qed (simp_all add: cf_up_ObjMap_app that cf_up_ObjMap_app[OF that])
from 𝔄.cat_CId_is_arr[OF this] show
"(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈ ∈⇩∘ (∏⇩Ci∈⇩∘I. 𝔄 i)⦇Arr⦈"
by auto
fix i assume prems: "i ∈⇩∘ I"
interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (simp add: prems assms(2))
from cf_up_φ_c prems show
"cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈⦇i⦈ =
(∏⇩Ci∈⇩∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈⦇i⦈"
unfolding cf_up_ArrMap_app_component[OF CId_c prems] cat_prod_components
by
(
that cf_up_ObjMap_app_component[OF that prems] φ.cf_ObjMap_CId
)
qed
qed (auto simp: cf_up_components cat_cs_intros)
qed

subsubsection‹Further properties›

lemma (in pcategory) pcat_Comp_cf_proj_cf_up:
assumes "category α ℭ"
and "⋀i. i ∈⇩∘ I ⟹ φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
and "i ∈⇩∘ I"
shows "φ i = π⇩C I 𝔄 i ∘⇩C⇩F (cf_up I 𝔄 ℭ φ)"
proof-
interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF assms(3)])
interpret π: is_functor α ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› ‹𝔄 i› ‹π⇩C I 𝔄 i›
interpret up: is_functor α ℭ ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› ‹cf_up I 𝔄 ℭ φ›
by (simp add: assms(2) φ.HomDom.category_axioms pcat_cf_up_is_functor)
show ?thesis
proof(rule cf_smcf_eqI)
show "π⇩C I 𝔄 i ∘⇩C⇩F cf_up I 𝔄 ℭ φ : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
by (auto intro: cat_cs_intros)
from assms show "cf_smcf (φ i) = cf_smcf (π⇩C I 𝔄 i ∘⇩C⇩F cf_up I 𝔄 ℭ φ)"
unfolding slicing_simps slicing_commute[symmetric]
by
(
intro pcat_smcf_comp_smcf_proj_smcf_up[
where φ=‹λi. cf_smcf (φ i)›, unfolded slicing_commute[symmetric]
]
)
(auto simp: is_functor.cf_is_semifunctor)
qed (auto intro: cat_cs_intros)
qed

lemma (in pcategory) pcat_cf_up_eq_cf_proj:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)"
and "⋀i. i ∈⇩∘ I ⟹ φ i = π⇩C I 𝔄 i ∘⇩C⇩F 𝔉"
shows "cf_up I 𝔄 ℭ φ = 𝔉"
proof(rule cf_smcf_eqI)
interpret 𝔉: is_functor α ℭ ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› 𝔉 by (rule assms(1))
show "cf_up I 𝔄 ℭ φ : ℭ ↦↦⇩C⇘α⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)"
proof(rule pcat_cf_up_is_functor)
fix i assume prems: "i ∈⇩∘ I"
then interpret π: is_functor α ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› ‹𝔄 i› ‹π⇩C I 𝔄 i›
by (rule pcat_cf_proj_is_functor)
show "φ i : ℭ ↦↦⇩C⇘α⇙ 𝔄 i"
unfolding assms(2)[OF prems] by (auto intro: cat_cs_intros)
qed (auto intro: cat_cs_intros)
show "𝔉 : ℭ ↦↦⇩C⇘α⇙ (∏⇩Ci∈⇩∘I. 𝔄 i)" by (rule assms(1))
from assms show "cf_smcf (cf_up I 𝔄 ℭ φ) = cf_smcf 𝔉"
unfolding slicing_commute[symmetric]
by (intro pcat_smcf_up_eq_smcf_proj) (auto simp: slicing_commute)
qed simp_all

subsection‹Prodfunctor with respect to a fixed argument›

text‹
A prodfunctor is a functor whose domain is a product category.
It is a generalization of the concept of the bifunctor,
as presented in Chapter II-3 in \<^cite>‹"mac_lane_categories_2010"›.
›

definition prodfunctor_proj :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ V ⇒ V ⇒ V"
where "prodfunctor_proj 𝔖 I 𝔄 𝔇 J c =
[
(λb∈⇩∘(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈),
(λf∈⇩∘(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇CId⦈⦇c⦈⦈),
(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i),
𝔇
]⇩∘"

syntax "_PPRODFUNCTOR_PROJ" :: "V ⇒ pttrn ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ V ⇒ V"
(‹(_⇘(3∏⇩C_∈⇩∘_-⇩∘_./_),_⇙/'(/-,_/'))› [51, 51, 51, 51, 51, 51, 51] 51)
translations "𝔖⇘∏⇩Ci∈⇩∘I-⇩∘J. 𝔄,𝔇⇙(-,c)" ⇌
"CONST prodfunctor_proj 𝔖 I (λi. 𝔄) 𝔇 J c"

text‹Components.›

lemma prodfunctor_proj_components:
shows "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c))⦇ObjMap⦈ =
(λb∈⇩∘(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈)"
and "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c))⦇ArrMap⦈ =
(λf∈⇩∘(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇CId⦈⦇c⦈⦈)"
and "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c))⦇HomDom⦈ = (∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)"
and "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c))⦇HomCod⦈ = 𝔇"
unfolding prodfunctor_proj_def dghm_field_simps

subsubsection‹Object map›

mk_VLambda prodfunctor_proj_components(1)
|vsv prodfunctor_proj_ObjMap_vsv[cat_cs_intros]|
|vdomain prodfunctor_proj_ObjMap_vdomain[cat_cs_simps]|
|app prodfunctor_proj_ObjMap_app[cat_cs_simps]|

subsubsection‹Arrow map›

mk_VLambda prodfunctor_proj_components(2)
|vsv prodfunctor_proj_ArrMap_vsv[cat_cs_intros]|
|vdomain prodfunctor_proj_ArrMap_vdomain[cat_cs_simps]|
|app  prodfunctor_proj_ArrMap_app[cat_cs_simps]|

subsubsection‹Prodfunctor with respect to a fixed argument is a functor›

lemma (in pcategory) pcat_prodfunctor_proj_is_functor:
assumes "𝔖 : (∏⇩Ci∈⇩∘I. 𝔄 i) ↦↦⇩C⇘α⇙ 𝔇"
and "c ∈⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇Obj⦈"
and "J ⊆⇩∘ I"
shows "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c)) : (∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i) ↦↦⇩C⇘α⇙ 𝔇"
proof-

interpret is_functor α ‹(∏⇩Ci∈⇩∘I. 𝔄 i)› 𝔇 𝔖 by (rule assms(1))
interpret 𝔄: pcategory α J 𝔄
using assms(3) by (intro pcat_vsubset_index_pcategory) auto
interpret J_𝔄: category α ‹∏⇩Ci∈⇩∘J. 𝔄 i› by (rule 𝔄.pcat_category_cat_prod)
interpret IJ: pcategory α ‹I -⇩∘ J› 𝔄
using assms(3) by (intro pcat_vsubset_index_pcategory) auto
interpret IJ_𝔄: category α ‹∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i›
by (rule IJ.pcat_category_cat_prod)

let ?IJ𝔄 = ‹(∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)›

from assms(2) have "c ∈⇩∘ (∏⇩∘j∈⇩∘J. 𝔄 j⦇Obj⦈)"
unfolding cat_prod_components by simp
then have "(∏⇩∘j∈⇩∘J. 𝔄 j⦇Obj⦈) ≠ 0" by (auto intro!: cat_cs_intros)

show ?thesis
proof(intro is_functorI', unfold prodfunctor_proj_components)

show "vfsequence (prodfunctor_proj 𝔖 I 𝔄 𝔇 J c)"
unfolding prodfunctor_proj_def by simp
show "vcard (prodfunctor_proj 𝔖 I 𝔄 𝔇 J c) = 4⇩ℕ"
unfolding prodfunctor_proj_def by (simp add: nat_omega_simps)

show "ℛ⇩∘ (λb∈⇩∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈) ⊆⇩∘ 𝔇⦇Obj⦈"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ ℛ⇩∘ (λb∈⇩∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈)"
then obtain b where x_def: "x = 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈" and b: "b ∈⇩∘ ?IJ𝔄⦇Obj⦈"
by auto
have "b ∪⇩∘ c ∈⇩∘ cat_prod I 𝔄⦇Obj⦈"
proof(rule cat_prod_vdiff_vunion_Obj_in_Obj)
show "b ∈⇩∘ ?IJ𝔄⦇Obj⦈" by (rule b)
qed (intro assms(2,3))+
then show "x ∈⇩∘ 𝔇⦇Obj⦈" unfolding x_def by (auto intro: cat_cs_intros)
qed

show is_arr:
"(λf∈⇩∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇f⦈ :
(λb∈⇩∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈)⦇a⦈ ↦⇘𝔇⇙
(λb∈⇩∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈)⦇b⦈"
(is ‹?V_f: ?V_a ↦⇘𝔇⇙ ?V_b›)
if "f : a ↦⇘?IJ𝔄⇙ b" for f a b
proof-
let ?fc = ‹f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈›
have "?fc : a ∪⇩∘ c ↦⇘cat_prod I 𝔄⇙ b ∪⇩∘ c"
proof(rule pcat_cat_prod_vdiff_vunion_is_arr)
show "f : a ↦⇘?IJ𝔄⇙ b" by (rule that)
qed (auto simp: assms cat_cs_intros)
then have "𝔖⦇ArrMap⦈⦇?fc⦈ : 𝔖⦇ObjMap⦈⦇a ∪⇩∘ c⦈ ↦⇘𝔇⇙ 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈"
by (auto intro: cat_cs_intros)
moreover from that have "f ∈⇩∘ ?IJ𝔄⦇Arr⦈" "a ∈⇩∘ ?IJ𝔄⦇Obj⦈" "b ∈⇩∘ ?IJ𝔄⦇Obj⦈"
by (auto intro: cat_cs_intros)
ultimately show ?thesis by simp
qed

show
"(λf∈⇩∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇g ∘⇩A⇘?IJ𝔄⇙ f⦈ =
(λf∈⇩∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇g⦈ ∘⇩A⇘𝔇⇙
(λf∈⇩∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇f⦈"
if "g : b' ↦⇘?IJ𝔄⇙ c'" and "f : a' ↦⇘?IJ𝔄⇙ b'" for g b' c' f a'
proof-
from that have gf: "g ∘⇩A⇘?IJ𝔄⇙ f : a' ↦⇘?IJ𝔄⇙ c'"
by (auto intro: cat_cs_intros)
from assms(2) have CId_c: "cat_prod J 𝔄⦇CId⦈⦇c⦈ : c ↦⇘cat_prod J 𝔄⇙ c"
by (auto intro: cat_cs_intros)
then have [simp]:
"cat_prod J 𝔄⦇CId⦈⦇c⦈ ∘⇩A⇘cat_prod J 𝔄⇙ cat_prod J 𝔄⦇CId⦈⦇c⦈ =
cat_prod J 𝔄⦇CId⦈⦇c⦈"
by (auto simp: cat_cs_simps)
from assms(3) that(1) CId_c have g_CId_c:
"g ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ : b' ∪⇩∘ c ↦⇘cat_prod I 𝔄⇙ c' ∪⇩∘ c"
by (rule pcat_cat_prod_vdiff_vunion_is_arr)
from assms(3) that(2) CId_c have f_CId_c:
"f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ : a' ∪⇩∘ c ↦⇘cat_prod I 𝔄⇙ b' ∪⇩∘ c"
by (rule pcat_cat_prod_vdiff_vunion_is_arr)
have
"𝔖⦇ArrMap⦈⦇(g ∘⇩A⇘?IJ𝔄⇙ f) ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ =
𝔖⦇ArrMap⦈⦇g ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ ∘⇩A⇘𝔇⇙
𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈"
unfolding
pcat_cat_prod_vdiff_vunion_Comp[
OF assms(3) that(1) CId_c that(2) CId_c, simplified
]
by (intro cf_ArrMap_Comp[OF g_CId_c f_CId_c])
moreover from gf have "g ∘⇩A⇘?IJ𝔄⇙ f ∈⇩∘ ?IJ𝔄⦇Arr⦈" by auto
moreover from that have "g ∈⇩∘ ?IJ𝔄⦇Arr⦈" "f ∈⇩∘ ?IJ𝔄⦇Arr⦈" by auto
ultimately show ?thesis by simp
qed

show
"(λf∈⇩∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇?IJ𝔄⦇CId⦈⦇c'⦈⦈ =
𝔇⦇CId⦈⦇(λb∈⇩∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪⇩∘ c⦈)⦇c'⦈⦈"
if "c' ∈⇩∘ ?IJ𝔄⦇Obj⦈" for c'
proof-
have "?IJ𝔄⦇CId⦈⦇c'⦈ ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ = cat_prod I 𝔄⦇CId⦈⦇c' ∪⇩∘ c⦈"
unfolding pcat_cat_prod_vdiff_vunion_CId[OF assms(3) that assms(2)] ..
moreover from assms(3) that assms(2) have "c' ∪⇩∘ c ∈⇩∘ cat_prod I 𝔄⦇Obj⦈"
by (rule cat_prod_vdiff_vunion_Obj_in_Obj)
ultimately have "𝔖⦇ArrMap⦈⦇?IJ𝔄⦇CId⦈⦇c'⦈ ∪⇩∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ =
𝔇⦇CId⦈⦇𝔖⦇ObjMap⦈⦇c' ∪⇩∘ c⦈⦈"
by (auto intro: cat_cs_intros)
moreover from that have CId_c': "?IJ𝔄⦇CId⦈⦇c'⦈ ∈⇩∘ ?IJ𝔄⦇Arr⦈"
by (auto dest!: IJ_𝔄.cat_CId_is_arr)
ultimately show ?thesis by (simp add: that)
qed

qed (auto intro: cat_cs_intros)

qed

lemma (in pcategory) pcat_prodfunctor_proj_is_functor':
assumes "𝔖 : (∏⇩Ci∈⇩∘I. 𝔄 i) ↦↦⇩C⇘α⇙ 𝔇"
and "c ∈⇩∘ (∏⇩Cj∈⇩∘J. 𝔄 j)⦇Obj⦈"
and "J ⊆⇩∘ I"
and "𝔄' = (∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i)"
and "𝔅' = 𝔇"
shows "(𝔖⇘∏⇩Ci∈⇩∘I -⇩∘ J. 𝔄 i,𝔇⇙(-,c)) : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
using assms(1-3)
unfolding assms(4,5)
by (rule pcat_prodfunctor_proj_is_functor)

lemmas [cat_cs_intros] = pcategory.pcat_prodfunctor_proj_is_functor'

subsection‹Singleton category›

subsubsection‹Slicing›

context
fixes ℭ :: V
begin

lemmas_with [where ℭ=‹cat_smc ℭ›, unfolded slicing_simps slicing_commute]:
cat_singleton_ObjI = smc_singleton_ObjI
and cat_singleton_ObjE = smc_singleton_ObjE
and cat_singleton_ArrI = smc_singleton_ArrI
and cat_singleton_ArrE = smc_singleton_ArrE

end

context category
begin

interpretation smc: semicategory α ‹cat_smc ℭ› by (rule cat_semicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
cat_finite_psemicategory_cat_singleton =
smc.smc_finite_psemicategory_smc_singleton
and cat_singleton_is_arrI = smc.smc_singleton_is_arrI
and cat_singleton_is_arrD = smc.smc_singleton_is_arrD
and cat_singleton_is_arrE = smc.smc_singleton_is_arrE

end

subsubsection‹Identity›

lemma cat_singleton_CId_app:
assumes "set {⟨j, a⟩} ∈⇩∘ (∏⇩Ci∈⇩∘set {j}. ℭ)⦇Obj⦈"
shows "(∏⇩Ci∈⇩∘set {j}. ℭ)⦇CId⦈⦇set {⟨j, a⟩}⦈ = set {⟨j, ℭ⦇CId⦈⦇a⦈⟩}"
using assms unfolding cat_prod_components VLambda_vsingleton by simp

subsubsection‹Singleton category is a category›

lemma (in category) cat_finite_pcategory_cat_singleton:
assumes "j ∈⇩∘ Vset α"
shows "finite_pcategory α (set {j}) (λi. ℭ)"
by
(
auto intro:
assms
category_axioms
finite_pcategory_finite_psemicategoryI
cat_finite_psemicategory_cat_singleton
)

lemma (in category) cat_category_cat_singleton:
assumes "j ∈⇩∘ Vset α"
shows "category α (∏⇩Ci∈⇩∘set {j}. ℭ)"
proof-
interpret finite_pcategory α ‹set {j}› ‹λi. ℭ›
using assms by (rule cat_finite_pcategory_cat_singleton)
show ?thesis by (rule pcat_category_cat_prod)
qed

subsection‹Singleton functor›

subsubsection‹Definition and elementary properties›

definition cf_singleton :: "V ⇒ V ⇒ V"
where "cf_singleton j ℭ =
[
(λa∈⇩∘ℭ⦇Obj⦈. set {⟨j, a⟩}),
(λf∈⇩∘ℭ⦇Arr⦈. set {⟨j, f⟩}),
ℭ,
(∏⇩Ci∈⇩∘set {j}. ℭ)
]⇩∘"

text‹Components.›

lemma cf_singleton_components:
shows "cf_singleton j ℭ⦇ObjMap⦈ = (λa∈⇩∘ℭ⦇Obj⦈. set {⟨j, a⟩})"
and "cf_singleton j ℭ⦇ArrMap⦈ = (λf∈⇩∘ℭ⦇Arr⦈. set {⟨j, f⟩})"
and "cf_singleton j ℭ⦇HomDom⦈ = ℭ"
and "cf_singleton j ℭ⦇HomCod⦈ = (∏⇩Ci∈⇩∘set {j}. ℭ)"
unfolding cf_singleton_def dghm_field_simps by (simp_all add: nat_omega_simps)

text‹Slicing.›

lemma cf_smcf_cf_singleton[slicing_commute]:
"smcf_singleton j (cat_smc ℭ)= cf_smcf (cf_singleton j ℭ)"
unfolding smcf_singleton_def cf_singleton_def slicing_simps slicing_commute
by
(
nat_omega_simps dghm_field_simps dg_field_simps cat_smc_def cf_smcf_def
)

context
fixes ℭ :: V
begin

lemmas_with [where ℭ=‹cat_smc ℭ›, unfolded slicing_simps slicing_commute]:
cf_singleton_ObjMap_vsv[cat_cs_intros] = smcf_singleton_ObjMap_vsv
and cf_singleton_ObjMap_vdomain[cat_cs_simps] = smcf_singleton_ObjMap_vdomain
and cf_singleton_ObjMap_vrange = smcf_singleton_ObjMap_vrange
and cf_singleton_ObjMap_app[cat_prod_cs_simps] = smcf_singleton_ObjMap_app
and cf_singleton_ArrMap_vsv[cat_cs_intros] = smcf_singleton_ArrMap_vsv
and cf_singleton_ArrMap_vdomain[cat_cs_simps] = smcf_singleton_ArrMap_vdomain
and cf_singleton_ArrMap_vrange = smcf_singleton_ArrMap_vrange
and cf_singleton_ArrMap_app[cat_prod_cs_simps] = smcf_singleton_ArrMap_app

end

subsubsection‹Singleton functor is an isomorphism of categories›

lemma (in category) cat_cf_singleton_is_functor:
assumes "j ∈⇩∘ Vset α"
shows "cf_singleton j ℭ : ℭ ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ (∏⇩Ci∈⇩∘set {j}. ℭ)"
proof(intro is_iso_functorI is_functorI)
from assms show smcf_singleton: "cf_smcf (cf_singleton j ℭ) :
cat_smc ℭ ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_smc (∏⇩Ci∈⇩∘set {j}. ℭ)"
unfolding slicing_commute[symmetric]
by (intro semicategory.smc_smcf_singleton_is_iso_semifunctor)
(auto intro: smc_cs_intros slicing_intros)
show "vfsequence (cf_singleton j ℭ)" unfolding cf_singleton_def by simp
show "vcard (cf_singleton j ℭ) = 4⇩ℕ"
unfolding cf_singleton_def by (simp add: nat_omega_simps)
show "cf_smcf (cf_singleton j ℭ) :
cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc (∏⇩Ci∈⇩∘set {j}. ℭ)"
by (intro is_iso_semifunctor.axioms(1) smcf_singleton)
show "cf_singleton j ℭ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ =
(∏⇩Ci∈⇩∘set {j}. ℭ)⦇CId⦈⦇cf_singleton j ℭ⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ ℭ⦇Obj⦈" for c
proof-
from that have CId_c: "ℭ⦇CId⦈⦇c⦈ : c ↦⇘ℭ⇙ c" by (auto simp: cat_cs_intros)
have "set {⟨j, c⟩} ∈⇩∘ (∏⇩Ci∈⇩∘set {j}. ℭ)⦇Obj⦈"
with that have "(∏⇩Ci∈⇩∘set {j}. ℭ)⦇CId⦈⦇cf_singleton j ℭ⦇ObjMap⦈⦇c⦈⦈ =
set {⟨j, ℭ⦇CId⦈⦇c⦈⟩}"
moreover from CId_c have
"cf_singleton j ℭ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = set {⟨j, ℭ⦇CId⦈⦇c⦈⟩}"
by (auto simp: cf_singleton_ArrMap_app cat_cs_intros)
ultimately show ?thesis by simp
qed
qed
(
auto simp:
cat_cs_intros assms cat_category_cat_singleton cf_singleton_components
)

subsection‹Product of two categories›

subsubsection‹Definition and elementary properties.›

text‹See Chapter II-3 in \<^cite>‹"mac_lane_categories_2010"›.›

definition cat_prod_2 :: "V ⇒ V ⇒ V" (infixr ‹×⇩C› 80)
where "𝔄 ×⇩C 𝔅 ≡ cat_prod (2⇩ℕ) (λi. if i = 0 then 𝔄 else 𝔅)"

text‹Slicing.›

lemma cat_smc_cat_prod_2[slicing_commute]:
"cat_smc 𝔄 ×⇩S⇩M⇩C cat_smc 𝔅 = cat_smc (𝔄 ×⇩C 𝔅)"
unfolding cat_prod_2_def smc_prod_2_def slicing_commute[symmetric] if_distrib
by simp

context
fixes α 𝔄 𝔅
assumes 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅"
begin

interpretation 𝔄: category α 𝔄 by (rule 𝔄)
interpretation 𝔅: category α 𝔅 by (rule 𝔅)

lemmas_with
[
where 𝔄=‹cat_smc 𝔄› and 𝔅=‹cat_smc 𝔅›,
unfolded slicing_simps slicing_commute,
OF 𝔄.cat_semicategory 𝔅.cat_semicategory
]:
cat_prod_2_ObjI = smc_prod_2_ObjI
and cat_prod_2_ObjI'[cat_prod_cs_intros] = smc_prod_2_ObjI'
and cat_prod_2_ObjE = smc_prod_2_ObjE
and cat_prod_2_ArrI = smc_prod_2_ArrI
and cat_prod_2_ArrI'[cat_prod_cs_intros] = smc_prod_2_ArrI'
and cat_prod_2_ArrE = smc_prod_2_ArrE
and cat_prod_2_is_arrI = smc_prod_2_is_arrI
and cat_prod_2_is_arrI'[cat_prod_cs_intros] = smc_prod_2_is_arrI'
and cat_prod_2_is_arrE = smc_prod_2_is_arrE
and cat_prod_2_Dom_vsv = smc_prod_2_Dom_vsv
and cat_prod_2_Dom_vdomain[cat_cs_simps] = smc_prod_2_Dom_vdomain
and cat_prod_2_Dom_app[cat_prod_cs_simps] = smc_prod_2_Dom_app
and cat_prod_2_Dom_vrange = smc_prod_2_Dom_vrange
and cat_prod_2_Cod_vsv = smc_prod_2_Cod_vsv
and cat_prod_2_Cod_vdomain[cat_cs_simps] = smc_prod_2_Cod_vdomain
and cat_prod_2_Cod_app[cat_prod_cs_simps] = smc_prod_2_Cod_app
and cat_prod_2_Cod_vrange = smc_prod_2_Cod_vrange
and cat_prod_2_op_cat_cat_Obj[cat_op_simps] = smc_prod_2_op_smc_smc_Obj
and cat_prod_2_cat_op_cat_Obj[cat_op_simps] = smc_prod_2_smc_op_smc_Obj
and cat_prod_2_op_cat_cat_Arr[cat_op_simps] = smc_prod_2_op_smc_smc_Arr
and cat_prod_2_cat_op_cat_Arr[cat_op_simps] = smc_prod_2_smc_op_smc_Arr

lemmas_with
[
where 𝔄=‹cat_smc 𝔄› and 𝔅=‹cat_smc 𝔅›,
unfolded slicing_simps slicing_commute,
OF 𝔄.cat_semicategory 𝔅.cat_semicategory
]:
cat_prod_2_Comp_app[cat_prod_cs_simps] = smc_prod_2_Comp_app

end

subsubsection‹Product of two categories is a category›

context
fixes α 𝔄 𝔅
assumes 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅"
begin

interpretation 𝒵 α by (rule categoryD[OF 𝔄])
interpretation 𝔄: category α 𝔄 by (rule 𝔄)
interpretation 𝔅: category α 𝔅 by (rule 𝔅)

lemma finite_pcategory_cat_prod_2: "finite_pcategory α (2⇩ℕ) (if2 𝔄 𝔅)"
proof(intro finite_pcategoryI pcategory_baseI)
from Axiom_of_Infinity show z1_in_Vset: "2⇩ℕ ∈⇩∘ Vset α" by blast
show "category α (i = 0 ? 𝔄 : 𝔅)" if "i ∈⇩∘ 2⇩ℕ" for i
by (auto simp: cat_cs_intros)
qed auto

interpretation finite_pcategory α ‹2⇩ℕ› ‹if2 𝔄 𝔅›
by (intro finite_pcategory_cat_prod_2 𝔄 𝔅)

lemma category_cat_prod_2[cat_cs_intros]: "category α (𝔄 ×⇩C 𝔅)"
unfolding cat_prod_2_def by (rule pcat_category_cat_prod)

end

subsubsection‹Identity›

lemma cat_prod_2_CId_vsv[cat_cs_intros]: "vsv ((𝔄 ×⇩C 𝔅)⦇CId⦈)"
unfolding cat_prod_2_def cat_prod_components by simp

lemma cat_prod_2_CId_vdomain[cat_cs_simps]:
"𝒟⇩∘ ((𝔄 ×⇩C 𝔅)⦇CId⦈) = (𝔄 ×⇩C 𝔅)⦇Obj⦈"
unfolding cat_prod_2_def cat_prod_components by simp

context
fixes α 𝔄 𝔅
assumes 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅"
begin

interpretation 𝔄: category α 𝔄 by (rule 𝔄)
interpretation 𝔅: category α 𝔅 by (rule 𝔅)

interpretation finite_pcategory α ‹2⇩ℕ› ‹(λi. if i = 0 then 𝔄 else 𝔅)›
by (intro finite_pcategory_cat_prod_2 𝔄 𝔅)

lemma cat_prod_2_CId_app[cat_prod_cs_simps]:
assumes "[a, b]⇩∘ ∈⇩∘ (𝔄 ×⇩C 𝔅)⦇Obj⦈"
shows "(𝔄 ×⇩C 𝔅)⦇CId⦈⦇a, b⦈⇩∙ = [𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]⇩∘"
proof-
have "(𝔄 ×⇩C 𝔅)⦇CId⦈⦇a, b⦈⇩∙ =
(λi∈⇩∘2⇩ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]⇩∘⦇i⦈⦈)"
by
(
rule
cat_prod_CId_app[
OF assms[unfolded cat_prod_2_def], folded cat_prod_2_def
]
)
also have
"(λi∈⇩∘2⇩ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]⇩∘⦇i⦈⦈) =
[𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]⇩∘"
proof(rule vsv_eqI, unfold vdomain_VLambda)
fix i assume "i ∈⇩∘ 2⇩ℕ"
then consider ‹i = 0› | ‹i = 1⇩ℕ› unfolding two by auto
then show
"(λi∈⇩∘2⇩ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]⇩∘⦇i⦈⦈)⦇i⦈ =
[𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]⇩∘⦇i⦈"
by cases (simp_all add: two nat_omega_simps)
qed (auto simp: two nat_omega_simps)
finally show ?thesis by simp
qed

lemma cat_prod_2_CId_vrange: "ℛ⇩∘ ((𝔄 ×⇩C 𝔅)⦇CId⦈) ⊆⇩∘ (𝔄 ×⇩C 𝔅)⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cat_cs_simps)
show "vsv ((𝔄 ×⇩C 𝔅)⦇CId⦈)" by (rule cat_prod_2_CId_vsv)
fix ab assume "ab ∈⇩∘ (𝔄 ×⇩C 𝔅)⦇Obj⦈"
then obtain a b where ab_def: "ab = [a, b]⇩∘"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
and b: "b ∈⇩∘ 𝔅⦇Obj⦈"
by (elim cat_prod_2_ObjE[OF 𝔄 𝔅])
from 𝔄 𝔅 a b show "(𝔄 ×⇩C 𝔅)⦇CId⦈⦇ab⦈ ∈⇩∘ (𝔄 ×⇩C 𝔅)⦇Arr⦈"
unfolding ab_def by (cs_concl cs_intro: cat_cs_intros cat_prod_cs_intros)
qed

end

subsubsection‹Opposite product category›

context
fixes α 𝔄 𝔅
assumes 𝔄: "category α 𝔄" and 𝔅: "category α 𝔅"
begin

interpretation 𝔄: category α 𝔄 by (rule 𝔄)
interpretation 𝔅: category α 𝔅 by (rule 𝔅)

lemma op_smc_smc_prod_2[smc_op_simps]:
"op_cat (𝔄 ×⇩C 𝔅) = op_cat 𝔄 ×⇩C op_cat 𝔅"
proof(rule cat_smc_eqI [of α])
from 𝔄 𝔅 show cat_lhs: "category α (op_cat (𝔄 ×⇩C 𝔅))"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: ```