# Theory DualCategory

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

chapter DualCategory

theory DualCategory
imports EpiMonoIso
begin

text‹
The locale defined here constructs the dual (opposite) of a category.
The arrows of the dual category are directly identified with the arrows of
the given category and simplification rules are introduced that automatically
eliminate notions defined for the dual category in favor of the corresponding
notions on the original category.  This makes it easy to use the dual of
a category in the same context as the category itself, without having to
worry about whether an arrow belongs to the category or its dual.
›

locale dual_category =
C: category C
for C :: "'a comp"     (infixr "⋅" 55)
begin

definition comp      (infixr "⋅⇧o⇧p" 55)
where "g ⋅⇧o⇧p f ≡ f ⋅ g"

lemma comp_char [simp]:
shows "g ⋅⇧o⇧p f = f ⋅ g"
using comp_def by auto

interpretation partial_composition comp
apply unfold_locales using comp_def C.ex_un_null by metis

notation in_hom ("«_ : _ ← _»")

lemma null_char [simp]:
shows "null = C.null"
by (metis C.null_is_zero(2) null_is_zero(2) comp_def)

lemma ide_char [simp]:
shows "ide a ⟷ C.ide a"
unfolding ide_def C.ide_def by auto

lemma domains_char:
shows "domains f = C.codomains f"
using C.codomains_def domains_def ide_char by auto

lemma codomains_char:
shows "codomains f = C.domains f"
using C.domains_def codomains_def ide_char by auto

interpretation category comp
using C.has_domain_iff_arr C.has_codomain_iff_arr domains_char codomains_char null_char
comp_def C.match_4 C.ext arr_def C.comp_assoc
apply (unfold_locales, auto)
using C.match_2 by metis

lemma is_category:
shows "category comp" ..

end

sublocale dual_category ⊆ category comp
using is_category by auto

context dual_category
begin

lemma dom_char [simp]:
shows "dom f = C.cod f"
by (simp add: C.cod_def dom_def domains_char)

lemma cod_char [simp]:
shows "cod f = C.dom f"
by (simp add: C.dom_def cod_def codomains_char)

lemma arr_char [simp]:
shows "arr f ⟷ C.arr f"
using C.has_codomain_iff_arr has_domain_iff_arr domains_char by auto

lemma hom_char [simp]:
shows "in_hom f b a ⟷ C.in_hom f a b"
by force

lemma seq_char [simp]:
shows "seq g f = C.seq f g"
by simp

lemma iso_char [simp]:
shows "iso f ⟷ C.iso f"
using C.iso_iff_section_and_retraction iso_iff_section_and_retraction
retraction_def section_def
by auto

end

end

```