Theory CZH_ECAT_Small_Order

(* Copyright 2020 (C) Mihails Milehins *)

section‹Smallness for orders›
theory CZH_ECAT_Small_Order
  imports 
    CZH_ECAT_Order
    CZH_ECAT_Small_Functor
begin



subsection‹Background›

named_theorems cat_small_order_cs_simps
named_theorems cat_small_order_cs_intros



subsection‹Tiny preorder category›

locale cat_tiny_preorder = tiny_category α  for α  + 
  assumes cat_tiny_peo:
    " a  Obj; b  Obj   
      (f. Hom  a b = set {f})  (Hom  a b = 0)"


text‹Rules.›

lemma (in cat_tiny_preorder) cat_tiny_preorder_axioms'[cat_order_cs_intros]:
  assumes "α' = α"
  shows "cat_tiny_preorder α' "
  unfolding assms by (rule cat_tiny_preorder_axioms)

mk_ide rf cat_tiny_preorder_def[unfolded cat_tiny_preorder_axioms_def]
  |intro cat_tiny_preorderI|
  |dest cat_tiny_preorderD[dest]|
  |elim cat_tiny_preorderE[elim]|

lemmas [cat_small_order_cs_intros] = cat_tiny_preorderD(1)


text‹Tiny preorder is a preorder.›

sublocale cat_tiny_preorder  cat_preorder
  by (intro cat_preorderI cat_tiny_peo category_axioms) simp_all

lemmas (in cat_tiny_preorder) cat_tiny_peo_is_cat_preoder = cat_preorder_axioms

lemmas [cat_small_order_cs_intros] = 
  cat_tiny_preorder.cat_tiny_peo_is_cat_preoder



subsection‹Tiny partial order category›

locale cat_tiny_partial_order = cat_tiny_preorder α  for α  + 
  assumes cat_tiny_po:
    " a  Obj; b  Obj; a Ob; b Oa   a = b"


text‹Rules.›

lemma (in cat_tiny_partial_order) 
  cat_tiny_partial_order_axioms'[cat_order_cs_intros]:
  assumes "α' = α"
  shows "cat_tiny_partial_order α' "
  unfolding assms by (rule cat_tiny_partial_order_axioms)

mk_ide rf cat_tiny_partial_order_def[unfolded cat_tiny_partial_order_axioms_def]
  |intro cat_tiny_partial_orderI|
  |dest cat_tiny_partial_orderD[dest]|
  |elim cat_tiny_partial_orderE[elim]|

lemmas [cat_small_order_cs_intros] = cat_tiny_partial_orderD(1)


text‹Tiny partial order is a partial order.›

sublocale cat_tiny_partial_order  cat_partial_order
  by (intro cat_partial_orderI cat_tiny_po cat_preorder_axioms) simp_all

lemmas (in cat_tiny_preorder) cat_tiny_po_is_cat_preoder = cat_preorder_axioms

lemmas [cat_small_order_cs_intros] = 
  cat_tiny_preorder.cat_tiny_peo_is_cat_preoder

lemma cat_tiny_partial_orderI':
  assumes "tiny_category α "
    and "cat_partial_order α "
  shows "cat_tiny_partial_order α "
proof-
  interpret tiny_category α  by (rule assms(1))
  interpret cat_partial_order α  by (rule assms(2))
  show ?thesis
    by (intro cat_tiny_partial_orderI cat_tiny_preorderI assms(1) cat_po cat_peo)
qed



subsection‹Tiny linear order category›

locale cat_tiny_linear_order = cat_tiny_partial_order α  for α  + 
  assumes cat_tiny_lo: " a  Obj; b  Obj   a Ob  b Oa"


text‹Rules.›

lemma (in cat_tiny_linear_order) 
  cat_tiny_linear_order_axioms'[cat_order_cs_intros]:
  assumes "α' = α"
  shows "cat_tiny_linear_order α' "
  unfolding assms by (rule cat_tiny_linear_order_axioms)

mk_ide rf cat_tiny_linear_order_def[unfolded cat_tiny_linear_order_axioms_def]
  |intro cat_tiny_linear_orderI|
  |dest cat_tiny_linear_orderD[dest]|
  |elim cat_tiny_linear_orderE[elim]|

lemmas [cat_small_order_cs_intros] = cat_tiny_linear_orderD(1)


text‹Tiny linear order is a partial order.›

sublocale cat_tiny_linear_order  cat_linear_order
  by (intro cat_linear_orderI cat_tiny_lo cat_partial_order_axioms) simp_all

lemmas (in cat_tiny_linear_order) cat_tiny_lo_is_cat_partial_order = 
  cat_linear_order_axioms

lemmas [cat_small_order_cs_intros] = 
  cat_tiny_linear_order.cat_tiny_lo_is_cat_partial_order

lemma cat_tiny_linear_orderI':
  assumes "tiny_category α " and "cat_linear_order α "
  shows "cat_tiny_linear_order α "
proof-
  interpret tiny_category α  by (rule assms(1))
  interpret cat_linear_order α  by (rule assms(2))
  show ?thesis
    by 
      (
        intro 
          assms(1) 
          cat_tiny_linear_orderI 
          cat_tiny_partial_orderI' 
          cat_partial_order_axioms 
          cat_lo
      )  
qed



subsection‹Tiny preorder functor›

locale is_tiny_preorder_functor =
  is_functor α 𝔄 𝔅 𝔉 +
  HomDom: cat_tiny_preorder α 𝔄 +
  HomCod: cat_tiny_preorder α 𝔅
  for α 𝔄 𝔅 𝔉 

syntax "_is_tiny_preorder_functor" :: "V  V  V  V  bool"
  ((_ :/ _ C.PEO.tinyı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 C.PEO.tinyα𝔅"  
  "CONST is_tiny_preorder_functor α 𝔄 𝔅 𝔉"


text‹Rules.›

lemma (in is_tiny_preorder_functor) 
  is_tiny_preorder_functor_axioms'[cat_order_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"  
  shows "𝔉 : 𝔄' C.PEO.tinyα'𝔅'"
  unfolding assms by (rule is_tiny_preorder_functor_axioms)

mk_ide rf is_tiny_preorder_functor_def
  |intro is_tiny_preorder_functorI|
  |dest is_tiny_preorder_functorD[dest]|
  |elim is_tiny_preorder_functorE[elim]|

lemmas [cat_small_order_cs_intros] = is_tiny_preorder_functorD(1)


text‹Tiny preorder functor is a tiny functor›

sublocale is_tiny_preorder_functor  is_tiny_functor
  by
    (
      intro
        is_tiny_functorI'
        is_functor_axioms
        HomDom.tiny_category_axioms
        HomCod.tiny_category_axioms
    )

end