A simple, elegant, ab initio first-order presentation of Category Theory?

[rockbr...@gmail.com]

I was looking for different ways to do Category Theory free of
set-theory in purely first-order form, so as to also lead quickly (in
one fell swoop, as it were) to all the finite presentations and a
formal treatment of such things as diagrams and commutative diagrams to
boot. There actually is a mathematical concept ready made for this -- a
'category without the identities'; a.k.a. a Quiver. But first things
first.

The formalization, then the narrative that leads up to it and beyond:

Definition: A category X = (A, B, C) is an algebra consisting of two
unary operators A, B and a PARTIAL binary operator C such that:
* Rules of Infrastructure:
- AAf = Af = BAf and ABf = Bf = BBf
- Af = Bg -> AC(f,g) = Ag and BC(f,g) = Bf
* Algebraic Rules:
- C(f,Af) = f = C(Bf,f)
- Af = Bg and Ag = Bh -> C(f,C(g,h)) = C(C(f,g),h)

The definition for a functor then reduces to the following form:
Definition: A functor F: X -> X' between categories X = (A, B, C) and
X' = (A', B', C') is a map between its morphisms satisfying:
* FAf = A'Ff, FBf = B'Ff, FC(f,g) = C'(Ff,Fg).

And now, the longer narrative treatment:

Category theory is normally presented in a way that makes informal use
of sets and set theory, like so:

Definition: A category X consists of:
* a set |X| of OBJECTS, and
* for any two objects, A, B in |X|, a set X(A, B) of MORPHISMS,
with each f in X(A, B) depicted an an arrow f: A -> B when X is
understood from context. It is assumed that:
* Rules of Infrastructure:
- Each object A in |X| is associated with
an IDENTITY morphism 1_A: A -> A
- Every two morphisms f: B -> C, g: A -> B yield
a COMPOSITION morphism f o g: A -> C
such that
* Algebraic Rules:
- For all morphisms f: A -> B; f o 1_A = f = 1_B o f
- For all morphisms
f: C -> D, g: B -> C, h: A -> B;
f o (g o h) = (f o g) o h.
Definition: A FUNCTOR F: X -> Y between categories X and Y consists of:
* a map F: |X| -> |Y| between its objects, and
* for any two objects A, B in |X|, a map F: X(A, B) -> Y(A, B)
that maps each arrow f: A -> B in X to an arrow
Ff: FA -> FB in Y.
such that
* for all objects A in |X|: F 1_A = 1_{FA}
* for all morphisms f: B -> C, g: A -> B in X:
F(f o g) = Ff o Fg.

Since category theory is often used as an alternate foundation for
mathematics itself, in place of set theory, and (just as importantly)
since it is used on collections that are too large to be formalised
within set theory, the question naturally arises whether and how it can
be defined and axiomatized in a way that removes all references to sets
and (even better) whether it can be formalized a purely algebraic
theory; i.e. within first-order logic.

To simplify the presentation, one expedient that is frequently adopted
is to reduce the language from two-sorted form (with objects and
morphisms as the sorts) to just one with just one sort (morphisms
alone) by eliminating all references to objects! This can be done
because the objects are already reflected by the identity morphisms: A
<-> 1_A.

This removes the need to mention |X|.

The second expedient is to remove the need to mention X(A, B) and the
arrows f: A -> B themselves by DEFINING:
- The source "object": Af = 1_A
- The destination "object": Bf = 1_B.
and to define the composition operator
- C(f, g) = f o g: A -> C, where f: B -> C and g: A -> B (i.e.
where Af = B = Bg).
With these fixes, one may adopt the following axiomatization:

Finally, to recover the notion of OBJECT we can then establish the
following results as theorems:
Theorem:
* If Ag = f then C(g,f) = g
* If Bg = f then C(f,g) = g
* If Ag = f or Bg = f then Af = f = Bf
* Af = f if and only if Bf = f
Proof:
* Assume Ag = f. Then C(g,f) = C(g,Ag) = g;
and Af = AAg = Ag = f, Bf = BAg = Ag = f.
* Assume Bg = f. Then C(f,g) = C(Bg,g) = g;
and Af = ABg = Bg = f, Bf = BBg = Bg = f.
* If Af = f or Bf = f, use the third property,
with g replaced by f, to get Af = f = Bf.
Definition: A morphism f for which Af = f or Bf = f is an IDENTITY;
i.e. an OBJECT.

This accomplishes the main goal, except for the issue of C only being a
partial operator.

In formal logic, operators are normally taken to be TOTAL, rather than
PARTIAL. To each operator o(a,...,b) is associated a predicate
O(a,...,b,c) such that:
c = o(a,...,b) <-> O(a,...,b,c).
And for o(a,...,b) to be defined, one needs the PRECONDITION:
there is at least one c such that O(a,...,b,c),
with O(a,...,b,o(a,...,b)) automatically holding true. In other words:
when operators are present, the language is Sapir-Worf'ed by having
these preconditions slipped in under the cover.

For a partial operator, the precondition is not always true, so one can
only state:
(there is at least one c such that O(a,...,b,c))
<-> O(a,...,b,o(a,...,b)) <-> o(a,...,b) is defined.
Without the ability to use partial operators in the formal treatment,
one would have to replace all partial operators by their predicates and
to condition all statements that make reference to partial operators by
those predicates.

Here, that would lead to alternate formulation, where h = C(f,g) is
replaced by the predicate C(f,g,h):
* Rules of Infrastructure:
- AAf = Af = BAf and ABf = Bf = BBf
- Af = Bg and C(f,g,h) -> Ah = Ag and Bh = Bf
* Algebraic Rules:
- C(f,Af,f) and C(Bf,f,f)
- Af = Bg, Ag = Bh,
C(f,g,k), C(g,h,l), C(f,l,m), C(k,h,n) -> m = n.
The corresponding precondition for the operator C(f,g) is:
(there is at least one h such that C(f,g,h)) <-> Af = Bg.

For expediency it is preferrable to change the rules of logic, itself,
to allow for formal systems with partial operators and to always remain
mindful of the issue of preconditions by understanding that all
statements involving such operators are tacitly premised on whatever
preconditions are required to make those operators meaningful.

This is the approach that has already been adopted by those doing
category theory.

Example: The "object" category 1.
All objects yield 1-element subcategories: o.
Each object is a 1-element subcategory 1 that consists solely of one
morphism o that satisfies:
* Ao = o = Bo, C(o,o) = o.
The functors F: 1 -> X to a category X are in one-to-one correspondence
with the objects of X.

Example: The "morphism" category 2.
All morphisms yield 3-element subcategories: c: a -> b.
Each morphism is a 2-element subcategory that consists of morphisms
(a,b,c) that satisfy:
* Aa = a = Ba = Ac, C(a,a) = a
* Ab = b = Bb = Bc, C(b,b) = b
* C(c,a) = c = C(b,c)
with C remaining undefined in all other cases. The functors F: 2 -> X
to a category X are in one-to-one correspondence with the morphisms of
X.

Example: Categories generated by a quiver.
Definition: A "quiver" Q is a labeled graph where two or more arrows
(each with different labels) may pass between any two nodes. This also
happens to be the actual infrastructure that is used in most
presentations of Category Theory, so we can repeat the key elements
here in this definition:
* Associated with Q is a set |Q| of nodes
* For any two nodes m, n in |Q| is a set Q(m,n) of arrows,
with a in Q(m,n) depicted as a: m -> n.

Definition: Associated with each quiver Q is the PATH CATEGORY Q*;
which is the category freely generated from Q as follows:
* for each m in |Q|: A(m) = m = B(m) and C(m, m) = m,
* for each m_0,...,m_K in |Q|
and arrows a_0: m_0 -> m_1, ..., a_{K-1}: m_{K-1} -> m_K:
- a_{K-1} ... a_0; with
A(a_{K-1} ... a_0) = m_0 and B(a_{K-1} ... a_0) = m_K,
- C(a_{K-1} ... a_0, m_0)
= a_{K-1} ... a_0
= C(m_K, a_{K-1} ... a_0).
- for each L in K:
C(a_{K-1} ... a_L, a_{L-1} ... a_0)
= a_{K-1} ... a_0.
The length-0 paths are treated the same as the nodes in Q, while the
paths of lengths 1, 2 and more are sequences of arrows in Q where the
tail of each arrow is connected to the head of the next.

This gives us the ability to handle the question of all small
presentable categories in one fell swoop. In particular, the category 1
is given simply as a node, while 2 is given as a single arrow
connecting two nodes.

Definition: A category X is FINITELY PRESENTED if it is the image under
a functor F: Q* -> X, for some finite quiver Q.

For all such categories X, where such a functor F: Q* -> X is given, we
may define the relation
rho(F) = { (a,b) in Q* x Q*: Fa = Fb }.
The category X, itself, may thus be defined by the presentation:
X = Q*/rho
where rho is any set of identities in Q* that generates rho(F). If rho
can be made finite, the category may then be said to be given by a
finitely related finite presentation.

This is enough to recover the notion of categories or subcategories
presented by a COMMUTATIVE DIAGRAM. Such a diagram is, itself, a quiver
in which some of its arrows are labelled, where it is understood that
all paths leading between any two nodes yield the same morphism (i.e,
they "commute").

Definition: The category CD(Q) generated from a quiver Q, regarded as a
commutative diagram, consists of:
* for each m in |Q|: A(m) = m = B(m) and C(m, m) = m.
* for each m, n in |Q|, where m != n
with at least one path connecting m to n
in Q*: A((m,n)) = m, B((m,n)) = n.
* C(n,(m,n)) = m = C((m,n), m),
m is connected to n by at least one path in Q*.
* C((n,p),(m,n)) = C(m,p),
if m is connected to n and n to p each
by at least one path in Q*.
As a category, CD(Q) = Q*/rho, where rho = { (f,g) in Q* x Q*: Af = Ag,
Bf = Bg }.

Finally, in the coup de grace, categories themselves may all be
collected into a category (the "category of all categories") in which
the functors, themselves, play the role of morphisms (and the
categories, themselves, the objects).

[rockbr...@gmail.com]

On Tuesday, July 18, 2017 at 7:37:23 PM UTC-5, rockbr...@gmail.com
wrote:

> I was looking for different ways to do Category Theory free of

> set-theory in purely first-order form...
...

> Definition: A category X = (A, B, C) is an algebra consisting of two
> unary operators A, B and a PARTIAL binary operator C such that:
> *  Rules of Infrastructure:
>   -  AAf = Af = BAf and ABf = Bf = BBf
>   -  Af = Bg -> AC(f,g) = Ag and BC(f,g) = Bf
> *  Algebraic Rules:
>   -  C(f,Af) = f = C(Bf,f)
>   -  Af = Bg and Ag = Bh -> C(f,C(g,h)) = C(C(f,g),h)

This should also include explicit axioms on the domains
* For each f, Af and Bf are defined.
* For each f, g if Af = Bg, then C(f, g) is defined.