Theory DualCategory
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