Theory Category3.Subcategory

(*  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 ideISbC:
    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 ideISbC
          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 ideISbC
          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_charSbC:
    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 arrISbC [intro]:
    assumes "Arr f"
    shows "arr f"
      using assms arr_charSbC by simp

    lemma arrE [elim]:
    assumes "arr f"
    shows "Arr f"
      using assms arr_charSbC 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_charSbC:
    shows "dom f = (if arr f then C.dom f else C.null)"
      using dom_simp dom_def arr_def arr_charSbC 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_charSbC:
    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_charSbC:
    shows "«f : a → b» ⟷ arr a ∧ arr b ∧ arr f ∧ «f : a →C b»"
      using inclusion arr_charSbC 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_charSbC:
    shows "ide a ⟷ arr a ∧ C.ide a"
      using ide_in_hom C.ide_in_hom in_hom_charSbC by simp

    lemma seq_charSbC:
    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_charSbC dom_charSbC cod_charSbC by (intro seqI, auto)
      show "seq g f ⟹ arr f ∧ arr g ∧ C.seq g f"
        apply (elim seqE, auto)
        using inclusion arr_charSbC 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_charSbC by auto
      show "C.hom a b ∩ Collect Arr ⊆ hom a b"
        using arr_charSbC dom_charSbC cod_charSbC 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_charSbC 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_charSbC by metis

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

    lemma iso_charSbC:
    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_charSbC:
    assumes "iso f"
    shows "inv f = C.inv f"
      by (metis assms C.inverse_unique inclusion_preserves_inverse isoE inverse_unique)

    lemma inverse_arrows_charSbC:
    shows "inverse_arrows f g ⟷ seq f g ∧ C.inverse_arrows f g"
      by (metis C.inverse_arrows_def comp_simp ide_charSbC 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 inclusionFSbC: "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_charFSbC:
    shows "«f : a → b» ⟷ arr a ∧ arr b ∧ «f : a →C b»"
      using arr_charSbC in_hom_charSbC by auto

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

    lemma iso_charFSbC:
    shows "iso f ⟷ arr f ∧ C.iso f"
      using arr_charSbC iso_charSbC 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_charSbC S.inclusion S.dom_charSbC S.cod_charSbC
            S.dom_closed S.cod_closed S.comp_closed S.arr_charSbC 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_charSbC S.in_hom_charFSbC 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