Theory Category3.Functor
chapter Functor
theory Functor
imports Category ConcreteCategory DualCategory InitialTerminal
begin
text‹
One advantage of the ``object-free'' definition of category is that a functor
from category ‹A› to category ‹B› is simply a function from the type
of arrows of ‹A› to the type of arrows of ‹B› that satisfies certain
conditions: namely, that arrows are mapped to arrows, non-arrows are mapped to
‹null›, and domains, codomains, and composition of arrows are preserved.
›
locale "functor" =
A: category A +
B: category B
for A :: "'a comp" (infixr ‹⋅⇩A› 55)
and B :: "'b comp" (infixr ‹⋅⇩B› 55)
and F :: "'a ⇒ 'b" +
assumes extensionality: "¬A.arr f ⟹ F f = B.null"
and preserves_arr: "A.arr f ⟹ B.arr (F f)"
and preserves_dom [iff]: "A.arr f ⟹ B.dom (F f) = F (A.dom f)"
and preserves_cod [iff]: "A.arr f ⟹ B.cod (F f) = F (A.cod f)"
and preserves_comp [iff]: "A.seq g f ⟹ F (g ⋅⇩A f) = F g ⋅⇩B F f"
begin
notation A.in_hom (‹«_ : _ →⇩A _»›)
notation B.in_hom (‹«_ : _ →⇩B _»›)
lemma preserves_hom [intro]:
assumes "«f : a →⇩A b»"
shows "«F f : F a →⇩B F b»"
using assms B.in_homI
by (metis A.in_homE preserves_arr preserves_cod preserves_dom)
text‹
The following, which is made possible through the presence of ‹null›,
allows us to infer that the subterm @{term f} denotes an arrow if the
term @{term "F f"} denotes an arrow. This is very useful, because otherwise
doing anything with @{term f} would require a separate proof that it is an arrow
by some other means.
›
lemma preserves_reflects_arr [iff]:
shows "B.arr (F f) ⟷ A.arr f"
using preserves_arr extensionality B.not_arr_null by metis
lemma preserves_seq [intro]:
assumes "A.seq g f"
shows "B.seq (F g) (F f)"
using assms by auto
lemma preserves_ide [simp]:
assumes "A.ide a"
shows "B.ide (F a)"
using assms A.ide_in_hom B.ide_in_hom by auto
lemma preserves_iso [simp]:
assumes "A.iso f"
shows "B.iso (F f)"
using assms A.inverse_arrowsE
apply (elim A.isoE A.inverse_arrowsE A.seqE A.ide_compE)
by (metis A.arr_dom_iff_arr B.ide_dom B.inverse_arrows_def B.isoI preserves_arr
preserves_comp preserves_dom)
lemma preserves_isomorphic:
assumes "A.isomorphic a b"
shows "B.isomorphic (F a) (F b)"
by (meson A.isomorphic_def B.isomorphic_def assms preserves_hom preserves_iso)
lemma preserves_section_retraction:
assumes "A.ide (A e m)"
shows "B.ide (B (F e) (F m))"
using assms by (metis A.ide_compE preserves_comp preserves_ide)
lemma preserves_section:
assumes "A.section m"
shows "B.section (F m)"
using assms preserves_section_retraction by blast
lemma preserves_retraction:
assumes "A.retraction e"
shows "B.retraction (F e)"
using assms preserves_section_retraction by blast
lemma preserves_inverse_arrows:
assumes "A.inverse_arrows f g"
shows "B.inverse_arrows (F f) (F g)"
using assms A.inverse_arrows_def B.inverse_arrows_def preserves_section_retraction
by simp
lemma preserves_inv:
assumes "A.iso f"
shows "F (A.inv f) = B.inv (F f)"
using assms preserves_inverse_arrows A.inv_is_inverse B.inv_is_inverse
B.inverse_arrow_unique
by blast
lemma preserves_iso_in_hom [intro]:
assumes "A.iso_in_hom f a b"
shows "B.iso_in_hom (F f) (F a) (F b)"
using assms preserves_hom preserves_iso by blast
end
locale endofunctor =
"functor" A A F
for A :: "'a comp" (infixr ‹⋅› 55)
and F :: "'a ⇒ 'a"
locale faithful_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a ⇒ 'b" +
assumes is_faithful: "⟦ A.par f f'; F f = F f' ⟧ ⟹ f = f'"
begin
lemma locally_reflects_ide:
assumes "«f : a →⇩A a»" and "B.ide (F f)"
shows "A.ide f"
using assms is_faithful
by (metis A.arr_dom_iff_arr A.cod_dom A.dom_dom A.in_homE B.comp_ide_self
B.ide_self_inverse B.comp_arr_inv A.ide_cod preserves_dom)
end
locale full_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a ⇒ 'b" +
assumes is_full: "⟦ A.ide a; A.ide a'; «g : F a' →⇩B F a» ⟧ ⟹ ∃f. «f : a' →⇩A a» ∧ F f = g"
locale fully_faithful_functor =
faithful_functor A B F +
full_functor A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a ⇒ 'b"
begin
lemma reflects_iso:
assumes "«f : a' →⇩A a»" and "B.iso (F f)"
shows "A.iso f"
proof -
from assms obtain g' where g': "B.inverse_arrows (F f) g'" by blast
have 1: "«g' : F a →⇩B F a'»"
using assms g' by (metis B.inv_in_hom B.inverse_unique preserves_hom)
from this obtain g where g: "«g : a →⇩A a'» ∧ F g = g'"
using assms(1) is_full by (metis A.arrI A.ide_cod A.ide_dom A.in_homE)
have "A.inverse_arrows f g"
using assms 1 g g' A.inverse_arrowsI
by (metis A.arr_iff_in_hom A.dom_comp A.in_homE A.seqI' B.inverse_arrowsE
A.cod_comp locally_reflects_ide preserves_comp)
thus ?thesis by auto
qed
lemma reflects_isomorphic:
assumes "A.ide f" and "A.ide f'" and "B.isomorphic (F f) (F f')"
shows "A.isomorphic f f'"
by (metis A.isomorphic_def B.isomorphicE assms(1-3) is_full reflects_iso)
end
locale embedding_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a ⇒ 'b" +
assumes is_embedding: "⟦ A.arr f; A.arr f'; F f = F f' ⟧ ⟹ f = f'"
sublocale embedding_functor ⊆ faithful_functor
using is_embedding by (unfold_locales, blast)
context embedding_functor
begin
lemma reflects_ide:
assumes "B.ide (F f)"
shows "A.ide f"
using assms is_embedding A.ide_in_hom B.ide_in_hom
by (metis A.in_homE B.in_homE A.ide_cod preserves_cod preserves_reflects_arr)
end
locale full_embedding_functor =
embedding_functor A B F +
full_functor A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a ⇒ 'b"
locale essentially_surjective_functor = "functor" +
assumes essentially_surjective: "⋀b. B.ide b ⟹ ∃a. A.ide a ∧ B.isomorphic (F a) b"
locale constant_functor =
A: category A +
B: category B
for A :: "'a comp"
and B :: "'b comp"
and b :: 'b +
assumes value_is_ide: "B.ide b"
begin
definition map
where "map f = (if A.arr f then b else B.null)"
lemma map_simp [simp]:
assumes "A.arr f"
shows "map f = b"
using assms map_def by auto
lemma is_functor:
shows "functor A B map"
using map_def value_is_ide by (unfold_locales, auto)
end
sublocale constant_functor ⊆ "functor" A B map
using is_functor by auto
locale identity_functor =
C: category C
for C :: "'a comp"
begin
definition map :: "'a ⇒ 'a"
where "map f = (if C.arr f then f else C.null)"
lemma map_simp [simp]:
assumes "C.arr f"
shows "map f = f"
using assms map_def by simp
sublocale "functor" C C map
using C.arr_dom_iff_arr C.arr_cod_iff_arr
by (unfold_locales; auto simp add: map_def)
lemma is_functor:
shows "functor C C map"
..
sublocale fully_faithful_functor C C map
using C.arrI by unfold_locales auto
lemma is_fully_faithful:
shows "fully_faithful_functor C C map"
..
end
text ‹
It is convenient to have an easy way to obtain from a category the identity functor
on that category. The following declaration causes the definitions and facts from the
@{locale identity_functor} locale to be inherited by the @{locale category} locale,
including the function @{term map} on arrows that represents the identity functor.
This makes it generally unnecessary to give explicit interpretations of
@{locale identity_functor}.
›
sublocale category ⊆ identity_functor C ..
text‹
Composition of functors coincides with function composition, thanks to the
magic of ‹null›.
›
lemma functor_comp:
assumes "functor A B F" and "functor B C G"
shows "functor A C (G o F)"
proof -
interpret F: "functor" A B F using assms(1) by auto
interpret G: "functor" B C G using assms(2) by auto
show "functor A C (G o F)"
using F.preserves_arr F.extensionality G.extensionality by (unfold_locales, auto)
qed
locale composite_functor =
F: "functor" A B F +
G: "functor" B C G
for A :: "'a comp"
and B :: "'b comp"
and C :: "'c comp"
and F :: "'a ⇒ 'b"
and G :: "'b ⇒ 'c"
begin
abbreviation map
where "map ≡ G o F"
sublocale "functor" A C ‹G o F›
using functor_comp F.functor_axioms G.functor_axioms by blast
lemma is_functor:
shows "functor A C (G o F)"
..
end
lemma comp_functor_identity [simp]:
assumes "functor A B F"
shows "F o identity_functor.map A = F"
proof
interpret "functor" A B F using assms by blast
show "⋀x. (F o A.map) x = F x"
using A.map_def extensionality by simp
qed
lemma comp_identity_functor [simp]:
assumes "functor A B F"
shows "identity_functor.map B o F = F"
proof
interpret "functor" A B F using assms by blast
show "⋀x. (B.map o F) x = F x"
using B.map_def by (metis comp_apply extensionality preserves_arr)
qed
lemma faithful_functors_compose:
assumes "faithful_functor A B F" and "faithful_functor B C G"
shows "faithful_functor A C (G o F)"
proof -
interpret F: faithful_functor A B F
using assms(1) by simp
interpret G: faithful_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "faithful_functor A C (G o F)"
proof
show "⋀f f'. ⟦F.A.par f f'; map f = map f'⟧ ⟹ f = f'"
using F.is_faithful G.is_faithful
by (metis (mono_tags, lifting) F.preserves_arr F.preserves_cod F.preserves_dom o_apply)
qed
qed
lemma full_functors_compose:
assumes "full_functor A B F" and "full_functor B C G"
shows "full_functor A C (G o F)"
proof -
interpret F: full_functor A B F
using assms(1) by simp
interpret G: full_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "full_functor A C (G o F)"
proof
show "⋀a a' g. ⟦F.A.ide a; F.A.ide a'; «g : map a' → map a»⟧
⟹ ∃f. F.A.in_hom f a' a ∧ map f = g"
using F.is_full G.is_full
by (metis F.preserves_ide o_apply)
qed
qed
lemma fully_faithful_functors_compose:
assumes "fully_faithful_functor A B F" and "fully_faithful_functor B C G"
shows "full_functor A C (G o F)"
proof -
interpret F: fully_faithful_functor A B F
using assms(1) by simp
interpret G: fully_faithful_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
interpret faithful_functor A C ‹G o F›
using F.faithful_functor_axioms G.faithful_functor_axioms faithful_functors_compose
by blast
interpret full_functor A C ‹G o F›
using F.full_functor_axioms G.full_functor_axioms full_functors_compose
by blast
show "full_functor A C (G o F)" ..
qed
lemma embedding_functors_compose:
assumes "embedding_functor A B F" and "embedding_functor B C G"
shows "embedding_functor A C (G o F)"
proof -
interpret F: embedding_functor A B F
using assms(1) by simp
interpret G: embedding_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "embedding_functor A C (G o F)"
proof
show "⋀f f'. ⟦F.A.arr f; F.A.arr f'; map f = map f'⟧ ⟹ f = f'"
by (simp add: F.is_embedding G.is_embedding)
qed
qed
lemma full_embedding_functors_compose:
assumes "full_embedding_functor A B F" and "full_embedding_functor B C G"
shows "full_embedding_functor A C (G o F)"
proof -
interpret F: full_embedding_functor A B F
using assms(1) by simp
interpret G: full_embedding_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
interpret embedding_functor A C ‹G o F›
using F.embedding_functor_axioms G.embedding_functor_axioms embedding_functors_compose
by blast
interpret full_functor A C ‹G o F›
using F.full_functor_axioms G.full_functor_axioms full_functors_compose
by blast
show "full_embedding_functor A C (G o F)" ..
qed
lemma essentially_surjective_functors_compose:
assumes "essentially_surjective_functor A B F" and "essentially_surjective_functor B C G"
shows "essentially_surjective_functor A C (G o F)"
proof -
interpret F: essentially_surjective_functor A B F
using assms(1) by simp
interpret G: essentially_surjective_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "essentially_surjective_functor A C (G o F)"
proof
show "⋀c. G.B.ide c ⟹ ∃a. F.A.ide a ∧ G.B.isomorphic (map a) c"
by (metis F.essentially_surjective G.B.isomorphic_transitive
G.essentially_surjective G.preserves_isomorphic comp_def)
qed
qed
locale inverse_functors =
A: category A +
B: category B +
F: "functor" B A F +
G: "functor" A B G
for A :: "'a comp" (infixr ‹⋅⇩A› 55)
and B :: "'b comp" (infixr ‹⋅⇩B› 55)
and F :: "'b ⇒ 'a"
and G :: "'a ⇒ 'b" +
assumes inv: "G o F = identity_functor.map B"
and inv': "F o G = identity_functor.map A"
begin
lemma bij_betw_arr_sets:
shows "bij_betw F (Collect B.arr) (Collect A.arr)"
using inv inv'
apply (intro bij_betwI)
apply auto
using comp_eq_dest_lhs by force+
end
locale isomorphic_categories =
A: category A +
B: category B
for A :: "'a comp" (infixr ‹⋅⇩A› 55)
and B :: "'b comp" (infixr ‹⋅⇩B› 55) +
assumes iso: "∃F G. inverse_functors A B F G"
sublocale inverse_functors ⊆ isomorphic_categories A B
using inverse_functors_axioms by (unfold_locales, auto)
lemma inverse_functors_sym:
assumes "inverse_functors A B F G"
shows "inverse_functors B A G F"
proof -
interpret inverse_functors A B F G using assms by auto
show ?thesis using inv inv' by (unfold_locales, auto)
qed
text ‹
Inverse functors uniquely determine each other.
›
lemma inverse_functor_unique:
assumes "inverse_functors C D F G" and "inverse_functors C D F G'"
shows "G = G'"
proof -
interpret FG: inverse_functors C D F G using assms(1) by auto
interpret FG': inverse_functors C D F G' using assms(2) by auto
show "G = G'"
using FG.G.extensionality FG'.G.extensionality FG'.inv FG.inv'
by (metis FG'.G.functor_axioms FG.G.functor_axioms comp_assoc comp_identity_functor
comp_functor_identity)
qed
lemma inverse_functor_unique':
assumes "inverse_functors C D F G" and "inverse_functors C D F' G"
shows "F = F'"
using assms inverse_functors_sym inverse_functor_unique by blast
locale invertible_functor =
A: category A +
B: category B +
G: "functor" A B G
for A :: "'a comp" (infixr ‹⋅⇩A› 55)
and B :: "'b comp" (infixr ‹⋅⇩B› 55)
and G :: "'a ⇒ 'b" +
assumes invertible: "∃F. inverse_functors A B F G"
begin
lemma has_unique_inverse:
shows "∃!F. inverse_functors A B F G"
using invertible inverse_functor_unique' by blast
definition inv
where "inv ≡ THE F. inverse_functors A B F G"
interpretation inverse_functors A B inv G
using inv_def has_unique_inverse theI' [of "λF. inverse_functors A B F G"]
by simp
lemma inv_is_inverse:
shows "inverse_functors A B inv G" ..
sublocale inverse_functors A B inv G
using inv_is_inverse by simp
lemma is_surjective_on_objects:
shows "G ` Collect A.ide ⊇ Collect B.ide"
by (metis (no_types, lifting) B.category_axioms B.map_simp
CollectD CollectI F.preserves_ide category.ideD(1) image_eqI
inv o_apply subsetI)
sublocale fully_faithful_functor A B G
proof -
obtain F where F: "inverse_functors A B F G"
using invertible by auto
interpret FG: inverse_functors A B F G
using F by simp
show "fully_faithful_functor A B G"
proof
fix f f'
assume par: "A.par f f'" and eq: "G f = G f'"
show "f = f'"
using par eq FG.inv'
by (metis A.map_simp comp_apply)
next
fix a a' g
assume a: "A.ide a" and a': "A.ide a'" and g: "«g : G a →⇩B G a'»"
show "∃f. «f : a →⇩A a'» ∧ G f = g"
by (metis A.ideD(1) A.map_simp B.arrI B.map_simp FG.F.preserves_hom FG.inv FG.inv'
a a' g o_apply)
qed
qed
lemma is_fully_faithful:
shows "fully_faithful_functor A B G"
..
lemma preserves_terminal:
assumes "A.terminal a"
shows "B.terminal (G a)"
proof
show 0: "B.ide (G a)" using assms G.preserves_ide A.terminal_def by blast
fix b :: 'b
assume b: "B.ide b"
show "∃!g. «g : b →⇩B G a»"
proof
let ?F = "SOME F. inverse_functors A B F G"
from invertible have F: "inverse_functors A B ?F G"
using someI_ex [of "λF. inverse_functors A B F G"] by fast
interpret inverse_functors A B ?F G using F by auto
let ?P = "λf. «f : ?F b →⇩A a»"
have 1: "∃!f. ?P f" using assms b A.terminal_def by simp
hence 2: "?P (THE f. ?P f)" by (metis (no_types, lifting) theI')
thus "«G (THE f. ?P f) : b →⇩B G a»"
using b apply (elim A.in_homE, intro B.in_homI, auto)
using B.ideD(1) B.map_simp comp_def inv by metis
hence 3: "«(THE f. ?P f) : ?F b →⇩A a»"
using assms 2 b F by simp
fix g :: 'b
assume g: "«g : b →⇩B G a»"
have "?F (G a) = a"
using assms(1) A.terminal_def inv' A.map_simp
by (metis 0 B.ideD(1) G.preserves_reflects_arr comp_eq_dest_lhs)
hence "«?F g : ?F b →⇩A a»"
using assms(1) g A.terminal_def inv
by (elim B.in_homE, auto)
hence "?F g = (THE f. ?P f)" using assms 1 3 A.terminal_def by blast
thus "g = G (THE f. ?P f)"
using inv g by (metis B.in_homE B.map_simp comp_def)
qed
qed
end
context full_embedding_functor
begin
lemma is_invertible_if_surjective_on_objects:
assumes "F ` Collect A.ide ⊇ Collect B.ide"
shows "invertible_functor A B F"
and "inverse_functors A B (λy. if B.arr y then inv_into (Collect A.arr) F y else A.null) F"
proof -
have *: "F ` Collect A.ide = Collect B.ide"
using assms preserves_reflects_arr by auto
have inj: "inj_on F (Collect A.arr)"
using is_embedding inj_on_def by blast
have inj': "inj_on F (Collect A.ide)"
by (simp add: inj_on_def is_embedding)
have surj: "F ` Collect A.arr = Collect B.arr"
proof
show "F ` Collect A.arr ⊆ Collect B.arr"
using preserves_reflects_arr by auto
show "Collect B.arr ⊆ F ` Collect A.arr"
proof
fix g
assume g: "g ∈ Collect B.arr"
let ?a = "inv_into (Collect A.ide) F (B.dom g)"
let ?a' = "inv_into (Collect A.ide) F (B.cod g)"
have a: "A.ide ?a ∧ F ?a = B.dom g"
using * g by (simp add: f_inv_into_f reflects_ide)
have a': "A.ide ?a' ∧ F ?a' = B.cod g"
using * g by (simp add: f_inv_into_f reflects_ide)
have "«g : F ?a →⇩B F ?a'»"
using g a a' by auto
hence "∃f. «f : ?a →⇩A ?a'» ∧ F f = g"
using a a' is_full by blast
thus "g ∈ F ` Collect A.arr" by blast
qed
qed
let ?G = "λy. if B.arr y then inv_into (Collect A.arr) F y else A.null"
show "inverse_functors A B ?G F"
proof
show "⋀f. ¬ B.arr f ⟹ ?G f = A.null"
by simp
show 1: "⋀f. B.arr f ⟹ A.arr (?G f)"
using assms inj surj inv_into_into
by (metis (full_types) mem_Collect_eq)
show 2: "⋀f. B.arr f ⟹ A.dom (?G f) = ?G (B.dom f)"
proof -
fix f
assume f: "B.arr f"
have "F (A.dom (?G f)) = B.dom f"
proof -
have "F (A.dom (?G f)) = B.dom (F (inv_into (Collect A.arr) F f))"
using f 1 preserves_dom by simp
also have "... = B.dom f"
using f f_inv_into_f by (metis CollectI surj)
finally show ?thesis by blast
qed
thus "A.dom (?G f) = ?G (B.dom f)"
using f
by (metis 1 A.arr_dom B.arr_dom inj inv_into_f_f mem_Collect_eq)
qed
show 3: "⋀f. B.arr f ⟹ A.cod (?G f) = ?G (B.cod f)"
proof -
fix f
assume f: "B.arr f"
have "F (A.cod (?G f)) = B.cod f"
proof -
have "F (A.cod (?G f)) = B.cod (F (inv_into (Collect A.arr) F f))"
using f 1 preserves_cod by simp
also have "... = B.cod f"
using f f_inv_into_f by (metis CollectI surj)
finally show ?thesis by blast
qed
thus "A.cod (?G f) = ?G (B.cod f)"
using f
by (metis 1 A.arr_cod B.arr_cod inj inv_into_f_f mem_Collect_eq)
qed
fix f g
assume fg: "B.seq g f"
show "?G (B g f) = A (?G g) (?G f)"
using assms fg 1 2 3 inj surj f_inv_into_f inj_on_def inv_into_into
preserves_comp
by (auto simp add: f_inv_into_f is_embedding)
next
show "F ∘ ?G = B.map"
using inj surj f_inv_into_f A.not_arr_null B.map_def extensionality
by (auto simp add: f_inv_into_f)
show "?G ∘ F = A.map"
using inj surj A.extensionality by auto
qed
hence "∃G. inverse_functors A B G F"
by blast
thus "invertible_functor A B F"
using functor_axioms functor_def invertible_functor.intro
invertible_functor_axioms.intro
by blast
qed
end
locale dual_functor =
F: "functor" A B F +
Aop: dual_category A +
Bop: dual_category B
for A :: "'a comp" (infixr ‹⋅⇩A› 55)
and B :: "'b comp" (infixr ‹⋅⇩B› 55)
and F :: "'a ⇒ 'b"
begin
notation Aop.comp (infixr ‹⋅⇩A⇧o⇧p› 55)
notation Bop.comp (infixr ‹⋅⇩B⇧o⇧p› 55)
abbreviation map
where "map ≡ F"
lemma is_functor:
shows "functor Aop.comp Bop.comp map"
using F.extensionality by (unfold_locales, auto)
end
sublocale dual_functor ⊆ "functor" Aop.comp Bop.comp map
using is_functor by auto
text ‹
A bijection from a set ‹S› to the set of arrows of a category ‹C› induces an isomorphic
copy of ‹C› having ‹S› as its set of arrows, assuming that there exists some ‹n ∉ S›
to serve as the null.
›
context category
begin
lemma bij_induces_invertible_functor:
assumes "bij_betw φ S (Collect arr)" and "n ∉ S"
shows "∃C'. Collect (partial_composition.arr C') = S ∧
invertible_functor C' C (λi. if partial_composition.arr C' i then φ i else null)"
proof -
define ψ where "ψ = (λf. if arr f then inv_into S φ f else n)"
have ψ: "bij_betw ψ (Collect arr) S"
using assms(1) ψ_def bij_betw_inv_into
by (metis (no_types, lifting) bij_betw_cong mem_Collect_eq)
have φ_ψ [simp]: "⋀f. arr f ⟹ φ (ψ f) = f"
using assms(1) ψ ψ_def bij_betw_inv_into_right by fastforce
have ψ_φ [simp]: "⋀i. i ∈ S ⟹ ψ (φ i) = i"
unfolding ψ_def
using assms(1) ψ bij_betw_inv_into_left [of φ S "Collect arr"]
by (metis bij_betw_def image_eqI mem_Collect_eq)
define C' where "C' = (λi j. if i ∈ S ∧ j ∈ S ∧ seq (φ i) (φ j) then ψ (φ i ⋅ φ j) else n)"
interpret C': partial_composition C'
using assms(1-2) C'_def ψ_def
by unfold_locales metis
have null_char: "C'.null = n"
using assms(1-2) C'_def ψ_def C'.null_eqI by metis
have ide_char: "⋀i. C'.ide i ⟷ i ∈ S ∧ ide (φ i)"
proof
fix i
assume i: "C'.ide i"
show "i ∈ S ∧ ide (φ i)"
proof (unfold ide_def, intro conjI)
show 1: "φ i ⋅ φ i ≠ null"
using i assms(1) C'.ide_def C'_def null_char by auto
show 2: "i ∈ S"
using 1 assms(1) by (metis C'.ide_def C'_def i)
show "∀f. (f ⋅ φ i ≠ null ⟶ f ⋅ φ i = f) ∧ (φ i ⋅ f ≠ null ⟶ φ i ⋅ f = f)"
proof (intro allI conjI impI)
show "⋀f. f ⋅ φ i ≠ null ⟹ f ⋅ φ i = f"
proof -
fix f
assume f: "f ⋅ φ i ≠ null"
hence 1: "arr f ∧ arr (φ i) ∧ seq f (φ i)"
by (meson seqE ext)
have "f ⋅ φ i = φ (C' (ψ f) i)"
using 1 2 C'_def null_char
by (metis (no_types, lifting) φ_ψ ψ bij_betw_def image_eqI mem_Collect_eq)
also have "... = f"
by (metis 1 C'.ide_def C'_def φ_ψ ψ assms(2) bij_betw_def i image_eqI
mem_Collect_eq null_char)
finally show "f ⋅ φ i = f" by simp
qed
show "⋀f. φ i ⋅ f ≠ null ⟹ φ i ⋅ f = f"
proof -
fix f
assume f: "φ i ⋅ f ≠ null"
hence 1: "arr f ∧ arr (φ i) ∧ seq (φ i) f"
by (meson seqE ext)
show "φ i ⋅ f = f"
using 1 2 C'_def null_char ψ
by (metis (no_types, lifting) ‹⋀f. f ⋅ φ i ≠ null ⟹ f ⋅ φ i = f›
ide_char' codomains_null comp_cod_arr has_codomain_iff_arr
comp_ide_arr)
qed
qed
qed
next
fix i
assume i: "i ∈ S ∧ ide (φ i)"
have "ψ (φ i) ∈ S"
using i assms(1)
by (metis ψ bij_betw_def ideD(1) image_eqI mem_Collect_eq)
show "C'.ide i"
using assms(2) i C'_def null_char comp_arr_ide comp_ide_arr
apply (unfold C'.ide_def, intro conjI allI impI)
apply auto[1]
by force+
qed
have dom: "⋀i. i ∈ S ⟹ ψ (dom (φ i)) ∈ C'.domains i"
proof -
fix i
assume i: "i ∈ S"
have 1: "C'.ide (ψ (dom (φ i)))"
by (metis φ_ψ ψ ψ_φ ψ_def arr_dom assms(2) bij_betw_def i ide_char ide_dom
image_eqI mem_Collect_eq)
moreover have "C' i (ψ (dom (φ i))) ≠ C'.null"
by (metis C'_def φ_ψ ψ_φ ψ_def assms(2) calculation comp_arr_dom i ide_char
null_char)
ultimately show "ψ (dom (φ i)) ∈ C'.domains i"
using C'.domains_def by simp
qed
have cod: "⋀i. i ∈ S ⟹ ψ (cod (φ i)) ∈ C'.codomains i"
proof -
fix i
assume i: "i ∈ S"
have 1: "C'.ide (ψ (cod (φ i)))"
by (metis φ_ψ ψ ψ_φ ψ_def arr_cod assms(2) bij_betw_def i ide_char ide_cod
image_eqI mem_Collect_eq)
moreover have "C' (ψ (cod (φ i))) i ≠ C'.null"
by (metis 1 C'_def φ_ψ ψ_φ ψ_def assms(2) comp_cod_arr i ide_char null_char)
ultimately show "ψ (cod (φ i)) ∈ C'.codomains i"
using C'.codomains_def by simp
qed
have arr_char: "⋀i. C'.arr i ⟷ i ∈ S"
by (metis (mono_tags, lifting) C'.arr_def C'.codomains_def C'.domains_def
C'_def assms(2) dom mem_Collect_eq null_char C'.cod_in_codomains C'.dom_in_domains)
have seq_char: "⋀i j. C'.seq i j ⟷ i ∈ S ∧ j ∈ S ∧ seq (φ i) (φ j)"
using assms(1-2) C'_def arr_char null_char
apply simp
using ψ bij_betw_apply by fastforce
interpret C': category C'
proof
show "⋀g f. C' g f ≠ C'.null ⟹ C'.seq g f"
using C'_def null_char seq_char by fastforce
show "⋀f. (C'.domains f ≠ {}) = (C'.codomains f ≠ {})"
using dom cod null_char arr_char C'.arr_def by blast
show "⋀h g f. ⟦C'.seq h g; C'.seq (C' h g) f⟧ ⟹ C'.seq g f"
using seq_char
apply simp
using C'_def by fastforce
show "⋀h g f. ⟦C'.seq h (C' g f); C'.seq g f⟧ ⟹ C'.seq h g"
using seq_char
apply simp
using C'_def by fastforce
show "⋀g f h. ⟦C'.seq g f; C'.seq h g⟧ ⟹ C'.seq (C' h g) f"
using seq_char arr_char
apply simp
using C'_def by auto
show "⋀g f h. ⟦C'.seq g f; C'.seq h g⟧ ⟹ C' (C' h g) f = C' h (C' g f)"
using seq_char arr_char C'_def comp_assoc assms(2)
apply simp by presburger
qed
have dom_char: "C'.dom = (λi. if i ∈ S then ψ (dom (φ i)) else n)"
using dom arr_char null_char C'.dom_eqI' C'.arr_def C'.dom_def by metis
have cod_char: "C'.cod = (λi. if i ∈ S then ψ (cod (φ i)) else n)"
using cod arr_char null_char C'.cod_eqI' C'.arr_def C'.cod_def by metis
interpret φ: "functor" C' C ‹λi. if C'.arr i then φ i else null›
using arr_char null_char dom_char cod_char seq_char φ_ψ ψ_φ ψ_def C'.not_arr_null C'_def
C'.arr_dom C'.arr_cod
apply unfold_locales
apply simp_all
by metis+
interpret ψ: "functor" C C' ψ
using ψ_def null_char arr_char
apply unfold_locales
apply simp
apply (metis (no_types, lifting) ψ bij_betw_def image_eqI mem_Collect_eq)
apply (metis (no_types, lifting) φ_ψ ψ bij_betw_def dom_char image_eqI mem_Collect_eq)
apply (metis (no_types, lifting) φ_ψ ψ bij_betw_def cod_char image_eqI mem_Collect_eq)
by (metis (no_types, lifting) C'_def φ_ψ ψ bij_betw_def seqE image_eqI mem_Collect_eq)
interpret φψ: inverse_functors C' C ψ ‹λi. if C'.arr i then φ i else null›
proof
show "ψ ∘ (λi. if C'.arr i then φ i else null) = C'.map"
by (auto simp add: C'.extensionality ψ.extensionality arr_char)
show "(λi. if C'.arr i then φ i else null) ∘ ψ = map"
by (auto simp add: extensionality)
qed
have "invertible_functor C' C (λi. if C'.arr i then φ i else null)"
using φψ.inverse_functors_axioms by unfold_locales auto
thus ?thesis
using arr_char by blast
qed
corollary (in category) finite_imp_ex_iso_nat_comp:
assumes "finite (Collect arr)"
shows "∃C' :: nat comp. isomorphic_categories C' C"
proof -
obtain n :: nat and φ where φ: "bij_betw φ {0..<n} (Collect arr)"
using assms ex_bij_betw_nat_finite by blast
obtain C' where C': "Collect (partial_composition.arr C') = {0..<n} ∧
invertible_functor C' (⋅)
(λi. if partial_composition.arr C' i then φ i else null)"
using φ bij_induces_invertible_functor [of φ "{0..<n}"] by auto
interpret φ: invertible_functor C' C ‹λi. if partial_composition.arr C' i then φ i else null›
using C' by simp
show ?thesis
using φ.isomorphic_categories_axioms by blast
qed
end
text ‹
We now prove the result, advertised earlier in theory ‹ConcreteCategory›,
that any category is in fact isomorphic to the concrete category formed from it in
the obvious way.
›
context category
begin
interpretation CC: concrete_category ‹Collect ide› hom id ‹λ_ _ _ g f. g ⋅ f›
using comp_arr_dom comp_cod_arr comp_assoc
by (unfold_locales, auto)
interpretation F: "functor" C CC.COMP
‹λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null›
by (unfold_locales, auto simp add: in_homI)
interpretation G: "functor" CC.COMP C ‹λF. if CC.arr F then CC.Map F else null›
using CC.Map_in_Hom CC.seq_char
by (unfold_locales, auto)
interpretation FG: inverse_functors C CC.COMP
‹λF. if CC.arr F then CC.Map F else null›
‹λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null›
proof
show "(λF. if CC.arr F then CC.Map F else null) ∘
(λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null) =
map"
using CC.arr_char map_def by fastforce
show "(λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null) ∘
(λF. if CC.arr F then CC.Map F else null) =
CC.map"
using CC.MkArr_Map G.preserves_arr G.preserves_cod G.preserves_dom
CC.extensionality
by auto
qed
theorem is_isomorphic_to_concrete_category:
shows "isomorphic_categories C CC.COMP"
..
end
end