# Theory DiscreteCategory

```(*  Title:       DiscreteCategory
Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter DiscreteCategory

theory DiscreteCategory
imports Category
begin

text‹
The locale defined here permits us to construct a discrete category having
a specified set of objects, assuming that the set does not exhaust the elements
of its type.  In that case, we have the convenient situation that the arrows of
the category can be directly identified with the elements of the given set,
rather than having to pass between the two via tedious coercion maps.
If it cannot be guaranteed that the given set is not the universal set at its type,
then the more general discrete category construction defined (using coercions)
in ‹FreeCategory› can be used.
›

locale discrete_category =
fixes Obj :: "'a set"
and Null :: 'a
assumes Null_not_in_Obj: "Null ∉ Obj"
begin

definition comp :: "'a comp"      (infixr "⋅" 55)
where "y ⋅ x ≡ (if x ∈ Obj ∧ x = y then x else Null)"

interpretation partial_composition comp
apply unfold_locales
using comp_def by metis

lemma null_char:
shows "null = Null"
using comp_def null_def by auto

lemma ide_char [iff]:
shows "ide f ⟷ f ∈ Obj"
using comp_def null_char ide_def Null_not_in_Obj by auto

lemma domains_char:
shows "domains f = {x. x ∈ Obj ∧ x = f}"
unfolding domains_def
using ide_char ide_def comp_def null_char by metis

theorem is_category:
shows "category comp"
using comp_def
apply unfold_locales
using arr_def null_char self_domain_iff_ide ide_char
apply fastforce
using null_char self_codomain_iff_ide domains_char codomains_def ide_char
apply fastforce
apply (metis not_arr_null null_char)
apply (metis not_arr_null null_char)
by auto

end

sublocale discrete_category ⊆ category comp
using is_category by auto

context discrete_category
begin

lemma arr_char [iff]:
shows "arr f ⟷ f ∈ Obj"
using comp_def comp_cod_arr
by (metis empty_iff has_codomain_iff_arr not_arr_null null_char self_codomain_iff_ide ide_char)

lemma dom_char [simp]:
shows "dom f = (if f ∈ Obj then f else null)"
using arr_def dom_def arr_char ideD(2) by auto

lemma cod_char [simp]:
shows "cod f = (if f ∈ Obj then f else null)"
using arr_def in_homE cod_def ideD(3) by auto

lemma comp_char [simp]:
shows "comp g f = (if f ∈ Obj ∧ f = g then f else null)"
using comp_def null_char by auto

lemma is_discrete:
shows "ide = arr"
using arr_char ide_char by auto

lemma seq_char [iff]:
shows "seq f g ⟷ ide f ∧ f = g"
using is_discrete by (metis (full_types) ide_def seqE)

end

end
```