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

The 2-category of categories #526

Merged
merged 9 commits into from
Oct 20, 2021
Prev Previous commit
Next Next commit
ENH: Basic data structures for natural transformations.
For the case of natural transformations where the domain category is
finitely presented.
  • Loading branch information
epatters committed Oct 19, 2021
commit f50aa76fbd906ce9c6439663d21fbe897331e576
7 changes: 1 addition & 6 deletions src/categorical_algebra/CSets.jl
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import ..Subobjects: Subobject, SubobjectBiHeytingAlgebra,
implies, ⟹, subtract, \, negate, ¬, non, ~
import ..Sets: TypeSet
import ..FinSets: FinSet, FinFunction, FinDomFunction, force, predicate
import ..FinCats: components, is_natural
using ...Theories: Category, SchemaDescType, CSetSchemaDescType,
attrtype, attrtype_num, attr, adom, acodom, acodom_nums, roottype
import ...Theories: dom, codom, compose, ⋅, id,
Expand Down Expand Up @@ -261,12 +262,6 @@ function Base.getindex(α::LooseACSetTransformation, c::Symbol)
end
end

""" Is the transformation between attributed C-sets a natural transformation?

This function uses the fact that to check whether a transformation is natural,
it suffices to check the naturality equation on a generating set of morphisms of
the category C.
"""
function is_natural(α::ACSetTransformation{S}) where {S}
X, Y = dom(α), codom(α)
for (f, c, d) in flatten((zip(hom(S), dom(S), codom(S)),
Expand Down
4 changes: 2 additions & 2 deletions src/categorical_algebra/CategoricalAlgebra.jl
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@ include("Sets.jl")
include("FinSets.jl")
include("Matrices.jl")
include("FinRelations.jl")
include("CSets.jl")
include("Categories.jl")
include("FinCats.jl")
include("CSets.jl")
include("GraphCategories.jl")
include("StructuredCospans.jl")
include("CommutativeDiagrams.jl")
Expand All @@ -26,9 +26,9 @@ include("DPO.jl")

@reexport using .Sets
@reexport using .FinSets
@reexport using .CSets
@reexport using .Categories
@reexport using .FinCats
@reexport using .CSets

@reexport using .StructuredCospans
@reexport using .CatElements
Expand Down
36 changes: 35 additions & 1 deletion src/categorical_algebra/Categories.jl
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ instances are supported through the wrapper type [`TypeCat`](@ref). Finitely
presented categories are provided by another module, [`FinCats`](@ref).
"""
module Categories
export Cat, TypeCat, Ob, Functor, dom, codom, compose, id, ob_map, hom_map
export Cat, TypeCat, Ob, Functor, NatTransformation,
dom, codom, compose, id, ob, hom, ob_map, hom_map, dom_ob, codom_ob, component

using ..Sets
import ...Theories: Ob, ob, hom, dom, codom, compose, id
Expand Down Expand Up @@ -96,6 +97,37 @@ Sends a category to its set of objects and a functor to its object map.
"""
function Ob end

""" Abstract base type for a natural transformation between functors.

A natural transformation ``α: F ⇒ G`` has a domain ``F`` and codomain ``G``
([`dom`](@ref) and [`codom`](@ref)), which are functors ``F,G: C → D`` having
the same domain ``C`` and codomain ``D``. The transformation consists of a
component ``αₓ: Fx → Gx`` in ``D`` for each object ``x ∈ C``, accessible using
[`component`](@ref) or indexing notation (`Base.getindex`).
"""
abstract type NatTransformation{C<:Cat,D<:Cat,Dom<:Functor{C,D},Codom<:Functor{C,D}} end

dom(α::NatTransformation) = α.dom
codom(α::NatTransformation) = α.codom

""" Component of natural transformation.
"""
function component end

@inline Base.getindex(α::NatTransformation, c) = component(α, c)

""" Domain object of natural transformation.

Given ``α: F ⇒ G: C → D``, this function returns ``C``.
"""
dom_ob(α::NatTransformation) = dom(dom(α)) # == dom(codom(α))

""" Codomain object of natural transformation.

Given ``α: F ⇒ G: C → D``, this function returns ``D``.
"""
codom_ob(α::NatTransformation) = codom(dom(α)) # == codom(codom(α))

# Instances
###########

Expand All @@ -106,6 +138,8 @@ The Julia types should form an `@instance` of the theory of categories
"""
struct TypeCat{Ob,Hom} <: Cat{Ob,Hom} end

TypeCat(Ob::Type, Hom::Type) = TypeCat{Ob,Hom}()

Ob(::TypeCat{T}) where T = TypeSet{T}()

ob(::TypeCat{Ob,Hom}, x) where {Ob,Hom} = convert(Ob, x)
Expand Down
131 changes: 117 additions & 14 deletions src/categorical_algebra/FinCats.jl
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ and only if the graph is DAG, which is a fairly special condition. This usage of
finitely presented are equivalent.
"""
module FinCats
export FinCat, Path, ob, hom, ob_generators, hom_generators, equations,
is_free, graph, edges, src, tgt, presentation,
export FinCat, Path, ob_generators, hom_generators, equations, is_free,
graph, edges, src, tgt, presentation,
FinFunctor, FinDomFunctor, is_functorial, collect_ob, collect_hom,
Path, graph, edges, src, tgt
FinNatTransformation, components, is_natural

using AutoHashEquals
using Reexport
Expand All @@ -24,11 +24,11 @@ using ...GAT, ...Present, ...Syntax
import ...Present: equations
using ...Theories: Category, ObExpr, HomExpr, roottype
import ...Theories: dom, codom, id, compose, ⋅, ∘
using ...Graphs, ..FreeDiagrams, ..FinSets, ..CSets
using ...CSetDataStructures, ...Graphs, ..FreeDiagrams, ..FinSets
import ...Graphs: edges, src, tgt
import ..FreeDiagrams: FreeDiagram, diagram_type, cone_objects, cocone_objects
import ..Limits: limit, colimit
import ..Categories: Ob, ob, hom, ob_map, hom_map
import ..Categories: Ob, ob, hom, ob_map, hom_map, component

# Categories
############
Expand Down Expand Up @@ -210,14 +210,14 @@ hom(C::FinCatPresentation, fs::AbstractVector) =
# Functors
##########

""" Abstract type for functor out of a finitely presented category.
""" A functor out of a finitely presented category.
"""
abstract type FinDomFunctor{Dom<:FinCat,Codom<:Cat} <: Functor{Dom,Codom} end
const FinDomFunctor{Dom<:FinCat,Codom<:Cat} = Functor{Dom,Codom}

FinDomFunctor(ob_map::Union{AbstractVector{Ob},AbstractDict{<:Any,Ob}},
hom_map::Union{AbstractVector{Hom},AbstractDict{<:Any,Hom}},
dom) where {Ob,Hom} =
FinDomFunctor(ob_map, hom_map, dom, TypeCat{Ob,Hom}())
FinDomFunctor(ob_map, hom_map, dom, TypeCat(Ob,Hom))
FinDomFunctor(maps::NamedTuple{(:V,:E)}, dom::FinCatGraph, codom::Cat) =
FinDomFunctor(maps.V, maps.E, dom, codom)

Expand Down Expand Up @@ -261,7 +261,7 @@ function is_functorial(F::FinDomFunctor)
end
end

""" Abstract type for functor between finitely presented categories.
""" A functor between finitely presented categories.
"""
const FinFunctor{Dom<:FinCat,Codom<:FinCat} = FinDomFunctor{Dom,Codom}

Expand Down Expand Up @@ -318,13 +318,17 @@ end

function FinDomFunctor(ob_map::ObD, hom_map::HomD, dom::FinCat,
codom::Cat) where {ObD<:AbstractDict, HomD<:AbstractDict}
ob_map = (roottype(ObD))(functor_key(dom, k) => ob(codom, v)
for (k, v) in ob_map)
hom_map = (roottype(HomD))(functor_key(dom, k) => hom(codom, v)
for (k, v) in hom_map)
ob_map = (dicttype(ObD))(functor_key(dom, x) => ob(codom, y)
for (x, y) in ob_map)
hom_map = (dicttype(HomD))(functor_key(dom, f) => hom(codom, g)
for (f, g) in hom_map)
FinDomFunctorDict(ob_map, hom_map, dom, codom)
end

# XXX: Is there a less hacky way to get a dictionary constructor?
dicttype(T::Type) = roottype(T)
dicttype(::Type{<:Iterators.Pairs}) = Dict

functor_key(C::FinCat, x) = x
functor_key(C::FinCat, expr::GATExpr) = head(expr) == :generator ?
first(expr) : error("Functor must be defined on generators")
Expand All @@ -340,7 +344,8 @@ hom_map(F::FinDomFunctorDict{Dom,Codom,ObMap,HomMap}, f::Key) where
function FinDomFunctor(pres::Presentation, X::ACSet)
ob_map = Dict(c => FinSet(X, nameof(c)) for c in generators(pres, :Ob))
hom_map = Dict(f => FinFunction(X, nameof(f)) for f in generators(pres, :Hom))
FinDomFunctor(ob_map, hom_map, FinCat(pres))
FinDomFunctor(ob_map, hom_map,
FinCat(pres), TypeCat(FinSet{Int}, FinFunction{Int}))
end

# Free diagram interop
Expand All @@ -363,4 +368,102 @@ end
limit(F::FinDomFunctor) = limit(FreeDiagram(F))
colimit(F::FinDomFunctor) = colimit(FreeDiagram(F))

# Natural transformations
#########################

""" A natural transformation whose domain category is finitely generated.

This type is for natural transformations ``α: F ⇒ G: C → D`` such that the
domain category ``C`` is finitely generated. Such a natural transformation is
given by a finite amount of data (one morphism in ``D`` for each generating
object of ``C``) and its naturality is verified by finitely many equations (one
equation for each generating morphism of ``C``).
"""
const FinNatTransformation{C<:FinCat,D<:Cat,Dom<:FinDomFunctor{C,D},Codom<:FinDomFunctor{C,D}} =
NatTransformation{C,D,Dom,Codom}

FinNatTransformation(F, G; components...) =
FinNatTransformation(components, F, G)

""" Components of a natural transformation.
"""
components(α::FinNatTransformation) = α.components

""" Is the transformation between `FinDomFunctors` a natural transformation?

This function uses the fact that to check whether a transformation is natural,
it suffices to check the naturality equation on a generating set of morphisms of
the domain category.
"""
function is_natural(α::FinNatTransformation)
F, G = dom(α), codom(α)
C, D = dom(F), codom(F) # == dom(G), codom(G)
all(hom_generators(C)) do f
Ff, Gf = hom_map(F,f), hom_map(G,f)
α_c, α_d = α[dom(C,f)], α[codom(C,f)]
compose(D, α_c, Gf) == compose(D, Ff, α_d)
end
end

function check_transformation_domains(F::Functor, G::Functor)
(C = dom(F)) == dom(G) ||
error("Mismatched domains in functors $F and $G")
(D = codom(F)) == codom(G) ||
error("Mismatched codomains in functors $F and $G")
(C, D)
end

# Vector-based transformations
#-----------------------------

""" Natural transformation given explicitly by a vector of morphisms.
"""
@auto_hash_equals struct FinNatTransformationVector{C<:FinCat,D<:Cat,
Dom<:FinDomFunctor{C,D},Codom<:FinDomFunctor{C,D},Comp<:AbstractVector} <:
FinNatTransformation{C,D,Dom,Codom}
components::Comp
dom::Dom
codom::Codom
end

function FinNatTransformation(components::AbstractVector,
F::FinDomFunctor, G::FinDomFunctor)
C, D = check_transformation_domains(F, G)
length(components) == length(ob_generators(C)) ||
error("Incorrect number of components in $components for domain category $C")
FinNatTransformationVector(map(f -> hom(D,f), components), F, G)
end

component(α::FinNatTransformationVector, c::Integer) = α.components[c]

# Dict-based transformations
#---------------------------

""" Natural transformation given explicitly by a dictionary.
"""
@auto_hash_equals struct FinNatTransformationDict{C<:FinCat,D<:Cat,
Dom<:FinDomFunctor{C,D},Codom<:FinDomFunctor{C,D},Comp<:AbstractDict} <:
FinNatTransformation{C,D,Dom,Codom}
components::Comp
dom::Dom
codom::Codom
end

function FinNatTransformation(components::Comp, F::FinDomFunctor,
G::FinDomFunctor) where Comp<:AbstractDict
C, D = check_transformation_domains(F, G)
components = (dicttype(Comp))(transformation_key(C,x) => hom(D,f)
for (x, f) in components)
FinNatTransformationDict(components, F, G)
end

transformation_key(C::FinCat, x) = x
transformation_key(C::FinCat, expr::GATExpr) = head(expr) == :generator ?
first(expr) : error("Natural transformation must be defined on generators")

component(α::FinNatTransformationDict{C,D,F,G,Comp}, c::Key) where
{Key,C,D,F,G,Comp<:AbstractDict{Key}} = α.components[c]
component(α::FinNatTransformationDict, expr::GATExpr) =
component(α, first(expr))

end
4 changes: 2 additions & 2 deletions test/categorical_algebra/Categories.jl
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ using Catlab.CategoricalAlgebra.Sets, Catlab.CategoricalAlgebra.Categories
# Categories from Julia types
#############################

C = TypeCat{FreeCategory.Ob,FreeCategory.Hom}()
@test Ob(C) == TypeSet{FreeCategory.Ob}()
C = TypeCat(FreeCategory.Ob, FreeCategory.Hom)
@test Ob(C) == TypeSet(FreeCategory.Ob)

end
20 changes: 20 additions & 0 deletions test/categorical_algebra/FinCats.jl
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,15 @@ F = FinFunctor([1,3,5], [[1,2],[3,4]], C, D)
@test is_functorial(F)
@test hom_map(F, Path(g, [1,2])) == Path(h, [1,2,3,4])

# Commutative square as natural transformation.
C = FinCat(path_graph(Graph, 2))
F = FinDomFunctor([FinSet(4), FinSet(2)], [FinFunction([1,1,2,2])], C)
α₀, α₁ = FinFunction([3,4,1,2]), FinFunction([2,1])
α = FinNatTransformation([α₀, α₁], F, F)
@test is_natural(α)
@test (α[1], α[2]) == (α₀, α₁)
@test components(α) == [α₀, α₁]

# Free diagrams
#--------------

Expand Down Expand Up @@ -104,6 +113,7 @@ end
@test length(equations(Δ¹)) == 2
@test !is_free(Δ¹)

# Graph as set-valued functor on the theory of graphs.
g = path_graph(Graph, 3)
F = FinDomFunctor(TheoryGraph, g)
C = dom(F)
Expand All @@ -114,4 +124,14 @@ C = dom(F)
@test F(hom(C, :tgt)) == FinFunction([2,3], 3)
@test F(id(ob(C, :E))) == id(FinSet(2))

# Graph homomorphism as natural transformation.
h = path_graph(Graph, 2)
add_edge!(h, 2, 2)
G = FinDomFunctor(TheoryGraph, h)
α = FinNatTransformation(F, G, V=FinFunction([1,2,2]), E=FinFunction([1,2]))
@test dom_ob(α) == C
@test codom_ob(α) isa TypeCat{<:FinSet{Int},<:FinFunction{Int}}
@test is_natural(α)
@test α[:V](3) == 2

end