[FOM] two interpretations of identity morphisms in category theory
peklund at cs.umu.se
Mon May 1 02:08:24 EDT 2017
We shouldn't speak about 'objectual' and 'algorithmic' interpretations
of the identity morphism.
The foundations of category theory has been debated since its beginning,
and I won't go into detail in this response.
However, through decades there has been discussions about which comes
first, objects or morphisms. Traditionally we train students saying
"these are the objects, and the morhpisms are ...". However, if we look
back e.g. at Ehresmann et co's algebraic view on categories dating back
to the 1950s, there are notions of identities where seemingly morphisms
precede objects. It appears implicitly in Menger's paper's from that
time, so even Newton had some intuition of "identity" which is not
overwritten today in any way, I would say.
Paul Hollander appears to include "the logic of it" aspects to morphisms
and objects, but it is important to note that we shouldn't neglect any
of algebra, logic and topology influences to category theory.
On algebraic aspects, note e.g. how we have algebras and co-algebras,
where the former is closer to dealing with Eilenberg-Moore categories of
monads, whereas co-algebras go in direction of substitutions and Kleisli
categories. An interesting thing is also if algebraic structure (in
category theory) resides in objects or in morphisms. It may even be seen
as a matter of choice, which we can see e.g. with playing just with
categories of relations, which can be defined algebraically and
co-algebraically. An additional algebraic abstraction enters the scene
in monoidal categories. Here we should note that there is no notion of a
free monoidal category (there are 'free categories', but that's another
thing), so "categorical algebra" is not subsumed by "universal algebra".
Logic aspects of catagories are many. There is the "fons-et-origo" logic
intertwined with set theory which appears in the metalanguage of
categories. We have toposes and internal logic, and we have categories
of logics in the style of institutions (Goguen-Burstall) and entailment
systems (Meseguer). The latter can be generalized as can be seen under
Topologies seem a b it far fetched but to me an important question is
related to "structure or space?". If we again use monads as examples, we
have coarse structures starting from adding stuff to relations. The
Kleisli category of the powerset monad is one of the to relational
categories (in some sense the "wrong one" since it emphasizes
substitution in the morphism rather than in the object), and the
Eilenberg-Moore category of the powerset monad is (isomorphic to) the
category of complete lattices and join-preserving maps. This intuitively
shows that as we add more structure to the functor in that monad, we
also add more algebraic structure to the corresponding Eilenberg-Moore
category. What is interesting is the folklore "algebra and topology
meet" in the case of the ultrafilter monad. The "algebraic structure" of
its Eilenberg-Moore category is compact Hausdorff spaces.
So, adding stuff to (algebraic) structure is not the same as adding
stuff to (topological) space. Here we might then wonder is a logic is a
structure or a space. I personally tend to see it more as a space than
many others do, but I wouldn't say "logic is all about space".
My remarks above may underline that we shouldn't separate algebra, logic
and topology from each other, and definitely not without justification
say that one is more foundational than the other.
What I would like to say also is that we mustn't forget "old papers and
writings". If we rely too much on papers and books no more than a couple
of decades old, we probably lose lots of stories.
FOM is very fascinating!
We are living interesting times!
On 2017-04-29 22:22, Paul Hollander wrote:
> In category theory, the identity morphism 1x:x → x is ambiguous as
> between an objectual interpretation and an algorithmic interpretation.
> Objectually, '1x:x → x' refers to the morphism 1x such that 'x = x' is
> Algorithmically, '1x:x → x' encodes the algorithm by which premiss |-
> (x = x) implies conclusion |- (x = x).
More information about the FOM