diff --git a/src/categorical_algebra/FinCats.jl b/src/categorical_algebra/FinCats.jl index e05054548..ed50c211b 100644 --- a/src/categorical_algebra/FinCats.jl +++ b/src/categorical_algebra/FinCats.jl @@ -25,8 +25,8 @@ using DataStructures: IntDisjointSets, in_same_set, num_groups using ACSets using ...GATs import ...GATs: equations -using ...Theories: ThCategory, ThSchema, ThPointedSetCategory, ThPointedSetSchema, - ObExpr, HomExpr, AttrExpr, AttrTypeExpr, FreeSchema, FreePointedSetCategory, zeromap +using ...Theories: ThCategory, ThSchema, ThPointedCategory, ThPointedSchema, + ObExpr, HomExpr, AttrExpr, AttrTypeExpr, FreeSchema, FreePointedCategory, zeromap import ...Theories: dom, codom, id, compose, ⋅, ∘ using ...Graphs import ...Graphs: edges, src, tgt, enumerate_paths @@ -312,11 +312,11 @@ function FinCatPresentation(pres::Presentation{ThSchema}) FinCatPresentation{ThSchema,Ob,Hom}(pres) end -function FinCatPresentation(pres::Presentation{ThPointedSetSchema}) +function FinCatPresentation(pres::Presentation{ThPointedSchema}) S = pres.syntax Ob = Union{S.Ob, S.AttrType} Hom = Union{S.Hom, S.Attr, S.AttrType} - FinCatPresentation{ThPointedSetSchema,Ob,Hom}(pres) + FinCatPresentation{ThPointedSchema,Ob,Hom}(pres) end """ Computes the graph generating a finitely @@ -328,12 +328,12 @@ in the resulting graph. presentation(C::FinCatPresentation) = C.presentation ob_generators(C::FinCatPresentation) = generators(presentation(C), :Ob) -ob_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}) = let P = presentation(C) +ob_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}) = let P = presentation(C) vcat(generators(P, :Ob), generators(P, :AttrType)) end hom_generators(C::FinCatPresentation) = generators(presentation(C), :Hom) -hom_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}) = let P = presentation(C) +hom_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}) = let P = presentation(C) vcat(generators(P, :Hom), generators(P, :Attr)) end equations(C::FinCatPresentation) = equations(presentation(C)) @@ -348,7 +348,7 @@ hom_generator_name(C::FinCatPresentation, f::GATExpr{:generator}) = first(f) ob(C::FinCatPresentation, x::GATExpr) = gat_typeof(x) == :Ob ? x : error("Expression $x is not an object") -ob(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}, x::GATExpr) = +ob(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}, x::GATExpr) = gat_typeof(x) ∈ (:Ob, :AttrType) ? x : error("Expression $x is not an object or attribute type") @@ -357,7 +357,7 @@ hom(C::FinCatPresentation, fs::AbstractVector) = mapreduce(f -> hom(C, f), compose, fs) hom(C::FinCatPresentation, f::GATExpr) = gat_typeof(f) == :Hom ? f : error("Expression $f is not a morphism") -hom(::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}, f::GATExpr) = +hom(::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}, f::GATExpr) = gat_typeof(f) ∈ (:Hom, :Attr, :AttrType) ? f : error("Expression $f is not a morphism or attribute") diff --git a/src/theories/Category.jl b/src/theories/Category.jl index 5261fec39..0b05fae95 100644 --- a/src/theories/Category.jl +++ b/src/theories/Category.jl @@ -3,7 +3,7 @@ export ThCategory, FreeCategory, Ob, Hom, dom, codom, id, compose, ⋅, ThCopresheaf, FreeCopresheaf, El, ElExpr, ob, act, ThPresheaf, FreePresheaf, coact, ThMCategory, FreeMCategory, Tight, reflexive, transitive, - ThPointedSetCategory, FreePointedSetCategory, zeromap + ThPointedCategory, FreePointedCategory, zeromap, ZeroOb import Base: inv, show @@ -200,21 +200,27 @@ abstract type TightExpr{T} <: GATExpr{T} end end """ -Theory of a pointed set-enriched category. -We axiomatize a category equipped with zero morphisms. +Theory of a pointed category. +We axiomatize a category equipped with a zero object and zero morphisms. +At the moment, the zero object is technically only required to be +a weak zero object; we don't ban nonzero maps to and from it. A functor from an ordinary category into a freely generated -pointed-set enriched category, -equivalently, a pointed-set enriched category in which no two nonzero maps +pointed category, +equivalently, a pointed category in which no two nonzero maps compose to a zero map, is a good notion -of a functor that's total on objects and partial on morphisms. +of a partial functor. """ -@theory ThPointedSetCategory{Ob,Hom} <: ThCategory{Ob,Hom} begin +@theory ThPointedCategory{Ob,Hom} <: ThCategory{Ob,Hom} begin + ZeroOb()::Ob zeromap(A,B)::Hom(A,B)⊣(A::Ob,B::Ob) compose(zeromap(A,B),f::(B→C))==zeromap(A,C)⊣(A::Ob,B::Ob,C::Ob) compose(g::(A→B),zeromap(A,B))==zeromap(A,C)⊣(A::Ob,B::Ob,C::Ob) + + #f == g ⊣ (A::Ob,f::Hom(A,ZeroOb()),g::Hom(A,ZeroOb())) + #f == g ⊣ (B::Ob,f::Hom(ZeroOb(),B),g::Hom(ZeroOb(),B)) end -@syntax FreePointedSetCategory{ObExpr,HomExpr} ThPointedSetCategory begin +@syntax FreePointedCategory{ObExpr,HomExpr} ThPointedCategory begin compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id) end diff --git a/src/theories/Schema.jl b/src/theories/Schema.jl index 4d25a91e1..c80fcdebe 100644 --- a/src/theories/Schema.jl +++ b/src/theories/Schema.jl @@ -1,4 +1,4 @@ -export ThSchema, FreeSchema, AttrType, Attr, SchemaExpr, AttrTypeExpr, AttrExpr, ThPointedSetSchema, FreePointedSetSchema,zeromap +export ThSchema, FreeSchema, AttrType, Attr, SchemaExpr, AttrTypeExpr, AttrExpr, ThPointedSchema, FreePointedSchema,zeromap, ZeroAttr # Schema @@ -33,9 +33,14 @@ abstract type AttrExpr{T} <: SchemaExpr{T} end compose(f::Hom, x::Attr) = associate_unit(new(f,x; strict=true), id) end -@theory ThPointedSetSchema{Ob,Hom,AttrType,Attr} <: ThPointedSetCategory{Ob,Hom} begin +""" +A pointed schema is a schema which is pointed on both sides. +""" +@theory ThPointedSchema{Ob,Hom,AttrType,Attr} <: ThPointedCategory{Ob,Hom} begin AttrType::TYPE Attr(dom::Ob,codom::AttrType)::TYPE + + ZeroAttr()::AttrType zeromap(A::Ob,X::AttrType)::Attr(A,X) compose(f::Hom(A,B), g::Attr(B,X))::Attr(A,X) ⊣ (A::Ob, B::Ob, X::AttrType) @@ -46,9 +51,10 @@ end (compose(f, compose(g, a)) == compose(compose(f, g), a) ⊣ (A::Ob, B::Ob, C::Ob, X::AttrType, f::Hom(A,B), g::Hom(B,C), a::Attr(C, X))) compose(id(A), a) == a ⊣ (A::Ob, X::AttrType, a::Attr(A,X)) + #a == b ⊣(A::Ob,a::Attr(A,ZeroAttr()),b::Attr(A,ZeroAttr())) end -@syntax FreePointedSetSchema{ObExpr,HomExpr,AttrTypeExpr,AttrExpr} ThPointedSetSchema begin +@syntax FreePointedSchema{ObExpr,HomExpr,AttrTypeExpr,AttrExpr} ThPointedSchema begin compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id) compose(f::Hom,a::Attr) = associate_unit(normalize_zero(new(f,a; strict=true)), id) end \ No newline at end of file diff --git a/test/theories/Category.jl b/test/theories/Category.jl index 77f1fa400..85f65862d 100644 --- a/test/theories/Category.jl +++ b/test/theories/Category.jl @@ -125,8 +125,13 @@ x = El(:x, A) # Pointed category ################## -A,B,C,D = map(x->Ob(FreePointedSetCategory,x),[:A,:B,:C,:D]) +A,B,C,D = map(x->Ob(FreePointedCategory,x),[:A,:B,:C,:D]) +Z = ZeroOb(FreePointedCategory.Ob) f,g,h = Hom(:f,A,B),Hom(:g,B,C),Hom(:h,C,D) zAB,zBC,zAC = zeromap(A,B),zeromap(B,C),zeromap(A,C) +k,l = Hom(:k,A,Z), Hom(:l,Z,A) +zAZ,zZA = zeromap(A,Z),zeromap(Z,A) @test zAC == compose(f,zBC) == compose(zAB,g) @test compose(f,zBC,h) == zeromap(A,D) +#@test k == zAZ +#@test l == zZA diff --git a/test/theories/Schema.jl b/test/theories/Schema.jl index b97bfb1c3..8d0af4bf0 100644 --- a/test/theories/Schema.jl +++ b/test/theories/Schema.jl @@ -21,8 +21,8 @@ x, y = Attr(:x, A, C), Attr(:y, B, C) # Pointed schema ################## -A,B,C = map(x->Ob(FreePointedSetSchema,x),[:A,:B,:C]) -X = AttrType(FreePointedSetSchema.AttrType,:X) +A,B,C = map(x->Ob(FreePointedSchema,x),[:A,:B,:C]) +X = AttrType(FreePointedSchema.AttrType,:X) f,g = Hom(:f,A,B),Hom(:g,B,C) a = Attr(:a,C,X) zAB,zBC,zAC,zAX,zBX,zCX = zeromap(A,B),zeromap(B,C),zeromap(A,C),zeromap(A,X),zeromap(B,X),zeromap(C,X)