Theory Multimonoid

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

section ‹Multimonoids›

theory Multimonoid
  imports Catoid

begin

context multimagma
begin

subsection ‹Unital multimagmas›

text ‹This component presents an alternative approach to catoids, as multisemigroups with many units.
This is more akin to the formalisation of single-set categories in Chapter I of Mac Lane's book, but
in fact this approach to axiomatising categories goes back to the middle of the twentieth century.›

text ‹Units can already be defined in multimagmas.›

definition "munitl e = ((∃x. x ∈ e ⊙ x) ∧ (∀x y. y ∈ e ⊙ x ⟶ y = x))"

definition "munitr e = ((∃x. x ∈ x ⊙ e) ∧ (∀x y. y ∈ x ⊙ e ⟶ y = x))"

abbreviation "munit e ≡ (munitl e ∨ munitr e)"

end

text ‹A multimagma is unital if every element has a left and a right unit.›

class unital_multimagma_var = multimagma +
  assumes munitl_ex: "∀x.∃e. munitl e ∧ Δ e x"
  assumes munitr_ex: "∀x.∃e. munitr e ∧ Δ x e"

begin

lemma munitl_ex_var: "∀x.∃e. munitl e ∧ x ∈ e ⊙ x"
  by (metis equals0I local.munitl_def local.munitl_ex)

lemma unitl: "⋃{e ⊙ x |e. munitl e} = {x}"
  apply safe
  apply (simp add: multimagma.munitl_def)
  by (simp, metis munitl_ex_var)

lemma munitr_ex_var: "∀x.∃e. munitr e ∧ x ∈ x ⊙ e"
  by (metis equals0I local.munitr_def local.munitr_ex)

lemma unitr: "⋃{x ⊙ e |e. munitr e} = {x}"
  apply safe
   apply (simp add: multimagma.munitr_def)
  by (simp, metis munitr_ex_var)

end

text ‹Here is an alternative definition.›

class unital_multimagma = multimagma +
  fixes E :: "'a set"
  assumes El: "⋃{e ⊙ x |e. e ∈ E} = {x}"
  and Er: "⋃{x ⊙ e |e. e ∈ E} = {x}"

begin

lemma E1: "∀e ∈ E. (∀x y. y ∈ e ⊙ x ⟶ y = x)"
  using local.El by fastforce

lemma E2: "∀e ∈ E. (∀x y. y ∈ x ⊙ e ⟶ y = x)"
  using local.Er by fastforce

lemma El11: "∀x.∃e ∈ E. x ∈ e ⊙ x"
  using local.El by fastforce

lemma El12: "∀x.∃e ∈ E. e ⊙ x = {x}"
  using E1 El11 by fastforce

lemma Er11: "∀x.∃e ∈ E. x ∈ x ⊙ e"
  using local.Er by fastforce

lemma Er12: "∀x.∃e ∈ E. x ⊙ e = {x}"
  using Er Er11 by fastforce

text ‹Units are "orthogonal" idempotents.›

lemma unit_id: "∀e ∈ E. e ∈ e ⊙ e"
  using E1 local.Er by fastforce

lemma unit_id_eq: "∀e ∈ E. e ⊙ e = {e}"
  by (simp add: E1 equalityI subsetI unit_id)

lemma unit_comp:
  assumes "e⇩1 ∈ E"
and "e⇩2 ∈ E"
and "Δ e⇩1 e⇩2"
shows "e⇩1 = e⇩2"
proof-
  obtain x where a: "x ∈ e⇩1 ⊙ e⇩2"
    using assms(3) by auto
  hence b: "x = e⇩1"
    using E2 assms(2) by blast
  hence "x = e⇩2"
    using E1 a assms(1) by blast
  thus "e⇩1 = e⇩2"
    by (simp add: b)
qed

lemma unit_comp_iff: "e⇩1 ∈ E ⟹ e⇩2 ∈ E ⟹ (Δ e⇩1 e⇩2 = (e⇩1 = e⇩2))"
  using unit_comp unit_id by fastforce

lemma "∀e ∈ E.∃x. x ∈ e ⊙ x"
  using unit_id by force

lemma "∀e ∈ E.∃x. x ∈ x ⊙ e"
  using unit_id by force

sublocale unital_multimagma_var
  apply unfold_locales
  apply (metis E1 El12 empty_not_insert insertI1 local.munitl_def)
  by (metis E2 Er12 empty_not_insert insertI1 local.munitr_def)

text ‹Now it is clear that the two definitions are equivalent.›

text ‹The next two lemmas show that the set of units is a left and right unit of composition at powerset level.›

lemma conv_unl: "E ⋆ X = X"
  unfolding conv_def
  apply safe
  using E1 apply blast
  using El12 by fastforce

lemma conv_unr: "X ⋆ E = X"
  unfolding conv_def
  apply safe
  using E2 apply blast
  using Er12 by fastforce

end


subsection ‹Multimonoids›

text ‹A multimonoid is a unital multisemigroup.›

class multimonoid = multisemigroup + unital_multimagma

begin

text ‹In a multimonoid, left and right units are unique for each element.›

lemma munits_uniquel: "∀x.∃!e. e ∈ E ∧ e ⊙ x = {x}"
proof-
  {fix x
  obtain e where a: "e ∈ E ∧ e ⊙ x = {x}"
    using local.El12 by blast
  {fix e'
  assume b: "e' ∈ E ∧ e' ⊙ x = {x}"
  hence "{e} ⋆ (e' ⊙ x) = {x}"
    by (simp add: a multimagma.conv_atom)
  hence "(e ⊙ e') ⋆ {x}  = {x}"
    by (simp add: local.assoc_var)
  hence "Δ e e'"
    using local.conv_exp2 by auto
  hence "e = e'"
    by (simp add: a b local.unit_comp_iff)}
  hence "∃e ∈ E. e ⊙ x = {x} ∧ (∀e' ∈ E. e' ⊙ x = {x} ⟶ e = e)"
    using a by blast}
  thus ?thesis
    by (metis emptyE local.assoc_exp local.unit_comp singletonI)
qed

lemma munits_uniquer: "∀x.∃!e. e ∈ E ∧ x ⊙ e = {x}"
  apply safe
   apply (meson local.Er12)
  by (metis insertI1 local.E1 local.E2 local.assoc_var local.conv_exp2)

text ‹In a monoid, there is of course one single unit, and my definition of many units reduces to this one.›

lemma units_unique: "(∀x y. Δ x y) ⟹ ∃!e. e ∈ E"
  apply safe
  using local.El11 apply blast
  using local.unit_comp_iff by presburger

lemma units_rm2l: "e⇩1 ∈ E ⟹ e⇩2 ∈ E ⟹ Δ e⇩1 x ⟹ Δ e⇩2 x ⟹ e⇩1 = e⇩2"
  by (smt (verit, del_insts) ex_in_conv local.E1 local.assoc_exp local.unit_comp)

lemma units_rm2r: "e⇩1 ∈ E ⟹ e⇩2 ∈ E ⟹ Δ x e⇩1 ⟹ Δ x e⇩2 ⟹ e⇩1 = e⇩2"
  by (metis (full_types) ex_in_conv local.E2 local.assoc_exp local.unit_comp)

text ‹One can therefore express the functional relationship between elements and their units in terms of
explict (source and target) maps -- as in catoids.›

definition so :: "'a ⇒ 'a" where
  "so x = (THE e. e ∈ E ∧ e ⊙ x = {x})"

definition ta :: "'a ⇒ 'a"  where
  "ta x = (THE e. e ∈ E ∧ x ⊙ e = {x})"

abbreviation So :: "'a set ⇒ 'a set" where
 "So X ≡ image so X"

abbreviation Ta :: "'a set ⇒ 'a set" where
 "Ta X ≡ image ta X"

end

subsection ‹Multimonoids and catoids›

text ‹It is now easy to show that every catoid is a multimonoid and vice versa.›

(*sublocale catoid ⊆ lrmon: multimonoid "(⊙)" sfix
  apply unfold_locales
  using local.sfix_absorb_var apply presburger
  using local.stfix_set local.tfix_absorb_var by presburger*)

text ‹One cannot have both sublocale statements at the same time.›

text ‹The converse direction requires some preparation.›

lemma (in multimonoid) so_unit: "so x ∈ E"
  unfolding so_def by (metis (mono_tags, lifting) local.munits_uniquel theI')

lemma (in multimonoid) ta_unit: "ta x ∈ E"
  unfolding ta_def by (metis (mono_tags, lifting) local.munits_uniquer theI')

lemma (in multimonoid) so_absorbl: "so x ⊙ x = {x}"
  unfolding so_def by (metis (mono_tags, lifting) local.munits_uniquel the_equality)

lemma (in multimonoid) ta_absorbr: "x ⊙ ta x = {x}"
  unfolding ta_def by (metis (mono_tags, lifting) local.munits_uniquer the_equality)

lemma (in multimonoid) semi_locality: "Δ x y ⟹ ta x = so y"
  by (smt (verit, best) local.assoc_var local.conv_atom local.so_absorbl local.so_unit local.ta_absorbr local.ta_unit local.units_rm2l local.units_rm2r)

sublocale multimonoid ⊆ monlr: catoid "(⊙)" "so" "ta"
  by (unfold_locales, simp_all add: local.semi_locality local.so_absorbl local.ta_absorbr)


subsection‹From multimonoids to categories›

text‹Single-set categories are precisely local partial monoids, that is, object-free categories
as in Chapter I of Mac Lane's book.›

class local_multimagma = multimagma +
  assumes locality: "v ∈ x ⊙ y ⟹ Δ y z  ⟹ Δ v z"

class local_multisemigroup = multisemigroup + local_multimagma

text ‹In this context, a semicategory is an object-free category without identity arrows›

class of_semicategory = local_multisemigroup + functional_semigroup

begin

lemma part_locality: "Δ x y  ⟹ Δ y z  ⟹ Δ (x ⊗ y) z"
  by (meson local.locality local.pcomp_def_var2)

lemma part_locality_var: "Δ x y  ⟹ Δ y z  ⟹ (x ⊙ y) ⋆ {z} ≠ {}"
  by (smt (z3) ex_in_conv local.locality multimagma.conv_exp2 singleton_iff)

lemma locality_iff: "(Δ x y ∧ Δ y z) = (Δ x y ∧ Δ (x ⊗ y) z)"
  by (meson local.pcomp_assoc_defined part_locality)

lemma locality_iff_var: "(Δ x y ∧ Δ y z) = (Δ x y ∧ (x ⊙ y) ⋆ {z} ≠ {})"
  by (metis ex_in_conv local.assoc_var local.conv_exp2 part_locality_var)

end

class partial_monoid = multimonoid + functional_magma

class local_multimonoid = multimonoid + local_multimagma

begin

lemma sota_locality: "ta x = so y ⟹ Δ x y"
  using local.locality monlr.st_local_iff by blast

lemma So_local: "So (x ⊙ so y) = So (x ⊙ y)"
  using local.locality monlr.st_local_iff monlr.st_locality_locality by presburger

lemma Ta_local: "Ta (ta x ⊙ y) = Ta (x ⊙ y)"
  using local.locality monlr.st_local_iff monlr.st_locality_locality by presburger

sublocale locmm: local_catoid "(⊙)" so ta
  by (unfold_locales, simp_all add: So_local Ta_local)

text ‹The following statements formalise compatibility properties.›

lemma local_conv: "v ∈ x ⊙ y ⟹ (Δ v z = Δ y z)"
  by (metis ex_in_conv local.assoc_exp local.locality)

lemma local_alt: "e ∈ E ⟹ x ∈ x ⊙ e ⟹ y ∈ e ⊙ y ⟹ Δ x y"
  using local_conv by blast

lemma local_iff: "Δ x y = (∃e ∈ E. Δ x e ∧ Δ e y)"
  by (smt (verit, best) local.Er11 local.units_rm2l local_alt local_conv)

lemma local_iff2: "(ta x = so y) = Δ x y"
  by (simp add: locmm.st_local)

end

text ‹Finally I formalise object-free categories. The axioms are essentially Mac Lane's,
but a multioperation is used for arrow composition, to capture partiality.›

class of_category = of_semicategory + partial_monoid

text ‹The next statements show that single-set categories based on catoids and object-free categories
based on multimonoids are the same (we can only have one direction as a sublocale statement). It then
follows from results about catoids and single-set categories that object-free categories are indeed categories.
These results can be found in the catoid component. I do not present explicit proofs for object-free categories
here.›

sublocale of_category ⊆ ofss_cat: single_set_category _ so ta
  apply unfold_locales
  using local.locality monlr.st_local_iff monlr.st_locality_locality apply auto[1]
  using local.locality monlr.st_local_iff monlr.st_locality_locality monlr.tgt_weak_local by presburger

(*
sublocale single_set_category ⊆ of_category _ sfix
  apply unfold_locales
  using local.st_local local.st_local_iff apply auto[1]
  using local.sfix_absorb_var apply presburger
  using local.stfix_set local.tfix_absorb_var by presburger
*)

subsection ‹Multimonoids and relational monoids›

text ‹Relational monoids are monoids in the category Rel. They have been used previously to construct
convolution algebras in another AFP entry. Here I show that relational monoids are isomorphic to multimonoids,
but I do not integrate the AFP entry with relational monoids because it uses a historic quantale component,
which is different from the quantale component in the AFP. Instead, I simply copy in the definitions
leading to relational monoids and leave the consolidation of Isabelle theories to the future.›

class rel_magma =
  fixes ρ :: "'a ⇒ 'a ⇒ 'a ⇒ bool"

class rel_semigroup = rel_magma +
  assumes rel_assoc: "(∃y. ρ y u v ∧ ρ x y w) = (∃z. ρ z v w ∧ ρ x u z)"

class rel_monoid = rel_semigroup +
  fixes ξ :: "'a set"
  assumes unitl_ex: "∃e ∈ ξ. ρ x e x"
  and unitr_ex: "∃e ∈ ξ. ρ x x e"
  and unitl_eq: "e ∈ ξ ⟹ ρ x e y ⟹ x = y"
  and unitr_eq: "e ∈ ξ ⟹ ρ x y e ⟹ x = y"

text ‹Once again, only one of the two sublocale statements compiles.›

(*sublocale rel_monoid ⊆ multimonoid "λx y. {z. ρ z x y}" ξ
  apply unfold_locales
    apply safe
       apply simp_all
       apply (metis CollectI local.rel_assoc)
      apply (metis CollectI local.rel_assoc)
     apply (simp add: local.unitl_eq)
    apply (metis CollectI local.unitl_ex)
  apply (simp add: local.unitr_eq)
  by (metis local.unitr_ex mem_Collect_eq)*)

sublocale multimonoid ⊆ rel_monoid "λx y z. x ∈ y ⊙ z" E
  apply unfold_locales
  using local.assoc_exp apply blast
  using local.El11 apply blast
    apply (simp add: local.Er11)
  using local.E1 apply blast
  by (simp add: local.E2)

end