Theory Category

(*
Author: Alexander Katovsky
*)

section "Category"

theory Category
imports "HOL-Library.FuncSet"
begin

record ('o,'m) Category = 
  Obj :: "'o set" (‹objı› 70) 
  Mor :: "'m set" (‹morı› 70)
  Dom :: "'m ⇒ 'o" (‹domı _› [80] 70)
  Cod :: "'m ⇒ 'o" (‹codı _› [80] 70)
  Id  :: "'o ⇒ 'm" (‹idı _› [80] 75)
  Comp :: "'m ⇒ 'm ⇒ 'm" (infixl ‹;;ı› 70)

definition
  MapsTo :: "('o,'m,'a) Category_scheme ⇒ 'm ⇒ 'o ⇒ 'o ⇒ bool" (‹_ mapsı _ to _› [60, 60, 60] 65) where
  "MapsTo CC f X Y ≡ f ∈ Mor CC ∧ Dom CC f = X ∧ Cod CC f = Y"

definition
  CompDefined :: "('o,'m,'a) Category_scheme ⇒ 'm ⇒ 'm ⇒ bool" (infixl ‹≈>ı› 65) where
  "CompDefined CC f g ≡ f ∈ Mor CC ∧ g ∈ Mor CC ∧ Cod CC f = Dom CC g"

locale ExtCategory = 
  fixes C :: "('o,'m,'a) Category_scheme" (structure)
  assumes CdomExt: "(Dom C) ∈ extensional (Mor C)"
  and     CcodExt: "(Cod C) ∈ extensional (Mor C)"
  and     CidExt:  "(Id C) ∈ extensional (Obj C)"
  and     CcompExt:  "(case_prod (Comp C)) ∈ extensional ({(f,g) | f g . f ≈> g})"

locale Category = ExtCategory +
  assumes Cdom : "f ∈ mor ⟹ dom f ∈ obj"
  and     Ccod : "f ∈ mor ⟹ cod f ∈ obj"
  and     Cidm [dest]: "X ∈ obj ⟹ (id X) maps X to X"
  and     Cidl : "f ∈ mor ⟹ id (dom f) ;; f = f"
  and     Cidr : "f ∈ mor ⟹ f ;; id (cod f) = f"
  and     Cassoc : "⟦f ≈> g ; g ≈> h⟧ ⟹ (f ;; g) ;; h = f ;; (g ;; h)"
  and     Ccompt : "⟦f maps X to Y ; g maps Y to Z⟧ ⟹ (f ;; g) maps X to Z"

definition 
  MakeCat :: "('o,'m,'a) Category_scheme ⇒ ('o,'m,'a) Category_scheme" where
  "MakeCat C ≡ ⦇
      Obj = Obj C , 
      Mor = Mor C , 
      Dom = restrict (Dom C) (Mor C) , 
      Cod = restrict (Cod C) (Mor C) , 
      Id  = restrict (Id C) (Obj C) , 
      Comp = λ f g . (restrict (case_prod (Comp C)) ({(f,g) | f g . f ≈>⇘C⇙ g})) (f,g), 
      … = Category.more C
  ⦈"

lemma MakeCatMapsTo: "f maps⇘C⇙ X to Y ⟹ f maps⇘MakeCat C⇙ X to Y"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatComp: "f ≈>⇘C⇙ g ⟹ f ;;⇘MakeCat C⇙ g = f ;;⇘C⇙ g"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatId: "X ∈ obj⇘C⇙ ⟹ id⇘C⇙ X = id⇘MakeCat C⇙ X"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatObj: "obj⇘MakeCat C⇙ = obj⇘C⇙"
by (simp add: MakeCat_def)

lemma MakeCatMor: "mor⇘MakeCat C⇙ = mor⇘C⇙"
by (simp add: MakeCat_def)

lemma MakeCatDom: "f ∈ mor⇘C⇙ ⟹ dom⇘C⇙ f = dom⇘MakeCat C⇙ f"
by (simp add: MakeCat_def)

lemma MakeCatCod: "f ∈ mor⇘C⇙ ⟹ cod⇘C⇙ f = cod⇘MakeCat C⇙ f"
by (simp add: MakeCat_def)


lemma MakeCatCompDef: "f ≈>⇘MakeCat C⇙ g = f ≈>⇘C⇙ g"
by (auto simp add: CompDefined_def MakeCat_def)

lemma MakeCatComp2: "f ≈>⇘MakeCat C⇙ g ⟹ f ;;⇘MakeCat C⇙ g = f ;;⇘C⇙ g"
by (simp add: MakeCatCompDef MakeCatComp)


lemma ExtCategoryMakeCat: "ExtCategory (MakeCat C)"
by (unfold_locales, simp_all add: MakeCat_def extensional_def CompDefined_def)

lemma MakeCat: "Category_axioms C ⟹ Category (MakeCat C)"
apply(intro_locales, simp add: ExtCategoryMakeCat)
apply (simp add: Category_axioms_def)
apply (auto simp add: MakeCat_def CompDefined_def MapsTo_def)
done

lemma MapsToE[elim]: "⟦f maps⇘C⇙ X to Y ; ⟦f ∈ mor⇘C⇙ ; dom⇘C⇙ f = X ; cod⇘C⇙ f = Y⟧ ⟹ R⟧ ⟹ R"
  by (auto simp add: MapsTo_def)

lemma MapsToI[intro]: "⟦f ∈ mor⇘C⇙ ; dom⇘C⇙ f = X ; cod⇘C⇙ f = Y⟧ ⟹ f maps⇘C⇙ X to Y"
  by (auto simp add: MapsTo_def)

lemma CompDefinedE[elim]: "⟦f ≈>⇘C⇙ g ; ⟦f ∈ mor⇘C⇙ ; g ∈ mor⇘C⇙ ; cod⇘C⇙ f = dom⇘C⇙ g⟧ ⟹ R⟧ ⟹ R"
  by (auto simp add: CompDefined_def)

lemma CompDefinedI[intro]: "⟦f ∈ mor⇘C⇙ ; g ∈ mor⇘C⇙ ; cod⇘C⇙ f = dom⇘C⇙ g⟧ ⟹ f ≈>⇘C⇙ g"
  by (auto simp add: CompDefined_def)

lemma (in Category) MapsToCompI: assumes "f ≈> g" shows "(f ;; g) maps (dom f) to (cod g)"
proof-
  have "f maps (dom f) to (dom g)" 
  and  "g maps (dom g) to (cod g)" using assms by auto
  thus ?thesis by (simp add: Ccompt[of f "dom f" "dom g" g "cod g"])
qed

lemma MapsToCompDef:
  assumes "f maps⇘C⇙ X to Y" and "g maps⇘C⇙ Y to Z"
  shows "f ≈>⇘C⇙ g"
proof(rule CompDefinedI)
  show "f ∈ mor⇘C⇙" and "g ∈ mor⇘C⇙" using assms by auto
  have "cod⇘C⇙ f = Y" and "dom⇘C⇙ g = Y" using assms by auto
  thus "cod⇘C⇙ f = dom⇘C⇙ g" by simp
qed

lemma (in Category) MapsToMorDomCod: 
  assumes "f ≈> g" 
  shows "f ;; g ∈ mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g"
proof-
  have "(f ;; g) maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)
  thus "f ;; g ∈ mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g" by auto
qed

lemma (in Category) MapsToObj: 
  assumes "f maps X to Y"
  shows "X ∈ obj" and "Y ∈ obj"
proof-
  have "dom f = X" and "cod f = Y" and "f ∈ mor" using assms by auto
  thus "X ∈ obj" and "Y ∈ obj" by (auto simp add: Cdom Ccod)
qed

lemma (in Category) IdInj: 
  assumes "X ∈ obj" and "Y ∈ obj" and "id X = id Y"
  shows   "X = Y"
proof-
  have "dom (id X) = dom (id Y)" using assms by simp
  moreover have "dom (id X) = X" and "dom (id Y) = Y" using assms by (auto simp add: MapsTo_def)
  ultimately show ?thesis by simp
qed

lemma (in Category) CompDefComp:
  assumes "f ≈> g" and "g ≈> h"
  shows "f ≈> (g ;; h)" and "(f ;; g) ≈> h"
proof(auto simp add: CompDefined_def)
  show "f ∈ mor" and "h ∈ mor" using assms by auto
  have  1: "g ;; h maps (dom g) to (cod h)" 
    and 2: "f ;; g maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)+
  thus "g ;; h ∈ mor" and "f ;; g ∈ mor" by auto
  have "cod f = dom g" using assms by auto
  also have "... = dom (g ;; h)" using 1 by auto
  finally show "cod f = dom (g ;; h)" .
  have "dom h = cod g" using assms by auto
  also have "... = cod (f ;; g)" using 2 by auto
  finally show "cod (f ;; g) = dom h" by simp
qed

lemma (in Category) CatIdInMor: "X ∈ obj ⟹ id X ∈ mor"
by (auto simp add: Cidm)

lemma (in Category) MapsToId: assumes "X ∈ obj" shows "id X ≈> id X"
proof(rule CompDefinedI)
  have "id X maps X to X" using assms by (simp add: Cidm)
  thus "id X ∈ mor" and "id X ∈ mor" and "cod (id X) = dom (id X)" by auto
qed

lemmas (in Category) Simps = Cdom Ccod Cidm Cidl Cidr MapsToCompI IdInj MapsToId

lemma (in Category) LeftRightInvUniq: 
  assumes 0: "h ≈> f" and  z: "f ≈> g"
  assumes 1: "f ;; g = id (dom f)" 
  and     2: "h ;; f = id (cod f)"
  shows   "h = g"
proof-
  have mor: "h ∈ mor ∧ g ∈ mor" 
  and  dc : "dom f = cod h ∧ cod f = dom g" using 0 z by auto
  then have "h = h ;; id (dom f)" by (auto simp add: Simps)
  also have "... = h ;; (f ;; g)" using 1 by simp+
  also have "... = (h ;; f) ;; g" using 0 z by (simp add: Cassoc)
  also have "... = (id (cod f)) ;; g" using 2 by simp+
  also have "... = g" using mor dc by (auto simp add: Simps)
  finally show ?thesis .
qed

lemma (in Category) CatIdDomCod:
  assumes "X ∈ obj"
  shows "dom (id X) = X" and "cod (id X) = X"
proof-
  have "id X maps X to X" using assms
    by (simp add: Simps)
  thus "dom (id X) = X" and "cod (id X) = X" by auto
qed

lemma (in Category) CatIdCompId:
  assumes "X ∈ obj"
  shows   "id X ;; id X = id X"
proof-
  have 0: "id X ∈ mor" using assms by (auto simp add: Simps)
  moreover have "cod (id X) = X" using assms by auto
  moreover have "id X ;; id (cod (id X)) = id X" using 0 by (simp add: Simps)
  ultimately show ?thesis by simp
qed

(*lemmas (in Category) simps2 = simps CatIdCompId Cassoc CatIdDomCod*)

lemma (in Category) CatIdUniqR: 
  assumes iota: "ι maps X to X"
  and     rid:  "∀ f . f ≈> ι ⟶ f ;; ι = f"
  shows "id X = ι"
proof(rule LeftRightInvUniq [of "id X" "id X" ι ])
  have 0: "X ∈ obj" using iota by (auto simp add: Simps)
  hence "id X maps X to X" by (simp add: Cidm)
  thus 1: "id X ≈> ι" using iota by (auto simp add: Simps)
  show    "id X ≈> id X" using 0 by (auto simp add: Simps)
  show    "(id X) ;; ι = (id (dom (id X)))" using 0 1 rid by (auto simp add: Simps CompDefined_def MapsTo_def)
  show    "(id X) ;; (id X) = (id (cod (id X)))" using 0 by (auto simp add: CatIdCompId CompDefined_def MapsTo_def)
qed
  
definition
  inverse_rel :: "('o,'m,'a) Category_scheme ⇒ 'm ⇒ 'm ⇒ bool" (‹cinvı _ _› 60) where
  "inverse_rel C f g ≡ (f ≈>⇘C⇙ g) ∧ (f ;;⇘C⇙ g) = (id⇘C⇙ (dom⇘C⇙ f)) ∧ (g ;;⇘C⇙ f) = (id⇘C⇙ (cod⇘C⇙ f))"

definition 
  isomorphism :: "('o,'m,'a) Category_scheme ⇒ 'm ⇒ bool" (‹cisoı _› [70]) where
  "isomorphism C f ≡ ∃ g . inverse_rel C f g"

lemma (in Category) Inverse_relI: "⟦f ≈> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)⟧ ⟹ (cinv f g)"
by (auto simp add: inverse_rel_def)

lemma (in Category) Inverse_relE[elim]: "⟦cinv f g ; ⟦f ≈> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)⟧ ⟹ P⟧ ⟹ P"
by (auto simp add: inverse_rel_def)

lemma (in Category) Inverse_relSym: 
  assumes "cinv f g"
  shows   "cinv g f"
proof(rule Inverse_relI)
  have 1: "f ≈> g" using assms by auto
  show 2: "g ≈> f"
  proof(rule CompDefinedI)
    show "g ∈ mor" and 0: "f ∈ mor" using assms by auto
    have "f ;; g maps dom f to cod g" using 1 by (simp add: MapsToCompI)
    hence "cod g = cod (f ;; g)" by auto
    also have "... = cod (id (dom f))" using assms by (auto simp add: inverse_rel_def)
    also have "... = dom f"
    proof-
      have "dom f ∈ obj" using 0 by (simp add: Simps)
      hence "id (dom f) maps (dom f) to (dom f)" by (simp add: Simps)
      thus ?thesis by auto
    qed
    finally show 2: "cod g = dom f" by simp
  qed
  show "g ;; f = id (dom g)" using assms by (auto simp add: inverse_rel_def)
  show "f ;; g = id (cod g)"using assms 1 2 by (auto simp add: inverse_rel_def)
qed

lemma (in Category) InverseUnique: 
  assumes 1: "cinv f g"
  and     2: "cinv f h"
  shows   "g = h"
proof(rule LeftRightInvUniq [of g f h])
  have "cinv g f" using 1 2 by (simp only: Inverse_relSym[of f g])
  thus "g ≈> f" and
    "g ;; f = id (cod f)" using 1 by auto
  show "f ≈> h" using 2 by auto
  show "f ;; h = id (dom f)" using 2 by auto
qed

lemma (in Category) InvId: assumes "X ∈ obj" shows "(cinv (id X) (id X))"
proof(rule Inverse_relI)
  show "id X ≈> id X" using assms by (simp add: Simps)
  have "dom (id X) = X" and "dom (id X) = X" using assms by (simp add: CatIdDomCod)+
  thus "id X ;; id X = id (dom (id X))" and "id X ;; id X = id (cod (id X))" 
    using assms by (simp add: CatIdCompId CatIdDomCod)+
qed
    
definition
  inverse :: "('o,'m,'a) Category_scheme ⇒ 'm ⇒ 'm" (‹Cinvı _› [70]) where
  "inverse C f ≡ THE g . inverse_rel C f g"

lemma (in Category) inv2Inv:
  assumes "cinv f g"
  shows   "ciso f" and "Cinv f = g"
proof-
  show "ciso f" using assms by (auto simp add: isomorphism_def)
  hence "∃! g . cinv f g" using assms by (auto simp add: InverseUnique)
  thus "Cinv f = g" using assms by (auto simp add: inverse_def)
qed

lemma (in Category) iso2Inv:
  assumes "ciso f"
  shows   "cinv f (Cinv f)"
proof-
  have "∃! g . cinv f g" using assms by (auto simp add: InverseUnique isomorphism_def)
  thus ?thesis by (auto simp add:  inverse_def intro:theI')
qed

lemma (in Category) InvInv:
  assumes "ciso f" 
  shows   "ciso (Cinv f)" and "(Cinv (Cinv f)) = f"
proof-
  have "cinv f (Cinv f)" using assms by (simp add: iso2Inv)
  hence "cinv (Cinv f) f" by (simp add: Inverse_relSym[of f])
  thus  "ciso (Cinv f)" and "Cinv (Cinv f) = f" by (auto simp add: inv2Inv)
qed

lemma (in Category) InvIsMor: "(cinv f g) ⟹ (f ∈ mor ∧ g ∈ mor)"
  by (auto simp add: inverse_rel_def)

lemma (in Category) IsoIsMor: "ciso f ⟹ f ∈ mor"
  by (auto simp add: InvIsMor dest: iso2Inv)

lemma (in Category) InvDomCod:
  assumes "ciso f"
  shows "dom (Cinv f) = cod f" and "cod (Cinv f) = dom f" and "Cinv f ∈ mor"
proof-
  have 1: "cinv f (Cinv f)" using assms by (auto simp add: iso2Inv)
  thus "dom (Cinv f) = cod f" by (auto simp add: inverse_rel_def)
  from 1 have "cinv (Cinv f) f" by (auto simp add: Inverse_relSym[of f])
  thus  "cod (Cinv f) = dom f" by (auto simp add: inverse_rel_def)
  show "Cinv f ∈ mor" using 1 by (auto simp add: inverse_rel_def)
qed

lemma (in Category) IsoCompInv: "ciso f ⟹ f ≈> Cinv f"
  by (auto simp add: IsoIsMor InvDomCod)

lemma (in Category) InvCompIso: "ciso f ⟹ Cinv f ≈> f"
  by (auto simp add: IsoIsMor InvDomCod)

lemma (in Category) IsoInvId1 : "ciso f ⟹ (Cinv f) ;; f = (id (cod f))"
by (auto dest: iso2Inv)

lemma (in Category) IsoInvId2 :  "ciso f ⟹ f ;; (Cinv f) = (id (dom f))"
by (auto dest: iso2Inv)

lemma (in Category) IsoCompDef:
  assumes 1: "f ≈> g" and 2: "ciso f" and 3: "ciso g"
  shows "(Cinv g) ≈> (Cinv f)"
proof(rule CompDefinedI)
  show "Cinv g ∈ mor" and "Cinv f ∈ mor" using assms by (auto simp add: InvDomCod)
  have "cod (Cinv g) = dom g" using 3 by (simp add: InvDomCod)
  also have "... = cod f" using 1 by auto
  also have "... = dom (Cinv f)" using 2 by (simp add: InvDomCod)
  finally show "cod (Cinv g) = dom (Cinv f)" .
qed

lemma (in Category) IsoCompose: 
  assumes 1: "f ≈> g" and 2: "ciso f" and 3: "ciso g"
  shows "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)"
proof-
  have  a: "(Cinv g) ≈> (Cinv f)" using assms by (simp add: IsoCompDef)
  hence b: "(Cinv g) ;; (Cinv f) maps (dom (Cinv g)) to (cod (Cinv f))" by (simp add: MapsToCompI)
  hence c: "(Cinv g) ;; (Cinv f) maps (cod g) to (dom f)" using 2 3 by (simp add: InvDomCod) 
  have  d: "f ;; g maps (dom f) to (cod g)" using 1 by (simp add: Simps)
  have "cinv (f ;; g) ((Cinv g) ;; (Cinv f))"
  proof(auto simp add: inverse_rel_def)
    show "f ;; g ≈> (Cinv g) ;; (Cinv f)"
    proof(rule CompDefinedI)
      show "f ;; g ∈ mor" using d by auto
      show "(Cinv g) ;; (Cinv f) ∈ mor" using c by auto
      have "cod (f ;; g) = cod g" using d by auto
      also have "... = dom (Cinv g)" using assms by (simp add: InvDomCod)
      also have "... = dom ((Cinv g) ;; (Cinv f))" using b by auto
      finally show "cod (f ;; g) = dom ((Cinv g) ;; (Cinv f))" .
    qed
    show "f ;; g ;; ((Cinv g) ;; (Cinv f)) = id (dom (f ;; g))"
    proof-
      have e: "g ≈> (Cinv g)" using assms by (simp add: IsoCompInv)
      have f: "f ∈ mor" using 1 by auto
      have "(f ;; g) ;; ((Cinv g) ;; (Cinv f)) = (f ;; (g ;; (Cinv g))) ;; (Cinv f)" 
        using 1 e a by (auto simp add: Cassoc CompDefComp)
      also have "... = f ;; (id (dom g)) ;; (Cinv f)" using 3 by (simp add: IsoInvId2)
      also have "... = f ;; id (cod f) ;; (Cinv f)" using 1 by (auto simp add: Simps)
      also have "... = f ;; (Cinv f)" using f by (auto simp add: Cidr)
      also have "... = id (dom f)" using 2 by (simp add: IsoInvId2)
      also have "... = id (dom (f ;; g))" using d by auto
      finally show ?thesis by simp
    qed
    show "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = id (cod (f ;; g))"
    proof-
      have e: "(Cinv f) ≈> f" using assms by (simp add: InvCompIso)
      have f: "g ∈ mor" using 1 by auto
      have "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = (Cinv g) ;; (((Cinv f) ;; f) ;; g)"
        using 1 e a by (auto simp add: Cassoc CompDefComp)
      also have "... = (Cinv g) ;; ((id (cod f)) ;; g)" using 2 by (simp add: IsoInvId1)
      also have "... = (Cinv g) ;; ((id (dom g)) ;; g)" using 1 by (auto simp add: Simps)
      also have "... = (Cinv g) ;; g" using f by (auto simp add: Cidl)
      also have "... = id (cod g)" using 3 by (simp add: IsoInvId1)
      also have "... = id (cod (f ;; g))" using d by auto
      finally show ?thesis by simp
    qed
  qed
  thus "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)" by (auto simp add: inv2Inv)
qed

definition "ObjIso C A B ≡ ∃ k . (k maps⇘C⇙ A to B) ∧ ciso⇘C ⇙k"

definition 
  UnitCategory :: "(unit, unit) Category" where
  "UnitCategory = MakeCat ⦇
      Obj = {()} , 
      Mor = {()} , 
      Dom = (λf.()) , 
      Cod = (λf.()) , 
      Id = (λf.()) , 
      Comp = (λf g. ())
  ⦈"

lemma [simp]: "Category(UnitCategory)"
apply (simp add: UnitCategory_def, rule MakeCat)
by (unfold_locales, auto simp add: UnitCategory_def)

definition 
  OppositeCategory :: "('o,'m,'a) Category_scheme ⇒ ('o,'m,'a) Category_scheme" (‹Op _› [65] 65) where
  "OppositeCategory C ≡ ⦇
      Obj = Obj C , 
      Mor = Mor C , 
      Dom = Cod C , 
      Cod = Dom C , 
      Id  = Id C , 
      Comp = (λf g. g ;;⇘C⇙ f), 
      … = Category.more C
  ⦈"

lemma OpCatOpCat: "Op (Op C) = C"
  by (simp add: OppositeCategory_def)


lemma OpCatCatAx: "Category_axioms C ⟹ Category_axioms (Op C)"
  by (simp add: OppositeCategory_def Category_axioms_def MapsTo_def CompDefined_def)

lemma OpCatCatExt: "ExtCategory C ⟹ ExtCategory (Op C)"
  by (auto simp add: OppositeCategory_def ExtCategory_def MapsTo_def CompDefined_def extensional_def)

lemma OpCatCat: "Category C ⟹ Category (Op C)"
  by (intro_locales, simp_all add: Category_def OpCatCatAx OpCatCatExt)


lemma MapsToOp: "f maps⇘C ⇙X to Y ⟹ f maps⇘Op C ⇙Y to X"
by (simp add: MapsTo_def OppositeCategory_def)

lemma MapsToOpOp: "f maps⇘Op C ⇙X to Y ⟹ f maps⇘C ⇙Y to X"
by (simp add: MapsTo_def OppositeCategory_def)

lemma CompDefOp: "f ≈>⇘C⇙ g ⟹ g ≈>⇘Op C⇙ f"
by (simp add: CompDefined_def OppositeCategory_def)

end