(*
Title: Groupoids
Author: Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Groupoids›

theory Groupoid
  imports Catoid

begin

subsection ‹st-Multigroupoids›

text ‹I define multigroupoids, extending the standard definition. I equip catoids with an operation
  inversion.›

class inv_op = fixes inv :: "'a → 'a"

class st_multigroupoid = catoid + inv_op +
  assumes invl: "σ x ∈ x ⊙ inv x"
  and invr: "τ x ∈ inv x ⊙ x"

sublocale st_multigroupoid ⊆ st_mgpd: st_multigroupoid  "λx y. y ⊙ x" tgt src inv
  by unfold_locales (simp_all add: local.invr local.invl)

text ‹Every multigroupoid is local.›

lemma (in st_multigroupoid) st_mgpd_local:
  assumes "τ x = σ y"
  shows "Δ x y"
proof-
  have "x ∈ x ⊙ σ y"
    by (metis assms local.t_absorb singletonI)
  hence "x ∈ {x} ⋆ (y ⊙ inv y)"
    using local.conv_exp2 local.invl by auto
  hence "x ∈ (x ⊙ y) ⋆ {inv y}"
    using local.assoc_var by force
  hence "∃u v. x ∈ u ⊙ v ∧ u ∈ x ⊙ y ∧ v = inv y"
    by (metis multimagma.conv_exp2 singletonD)
  hence "∃u. x ∈ u ⊙ inv y ∧ u ∈ x ⊙ y"
    by presburger
  hence "∃u. u ∈ x ⊙ y"
    by fastforce
  thus ?thesis
    by force
qed

sublocale st_multigroupoid ⊆ stmgpd: local_catoid "(⊙)" src tgt
  apply unfold_locales
   apply (metis local.Dst local.st_locality_locality local.st_mgpd_local set_eq_subset)
  by (metis local.Dst local.st_locality_locality local.st_mgpd_local subset_refl)

lemma (in st_multigroupoid) tgt_inv [simp]: "τ (inv x) = σ x"
  using local.Dst local.invr by fastforce

lemma (in st_multigroupoid) src_inv: "σ (inv x) = τ x"
  by simp

text ‹The following lemma is from Theorem 5.2 of Jónsson and Tarski's Boolean Algebras with Operators II article.›

lemma (in st_multigroupoid) bao3:
  assumes "x ⊙ y = {σ x}"
  shows "inv x = y"
proof -
  have "τ x = σ y"
    using assms local.Dst by force
  hence "{y} = τ x ⊙ y"
    by simp
  hence "y ∈ {inv x} ⋆ {x} ⋆ {y}"
    using local.conv_exp2 local.invr by fastforce
  hence "y ∈ inv x ⊙ σ x"
    by (metis assms local.assoc_var local.conv_atom)
  hence "y ∈ inv x ⊙ τ (inv x)"
    by simp
  thus ?thesis
    by (metis local.t_absorb singletonD)
qed

lemma (in st_multigroupoid) inv_s [simp]: "inv (σ x) = σ x"
proof-
  have "σ x ⊙ σ x = {σ x}"
    by simp
  thus "inv (σ x) = σ x"
    by (simp add: local.st_mgpd.bao3)
qed

lemma (in st_multigroupoid) srcfunct_inv:
   "σ x ∈ x ⊙ inv x ==> σ y ∈ x ⊙ inv x ==> σ x = σ y"
  using local.ts_msg.src_funct by fastforce

lemma (in st_multigroupoid) tgtfunct_inv:
   "τ x ∈ inv x ⊙ x ==> τ y ∈ inv x ⊙ x ==> τ x = τ y"
  by (metis local.ts_msg.src_comp_aux local.tt_idem)

text ‹As for catoids, I prove quantalic properties, lifting to powersets.›

abbreviation (in st_multigroupoid) Inv :: "'a set → 'a set" where
  "Inv ≡ image inv"

lemma (in st_multigroupoid) Inv_exp: "Inv X = {inv x |x. x ∈ X}"
  by blast

lemma (in st_multigroupoid) Inv_un: "Inv (X ∪ Y) = Inv X ∪ Inv Y"
  by (simp add: image_Un)

lemma (in st_multigroupoid) Inv_Un: "Inv (∪X) = (∪X ∈ X. Inv X)"
  unfolding Inv_exp by auto

lemma (in st_multigroupoid) Invl: "Src X ⊆ X ⋆ Inv X"
  unfolding Inv_exp conv_exp using local.invl by fastforce

lemma (in st_multigroupoid) Invr: "Tgt X ⊆ Inv X ⋆ X"
  by (meson imageI image_subsetI local.invr local.stopp.conv_exp2)

lemma (in st_multigroupoid) Inv_strong_gelfand: "X ⊆ X ⋆ Inv X ⋆ X"
proof-
  have "X = Src X ⋆ X"
    by simp
  also have "… ⊆ X ⋆ Inv X ⋆ X"
    using local.Invl local.conv_isor by presburger
  finally show ?thesis.
qed

text ‹At powerset level, one can define domain and codomain operations explicitly as in
  algebras.›

lemma (in st_multigroupoid) dom_def: "Src X = sfix ∩ (X ⋆ Inv X)"
proof-
  {fix a
  have "(a ∈ sfix ∩ (X ⋆ Inv X)) = (σ a = a ∧ σ a ∈ X ⋆ Inv X)"
    by fastforce
  also have "… = (σ a = a ∧ (∃b ∈ X.∃c ∈ Inv X. σ a ∈ b ⊙ c))"
    using local.conv_exp2 by auto
  also have "… = (σ a = a ∧ (∃b ∈ X. σ a = σ b))"
    by (metis imageI local.invl local.ts_msg.tgt_comp_aux)
  also have "… = (a ∈ Src X)"
    by auto
  finally have "(a ∈ sfix ∩ (X ⋆ Inv X)) = (a ∈ Src X)".}
  thus ?thesis
    by blast
qed

lemma (in st_multigroupoid) cod_def: "Tgt X = sfix ∩ (Inv X ⋆ X)"
  by (metis local.st_mgpd.dom_def local.stfix_set local.stopp.conv_def multimagma.conv_def)

lemma (in st_multigroupoid) dom_def_var: "Src X = sfix ∩ (X ⋆ UNIV)"
proof-
  {fix a
  have "(a ∈ sfix ∩ (X ⋆ UNIV)) = (σ a = a ∧ σ a ∈ X ⋆ UNIV)"
    by fastforce
  also have "… = (σ a = a ∧ (∃b ∈ X.∃c. σ a ∈ b ⊙ c))"
    using local.conv_exp2 by auto
  also have "… = (σ a = a ∧ (∃b ∈ X. σ a = σ b))"
    by (metis local.invl local.ts_msg.tgt_comp_aux)
  also have "… = (a ∈ Src X)"
    by auto
  finally have "(a ∈ sfix ∩ (X ⋆ UNIV)) = (a ∈ Src X)".}
  thus ?thesis
    by blast
qed

lemma (in st_multigroupoid) cod_def_var: "Tgt X = sfix ∩ (UNIV ⋆ X)"
  by (metis local.ST_im local.sfix_im local.st_mgpd.dom_def_var local.stopp.conv_def local.tfix_im multimagma.conv_def)

lemma (in st_multigroupoid) dom_univ: "X ⋆ UNIV = Src X ⋆ UNIV"
proof-
  have "X ⋆ UNIV = Src X ⋆ X ⋆ UNIV"
    using local.Src_absorp by presburger
  also have "… ⊆ Src X ⋆ UNIV ⋆ UNIV"
    by (meson local.conv_isol local.conv_isor subset_UNIV)
  finally have a: "X ⋆ UNIV ⊆ Src X ⋆ UNIV"
    using local.conv_assoc local.conv_isol subset_UNIV by blast
  have "Src X ⋆ UNIV ⊆ X ⋆ Inv X ⋆ UNIV"
    using local.Invl local.conv_isor by presburger
  also have "… ⊆ X ⋆ UNIV ⋆ UNIV"
    by (simp add: local.conv_isol local.conv_isor)
  finally have "Src X ⋆ UNIV ⊆ X ⋆ UNIV"
    by (metis dual_order.trans local.conv_assoc local.conv_isol subset_UNIV)
  thus ?thesis
    using a by force
qed

lemma (in st_multigroupoid) cod_univ: "UNIV ⋆ X = UNIV ⋆ Tgt X"
  by (metis local.st_mgpd.dom_univ local.stopp.conv_def multimagma.conv_def)


subsection ‹Groupoids›

text ‹Groupoids are simply functional multigroupoids. I start with a somewhat indirect axiomatisaion.›

class groupoid_var = st_multigroupoid + functional_catoid

begin

lemma invl [simp]: "x ⊙ inv x = {σ x}"
  using local.fun_in_sgl local.invl by force

lemma invr [simp]: "inv x ⊙ x = {τ x}"
  using local.fun_in_sgl local.invr by force

end

text ‹Next, I provide a more direct axiomatisation.›

class groupoid = catoid + inv_op +
  assumes invs [simp]: "x ⊙ inv x = {σ x}"
  and invt [simp]: "inv x ⊙ x = {τ x}"

subclass (in groupoid) st_multigroupoid
  by unfold_locales simp_all

sublocale groupoid ⊆ lrgpd: groupoid "λx y. y ⊙ x"  tgt src inv
  by unfold_locales simp_all

lemma (in groupoid) bao4 [simp]: "inv (inv x) = x"
proof-
  have "inv x ⊙ x = {σ (inv x)}"
    by simp
  thus ?thesis
    using local.bao3 by blast
qed

lemma (in groupoid) rev1:
  "x ∈ y ⊙ z ==> y ∈ x ⊙ inv z"
proof-
  assume h: "x ∈ y ⊙ z"
  hence "x ⊙ inv z ⊆ y ⊙ z ⋆ {inv z}"
    using multimagma.conv_exp2 by fastforce
  hence "x ⊙ inv z ⊆ {y} ⋆ (z ⊙ inv z)"
    using local.assoc_var by presburger
  hence "x ⊙ inv z ⊆ y ⊙ σ z"
    by simp
  hence "x ⊙ inv z ⊆ y ⊙ τ y"
    using h local.src_comp_aux local.src_twisted_aux by auto
  hence a: "x ⊙ inv z ⊆ {y}"
    by simp
  have "τ x = τ z"
    using h local.tgt_comp_aux by auto
  hence  "x ⊙ inv z ≠ {}"
    by (simp add: local.st_mgpd_local)
  hence "x ⊙ inv z = {y}"
    using a by auto
  thus ?thesis
    by force
qed

lemma (in groupoid) rev2:
  "x ∈ y ⊙ z ==> z ∈ inv y ⊙ x"
  by (simp add: local.lrgpd.rev1)

lemma (in groupoid) rev1_eq: "(y ∈ x ⊙ (inv z)) = (x ∈ y ⊙ z)"
  using local.lrgpd.rev2 by force

lemma (in groupoid) rev2_eq: "(z ∈ (inv y) ⊙ x) = (x ∈ y ⊙ z)"
  by (simp add: local.lrgpd.rev1_eq)

text ‹The following fact show that the axiomatisation above captures indeed groupoids.›

lemma (in groupoid) lr_mgpd_partial:
  assumes "x ∈ y ⊙ z"
  and "x' ∈ y ⊙ z"
  shows "x = x'"
proof-
  have "z ∈ inv y ⊙ x"
    by (simp add: assms(1) rev2)
  hence "x' ∈ {y} ⋆ (inv y ⊙ x)"
    using assms(2) local.conv_exp2 by auto
  hence "x'∈ (y ⊙ inv y) ⋆ {x}"
    by (simp add: local.assoc_var)
  hence "x' ∈ σ y ⊙ x"
    by (simp add: multimagma.conv_atom)
  hence "x' ∈ σ x ⊙ x"
    using assms(1) local.ts_msg.tgt_comp_aux by auto
  thus ?thesis
    by simp
qed

subclass (in groupoid) single_set_category
  by unfold_locales (simp add: local.lr_mgpd_partial)

text ‹Hence st-groupoids are indeed single-set categories in which all arrows
  isomorphisms.›

lemma (in groupoid) src_canc1:
  assumes "τ z = σ x"
  and "τ z = σ y"
  and "z ⊗ x = z ⊗ y"
shows "x = y"
proof-
  have "inv z ⊗ (z ⊗ x) = inv z ⊗ (z ⊗ y)"
    by (simp add: assms(3))
  hence "(inv z ⊗ z) ⊗ x = (inv z ⊗ z) ⊗ y"
    using assms(1) assms(2) local.sscatml.comp0_assoc by auto
  hence "τ z ⊗ x = τ z ⊗ y"
    by (simp add: local.pcomp_def)
  thus ?thesis
    by (metis assms(1) assms(2) local.sscatml.l0_absorb)
qed

lemma (in groupoid) tgt_canc1:
  assumes "τ x = σ z"
  and "τ y = σ z"
  and "x ⊗ z = y ⊗ z"
  shows "x = y"
  by (metis assms local.lrgpd.pcomp_def_var local.lrgpd.src_canc1 local.pcomp_def_var local.st_mgpd.st_mgpd_local)

text ‹The following lemmas are from Theorem 5.2 of Jónsson and Tarski's BAO II article.›

lemma (in groupoid) bao1 [simp]: "x ⊗ (inv x ⊗ x) = x"
  by (simp add: local.pcomp_def)

lemma (in groupoid) bao2 [simp]: "(x ⊗ inv x) ⊗ x = x"
  by (simp add: local.st_assoc)

lemma (in groupoid) bao5:
  "τ x = σ y ==> inv x ⊗ x = y ⊗ inv y"
  using local.invs local.invt local.pcomp_def by auto

lemma (in groupoid) bao6: "Inv (x ⊙ y) = inv y ⊙ inv x"
  apply (rule antisym)
  using rev1_eq rev2_eq apply force
  by (clarsimp, metis imageI local.bao4 local.rev1_eq local.rev2_eq)


subsection ‹Axioms of relation algebra›

text ‹I formalise a special case of a famous theorem of Jónsson and Tarski, showing that groupoids lift
  relation algebras at powerset level. All axioms not related to converse have already been considered
 .›

lemma (in groupoid) Inv_invol [simp]: "Inv (Inv X) = X"
proof-
  have "Inv (Inv X) = {inv (inv x) |x. x ∈ X}"
    by (simp add: image_image)
  also have "… = X"
    by simp
  finally show ?thesis.
qed

lemma (in groupoid) Inv_contrav: "Inv (X ⋆ Y) = Inv Y ⋆ Inv X"
proof-
  have "Inv (X ⋆ Y) = (∪x ∈ X. ∪y ∈ Y. Inv (x ⊙ y))"
    unfolding conv_def image_def by blast
  also have "… = (∪x ∈ X. ∪y ∈ Y. inv y ⊙ inv x)"
    by (simp add: local.bao6)
  also have "… = Inv Y ⋆ Inv X"
    unfolding conv_def image_def by blast
  finally show ?thesis.
qed

lemma (in groupoid) residuation: "Inv X ⋆ -(X ⋆ Y) ⊆ -Y"
  using local.lrgpd.rev1 local.stopp.conv_exp2 by fastforce

lemma (in groupoid) modular_law: "(X ⋆ Y) ∩ Z ⊆ (X ∩ (Z ⋆ Inv Y)) ⋆ Y"
  using local.lrgpd.rev2 local.stopp.conv_exp2 by fastforce

lemma (in groupoid) dedekind: "(X ⋆ Y) ∩ Z ⊆ (X ∩ (Z ⋆ Inv Y)) ⋆ (Y ∩ (Inv X ⋆ Z))"
  unfolding Inv_exp conv_exp
  apply clarsimp
  using local.rev1 local.rev2 by blast

text ‹In sum, this shows that the powerset lifting of a groupoid is a relation algebra. I link this formally with relations
  an interpretation statement in another component.›

text ‹Jónsson and Tarski's axioms of relation algebra are slightly different. It is routine to related them formally with those used here.
  might also be interested to use their partiality-by-closure approach to defining groupoids in a setting with explicit carrier sets
  another Isabelle formalisation.›

lemma (in groupoid) Inv_compl: "Inv (-X) = -(Inv X)"
  by (metis UNIV_I bij_def bij_image_Compl_eq equalityI image_eqI inj_def local.bao4 subsetI)

lemma (in groupoid) Inv_inter: "Inv (X ∩ Y) = Inv X ∩ Inv Y"
  using local.Inv_compl by auto

lemma (in groupoid) Inv_Un: "Inv (∩X) = (∩X ∈ X. Inv X)"
proof-
  have "Inv (∩X) = Inv (-(∪X ∈ X. -X))"
    by (simp add: Setcompr_eq_image)
  also have "… = - (Inv (∪X ∈ X. -X))"
    using local.Inv_compl by presburger
  also have "… = -(∪ X ∈ X. Inv (-X))"
    by blast
  also have "… = -(∪X ∈ X. -(Inv X))"
    using local.Inv_compl by presburger
  also have "… = (∩X ∈ X. Inv X)"
    by blast
  finally show "Inv (∩X) = (∩X ∈ X. Inv X)".
qed

end