-
a [[class]]
- on [[2021-05-30]]
Idea of what [[category theory]] is. Basic definition of mathematical concepts.
Notions that are important in category theory. Commutative diagrams; categories as kinds of [[context]]. At the end, how this fits in a bigger picture.
Aside: I'm reading Feynman and this fits in amazingly well with the introduction of that book, six easy pieces.
An [[elegant framework]] for reasoning about situations where we are composing stuff together. [[modeling]], [[computation]].
Category theory is about [[composing stuff]] together.
Example: composing [[journeys]].
Example: composing processes. Mathematical functions, algorithms, physical processes.
Notation: boxes instead of arrows. Directionality is from left to right.
The output of the first box is the same [[type]] as the input of the second.
You can also compose physical components, of course.
And physical processes.
The fundamental example is mathematical; composing functions as sets.
Aside: we should put this on youtube.
We'll be used 'then' notations for compositions, not traditional.
We'll relate [[objects]]. The things doing the relating are [[morphisms]].
(here there should be a better screenshot, I couldn't get it on time)
Each morphism has a [[source]] and a [[target]].
We can compose morphisms when the target of the first matches the source of the second.
Common feature of all examples: they are [[associative]]. The order of composition doesn't matter; the order of application may. (check)
This was [[true]] for all the examples we looked at so far.
Associativity means that brackets are not needed.
Aside: going from a class in real time to screenshots is one morphism; going from screenshots to notes is another. Going from notes to a chapter or blog post is another.
Associativiy in plugs:
Identity morphisms: morphisms that do nothing. Like a zero in addition.
Identity morphism for functions: the identity function.
A converter that converts to the same electrical standard is just an extension that can become a converter of any type with one additional composition.
[[identity journeys]] (aside: I call these [[excursions]])
Mathematical notion of a category
Aside: I think most concepts had been introduced before except one?
"F is a morphism from X to Y":
Identity morphisms:
Composition:
Unitality: identity "works" (I think this was the concept I thought hadn't been defined previously):
The [[category of sets and functions]] plays a central role in category:
The [[category of plugs and chords]]:
The [[category of journeys]]:
(Aside: some screenshots might be duplicate, they are likely from two moments that felt significant)
Any directed graph generates a category.
(Aside: a directed graph generates dependency trees.)
But categories are [[richer]] than [[directed graphs]], so they aren't used that much as such.
Category theory is interested in [[relations between morphisms]].
if f;g is equal to h, this diagram [[commutes]].
Aside: when you say 'if you compose' something, it'd be nice to have the right notation for the composition on screen.
Sameness: [[isomorphism]]. Identity is equal to roundtrip.
(in the category of sets/functions, an isomorphism is equivalent to a [[bijection]]. in the category of topological spaces and continuous maps, it is a [[homeomorphism]])
A context.
(Aside: I needed more time in this slide).
Contexts leads to [[universal constructions]] and [[universal properties]].
Example: [[categorical product]].
You start with objects, no morphisms. From the left diagram, you construct one with [[morphisms]]. In this one, we generalize cartesian product.
[[pushouts]] Using the information given by f and g, you [[integrate]] two objects (check).
Additional structures: [[monoidal products]]. A way to compose objects and morphisms "in parallel".
(Aside: it would be nice to have original and post application of composition side by side or top to bottom).
(Aside: missing screenshot here, find in Pictures)
- public document at doc.anagora.org/category-theory-basics
- video call at meet.jit.si/category-theory-basics
2021 05 30
associative
bijection
categorical product
category of journeys
category of plugs and chords
category of sets and functions
category theory
class
commutative diagrams
commutes
composing stuff
computation
context
directed graphs
elegant framework
excursions
homeomorphism
identity journeys
integrate
isomorphism
journeys
modeling
monoidal products
morphisms
objects
pasted image 20210530135545 png
pasted image 20210530135718 png
pasted image 20210530135755 png
pasted image 20210530135825 png
pasted image 20210530135906 png
pasted image 20210530135937 png
pasted image 20210530140048 png
pasted image 20210530140116 png
pasted image 20210530140203 png
pasted image 20210530140223 png
pasted image 20210530140255 png
pasted image 20210530140312 png
pasted image 20210530140330 png
pasted image 20210530140421 png
pasted image 20210530140543 png
pasted image 20210530140623 png
pasted image 20210530140657 png
pasted image 20210530140711 png
pasted image 20210530140748 png
pasted image 20210530140849 png
pasted image 20210530140955 png
pasted image 20210530141056 png
pasted image 20210530141124 png
pasted image 20210530141159 png
pasted image 20210530141245 png
pasted image 20210530141302 png
pasted image 20210530141330 png
pasted image 20210530141404 png
pasted image 20210530141427 png
pasted image 20210530141507 png
pasted image 20210530141542 png
pasted image 20210530141611 png
pasted image 20210530141716 png
pasted image 20210530141809 png
pasted image 20210530141831 png
pasted image 20210530141857 png
pasted image 20210530141942 png
pasted image 20210530141956 png
pasted image 20210530142018 png
pasted image 20210530142110 png
pasted image 20210530142206 png
pasted image 20210530142319 png
pasted image 20210530142330 png
pasted image 20210530142425 png
pasted image 20210530142541 png
pushouts
relations between morphisms
richer
source
target
true
type
universal constructions
universal properties