Skip to content

Commit

Permalink
sigma action on morphisms
Browse files Browse the repository at this point in the history
working draft for SimpleMigrations
  • Loading branch information
Kris Brown committed Sep 11, 2024
1 parent b71a5b8 commit 511a515
Show file tree
Hide file tree
Showing 7 changed files with 394 additions and 117 deletions.
77 changes: 64 additions & 13 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")

Check warning on line 224 in src/categorical_algebra/CSets.jl

View check run for this annotation

Codecov / codecov/patch

src/categorical_algebra/CSets.jl#L224

Added line #L224 was not covered by tests
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")

Check warning on line 231 in src/categorical_algebra/CSets.jl

View check run for this annotation

Codecov / codecov/patch

src/categorical_algebra/CSets.jl#L231

Added line #L231 was not covered by tests
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 @@ -1353,7 +1363,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).

Check warning on line 1366 in src/categorical_algebra/CSets.jl

View check run for this annotation

Codecov / codecov/patch

src/categorical_algebra/CSets.jl#L1366

Added line #L1366 was not covered by tests
"""
function var_reference(X::ACSet, at::Symbol, i::Int)
S = acset_schema(X)
Expand All @@ -1363,9 +1373,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(

Check warning on line 480 in src/categorical_algebra/FinCats.jl

View check run for this annotation

Codecov / codecov/patch

src/categorical_algebra/FinCats.jl#L480

Added line #L480 was not covered by tests
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
Loading

0 comments on commit 511a515

Please sign in to comment.