Theory CZH_ECAT_Small_Functor

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for functors›
theory CZH_ECAT_Small_Functor
  imports 
    CZH_Foundations.CZH_SMC_Small_Semifunctor
    CZH_ECAT_Functor
    CZH_ECAT_Small_Category
begin



subsection‹Functor with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_functor = is_functor α 𝔄 𝔅 𝔉  for α 𝔄 𝔅 𝔉 +
  assumes tm_cf_is_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tmαcat_smc 𝔅" 

syntax "_is_tm_functor" :: "V  V  V  V  bool" 
  ((_ :/ _ ↦↦C.tmı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦C.tmα𝔅"  "CONST is_tm_functor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_tm_functor :: "V  V  V  V  bool"
  where "is_cn_tm_functor α 𝔄 𝔅 𝔉  𝔉 : op_dg 𝔄 ↦↦C.tmα𝔅"

syntax "_is_cn_tm_functor" :: "V  V  V  V  bool" 
  ((_ :/ _ C.tm↦↦ı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 C.tm↦↦α𝔅"  "CONST is_cn_tm_functor α 𝔄 𝔅 𝔉"

abbreviation all_tm_cfs :: "V  V"
  where "all_tm_cfs α  set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tmα𝔅}"

abbreviation small_tm_cfs :: "V  V  V  V"
  where "small_tm_cfs α 𝔄 𝔅  set {𝔉. 𝔉 : 𝔄 ↦↦C.tmα𝔅}"

lemma (in is_tm_functor) tm_cf_is_semifunctor':
  assumes "α' = α"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↦↦SMC.tmα'𝔅'"
  unfolding assms by (rule tm_cf_is_semifunctor)

lemmas [slicing_intros] = is_tm_functor.tm_cf_is_semifunctor'


text‹Rules.›

lemma (in is_tm_functor) is_tm_functor_axioms'[cat_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦C.tmα'𝔅'"
  unfolding assms by (rule is_tm_functor_axioms)

mk_ide rf is_tm_functor_def[unfolded is_tm_functor_axioms_def]
  |intro is_tm_functorI|
  |dest is_tm_functorD[dest]|
  |elim is_tm_functorE[elim]|

lemmas [cat_small_cs_intros] = is_tm_functorD(1)


text‹Slicing.›

context is_tm_functor
begin

interpretation smcf: is_tm_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
  by (rule tm_cf_is_semifunctor)

lemmas_with [unfolded slicing_simps]:
  tm_cf_ObjMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ObjMap_in_Vset
  and tm_cf_ArrMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ArrMap_in_Vset

end

sublocale is_tm_functor  HomDom: tiny_category α 𝔄
proof(rule tiny_categoryI')
  show "𝔄Obj  Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ObjMap_in_Vset, unfolded cat_cs_simps])
  show "𝔄Arr  Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ArrMap_in_Vset, unfolded cat_cs_simps])
qed (simp add: cat_cs_intros)


text‹Further rules.›

lemma is_tm_functorI':
  assumes [simp]: "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and [simp]: "𝔉ObjMap  Vset α"
    and [simp]: "𝔉ArrMap  Vset α"
  shows "𝔉 : 𝔄 ↦↦C.tmα𝔅"
proof(intro is_tm_functorI)
  interpret is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tmαcat_smc 𝔅"
    by (intro is_tm_semifunctorI', unfold slicing_simps) 
      (auto simp: slicing_intros)
qed simp_all

lemma is_tm_functorD':
  assumes "𝔉 : 𝔄 ↦↦C.tmα𝔅"
  shows "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "𝔉ObjMap  Vset α"
    and "𝔉ArrMap  Vset α"
proof-
  interpret is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(1))    
  show "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "𝔉ObjMap  Vset α"
    and "𝔉ArrMap  Vset α"
    by (auto intro: cat_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tm_functorD'(1)

lemma is_tm_functorE':
  assumes "𝔉 : 𝔄 ↦↦C.tmα𝔅"
  obtains "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "𝔉ObjMap  Vset α"
    and "𝔉ArrMap  Vset α"
  using is_tm_functorD'[OF assms] by simp


text‹Size.›

lemma small_all_tm_cfs[simp]: "small {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tmα𝔅}"
proof(rule down)
  show 
    "{𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tmα𝔅} 
      elts (set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅})"
  proof
    (
      simp only: elts_of_set small_all_cfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tmα𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦C.tmα𝔅" by clarsimp
    then interpret is_tm_functor α 𝔄 𝔅 𝔉 .
    show "𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅" by (blast intro: is_functor_axioms')
  qed
qed


subsubsection‹Opposite functor with tiny maps›

lemma (in is_tm_functor) is_tm_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↦↦C.tmαop_cat 𝔅"
  by (intro is_tm_functorI', unfold cat_op_simps)
    (cs_concl cs_intro: cat_cs_intros cat_op_intros)

lemma (in is_tm_functor) is_tm_functor_op'[cat_op_intros]:  
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅" and "α' = α"
  shows "op_cf 𝔉 : 𝔄' ↦↦C.tmα'𝔅'"
  unfolding assms by (rule is_tm_functor_op)

lemmas is_tm_functor_op[cat_op_intros] = is_tm_functor.is_tm_functor_op'


subsubsection‹Composition of functors with tiny maps›

lemma cf_comp_is_tm_functor[cat_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦C.tmα" and "𝔉 : 𝔄 ↦↦C.tmα𝔅"
  shows "𝔊 CF 𝔉 : 𝔄 ↦↦C.tmα"
proof(rule is_tm_functorI)
  interpret 𝔉: is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_functor α 𝔅  𝔊 by (rule assms(1))
  from 𝔉.tm_cf_is_semifunctor 𝔊.tm_cf_is_semifunctor show 
    "cf_smcf (𝔊 CF 𝔉) : cat_smc 𝔄 ↦↦SMC.tmαcat_smc "   
    by (auto simp: smc_small_cs_intros slicing_commute[symmetric])
  show "𝔊 CF 𝔉 : 𝔄 ↦↦Cα" by (auto intro: cat_cs_intros)
qed


subsubsection‹Finite categories and functors with tiny maps›

lemma (in is_functor) cf_is_tm_functor_if_HomDom_finite_category:
  assumes "finite_category α 𝔄"
  shows "𝔉 : 𝔄 ↦↦C.tmα𝔅"
proof(intro is_tm_functorI)
  interpret 𝔄: finite_category α 𝔄 by (rule assms(1))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tmαcat_smc 𝔅"
    by 
      (
        rule 
          is_semifunctor.smcf_is_tm_semifunctor_if_HomDom_finite_semicategory[
            OF cf_is_semifunctor 𝔄.fin_cat_finite_semicategory
            ]
      )
qed (auto intro: cat_cs_intros)


subsubsection‹Constant functor with tiny maps›

lemma cf_const_is_tm_functor: 
  assumes "tiny_category α " and "category α 𝔇" and "a  𝔇Obj"
  shows "cf_const  𝔇 a :  ↦↦C.tmα𝔇"
proof(intro is_tm_functorI)
  from assms show "cf_smcf (cf_const  𝔇 a) : cat_smc  ↦↦SMC.tmαcat_smc 𝔇"
    by 
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] slicing_simps cat_cs_simps 
          cs_intro: slicing_intros cat_cs_intros smc_small_cs_intros
      )+
  from assms show "cf_const  𝔇 a :  ↦↦Cα𝔇"
    by (cs_concl cs_intro: cat_cs_intros cat_small_cs_intros)
qed

lemma cf_const_is_tm_functor'[cat_small_cs_intros]:
  assumes "tiny_category α "
    and "category α 𝔇" 
    and "a  𝔇Obj"
    and "ℭ' = "
    and "𝔇' = 𝔇"
  shows "cf_const  𝔇 a : ℭ' ↦↦C.tmα𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule cf_const_is_tm_functor)



subsection‹Tiny functor›


subsubsection‹Definition and elementary properties›

locale is_tiny_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes tiny_cf_is_tiny_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tinyαcat_smc 𝔅" 

syntax "_is_tiny_functor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦C.tinyı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦C.tinyα𝔅"  "CONST is_tiny_functor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_tiny_cf :: "V  V  V  V  bool"
  where "is_cn_tiny_cf α 𝔄 𝔅 𝔉  𝔉 : op_cat 𝔄 ↦↦C.tinyα𝔅"

syntax "_is_cn_tiny_cf" :: "V  V  V  V  bool"
  ((_ :/ _ C.tiny↦↦ı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 C.tiny↦↦α𝔅"  "CONST is_cn_cf α 𝔄 𝔅 𝔉"

abbreviation all_tiny_cfs :: "V  V"
  where "all_tiny_cfs α  set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}"

abbreviation tiny_cfs :: "V  V  V  V"
  where "tiny_cfs α 𝔄 𝔅  set {𝔉. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}"

lemmas [slicing_intros] = is_tiny_functor.tiny_cf_is_tiny_semifunctor


text‹Rules.›

lemma (in is_tiny_functor) is_tiny_functor_axioms'[cat_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦C.tinyα'𝔅'"
  unfolding assms by (rule is_tiny_functor_axioms)

mk_ide rf is_tiny_functor_def[unfolded is_tiny_functor_axioms_def]
  |intro is_tiny_functorI|
  |dest is_tiny_functorD[dest]|
  |elim is_tiny_functorE[elim]|

lemmas [cat_small_cs_intros] = is_tiny_functorD(1)


text‹Elementary properties.›

sublocale is_tiny_functor  HomDom: tiny_category α 𝔄
proof(intro tiny_categoryI')
  interpret smcf: is_tiny_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
    by (rule tiny_cf_is_tiny_semifunctor)
  show "𝔄Obj  Vset α"
    by (rule smcf.HomDom.tiny_smc_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔄Arr  Vset α"
    by (rule smcf.HomDom.tiny_smc_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: cat_cs_intros)

sublocale is_tiny_functor  HomCod: tiny_category α 𝔅
proof(intro tiny_categoryI')
  interpret smcf: is_tiny_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
    by (rule tiny_cf_is_tiny_semifunctor)
  show "𝔅Obj  Vset α"
    by (rule smcf.HomCod.tiny_smc_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔅Arr  Vset α"
    by (rule smcf.HomCod.tiny_smc_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: cat_cs_intros)

sublocale is_tiny_functor  is_tm_functor
proof(intro is_tm_functorI')
  interpret smcf: is_tiny_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
    by (rule tiny_cf_is_tiny_semifunctor)
  note Vset[unfolded slicing_simps] = 
    smcf.tm_smcf_ObjMap_in_Vset
    smcf.tm_smcf_ArrMap_in_Vset
  show "𝔉ObjMap  Vset α" "𝔉ArrMap  Vset α" by (intro Vset)+
qed (auto simp: cat_cs_intros)


text‹Further rules.›

lemma is_tiny_functorI':
  assumes [simp]: "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "tiny_category α 𝔄"
    and "tiny_category α 𝔅"
  shows "𝔉 : 𝔄 ↦↦C.tinyα𝔅"
proof(intro is_tiny_functorI)
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔄: tiny_category α 𝔄 by (rule assms(2))
  interpret 𝔅: tiny_category α 𝔅 by (rule assms(3))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tinyαcat_smc 𝔅"
    by (intro is_tiny_semifunctorI') (auto intro: slicing_intros)
qed (rule assms(1))

lemma is_tiny_functorD':
  assumes "𝔉 : 𝔄 ↦↦C.tinyα𝔅"
  shows "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "tiny_category α 𝔄"
    and "tiny_category α 𝔅"
proof-
  interpret is_tiny_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  show "𝔉 : 𝔄 ↦↦Cα𝔅" and "tiny_category α 𝔄" and "tiny_category α 𝔅"
    by (auto intro: cat_small_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tiny_functorD'(2,3)

lemma is_tiny_functorE':
  assumes "𝔉 : 𝔄 ↦↦C.tinyα𝔅"
  obtains "𝔉 : 𝔄 ↦↦Cα𝔅" 
    and "tiny_category α 𝔄"
    and "tiny_category α 𝔅"
  using is_tiny_functorD'[OF assms] by auto

lemma is_tiny_functor_iff:
  "𝔉 : 𝔄 ↦↦C.tinyα𝔅  
    (𝔉 : 𝔄 ↦↦Cα𝔅  tiny_category α 𝔄  tiny_category α 𝔅)"
  by (auto intro: is_tiny_functorI' dest: is_tiny_functorD'(2,3))


text‹Size.›

lemma (in is_tiny_functor) tiny_cf_in_Vset: "𝔉  Vset α"
proof-
  note [cat_cs_intros] = 
    tm_cf_ObjMap_in_Vset 
    tm_cf_ArrMap_in_Vset
    HomDom.tiny_cat_in_Vset 
    HomCod.tiny_cat_in_Vset 
  show ?thesis
    by (subst cf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma small_all_tiny_cfs[simp]: "small {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}"
proof(rule down)
  show 
    "{𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}  
      elts (set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅})"
  proof
    (
      simp only: elts_of_set small_all_cfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦C.tinyα𝔅" by clarsimp
    then interpret is_tiny_functor α 𝔄 𝔅 𝔉 by simp
    show "𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅" by (meson is_functor_axioms)
  qed
qed

lemma small_tiny_cfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}"
  by (rule down[of _ set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}]) auto

lemma all_tiny_cfs_vsubset_Vset[simp]: 
  "set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦C.tinyα𝔅}  Vset α"
proof(rule vsubsetI) 
  fix 𝔉 assume "𝔉  all_tiny_cfs α"
  then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦C.tinyα𝔅" by clarsimp
  then show "𝔉  Vset α" by (auto simp: is_tiny_functor.tiny_cf_in_Vset)
qed

lemma (in is_functor) cf_is_tiny_functor_if_ge_Limit:
  assumes "𝒵 β" and "α  β"
  shows "𝔉 : 𝔄 ↦↦C.tinyβ𝔅"
proof(intro is_tiny_functorI)
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMC.tinyβcat_smc 𝔅"
    by 
      (
        rule is_semifunctor.smcf_is_tiny_semifunctor_if_ge_Limit, 
        rule cf_is_semifunctor; 
        intro assms
      )
qed (simp add: cf_is_functor_if_ge_Limit assms)


subsubsection‹Opposite tiny semifunctor›

lemma (in is_tiny_functor) is_tiny_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↦↦C.tinyαop_cat 𝔅"
  by (intro is_tiny_functorI') 
    (cs_concl cs_intro: cat_op_intros cat_small_cs_intros)+

lemma (in is_tiny_functor) is_tiny_functor_op'[cat_op_intros]:  
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅" and "α' = α"
  shows "op_cf 𝔉 : 𝔄' ↦↦C.tinyα'𝔅'"
  unfolding assms by (rule is_tiny_functor_op)

lemmas is_tiny_functor_op[cat_op_intros] = 
  is_tiny_functor.is_tiny_functor_op'


subsubsection‹Composition of tiny functors›

lemma cf_comp_is_tiny_functor[cat_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦C.tinyα" and "𝔉 : 𝔄 ↦↦C.tinyα𝔅"
  shows "𝔊 CF 𝔉 : 𝔄 ↦↦C.tinyα"
proof-
  interpret 𝔉: is_tiny_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_functor α 𝔅  𝔊 by (rule assms(1))
  show ?thesis by (rule is_tiny_functorI') (auto intro: cat_small_cs_intros)
qed


subsubsection‹Tiny constant functor›

lemma cf_const_is_tiny_functor:
  assumes "tiny_category α " and "tiny_category α 𝔇" and "a  𝔇Obj"
  shows "cf_const  𝔇 a :  ↦↦C.tinyα𝔇"
proof(intro is_tiny_functorI')
  from assms show "cf_const  𝔇 a :  ↦↦Cα𝔇"
    by (cs_concl cs_intro: cat_small_cs_intros)
qed (auto simp: assms(1,2))

lemma cf_const_is_tiny_functor':
  assumes "tiny_category α "
    and "tiny_category α 𝔇" 
    and "a  𝔇Obj"
    and "ℭ' = "
    and "𝔇' = 𝔇"
  shows "cf_const  𝔇 a : ℭ' ↦↦C.tinyα𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule cf_const_is_tiny_functor)

lemmas [cat_small_cs_intros] = cf_const_is_tiny_functor'

text‹\newpage›

end