Theory Two_Catoid_Collapse

(* 
Title: Eckmann-Hilton Collapse for 2-Catoids
Author: Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹2-Catoids with (too) strong homomorphisms›

theory Two_Catoid_Collapse
  imports Two_Catoid

begin

text ‹Here we present  variants of 2-categories where the axioms are too strong. There is an Eckmann-Hilton
style collapse of the two structures.›


subsection ‹2-st-Multimagmas with strong homomorphism laws›

class two_st_multimagma_collapse = st_multimagma0 + st_multimagma1 +
  assumes comm_s0s1: "σ⇩0 (σ⇩1 x) = σ⇩1 (σ⇩0 x)"
  and comm_t0t1: "τ⇩0 (τ⇩1 x) = τ⇩1 (τ⇩0 x)"
  and comm_s0t1: "σ⇩0 (τ⇩1 x) = τ⇩1 (σ⇩0 x)"
  and commtr0s1: "τ⇩0 (σ⇩1 x) = σ⇩1 (τ⇩0 x)"
  assumes interchange: "(w ⊙⇩1 x) *⇩0 (y ⊙⇩1 z) ⊆ (w ⊙⇩0 y) *⇩1 (x ⊙⇩0 z)"
  and t0_hom: "Tgt⇩0 (x ⊙⇩1 y) = τ⇩0 x ⊙⇩1 τ⇩0 y"  (* this is too strong *)
  and t1_hom: "Tgt⇩1 (x ⊙⇩0 y) = τ⇩1 x ⊙⇩0 τ⇩1 y"
  and s0_hom: "Src⇩0 (x ⊙⇩1 y) = σ⇩0 x ⊙⇩1 σ⇩0 y" (* this is too strong *)
  and s1_hom: "Src⇩1 (x ⊙⇩0 y) = σ⇩1 x ⊙⇩0 σ⇩1 y" 
  and s1_s0 [simp]: "σ⇩1 (σ⇩0 x) = σ⇩0 x" 
  and t1_s0 [simp]: "τ⇩1 (σ⇩0 x) = σ⇩0 x"  
  and s1_t0 [simp]: "σ⇩1 (τ⇩0 x) = τ⇩0 x" 
  and t1_t0 [simp]: "τ⇩1 (τ⇩0 x) = τ⇩0 x" 

begin

text ‹The source and target structure collapses.›

lemma s0s1: "σ⇩0 x = σ⇩1 x"
proof-
  have "Src⇩0 (σ⇩1 x ⊙⇩1 σ⇩0 (σ⇩1 x)) = σ⇩0 (σ⇩1 x) ⊙⇩1 σ⇩0 (σ⇩0 (σ⇩1 x))"
    by (simp add: local.s0_hom)
  also have "…  = σ⇩1 (σ⇩0 (σ⇩1 x)) ⊙⇩1 σ⇩0 (σ⇩1 x)"
    by simp
  also have "… = {σ⇩0 (σ⇩1 x)}"
    using local.src1_absorb by presburger
  also have "… ≠ {}" 
   by (metis insert_not_empty)
  finally have "Src⇩0 (σ⇩1 x ⊙⇩1 σ⇩0 (σ⇩1 x)) ≠ {}".
  hence "σ⇩1 x ⊙⇩1 σ⇩0 (σ⇩1 x) ≠ {}" 
    by (metis image_empty) 
  hence "τ⇩1 (σ⇩1 x) = σ⇩1 (σ⇩0 (σ⇩1 x))"
    using local.Dst1 by presburger
  hence "σ⇩1 x = σ⇩1 (σ⇩0 (σ⇩1 x))"
    by simp
  also have "… = σ⇩1 (σ⇩1 (σ⇩0 x))"
    by (simp add: local.comm_s0s1)
  also have "… = σ⇩1 (σ⇩0 x)"
    by simp
  also have "… = σ⇩0 x"
    by simp
  finally show ?thesis..
qed

lemma t0t1: "τ⇩0 x = τ⇩1 x"
  using local.comm_s0t1 local.commtr0s1 local.s0s1 stmm0.ts_compat by force

lemma s0t0: "σ⇩0 x = τ⇩0 x"
proof-
  have "σ⇩0 x = τ⇩1 (σ⇩0 x)"
    by simp
  also have "… = σ⇩0 (τ⇩1 x)"
    by (simp add: local.comm_s0t1)
  also have "… = σ⇩0 (τ⇩0 x)"
    by (simp add: t0t1)
  also have "… = τ⇩0 x "
    by simp
  finally show ?thesis.
qed

lemma "σ⇩0 x = x"
  (*nitpick [expect = genuine]*)
  oops 

lemma s1t1: "σ⇩1 x = τ⇩1 x"
  using local.s0s1 s0t0 t0t1 by force

lemma "x ∈ y ⊙⇩0 z ⟹ x' ∈ y ⊙⇩0 z ⟹ x = x'"
  (*nitpick [expect = genuine]*)
  oops 

lemma "x ∈ y ⊙⇩1 z ⟹ x' ∈ y ⊙⇩1 z ⟹ x = x'"
  (*nitpick [expect = genuine]*)
  oops 

text ‹The two compositions are still different---but see below for 2-catoids.›

end

subsection‹2-Catoids with (too) strong homomorphisms›

class two_catoid_collapse = two_st_multimagma_collapse + catoid0 + catoid1

begin

text ‹The two compositions are still different, and neither of them commutes.›

lemma "x ⊙⇩0 y = x ⊙⇩1 y"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙⇩0 y = y ⊙⇩0 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙⇩1 y = y ⊙⇩1 x"
  (*nitpick [expect = genuine]*)
  oops

end

subsection‹Single-set 2-categories with (too) strong homomorphisms›

class two_category_collapse = two_catoid_collapse + single_set_category0 + single_set_category1

begin

lemma comp_collapse: "x ⊙⇩0 y = x ⊙⇩1 y"
  by (smt (verit, del_insts) local.interchange local.mm0.conv_atom local.mm1.conv_atom local.pm1.functionality_lem_var local.s0s1 local.src0_absorb local.src1_absorb local.stmsg1.sts_msg.st_local local.t0t1 local.tgt0_absorb local.tgt1_absorb ssmsg0.st_local subset_singleton_iff)

lemma comp0_comm: "x ⊙⇩0 y = y ⊙⇩0 x"
  by (smt (verit, best) bot_set_def comp_collapse doubleton_eq_iff local.interchange local.mm0.conv_atom local.mm1.conv_atom local.pm0.functionality_lem_var local.s0t0 local.src0_absorb local.tgt0_absorb singleton_insert_inj_eq' ssmsg0.st_local)

lemma comp1_comm: "x ⊙⇩1 y = y ⊙⇩1 x"
  using comp0_comm comp_collapse by auto

lemma "σ⇩0 x = x"
  (*nitpick [expect = genuine]*)
  oops 

lemma "σ⇩0 x = σ⇩0 y"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙⇩0 y ≠ {}"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙⇩1 y ≠ {}"
  (*nitpick [expect = genuine]*)
  oops

end

subsection ‹2-lr-Multimagmas with strong interchange law›

class two_lr_multimagma_bad = st_multimagma0 + st_multimagma1 +
  assumes comm_s0s1: "σ⇩0 (σ⇩1 x) = σ⇩1 (σ⇩0 x)"
  and comm_t0t1: "τ⇩0 (τ⇩1 x) = τ⇩1 (τ⇩0 x)"
  and comm_s0t1: "σ⇩0 (τ⇩1 x) = τ⇩1 (σ⇩0 x)"
  and comm_t0s1: "τ⇩0 (σ⇩1 x) = σ⇩1 (τ⇩0 x)"
  assumes interchange: "(w ⊙⇩1 x) *⇩0 (y ⊙⇩1 z) = (w ⊙⇩0 y) *⇩1 (x ⊙⇩0 z)" (* this is too strong *)
  and t0_hom: "Tgt⇩0 (x ⊙⇩1 y) = τ⇩0 x ⊙⇩1 τ⇩0 y"
  and t1_hom: "Tgt⇩1 (x ⊙⇩0 y) = τ⇩1 x ⊙⇩0 τ⇩1 y"
  and s0_hom: "Src⇩0 (x ⊙⇩1 y) ⊆ σ⇩0 x ⊙⇩1 σ⇩0 y" 
  and s1_hom: "Src⇩1 (x ⊙⇩0 y) ⊆ σ⇩1 x ⊙⇩0 σ⇩1 y" 
  and s1_s0 [simp]: "σ⇩1 (σ⇩0 x) = σ⇩0 x" 
  and t1_s0 [simp]: "τ⇩1 (σ⇩0 x) = σ⇩0 x"  
  and s1_t0 [simp]: "σ⇩1 (τ⇩0 x) = τ⇩0 x" 
  and t1_t0 [simp]: "τ⇩1 (τ⇩0 x) = τ⇩0 x" 

begin

text ‹The source and target structure collapses.›

lemma s0s1: "σ⇩0 x = σ⇩1 x"
  by (metis image_empty local.comm_s0s1 local.s1_s0 local.stmm0.stopp.st_fix local.stmm0.stopp.ts_compat local.t0_hom stmm1.s_absorb_var3)

lemma t0t1: "τ⇩0 x = τ⇩1 x"
  using local.comm_s0t1 local.comm_t0s1 local.s0s1 stmm0.ts_compat by auto

lemma s0t0: "σ⇩0 x = τ⇩0 x"
proof-
  have "σ⇩0 x = τ⇩1 (σ⇩0 x)"
    by simp
  also have "… = σ⇩0 (τ⇩1 x)"
    by (simp add: local.comm_s0t1)
  also have "… = σ⇩0 (τ⇩0 x)"
    by (simp add: local.t0t1)
  also have "… = τ⇩0 x "
    by simp
  finally show ?thesis.
qed

lemma s1t1: "σ⇩1 x = τ⇩1 x"
  using local.comm_t0s1 local.t0t1 by force

lemma comp_collapse: "x ⊙⇩0 y = x ⊙⇩1 y"
  by (metis (no_types, opaque_lifting) local.interchange local.s0s1 local.src0_absorb local.src1_absorb local.stmm0.stopp.Dst local.stmm1.stopp.Dst local.t0t1 local.tgt0_absorb local.tgt1_absorb multimagma.conv_atom)

lemma comp0_comm: "x ⊙⇩0 y = y ⊙⇩0 x"
  by (metis local.comp_collapse local.interchange local.mm0.conv_atom local.s0s1 local.s1t1 local.src0_absorb local.tgt1_absorb stmm1.t_comm)

lemma comp1_comm: "x ⊙⇩1 y = y ⊙⇩1 x"
  using local.comp0_comm local.comp_collapse by auto

lemma comp0_assoc: "{x} *⇩0 (y ⊙⇩0 z) = (x ⊙⇩0 y) *⇩0 {z}"
  by (smt (z3) local.comp_collapse local.interchange local.s1t1 local.src1_absorb local.stmm0.stopp.Dst local.stmm0.stopp.s_assoc local.stmm1.stopp.conv_atom local.t0t1 local.t1_t0 local.tgt1_absorb)

lemma comp1_assoc: "{x} *⇩1 (y ⊙⇩1 z) = (x ⊙⇩1 y) *⇩1 {z}"
  by (metis (full_types) local.comp0_assoc local.comp1_comm local.comp_collapse local.interchange local.tgt1_absorb)

lemma "σ⇩0 x = x"
  (*nitpick [expect = genuine]*)
  oops 

lemma "σ⇩0 x = σ⇩0 y"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙⇩0 y ≠ {}"
  (*nitpick [expect = genuine]*) 
  oops

lemma "x ∈ y ⊙⇩0 z ⟹ x' ∈ y ⊙⇩0 z ⟹ x = x'"
  (*nitpick [expect = genuine]*)
  oops 

lemma "x ⊙⇩1 y ≠ {}"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ∈ y ⊙⇩1 z ⟹ x' ∈ y ⊙⇩1 z ⟹ x = x'"
  (*nitpick [expect = genuine]*)
  oops 

end

end