Theory Yoneda
section "Yoneda"
theory Yoneda
imports NatTrans SetCat
begin
definition "YFtorNT' C f ≡ ⦇NTDom = Hom⇘C⇙[─,dom⇘C⇙ f] , NTCod = Hom⇘C⇙[─,cod⇘C⇙ f] ,
NatTransMap = λ B . Hom⇘C⇙[B,f]⦈"
definition "YFtorNT C f ≡ MakeNT (YFtorNT' C f)"
lemmas YFtorNT_defs = YFtorNT'_def YFtorNT_def MakeNT_def
lemma YFtorNTCatDom: "NTCatDom (YFtorNT C f) = Op C"
by (simp add: YFtorNT_defs NTCatDom_def HomFtorContraDom)
lemma YFtorNTCatCod: "NTCatCod (YFtorNT C f) = SET"
by (simp add: YFtorNT_defs NTCatCod_def HomFtorContraCod)
lemma YFtorNTApp1: assumes "X ∈ Obj (NTCatDom (YFtorNT C f))" shows "(YFtorNT C f) $$ X = Hom⇘C⇙[X,f]"
proof-
have "(YFtorNT C f) $$ X = (YFtorNT' C f) $$ X" using assms by (simp add: MakeNTApp YFtorNT_def)
thus ?thesis by (simp add: YFtorNT'_def)
qed
definition
"YFtor' C ≡ ⦇
CatDom = C ,
CatCod = CatExp (Op C) SET ,
MapM = λ f . YFtorNT C f
⦈"
definition "YFtor C ≡ MakeFtor(YFtor' C)"
lemmas YFtor_defs = YFtor'_def YFtor_def MakeFtor_def
lemma YFtorNTNatTrans':
assumes "LSCategory C" and "f ∈ Mor C"
shows "NatTransP (YFtorNT' C f)"
proof(auto simp only: NatTransP_def)
have Fd: "Ftor (NTDom (YFtorNT' C f)) : (Op C) ⟶ SET" using assms
by (simp add: HomFtorContraFtor Category.Cdom YFtorNT'_def)
have Fc: "Ftor (NTCod (YFtorNT' C f)) : (Op C) ⟶ SET" using assms
by (simp add: HomFtorContraFtor Category.Ccod YFtorNT'_def)
show "Functor (NTDom (YFtorNT' C f))" using Fd by auto
show "Functor (NTCod (YFtorNT' C f))" using Fc by auto
show "NTCatDom (YFtorNT' C f) = CatDom (NTCod (YFtorNT' C f))"
by(simp add: YFtorNT'_def NTCatDom_def HomFtorContraDom)
show "NTCatCod (YFtorNT' C f) = CatCod (NTDom (YFtorNT' C f))"
by(simp add: YFtorNT'_def NTCatCod_def HomFtorContraCod)
{
fix X assume a: "X ∈ Obj (NTCatDom (YFtorNT' C f))"
show "(YFtorNT' C f) $$ X maps⇘NTCatCod (YFtorNT' C f)⇙ (NTDom (YFtorNT' C f) @@ X) to (NTCod (YFtorNT' C f) @@ X)"
proof-
have Obj: "X ∈ Obj C" using a by (simp add: NTCatDom_def YFtorNT'_def HomFtorContraDom OppositeCategory_def)
have H1: "(Hom⇘C⇙[─,dom⇘C⇙ f]) @@ X = Hom⇘C ⇙X dom⇘C⇙ f " using assms Obj by(simp add: HomFtorOpObj Category.Cdom)
have H2: "(Hom⇘C⇙[─,cod⇘C⇙ f]) @@ X = Hom⇘C ⇙X cod⇘C⇙ f " using assms Obj by(simp add: HomFtorOpObj Category.Ccod)
have "Hom⇘C⇙[X,f] maps⇘SET⇙ (Hom⇘C ⇙X dom⇘C⇙ f) to (Hom⇘C ⇙X cod⇘C⇙ f)" using assms Obj by (simp add: HomFtorMapsTo)
thus ?thesis using H1 H2 by(simp add: YFtorNT'_def NTCatCod_def NTCatDom_def HomFtorContraCod)
qed
}
{
fix g X Y assume a: "g maps⇘NTCatDom (YFtorNT' C f)⇙ X to Y"
show "((NTDom (YFtorNT' C f)) ## g) ;;⇘NTCatCod (YFtorNT' C f) ⇙(YFtorNT' C f $$ Y) =
((YFtorNT' C f) $$ X) ;;⇘NTCatCod (YFtorNT' C f) ⇙(NTCod (YFtorNT' C f) ## g)"
proof-
have M1: "g maps⇘Op C⇙ X to Y" using a by (auto simp add: NTCatDom_def YFtorNT'_def HomFtorContraDom)
have D1: "dom⇘C⇙ g = Y" and C1: "cod⇘C⇙ g = X" using M1 by (auto simp add: OppositeCategory_def)
have morf: "f ∈ Mor C" and morg: "g ∈ Mor C" using assms M1 by (auto simp add: OppositeCategory_def)
have H1: "(HomC⇘C⇙[g,dom⇘C⇙ f]) = (Hom⇘C⇙[─,dom⇘C⇙ f]) ## g"
and H2: "(HomC⇘C⇙[g,cod⇘C⇙ f]) = (Hom⇘C⇙[─,cod⇘C⇙ f]) ## g" using M1
by (auto simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
have "(HomC⇘C⇙[g,dom⇘C⇙ f]) ;;⇘SET⇙ (Hom⇘C⇙[dom⇘C⇙ g,f]) = (Hom⇘C⇙[cod⇘C⇙ g,f]) ;;⇘SET⇙ (HomC⇘C⇙[g,cod⇘C⇙ f])" using assms morf morg
by (simp add: HomCHom)
hence "((Hom⇘C⇙[─,dom⇘C⇙ f]) ## g) ;;⇘SET⇙ (Hom⇘C⇙[Y,f]) = (Hom⇘C⇙[X,f]) ;;⇘SET⇙ ((Hom⇘C⇙[─,cod⇘C⇙ f]) ## g)"
using H1 H2 D1 C1 by simp
thus ?thesis by (simp add: YFtorNT'_def NTCatCod_def HomFtorContraCod)
qed
}
qed
lemma YFtorNTNatTrans:
assumes "LSCategory C" and "f ∈ Mor C"
shows "NatTrans (YFtorNT C f)"
by (simp add: assms YFtorNTNatTrans' YFtorNT_def MakeNT)
lemma YFtorNTMor:
assumes "LSCategory C" and "f ∈ Mor C"
shows "YFtorNT C f ∈ Mor (CatExp (Op C) SET)"
proof(auto simp add: CatExp_def CatExp'_def MakeCatMor)
have "f ∈ Mor C" using assms by auto
thus "NatTrans (YFtorNT C f)" using assms by (simp add: YFtorNTNatTrans)
show "NTCatDom (YFtorNT C f) = Op C" by (simp add: YFtorNTCatDom)
show "NTCatCod (YFtorNT C f) = SET" by (simp add: YFtorNTCatCod)
qed
lemma YFtorNtMapsTo:
assumes "LSCategory C" and "f ∈ Mor C"
shows "YFtorNT C f maps⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[─,dom⇘C⇙ f]) to (Hom⇘C⇙[─,cod⇘C⇙ f])"
proof(rule MapsToI)
have "f ∈ Mor C" using assms by auto
thus 1: "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙" using assms by (simp add: YFtorNTMor)
show "dom⇘CatExp (Op C) SET⇙ YFtorNT C f = Hom⇘C⇙[─,dom⇘C⇙ f]" using 1 by(simp add:CatExpDom YFtorNT_defs)
show "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = Hom⇘C⇙[─,cod⇘C⇙ f]" using 1 by(simp add:CatExpCod YFtorNT_defs)
qed
lemma YFtorNTCompDef:
assumes "LSCategory C" and "f ≈>⇘C⇙ g"
shows "YFtorNT C f ≈>⇘CatExp (Op C) SET⇙ YFtorNT C g"
proof(rule CompDefinedI)
have "f ∈ Mor C" and "g ∈ Mor C" using assms by auto
hence 1: "YFtorNT C f maps⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[─,dom⇘C⇙ f]) to (Hom⇘C⇙[─,cod⇘C⇙ f])"
and 2: "YFtorNT C g maps⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[─,dom⇘C⇙ g]) to (Hom⇘C⇙[─,cod⇘C⇙ g])"
using assms by (simp add: YFtorNtMapsTo)+
thus "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙"
and "YFtorNT C g ∈ mor⇘CatExp (Op C) SET⇙" by auto
have "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = (Hom⇘C⇙[─,cod⇘C⇙ f])" using 1 by auto
moreover have "dom⇘CatExp (Op C) SET⇙ YFtorNT C g = (Hom⇘C⇙[─,dom⇘C⇙ g])" using 2 by auto
moreover have "cod⇘C⇙ f = dom⇘C⇙ g" using assms by auto
ultimately show "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = dom⇘CatExp (Op C) SET⇙ YFtorNT C g" by simp
qed
lemma PreSheafCat: "LSCategory C ⟹ Category (CatExp (Op C) SET)"
by(simp add: YFtor'_def OpCatCat SETCategory CatExpCat)
lemma YFtor'Obj1:
assumes "X ∈ Obj (CatDom (YFtor' C))" and "LSCategory C"
shows "(YFtor' C) ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) (Hom⇘C ⇙[─,X])"
proof(simp add: YFtor'_def, rule NatTransExt)
have Obj: "X ∈ Obj C" using assms by (simp add: YFtor'_def)
have HomObj: "(Hom⇘C⇙[─,X]) ∈ Obj (CatExp (Op C) SET)" using assms Obj by(simp add: CatExp_defs HomFtorContraFtor)
hence Id: "Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]) ∈ Mor (CatExp (Op C) SET)" using assms
by (simp add: PreSheafCat Category.CatIdInMor)
have CAT: "Category(CatExp (Op C) SET)" using assms by (simp add: PreSheafCat)
have HomObj: "(Hom⇘C⇙[─,X]) ∈ Obj (CatExp (Op C) SET)" using assms Obj
by(simp add: CatExp_defs HomFtorContraFtor)
show "NatTrans (YFtorNT C (Id C X))"
proof(rule YFtorNTNatTrans)
show "LSCategory C" using assms(2) .
show "Id C X ∈ Mor C" using assms Obj by (simp add: Category.CatIdInMor)
qed
show "NatTrans(Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" using Id by (simp add: CatExp_defs)
show "NTDom (YFtorNT C (Id C X)) = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))"
proof(simp add: YFtorNT_defs)
have "Hom⇘C⇙[─,dom⇘C⇙ (Id C X)] = Hom⇘C⇙[─,X]" using assms Obj by (simp add: Category.CatIdDomCod)
also have "... = dom⇘CatExp (Op C) SET⇙ (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" using CAT HomObj
by (simp add: Category.CatIdDomCod)
also have "... = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" using Id by (simp add: CatExpDom)
finally show "Hom⇘C⇙[─,dom⇘C⇙ (Id C X)] = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" .
qed
show "NTCod (YFtorNT C (Id C X)) = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))"
proof(simp add: YFtorNT_defs)
have "Hom⇘C⇙[─,cod⇘C⇙ (Id C X)] = Hom⇘C⇙[─,X]" using assms Obj by (simp add: Category.CatIdDomCod)
also have "... = cod⇘CatExp (Op C) SET⇙ (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" using CAT HomObj
by (simp add: Category.CatIdDomCod)
also have "... = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" using Id by (simp add: CatExpCod)
finally show "Hom⇘C⇙[─,cod⇘C⇙ (Id C X)] = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X]))" .
qed
{
fix Y assume a: "Y ∈ Obj (NTCatDom (YFtorNT C (Id C X)))"
show "(YFtorNT C (Id C X)) $$ Y = (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X])) $$ Y"
proof-
have CD: "CatDom (Hom⇘C⇙[─,X]) = Op C" by (simp add: HomFtorContraDom)
have CC: "CatCod (Hom⇘C⇙[─,X]) = SET" by (simp add: HomFtorContraCod)
have ObjY: "Y ∈ Obj C" and ObjYOp: "Y ∈ Obj (Op C)" using a by(simp add: YFtorNTCatDom OppositeCategory_def)+
have "(YFtorNT C (Id C X)) $$ Y = (Hom⇘C⇙[Y,(Id C X)])" using a by (simp add: YFtorNTApp1)
also have "... = id⇘SET⇙ (Hom⇘C ⇙Y X)" using Obj ObjY assms by (simp add: HomFtorId)
also have "... = id⇘SET⇙ ((Hom⇘C⇙[─,X]) @@ Y)" using Obj ObjY assms by (simp add: HomFtorOpObj )
also have "... = (IdNatTrans (Hom⇘C⇙[─,X])) $$ Y" using CD CC ObjYOp by (simp add: IdNatTrans_map)
also have "... = (Id (CatExp (Op C) SET) (Hom⇘C⇙[─,X])) $$ Y" using HomObj by (simp add: CatExpId)
finally show ?thesis .
qed
}
qed
lemma YFtorPreFtor:
assumes "LSCategory C"
shows "PreFunctor (YFtor' C)"
proof(auto simp only: PreFunctor_def)
have CAT: "Category(CatExp (Op C) SET)" using assms by (simp add: PreSheafCat)
{
fix f g assume a: "f ≈>⇘CatDom (YFtor' C)⇙ g"
show "(YFtor' C) ## (f ;;⇘CatDom (YFtor' C)⇙ g) = ((YFtor' C) ## f) ;;⇘CatCod (YFtor' C)⇙ ((YFtor' C) ## g)"
proof(simp add: YFtor'_def, rule NatTransExt)
have CD: "f ≈>⇘C⇙ g" using a by (simp add: YFtor'_def)
have CD2: "YFtorNT C f ≈>⇘CatExp (Op C) SET⇙ YFtorNT C g" using CD assms by (simp add: YFtorNTCompDef)
have Mor1: "YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g ∈ Mor (CatExp (Op C) SET)" using CAT CD2
by (simp add: Category.MapsToMorDomCod)
show "NatTrans (YFtorNT C (f ;;⇘C⇙ g))" using assms by (simp add: Category.MapsToMorDomCod CD YFtorNTNatTrans)
show "NatTrans (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)" using Mor1 by (simp add: CatExpMorNT)
show "NTDom (YFtorNT C (f ;;⇘C⇙ g)) = NTDom (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)"
proof-
have 1: "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙" using CD2 by auto
have "NTDom (YFtorNT C (f ;;⇘C⇙ g)) = Hom⇘C⇙[─,dom⇘C⇙ (f ;;⇘C⇙ g)]" by (simp add: YFtorNT_defs)
also have "... = Hom⇘C⇙[─,dom⇘C⇙ f]" using CD assms by (simp add: Category.MapsToMorDomCod)
also have "... = NTDom (YFtorNT C f)" by (simp add: YFtorNT_defs)
also have "... = dom⇘CatExp (Op C) SET⇙ (YFtorNT C f)" using 1 by (simp add: CatExpDom)
also have "... = dom⇘CatExp (Op C) SET⇙ (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)" using CD2 CAT
by (simp add: Category.MapsToMorDomCod)
finally show ?thesis using Mor1 by (simp add: CatExpDom)
qed
show "NTCod (YFtorNT C (f ;;⇘C⇙ g)) = NTCod (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)"
proof-
have 1: "YFtorNT C g ∈ mor⇘CatExp (Op C) SET⇙" using CD2 by auto
have "NTCod (YFtorNT C (f ;;⇘C⇙ g)) = Hom⇘C⇙[─,cod⇘C⇙ (f ;;⇘C⇙ g)]" by (simp add: YFtorNT_defs)
also have "... = Hom⇘C⇙[─,cod⇘C⇙ g]" using CD assms by (simp add: Category.MapsToMorDomCod)
also have "... = NTCod (YFtorNT C g)" by (simp add: YFtorNT_defs)
also have "... = cod⇘CatExp (Op C) SET⇙ (YFtorNT C g)" using 1 by (simp add: CatExpCod)
also have "... = cod⇘CatExp (Op C) SET⇙ (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)" using CD2 CAT
by (simp add: Category.MapsToMorDomCod)
finally show ?thesis using Mor1 by (simp add: CatExpCod)
qed
{
fix X assume a: "X ∈ Obj (NTCatDom (YFtorNT C (f ;;⇘C⇙ g)))"
show "YFtorNT C (f ;;⇘C⇙ g) $$ X = (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g) $$ X"
proof-
have Obj: "X ∈ Obj C" and ObjOp: "X ∈ Obj (Op C)" using a by (simp add: YFtorNTCatDom OppositeCategory_def)+
have App1: "(Hom⇘C⇙[X,f]) = (YFtorNT C f) $$ X"
and App2: "(Hom⇘C⇙[X,g]) = (YFtorNT C g) $$ X" using a by (simp add: YFtorNTApp1 YFtorNTCatDom)+
have "(YFtorNT C (f ;;⇘C⇙ g)) $$ X = (Hom⇘C⇙[X,(f ;;⇘C⇙ g)])" using a by (simp add: YFtorNTApp1)
also have "... = (Hom⇘C⇙[X,f]) ;;⇘SET⇙ (Hom⇘C⇙[X,g])" using CD assms Obj by (simp add: HomFtorDist)
also have "... = ((YFtorNT C f) $$ X) ;;⇘SET⇙ ((YFtorNT C g) $$ X)" using App1 App2 by simp
finally show ?thesis using ObjOp CD2 by (simp add: CatExpDist)
qed
}
qed
}
{
fix X assume a: "X ∈ Obj (CatDom (YFtor' C))"
show "∃ Y ∈ Obj (CatCod (YFtor' C)) . YFtor' C ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) Y"
proof(rule_tac x="Hom⇘C ⇙[─,X]" in Set.rev_bexI)
have "X ∈ Obj C" using a by(simp add: YFtor'_def)
thus "Hom⇘C ⇙[─,X] ∈ Obj (CatCod (YFtor' C))" using assms by(simp add: YFtor'_def CatExp_defs HomFtorContraFtor)
show "(YFtor' C) ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) (Hom⇘C ⇙[─,X])" using a assms
by (simp add: YFtor'Obj1)
qed
}
show "Category (CatDom (YFtor' C))" using assms by (simp add: YFtor'_def)
show "Category (CatCod (YFtor' C))" using CAT by (simp add: YFtor'_def)
qed
lemma YFtor'Obj:
assumes "X ∈ Obj (CatDom (YFtor' C))"
and "LSCategory C"
shows "(YFtor' C) @@ X = Hom⇘C ⇙[─,X]"
proof(rule PreFunctor.FmToFo, simp_all add: assms YFtor'Obj1 YFtorPreFtor)
have "X ∈ Obj C" using assms by(simp add: YFtor'_def)
thus "Hom⇘C ⇙[─,X] ∈ Obj (CatCod (YFtor' C))" using assms by(simp add: YFtor'_def CatExp_defs HomFtorContraFtor)
qed
lemma YFtorFtor':
assumes "LSCategory C"
shows "FunctorM (YFtor' C)"
proof(auto simp only: FunctorM_def)
show "PreFunctor (YFtor' C)" using assms by (rule YFtorPreFtor)
show "FunctorM_axioms (YFtor' C)"
proof(auto simp add:FunctorM_axioms_def)
{
fix f X Y assume aa: "f maps⇘CatDom (YFtor' C) ⇙X to Y"
show "YFtor' C ## f maps⇘CatCod (YFtor' C)⇙ YFtor' C @@ X to YFtor' C @@ Y"
proof-
have Mor1: "f maps⇘C⇙ X to Y" using aa by (simp add: YFtor'_def)
have "Category (CatDom (YFtor' C))" using assms by (simp add: YFtor'_def)
hence Obj1: "X ∈ Obj (CatDom (YFtor' C))" and
Obj2: "Y ∈ Obj (CatDom (YFtor' C))" using aa assms by (simp add: Category.MapsToObj)+
have "(YFtor' C ## f) = YFtorNT C f" by (simp add: YFtor'_def)
moreover have "YFtor' C @@ X = Hom⇘C ⇙[─,X]"
and "YFtor' C @@ Y = Hom⇘C ⇙[─,Y]" using Obj1 Obj2 assms by (simp add: YFtor'Obj)+
moreover have "CatCod (YFtor' C) = CatExp (Op C) SET" by (simp add: YFtor'_def)
moreover have "YFtorNT C f maps⇘CatExp (Op C) SET⇙ (Hom⇘C ⇙[─,X]) to (Hom⇘C ⇙[─,Y])"
using assms Mor1 by (auto simp add: YFtorNtMapsTo)
ultimately show ?thesis by simp
qed
}
qed
qed
lemma YFtorFtor: assumes "LSCategory C" shows "Ftor (YFtor C) : C ⟶ (CatExp (Op C) SET)"
proof(auto simp only: functor_abbrev_def)
show "Functor (YFtor C)" using assms by(simp add: MakeFtor YFtor_def YFtorFtor')
show "CatDom (YFtor C) = C" and "CatCod (YFtor C) = (CatExp (Op C) SET)"
using assms by(simp add: MakeFtor_def YFtor_def YFtor'_def)+
qed
lemma YFtorObj:
assumes "LSCategory C" and "X ∈ Obj C"
shows "(YFtor C) @@ X = Hom⇘C ⇙[─,X]"
proof-
have "CatDom (YFtor' C) = C" by (simp add: YFtor'_def)
moreover hence "(YFtor' C) @@ X = Hom⇘C ⇙[─,X]" using assms by(simp add: YFtor'Obj)
moreover have "PreFunctor (YFtor' C)" using assms by (simp add: YFtorPreFtor)
ultimately show ?thesis using assms by (simp add: MakeFtorObj YFtor_def)
qed
lemma YFtorObj2:
assumes "LSCategory C" and "X ∈ Obj C" and "Y ∈ Obj C"
shows "((YFtor C) @@ Y) @@ X = Hom⇘C ⇙X Y"
proof-
have "Hom⇘C ⇙X Y = ((Hom⇘C⇙[─,Y]) @@ X)" using assms by (simp add: HomFtorOpObj)
also have "... = ((YFtor C @@ Y) @@ X)" using assms by (simp add: YFtorObj)
finally show ?thesis by simp
qed
lemma YFtorMor: "⟦LSCategory C ; f ∈ Mor C⟧ ⟹ (YFtor C) ## f = YFtorNT C f"
by (simp add: YFtor_defs MakeFtorMor)
definition "YMap C X η ≡ (η $$ X) |@| (m2z⇘C⇙ (id⇘C ⇙X))"
definition "YMapInv' C X F x ≡ ⦇
NTDom = ((YFtor C) @@ X),
NTCod = F,
NatTransMap = λ B . ZFfun (Hom⇘C⇙ B X) (F @@ B) (λ f . (F ## (z2m⇘C⇙ f)) |@| x)
⦈"
definition "YMapInv C X F x ≡ MakeNT (YMapInv' C X F x)"
lemma YMapInvApp:
assumes "X ∈ Obj C" and "B ∈ Obj C" and "LSCategory C"
shows "(YMapInv C X F x) $$ B = ZFfun (Hom⇘C⇙ B X) (F @@ B) (λ f . (F ## (z2m⇘C⇙ f)) |@| x)"
proof-
have "NTCatDom (MakeNT (YMapInv' C X F x)) = CatDom (NTDom (YMapInv' C X F x))" by (simp add: MakeNT_def NTCatDom_def)
also have "... = CatDom (Hom⇘C⇙[─,X])" using assms by (simp add: YFtorObj YMapInv'_def)
also have "... = Op C" using assms HomFtorContraFtor[of C X] by auto
finally have "NTCatDom (MakeNT (YMapInv' C X F x)) = Op C" .
hence 1: "B ∈ Obj (NTCatDom (MakeNT (YMapInv' C X F x)))" using assms by (simp add: OppositeCategory_def)
have "(YMapInv C X F x) $$ B = (MakeNT (YMapInv' C X F x)) $$ B" by (simp add: YMapInv_def)
also have "... = (YMapInv' C X F x) $$ B" using 1 by(simp add: MakeNTApp)
finally show ?thesis by (simp add: YMapInv'_def)
qed
lemma YMapImage:
assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
and "NT η : (YFtor C @@ X) ⟹ F"
shows "(YMap C X η) |∈| (F @@ X)"
proof(simp only: YMap_def)
have "(YFtor C @@ X) = (Hom⇘C⇙[─,X])" using assms by (auto simp add: YFtorObj)
moreover have "Ftor (Hom⇘C⇙[─,X]) : (Op C) ⟶ SET" using assms by (simp add: HomFtorContraFtor)
ultimately have "CatDom (YFtor C @@ X) = Op C" by auto
hence Obj: "X ∈ Obj (CatDom (YFtor C @@ X))" using assms by (simp add: OppositeCategory_def)
moreover have "CatCod F = SET" using assms by auto
moreover have "η $$ X maps⇘CatCod F ⇙((YFtor C @@ X) @@ X) to (F @@ X)" using assms Obj by (simp add: NatTransMapsTo)
ultimately have "η $$ X maps⇘SET⇙ ((YFtor C @@ X) @@ X) to (F @@ X)" by simp
moreover have "(m2z⇘C ⇙(Id C X)) |∈| ((YFtor C @@ X) @@ X)"
proof-
have "(Id C X) maps⇘C ⇙X to X" using assms by (simp add: Category.Simps)
moreover have "((YFtor C @@ X) @@ X) = Hom⇘C⇙ X X" using assms by (simp add: YFtorObj2)
ultimately show ?thesis using assms by (simp add: LSCategory.m2zz2m)
qed
ultimately show "((η $$ X) |@| (m2z⇘C ⇙(Id C X))) |∈| (F @@ X)" by (simp add: SETfunDomAppCod)
qed
lemma YMapInvNatTransP:
assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and xobj: "X ∈ Obj C" and xinF: "x |∈| (F @@ X)"
shows "NatTransP (YMapInv' C X F x)"
proof(auto simp only: NatTransP_def, simp_all add: YMapInv'_def NTCatCod_def NTCatDom_def)
have yf: "(YFtor C @@ X) = Hom⇘C⇙[─,X]" using assms by (simp add: YFtorObj)
hence hf: "Ftor (YFtor C @@ X) : (Op C) ⟶ SET" using assms by (simp add: HomFtorContraFtor)
thus "Functor (YFtor C @@ X)" by auto
show ftf: "Functor F" using assms by auto
have df: "CatDom F = Op C" and cf: "CatCod F = SET" using assms by auto
have dy: "CatDom ((YFtor C) @@ X) = Op C" and cy: "CatCod ((YFtor C) @@ X) = SET" using hf by auto
show "CatDom ((YFtor C) @@ X) = CatDom F" using df dy by simp
show "CatCod F = CatCod ((YFtor C) @@ X)" using cf cy by simp
{
fix Y assume yobja: "Y ∈ Obj (CatDom ((YFtor C) @@ X))"
show "ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## (z2m⇘C ⇙f)) |@| x) maps⇘CatCod F⇙ ((YFtor C @@ X) @@ Y) to (F @@ Y)"
proof(simp add: cf, rule MapsToI)
have yobj: "Y ∈ Obj C" using yobja dy by (simp add: OppositeCategory_def)
have zffun: "isZFfun (ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x))"
proof(rule SETfun, rule allI, rule impI)
{
fix y assume yhom: "y |∈| (Hom⇘C⇙ Y X)" show "(F ## (z2m⇘C ⇙y)) |@| x |∈| (F @@ Y)"
proof-
let ?f = "(F ## (z2m⇘C ⇙y))"
have "(z2m⇘C ⇙y) maps⇘C⇙ Y to X" using yhom yobj assms by (simp add: LSCategory.z2mm2z)
hence "(z2m⇘C ⇙y) maps⇘Op C⇙ X to Y" by (simp add: MapsToOp)
hence "?f maps⇘SET⇙ (F @@ X) to (F @@ Y)" using assms by (simp add: FunctorMapsTo)
hence "isZFfun (?f)" and "|dom| ?f = F @@ X" and "|cod| ?f = F @@ Y" by (simp add: SETmapsTo)+
thus "(?f |@| x) |∈| (F @@ Y)" using assms ZFfunDomAppCod[of ?f x] by simp
qed
}
qed
show "ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) ∈ mor⇘SET⇙" using zffun
by(simp add: SETmor)
show "cod⇘SET⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) = F @@ Y" using zffun
by(simp add: SETcod)
have "(Hom⇘C⇙ Y X) = (YFtor C @@ X) @@ Y" using assms yobj by (simp add: YFtorObj2)
thus "dom⇘SET⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) = (YFtor C @@ X) @@ Y" using zffun
by(simp add: SETdom)
qed
}
{
fix f Z Y assume fmaps: "f maps⇘CatDom ((YFtor C ) @@ X)⇙ Z to Y"
have fmapsa: "f maps⇘Op C⇙ Z to Y" using fmaps dy by simp
hence fmapsb: "f maps⇘C⇙ Y to Z" by (rule MapsToOpOp)
hence fmor: "f ∈ Mor C" and fdom: "dom⇘C⇙ f = Y" and fcod: "cod⇘C⇙ f = Z" by (auto simp add: OppositeCategory_def)
hence hc: "(Hom⇘C⇙[─,X]) ## f = (HomC⇘C⇙[f,X])" using assms by (simp add: HomContraMor)
have yobj: "Y ∈ Obj C" and zobj: "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)+
have Ffmaps: "(F ## f) maps⇘SET⇙ (F @@ Z) to (F @@ Y)" using assms fmapsa by (simp add: FunctorMapsTo)
have Fzmaps: "⋀ h A B . ⟦h |∈| (Hom⇘C⇙ A B) ; A ∈ Obj C ; B ∈ Obj C⟧ ⟹
(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ B) to (F @@ A)"
proof-
fix h A B assume h: "h |∈| (Hom⇘C⇙ A B)" and oA: "A ∈ Obj C" and oB: "B ∈ Obj C"
have "(z2m⇘C ⇙h) maps⇘C⇙ A to B" using assms h oA oB by (simp add: LSCategory.z2mm2z)
hence "(z2m⇘C ⇙h) maps⇘Op C⇙ B to A" by (rule MapsToOp)
thus "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ B) to (F @@ A)" using assms by (simp add: FunctorMapsTo)
qed
have hHomF: "⋀h. h |∈| (Hom⇘C⇙ Z X) ⟹ (F ## (z2m⇘C ⇙h)) |@| x |∈| (F @@ Z)" using xobj zobj xinF
proof-
fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
have "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Z)" using xobj zobj h by (simp add: Fzmaps)
thus "(F ## (z2m⇘C ⇙h)) |@| x |∈| (F @@ Z)" using assms by (simp add: SETfunDomAppCod)
qed
have Ff: "F ## f = ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)" using Ffmaps by (simp add: SETZFfun)
have compdefa: "ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) ≈>⇘SET⇙
ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x)"
proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
show "isZFfun (ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))"
proof(rule SETfun, rule allI, rule impI)
fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
have "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h xobj zobj by (simp add: LSCategory.z2mm2z)
hence "f ;;⇘C⇙ (z2m⇘C ⇙h) maps⇘C⇙ Y to X" using fmapsb assms(1) by (simp add: Category.Ccompt)
thus "(m2z⇘C⇙ (f ;;⇘C⇙ (z2m⇘C ⇙h))) |∈| (Hom⇘C⇙ Y X)" using assms by (simp add: LSCategory.m2zz2m)
qed
moreover show "isZFfun (ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x))"
proof(rule SETfun, rule allI, rule impI)
fix h assume h: "h |∈| (Hom⇘C⇙ Y X)"
have "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Y)" using xobj yobj h by (simp add: Fzmaps)
thus "(F ## (z2m⇘C ⇙h)) |@| x |∈| (F @@ Y)" using assms by (simp add: SETfunDomAppCod)
qed
ultimately show "cod⇘SET⇙(ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h)))) =
dom⇘SET⇙(ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x))" by (simp add: SETcod SETdom)
qed
have compdefb: "ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x) ≈>⇘SET⇙
ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)"
proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
show "isZFfun (ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x))" using hHomF by (simp add: SETfun)
moreover show "isZFfun (ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h))"
proof(rule SETfun, rule allI, rule impI)
fix h assume h: "h |∈| (F @@ Z)"
have "F ## f maps⇘SET⇙ F @@ Z to F @@ Y" using Ffmaps .
thus "(F ## f) |@| h |∈| (F @@ Y)" using h by (simp add: SETfunDomAppCod)
qed
ultimately show "cod⇘SET⇙ (ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x)) =
dom⇘SET⇙ (ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h))" by (simp add: SETcod SETdom)
qed
have "ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) ;;⇘SET⇙
ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x) =
ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) |o|
ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x)" using Ff compdefa by (simp add: SETComp)
also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Y) ((λh. (F ## (z2m⇘C ⇙h)) |@| x) o (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))"
proof(rule ZFfunComp, rule allI, rule impI)
{
fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
show "(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) |∈| (Hom⇘C⇙ Y X)"
proof-
have "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
hence "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h by (simp add: LSCategory.z2mm2z)
hence "f ;;⇘C⇙ (z2m⇘C ⇙h) maps⇘C⇙ Y to X" using fmapsb assms(1) by (simp add: Category.Ccompt)
thus ?thesis using assms by (simp add: LSCategory.m2zz2m)
qed
}
qed
also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Y) ((λh. (F ## f) |@| h) o (λh. (F ## (z2m⇘C ⇙h)) |@| x))"
proof(rule ZFfun_ext, rule allI, rule impI, simp)
{
fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
have zObj: "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
hence hmaps: "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h by (simp add: LSCategory.z2mm2z)
hence "(z2m⇘C ⇙h) ∈ Mor C" and "dom⇘C⇙ (z2m⇘C ⇙h) = cod⇘C⇙ f" using fcod by auto
hence CompDef_hf: "f ≈>⇘C⇙ (z2m⇘C ⇙h)" using fmor by auto
hence CompDef_hfOp: "(z2m⇘C ⇙h) ≈>⇘Op C⇙ f" by (simp add: CompDefOp)
hence CompDef_FhfOp: "(F ## (z2m⇘C ⇙h)) ≈>⇘SET⇙ (F ## f)" using assms by (simp add: FunctorCompDef)
hence "(z2m⇘C ⇙h) maps⇘Op C⇙ X to Z" using hmaps by (simp add: MapsToOp)
hence "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Z)" using assms by (simp add: FunctorMapsTo)
hence xin: "x |∈| |dom|(F ## (z2m⇘C ⇙h))" using assms by (simp add: SETmapsTo)
have "(f ;;⇘C⇙ (z2m⇘C ⇙h)) ∈ Mor C" using CompDef_hf assms by(simp add: Category.MapsToMorDomCod)
hence "(F ## (z2m⇘C ⇙(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))) |@| x = (F ## (f ;;⇘C⇙ (z2m⇘C ⇙h))) |@| x"
using assms by (simp add: LSCategory.m2zz2mInv)
also have "... = (F ## ((z2m⇘C ⇙h) ;;⇘Op C⇙ f)) |@| x" by (simp add: OppositeCategory_def)
also have "... = ((F ## (z2m⇘C ⇙h)) ;;⇘SET ⇙(F ## f)) |@| x" using assms CompDef_hfOp by (simp add: FunctorComp)
also have "... = (F ## f) |@| ((F ## (z2m⇘C ⇙h)) |@| x)" using CompDef_FhfOp xin by(rule SETCompAt)
finally show "(F ## (z2m⇘C ⇙(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))) |@| x = (F ## f) |@| ((F ## (z2m⇘C ⇙h)) |@| x)" .
}
qed
also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x) |o|
ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)"
by(rule ZFfunComp[THEN sym], rule allI, rule impI, simp add: hHomF)
also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x) ;;⇘SET⇙ (F ## f)"
using Ff compdefb by (simp add: SETComp)
finally show "(((YFtor C) @@ X) ## f) ;;⇘CatCod F⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## (z2m⇘C ⇙f)) |@| x) =
ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λf. (F ## (z2m⇘C ⇙f)) |@| x) ;;⇘CatCod F⇙ (F ## f)"
by(simp add: cf yf hc fdom fcod HomFtorMapContra_def)
}
qed
lemma YMapInvNatTrans:
assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C" and "x |∈| (F @@ X)"
shows "NatTrans (YMapInv C X F x)"
by (simp add: assms YMapInv_def MakeNT YMapInvNatTransP)
lemma YMapInvImage:
assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
and "x |∈| (F @@ X)"
shows "NT (YMapInv C X F x) : (YFtor C @@ X) ⟹ F"
proof(auto simp only: nt_abbrev_def)
show "NatTrans (YMapInv C X F x)" using assms by (simp add: YMapInvNatTrans)
show "NTDom (YMapInv C X F x) = YFtor C @@ X" by(simp add: YMapInv_def MakeNT_def YMapInv'_def)
show "NTCod (YMapInv C X F x) = F" by(simp add: YMapInv_def MakeNT_def YMapInv'_def)
qed
lemma YMap1:
assumes LSCat: "LSCategory C" and Fftor: "Ftor F : (Op C) ⟶ SET" and XObj: "X ∈ Obj C"
and NT: "NT η : (YFtor C @@ X) ⟹ F"
shows "YMapInv C X F (YMap C X η) = η"
proof(rule NatTransExt)
have "(YMap C X η) |∈| (F @@ X)" using assms by (simp add: YMapImage)
hence 1: "NT (YMapInv C X F (YMap C X η)) : (YFtor C @@ X) ⟹ F" using assms by (simp add: YMapInvImage)
thus "NatTrans (YMapInv C X F (YMap C X η))" by auto
show "NatTrans η" using assms by auto
have NTDYI: "NTDom (YMapInv C X F (YMap C X η)) = (YFtor C @@ X)" using 1 by auto
moreover have NTDeta: "NTDom η = (YFtor C @@ X)" using assms by auto
ultimately show "NTDom (YMapInv C X F (YMap C X η)) = NTDom η" by simp
have "NTCod (YMapInv C X F (YMap C X η)) = F" using 1 by auto
moreover have NTCeta: "NTCod η = F" using assms by auto
ultimately show "NTCod (YMapInv C X F (YMap C X η)) = NTCod η" by simp
{
fix Y assume Yobja: "Y ∈ Obj (NTCatDom (YMapInv C X F (YMap C X η)))"
have CCF: "CatCod F = SET" using assms by auto
have "Ftor (Hom⇘C⇙[─,X]) : (Op C) ⟶ SET" using LSCat XObj by (simp add: HomFtorContraFtor)
hence CDH: "CatDom (Hom⇘C⇙[─,X]) = Op C" by auto
hence CDYF: "CatDom (YFtor C @@ X) = Op C" using XObj LSCat by (auto simp add: YFtorObj)
hence "NTCatDom (YMapInv C X F (YMap C X η)) = Op C" using LSCat XObj NTDYI CDH by (simp add: NTCatDom_def)
hence YObjOp: "Y ∈ Obj (Op C)" using Yobja by simp
hence YObj: "Y ∈ Obj C" and XObjOp: "X ∈ Obj (Op C)" using XObj by (simp add: OppositeCategory_def)+
have yinv_mapsTo: "((YMapInv C X F (YMap C X η)) $$ Y) maps⇘SET⇙ (Hom⇘C ⇙Y X) to (F @@ Y)"
proof-
have "((YMapInv C X F (YMap C X η)) $$ Y) maps⇘SET⇙ ((YFtor C @@ X) @@ Y) to (F @@ Y)"
using 1 CCF CDYF YObjOp NatTransMapsTo[of "(YMapInv C X F (YMap C X η))" "(YFtor C @@ X)" F Y] by simp
thus ?thesis using LSCat XObj YObj by (simp add: YFtorObj2)
qed
have eta_mapsTo: "(η $$ Y) maps⇘SET⇙ (Hom⇘C ⇙Y X) to (F @@ Y)"
proof-
have "(η $$ Y) maps⇘SET⇙ ((YFtor C @@ X) @@ Y) to (F @@ Y)"
using NT CDYF CCF YObjOp NatTransMapsTo[of η "(YFtor C @@ X)" F Y] by simp
thus ?thesis using LSCat XObj YObj by (simp add: YFtorObj2)
qed
show "(YMapInv C X F (YMap C X η)) $$ Y = η $$ Y"
proof(rule ZFfunExt)
show "|dom|(YMapInv C X F (YMap C X η) $$ Y) = |dom|(η $$ Y)"
using yinv_mapsTo eta_mapsTo by (simp add: SETmapsTo)
show "|cod|(YMapInv C X F (YMap C X η) $$ Y) = |cod|(η $$ Y)"
using yinv_mapsTo eta_mapsTo by (simp add: SETmapsTo)
show "isZFfun (YMapInv C X F (YMap C X η) $$ Y)"
using yinv_mapsTo by (simp add: SETmapsTo)
show "isZFfun (η $$ Y)"
using eta_mapsTo by (simp add: SETmapsTo)
{
fix f assume fdomYinv: "f |∈| |dom|(YMapInv C X F (YMap C X η) $$ Y)"
have fHom: "f |∈| (Hom⇘C⇙ Y X)" using yinv_mapsTo fdomYinv by (simp add: SETmapsTo)
hence fMapsTo: "(z2m⇘C ⇙f) maps⇘C ⇙Y to X" using assms YObj by (simp add: LSCategory.z2mm2z)
hence fCod: "(cod⇘C⇙ (z2m⇘C ⇙f)) = X" and fDom: "(dom⇘C⇙ (z2m⇘C ⇙f)) = Y" and fMor: "(z2m⇘C ⇙f) ∈ Mor C" by auto
have "(YMapInv C X F (YMap C X η) $$ Y) |@| f =
(F ## (z2m⇘C ⇙f)) |@| ((η $$ X) |@| (m2z⇘C ⇙(Id C X)))"
using fHom assms YObj by (simp add: ZFfunApp YMapInvApp YMap_def)
also have "... = ((η $$ X) ;;⇘SET⇙ (F ## (z2m⇘C ⇙f))) |@| (m2z⇘C ⇙(Id C X))"
proof-
have aa: "(η $$ X) maps⇘SET⇙ ((YFtor C @@ X) @@ X) to (F @@ X)"
using NT CDYF CCF YObjOp XObjOp NatTransMapsTo[of η "(YFtor C @@ X)" F X] by simp
have bb: "(F ## (z2m⇘C ⇙f)) maps⇘SET⇙ (F @@ X) to (F @@ Y)"
using fMapsTo Fftor by (simp add: MapsToOp FunctorMapsTo)
have "(η $$ X) ≈>⇘SET⇙ (F ## (z2m⇘C ⇙f))" using aa bb by (simp add: MapsToCompDef)
moreover have "(m2z⇘C ⇙(Id C X)) |∈| |dom| (η $$ X)" using assms aa
by (simp add: SETmapsTo YFtorObj2 Category.Cidm LSCategory.m2zz2m)
ultimately show ?thesis by (simp add: SETCompAt)
qed
also have "... = ((HomC⇘C⇙[z2m⇘C ⇙f,X]) ;;⇘SET⇙ (η $$ Y)) |@| (m2z⇘C ⇙(Id C X))"
proof-
have "NTDom η = (Hom⇘C⇙[─,X])" using NTDeta assms by (simp add: YFtorObj)
moreover hence "NTCatDom η = Op C" by (simp add: NTCatDom_def HomFtorContraDom)
moreover have "NTCatCod η = SET" using assms by (auto simp add: NTCatCod_def)
moreover have "NatTrans η" and "NTCod η = F" using assms by auto
moreover have "(z2m⇘C ⇙f) maps⇘Op C ⇙X to Y"
using fMapsTo MapsToOp[where ?f = "(z2m⇘C ⇙f)" and ?X = Y and ?Y = X and ?C = C] by simp
ultimately have "(η $$ X) ;;⇘SET⇙ (F ## (z2m⇘C ⇙f)) = ((Hom⇘C⇙[─,X]) ## (z2m⇘C ⇙f)) ;;⇘SET⇙ (η $$ Y)"
using NatTransP.NatTrans[of η "(z2m⇘C ⇙f)" X Y] by simp
moreover have "((Hom⇘C⇙[─,X]) ## (z2m⇘C ⇙f)) = (HomC⇘C⇙[(z2m⇘C ⇙f),X])" using assms fMor by (simp add: HomContraMor)
ultimately show ?thesis by simp
qed
also have "... = (η $$ Y) |@| ((HomC⇘C⇙[z2m⇘C ⇙f,X]) |@| (m2z⇘C ⇙(Id C X)))"
proof-
have "(HomC⇘C⇙[z2m⇘C ⇙f,X]) ≈>⇘SET⇙ (η $$ Y)"
using fCod fDom XObj LSCat fMor HomFtorContraMapsTo[of C X "z2m⇘C ⇙f"] eta_mapsTo by (simp add: MapsToCompDef)
moreover have "|dom| (HomC⇘C⇙[z2m⇘C ⇙f,X]) = (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)"
by (simp add: ZFfunDom HomFtorMapContra_def)
moreover have "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)"
using assms fCod by (simp add: Category.Cidm LSCategory.m2zz2m)
ultimately show ?thesis by (simp add: SETCompAt)
qed
also have "... = (η $$ Y) |@| (m2z⇘C⇙ ((z2m⇘C ⇙f) ;;⇘C⇙ (z2m⇘C⇙ (m2z⇘C ⇙(Id C X)))))"
proof-
have "(Id C X) maps⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) to X" using assms fCod by (simp add: Category.Cidm)
hence "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)" using assms by (simp add: LSCategory.m2zz2m)
thus ?thesis by (simp add: HomContraAt)
qed
also have "... = (η $$ Y) |@| (m2z⇘C⇙ ((z2m⇘C ⇙f) ;;⇘C⇙ (Id C X)))"
using assms by (simp add: LSCategory.m2zz2mInv Category.CatIdInMor)
also have "... = (η $$ Y) |@| (m2z⇘C⇙ (z2m⇘C ⇙f))" using assms(1) fCod fMor Category.Cidr[of C "(z2m⇘C ⇙f)"] by (simp)
also have "... = (η $$ Y) |@| f" using assms YObj fHom by (simp add: LSCategory.z2mm2z)
finally show "(YMapInv C X F (YMap C X η) $$ Y) |@| f = (η $$ Y) |@| f" .
}
qed
}
qed
lemma YMap2:
assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
and "x |∈| (F @@ X)"
shows "YMap C X (YMapInv C X F x) = x"
proof(simp only: YMap_def)
let ?η = "(YMapInv C X F x)"
have "(?η $$ X) = ZFfun (Hom⇘C⇙ X X) (F @@ X) (λ f . (F ## (z2m⇘C⇙ f)) |@| x)" using assms by (simp add: YMapInvApp)
moreover have "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ X X)" using assms by (simp add: Category.Simps LSCategory.m2zz2m)
ultimately have "(?η $$ X) |@| (m2z⇘C ⇙(Id C X)) = (F ## (z2m⇘C⇙ (m2z⇘C ⇙(Id C X)))) |@| x"
by (simp add: ZFfunApp)
also have "... = (F ## (Id C X)) |@| x" using assms by (simp add: Category.CatIdInMor LSCategory.m2zz2mInv)
also have "... = (Id SET (F @@ X)) |@| x"
proof-
have "X ∈ Obj (Op C)" using assms by (auto simp add: OppositeCategory_def)
hence "(F ## (Id (Op C) X)) = (Id SET (F @@ X))"
using assms by(simp add: FunctorId)
moreover have "(Id (Op C) X) = (Id C X)" using assms by (auto simp add: OppositeCategory_def)
ultimately show ?thesis by simp
qed
also have "... = x" using assms by (simp add: SETId)
finally show "(?η $$ X) |@| (m2z⇘C ⇙(Id C X)) = x" .
qed
lemma YFtorNT_YMapInv:
assumes "LSCategory C" and "f maps⇘C⇙ X to Y"
shows "YFtorNT C f = YMapInv C X (Hom⇘C⇙[─,Y]) (m2z⇘C⇙ f)"
proof(simp only: YFtorNT_def YMapInv_def, rule NatTransExt')
have Cf: "cod⇘C⇙ f = Y" and Df: "dom⇘C⇙ f = X" using assms by auto
thus "NTCod (YFtorNT' C f) = NTCod (YMapInv' C X (Hom⇘C⇙[─,Y]) (m2z⇘C⇙f))"
by(simp add: YFtorNT'_def YMapInv'_def )
have "Hom⇘C⇙[─,dom⇘C⇙ f] = YFtor C @@ X" using Df assms by (simp add: YFtorObj Category.MapsToObj)
thus "NTDom (YFtorNT' C f) = NTDom (YMapInv' C X (Hom⇘C⇙[─,Y]) (m2z⇘C⇙f))"
by(simp add: YFtorNT'_def YMapInv'_def )
{
fix Z assume ObjZ1: "Z ∈ Obj (NTCatDom (YFtorNT' C f))"
have ObjZ2: "Z ∈ Obj C" using ObjZ1 by (simp add: YFtorNT'_def NTCatDom_def OppositeCategory_def HomFtorContraDom)
moreover have ObjX: "X ∈ Obj C" and ObjY: "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)+
moreover
{
fix x assume x: "x |∈| (Hom⇘C⇙ Z X)"
have "m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f) = ((Hom⇘C⇙[─,Y]) ## (z2m⇘C ⇙x)) |@| (m2z⇘C⇙f)"
proof-
have morf: "f ∈ Mor C" using assms by auto
have mapsx: "(z2m⇘C ⇙x) maps⇘C⇙ Z to X" using x assms(1) ObjZ2 ObjX by (simp add: LSCategory.z2mm2z)
hence morx: "(z2m⇘C ⇙x) ∈ Mor C" by auto
hence "(Hom⇘C⇙[─,Y]) ## (z2m⇘C ⇙x) = (HomC⇘C⇙[(z2m⇘C ⇙x),Y])" using assms by (simp add: HomContraMor)
moreover have "(HomC⇘C⇙[(z2m⇘C ⇙x),Y]) |@| (m2z⇘C ⇙f) = m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ (z2m⇘C ⇙(m2z⇘C ⇙f)))"
proof (rule HomContraAt)
have "cod⇘C⇙ (z2m⇘C ⇙x) = X" using mapsx by auto
thus "(m2z⇘C ⇙f) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙x)) Y)" using assms by (simp add: LSCategory.m2zz2m)
qed
moreover have "(z2m⇘C ⇙(m2z⇘C ⇙f)) = f" using assms morf by (simp add: LSCategory.m2zz2mInv)
ultimately show ?thesis by simp
qed
}
ultimately show "(YFtorNT' C f) $$ Z = (YMapInv' C X (Hom⇘C⇙[─,Y]) (m2z⇘C⇙f)) $$ Z" using Cf Df assms
apply(simp add: YFtorNT'_def YMapInv'_def HomFtorMap_def HomFtorOpObj)
apply(rule ZFfun_ext, rule allI, rule impI, simp)
done
}
qed
lemma YMapYoneda:
assumes "LSCategory C" and "f maps⇘C⇙ X to Y"
shows "YFtor C ## f = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ f)"
proof-
have "f ∈ Mor C" using assms by auto
moreover have "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)
moreover have "YFtorNT C f = YMapInv C X (Hom⇘C⇙[─,Y]) (m2z⇘C⇙ f)" using assms by (simp add: YFtorNT_YMapInv)
ultimately show ?thesis using assms by (simp add: YFtorMor YFtorObj)
qed
lemma YonedaFull:
assumes "LSCategory C" and "X ∈ Obj C" and "Y ∈ Obj C"
and "NT η : (YFtor C @@ X) ⟹ (YFtor C @@ Y)"
shows "YFtor C ## (z2m⇘C⇙ (YMap C X η)) = η"
and "z2m⇘C⇙ (YMap C X η) maps⇘C⇙ X to Y"
proof-
have ftor: "Ftor (YFtor C @@ Y) : (Op C) ⟶ SET" using assms by (simp add: YFtorObj HomFtorContraFtor)
hence "(YMap C X η) |∈| ((YFtor C @@ Y) @@ X)" using assms by (simp add: YMapImage)
hence yh: "(YMap C X η) |∈| (Hom⇘C⇙ X Y)" using assms by (simp add: YFtorObj2)
thus "(z2m⇘C⇙ (YMap C X η)) maps⇘C⇙ X to Y" using assms by (simp add: LSCategory.z2mm2z)
hence "YFtor C ## (z2m⇘C⇙ (YMap C X η)) = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ (z2m⇘C⇙ (YMap C X η)))"
using assms yh by (simp add: YMapYoneda)
also have "... = YMapInv C X (YFtor C @@ Y) (YMap C X η)"
using assms yh by (simp add: LSCategory.z2mm2z)
finally show "YFtor C ## (z2m⇘C⇙ (YMap C X η)) = η" using assms ftor by (simp add: YMap1)
qed
lemma YonedaFaithful:
assumes "LSCategory C" and "f maps⇘C⇙ X to Y" and "g maps⇘C⇙ X to Y"
and "YFtor C ## f = YFtor C ## g"
shows "f = g"
proof-
have ObjX: "X ∈ Obj C" and ObjY: "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)+
have M2Zf: "(m2z⇘C⇙ f) |∈| ((YFtor C @@ Y) @@ X)" and M2Zg: "(m2z⇘C⇙ g) |∈| ((YFtor C @@ Y) @@ X)"
using assms ObjX ObjY by (simp add: LSCategory.m2zz2m YFtorObj2)+
have Ftor: "Ftor (YFtor C @@ Y) : (Op C) ⟶ SET" using assms ObjY by (simp add: YFtorObj HomFtorContraFtor)
have Morf: "f ∈ Mor C" and Morg: "g ∈ Mor C" using assms by auto
have "YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ f) = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ g)"
using assms by (simp add: YMapYoneda)
hence "YMap C X (YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ f)) = YMap C X (YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ g))"
by simp
hence "(m2z⇘C⇙ f) = (m2z⇘C⇙ g)" using assms ObjX ObjY M2Zf M2Zg Ftor by (simp add: YMap2)
thus "f = g" using assms Morf Morg by (simp add: LSCategory.mor2ZFInj)
qed
lemma YonedaEmbedding:
assumes "LSCategory C" and "A ∈ Obj C" and "B ∈ Obj C" and "(YFtor C) @@ A = (YFtor C) @@ B"
shows "A = B"
proof-
have AObjOp: "A ∈ Obj (Op C)" and BObjOp: "B ∈ Obj (Op C)" using assms by (simp add: OppositeCategory_def)+
hence FtorA: "Ftor (Hom⇘C⇙[─,A]) : (Op C) ⟶ SET" and FtorB: "Ftor (Hom⇘C⇙[─,B]) : (Op C) ⟶ SET"
using assms by (simp add: HomFtorContraFtor)+
have "Hom⇘C⇙[─,A] = Hom⇘C⇙[─,B]" using assms by (simp add: YFtorObj)
hence "(Hom⇘C⇙[─,A]) ## (Id (Op C) A) = (Hom⇘C⇙[─,B]) ## (Id (Op C) A)" by simp
hence "Id SET ((Hom⇘C⇙[─,A]) @@ A) = Id SET ((Hom⇘C⇙[─,B]) @@ A)"
using AObjOp BObjOp FtorA FtorB by (simp add: FunctorId)
hence "Id SET (Hom⇘C ⇙A A) = Id SET (Hom⇘C ⇙A B)" using assms by (simp add: HomFtorOpObj)
hence "Hom⇘C ⇙A A = Hom⇘C ⇙A B" using SETCategory by (simp add: Category.IdInj SETobj[of "Hom⇘C ⇙A A"] SETobj[of "Hom⇘C ⇙A B"])
moreover have "(m2z⇘C⇙ (Id C A)) |∈| (Hom⇘C ⇙A A)" using assms by (simp add: Category.Cidm LSCategory.m2zz2m)
ultimately have "(m2z⇘C⇙ (Id C A)) |∈| (Hom⇘C ⇙A B)" by simp
hence "(z2m⇘C⇙ (m2z⇘C⇙ (Id C A))) maps⇘C⇙ A to B" using assms by (simp add: LSCategory.z2mm2z)
hence "(Id C A) maps⇘C⇙ A to B" using assms by (simp add: Category.CatIdInMor LSCategory.m2zz2mInv)
hence "cod⇘C⇙ (Id C A) = B" by auto
thus ?thesis using assms by (simp add: Category.CatIdDomCod)
qed
end