Skip to content
Draft
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
98 changes: 83 additions & 15 deletions src/categorical_algebra/pointwise/datamigrations/Yoneda.jl
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
module Yoneda
export representable, yoneda, subobject_classifier, internal_hom, @acset_colim
export representable, yoneda, subobject_classifier, internal_hom, @acset_colim,
@named_acset_colim, @acset_transformation_colim

using DataStructures, MLStyle

Expand Down Expand Up @@ -219,6 +220,19 @@ function parse_diagram_data(x::Expr, mod::Module)::DiagramData
Expr(:$, x) => Base.eval(mod, x)
end

function parse_eq(t1t2::Tuple)
p1,p2 = parse_call.(t1t2)
if p1 isa RPath
if p2 isa RPath
push!(data.eqs, p1 => p2)
else
data.vals[p1] = p2
end
else
data.vals[p2] = p1
end
end

for arg in Base.remove_linenums!(x).args
@match arg begin
Expr(:(::), partname::Symbol, parttype::Symbol) => begin
Expand All @@ -227,18 +241,13 @@ function parse_diagram_data(x::Expr, mod::Module)::DiagramData
Expr(:(::), Expr(:tuple, partnames...), parttype::Symbol) => begin
add_part.(partnames, Ref(parttype))
end
Expr(:call, :(==), t1, t2) => begin
p1,p2 = parse_call.([t1,t2])
if p1 isa RPath
if p2 isa RPath
push!(data.eqs, p1 => p2)
else
data.vals[p1] = p2
end
else
data.vals[p2] = p1
end
Expr(:call, :(==), t1, t2) => parse_eq((t1,t2))
Expr(:comparison, raw...) => begin
all(==(:(==)), raw[2:2:end]) || error("Improper equality $arg")
ts = raw[1:2:end]
parse_eq.(zip(ts, ts[2:end]))
end
_ => error("Unexpected expr $arg")
end
end
data
Expand All @@ -256,10 +265,59 @@ end
"""
macro acset_colim(yon, body)
quote
colimit_representables($(parse_diagram_data(body, __module__)), $(esc(yon)))
colimit_representables($(parse_diagram_data(body, __module__)), $(esc(yon)))[2]
end
end

"""
```
Dom = @named_acset_colim yGraph MyDomain begin
v::V; e::E; src(e)==v
end
```

This would be have like `@acset_colim` and assign to `Dom` the walking edge
ACSet with src=1 and tgt=2. However, unlike `@acset_colim`, this also assigns
to a variable MyDomain the NamedTuple `(v=(:V, 1),e=(:E, 1))`.
"""
macro named_acset_colim(yon, names_var, body)

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment on the PR moved here: #986 (comment)

Having some experience with these new macros now, I think that it might be unwise to have @named_acset_colimit implemented the way it is because it is not referentially transparent -- the names appear effectively by side-effect. This more functional (and simpler!) implementation might be better:

macro named_acset_colim(yon, body)
  quote 
    colimit_representables($(parse_diagram_data(body, __module__)), $(esc(yon)))
  end
end

quote
names, acset = colimit_representables($(parse_diagram_data(body, __module__)), $(esc(yon)))
$(esc(names_var)) = names
acset
end
end

"""
Although providing an assignment for every generator is sufficient to guarantee
a uniquely determined homomorphism, it is not always necessary. If a generator
`a` in the domain is equal to some `b.f`, then only specifying `b` is necessary.
Furthermore, keyword arguments like `monic`, `epic`, and `iso` can be used to
specify a morphism uniquely (or `any` + `random` if it doesn't matter).
"""
macro acset_transformation_colim(yon, body1, body2, body3, kwargs=:((;)))
initial = Dict(map(filter(e->e isa Expr,body3.args)) do e
@match e begin
Expr(:call, :(=>), a, b) => a => b
end
end)
quote
names1, acset1 = colimit_representables(
$(parse_diagram_data(body1, __module__)), $(esc(yon)))
names2, acset2 = colimit_representables(
$(parse_diagram_data(body2, __module__)), $(esc(yon)))

initial=DefaultDict{Symbol,Dict}(()->Dict())
for (k,v) in $initial
ty, domval = names1[k]
_, codval = names2[v]
initial[ty][domval] = codval
end
homomorphism(acset1, acset2; initial=initial, $(kwargs)...)
end
end


"""
Construct an ACSet given a colimit of representables, given by generating
representables and relations. Assumes a background context of VarACSetCategory
Expand Down Expand Up @@ -327,11 +385,21 @@ function colimit_representables(data::DiagramData, y::FinDomFunctor)
end

# If we are just asking for a coproduct of representables
isempty(spans) && return apex(Σ)
isempty(spans) && return (names, apex(Σ))

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

names is not yet defined here


# Perform all pushouts at once by putting the spans together in parallel
lefts, rights = left.(spans), right.(spans)
apex(pushout[𝒞](foldl(oplus[𝒞′], lefts), foldl(copair[𝒞′], rights)))
_,bigι = big_colim = pushout[𝒞](foldl(oplus[𝒞′], lefts), foldl(copair[𝒞′], rights))

# TODO get representing element for real. Requires passing in extra data.
names = NamedTuple(map(reprs) do (repr_type, repr_name)
ι = FinFunction(lookup[repr_name][repr_type], bigι[repr_type])
length(dom(ι)) == 1 || error("Assumption that representing element is "*
"unique has been violated, more data required by `colimit_representables`")
repr_name => (repr_type, ι(only(dom(ι))))
end)

(names, apex(big_colim))
end

end # module
26 changes: 26 additions & 0 deletions test/categorical_algebra/pointwise/csetcats/Yoneda.jl
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ ZG = ob(product[ACSetCategory(DDS42())](Z,G))
#############

@test is_isomorphic((@acset_colim y_Graph begin v::V end), Graph(1))
@test is_isomorphic((@acset_colim y_Graph begin (v1,v2,v3)::V; v1==v2==v3 end), Graph(1))

v3e2 = @acset_colim y_Graph begin
v1::V; (e1,e2)::E
Expand All @@ -84,4 +85,29 @@ v3e2′ = @acset Graph begin V=3; E=2; src=[1,2]; tgt=[2,3] end

@test is_isomorphic(v3e2, v3e2′)

acs = @named_acset_colim y_Graph MyDomain begin
v::V; e::E; src(e)==v
end

@test acs[MyDomain.e[2],:src] == MyDomain.v[2]

# sending path graph •→•→• to •→•↺↺. There are two graph momomorphisms if we
# identify the start vertices
f = @acset_transformation_colim y_Graph #=domain=# begin
(vstart,vend)::V; (e1,e2)::E;
src(e1)==vstart; tgt(e1)==src(e2); tgt(e2)==vend
end #=codomain =# begin
v::V; (ea,eb,ec)::E;
src(ea)==v; tgt(ea)==src(eb) == tgt(eb) == src(ec) == tgt(ec)
end #=mapping=# begin vstart=>v; end #=kw=# (any=true, monic=[:E])

# However, we can remove `any=true` by also specifying one the two loops
f2 = @acset_transformation_colim y_Graph #=domain=# begin
(vstart,vend)::V; (e1,e2)::E;
src(e1)==vstart; tgt(e1)==src(e2); tgt(e2)==vend
end #=codomain =# begin
v::V; (ea,eb,ec)::E;
src(ea)==v; tgt(ea)==src(eb) == tgt(eb) == src(ec) == tgt(ec)
end #=mapping=# begin vstart=>v; e2=>eb; end #=kw=# (monic=[:E],)

end # module
Loading