Theory IsomorphismClass
section "Isomorphism Classes"
text ‹
The following is a small theory that facilitates working with isomorphism classes of objects
in a category.
›
theory IsomorphismClass
imports Category3.EpiMonoIso Category3.NaturalTransformation
begin
context category
begin
notation isomorphic (infix ‹≅› 50)
definition iso_class (‹⟦_⟧›)
where "iso_class f ≡ {f'. f ≅ f'}"
definition is_iso_class
where "is_iso_class F ≡ ∃f. f ∈ F ∧ F = iso_class f"
definition iso_class_rep
where "iso_class_rep F ≡ SOME f. f ∈ F"
lemmas isomorphic_transitive [trans]
lemmas naturally_isomorphic_transitive [trans]
lemma inv_in_homI [intro]:
assumes "iso f" and "«f : a → b»"
shows "«inv f : b → a»"
using assms inv_is_inverse seqE inverse_arrowsE
by (metis ide_compE in_homE in_homI)
lemma iso_class_is_nonempty:
assumes "is_iso_class F"
shows "F ≠ {}"
using assms is_iso_class_def iso_class_def by auto
lemma iso_class_memb_is_ide:
assumes "is_iso_class F" and "f ∈ F"
shows "ide f"
using assms is_iso_class_def iso_class_def isomorphic_def by auto
lemma ide_in_iso_class:
assumes "ide f"
shows "f ∈ ⟦f⟧"
using assms iso_class_def is_iso_class_def isomorphic_reflexive by simp
lemma rep_in_iso_class:
assumes "is_iso_class F"
shows "iso_class_rep F ∈ F"
using assms is_iso_class_def iso_class_rep_def someI_ex [of "λf. f ∈ F"]
ide_in_iso_class
by metis
lemma is_iso_classI:
assumes "ide f"
shows "is_iso_class ⟦f⟧"
using assms iso_class_def is_iso_class_def isomorphic_reflexive by blast
lemma rep_iso_class:
assumes "ide f"
shows "iso_class_rep ⟦f⟧ ≅ f"
using assms is_iso_classI rep_in_iso_class iso_class_def isomorphic_symmetric
by blast
lemma iso_class_elems_isomorphic:
assumes "is_iso_class F" and "f ∈ F" and "f' ∈ F"
shows "f ≅ f'"
using assms iso_class_def
by (metis is_iso_class_def isomorphic_symmetric isomorphic_transitive mem_Collect_eq)
lemma iso_class_eqI [intro]:
assumes "f ≅ g"
shows "⟦f⟧ = ⟦g⟧"
proof -
have f: "ide f"
using assms isomorphic_def by auto
have g: "ide g"
using assms isomorphic_def by auto
have "f ∈ ⟦g⟧"
using assms iso_class_def isomorphic_symmetric by simp
moreover have "g ∈ ⟦g⟧"
using assms g iso_class_def isomorphic_reflexive isomorphic_def by simp
ultimately have "⋀h. (h ∈ ⟦f⟧) = (h ∈ ⟦g⟧)"
using assms g iso_class_def [of f] iso_class_def [of g]
isomorphic_reflexive isomorphic_symmetric isomorphic_transitive
by blast
thus ?thesis by auto
qed
lemma iso_class_eq:
assumes "is_iso_class F" and "is_iso_class G" and "F ∩ G ≠ {}"
shows "F = G"
proof -
obtain h where h: "h ∈ F ∧ h ∈ G"
using assms by auto
show ?thesis
using assms h
by (metis is_iso_class_def iso_class_elems_isomorphic iso_class_eqI)
qed
lemma iso_class_rep [simp]:
assumes "is_iso_class F"
shows "⟦iso_class_rep F⟧ = F"
proof (intro iso_class_eq)
show "is_iso_class ⟦iso_class_rep F⟧"
using assms is_iso_classI iso_class_memb_is_ide rep_in_iso_class by blast
show "is_iso_class F"
using assms by simp
show "⟦iso_class_rep F⟧ ∩ F ≠ {}"
using assms rep_in_iso_class
by (meson disjoint_iff_not_equal ide_in_iso_class iso_class_memb_is_ide)
qed
end
end