Theory CZH_DG_Set

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Set› as a digraph›
theory CZH_DG_Set
  imports CZH_DG_Par
begin



subsection‹Background›


text‹
‹Set› is usually defined as a category of sets and total functions
(see Chapter I-2 in cite‹"mac_lane_categories_2010"›). However, there
is little that can prevent one from exposing ‹Set› as a digraph and
provide additional structure gradually later. 
Thus, in this section, ‹α›-‹Set› is defined as a digraph of sets 
and binary relations in the set ‹Vα›. 
›

named_theorems dg_Set_cs_simps
named_theorems dg_Set_cs_intros

lemmas [dg_Set_cs_simps] = dg_Rel_shared_cs_simps
lemmas [dg_Set_cs_intros] = dg_Rel_shared_cs_intros



subsection‹Arrow for ‹Set››


subsubsection‹Definition and elementary properties›

locale arr_Set = 𝒵 α + vfsequence T + ArrVal: vsv ‹T⦇ArrVal⦈› for α T +
  assumes arr_Set_length[dg_Rel_shared_cs_simps, dg_Set_cs_simps]: 
      "vcard T = 3ℕ" 
    and arr_Set_ArrVal_vdomain[dg_Rel_shared_cs_simps, dg_Set_cs_simps]: 
      "𝒟∘ (T⦇ArrVal⦈) = T⦇ArrDom⦈"
    and arr_Set_ArrVal_vrange: "ℛ∘ (T⦇ArrVal⦈) ⊆∘ T⦇ArrCod⦈"
    and arr_Set_ArrDom_in_Vset: "T⦇ArrDom⦈ ∈∘ Vset α"
    and arr_Set_ArrCod_in_Vset: "T⦇ArrCod⦈ ∈∘ Vset α"

lemmas [dg_Set_cs_simps] = arr_Set.arr_Set_ArrVal_vdomain


text‹Elementary properties.›

sublocale arr_Set ⊆ arr_Par
  by unfold_locales 
    (
      simp_all add:
        dg_Set_cs_simps
        arr_Set_ArrVal_vrange arr_Set_ArrDom_in_Vset arr_Set_ArrCod_in_Vset
    )


text‹Rules.›

lemma (in arr_Set) arr_Set_axioms'[dg_cs_intros, dg_Set_cs_intros]:
  assumes "α' = α"
  shows "arr_Set α' T"
  unfolding assms by (rule arr_Set_axioms)

mk_ide rf arr_Set_def[unfolded arr_Set_axioms_def]
  |intro arr_SetI|
  |dest arr_SetD[dest]|
  |elim arr_SetE[elim!]|

lemma (in 𝒵) arr_Set_vfsequenceI: 
  assumes "vsv r" 
    and "𝒟∘ r = a"
    and "ℛ∘ r ⊆∘ b"
    and "a ∈∘ Vset α"
    and "b ∈∘ Vset α"
  shows "arr_Set α [r, a, b]∘"
  by (intro arr_SetI) 
    (insert assms, auto simp: arr_Rel_components nat_omega_simps)

lemma arr_Set_arr_ParI:
  assumes "arr_Par α T" and "𝒟∘ (T⦇ArrVal⦈) = T⦇ArrDom⦈"
  shows "arr_Set α T"
proof-
  interpret arr_Par α T by (rule assms(1))
  show ?thesis
    by (intro arr_SetI)
      (
        auto simp: 
          dg_Par_cs_simps
          assms(2) 
          vfsequence_axioms 
          arr_Rel_ArrVal_vrange 
          arr_Rel_ArrDom_in_Vset 
          arr_Rel_ArrCod_in_Vset
      )
qed 

lemma arr_Set_arr_ParD:
  assumes "arr_Set α T"
  shows "arr_Par α T" and "𝒟∘ (T⦇ArrVal⦈) = T⦇ArrDom⦈"
proof-
  interpret arr_Set α T by (rule assms)
  show "arr_Par α T" and "𝒟∘ (T⦇ArrVal⦈) = T⦇ArrDom⦈"
    by (rule arr_Par_axioms) (auto simp: dg_Set_cs_simps)
qed

lemma arr_Set_arr_ParE:
  assumes "arr_Set α T"
  obtains "arr_Par α T" and "𝒟∘ (T⦇ArrVal⦈) = T⦇ArrDom⦈"
  using assms by (auto simp: arr_Set_arr_ParD)


text‹Further properties.›

lemma arr_Set_eqI:
  assumes "arr_Set α S" 
    and "arr_Set α T"
    and "S⦇ArrVal⦈ = T⦇ArrVal⦈"
    and "S⦇ArrDom⦈ = T⦇ArrDom⦈"
    and "S⦇ArrCod⦈ = T⦇ArrCod⦈"
  shows "S = T"
proof-
  interpret S: arr_Set α S by (rule assms(1))
  interpret T: arr_Set α T by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟∘ S = 3ℕ" by (simp add: S.vfsequence_vdomain dg_Set_cs_simps)
    show "a ∈∘ 𝒟∘ S ⟹ S⦇a⦈ = T⦇a⦈" for a
      by (unfold dom, elim_in_numeral, insert assms)
        (auto simp: arr_field_simps)
  qed (auto simp: S.vfsequence_vdomain T.vfsequence_vdomain dg_Set_cs_simps) 
qed

lemma small_arr_Set[simp]: "small {T. arr_Set α T}"
proof(rule smaller_than_small)
  show "{T. arr_Set α T} ⊆ {T. arr_Par α T}" 
    by (simp add: Collect_mono arr_Set_arr_ParD(1))
qed simp

lemma set_Collect_arr_Set[simp]: 
  "T ∈∘ set (Collect (arr_Set α)) ⟷ arr_Set α T" 
  by auto


subsubsection‹Composition›


text‹See cite‹"mac_lane_categories_2010"›).›

abbreviation (input) comp_Set :: "V ⇒ V ⇒ V" (infixl ‹∘Set› 55)
  where "comp_Set ≡ comp_Rel"

lemma arr_Set_comp_Set[dg_Set_cs_intros]:
  assumes "arr_Set α S" and "arr_Set α T" and "ℛ∘ (T⦇ArrVal⦈) ⊆∘ 𝒟∘ (S⦇ArrVal⦈)"
  shows "arr_Set α (S ∘Set T)"
proof(intro arr_Set_arr_ParI)
  interpret S: arr_Set α S by (rule assms(1))
  interpret T: arr_Set α T by (rule assms(2))
  show "arr_Par α (S ∘Set T)"
    by (auto simp: S.arr_Par_axioms T.arr_Par_axioms arr_Par_comp_Par)
  show "𝒟∘ ((S ∘Rel T)⦇ArrVal⦈) = (S ∘Rel T)⦇ArrDom⦈"
    unfolding comp_Rel_components vdomain_vcomp_vsubset[OF assms(3)] 
    by (simp add: dg_Set_cs_simps)
qed

lemma arr_Set_comp_Set_ArrVal_app:
  assumes "arr_Set α S" 
    and "arr_Set α T" 
    and "x ∈∘ 𝒟∘ (T⦇ArrVal⦈)"
    and "T⦇ArrVal⦈⦇x⦈ ∈∘ 𝒟∘ (S⦇ArrVal⦈)"
  shows "(S ∘Set T)⦇ArrVal⦈⦇x⦈ = S⦇ArrVal⦈⦇T⦇ArrVal⦈⦇x⦈⦈"
proof-
  interpret S: arr_Set α S + T: arr_Set α T by (simp_all add: assms(1,2))  
  from assms show ?thesis 
    unfolding comp_Rel_components by (intro vcomp_atI) auto
qed


subsubsection‹Inclusion›

abbreviation (input) incl_Set :: "V ⇒ V ⇒ V"
  where "incl_Set ≡ incl_Rel"

lemma (in 𝒵) arr_Set_incl_SetI:
  assumes "A ∈∘ Vset α" and "B ∈∘ Vset α" and "A ⊆∘ B"
  shows "arr_Set α (incl_Set A B)"
proof(intro arr_Set_arr_ParI)
  from assms show "arr_Par α (incl_Set A B)" 
    by (force intro: arr_Par_incl_ParI)
qed (simp add: incl_Rel_components)


subsubsection‹Identity›

abbreviation (input) id_Set :: "V ⇒ V"
  where "id_Set ≡ id_Rel"

lemma (in 𝒵) arr_Set_id_SetI:
  assumes "A ∈∘ Vset α"
  shows "arr_Set α (id_Set A)"
proof(intro arr_Set_arr_ParI)
  from assms show "arr_Par α (id_Par A)" 
    by (force intro: arr_Par_id_ParI)
qed (simp add: id_Rel_components)

lemma arr_Set_comp_Set_id_Set_left[dg_Set_cs_simps]:
  assumes "arr_Set α F" and "F⦇ArrCod⦈ = A"
  shows "id_Set A ∘Set F = F"
proof-
  interpret F: arr_Set α F by (rule assms(1))
  have "arr_Rel α F" by (simp add: F.arr_Rel_axioms)
  from arr_Rel_comp_Rel_id_Rel_left[OF this assms(2)] show ?thesis.
qed

lemma arr_Set_comp_Set_id_Set_right[dg_Set_cs_simps]:
  assumes "arr_Set α F" and "F⦇ArrDom⦈ = A"
  shows "F ∘Set id_Set A = F"
proof-
  interpret F: arr_Set α F by (rule assms(1))
  have "arr_Rel α F" by (simp add: F.arr_Rel_axioms)
  from arr_Rel_comp_Rel_id_Rel_right[OF this assms(2)] show ?thesis.
qed



subsection‹‹Set› as a digraph›


subsubsection‹Definition and elementary properties›

definition dg_Set :: "V ⇒ V"
  where "dg_Set α =
    [
      Vset α,
      set {T. arr_Set α T},
      (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈),
      (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈)
    ]∘"


text‹Components.›

lemma dg_Set_components:
  shows "dg_Set α⦇Obj⦈ = Vset α"
    and "dg_Set α⦇Arr⦈ = set {T. arr_Set α T}"
    and "dg_Set α⦇Dom⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈)"
    and "dg_Set α⦇Cod⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈)"
  unfolding dg_Set_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object›

lemma dg_Set_Obj_iff: "x ∈∘ dg_Set α⦇Obj⦈ ⟷ x ∈∘ Vset α" 
  unfolding dg_Set_components by auto


subsubsection‹Arrow›

lemma dg_Set_Arr_iff[dg_Set_cs_simps]: "x ∈∘ dg_Set α⦇Arr⦈ ⟷ arr_Set α x" 
  unfolding dg_Set_components by auto


subsubsection‹Domain›

mk_VLambda dg_Set_components(3)
  |vsv dg_Set_Dom_vsv[dg_Set_cs_intros]|
  |vdomain dg_Set_Dom_vdomain[dg_Set_cs_simps]|
  |app dg_Set_Dom_app[unfolded set_Collect_arr_Set, dg_Set_cs_simps]|

lemma dg_Set_Dom_vrange: "ℛ∘ (dg_Set α⦇Dom⦈) ⊆∘ dg_Set α⦇Obj⦈"
  unfolding dg_Set_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Set) auto


subsubsection‹Codomain›

mk_VLambda dg_Set_components(4)
  |vsv dg_Set_Cod_vsv[dg_Set_cs_intros]|
  |vdomain dg_Set_Cod_vdomain[dg_Set_cs_simps]|
  |app dg_Set_Cod_app[unfolded set_Collect_arr_Set, dg_Set_cs_simps]|

lemma dg_Set_Cod_vrange: "ℛ∘ (dg_Set α⦇Cod⦈) ⊆∘ dg_Set α⦇Obj⦈"
  unfolding dg_Set_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Set) auto


subsubsection‹Arrow with a domain and a codomain›


text‹Rules.›

lemma dg_Set_is_arrI[dg_Set_cs_intros]:
  assumes "arr_Set α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  shows "S : A ↦⇘dg_Set α⇙ B"
  using assms by (intro is_arrI, unfold dg_Set_components) simp_all

lemma dg_Set_is_arrD:
  assumes "S : A ↦⇘dg_Set α⇙ B"
  shows "arr_Set α S" 
    and [dg_cs_simps]: "S⦇ArrDom⦈ = A" 
    and [dg_cs_simps]: "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Set_components by simp_all

lemma dg_Set_is_arrE:
  assumes "S : A ↦⇘dg_Set α⇙ B"
  obtains "arr_Set α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Set_components by simp_all

lemma dg_Set_ArrVal_vdomain[dg_Set_cs_simps, dg_cs_simps]:
  assumes "T : A ↦⇘dg_Set α⇙ B"
  shows "𝒟∘ (T⦇ArrVal⦈) = A"
proof-
  interpret T: arr_Set α T using assms by (auto simp: dg_Set_is_arrD)
  from assms show ?thesis by (auto simp: dg_Set_is_arrD dg_Set_cs_simps)
qed


text‹Elementary properties.›

lemma dg_Set_ArrVal_app_vrange[dg_Set_cs_intros]:
  assumes "F : A ↦⇘dg_Set α⇙ B" and "a ∈∘ A"
  shows "F⦇ArrVal⦈⦇a⦈ ∈∘ B"
proof-
  interpret F: arr_Set α F 
    rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
    by (intro dg_Set_is_arrD[OF assms(1)])+
  from assms F.arr_Par_ArrVal_vrange show ?thesis
    by (auto simp: F.ArrVal.vsv_vimageI2 vsubset_iff dg_Set_cs_simps)
qed

lemma dg_Set_is_arr_dg_Par_is_arr:
  assumes "T : A ↦⇘dg_Set α⇙ B" 
  shows "T : A ↦⇘dg_Par α⇙ B"
  using assms arr_Set_arr_ParD(1) 
  by (intro dg_Par_is_arrI; elim dg_Set_is_arrE) auto

lemma dg_Set_Hom_vsubset_dg_Par_Hom:
  assumes "a ∈∘ dg_Set α⦇Obj⦈" "b ∈∘ dg_Set α⦇Obj⦈" 
  shows "Hom (dg_Set α) a b ⊆∘ Hom (dg_Par α) a b"
  by (rule vsubsetI) (simp add: dg_Set_is_arr_dg_Par_is_arr)

lemma (in 𝒵) dg_Set_incl_Set_is_arr:
  assumes "A ∈∘ dg_Set α⦇Obj⦈" and "B ∈∘ dg_Set α⦇Obj⦈" and "A ⊆∘ B"
  shows "incl_Set A B : A ↦⇘dg_Set α⇙ B"
proof(rule dg_Set_is_arrI)
  from assms(1,2) show "arr_Set α (incl_Set A B)" 
    unfolding dg_Set_components(1) by (intro arr_Set_incl_SetI assms)
qed (simp_all add: dg_Set_components incl_Rel_components)

lemma (in 𝒵) dg_Set_incl_Set_is_arr'[dg_cs_intros, dg_Set_cs_intros]:
  assumes "A ∈∘ dg_Set α⦇Obj⦈" 
    and "B ∈∘ dg_Set α⦇Obj⦈" 
    and "A ⊆∘ B"
    and "A' = A"
    and "B' = B"
    and "ℭ' = dg_Set α"
  shows "incl_Set A B : A' ↦⇘ℭ'⇙ B'"
  using assms(1-3) unfolding assms(4-6) by (rule dg_Set_incl_Set_is_arr)

lemmas [dg_Set_cs_intros] = 𝒵.dg_Set_incl_Set_is_arr'


subsubsection‹‹Set› is a digraph›

lemma (in 𝒵) dg_Set_Hom_vifunion_in_Vset:
  assumes "X ∈∘ Vset α" and "Y ∈∘ Vset α"
  shows "(⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Set α) A B) ∈∘ Vset α"
proof-
  have 
    "(⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Set α) A B) ⊆∘
      (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Par α) A B)"
  proof
    fix F assume "F ∈∘ (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Set α) A B)"
    then obtain B where B: "B ∈∘ Y" and F_b: 
      "F ∈∘ (⋃∘A∈∘X. Hom (dg_Set α) A B)" 
      by fast
    then obtain A where A: "A ∈∘ X" and F_AB: "F ∈∘ Hom (dg_Set α) A B"
      by fast
    from A B assms have "A ∈∘ dg_Set α⦇Obj⦈" "B ∈∘ dg_Set α⦇Obj⦈"
      unfolding dg_Set_components by auto
    from F_AB A B dg_Set_Hom_vsubset_dg_Par_Hom[OF this] show 
      "F ∈∘ (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Par α) A B)"
      by (intro vifunionI) (auto elim!: vsubsetE simp: in_Hom_iff) 
  qed
  with dg_Par_Hom_vifunion_in_Vset[OF assms] show ?thesis by blast
qed

lemma (in 𝒵) digraph_dg_Set: "digraph α (dg_Set α)"
proof(intro digraphI)
  show "vfsequence (dg_Set α)" unfolding dg_Set_def by simp
  show "vcard (dg_Set α) = 4ℕ"
    unfolding dg_Set_def by (simp add: nat_omega_simps)
  show "ℛ∘ (dg_Set α⦇Dom⦈) ⊆∘ dg_Set α⦇Obj⦈" by (simp add: dg_Set_Dom_vrange)
  show "ℛ∘ (dg_Set α⦇Cod⦈) ⊆∘ dg_Set α⦇Obj⦈" by (simp add: dg_Set_Cod_vrange)
qed (auto simp: dg_Set_components dg_Set_Hom_vifunion_in_Vset)


subsubsection‹‹Set› is a wide subdigraph of ‹Par››

lemma (in 𝒵) wide_subdigraph_dg_Set_dg_Par: "dg_Set α ⊆DG.wide⇘α⇙ dg_Par α"
proof(intro wide_subdigraphI)
  interpret Set: digraph α ‹dg_Set α› by (rule digraph_dg_Set)
  interpret Par: digraph α ‹dg_Par α› by (rule digraph_dg_Par)
  show "dg_Set α ⊆DG⇘α⇙ dg_Par α"
  proof(intro subdigraphI, unfold dg_Set_components)
    show "F : A ↦⇘dg_Par α⇙ B" if "F : A ↦⇘dg_Set α⇙ B" for F A B
      using that by (rule dg_Set_is_arr_dg_Par_is_arr)
  qed (auto simp: dg_Par_components digraph_dg_Set digraph_dg_Par)
qed (simp_all add: dg_Par_components dg_Set_components)

text‹\newpage›

end