# Theory 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 ideI⇩S⇩b⇩C:
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⇩S⇩b⇩C
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⇩S⇩b⇩C
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⇩S⇩b⇩C:
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⇩S⇩b⇩C [intro]:
assumes "Arr f"
shows "arr f"
using assms arr_char⇩S⇩b⇩C by simp

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

lemma seq_char⇩S⇩b⇩C:
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⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C by (intro seqI, auto)
show "seq g f ⟹ arr f ∧ arr g ∧ C.seq g f"
apply (elim seqE, auto)
using inclusion arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C by auto
show "C.hom a b ∩ Collect Arr ⊆ hom a b"
using arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C 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⇩S⇩b⇩C 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⇩S⇩b⇩C by metis

lemma inclusion_preserves_inverse:
assumes "inverse_arrows f g"
shows "C.inverse_arrows f g"
using assms ide_char⇩S⇩b⇩C comp_simp arr_char⇩S⇩b⇩C
by (intro C.inverse_arrowsI, auto)

lemma iso_char⇩S⇩b⇩C:
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⇩S⇩b⇩C:
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⇩S⇩b⇩C:
shows "inverse_arrows f g ⟷ seq f g ∧ C.inverse_arrows f g"
by (metis C.inverse_arrows_def comp_simp ide_char⇩S⇩b⇩C 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⇩F⇩S⇩b⇩C: "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⇩F⇩S⇩b⇩C:
shows "«f : a → b» ⟷ arr a ∧ arr b ∧ «f : a →⇩C b»"
using arr_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C by auto

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

lemma iso_char⇩F⇩S⇩b⇩C:
shows "iso f ⟷ arr f ∧ C.iso f"
using arr_char⇩S⇩b⇩C iso_char⇩S⇩b⇩C 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⇩S⇩b⇩C S.inclusion S.dom_char⇩S⇩b⇩C S.cod_char⇩S⇩b⇩C
S.dom_closed S.cod_closed S.comp_closed S.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C S.in_hom_char⇩F⇩S⇩b⇩C 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
```