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 ≤⇩O⇘ℭ⇙ b; b ≤⇩O⇘ℭ⇙ a ⟧ ⟹ 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 ≤⇩O⇘ℭ⇙ b ∨ b ≤⇩O⇘ℭ⇙ a"


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⇩.⇩P⇩E⇩O⇩.⇩t⇩i⇩n⇩yı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ≤⇩C⇩.⇩P⇩E⇩O⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" ⇌ 
  "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⇩.⇩P⇩E⇩O⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  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