• A simple, elegant, ab initio first-order presentation of Category Theor

    From rockbrentwood@gmail.com@21:1/5 to All on Tue Jul 18 18:37:18 2017
    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

    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:
    * 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
    * 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

    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).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From rockbrentwood@gmail.com@21:1/5 to All on Fri Aug 11 04:13:14 2017
    On Tuesday, July 18, 2017 at 7:37:23 PM UTC-5, rockbr...@gmail.com
    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.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)