Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sigma migration of morphisms #937

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all 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
82 changes: 66 additions & 16 deletions src/categorical_algebra/CSets.jl
Original file line number Diff line number Diff line change
Expand Up @@ -211,15 +211,25 @@ hasvar(X::ACSetFunctor) = hasvar(X.acset)
dom(F::ACSetFunctor) = FinCat(Presentation(ACSet(F)))

#not clear this couldn't just always give the Vars
function codom(F::ACSetFunctor)
hasvar(F) ? TypeCat{Union{SetOb,VarSet},Union{FinDomFunction{Int},VarFunction}}() :
TypeCat{SetOb,FinDomFunction{Int}}()
end

Categories.do_ob_map(F::ACSetFunctor, x) =
(hasvar(F,functor_key(x)) ? VarSet : SetOb)(F.acset, functor_key(x))
Categories.do_hom_map(F::ACSetFunctor, f) =
(hasvar(F,functor_key(f)) ? VarFunction : FinFunction)(F.acset, functor_key(f))
function codom(::ACSetFunctor)
TypeCat{Union{SetOb,VarSet},Union{FinDomFunction{Int},VarFunction}}()
# hasvar(F) ? TypeCat{Union{SetOb,VarSet},Union{FinDomFunction{Int},VarFunction}}() :
# TypeCat{SetOb,FinDomFunction{Int}}()
end

function Categories.do_ob_map(F::ACSetFunctor, x)
S = acset_schema(F.acset)
Symbol(x) ∈ ob(S) && return SetOb(F.acset, functor_key(x))
Symbol(x) ∈ attrtypes(S) && return VarSet(F.acset, functor_key(x))
error("Bad object $S $x")
end
function Categories.do_hom_map(F::ACSetFunctor, x)
S = acset_schema(F.acset)
kx = functor_key(x)
Symbol(kx) ∈ homs(S; just_names=true) && return FinFunction(F.acset, kx)
Symbol(kx) ∈ attrs(S; just_names=true) && return VarFunction(F.acset, kx)
error("Bad hom $S $x")
end

functor_key(x) = x
functor_key(expr::GATExpr{:generator}) = first(expr)
Expand Down Expand Up @@ -442,11 +452,11 @@ function coerce_components(S, components, X::ACSet{<:PT}, Y) where PT
end)
ocomps = NamedTuple(map(objects(S)) do c
c => coerce_component(c, get(components, c, 1:0),
nparts(X,c), nparts(Y,c); kw[c]...)
maxpart(X,c), maxpart(Y,c); kw[c]...)
end)
acomps = NamedTuple(map(attrtypes(S)) do c
c => coerce_attrvar_component(c, get(components, c, 1:0),
TypeSet(X, c), TypeSet(Y, c), nparts(X,c), nparts(Y,c); kw[c]...)
TypeSet(X, c), TypeSet(Y, c), maxpart(X,c), maxpart(Y,c); kw[c]...)
end)
return merge(ocomps, acomps)
end
Expand Down Expand Up @@ -1125,9 +1135,8 @@ const SubACSet{S} = Subobject{<:StructACSet{S}}

# Componentwise subobjects: coerce VarFunctions to FinFunctions
components(A::SubACSet{S}) where S =
NamedTuple(k => Subobject(k ∈ ob(S) ? vs : FinFunction(vs)) for (k,vs) in
pairs(components(hom(A)))
)
NamedTuple(k => Subobject(k ∈ ob(S) ? vs : FinFunction(vs))
for (k,vs) in pairs(components(hom(A))))

force(A::SubACSet) = Subobject(force(hom(A)))

Expand Down Expand Up @@ -1353,7 +1362,7 @@ abstract_attributes(f::ACSetTransformation) = abstract_attributes(dom(f)) ⋅ f

"""
Find some part + attr that refers to an AttrVar.
Throw error if none exists (i.e. `i` is a wandering variable).
Return `nothing` if none exists (i.e. `i` is a wandering variable).
"""
function var_reference(X::ACSet, at::Symbol, i::Int)
S = acset_schema(X)
Expand All @@ -1363,9 +1372,50 @@ function var_reference(X::ACSet, at::Symbol, i::Int)
return (f, c, first(inc))
end
end
error("Wandering variable $at#$p")
end


"""
Given a value for each variable, create a morphism X → X′ which applies the
substitution. We do this via pushout.

O --> X where C has AttrVars for `merge` equivalence classes
↓ and O has only AttrVars (sent to concrete values or eq classes
C in the map to C.

`subs` and `merge` are dictionaries keyed by attrtype names

`subs` values are int-keyed dictionaries indicating binding, e.g.
`; subs = (Weight = Dict(1 => 3.20, 5 => 2.32), ...)`

`merge` values are vectors of vectors indicating equivalence classes, e.g.
`; merge = (Weight = [[2,3], [4,6]], ...)`
"""
function sub_vars(X::ACSet, subs::AbstractDict=Dict(), merge::AbstractDict=Dict())
S = acset_schema(X)
O, C = [constructor(X)() for _ in 1:2]
ox_, oc_ = Dict{Symbol, Any}(), Dict{Symbol,Any}()
for at in attrtypes(S)
d = get(subs, at, Dict())
ox_[at] = AttrVar.(filter(p->p ∈ keys(d) && !(d[p] isa AttrVar), parts(X,at)))
oc_[at] = Any[d[p.val] for p in ox_[at]]
add_parts!(O, at, length(oc_[at]))

for eq in get(merge, at, [])
isempty(eq) && error("Cannot have empty eq class")
c = AttrVar(add_part!(C, at))
for var in eq
add_part!(O, at)
push!(ox_[at], AttrVar(var))
push!(oc_[at], c)
end
end
end
ox = ACSetTransformation(O,X; ox_...)
oc = ACSetTransformation(O,C; oc_...)
return first(legs(pushout(ox, oc)))
end

# Mark as deleted
#################

Expand Down
12 changes: 5 additions & 7 deletions src/categorical_algebra/Chase.jl
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ function pres_to_eds(S::Presentation; types=Dict(), name="")
eds["$(f_)_total"] = tot
end

return Dict([Symbol(k) => v for (k,v) in collect(eds)])
return Dict{Symbol, ACSetTransformation}(Symbol(k) => v for (k,v) in eds)
end

"""
Expand Down Expand Up @@ -226,17 +226,15 @@ this occured).
function from_c_rel(J::ACSet,cset::ACSet)
S = acset_schema(cset)
res = typeof(cset)()
for o in ob(S)
for o in types(S)
add_parts!(res, o, nparts(J, o))
end
total = true
for (m, s, _) in homs(S)
for (m, s, _) in arrows(S)
msrc, mtgt = add_srctgt(m)
length(J[msrc]) == length(Set(J[msrc])) || error("non-unique $J")
total &= length(J[msrc]) != nparts(J, s)
for (domval, codomval) in zip(J[msrc], J[mtgt])
set_subpart!(res, domval, m, codomval)
end
total &= length(J[msrc]) == nparts(J, s)
res[J[msrc], m] = J[mtgt]
end
return res => total
end
Expand Down
24 changes: 24 additions & 0 deletions src/categorical_algebra/FinCats.jl
Original file line number Diff line number Diff line change
Expand Up @@ -469,12 +469,19 @@ end
"""
const FinFunctor{Dom<:FinCat,Codom<:FinCat} = FinDomFunctor{Dom,Codom}


FinFunctor(maps, dom::FinCat, codom::FinCat) = FinDomFunctor(maps, dom, codom)
FinFunctor(ob_map, hom_map, dom::FinCat, codom::FinCat) =
FinDomFunctor(ob_map, hom_map, dom, codom)
FinFunctor(ob_map, hom_map, dom::Presentation, codom::Presentation) =
FinDomFunctor(ob_map, hom_map, FinCat(dom), FinCat(codom))

"""Assume that dom ⊆ codom"""
FinFunctor(dom::Presentation, codom::Presentation) = FinFunctor(
Dict(x=>x for x in ob_generators(FinCat(dom))),
Dict(x=>x for x in hom_generators(FinCat(dom))),
dom, codom)

Categories.show_type_constructor(io::IO, ::Type{<:FinFunctor}) =
print(io, "FinFunctor")

Expand Down Expand Up @@ -615,15 +622,32 @@ See also: [`is_functorial`](@ref).
function is_natural(α::FinTransformation; check_equations::Bool=true)
F, G = dom(α), codom(α)
C, D = dom(F), codom(F) # == dom(G), codom(G)
# @show typeof(F)
# @show typeof(G)
# println("F"); show(stdout,"text/plain", force(F))
# println("\nG"); show(stdout,"text/plain", force(G))
# println("\nC"); show(stdout,"text/plain", C)
# println("\nD"); show(stdout,"text/plain", D)
all(ob_generators(C)) do c
α_c = α[c]
# println("")
# @show (α_c, c)
# @show (dom(D, α_c), ob_map(F,c))
# @show dom(D, α_c) == ob_map(F,c)
# @show (codom(D, α_c) , ob_map(G,c))
# @show (codom(D, α_c) == ob_map(G,c))
dom(D, α_c) == ob_map(F,c) && codom(D, α_c) == ob_map(G,c)
end || return false

if check_equations
all(hom_generators(C)) do f
Ff, Gf = hom_map(F,f), hom_map(G,f)
α_c, α_d = α[dom(C,f)], α[codom(C,f)]
# @show (f, Ff, Gf)
# @show (α_c, α_d)
# @show compose(D, α_c, Gf)
# @show compose(D, Ff, α_d)
# @show is_hom_equal(D, compose(D, α_c, Gf), compose(D, Ff, α_d))
is_hom_equal(D, compose(D, α_c, Gf), compose(D, Ff, α_d))
end || return false
end
Expand Down
4 changes: 3 additions & 1 deletion src/categorical_algebra/FinSets.jl
Original file line number Diff line number Diff line change
Expand Up @@ -355,11 +355,13 @@ Base.length(f::AbsVarFunction{T}) where T = length(collect(f.fun))
Base.collect(f::AbsVarFunction{T}) where T = collect(f.fun)

(f::VarFunction{T})(v::T) where T = v
#possibly kill this one
(f::AbsVarFunction{T})(v::AttrVar) where T = f.fun(v.val)
(f::AbsVarFunction{T})(v) where T = f.fun(v)

#XX if a VarSet could contain an arbitrary FinSet of variables this
# wouldn't need to be so violent
dom(f::AbsVarFunction{T}) where T = VarSet{T}(length(collect(f.fun)))
dom(f::AbsVarFunction{T}) where T = FinSet(length(collect(f.fun)))
codom(f::VarFunction{T}) where T = VarSet{T}(length(f.codom))
id(s::VarSet{T}) where T = VarFunction{T}(AttrVar.(1:s.n), FinSet(s.n))
function is_monic(f::VarFunction)
Expand Down
Loading
Loading