(*  Title:       Subcategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2017
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter "Subcategory"

  text‹
 In this chapter we give a construction of the subcategory of a category
 defined by a predicate on arrows subject to closure conditions. The arrows of
 the subcategory are directly identified with the arrows of the ambient category.
 We also define the related notions of full subcategory and inclusion functor.
 ›

theory Subcategory
imports Functor
begin

  locale subcategory =
    C: category C
    for C :: "'a comp"      (infixr ‹⋅_C› 55)
    and Arr :: "'a → bool" +
    assumes inclusion: "Arr f ==> C.arr f"
    and dom_closed: "Arr f ==> Arr (C.dom f)"
    and cod_closed: "Arr f ==> Arr (C.cod f)"
    and comp_closed: "[ Arr f; Arr g; C.cod f = C.dom g ] ==> Arr (g ⋅_C f)"
  begin

    no_notation C.in_hom    (‹«_ : _ → _¬›)
    notation C.in_hom       (‹«_ : _ →_C _¬›)

    definition comp         (infixr ‹⋅› 55)
    where "g ⋅ f = (if Arr f ∧ Arr g ∧ C.cod f = C.dom g then g ⋅_C f else C.null)"

    interpretation partial_composition comp
    proof
      show "∃!n. ∀f. n ⋅ f = n ∧ f ⋅ n = n"
      proof
        show 1: "∀f. C.null ⋅ f = C.null ∧ f ⋅ C.null = C.null"
          by (metis C.null_is_zero(1) C.ex_un_null comp_def)
        show "∧n. ∀f. n ⋅ f = n ∧ f ⋅ n = n ==> n = C.null"
          using 1 C.ex_un_null by metis
      qed
    qed

    lemma null_char [simp]:
    shows "null = C.null"
    proof -
      have "∀f. C.null ⋅ f = C.null ∧ f ⋅ C.null = C.null"
        by (metis C.null_is_zero(1) C.ex_un_null comp_def)
      thus ?thesis using ex_un_null by (metis null_is_zero(2))
    qed

    lemma ideI_SbC:
    assumes "Arr a" and "C.ide a"
    shows "ide a"
      unfolding ide_def
      using assms null_char C.ide_def comp_def by auto

    lemma Arr_iff_dom_in_domain:
    shows "Arr f ⟷ C.dom f ∈ domains f"
    proof
      show "C.dom f ∈ domains f ==> Arr f"
        using domains_def comp_def ide_def by fastforce
      show "Arr f ==> C.dom f ∈ domains f"
      proof -
        assume f: "Arr f"
        have "ide (C.dom f)"
          using f inclusion C.dom_in_domains C.has_domain_iff_arr C.domains_def
                dom_closed ideI_SbC
          by auto
        moreover have "f ⋅ C.dom f ≠ null"
          using f comp_def dom_closed null_char inclusion C.comp_arr_dom by force
        ultimately show ?thesis
          using domains_def by simp
      qed
    qed

    lemma Arr_iff_cod_in_codomain:
    shows "Arr f ⟷ C.cod f ∈ codomains f"
    proof
      show "C.cod f ∈ codomains f ==> Arr f"
        using codomains_def comp_def ide_def by fastforce
      show "Arr f ==> C.cod f ∈ codomains f"
      proof -
        assume f: "Arr f"
        have "ide (C.cod f)"
          using f inclusion C.cod_in_codomains C.has_codomain_iff_arr C.codomains_def
                cod_closed ideI_SbC
          by auto
        moreover have "C.cod f ⋅ f ≠ null"
          using f comp_def cod_closed null_char inclusion C.comp_cod_arr by force
        ultimately show ?thesis
          using codomains_def by simp
      qed
    qed

    lemma arr_char_SbC:
    shows "arr f ⟷ Arr f"
    proof
      show "Arr f ==> arr f"
        using arr_def comp_def Arr_iff_dom_in_domain Arr_iff_cod_in_codomain by auto
      show "arr f ==> Arr f"
      proof -
        assume f: "arr f"
        obtain a where a: "a ∈ domains f ∨ a ∈ codomains f"
          using f arr_def by auto
        have "f ⋅ a ≠ C.null ∨ a ⋅ f ≠ C.null"
          using a domains_def codomains_def null_char by auto
        thus "Arr f"
          using comp_def by metis
      qed
    qed

    lemma arrI_SbC [intro]:
    assumes "Arr f"
    shows "arr f"
      using assms arr_char_SbC by simp

    lemma arrE [elim]:
    assumes "arr f"
    shows "Arr f"
      using assms arr_char_SbC by simp

    interpretation category comp
    proof
      show 1: "∧g f. g ⋅ f ≠ null ==> seq g f"
        using comp_closed comp_def by fastforce
      show "∧f. (domains f ≠ {}) = (codomains f ≠ {})"
        using Arr_iff_cod_in_codomain Arr_iff_dom_in_domain arrE arr_def codomains_def by blast
      show "∧h g f. [seq h g; seq (h ⋅ g) f] ==> seq g f"
        by (metis (full_types) 1 C.dom_comp C.match_1 C.not_arr_null arrE inclusion comp_def)
      show "∧h g f. [seq h (g ⋅ f); seq g f] ==> seq h g"
        by (metis (full_types) 1 C.cod_comp C.match_2 C.not_arr_null arrE inclusion comp_def)
      show 2: "∧g f h. [seq g f; seq h g] ==> seq (h ⋅ g) f"
        by (metis (full_types) 1 C.dom_comp C.not_arr_null C.seqI arrE inclusion comp_def)
      show "∧g f h. [seq g f; seq h g] ==> (h ⋅ g) ⋅ f = h ⋅ g ⋅ f"
        by (metis 2 C.comp_assoc C.not_arr_null arrE C.cod_comp inclusion comp_def)
    qed

    theorem is_category:
    shows "category comp" ..

    notation in_hom     (‹«_ : _ → _¬›)

    lemma dom_simp:
    assumes "arr f"
    shows "dom f = C.dom f"
      by (metis Arr_iff_dom_in_domain arrE assms dom_eqI')

    lemma dom_char_SbC:
    shows "dom f = (if arr f then C.dom f else C.null)"
      using dom_simp dom_def arr_def arr_char_SbC by auto

    lemma cod_simp:
    assumes "arr f"
    shows "cod f = C.cod f"
      by (metis Arr_iff_cod_in_codomain arrE assms cod_eqI')

    lemma cod_char_SbC:
    shows "cod f = (if arr f then C.cod f else C.null)"
      using cod_simp cod_def arr_def by auto

    lemma in_hom_char_SbC:
    shows "«f : a → b¬ ⟷ arr a ∧ arr b ∧ arr f ∧ «f : a →_C b¬"
      using inclusion arr_char_SbC cod_closed dom_closed
      by (metis C.arr_iff_in_hom C.in_homE arr_iff_in_hom cod_simp dom_simp in_homE)

    lemma ide_char_SbC:
    shows "ide a ⟷ arr a ∧ C.ide a"
      using ide_in_hom C.ide_in_hom in_hom_char_SbC by simp

    lemma seq_char_SbC:
    shows "seq g f ⟷ arr f ∧ arr g ∧ C.seq g f"
    proof
      show "arr f ∧ arr g ∧ C.seq g f ==> seq g f"
        using arr_char_SbC dom_char_SbC cod_char_SbC by (intro seqI, auto)
      show "seq g f ==> arr f ∧ arr g ∧ C.seq g f"
        apply (elim seqE, auto)
        using inclusion arr_char_SbC dom_simp cod_simp by auto
    qed

    lemma hom_char:
    shows "hom a b = C.hom a b ∩ Collect Arr"
    proof
      show "hom a b ⊆ C.hom a b ∩ Collect Arr"
        using in_hom_char_SbC by auto
      show "C.hom a b ∩ Collect Arr ⊆ hom a b"
        using arr_char_SbC dom_char_SbC cod_char_SbC by force
    qed

    lemma comp_char:
    shows "g ⋅ f = (if arr f ∧ arr g ∧ C.seq g f then g ⋅_C f else C.null)"
      using arr_char_SbC comp_def comp_closed C.ext by force

    lemma comp_simp:
    assumes "seq g f"
    shows "g ⋅ f = g ⋅_C f"
      using assms comp_char seq_char_SbC by metis

    lemma inclusion_preserves_inverse:
    assumes "inverse_arrows f g"
    shows "C.inverse_arrows f g"
      using assms ide_char_SbC comp_simp arr_char_SbC
      by (intro C.inverse_arrowsI, auto)

    lemma iso_char_SbC:
    shows "iso f ⟷ C.iso f ∧ arr f ∧ arr (C.inv f)"
      by (metis C.category_axioms C.cod_inv C.comp_arr_inv' C.comp_inv_arr' C.dom_inv arr_inv
          category.inverse_unique category.isoI category.seqI cod_simp comp_simp dom_simp
          ide_cod inverse_arrowsI is_category iso_is_arr iso_def inclusion_preserves_inverse)

    lemma inv_char_SbC:
    assumes "iso f"
    shows "inv f = C.inv f"
      by (metis assms C.inverse_unique inclusion_preserves_inverse isoE inverse_unique)

    lemma inverse_arrows_char_SbC:
    shows "inverse_arrows f g ⟷ seq f g ∧ C.inverse_arrows f g"
      by (metis C.inverse_arrows_def comp_simp ide_char_SbC ide_compE inverse_arrows_def)

  end

  sublocale subcategory ⊆ category comp
    using is_category by auto

  section "Full Subcategory"

  locale full_subcategory =
    C: category C
    for C :: "'a comp"
    and Ide :: "'a → bool" +
    assumes inclusion_FSbC: "Ide f ==> C.ide f"
  begin

    sublocale subcategory C "λf. C.arr f ∧ Ide (C.dom f) ∧ Ide (C.cod f)"
      by (unfold_locales; simp)

    lemma is_subcategory:
    shows "subcategory C (λf. C.arr f ∧ Ide (C.dom f) ∧ Ide (C.cod f))"
      ..

    lemma in_hom_char_FSbC:
    shows "«f : a → b¬ ⟷ arr a ∧ arr b ∧ «f : a →_C b¬"
      using arr_char_SbC in_hom_char_SbC by auto

    text ‹
 Isomorphisms in a full subcategory are inherited from the ambient category.
 ›

    lemma iso_char_FSbC:
    shows "iso f ⟷ arr f ∧ C.iso f"
      using arr_char_SbC iso_char_SbC by force

  end

  section "Inclusion Functor"

  text ‹
 If ‹S› is a subcategory of ‹C›, then there is an inclusion functor
 from ‹S› to ‹C›. Inclusion functors are faithful embeddings.
 ›

  locale inclusion_functor =
    C: category C +
    S: subcategory C Arr
  for C :: "'a comp"
  and Arr :: "'a → bool"
  begin

    interpretation "functor" S.comp C S.map
      using S.map_def S.arr_char_SbC S.inclusion S.dom_char_SbC S.cod_char_SbC
            S.dom_closed S.cod_closed S.comp_closed S.arr_char_SbC S.comp_char
      apply unfold_locales
          apply auto[4]
      by (elim S.seqE, auto)

    lemma is_functor:
    shows "functor S.comp C S.map" ..

    interpretation faithful_functor S.comp C S.map
      apply unfold_locales by simp

    lemma is_faithful_functor:
    shows "faithful_functor S.comp C S.map" ..

    interpretation embedding_functor S.comp C S.map
      apply unfold_locales by simp

    lemma is_embedding_functor:
    shows "embedding_functor S.comp C S.map" ..

  end

  sublocale inclusion_functor ⊆ faithful_functor S.comp C S.map
    using is_faithful_functor by auto
  sublocale inclusion_functor ⊆ embedding_functor S.comp C S.map
    using is_embedding_functor by auto

  text ‹
 The inclusion of a full subcategory is a special case.
 Such functors are fully faithful.
 ›

  locale full_inclusion_functor =
    C: category C +
    S: full_subcategory C Ide
  for C :: "'a comp"
  and Ide :: "'a → bool"
  begin

    sublocale inclusion_functor C ‹λf. C.arr f ∧ Ide (C.dom f) ∧ Ide (C.cod f)› ..

    lemma is_inclusion_functor:
    shows "inclusion_functor C (λf. C.arr f ∧ Ide (C.dom f) ∧ Ide (C.cod f))"
      ..

    interpretation full_functor S.comp C S.map
      apply unfold_locales
      using S.ide_in_hom
      by (metis (no_types, lifting) C.in_homE S.arr_char_SbC S.in_hom_char_FSbC S.map_simp)

    lemma is_full_functor:
    shows "full_functor S.comp C S.map" ..

    sublocale full_functor S.comp C S.map
      using is_full_functor by auto
    sublocale fully_faithful_functor S.comp C S.map ..

  end

end