Partial abstraction / variable substitution+merging #29
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
VarACSets work very well with colimits, but limits are subtle. Likewise, maps out of VarACSets are very nice, but maps into VarACSets are subtle. Some more machinery for working with VarACSets is implemented here (which could potentially be upstreamed once it gets battle-tested).
Firstly,
sub_vars
takes an ACSet + some data (e.g.AttrVar(1) -> :x, AttrVar(3)->:abc
) and "evaluates" the variables. This PR also allows this to merge variables together based on input data like[AttrVar(2), AttrVar(4)]
. This is all done via a pushout.Secondly, a notion of "partial abstraction" is needed because we want to take maps
B->X
and lift them to maps into the "fully abstracted" version ofX
1 (call itA
). This is hard for two reasons: 1.) no ACSet with concrete attribute values can map intoA
, 2.) an issue with needing to send an AttrVar to two distinct AttrVars inA
, explained more in the docstring. This problem is addressed via applyingsub_vars
to a fully abstracted ACSet.This corresponds to a factorization of
B->X
intoB->ParAbs(X)->X
(observed by @KevinArlin: see nlab and the blog for more details).Footnotes
This replaces all attributes with distinct variables, even if (e.g.) all the weights of the graph edges are the same value. ↩