Theory CZH_ECAT_Subcategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Subcategory›
theory CZH_ECAT_Subcategory
  imports 
    CZH_ECAT_Functor
    CZH_Foundations.CZH_SMC_Subsemicategory
begin



subsection‹Background›

named_theorems cat_sub_cs_intros
named_theorems cat_sub_bw_cs_intros
named_theorems cat_sub_fw_cs_intros
named_theorems cat_sub_bw_cs_simps



subsection‹Simple subcategory›


subsubsection‹Definition and elementary properties›


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

locale subcategory = sdg: category α 𝔅 + dg: category α ℭ for α 𝔅 ℭ  +
  assumes subcat_subsemicategory: "cat_smc 𝔅 ⊆⇩S⇩M⇩C⇘α⇙ cat_smc ℭ" 
    and subcat_CId: "a ∈⇩∘ 𝔅⦇Obj⦈ ⟹ 𝔅⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈"

abbreviation is_subcategory ("(_/ ⊆⇩Cı _)" [51, 51] 50)
  where "𝔅 ⊆⇩C⇘α⇙ ℭ ≡ subcategory α 𝔅 ℭ"


text‹Rules.›

lemma (in subcategory) subcategory_axioms'[cat_cs_intros]:
  assumes "α' = α" and "𝔅' = 𝔅"
  shows "𝔅' ⊆⇩C⇘α'⇙ ℭ"
  unfolding assms by (rule subcategory_axioms)

lemma (in subcategory) subcategory_axioms''[cat_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ"
  shows "𝔅 ⊆⇩C⇘α'⇙ ℭ'"
  unfolding assms by (rule subcategory_axioms)

mk_ide rf subcategory_def[unfolded subcategory_axioms_def]
  |intro subcategoryI[intro!]|
  |dest subcategoryD[dest]|
  |elim subcategoryE[elim!]|

lemmas [cat_sub_cs_intros] = subcategoryD(1,2)

lemma subcategoryI':
  assumes "category α 𝔅"
    and "category α ℭ"
    and "⋀a. a ∈⇩∘ 𝔅⦇Obj⦈ ⟹ a ∈⇩∘ ℭ⦇Obj⦈"
    and "⋀a b f. f : a ↦⇘𝔅⇙ b ⟹ f : a ↦⇘ℭ⇙ b"
    and "⋀b c g a f. ⟦ g : b ↦⇘𝔅⇙ c; f : a ↦⇘𝔅⇙ b ⟧ ⟹
      g ∘⇩A⇘𝔅⇙ f = g ∘⇩A⇘ℭ⇙ f"
    and "⋀a. a ∈⇩∘ 𝔅⦇Obj⦈ ⟹ 𝔅⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈"
  shows "𝔅 ⊆⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔅: category α 𝔅 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))  
  show ?thesis
    by 
      (
        intro subcategoryI subsemicategoryI', 
        unfold slicing_simps; 
        (intro 𝔅.cat_semicategory ℭ.cat_semicategory assms)?
      )
qed


text‹A subcategory is a subsemicategory.›

context subcategory
begin

interpretation subsmc: subsemicategory α ‹cat_smc 𝔅› ‹cat_smc ℭ›
  by (rule subcat_subsemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
  subcat_Obj_vsubset = subsmc.subsmc_Obj_vsubset
  and subcat_is_arr_vsubset = subsmc.subsmc_is_arr_vsubset
  and subcat_subdigraph_op_dg_op_dg = subsmc.subsmc_subdigraph_op_dg_op_dg
  and subcat_objD = subsmc.subsmc_objD
  and subcat_arrD = subsmc.subsmc_arrD
  and subcat_dom_simp = subsmc.subsmc_dom_simp
  and subcat_cod_simp = subsmc.subsmc_cod_simp
  and subcat_is_arrD = subsmc.subsmc_is_arrD

lemmas_with [unfolded slicing_simps slicing_commute]:
  subcat_Comp_simp = subsmc.subsmc_Comp_simp
  and subcat_is_idem_arrD = subsmc.subsmc_is_idem_arrD

end

lemmas [cat_sub_fw_cs_intros] = 
  subcategory.subcat_Obj_vsubset
  subcategory.subcat_is_arr_vsubset
  subcategory.subcat_objD
  subcategory.subcat_arrD
  subcategory.subcat_is_arrD

lemmas [cat_sub_bw_cs_simps] =
  subcategory.subcat_dom_simp
  subcategory.subcat_cod_simp

lemmas [cat_sub_fw_cs_intros] = 
  subcategory.subcat_is_idem_arrD

lemmas [cat_sub_bw_cs_simps] = 
  subcategory.subcat_Comp_simp


text‹The opposite subcategory.›

lemma (in subcategory) subcat_subcategory_op_cat: "op_cat 𝔅 ⊆⇩C⇘α⇙ op_cat ℭ"
proof(rule subcategoryI)
  show "cat_smc (op_cat 𝔅) ⊆⇩S⇩M⇩C⇘α⇙ cat_smc (op_cat ℭ)"
    unfolding slicing_commute[symmetric]
    by (intro subsmc_subsemicategory_op_smc subcat_subsemicategory)    
qed (simp_all add: sdg.category_op dg.category_op cat_op_simps subcat_CId)

lemmas subcat_subcategory_op_cat[intro] = subcategory.subcat_subcategory_op_cat


text‹Elementary properties.›

lemma (in subcategory) subcat_CId_is_arr[intro]:
  assumes "a ∈⇩∘ 𝔅⦇Obj⦈"
  shows "ℭ⦇CId⦈⦇a⦈ : a ↦⇘𝔅⇙ a"
proof-
  from assms have 𝔅ℭ: "𝔅⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈" by (simp add: subcat_CId)
  from assms have "𝔅⦇CId⦈⦇a⦈ : a ↦⇘𝔅⇙ a" by (auto intro: cat_cs_intros)
  then show ?thesis unfolding 𝔅ℭ by simp
qed


text‹Further rules.›

lemma (in subcategory) subcat_CId_simp[cat_sub_bw_cs_simps]:
  assumes "a ∈⇩∘ 𝔅⦇Obj⦈" 
  shows "𝔅⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈"
  using assms by (simp add: subcat_CId)

lemmas [cat_sub_bw_cs_simps] = subcategory.subcat_CId_simp 

lemma (in subcategory) subcat_is_right_inverseD[cat_sub_fw_cs_intros]: 
  assumes "is_right_inverse 𝔅 g f" 
  shows "is_right_inverse ℭ g f"
  using assms subcategory_axioms
  by (elim is_right_inverseE, intro is_right_inverseI)
    (
      cs_concl 
        cs_simp: cat_sub_bw_cs_simps[symmetric]
        cs_intro: cat_sub_fw_cs_intros cat_cs_intros cat_sub_cs_intros
    )

lemmas [cat_sub_fw_cs_intros] = subcategory.subcat_is_right_inverseD

lemma (in subcategory) subcat_is_left_inverseD[cat_sub_fw_cs_intros]: 
  assumes "is_left_inverse 𝔅 g f" 
  shows "is_left_inverse ℭ g f"
proof-
  have "op_cat 𝔅 ⊆⇩C⇘α⇙ op_cat ℭ" by (simp add: subcat_subcategory_op_cat)
  from subcategory.subcat_is_right_inverseD[OF this] show ?thesis 
    unfolding cat_op_simps using assms.
qed

lemmas [cat_sub_fw_cs_intros] = subcategory.subcat_is_left_inverseD

lemma (in subcategory) subcat_is_inverseD[cat_sub_fw_cs_intros]: 
  assumes "is_inverse 𝔅 g f" 
  shows "is_inverse ℭ g f"
  using assms subcategory_axioms
  by (elim is_inverseE, intro is_inverseI)
    (
      cs_concl 
        cs_simp: cat_sub_bw_cs_simps[symmetric]
        cs_intro: cat_sub_fw_cs_intros cat_cs_intros cat_sub_cs_intros
    )

lemmas [cat_sub_fw_cs_intros] = subcategory.subcat_is_inverseD

lemma (in subcategory) subcat_is_iso_arrD[cat_sub_fw_cs_intros]:
  assumes "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b" 
  shows "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
proof(intro is_iso_arrI)
  from subcategory_axioms is_iso_arrD(1)[OF assms] show "f : a ↦⇘ℭ⇙ b"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_sub_bw_cs_simps[symmetric] cs_intro: cat_sub_fw_cs_intros
      )
  from assms have "is_inverse 𝔅 (f¯⇩C⇘𝔅⇙) f"
    by (rule sdg.cat_the_inverse_is_inverse)
  with subcategory_axioms show "is_inverse ℭ (f¯⇩C⇘𝔅⇙) f"
    by (elim is_inverseE, intro is_inverseI)
      (
        cs_concl 
          cs_simp: cat_sub_bw_cs_simps[symmetric] 
          cs_intro: cat_sub_fw_cs_intros cat_cs_intros
      )
qed

lemmas [cat_sub_fw_cs_intros] = subcategory.subcat_is_iso_arrD

lemma (in subcategory) subcat_the_inverse_simp[cat_sub_bw_cs_simps]:
  assumes "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b" 
  shows "f¯⇩C⇘𝔅⇙ = f¯⇩C⇘ℭ⇙"
proof-
  from assms have "is_inverse 𝔅 (f¯⇩C⇘𝔅⇙) f"
    by (auto dest: sdg.cat_the_inverse_is_inverse)
  with subcategory_axioms have inv_f𝔅: "is_inverse ℭ (f¯⇩C⇘𝔅⇙) f" 
    by (auto dest: cat_sub_fw_cs_intros)
  from assms have "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b" by (auto dest: cat_sub_fw_cs_intros)
  then have inv_fℭ: "is_inverse ℭ (f¯⇩C⇘ℭ⇙) f" 
    by (auto dest: dg.cat_the_inverse_is_inverse)
  from inv_f𝔅 inv_fℭ show ?thesis by (intro dg.cat_is_inverse_eq)
qed

lemmas [cat_sub_bw_cs_simps] = subcategory.subcat_the_inverse_simp

lemma (in subcategory) subcat_obj_isoD:
  assumes "a ≈⇩o⇩b⇩j⇘𝔅⇙ b" 
  shows "a ≈⇩o⇩b⇩j⇘ℭ⇙ b"
  using assms subcategory_axioms
  by (elim obj_isoE) 
    (
      cs_concl cs_shallow
        cs_simp: cat_sub_bw_cs_simps cs_intro: obj_isoI cat_sub_fw_cs_intros
    )

lemmas [cat_sub_fw_cs_intros] = subcategory.subcat_obj_isoD


subsubsection‹Subcategory relation is a partial order›

lemma subcat_refl:
  assumes "category α 𝔄"
  shows "𝔄 ⊆⇩C⇘α⇙ 𝔄"
proof-
  interpret category α 𝔄 by (rule assms)
  show ?thesis 
    by (auto intro: cat_cs_intros slicing_intros subdg_refl subsemicategoryI)
qed

lemma subcat_trans: 
  assumes "𝔄 ⊆⇩C⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: subcategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis 
  proof(rule subcategoryI)
    show "cat_smc 𝔄 ⊆⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      by 
        (
          meson 
            𝔄𝔅.subcat_subsemicategory 
            𝔅ℭ.subcat_subsemicategory 
            subsmc_trans
        )
  qed 
    ( 
      use 𝔄𝔅.subcategory_axioms 𝔅ℭ.subcategory_axioms in 
        ‹auto simp: 𝔄𝔅.subcat_Obj_vsubset cat_sub_bw_cs_simps›
    )
qed

lemma subcat_antisym:
  assumes "𝔄 ⊆⇩C⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇘α⇙ 𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: subcategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis
  proof(rule cat_eqI)
    from 
      subsmc_antisym[
        OF 𝔄𝔅.subcat_subsemicategory 𝔅𝔄.subcat_subsemicategory
        ] 
    have 
      "cat_smc 𝔄⦇Obj⦈ = cat_smc 𝔅⦇Obj⦈" "cat_smc 𝔄⦇Arr⦈ = cat_smc 𝔅⦇Arr⦈"
      by simp_all
    then show Obj: "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" and Arr: "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" 
      unfolding slicing_simps by simp_all
    show "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈"
      by (rule vsv_eqI) (auto simp: 𝔄𝔅.subcat_dom_simp Arr cat_cs_simps)
    show "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
      by (rule vsv_eqI) (auto simp: 𝔅𝔄.subcat_cod_simp Arr cat_cs_simps)
    have "cat_smc 𝔄 ⊆⇩S⇩M⇩C⇘α⇙ cat_smc 𝔅" "cat_smc 𝔅 ⊆⇩S⇩M⇩C⇘α⇙ cat_smc 𝔄" 
      by (simp_all add: 𝔄𝔅.subcat_subsemicategory 𝔅𝔄.subcat_subsemicategory)
    from subsmc_antisym[OF this] have "cat_smc 𝔄 = cat_smc 𝔅" .
    then have "cat_smc 𝔄⦇Comp⦈ = cat_smc 𝔅⦇Comp⦈" by auto
    then show "𝔄⦇Comp⦈ = 𝔅⦇Comp⦈" unfolding slicing_simps by simp
    show "𝔄⦇CId⦈ = 𝔅⦇CId⦈"
      by (rule vsv_eqI) (auto simp: Obj 𝔄𝔅.subcat_CId_simp cat_cs_simps)
  qed (auto intro: cat_cs_intros)
qed



subsection‹Inclusion functor›


subsubsection‹Definition and elementary properties›


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

abbreviation (input) cf_inc :: "V ⇒ V ⇒ V"
  where "cf_inc ≡ dghm_inc"


text‹Slicing.›

lemma dghm_smcf_inc[slicing_commute]: 
  "dghm_inc (cat_smc 𝔅) (cat_smc ℭ) = cf_smcf (cf_inc 𝔅 ℭ)"
  unfolding cf_smcf_def dghm_inc_def cat_smc_def dg_field_simps dghm_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemmas [cat_cs_simps] = 
  dghm_inc_ObjMap_app 
  dghm_inc_ArrMap_app


subsubsection‹Canonical inclusion functor associated with a subcategory›

sublocale subcategory ⊆ inc: is_ft_functor α 𝔅 ℭ ‹cf_inc 𝔅 ℭ›
proof(rule is_ft_functorI)
  interpret subsmc: subsemicategory α ‹cat_smc 𝔅› ‹cat_smc ℭ›
    by (rule subcat_subsemicategory)
  show "cf_inc 𝔅 ℭ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"  
  proof(rule is_functorI) 
    show "vfsequence (cf_inc 𝔅 ℭ)" unfolding dghm_inc_def by auto
    show "vcard (cf_inc 𝔅 ℭ) = 4⇩ℕ"
      unfolding dghm_inc_def by (simp add: nat_omega_simps)
    from sdg.cat_CId_is_arr subcat_CId_simp show "c ∈⇩∘ 𝔅⦇Obj⦈ ⟹ 
      cf_inc 𝔅 ℭ⦇ArrMap⦈⦇𝔅⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇cf_inc 𝔅 ℭ⦇ObjMap⦈⦇c⦈⦈"
      for c
      unfolding dghm_inc_components by force
    from subsmc.inc.is_ft_semifunctor_axioms show 
      "cf_smcf (cf_inc 𝔅 ℭ) : cat_smc 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      unfolding slicing_commute by auto
  qed (auto simp: dghm_inc_components cat_cs_intros)
  from subsmc.inc.is_ft_semifunctor_axioms show 
    "cf_smcf (cf_inc 𝔅 ℭ) : cat_smc 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ cat_smc ℭ" 
    unfolding slicing_commute by auto
qed

lemmas (in subcategory) subcat_cf_inc_is_ft_functor = inc.is_ft_functor_axioms


subsubsection‹Inclusion functor for the opposite categories›

lemma (in subcategory) subcat_cf_inc_op_cat_is_functor:
  "cf_inc (op_cat 𝔅) (op_cat ℭ) : op_cat 𝔅 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_cat ℭ"
  by 
    (
      intro 
        subcategory.subcat_cf_inc_is_ft_functor
        subcat_subcategory_op_cat
    )
  
lemma (in subcategory) subcat_op_cat_cf_inc: 
  "cf_inc (op_cat 𝔅) (op_cat ℭ) = op_cf (cf_inc 𝔅 ℭ)"
  by (rule cf_eqI)
    (
      auto 
        simp: 
          cat_op_simps 
          dghm_inc_components
          subcat_cf_inc_op_cat_is_functor
          is_ft_functor.axioms(1) 
        intro: cat_op_intros 
    )



subsection‹Full subcategory›


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

locale fl_subcategory = subcategory +
  assumes fl_subcat_fl_subsemicategory: "cat_smc 𝔅 ⊆⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ cat_smc ℭ"

abbreviation is_fl_subcategory ("(_/ ⊆⇩C⇩.⇩f⇩u⇩l⇩lı _)" [51, 51] 50)
  where "𝔅 ⊆⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ ≡ fl_subcategory α 𝔅 ℭ"


text‹Rules.›

mk_ide rf fl_subcategory_def[unfolded fl_subcategory_axioms_def]
  |intro fl_subcategoryI|
  |dest fl_subcategoryD[dest]|
  |elim fl_subcategoryE[elim!]|

lemmas [cat_sub_cs_intros] = fl_subcategoryD(1)


text‹Elementary properties.›

sublocale fl_subcategory ⊆ inc: is_fl_functor α 𝔅 ℭ ‹cf_inc 𝔅 ℭ›
proof(rule is_fl_functorI)
  interpret fl_subsemicategory α ‹cat_smc 𝔅› ‹cat_smc ℭ›
    by (rule fl_subcat_fl_subsemicategory)
  from inc.is_fl_semifunctor_axioms show 
    "cf_smcf (cf_inc 𝔅 ℭ) : cat_smc 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ cat_smc ℭ"
    unfolding slicing_commute by simp
qed (rule inc.is_functor_axioms)



subsection‹Wide subcategory›


subsubsection‹Definition and elementary properties›


text‹
See 
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/wide+subcategory}
}.
›

locale wide_subcategory = subcategory +
  assumes wide_subcat_wide_subsemicategory: "cat_smc 𝔅 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ cat_smc ℭ"

abbreviation is_wide_subcategory ("(_/ ⊆⇩C⇩.⇩w⇩i⇩d⇩eı _)" [51, 51] 50)
  where "𝔅 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ ≡ wide_subcategory α 𝔅 ℭ"


text‹Rules.›

mk_ide rf wide_subcategory_def[unfolded wide_subcategory_axioms_def]
  |intro wide_subcategoryI|
  |dest wide_subcategoryD[dest]|
  |elim wide_subcategoryE[elim!]|

lemmas [cat_sub_cs_intros] = wide_subcategoryD(1)


text‹Wide subcategory is wide subsemicategory.›

context wide_subcategory
begin

interpretation wide_subsmc: wide_subsemicategory α ‹cat_smc 𝔅› ‹cat_smc ℭ›
  by (rule wide_subcat_wide_subsemicategory)

lemmas_with [unfolded slicing_simps]:
  wide_subcat_Obj[dg_sub_bw_cs_intros] = wide_subsmc.wide_subsmc_Obj
  and wide_subcat_obj_eq[dg_sub_bw_cs_simps] = wide_subsmc.wide_subsmc_obj_eq

end

lemmas [cat_sub_bw_cs_simps] =  wide_subcategory.wide_subcat_obj_eq[symmetric]
lemmas [cat_sub_bw_cs_simps] = wide_subsemicategory.wide_subsmc_obj_eq


subsubsection‹The wide subcategory relation is a partial order›

lemma wide_subcat_refl: 
  assumes "category α 𝔄" 
  shows "𝔄 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔄"
proof-
  interpret category α 𝔄 by (rule assms)
  show ?thesis
    by
      (
        auto intro: 
          assms
          slicing_intros 
          wide_subsmc_refl 
          wide_subcategoryI 
          subsmc_refl 
      )
qed

lemma wide_subcat_trans[trans]:
  assumes "𝔄 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: wide_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: wide_subcategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis
    by 
      (
        intro 
          wide_subcategoryI 
          subcat_trans[OF 𝔄𝔅.subcategory_axioms 𝔅ℭ.subcategory_axioms], 
        rule wide_subsmc_trans, 
        rule 𝔄𝔅.wide_subcat_wide_subsemicategory, 
        rule 𝔅ℭ.wide_subcat_wide_subsemicategory
     )
qed

lemma wide_subcat_antisym:
  assumes "𝔄 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: wide_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: wide_subcategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis 
    by (rule subcat_antisym[OF 𝔄𝔅.subcategory_axioms 𝔅𝔄.subcategory_axioms])
qed



subsection‹Replete subcategory›


subsubsection‹Definition and elementary properties›

text‹
See nLab
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/replete+subcategory}
}.
›

locale replete_subcategory = subcategory α 𝔅 ℭ for α 𝔅 ℭ +
  assumes rep_subcat_is_iso_arr_is_arr: 
    "a ∈⇩∘ 𝔅⦇Obj⦈ ⟹ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b ⟹ f : a ↦⇘𝔅⇙ b"

abbreviation is_replete_subcategory ("(_/ ⊆⇩C⇩.⇩r⇩e⇩pı _)" [51, 51] 50)
  where "𝔅 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ ℭ ≡ replete_subcategory α 𝔅 ℭ"


text‹Rules.›

mk_ide rf replete_subcategory_def[unfolded replete_subcategory_axioms_def]
  |intro replete_subcategoryI|
  |dest replete_subcategoryD[dest]|
  |elim replete_subcategoryE[elim!]|

lemmas [cat_sub_cs_intros] = replete_subcategoryD(1)


text‹Elementary properties.›

lemma (in replete_subcategory) (*not cat_sub_intro*)
  rep_subcat_is_iso_arr_is_iso_arr_left:
  assumes "a ∈⇩∘ 𝔅⦇Obj⦈" and "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b"
proof(intro is_iso_arrI is_inverseI)
  from assms show f: "f : a ↦⇘𝔅⇙ b" 
    by (auto intro: rep_subcat_is_iso_arr_is_arr)
  have "f¯⇩C⇘ℭ⇙ : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
    by (rule dg.cat_the_inverse_is_iso_arr[OF assms(2)])
  with f show inv_f: "f¯⇩C⇘ℭ⇙ : b ↦⇘𝔅⇙ a" 
    by (auto intro: rep_subcat_is_iso_arr_is_arr)
  show "f : a ↦⇘𝔅⇙ b" by (rule f)
  from dg.category_axioms assms have [cat_sub_bw_cs_simps]: 
    "f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from dg.category_axioms assms have [cat_sub_bw_cs_simps]: 
    "f ∘⇩A⇘ℭ⇙ f¯⇩C⇘ℭ⇙ = ℭ⦇CId⦈⦇b⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from subcategory_axioms f inv_f show "f¯⇩C⇘ℭ⇙ ∘⇩A⇘𝔅⇙ f = 𝔅⦇CId⦈⦇a⦈"
    by (cs_concl cs_simp: cat_sub_bw_cs_simps cs_intro: cat_cs_intros)
  from subcategory_axioms f inv_f show "f ∘⇩A⇘𝔅⇙ f¯⇩C⇘ℭ⇙ = 𝔅⦇CId⦈⦇b⦈"
    by (cs_concl cs_simp: cat_sub_bw_cs_simps cs_intro: cat_cs_intros)
qed

lemma (in replete_subcategory) (*not cat_sub_intro*)
  rep_subcat_is_iso_arr_is_iso_arr_right:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈" and "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b"
proof-
  from assms(2) have "f¯⇩C⇘ℭ⇙ : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
    by (rule dg.cat_the_inverse_is_iso_arr)
  with assms(1) have inv_f: "f¯⇩C⇘ℭ⇙ : b ↦⇩i⇩s⇩o⇘𝔅⇙ a"
    by (intro rep_subcat_is_iso_arr_is_iso_arr_left)
  then have "(f¯⇩C⇘ℭ⇙)¯⇩C⇘𝔅⇙ : a ↦⇩i⇩s⇩o⇘𝔅⇙ b" 
    by (rule sdg.cat_the_inverse_is_iso_arr)
  moreover from replete_subcategory_axioms assms inv_f have "(f¯⇩C⇘ℭ⇙)¯⇩C⇘𝔅⇙ = f"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_sub_bw_cs_simps cat_cs_simps cs_intro: cat_cs_intros 
      )
  ultimately show ?thesis by simp
qed

lemma (in replete_subcategory) (*not cat_sub_bw_cs_simps*)
  rep_subcat_is_iso_arr_is_iso_arr_left_iff:
  assumes "a ∈⇩∘ 𝔅⦇Obj⦈" 
  shows "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b ⟷ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  using assms replete_subcategory_axioms 
  by (intro iffI)
    (
      cs_concl cs_intro: 
        rep_subcat_is_iso_arr_is_iso_arr_left 
        cat_sub_fw_cs_intros
    )

lemma (in replete_subcategory) (*not cat_sub_bw_cs_simps*)
  rep_subcat_is_iso_arr_is_iso_arr_right_iff:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈" 
  shows "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b ⟷ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  using assms replete_subcategory_axioms 
  by (intro iffI)
    (
      cs_concl cs_intro: 
        rep_subcat_is_iso_arr_is_iso_arr_right
        cat_sub_fw_cs_intros
    )


subsubsection‹The replete subcategory relation is a partial order›

lemma rep_subcat_refl: 
  assumes "category α 𝔄" 
  shows "𝔄 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ 𝔄"
proof-
  interpret category α 𝔄 by (rule assms)
  show ?thesis 
    by (intro replete_subcategoryI subcat_refl assms is_iso_arrD(1))
qed

lemma rep_subcat_trans[trans]:
  assumes "𝔄 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: replete_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: replete_subcategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis
  proof
    (
      intro 
        replete_subcategoryI 
        subcat_trans[OF 𝔄𝔅.subcategory_axioms 𝔅ℭ.subcategory_axioms]
    )
    fix a b f assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
    have "b ∈⇩∘ 𝔅⦇Obj⦈"
      by 
        (
          rule 𝔄𝔅.dg.cat_is_arrD(3)
            [
              OF 𝔅ℭ.rep_subcat_is_iso_arr_is_arr[
                OF 𝔄𝔅.subcat_objD[OF prems(1)] prems(2)
                ]
            ]
        )
    then have "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b"
      by 
        (
          rule 𝔅ℭ.rep_subcat_is_iso_arr_is_iso_arr_right[
            OF _ prems(2)
            ]
        )
    then show "f : a ↦⇘𝔄⇙ b"
      by (rule 𝔄𝔅.rep_subcat_is_iso_arr_is_arr[OF prems(1)])
  qed
qed

lemma rep_subcat_antisym:
  assumes "𝔄 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇩.⇩r⇩e⇩p⇘α⇙ 𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: replete_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: replete_subcategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis 
    by (rule subcat_antisym[OF 𝔄𝔅.subcategory_axioms 𝔅𝔄.subcategory_axioms])
qed



subsection‹Wide replete subcategory›


subsubsection‹Definition and elementary properties›

locale wide_replete_subcategory = 
  wide_subcategory α 𝔅 ℭ + replete_subcategory α 𝔅 ℭ for α 𝔅 ℭ

abbreviation is_wide_replete_subcategory ("(_/ ⊆⇩C⇩.⇩w⇩rı _)" [51, 51] 50)
  where "𝔅 ⊆⇩C⇩.⇩w⇩r⇘α⇙ ℭ ≡ wide_replete_subcategory α 𝔅 ℭ"


text‹Rules.›

mk_ide rf wide_replete_subcategory_def
  |intro wide_replete_subcategoryI|
  |dest wide_replete_subcategoryD[dest]|
  |elim wide_replete_subcategoryE[elim!]|

lemmas [cat_sub_cs_intros] = wide_replete_subcategoryD


text‹Wide replete subcategory preserves isomorphisms.›

lemma (in wide_replete_subcategory) 
  wr_subcat_is_iso_arr_is_iso_arr:
  "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b ⟷ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
proof(rule iffI)
  assume prems: "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  then have "a ∈⇩∘ ℭ⦇Obj⦈" by auto
  then have a: "a ∈⇩∘ 𝔅⦇Obj⦈" by (simp add: wide_subcat_obj_eq)
  show "f : a ↦⇩i⇩s⇩o⇘𝔅⇙ b"
    by (intro rep_subcat_is_iso_arr_is_iso_arr_left[OF a prems])
qed 
  (
    use wide_replete_subcategory_axioms in
      ‹cs_concl cs_shallow cs_intro: cat_sub_fw_cs_intros ›
  )

lemmas [cat_sub_bw_cs_simps] = 
  wide_replete_subcategory.wr_subcat_is_iso_arr_is_iso_arr


subsubsection‹The wide replete subcategory relation is a partial order›

lemma wr_subcat_refl: 
  assumes "category α 𝔄" 
  shows "𝔄 ⊆⇩C⇩.⇩w⇩r⇘α⇙ 𝔄"
  by (intro wide_replete_subcategoryI wide_subcat_refl rep_subcat_refl assms)

lemma wr_subcat_trans[trans]:
  assumes "𝔄 ⊆⇩C⇩.⇩w⇩r⇘α⇙ 𝔅" and "𝔅 ⊆⇩C⇩.⇩w⇩r⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩C⇩.⇩w⇩r⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: wide_replete_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: wide_replete_subcategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis
    by 
      (
        intro wide_replete_subcategoryI,
        rule wide_subcat_trans, 
        rule 𝔄𝔅.wide_subcategory_axioms,
        rule 𝔅ℭ.wide_subcategory_axioms,
        rule rep_subcat_trans,
        rule 𝔄𝔅.replete_subcategory_axioms,
        rule 𝔅ℭ.replete_subcategory_axioms
      )
qed

lemma wr_subcat_antisym:
  assumes "𝔄 ⊆⇩C⇩.⇩w⇩r⇘α⇙  𝔅" and "𝔅 ⊆⇩C⇩.⇩w⇩r⇘α⇙  𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: wide_replete_subcategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: wide_replete_subcategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis 
    by (rule subcat_antisym[OF 𝔄𝔅.subcategory_axioms 𝔅𝔄.subcategory_axioms])
qed

text‹\newpage›

end