Theory CZH_ECAT_Discrete

(* Copyright 2021 (C) Mihails Milehins *)

section‹Discrete category›
theory CZH_ECAT_Discrete
  imports 
    CZH_ECAT_Simple
    CZH_ECAT_Small_Functor
begin



subsection‹Abstract discrete category›

named_theorems cat_discrete_cs_simps
named_theorems cat_discrete_cs_intros


subsubsection‹Definition and elementary properties›


text‹See Chapter I-2 in cite‹"mac_lane_categories_2010"›.›

locale cat_discrete = category α ℭ for α ℭ +
  assumes cat_discrete_Arr: "f ∈∘ ℭ⦇Arr⦈ ⟹ f ∈∘ ℛ∘ (ℭ⦇CId⦈)"


text‹Rules.›

lemma (in cat_discrete)
  assumes "α' = α" "ℭ' = ℭ"
  shows "cat_discrete α' ℭ'"
  unfolding assms by (rule cat_discrete_axioms)

mk_ide rf cat_discrete_def[unfolded cat_discrete_axioms_def]
  |intro cat_discreteI|
  |dest cat_discreteD[dest]|
  |elim cat_discreteE[elim]|

lemmas [cat_discrete_cs_intros] = cat_discreteD(1)


text‹Elementary properties.›

lemma (in cat_discrete) cat_discrete_is_arrD[dest]:
  assumes "f : a ↦⇘ℭ⇙ b"
  shows "b = a" and "f = ℭ⦇CId⦈⦇a⦈"
proof-
  from assms cat_discrete_Arr have "f ∈∘ ℛ∘ (ℭ⦇CId⦈)" 
    by (auto simp: cat_cs_simps)
  with cat_CId_vdomain obtain a' where f_def: "f = ℭ⦇CId⦈⦇a'⦈" and "a' ∈∘ ℭ⦇Obj⦈" 
    by (blast dest: CId.vrange_atD)
  then have "f : a' ↦⇘ℭ⇙ a'" by (auto intro: cat_CId_is_arr')
  with assms have "a = a'" and "b = a'" by blast+
  with f_def show "b = a" and "f = ℭ⦇CId⦈⦇a⦈" by auto
qed

lemma (in cat_discrete) cat_discrete_is_arrE[elim]:
  assumes "f : b ↦⇘ℭ⇙ c"
  obtains a where "f : a ↦⇘ℭ⇙ a" and "f = ℭ⦇CId⦈⦇a⦈"
  using assms by auto



subsection‹The discrete category›

text‹
As explained in Chapter I-2 in cite‹"mac_lane_categories_2010"›, every discrete
category is identified with its set of objects. 
In this work, it is assumed that the set of objects and the set of arrows
in the canonical discrete category coincide; the domain and the codomain 
functions are identities.
›


subsubsection‹Definition and elementary properties›

definition the_cat_discrete :: "V ⇒ V" (‹:C›)
  where ":C I = [I, I, vid_on I, vid_on I, (λfg∈∘fid_on I. fg⦇0⦈), vid_on I]∘"


text‹Components.›

lemma the_cat_discrete_components:
  shows ":C I⦇Obj⦈ = I"
    and ":C I⦇Arr⦈ = I"
    and ":C I⦇Dom⦈ = vid_on I"
    and ":C I⦇Cod⦈ = vid_on I"
    and ":C I⦇Comp⦈ = (λfg∈∘fid_on I. fg⦇0⦈)"
    and ":C I⦇CId⦈ = vid_on I"
  unfolding the_cat_discrete_def dg_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Domain›

mk_VLambda the_cat_discrete_components(3)[folded VLambda_vid_on]
  |vsv the_cat_discrete_Dom_vsv[cat_discrete_cs_intros]|
  |vdomain the_cat_discrete_Dom_vdomain[cat_discrete_cs_simps]|
  |app the_cat_discrete_Dom_app[cat_discrete_cs_simps]|


subsubsection‹Codomain›

mk_VLambda the_cat_discrete_components(4)[folded VLambda_vid_on]
  |vsv the_cat_discrete_Cod_vsv[cat_discrete_cs_intros]|
  |vdomain the_cat_discrete_Cod_vdomain[cat_discrete_cs_simps]|
  |app the_cat_discrete_Cod_app[cat_discrete_cs_simps]|


subsubsection‹Composition›

lemma the_cat_discrete_Comp_vsv[cat_discrete_cs_intros]: "vsv (:C I⦇Comp⦈)"
  unfolding the_cat_discrete_components by simp

lemma the_cat_discrete_Comp_vdomain: "𝒟∘ (:C I⦇Comp⦈) = fid_on I"
  unfolding the_cat_discrete_components by simp

lemma the_cat_discrete_Comp_vrange: 
  "ℛ∘ (:C I⦇Comp⦈) = I"
proof(intro vsubset_antisym vsubsetI)
  fix f assume "f ∈∘ ℛ∘ (:C I⦇Comp⦈)"
  then obtain gg where f_def: "f = :C I⦇Comp⦈⦇gg⦈" and gg: "gg ∈∘ fid_on I"
    unfolding the_cat_discrete_components by auto
  from gg show "f ∈∘ I"
    unfolding f_def the_cat_discrete_components by clarsimp
next
  fix f assume "f ∈∘ I"
  then have "[f, f]∘ ∈∘ fid_on I" by clarsimp
  moreover then have "f = :C I⦇Comp⦈⦇f, f⦈∙"
    unfolding the_cat_discrete_components by simp
  ultimately show "f ∈∘ ℛ∘ (:C I⦇Comp⦈)"
    unfolding the_cat_discrete_components
    by (metis rel_VLambda.vsv_vimageI2 vdomain_VLambda)
qed
 
lemma the_cat_discrete_Comp_app[cat_discrete_cs_simps]: 
  assumes "i ∈∘ I"
  shows "i ∘A⇘:C I⇙ i = i"
proof-
  from assms have "[i, i]∘ ∈∘ fid_on I" by clarsimp
  then show ?thesis unfolding the_cat_discrete_components by simp
qed


subsubsection‹Identity›

mk_VLambda the_cat_discrete_components(6)[folded VLambda_vid_on]
  |vsv the_cat_discrete_CId_vsv[cat_discrete_cs_intros]|
  |vdomain the_cat_discrete_CId_vdomain[cat_discrete_cs_simps]|
  |app the_cat_discrete_CId_app[cat_discrete_cs_simps]|


subsubsection‹Arrow with a domain and a codomain›

lemma the_cat_discrete_is_arrI:
  assumes "i ∈∘ I"
  shows "i : i ↦⇘:C I⇙ i"
  using assms unfolding is_arr_def the_cat_discrete_components by simp

lemma the_cat_discrete_is_arrI'[cat_discrete_cs_intros]:
  assumes "i ∈∘ I"
    and "a = i"
    and "b = i"
  shows "i : a ↦⇘:C I⇙ b"
  using assms(1) unfolding assms(2,3) by (rule the_cat_discrete_is_arrI)

lemma the_cat_discrete_is_arrD:
  assumes "f : a ↦⇘:C I⇙ b"
  shows "f : f ↦⇘:C I⇙ f"
    and "a : a ↦⇘:C I⇙ a" 
    and "b : b ↦⇘:C I⇙ b"
    and "f ∈∘ I"
    and "a ∈∘ I"
    and "b ∈∘ I"
    and "f = a"
    and "f = b"
    and "b = a"
  using assms unfolding is_arr_def the_cat_discrete_components by force+


subsubsection‹The discrete category is a discrete category›

lemma (in 𝒵) cat_discrete_the_cat_discrete:
  assumes "I ⊆∘ Vset α"
  shows "cat_discrete α (:C I)"
proof(intro cat_discreteI categoryI')
  show "vfsequence (:C I)" unfolding the_cat_discrete_def by simp
  show "vcard (:C I) = 6ℕ"
    unfolding the_cat_discrete_def by (simp add: nat_omega_simps)
  show "gf ∈∘ 𝒟∘ (:C I⦇Comp⦈) ⟷ 
    (∃g f b c a. gf = [g, f]∘ ∧ g : b ↦⇘:C I⇙ c ∧ f : a ↦⇘:C I⇙ b)"
    for gf
    unfolding the_cat_discrete_Comp_vdomain
  proof
    assume "gf ∈∘ fid_on I"
    then obtain a where "gf = [a, a]∘" and "a ∈∘ I" by clarsimp
    moreover then have "a : a ↦⇘:C I⇙ a" 
      by (auto intro: the_cat_discrete_is_arrI)
    ultimately show 
      "∃g f b c a. gf = [g, f]∘ ∧ g : b ↦⇘:C I⇙ c ∧ f : a ↦⇘:C I⇙ b"
      by auto 
  next
    assume "∃g f b c a. gf = [g, f]∘ ∧ g : b ↦⇘:C I⇙ c ∧ f : a ↦⇘:C I⇙ b"
    then obtain g f b c a where gf_def: "gf = [g, f]∘"  
      and g: "g : b ↦⇘:C I⇙ c"
      and f: "f : a ↦⇘:C I⇙ b"
      by clarsimp
    then have "g = f" by (metis is_arrE the_cat_discrete_is_arrD(1))
    with the_cat_discrete_is_arrD(4)[OF f] show "gf ∈∘ fid_on I"
      unfolding gf_def by clarsimp
  qed
  show "g ∘A⇘:C I⇙ f : a ↦⇘:C I⇙ c" if "g : b ↦⇘:C I⇙ c" and "f : a ↦⇘:C I⇙ b"
    for g b c f a
  proof-
    from that have fba: "f = a" "b = a" and a: "a ∈∘ I" 
      unfolding the_cat_discrete_is_arrD[OF that(2)] by (simp_all add: ‹a ∈∘ I›)
    from that have gcb: "g = b" "c = b"
      unfolding the_cat_discrete_is_arrD[OF that(1)] by simp_all
    from a show ?thesis
      unfolding fba gcb  
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_discrete_cs_simps cs_intro: cat_discrete_cs_intros
        )
  qed
  show "h ∘A⇘:C I⇙ g ∘A⇘:C I⇙ f = h ∘A⇘:C I⇙ (g ∘A⇘:C I⇙ f)"
    if "h : c ↦⇘:C I⇙ d" and "g : b ↦⇘:C I⇙ c" and "f : a ↦⇘:C I⇙ b"
    for h c d g b f a
  proof-
    from that have fba: "f = a" "b = a" and a: "a ∈∘ I" 
      unfolding the_cat_discrete_is_arrD[OF that(3)] by (simp_all add: ‹a ∈∘ I›)
    from that have gcb: "g = b" "c = b" 
      unfolding the_cat_discrete_is_arrD[OF that(2)] by simp_all
    from that have hcd: "h = c" "d = c"
      unfolding the_cat_discrete_is_arrD[OF that(1)] by simp_all
    from a show ?thesis
      unfolding fba gcb hcd 
      by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps)
  qed
  show ":C I⦇CId⦈⦇b⦈ ∘A⇘:C I⇙ f = f" if "f : a ↦⇘:C I⇙ b" for f a b
  proof-
    from that have fba: "f = a" "b = a" and a: "a ∈∘ I" 
      unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹a ∈∘ I›)
    from a show ?thesis 
      by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps fba)
  qed
  show "f ∘A⇘:C I⇙ :C I⦇CId⦈⦇b⦈ = f" if "f : b ↦⇘:C I⇙ c" for f b c
  proof-
    from that have fba: "f = b" "c = b" and b: "b ∈∘ I" 
      unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹b ∈∘ I›)
    from b show ?thesis 
      by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps fba)
  qed
  show ":C I⦇CId⦈⦇a⦈ : a ↦⇘:C I⇙ a"
    if "a ∈∘ :C I⦇Obj⦈" for a 
    using that 
    by (auto simp: the_cat_discrete_components intro: cat_discrete_cs_intros)
  show "⋃∘((λa∈∘A. ⋃∘(VLambda B (Hom (:C I) a) `∘ B)) `∘ A) ∈∘ Vset α"
    if "A ⊆∘ :C I⦇Obj⦈"
      and "B ⊆∘ :C I⦇Obj⦈"
      and "A ∈∘ Vset α"
      and "B ∈∘ Vset α"
    for A B
  proof-
    have "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (:C I) a b) ⊆∘ A ∪∘ B"
    proof(intro vsubsetI, elim vifunionE, unfold in_Hom_iff)
      fix i j f assume prems: "i ∈∘ A" "j ∈∘ B" "f : i ↦⇘:C I⇙ j"
      then show "f ∈∘ A ∪∘ B" 
        unfolding the_cat_discrete_is_arrD[OF prems(3)] by simp
    qed
    moreover have "A ∪∘ B ∈∘ Vset α" by (simp add: that(3,4) vunion_in_VsetI)
    ultimately show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (:C I) a b) ∈∘ Vset α"
      by (auto simp: vsubset_in_VsetI)
  qed
qed (auto simp: assms the_cat_discrete_components intro: cat_cs_intros)

lemmas [cat_discrete_cs_intros] = 𝒵.cat_discrete_the_cat_discrete


subsubsection‹Opposite discrete category›

lemma (in 𝒵) the_cat_discrete_op[cat_op_simps]:
  assumes "I ⊆∘ Vset α"
  shows "op_cat (:C I) = :C I"
proof(rule cat_eqI[of α])
  from assms show dI: "category α (:C I)"
    by (cs_concl cs_intro: cat_discrete_the_cat_discrete cat_discrete_cs_intros)
  then show op_dI: "category α (op_cat (:C I))"
    by (cs_concl cs_shallow cs_intro: cat_op_intros)
  interpret category α ‹op_cat (:C I)› by (rule op_dI)
  show "op_cat (:C I)⦇Comp⦈ = :C I⦇Comp⦈"
  proof(rule vsv_eqI)
    show "𝒟∘ (op_cat (:C I)⦇Comp⦈) = 𝒟∘ (:C I⦇Comp⦈)"
      by (simp add: the_cat_discrete_components op_cat_components)
    fix gf assume "gf ∈∘ 𝒟∘ (op_cat (:C I)⦇Comp⦈)"
    then have "gf ∈∘ fid_on I" 
      by (simp add: the_cat_discrete_components op_cat_components)
    then obtain h where gf_def: "gf = [h, h]∘" and h: "h ∈∘ I" by clarsimp
    from dI h show "op_cat (:C I)⦇Comp⦈⦇gf⦈ = :C I⦇Comp⦈⦇gf⦈" 
      by 
        ( 
          cs_concl cs_shallow
            cs_simp: cat_op_simps gf_def cs_intro: cat_discrete_cs_intros
        )
  qed (auto intro: cat_discrete_cs_intros)
qed (unfold the_cat_discrete_components op_cat_components, simp_all)



subsection‹Discrete functor›


subsubsection‹Local assumptions for the discrete functor›


text‹See Chapter III in cite‹"mac_lane_categories_2010"›).›

locale cf_discrete = category α ℭ for α I F ℭ +
  assumes cf_discrete_selector_vrange[cat_discrete_cs_intros]: 
    "i ∈∘ I ⟹ F i ∈∘ ℭ⦇Obj⦈"
    and cf_discrete_vdomain_vsubset_Vset: "I ⊆∘ Vset α"

lemmas (in cf_discrete) cf_discrete_category = category_axioms

lemmas [cat_discrete_cs_intros] = cf_discrete.cf_discrete_category


text‹Rules.›

lemma (in cf_discrete) cf_discrete_axioms'[cat_discrete_cs_intros]:
  assumes "α' = α" and "I' = I" and "F' = F" 
  shows "cf_discrete α' I' F' ℭ"
  unfolding assms by (rule cf_discrete_axioms)

mk_ide rf cf_discrete_def[unfolded cf_discrete_axioms_def]
  |intro cf_discreteI|
  |dest cf_discreteD[dest]|
  |elim cf_discreteE[elim]|


text‹Elementary properties.›

lemma (in cf_discrete) cf_discrete_is_functor_cf_CId_selector_is_arr: 
  assumes "i ∈∘ I"
  shows "ℭ⦇CId⦈⦇F i⦈ : F i ↦⇘ℭ⇙ F i"
  using assms by (meson cat_CId_is_arr' cf_discreteD(2) cf_discrete_axioms)

lemma (in cf_discrete) 
  cf_discrete_is_functor_cf_CId_selector_is_arr'[cat_discrete_cs_intros]: 
  assumes "i ∈∘ I" and "a = F i" and "b = F i"
  shows "ℭ⦇CId⦈⦇F i⦈ : a ↦⇘ℭ⇙ b"
  using assms(1)
  unfolding assms(2,3) 
  by (rule cf_discrete_is_functor_cf_CId_selector_is_arr)


subsubsection‹Definition and elementary properties›

definition the_cf_discrete :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V" (‹:→:›)
  where ":→: I F ℭ = [VLambda I F, (λi∈∘I. ℭ⦇CId⦈⦇F i⦈), :C I, ℭ]∘"


text‹Components.›

lemma the_cf_discrete_components:
  shows ":→: I F ℭ⦇ObjMap⦈ = (λi∈∘I. F i)"
    and ":→: I F ℭ⦇ArrMap⦈ = (λi∈∘I. ℭ⦇CId⦈⦇F i⦈)"
    and [cat_discrete_cs_simps]: ":→: I F ℭ⦇HomDom⦈ = :C I"
    and [cat_discrete_cs_simps]: ":→: I F ℭ⦇HomCod⦈ = ℭ"
  unfolding the_cf_discrete_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda the_cf_discrete_components(1)
  |vsv the_cf_discrete_ObjMap_vsv[cat_discrete_cs_intros]|
  |vdomain the_cf_discrete_ObjMap_vdomain[cat_discrete_cs_simps]|
  |app the_cf_discrete_ObjMap_app[cat_discrete_cs_simps]|

lemma (in cf_discrete) cf_discrete_the_cf_discrete_ObjMap_vrange: 
  "ℛ∘ (:→: I F ℭ⦇ObjMap⦈) ⊆∘ ℭ⦇Obj⦈"
  using cf_discrete_is_functor_cf_CId_selector_is_arr
  unfolding the_cf_discrete_components
  by (intro vrange_VLambda_vsubset) auto


subsubsection‹Arrow map›

mk_VLambda the_cf_discrete_components(2)
  |vsv the_cf_discrete_ArrMap_vsv[cat_discrete_cs_intros]|
  |vdomain the_cf_discrete_ArrMap_vdomain[cat_discrete_cs_simps]|
  |app the_cf_discrete_ArrMap_app[cat_discrete_cs_simps]|

lemma (in cf_discrete) cf_discrete_the_cf_discrete_ArrMap_vrange: 
  "ℛ∘ (:→: I F ℭ⦇ArrMap⦈) ⊆∘ ℭ⦇Arr⦈"
  using cf_discrete_is_functor_cf_CId_selector_is_arr
  unfolding the_cf_discrete_components
  by (intro vrange_VLambda_vsubset) (auto simp: cf_discrete_selector_vrange)


subsubsection‹Discrete functor is a functor›

lemma (in cf_discrete) cf_discrete_the_cf_discrete_is_functor:  
  ":→: I F ℭ : :C I ↦↦C⇘α⇙ ℭ"
proof(intro is_functorI')
  show "vfsequence (:→: I F ℭ)" unfolding the_cf_discrete_def by simp
  show "category α (:C I)"
    by 
      (
        simp add:
          cat_discrete_the_cat_discrete 
          cf_discrete_vdomain_vsubset_Vset 
          cat_discrete.axioms(1)
      )  
  show "vcard (:→: I F ℭ) = 4ℕ"
    unfolding the_cf_discrete_def by (simp add: nat_omega_simps)
  show 
    ":→: I F ℭ⦇ArrMap⦈⦇f⦈ : :→: I F ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ :→: I F ℭ⦇ObjMap⦈⦇b⦈"
    if "f : a ↦⇘:C I⇙ b" for f a b
  proof-
    from that have fba: "f = a" "b = a" and a: "a ∈∘ I" 
      unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹a ∈∘ I›)
    from that ‹a ∈∘ I› show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_discrete_cs_simps fba cs_intro: cat_discrete_cs_intros
        )
  qed
  show ":→: I F ℭ⦇ArrMap⦈⦇g ∘A⇘:C I⇙ f⦈ = 
    :→: I F ℭ⦇ArrMap⦈⦇g⦈ ∘A⇘ℭ⇙ :→: I F ℭ⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘:C I⇙ c" and "f : a ↦⇘:C I⇙ b" for g b c f a
  proof-
    from that have gfacb: "f = a" "a = b" "g = b" "c = b" and b: "b ∈∘ I"  
      by 
        (
          simp_all add: 
            the_cat_discrete_is_arrD(8-9)[OF that(1)] 
            the_cat_discrete_is_arrD(5-9)[OF that(2)]
        )
    have "F b ∈∘ ℭ⦇Obj⦈" by (simp add: b cf_discrete_selector_vrange)
    from b category_axioms this show ?thesis
      using that 
      unfolding gfacb
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_discrete_cs_simps cs_intro: cat_cs_intros
        )
  qed
  show ":→: I F ℭ⦇ArrMap⦈⦇:C I⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇:→: I F ℭ⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈∘ :C I⦇Obj⦈" for c
    using that
    unfolding the_cat_discrete_components(1)
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_discrete_cs_simps cs_intro: cat_cs_intros
      )
qed 
  (
    auto simp: 
      the_cf_discrete_components 
      the_cat_discrete_components 
      cat_cs_intros
      cat_discrete_cs_intros
  ) 

lemma (in cf_discrete) cf_discrete_the_cf_discrete_is_functor':
  assumes "𝔄' = :C I" and "ℭ' = ℭ"
  shows ":→: I F ℭ : 𝔄' ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule cf_discrete_the_cf_discrete_is_functor)

lemmas [cat_discrete_cs_intros] = 
  cf_discrete.cf_discrete_the_cf_discrete_is_functor'


subsubsection‹Uniqueness of the discrete category›

lemma (in cat_discrete) cat_discrete_iso_the_cat_discrete:
  assumes "I ⊆∘ Vset α" and "I ≈∘ ℭ⦇Obj⦈"
  obtains F where ":→: I F ℭ : :C I ↦↦C.iso⇘α⇙ ℭ"
proof-

  from assms obtain F where v11_f: "v11 F" 
    and dr[simp]: "𝒟∘ F = I" "ℛ∘ F = ℭ⦇Obj⦈" 
    by auto
  let ?F = "λi. F⦇i⦈"
  interpret F: v11 F by (rule v11_f)
  from assms(1) interpret ℭ: cf_discrete α I ?F ℭ 
    apply(intro cf_discreteI) 
    unfolding dr[symmetric] 
    by (cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros)+
  have ":→: I ?F ℭ : :C I ↦↦C.iso⇘α⇙ ℭ"
  proof(intro is_iso_functorI')
    from ℭ.cf_discrete_selector_vrange show  
      ":→: I ?F ℭ : :C I ↦↦C⇘α⇙ ℭ" 
      by (intro cf_discrete.cf_discrete_the_cf_discrete_is_functor cf_discreteI)
        (auto simp: category_axioms assms(1))
    show "v11 (:→: I ?F ℭ⦇ArrMap⦈)"
    proof(rule vsv.vsv_valeq_v11I, unfold the_cf_discrete_ArrMap_vdomain)
      fix i j assume prems:
        "i ∈∘ I" "j ∈∘ I" ":→: I ?F ℭ⦇ArrMap⦈⦇i⦈ = :→: I ?F ℭ⦇ArrMap⦈⦇j⦈"
      from prems(3) have "ℭ⦇CId⦈⦇?F i⦈ = ℭ⦇CId⦈⦇?F j⦈"
        unfolding 
          the_cf_discrete_ArrMap_app[OF prems(1)]
          the_cf_discrete_ArrMap_app[OF prems(2)].
      then have "?F i = ?F j"
        by 
          (
            metis 
              ℭ.cf_discrete_is_functor_cf_CId_selector_is_arr 
              prems(1,2) 
              cat_is_arrD(4)
          )
      with F.v11_eq_iff prems show "i = j" by simp
    qed (simp add: the_cf_discrete_components)
    show "ℛ∘ (:→: I ?F ℭ⦇ArrMap⦈) = ℭ⦇Arr⦈"
    proof(intro vsubset_antisym vsubsetI)
      fix f assume "f ∈∘ ℛ∘ (:→: I ?F ℭ⦇ArrMap⦈)"
      with ℭ.cf_discrete_the_cf_discrete_ArrMap_vrange show "f ∈∘ ℭ⦇Arr⦈" 
        by auto
    next
      fix f assume "f ∈∘ ℭ⦇Arr⦈"
      then obtain a b where "f : a ↦⇘ℭ⇙ b" by auto
      then obtain a where f_def: "f = ℭ⦇CId⦈⦇a⦈" and a: "a ∈∘ ℭ⦇Obj⦈" by auto
      from a F.vrange_atD dr obtain i where a_def: "a = ?F i" and i: "i ∈∘ I"
        by blast
      from a i show "f ∈∘ ℛ∘ (:→: I ?F ℭ⦇ArrMap⦈)"
        unfolding a_def f_def the_cf_discrete_components by auto
    qed
  qed (auto simp: v11_f the_cf_discrete_components)
  with that show ?thesis by simp

qed


subsubsection‹Opposite discrete functor›

lemma (in cf_discrete) cf_discrete_the_cf_discrete_op[cat_op_simps]:
  "op_cf (:→: I F ℭ) = :→: I F (op_cat ℭ)"
proof(rule cf_eqI)
  from cf_discrete_vdomain_vsubset_Vset show 
    "op_cf (:→: I F ℭ) : :C I ↦↦C⇘α⇙ op_cat ℭ"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_op_simps cs_intro: cat_op_intros cat_discrete_cs_intros
      )
  show ":→: I F (op_cat ℭ) : :C I ↦↦C⇘α⇙ op_cat ℭ"
  proof(intro cf_discrete.cf_discrete_the_cf_discrete_is_functor cf_discreteI)
    fix i assume "i ∈∘ I"
    then show "F i ∈∘ op_cat ℭ⦇Obj⦈"
      by (simp add: cat_op_simps cf_discrete_selector_vrange)
  qed (intro cf_discrete_vdomain_vsubset_Vset cat_cs_intros)+
qed (unfold cat_op_simps the_cf_discrete_components, simp_all)

lemmas [cat_op_simps] = cf_discrete.cf_discrete_the_cf_discrete_op

lemma (in cf_discrete) cf_discrete_op[cat_op_intros]: 
  "cf_discrete α I F (op_cat ℭ)"
proof(intro cf_discreteI)
  show "category α (op_cat ℭ)" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  fix i assume "i ∈∘ I"
  then show "F i ∈∘ op_cat ℭ⦇Obj⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_discrete_cs_intros
      )
qed (intro cf_discrete_vdomain_vsubset_Vset)

lemmas [cat_op_intros] = cf_discrete.cf_discrete_op



subsection‹Tiny discrete category›


subsubsection‹Background›

named_theorems cat_small_discrete_cs_simps
named_theorems cat_small_discrete_cs_intros

lemmas [cat_small_discrete_cs_simps] = cat_discrete_cs_simps
lemmas [cat_small_discrete_cs_intros] = cat_discrete_cs_intros


subsubsection‹Definition and elementary properties›

locale tiny_cat_discrete = cat_discrete α ℭ + tiny_category α ℭ for α ℭ


text‹Rules.›

lemma (in tiny_cat_discrete) tiny_cat_discrete_axioms'[cat_discrete_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ"
  shows "tiny_cat_discrete α' ℭ'"
  unfolding assms by (rule tiny_cat_discrete_axioms)

mk_ide rf tiny_cat_discrete_def
  |intro tiny_cat_discreteI|
  |dest tiny_cat_discreteD[dest]|
  |elim tiny_cat_discreteE[elim]|

lemmas [cat_small_discrete_cs_intros] = tiny_cat_discreteD

lemma tiny_cat_discreteI':
  assumes "tiny_category α ℭ" and "⋀f. f ∈∘ ℭ⦇Arr⦈ ⟹ f ∈∘ ℛ∘ (ℭ⦇CId⦈)"
  shows "tiny_cat_discrete α ℭ"
proof(intro tiny_cat_discreteI cat_discreteI)
  interpret tiny_category α ℭ by (rule assms(1))
  show "category α ℭ" by (auto intro: tiny_cat_category)
  show "f ∈∘ ℛ∘ (ℭ⦇CId⦈)" if "f ∈∘ ℭ⦇Arr⦈" for f using that by (rule assms(2))
qed (auto intro: assms(1))


subsubsection‹The discrete category is a tiny category›

lemma (in 𝒵) tiny_cat_discrete_the_cat_discrete[cat_small_discrete_cs_intros]:
  assumes "I ∈∘ Vset α"
  shows "tiny_cat_discrete α (:C I)"
proof(intro tiny_cat_discreteI cat_discrete_the_cat_discrete)
  from assms show "I ⊆∘ Vset α" by auto
  then interpret cat_discrete α ‹:C I› by (intro cat_discrete_the_cat_discrete)
  show "tiny_category α (:C I)"
    by (intro tiny_categoryI', unfold the_cat_discrete_components)
      (auto intro: cat_cs_intros assms)
qed

lemmas [cat_small_discrete_cs_intros] = 𝒵.cat_discrete_the_cat_discrete



subsection‹Discrete functor with tiny maps›


subsubsection‹Definition and elementary properties›

locale tm_cf_discrete = category α ℭ for α I F ℭ +
  assumes tm_cf_discrete_selector_vrange[cat_small_discrete_cs_intros]: 
    "i ∈∘ I ⟹ F i ∈∘ ℭ⦇Obj⦈"
    and tm_cf_discrete_ObjMap_in_Vset: "VLambda I F ∈∘ Vset α"
    and tm_cf_discrete_ArrMap_in_Vset: "(λi∈∘I. ℭ⦇CId⦈⦇F i⦈) ∈∘ Vset α"


text‹Rules.›

lemma (in tm_cf_discrete) tm_cf_discrete_axioms'[cat_small_discrete_cs_intros]:
  assumes "α' = α" and "I' = I" and "F' = F" 
  shows "tm_cf_discrete α' I' F' ℭ"
  unfolding assms by (rule tm_cf_discrete_axioms)

mk_ide rf tm_cf_discrete_def[unfolded tm_cf_discrete_axioms_def]
  |intro tm_cf_discreteI|
  |dest tm_cf_discreteD[dest]|
  |elim tm_cf_discreteE[elim]|

lemma tm_cf_discreteI': 
  assumes "cf_discrete α I F ℭ"
    and "(λi∈∘I. F i) ∈∘ Vset α"
    and "(λi∈∘I. ℭ⦇CId⦈⦇F i⦈) ∈∘ Vset α"
  shows "tm_cf_discrete α I F ℭ"
proof-
  interpret cf_discrete α I F ℭ by (rule assms(1))
  show ?thesis
    by (intro tm_cf_discreteI)
      (auto intro: assms cf_discrete_selector_vrange cat_cs_intros)
qed


text‹Elementary properties.›

sublocale tm_cf_discrete ⊆ cf_discrete
proof(intro cf_discreteI)
  from tm_cf_discrete_ObjMap_in_Vset have "𝒟∘ (λi∈∘I. F i) ∈∘ Vset α"
    by (cs_concl cs_shallow cs_intro: vdomain_in_VsetI)
  then show "I ⊆∘ Vset α" by auto
qed (auto intro: cat_cs_intros tm_cf_discrete_selector_vrange)

lemmas (in tm_cf_discrete) tm_cf_discrete_is_cf_discrete_axioms = 
  cf_discrete_axioms

lemmas [cat_small_discrete_cs_intros] = 
  tm_cf_discrete.tm_cf_discrete_is_cf_discrete_axioms

lemma (in tm_cf_discrete) 
  tm_cf_discrete_index_in_Vset[cat_small_discrete_cs_intros]: 
  "I ∈∘ Vset α"
proof-
  from tm_cf_discrete_ObjMap_in_Vset have "𝒟∘ (λi∈∘I. F i) ∈∘ Vset α"
    by (cs_concl cs_shallow cs_intro: vdomain_in_VsetI)
  then show ?thesis by simp
qed


subsubsection‹Opposite discrete functor with tiny maps›

lemma (in tm_cf_discrete) tm_cf_discrete_op[cat_op_intros]: 
  "tm_cf_discrete α I F (op_cat ℭ)"
  using tm_cf_discrete_ObjMap_in_Vset tm_cf_discrete_ArrMap_in_Vset 
  by (intro tm_cf_discreteI' cf_discrete_op) (auto simp: cat_op_simps)

lemmas [cat_op_intros] = tm_cf_discrete.tm_cf_discrete_op


subsubsection‹Discrete functor with tiny maps is a functor with tiny maps›

lemma (in tm_cf_discrete) tm_cf_discrete_the_cf_discrete_is_tm_functor: 
  ":→: I F ℭ : :C I ↦↦C.tm⇘α⇙ ℭ"
  by (intro is_tm_functorI' cf_discrete_the_cf_discrete_is_functor)
    (
      auto simp: 
        the_cf_discrete_components 
        tm_cf_discrete_ObjMap_in_Vset 
        tm_cf_discrete_ArrMap_in_Vset
    )

lemma (in tm_cf_discrete) tm_cf_discrete_the_cf_discrete_is_tm_functor':
  assumes "𝔄' = :C I" and "ℭ' = ℭ"
  shows ":→: I F ℭ : 𝔄' ↦↦C.tm⇘α⇙ ℭ'"
  unfolding assms by (rule tm_cf_discrete_the_cf_discrete_is_tm_functor)

lemmas [cat_discrete_cs_intros] = 
  tm_cf_discrete.tm_cf_discrete_the_cf_discrete_is_tm_functor'

text‹\newpage›

end