{
"cells": [
{
"cell_type": "markdown",
"source": [
"# Partitions\n",
"\n",
"\n",
"Partitions are a categorical construction that we derive from sets and functions.\n",
"Given a set A, you can think of all of the ways to partition A into parts.\n",
"These ways of partitioning are isomorphic to equivalence relations R ⊆ A × A."
],
"metadata": {}
},
{
"cell_type": "markdown",
"source": [
"The first step is our Catlab imports"
],
"metadata": {}
},
{
"outputs": [],
"cell_type": "code",
"source": [
"using Core: GeneratedFunctionStub\n",
"using Test\n",
"\n",
"using GATlab, Catlab.Theories, Catlab.CategoricalAlgebra\n",
"import Catlab.Theories: compose\n",
"using DataStructures\n",
"using PrettyTables\n",
"PrettyTables.pretty_table(f::FinFunction, name::Symbol=:f) =\n",
" pretty_table(OrderedDict(:x=>1:length(dom(f)), Symbol(\"$(name)(x)\")=>collect(f)))\n",
"using LaTeXStrings"
],
"metadata": {},
"execution_count": 1
},
{
"cell_type": "markdown",
"source": [
"## FinSet: the category of Finite Sets\n",
"In FinSet the objects are sets n = {1...n} and the morphisms are functions between finite sets.\n",
"You can wrap a plain old Int into a finite set with the FinSet(n::Int) function. These sets will\n",
"serve as the domain and codomains of our functions."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "FinSet(4)"
},
"metadata": {},
"execution_count": 2
}
],
"cell_type": "code",
"source": [
"n = FinSet(3)\n",
"m = FinSet(4)"
],
"metadata": {},
"execution_count": 2
},
{
"cell_type": "markdown",
"source": [
"once you have some sets, you can define functions between them. A FinFunction from n to m, f:n→m, can be specified as\n",
"an array of length n with elements from m."
],
"metadata": {}
},
{
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"┌───────┬───────┐\n",
"│ x │ f(x) │\n",
"│ Int64 │ Int64 │\n",
"├───────┼───────┤\n",
"│ 1 │ 2 │\n",
"│ 2 │ 4 │\n",
"│ 3 │ 3 │\n",
"└───────┴───────┘\n"
]
}
],
"cell_type": "code",
"source": [
"f = FinFunction([2,4,3], n, m)\n",
"\n",
"pretty_table(f)"
],
"metadata": {},
"execution_count": 3
},
{
"cell_type": "markdown",
"source": [
"## Surjective maps\n",
"In order to use a map to represent a partition, we have to make sure that it is surjective.\n",
"Given a FinFunction, we can compute the preimage of any element in its codomain."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "Int64[]"
},
"metadata": {},
"execution_count": 4
}
],
"cell_type": "code",
"source": [
"preimage(f, 2)\n",
"\n",
"preimage(f, 1)"
],
"metadata": {},
"execution_count": 4
},
{
"cell_type": "markdown",
"source": [
"If the preimage is empty, then there is no element in the domain that maps to that element of the codomain.\n",
"This gives us a definition of surjective functions by asserting that all the preimages are nonempty.\n",
"Julia note: !p is the predicate x ↦ ¬p(x), f.(A) applies f to all of the elements in A."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "false"
},
"metadata": {},
"execution_count": 5
}
],
"cell_type": "code",
"source": [
"is_surjective(f::FinFunction) = all((!isempty).(preimage(f,i) for i in codom(f)))\n",
"is_surjective(f)"
],
"metadata": {},
"execution_count": 5
},
{
"cell_type": "markdown",
"source": [
"Our function f, wasn't surjective so it can't be used to induce a partition via its preimages.\n",
"Let's try again,"
],
"metadata": {}
},
{
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"┌───────┬───────┐\n",
"│ x │ g(x) │\n",
"│ Int64 │ Int64 │\n",
"├───────┼───────┤\n",
"│ 1 │ 1 │\n",
"│ 2 │ 2 │\n",
"│ 3 │ 3 │\n",
"│ 4 │ 3 │\n",
"└───────┴───────┘\n"
]
},
{
"output_type": "execute_result",
"data": {
"text/plain": "true"
},
"metadata": {},
"execution_count": 6
}
],
"cell_type": "code",
"source": [
"g = FinFunction([1,2,3,3], m, n)\n",
"pretty_table(g, :g)\n",
"is_surjective(g)"
],
"metadata": {},
"execution_count": 6
},
{
"cell_type": "markdown",
"source": [
"# Refinements of a Partition\n",
"When defining partitions classically as A = ∪ₚ Aₚ with p ≠ r ⟹ Aₚ ≠ Aᵣ,\n",
"it is not immediately obvious how to define comparisons between partitions.\n",
"With the \"a partition of A is a surjective map out of A\" definition, the comparisons\n",
"are obvious. The composition of surjective maps is surjective, so we can define\n",
"the refinement order in terms of a diagram in Set.\n",
"\n",
"You can see a graphical definition in [quiver](https://q.uiver.app/?q=WzAsMyxbMCwwLCJBIl0sWzMsMCwiUSJdLFszLDIsIlAiXSxbMSwyLCJoIiwwLHsic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoiZXBpIn19fV0sWzAsMSwiZiIsMCx7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFswLDIsImciLDIseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJlcGkifX19XV0=)"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "TikzPictures.TikzPicture(\"A &&& Q \\\\\\\\\\n\\\\\\\\\\n&&& P\\n\\\\arrow[\\\"h\\\", two heads, from=1-4, to=3-4]\\n\\\\arrow[\\\"f\\\", two heads, from=1-1, to=1-4]\\n\\\\arrow[\\\"g\\\"', two heads, from=1-1, to=3-4]\", \"\", \"\\\\usepackage{tikz-cd}\\n% contents of quiver.sty\\n% `tikz-cd` is necessary to draw commutative diagrams.\\n\\\\RequirePackage{tikz-cd}\\n% `amssymb` is necessary for `\\\\lrcorner` and `\\\\ulcorner`.\\n\\\\RequirePackage{amssymb}\\n% `calc` is necessary to draw curved arrows.\\n\\\\usetikzlibrary{calc}\\n% `pathmorphing` is necessary to draw squiggly arrows.\\n\\\\usetikzlibrary{decorations.pathmorphing}\\n\\n% A TikZ style for curved arrows of a fixed height, due to AndréC.\\n\\\\tikzset{curve/.style={settings={#1},to path={(\\\\tikztostart)\\n .. controls (\\$(\\\\tikztostart)!\\\\pv{pos}!(\\\\tikztotarget)!\\\\pv{height}!270:(\\\\tikztotarget)\\$)\\n and (\\$(\\\\tikztostart)!1-\\\\pv{pos}!(\\\\tikztotarget)!\\\\pv{height}!270:(\\\\tikztotarget)\\$)\\n .. (\\\\tikztotarget)\\\\tikztonodes}},\\n settings/.code={\\\\tikzset{quiver/.cd,#1}\\n \\\\def\\\\pv##1{\\\\pgfkeysvalueof{/tikz/quiver/##1}}},\\n quiver/.cd,pos/.initial=0.35,height/.initial=0}\\n\\n% TikZ arrowhead/tail styles.\\n\\\\tikzset{tail reversed/.code={\\\\pgfsetarrowsstart{tikzcd to}}}\\n\\\\tikzset{2tail/.code={\\\\pgfsetarrowsstart{Implies[reversed]}}}\\n\\\\tikzset{2tail reversed/.code={\\\\pgfsetarrowsstart{Implies}}}\\n% TikZ arrow styles.\\n\\\\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}\", \"tikzcd\", \"\", \"\", true, true)",
"image/svg+xml": [
"\n",
"\n",
"\n"
]
},
"metadata": {},
"execution_count": 7
}
],
"cell_type": "code",
"source": [
"using TikzCDs\n",
"\n",
"triangle = L\"\"\"\n",
"A &&& Q \\\\\n",
"\\\\\n",
"&&& P\n",
"\\arrow[\"h\", two heads, from=1-4, to=3-4]\n",
"\\arrow[\"f\", two heads, from=1-1, to=1-4]\n",
"\\arrow[\"g\"', two heads, from=1-1, to=3-4]\n",
"\"\"\";\n",
"\n",
"TikzCD(triangle, preamble=TikzCDs.Styles.Quiver)"
],
"metadata": {},
"execution_count": 7
},
{
"cell_type": "markdown",
"source": [
"Let's take a look at an example:"
],
"metadata": {}
},
{
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"┌───────┬──────────┐\n",
"│ x │ (f⋅h)(x) │\n",
"│ Int64 │ Int64 │\n",
"├───────┼──────────┤\n",
"│ 1 │ 1 │\n",
"│ 2 │ 1 │\n",
"│ 3 │ 2 │\n",
"│ 4 │ 2 │\n",
"└───────┴──────────┘\n"
]
},
{
"output_type": "execute_result",
"data": {
"text/plain": "true"
},
"metadata": {},
"execution_count": 8
}
],
"cell_type": "code",
"source": [
"A = FinSet(4)\n",
"Q = FinSet(3)\n",
"P = FinSet(2)\n",
"\n",
"f = FinFunction([1,2,3,3], A, Q)\n",
"g = FinFunction([1,1,2,2], A, P)\n",
"h = FinFunction([1,1,2], Q, P)\n",
"\n",
"@test_throws ErrorException compose(g,h) #Catlab checks the domains match\n",
"\n",
"pretty_table(compose(f,h), Symbol(\"(f⋅h)\"))\n",
"\n",
"compose(f,h) == g"
],
"metadata": {},
"execution_count": 8
},
{
"cell_type": "markdown",
"source": [
"This triangle commutes, so f is a refinement of g equivalently g is coarser than f."
],
"metadata": {}
},
{
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"┌───────┬───────────┐\n",
"│ x │ f⋅h⋅h′(x) │\n",
"│ Int64 │ Int64 │\n",
"├───────┼───────────┤\n",
"│ 1 │ 1 │\n",
"│ 2 │ 1 │\n",
"│ 3 │ 1 │\n",
"│ 4 │ 1 │\n",
"└───────┴───────────┘\n"
]
}
],
"cell_type": "code",
"source": [
"h′ = FinFunction([1,1], P, FinSet(1))\n",
"\n",
"pretty_table(f⋅h⋅h′, Symbol(\"f⋅h⋅h′\"))"
],
"metadata": {},
"execution_count": 9
},
{
"cell_type": "markdown",
"source": [
"### Properties of refinements\n",
"We can show that refinement gives us a preorder on partitions directly from the\n",
"nice properties of surjective maps.\n",
"1. Reflexive: Any partition is a refinement of itself.\n",
"2. Transitive: If f ≤ g ≤ h as partitions, then f ≤ h\n",
"You can read these directly off the definition of refinements as a commutative\n",
"triangle in the category of (Set, Surjections).\n",
"You can edit this diagram in [quiver](https://q.uiver.app/?q=WzAsNCxbMCwwLCJBIl0sWzMsMCwiUSJdLFszLDIsIlAiXSxbMyw0LCJRXlxccHJpbWUiXSxbMSwyLCJoIl0sWzAsMSwiZiIsMCx7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFswLDIsImciLDIseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJlcGkifX19XSxbMiwzLCJoXlxccHJpbWUiXSxbMCwzLCJmXFxjZG90IGhcXGNkb3QgaF5cXHByaW1lID0gZ1xcY2RvdCBoXlxccHJpbWUiLDIseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJlcGkifX19XV0=)"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "TikzPictures.TikzPicture(\"A &&& Q \\\\\\\\\\n\\\\\\\\\\n&&& P \\\\\\\\\\n\\\\\\\\\\n&&& {Q^\\\\prime}\\n\\\\arrow[\\\"h\\\", from=1-4, to=3-4]\\n\\\\arrow[\\\"f\\\", two heads, from=1-1, to=1-4]\\n\\\\arrow[\\\"g\\\"', two heads, from=1-1, to=3-4]\\n\\\\arrow[\\\"{h^\\\\prime}\\\", from=3-4, to=5-4]\\n\\\\arrow[\\\"{f\\\\cdot h\\\\cdot h^\\\\prime = g\\\\cdot h^\\\\prime}\\\"', two heads, from=1-1, to=5-4]\", \"\", \"\\\\usepackage{tikz-cd}\\n% contents of quiver.sty\\n% `tikz-cd` is necessary to draw commutative diagrams.\\n\\\\RequirePackage{tikz-cd}\\n% `amssymb` is necessary for `\\\\lrcorner` and `\\\\ulcorner`.\\n\\\\RequirePackage{amssymb}\\n% `calc` is necessary to draw curved arrows.\\n\\\\usetikzlibrary{calc}\\n% `pathmorphing` is necessary to draw squiggly arrows.\\n\\\\usetikzlibrary{decorations.pathmorphing}\\n\\n% A TikZ style for curved arrows of a fixed height, due to AndréC.\\n\\\\tikzset{curve/.style={settings={#1},to path={(\\\\tikztostart)\\n .. controls (\\$(\\\\tikztostart)!\\\\pv{pos}!(\\\\tikztotarget)!\\\\pv{height}!270:(\\\\tikztotarget)\\$)\\n and (\\$(\\\\tikztostart)!1-\\\\pv{pos}!(\\\\tikztotarget)!\\\\pv{height}!270:(\\\\tikztotarget)\\$)\\n .. (\\\\tikztotarget)\\\\tikztonodes}},\\n settings/.code={\\\\tikzset{quiver/.cd,#1}\\n \\\\def\\\\pv##1{\\\\pgfkeysvalueof{/tikz/quiver/##1}}},\\n quiver/.cd,pos/.initial=0.35,height/.initial=0}\\n\\n% TikZ arrowhead/tail styles.\\n\\\\tikzset{tail reversed/.code={\\\\pgfsetarrowsstart{tikzcd to}}}\\n\\\\tikzset{2tail/.code={\\\\pgfsetarrowsstart{Implies[reversed]}}}\\n\\\\tikzset{2tail reversed/.code={\\\\pgfsetarrowsstart{Implies}}}\\n% TikZ arrow styles.\\n\\\\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}\", \"tikzcd\", \"\", \"\", true, true)",
"image/svg+xml": [
"\n",
"\n",
"\n"
]
},
"metadata": {},
"execution_count": 10
}
],
"cell_type": "code",
"source": [
"refinement = L\"\"\"\n",
"A &&& Q \\\\\n",
"\\\\\n",
"&&& P \\\\\n",
"\\\\\n",
"&&& {Q^\\prime}\n",
"\\arrow[\"h\", from=1-4, to=3-4]\n",
"\\arrow[\"f\", two heads, from=1-1, to=1-4]\n",
"\\arrow[\"g\"', two heads, from=1-1, to=3-4]\n",
"\\arrow[\"{h^\\prime}\", from=3-4, to=5-4]\n",
"\\arrow[\"{f\\cdot h\\cdot h^\\prime = g\\cdot h^\\prime}\"', two heads, from=1-1, to=5-4]\n",
"\"\"\";\n",
"\n",
"TikzCD(refinement, preamble=TikzCDs.Styles.Quiver)"
],
"metadata": {},
"execution_count": 10
}
],
"nbformat_minor": 3,
"metadata": {
"language_info": {
"file_extension": ".jl",
"mimetype": "application/julia",
"name": "julia",
"version": "1.10.2"
},
"kernelspec": {
"name": "julia-1.10",
"display_name": "Julia 1.10.2",
"language": "julia"
}
},
"nbformat": 4
}