Theory Cfunc
section ‹Basic Types and Operators for the Category of Sets›
theory Cfunc
imports Main "HOL-Eisbach.Eisbach"
begin
typedecl cset
typedecl cfunc
text ‹We declare @{type cset} and @{type cfunc} as types to represent the sets and functions within
ETCS, as distinct from HOL sets and functions.
The "c" prefix here is intended to stand for "category", and emphasises that these are
category-theoretic objects.›
text ‹The axiomatization below corresponds to Axiom 1 (Sets Is a Category) in Halvorson.›
axiomatization
domain :: "cfunc ⇒ cset" and
codomain :: "cfunc ⇒ cset" and
comp :: "cfunc ⇒ cfunc ⇒ cfunc" (infixr "∘⇩c" 55) and
id :: "cset ⇒ cfunc" ("id⇩c")
where
domain_comp: "domain g = codomain f ⟹ domain (g ∘⇩c f) = domain f" and
codomain_comp: "domain g = codomain f ⟹ codomain (g ∘⇩c f) = codomain g" and
comp_associative: "domain h = codomain g ⟹ domain g = codomain f ⟹ h ∘⇩c (g ∘⇩c f) = (h ∘⇩c g) ∘⇩c f" and
id_domain: "domain (id X) = X" and
id_codomain: "codomain (id X) = X" and
id_right_unit: "f ∘⇩c id (domain f) = f" and
id_left_unit: "id (codomain f) ∘⇩c f = f"
text ‹We define a neater way of stating types and lift the type axioms into lemmas using it.›
definition cfunc_type :: "cfunc ⇒ cset ⇒ cset ⇒ bool" ("_ : _ → _" [50, 50, 50]50) where
"(f : X → Y) ⟷ (domain f = X ∧ codomain f = Y)"
lemma comp_type:
"f : X → Y ⟹ g : Y → Z ⟹ g ∘⇩c f : X → Z"
by (simp add: cfunc_type_def codomain_comp domain_comp)
lemma comp_associative2:
"f : X → Y ⟹ g : Y → Z ⟹ h : Z → W ⟹ h ∘⇩c (g ∘⇩c f) = (h ∘⇩c g) ∘⇩c f"
by (simp add: cfunc_type_def comp_associative)
lemma id_type: "id X : X → X"
unfolding cfunc_type_def using id_domain id_codomain by auto
lemma id_right_unit2: "f : X → Y ⟹ f ∘⇩c id X = f"
unfolding cfunc_type_def using id_right_unit by auto
lemma id_left_unit2: "f : X → Y ⟹ id Y ∘⇩c f = f"
unfolding cfunc_type_def using id_left_unit by auto
subsection ‹Tactics for Applying Typing Rules›
text ‹ETCS lemmas often have assumptions on its ETCS type, which can often be cumbersome to prove.
To simplify proofs involving ETCS types, we provide proof methods that apply type rules in a
structured way to prove facts about ETCS function types.
The type rules state the types of the basic constants and operators of ETCS and are declared as
a named set of theorems called $type\_rule$.›
named_theorems type_rule
declare id_type[type_rule]
declare comp_type[type_rule]
ML_file ‹typecheck.ml›
subsubsection ‹typecheck\_cfuncs: Tactic to Construct Type Facts›
method_setup typecheck_cfuncs =
‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> typecheck_cfuncs_method›
"Check types of cfuncs in current goal and add as assumptions of the current goal"
method_setup typecheck_cfuncs_all =
‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> typecheck_cfuncs_all_method›
"Check types of cfuncs in all subgoals and add as assumptions of the current goal"
method_setup typecheck_cfuncs_prems =
‹Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> typecheck_cfuncs_prems_method›
"Check types of cfuncs in assumptions of the current goal and add as assumptions of the current goal"
subsubsection ‹etcs\_rule: Tactic to Apply Rules with ETCS Typechecking›
method_setup etcs_rule =
‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
-- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> ETCS_resolve_method›
"apply rule with ETCS type checking"
subsubsection ‹etcs\_subst: Tactic to Apply Substitutions with ETCS Typechecking›
method_setup etcs_subst =
‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
-- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> ETCS_subst_method›
"apply substitution with ETCS type checking"
method etcs_assocl declares type_rule = (etcs_subst comp_associative2)+
method etcs_assocr declares type_rule = (etcs_subst sym[OF comp_associative2])+
method_setup etcs_subst_asm =
‹Runtime.exn_trace (fn _ => Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
-- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> ETCS_subst_asm_method)›
"apply substitution to assumptions of the goal, with ETCS type checking"
method etcs_assocl_asm declares type_rule = (etcs_subst_asm comp_associative2)+
method etcs_assocr_asm declares type_rule = (etcs_subst_asm sym[OF comp_associative2])+
subsubsection ‹etcs\_erule: Tactic to Apply Elimination Rules with ETCS Typechecking›
method_setup etcs_erule =
‹Scan.repeats (Scan.unless (Scan.lift (Args.$$$ "type_rule" -- Args.colon)) Attrib.multi_thm)
-- Scan.option ((Scan.lift (Args.$$$ "type_rule" -- Args.colon)) |-- Attrib.thms)
>> ETCS_eresolve_method›
"apply erule with ETCS type checking"
subsection ‹Monomorphisms, Epimorphisms and Isomorphisms›
subsubsection ‹Monomorphisms›
definition monomorphism :: "cfunc ⇒ bool" where
"monomorphism f ⟷ (∀ g h.
(codomain g = domain f ∧ codomain h = domain f) ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"
lemma monomorphism_def2:
"monomorphism f ⟷ (∀ g h A X Y. g : A → X ∧ h : A → X ∧ f : X → Y ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"
unfolding monomorphism_def by (smt cfunc_type_def domain_comp)
lemma monomorphism_def3:
assumes "f : X → Y"
shows "monomorphism f ⟷ (∀ g h A. g : A → X ∧ h : A → X ⟶ (f ∘⇩c g = f ∘⇩c h ⟶ g = h))"
unfolding monomorphism_def2 using assms cfunc_type_def by auto
text ‹The lemma below corresponds to Exercise 2.1.7a in Halvorson.›
lemma comp_monic_imp_monic:
assumes "domain g = codomain f"
shows "monomorphism (g ∘⇩c f) ⟹ monomorphism f"
unfolding monomorphism_def
proof clarify
fix s t
assume gf_monic: "∀s. ∀t.
codomain s = domain (g ∘⇩c f) ∧ codomain t = domain (g ∘⇩c f) ⟶
(g ∘⇩c f) ∘⇩c s = (g ∘⇩c f) ∘⇩c t ⟶ s = t"
assume codomain_s: "codomain s = domain f"
assume codomain_t: "codomain t = domain f"
assume "f ∘⇩c s = f ∘⇩c t"
then have "(g ∘⇩c f) ∘⇩c s = (g ∘⇩c f) ∘⇩c t"
by (metis assms codomain_s codomain_t comp_associative)
then show "s = t"
using gf_monic codomain_s codomain_t domain_comp by (simp add: assms)
qed
lemma comp_monic_imp_monic':
assumes "f : X → Y" "g : Y → Z"
shows "monomorphism (g ∘⇩c f) ⟹ monomorphism f"
by (metis assms cfunc_type_def comp_monic_imp_monic)
text ‹The lemma below corresponds to Exercise 2.1.7c in Halvorson.›
lemma composition_of_monic_pair_is_monic:
assumes "codomain f = domain g"
shows "monomorphism f ⟹ monomorphism g ⟹ monomorphism (g ∘⇩c f)"
unfolding monomorphism_def
proof clarify
fix h k
assume f_mono: "∀s t.
codomain s = domain f ∧ codomain t = domain f ⟶ f ∘⇩c s = f ∘⇩c t ⟶ s = t"
assume g_mono: "∀s. ∀t.
codomain s = domain g ∧ codomain t = domain g ⟶ g ∘⇩c s = g ∘⇩c t ⟶ s = t"
assume codomain_k: "codomain k = domain (g ∘⇩c f)"
assume codomain_h: "codomain h = domain (g ∘⇩c f)"
assume gfh_eq_gfk: "(g ∘⇩c f) ∘⇩c k = (g ∘⇩c f) ∘⇩c h"
have "g ∘⇩c (f ∘⇩c h) = (g ∘⇩c f) ∘⇩c h"
by (simp add: assms codomain_h comp_associative domain_comp)
also have "... = (g ∘⇩c f) ∘⇩c k"
by (simp add: gfh_eq_gfk)
also have "... = g ∘⇩c (f ∘⇩c k)"
by (simp add: assms codomain_k comp_associative domain_comp)
ultimately have "f ∘⇩c h = f ∘⇩c k"
using assms cfunc_type_def codomain_h codomain_k comp_type domain_comp g_mono by auto
then show "k = h"
by (simp add: codomain_h codomain_k domain_comp f_mono assms)
qed
subsubsection ‹Epimorphisms›
definition epimorphism :: "cfunc ⇒ bool" where
"epimorphism f ⟷ (∀ g h.
(domain g = codomain f ∧ domain h = codomain f) ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"
lemma epimorphism_def2:
"epimorphism f ⟷ (∀ g h A X Y. f : X → Y ∧ g : Y → A ∧ h : Y → A ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"
unfolding epimorphism_def by (smt cfunc_type_def codomain_comp)
lemma epimorphism_def3:
assumes "f : X → Y"
shows "epimorphism f ⟷ (∀ g h A. g : Y → A ∧ h : Y → A ⟶ (g ∘⇩c f = h ∘⇩c f ⟶ g = h))"
unfolding epimorphism_def2 using assms cfunc_type_def by auto
text ‹The lemma below corresponds to Exercise 2.1.7b in Halvorson.›
lemma comp_epi_imp_epi:
assumes "domain g = codomain f"
shows "epimorphism (g ∘⇩c f) ⟹ epimorphism g"
unfolding epimorphism_def
proof clarify
fix s t
assume gf_epi: "∀s. ∀t.
domain s = codomain (g ∘⇩c f) ∧ domain t = codomain (g ∘⇩c f) ⟶
s ∘⇩c g ∘⇩c f = t ∘⇩c g ∘⇩c f ⟶ s = t"
assume domain_s: "domain s = codomain g"
assume domain_t: "domain t = codomain g"
assume sf_eq_tf: "s ∘⇩c g = t ∘⇩c g"
from sf_eq_tf have "s ∘⇩c (g ∘⇩c f) = t ∘⇩c (g ∘⇩c f)"
by (simp add: assms comp_associative domain_s domain_t)
then show "s = t"
using gf_epi codomain_comp domain_s domain_t by (simp add: assms)
qed
text ‹The lemma below corresponds to Exercise 2.1.7d in Halvorson.›
lemma composition_of_epi_pair_is_epi:
assumes "codomain f = domain g"
shows "epimorphism f ⟹ epimorphism g ⟹ epimorphism (g ∘⇩c f)"
unfolding epimorphism_def
proof clarify
fix h k
assume f_epi :"∀ s h.
(domain s = codomain f ∧ domain h = codomain f) ⟶ (s ∘⇩c f = h ∘⇩c f ⟶ s = h)"
assume g_epi :"∀ s h.
(domain s = codomain g ∧ domain h = codomain g) ⟶ (s ∘⇩c g = h ∘⇩c g ⟶ s = h)"
assume domain_k: "domain k = codomain (g ∘⇩c f)"
assume domain_h: "domain h = codomain (g ∘⇩c f)"
assume hgf_eq_kgf: "h ∘⇩c (g ∘⇩c f) = k ∘⇩c (g ∘⇩c f)"
have "(h ∘⇩c g) ∘⇩c f = h ∘⇩c (g ∘⇩c f)"
by (simp add: assms codomain_comp comp_associative domain_h)
also have "... = k ∘⇩c (g ∘⇩c f)"
by (simp add: hgf_eq_kgf)
also have "... =(k ∘⇩c g) ∘⇩c f "
by (simp add: assms codomain_comp comp_associative domain_k)
ultimately have "h ∘⇩c g = k ∘⇩c g"
by (simp add: assms codomain_comp domain_comp domain_h domain_k f_epi)
then show "h = k"
by (simp add: codomain_comp domain_h domain_k g_epi assms)
qed
subsubsection ‹Isomorphisms›
definition isomorphism :: "cfunc ⇒ bool" where
"isomorphism f ⟷ (∃ g. domain g = codomain f ∧ codomain g = domain f ∧
g ∘⇩c f = id(domain f) ∧ f ∘⇩c g = id(domain g))"
lemma isomorphism_def2:
"isomorphism f ⟷ (∃ g X Y. f : X → Y ∧ g : Y → X ∧ g ∘⇩c f = id X ∧ f ∘⇩c g = id Y)"
unfolding isomorphism_def cfunc_type_def by auto
lemma isomorphism_def3:
assumes "f : X → Y"
shows "isomorphism f ⟷ (∃ g. g : Y → X ∧ g ∘⇩c f = id X ∧ f ∘⇩c g = id Y)"
using assms unfolding isomorphism_def2 cfunc_type_def by auto
definition inverse :: "cfunc ⇒ cfunc" ("_❙¯" [1000] 999) where
"inverse f = (THE g. g : codomain f → domain f ∧ g ∘⇩c f = id(domain f) ∧ f ∘⇩c g = id(codomain f))"
lemma inverse_def2:
assumes "isomorphism f"
shows "f❙¯ : codomain f → domain f ∧ f❙¯ ∘⇩c f = id(domain f) ∧ f ∘⇩c f❙¯ = id(codomain f)"
unfolding inverse_def
proof (rule theI', safe)
show "∃g. g : codomain f → domain f ∧ g ∘⇩c f = id⇩c (domain f) ∧ f ∘⇩c g = id⇩c (codomain f)"
using assms unfolding isomorphism_def cfunc_type_def by auto
next
fix g1 g2
assume g1_f: "g1 ∘⇩c f = id⇩c (domain f)" and f_g1: "f ∘⇩c g1 = id⇩c (codomain f)"
assume g2_f: "g2 ∘⇩c f = id⇩c (domain f)" and f_g2: "f ∘⇩c g2 = id⇩c (codomain f)"
assume "g1 : codomain f → domain f" "g2 : codomain f → domain f"
then have "codomain g1 = domain f" "domain g2 = codomain f"
unfolding cfunc_type_def by auto
then show "g1 = g2"
by (metis comp_associative f_g1 g2_f id_left_unit id_right_unit)
qed
lemma inverse_type[type_rule]:
assumes "isomorphism f" "f : X → Y"
shows "f❙¯ : Y → X"
using assms inverse_def2 unfolding cfunc_type_def by auto
lemma inv_left:
assumes "isomorphism f" "f : X → Y"
shows "f❙¯ ∘⇩c f = id X"
using assms inverse_def2 unfolding cfunc_type_def by auto
lemma inv_right:
assumes "isomorphism f" "f : X → Y"
shows "f ∘⇩c f❙¯ = id Y"
using assms inverse_def2 unfolding cfunc_type_def by auto
lemma inv_iso:
assumes "isomorphism f"
shows "isomorphism(f❙¯)"
using assms inverse_def2 unfolding isomorphism_def cfunc_type_def by (intro exI[where x=f], auto)
lemma inv_idempotent:
assumes "isomorphism f"
shows "(f❙¯)❙¯ = f"
by (smt assms cfunc_type_def comp_associative id_left_unit inv_iso inverse_def2)
definition is_isomorphic :: "cset ⇒ cset ⇒ bool" (infix "≅" 50) where
"X ≅ Y ⟷ (∃ f. f : X → Y ∧ isomorphism f)"
lemma id_isomorphism: "isomorphism (id X)"
unfolding isomorphism_def
by (intro exI[where x= "id X"], auto simp add: id_codomain id_domain, metis id_domain id_right_unit)
lemma isomorphic_is_reflexive: "X ≅ X"
unfolding is_isomorphic_def
by (intro exI[where x= "id X"], auto simp add: id_domain id_codomain id_isomorphism id_type)
lemma isomorphic_is_symmetric: "X ≅ Y ⟶ Y ≅ X"
unfolding is_isomorphic_def isomorphism_def
by (auto, metis cfunc_type_def)
lemma isomorphism_comp:
"domain f = codomain g ⟹ isomorphism f ⟹ isomorphism g ⟹ isomorphism (f ∘⇩c g)"
unfolding isomorphism_def by (auto, smt codomain_comp comp_associative domain_comp id_right_unit)
lemma isomorphism_comp':
assumes "f : Y → Z" "g : X → Y"
shows "isomorphism f ⟹ isomorphism g ⟹ isomorphism (f ∘⇩c g)"
using assms cfunc_type_def isomorphism_comp by auto
lemma isomorphic_is_transitive: "(X ≅ Y ∧ Y ≅ Z) ⟶ X ≅ Z"
unfolding is_isomorphic_def by (auto, metis cfunc_type_def comp_type isomorphism_comp)
lemma is_isomorphic_equiv:
"equiv UNIV {(X, Y). X ≅ Y}"
unfolding equiv_def
proof safe
show "refl {(x, y). x ≅ y}"
unfolding refl_on_def using isomorphic_is_reflexive by auto
next
show "sym {(x, y). x ≅ y}"
unfolding sym_def using isomorphic_is_symmetric by blast
next
show "trans {(x, y). x ≅ y}"
unfolding trans_def using isomorphic_is_transitive by blast
qed
text ‹The lemma below corresponds to Exercise 2.1.7e in Halvorson.›
lemma iso_imp_epi_and_monic:
"isomorphism f ⟹ epimorphism f ∧ monomorphism f"
unfolding isomorphism_def epimorphism_def monomorphism_def
proof safe
fix g s t
assume domain_g: "domain g = codomain f"
assume codomain_g: "codomain g = domain f"
assume gf_id: "g ∘⇩c f = id (domain f)"
assume fg_id: "f ∘⇩c g = id (domain g)"
assume domain_s: "domain s = codomain f"
assume domain_t: "domain t = codomain f"
assume sf_eq_tf: "s ∘⇩c f = t ∘⇩c f"
have "s = s ∘⇩c id(codomain(f))"
by (metis domain_s id_right_unit)
also have "... = s ∘⇩c (f ∘⇩c g)"
by (simp add: domain_g fg_id)
also have "... = (s ∘⇩c f) ∘⇩c g"
by (simp add: codomain_g comp_associative domain_s)
also have "... = (t ∘⇩c f) ∘⇩c g"
by (simp add: sf_eq_tf)
also have "... = t ∘⇩c (f ∘⇩c g)"
by (simp add: codomain_g comp_associative domain_t)
also have "... = t ∘⇩c id(codomain f)"
by (simp add: domain_g fg_id)
also have "... = t"
by (metis domain_t id_right_unit)
finally show "s = t".
next
fix g h k
assume domain_g: "domain g = codomain f"
assume codomain_g: "codomain g = domain f"
assume gf_id: "g ∘⇩c f = id (domain f)"
assume fg_id: "f ∘⇩c g = id (domain g)"
assume codomain_h: "codomain h = domain f"
assume codomain_k: "codomain k = domain f"
assume fk_eq_fh: "f ∘⇩c k = f ∘⇩c h"
have "h = id(domain f) ∘⇩c h"
by (metis codomain_h id_left_unit)
also have "... = (g ∘⇩c f) ∘⇩c h"
using gf_id by auto
also have "... = g ∘⇩c (f ∘⇩c h)"
by (simp add: codomain_h comp_associative domain_g)
also have "... = g ∘⇩c (f ∘⇩c k)"
by (simp add: fk_eq_fh)
also have "... = (g ∘⇩c f) ∘⇩c k"
by (simp add: codomain_k comp_associative domain_g)
also have "... = id(domain f) ∘⇩c k"
by (simp add: gf_id)
also have "... = k"
by (metis codomain_k id_left_unit)
ultimately show "k = h"
by simp
qed
lemma isomorphism_sandwich:
assumes f_type: "f : A → B" and g_type: "g : B → C" and h_type: "h: C → D"
assumes f_iso: "isomorphism f"
assumes h_iso: "isomorphism h"
assumes hgf_iso: "isomorphism(h ∘⇩c g ∘⇩c f)"
shows "isomorphism g"
proof -
have "isomorphism(h❙¯ ∘⇩c (h ∘⇩c g ∘⇩c f) ∘⇩c f❙¯)"
using assms by (typecheck_cfuncs, simp add: f_iso h_iso hgf_iso inv_iso isomorphism_comp')
then show "isomorphism g"
using assms by (typecheck_cfuncs_prems, smt comp_associative2 id_left_unit2 id_right_unit2 inv_left inv_right)
qed
end