Skip to content

Commit

Permalink
slice categories
Browse files Browse the repository at this point in the history
  • Loading branch information
Kris Brown committed Jan 22, 2025
1 parent 5ea5b7e commit 69f163b
Show file tree
Hide file tree
Showing 11 changed files with 256 additions and 145 deletions.
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
export ThFreeDiagram, FreeDiagram, cocone_objects, cone_objects, diagram_type,
fmap, specialize, ob, hom
fmap, specialize, ob, hom, obset, homset, obmap, hommap
using StaticArrays: StaticVector, SVector

using GATlab, ACSets
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -154,8 +154,12 @@ end


""" Replace homs via a replacement function """
fmap(d::Multispan, o, h, O::Type, H::Type) =
Multispan{O,H,O}(o(apex(d))::O, Vector{H}(h.(legs(d))), Vector{O}(o.(feet(d))))
function fmap(d::Multispan, o, h, O::Type, H::Type)
new_apex::O = o(apex(d))
new_legs::Vector{H} = h.(legs(d))
new_feet::Vector{O} = Vector{O}(o.(feet(d)))
Multispan{O,H,O}(new_apex, new_legs, new_feet)
end

function untag(d::Multispan{Ob,Hom}, i::Int, j::Int) where {Ob,Hom}
O, H = untag(Ob, i), untag(Hom, j)
Expand Down
128 changes: 128 additions & 0 deletions src/04_categorical_algebra/01_cats/12_slice/LimitsColimits.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,128 @@
module SliceLimitsColimits

using StructEquality
using GATlab

using ...Cats
import ...Cats: limit, colimit, universal
using ..SliceCategories

############
# Colimits #
############

@instance ThCategoryWithInitial{SliceOb{ObT, HomT}, HomT, AbsSet, AbsColimit,
Multicospan, EmptyDiagram} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin

colimit(::EmptyDiagram)::AbsColimit =
InitialColimit{SliceOb{<:ObT, <:HomT}, HomT}(
SliceOb(apex(initial[model.cat]()), create[model.cat](model.over)))

universal(::AbsColimit, ::EmptyDiagram, a::Multicospan) =
FinFunction(Int[], FinSet(apex[model](a)))
end

@instance ThCategoryUnbiasedCoproducts{SliceOb{ObT, HomT}, HomT, AbsSet, AbsColimit,
Multicospan, DiscreteDiagram} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin

colimit(d::DiscreteDiagram)::AbsColimit = colimit_slice(model, FreeDiagram(d))

universal(colim::AbsColimit, diag::DiscreteDiagram, csp::Multicospan) =
slice_colimit_universal(model, colim, diag, csp)
end

@instance ThCategoryWithPushouts{SliceOb{ObT, HomT}, HomT, AbsSet, AbsColimit,
Multicospan, Multispan} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin

colimit(d::Multispan)::AbsColimit = colimit_slice(model, FreeDiagram(d))

universal(colim::AbsColimit, diag::Multispan, csp::Multicospan) =
slice_colimit_universal(model, colim, diag, csp)
end

@instance ThCategoryWithBipartiteColimits{SliceOb{ObT, HomT}, HomT, AbsSet, AbsColimit,
Multicospan, BipartiteFreeDiagram} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin

colimit(d::BipartiteFreeDiagram)::AbsColimit = colimit_slice(model, FreeDiagram(d))

universal(colim::AbsColimit, diag::BipartiteFreeDiagram, csp::Multicospan) =
slice_colimit_universal(model, colim, FreeDiagram(diag), csp)
end


"""
Convert colimit in slice category into computation in the underlying category
"""
function colimit_slice(model::SliceC, diagram::FreeDiagram)
𝒞, D = model.cat, getvalue(diagram)
Ob, Hom = impl_type(𝒞, ThCategory, :Ob), impl_type(𝒞, ThCategory, :Hom)
# discard all the slice info in the colimit diagram - it's irrelevant
colim = colimit[𝒞](fmap(D, x -> x.ob, identity, Ob, Hom))

# compute new apex using the universal property of colimits
csp = Multicospan(model.over, map(x -> x.hom,
cocone_objects(D));
cat=𝒞)
new_apex = SliceOb(ob(colim), universal[𝒞](colim, csp))
cocone = Multicospan(new_apex, legs(colim), cocone_objects(D))
return ColimitCocone(cocone, diagram)
end

##########
# Limits #
##########
@instance ThCategoryUnbiasedProducts{SliceOb{ObT, HomT}, HomT, AbsSet, AbsLimit,
Multispan, DiscreteDiagram} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin

limit(d::DiscreteDiagram)::AbsLimit = limit_slice(model, FreeDiagram(d))

universal(colim::AbsLimit, diag::DiscreteDiagram, csp::Multispan) =
slice_limit_universal(model, colim, FreeDiagram(diag), csp)
end

"""
A limit cone in a slice category 𝒞/X contains the limit cone data (where
objects are SliceOb and morphisms are Homs in 𝒞) in addition to caching the
limit in 𝒞 (which has a diagram with one extra object) in order to easily
apply the universal property.
"""
@struct_hash_equal struct SliceLimitCone <: AbsLimit
cone::Multispan
diagram::FreeDiagram
underlying::AbsLimit # in underlying 𝒞: `diagram` + 1 extra object
end

"""
Convert a limit problem in the slice category to a limit problem of the
underlying category.
Encode the base of slice as the first object in the new diagram
"""
function limit_slice(model, diagram::FreeDiagram)
𝒞 = model.cat
obs = [model.over, [x.ob for x in ob(diagram)]...] # one extra object

# assumes that the Ob/Hom sets of `diagram` are Int!
# fix by making a Dict{Int,Ob} for input diagram
homs = map(obset(diagram)) do o
(obmap(diagram, o).hom,o+1,1)
end map(homset(diagram)) do h
(hommap(diagram, h), src(diagram, h)+1, tgt(diagram, h)+1)
end |> Vector{Tuple{impl_type(𝒞, ThCategory, :Hom), Int, Int}}

FG = FreeGraph(obs,homs)
lim = limit[𝒞](FG)

new_apex = SliceOb(apex(lim), first(legs(lim.cone)))
spn = Multispan(new_apex, legs(lim.cone)[2:end], FG[:ob][2:end])
SliceLimitCone(spn, diagram, lim)
end

""" Use the universal property of the underlying category. """
function slice_limit_universal(model, lim::AbsLimit, diag::FreeDiagram, sp::Multispan)
𝒞, apx = model.cat, apex(sp)
universal[𝒞](lim.underlying, Multispan(apx.ob, [apx.hom, sp...]; cat=𝒞))
end


end # module
155 changes: 59 additions & 96 deletions src/04_categorical_algebra/01_cats/12_slice/SliceCategories.jl
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
module SliceCategories
export Slice, SliceHom
export SliceC, SliceOb

using StructEquality

Expand All @@ -8,16 +7,20 @@ using GATlab
import ....Theories: dom, codom, compose, id, ThCategory
import ....BasicSets: force

using ..FreeDiagrams, ..LimitsColimits
using ...Cats

"""
The data of the object of a slice category (say, some category C sliced over an
object X in Ob(C)) is the data of a homomorphism in Hom(A,X) for some ob A.
"""
@struct_hash_equal struct Slice{Hom}
slice::Hom
@struct_hash_equal struct SliceOb{ObT, HomT}
ob::ObT
hom::HomT
end

SliceOb(hom; cat=nothing) =
SliceOb(isnothing(cat) ? dom(hom) : dom[cat](hom), hom)

"""
The data of the morphism of a slice category (call it h, and suppose a category
C is sliced over an object X in Ob(C)) between objects f and g is a homomorphism
Expand All @@ -27,107 +30,67 @@ in the underlying category that makes the following triangle commute.
A --> B
f ↘ ↙ g
X
"""
@struct_hash_equal struct SliceHom{Hom, Dom<:Slice, Codom<:Slice}
dom::Dom
codom::Codom
f::Hom
end

function SliceHom(d::Dom, cd::Codom, f::Hom; strict::Bool=true) where {Dom,Codom,Hom}
!strict || codom(d) == codom(cd) || error("$d and $cd not in same category")
!strict || dom(d) == dom(f) || error("dom $d does not match $f")
!strict || dom(cd) == codom(f) || error("codom $cd does not match $f")
return SliceHom{Hom,Dom,Codom}(d, cd, f)
end

dom(s::Slice) = dom(s.slice)
codom(s::Slice) = codom(s.slice)
force(s::Slice) = Slice(force(s.slice))
force(s::SliceHom) = SliceHom(
force(dom(s)), force(codom(s)), force(s.f))


struct SliceLimit{Hom, Ob <: Slice{Hom}, Diagram,
Cone <: Multispan{Ob}} <: AbsLimit
diagram::Diagram
cone::Cone
underlying::AbsLimit
end

struct SliceColimit{Hom, Ob <: Slice{Hom}, Diagram,
Cocone <: Multicospan{Ob}} <: AbsColimit
diagram::Diagram
cocone::Cocone
underlying::AbsColimit
end


@instance ThCategory{Slice, SliceHom} begin
dom(f::SliceHom) = f.dom
codom(f::SliceHom) = f.codom
id(A::Slice) = SliceHom(A, A, id(dom(A.slice)))
function compose(f::SliceHom, g::SliceHom)
SliceHom(dom(f), codom(g), compose(f.f, g.f))
end
end

"""
Get the underlying diagram of a slice category diagram which has the object
being sliced over explicitly, and arrows are ACSetTransformations
So a slice category has
"""
function slice_diagram(f::FreeDiagram)::FreeDiagram
obs = vcat([codom(f[:ob][1])], [dom(x.slice) for x in f[:ob]])
homs = [(h.slice,i+1,1) for (i, h) in enumerate(f[:ob])]
append!(homs, [(h.f, i+1, j+1) for (i,j,h) in zip(f[:src],f[:tgt],f[:hom])])
FreeDiagram(obs,homs)
@struct_hash_equal struct SliceC{ObT, HomT, C}
cat::C
over::ObT
function SliceC(cat::C, over) where C
types = try
impl_types(cat, ThCategory)
catch e
throw(e)
end
implements(cat, ThCategoryExplicitSets, types) || error("Bad cat $cat")
new{types..., C}(cat, over)
end
end

"""
Convert a limit problem in the slice category to a limit problem of the
underlying category.
using .ThCategoryExplicitSets

@instance ThCategoryExplicitSets{SliceOb{<:ObT, <:HomT}, HomT, AbsSet
} [model::SliceC{ObT, HomT, C}
] where {ObT, HomT, C} begin
function Ob(x::SliceOb{<:ObT, <:HomT})
try
Ob[model.cat](x.ob)
catch e
error("ob is not valid", e)
end
try
Hom[model.cat](x.hom, x.ob, model.over)
catch e
error("hom is not valid", e)
end
x
end

Encode the base of slice as the first object in the new diagram
"""
function limit(::Type{Tuple{S,H}}, f::FreeDiagram) where {S<:Slice, H<:SliceHom}
obs = [codom(f[:ob][1]), [dom(x.slice) for x in f[:ob]]...] # one extra object
homs = [[(h.slice,i+1,1) for (i, h) in enumerate(f[:ob])]...,
[(h.f, i+1, j+1) for (i,j,h) in zip(f[:src],f[:tgt],f[:hom])]...]
lim = limit(FreeDiagram(obs,homs))
new_apex = Slice(first(legs(lim.cone)))
new_cone_legs = [SliceHom(new_apex, ob, leg) for (ob, leg)
in zip(f[:ob],legs(lim.cone)[2:end])]
return SliceLimit(f, Multispan(new_apex, new_cone_legs), lim)
end
function Hom(f::HomT, x::SliceOb{<:ObT, <:HomT}, y::SliceOb{<:ObT, <:HomT})
try
Hom[model.cat](f, x.ob, y.ob)
catch e
error("morphism is not valid in base category", e)
end
compose[model.cat](f, y.hom; context=(a=x.ob, b=y.ob, c=model.over)) == x.hom ||
error("commutativity of triangle does not hold")
f
end

id(x::SliceOb{<:ObT, <:HomT}) = id[model.cat](x.ob)

colimit(s::Multispan{<:Slice}) = colimit(FreeDiagram{Slice,SliceHom}(s))
dom(::HomT; context) = context[:dom]

function colimit(::Type{Tuple{S,H}}, diagram::FreeDiagram) where {S<:Slice, H<:SliceHom}
nparts(diagram, :V) > 0 ||
error("Requires nonempty diagram in order to know what is sliced over")
codom(::HomT; context) = context[:codom]

# discard all the slice info in the colimit diagram - it's irrelevant
colim = colimit(map(diagram, ob = x -> dom(x.slice), hom = h -> h.f))
function compose(f::HomT, g::HomT; context=nothing)
context=isnothing(context) ? nothing : map(x -> x.ob, context)
compose[model.cat](f, g; context)
end

# compute new apex using the universal property of colimits
X = codom(first(diagram[:ob]))
csp = Multicospan(X, map(x -> x.slice, diagram[:ob]))
new_apex = Slice(universal(colim, csp))
new_cocone_legs = [SliceHom(o, new_apex, l)
for (o, l) in zip(diagram[:ob],legs(colim))]
return SliceColimit(diagram, Multicospan(new_apex, new_cocone_legs), colim)
# Actually we can get more specific than this with PredicatedSets.
ob_set() = SetOb(SliceOb{ObT, HomT})
hom_set() = SetOb(HomT)
end


function universal(lim::SliceLimit, sp::Multispan)
# Use the universal property of the underlying category.
apx = apex(sp)
newspan = vcat([apx.slice],[x.f for x in sp])
u = universal(lim.underlying, Multispan(dom(apx), newspan))
apx2 = Slice(first(legs(lim.underlying.cone)))
return SliceHom(apx, apx2, u)
end

end # module
11 changes: 11 additions & 0 deletions src/04_categorical_algebra/01_cats/12_slice/module.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
"""
This largely copies the `GATlab.Stdlib` version of Slice categories, except it
uses `ThCategoryExplicitSets` rather than `ThCategory`.
"""
module SliceCategories

include("SliceCategories.jl")
include("LimitsColimits.jl")


end # module
2 changes: 1 addition & 1 deletion src/04_categorical_algebra/01_cats/module.jl
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ include("10_commutative_diagrams/CommutativeDiagrams.jl")
include("11_diagrams/module.jl") # 5
@reexport using .Diagrams

include("12_slice/SliceCategories.jl")
include("12_slice/module.jl")
@reexport using .SliceCategories

include("13_subobjects/Subobjects.jl") # Limits
Expand Down
3 changes: 3 additions & 0 deletions src/04_categorical_algebra/02_setcats/SetCat/SetCat.jl
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ using ...Cats

@instance ThCategoryExplicitSets{AbsSet, SetFunction,AbsSet} [model::SetC] begin
dom(f::SetFunction)::AbsSet = dom(f)

codom(f::SetFunction)::AbsSet = codom(f)

id(A::AbsSet)::SetFunction = SetFunction(A) # identity function
Expand All @@ -24,6 +25,8 @@ using ...Cats
error("Domain mismatch in composition: $(codom(f)) != $(dom(g))")
SetFunction(f, g)
end

ob_set() = SetOb(AbsSet)

hom_set() = SetOb(SetFunction)
end
Loading

0 comments on commit 69f163b

Please sign in to comment.