oooooooooo
As a tex or
djvu file.
A draft of a research proposal. We translate excerpts of (Bourbaki, General Topology) into diagram chasing arguments,
and speculate it might lead to a naive diagramchasing approach to the formalisation and foundations of tame topology.
We observe that some natural mathematical definitions are lifting properties
relative to simplest counterexamples, namely the definitions of surjectivity and injectivity of maps,
as well as of being connected, separation axioms T0 and T1 in topology,
having dense image, induced (pullback) topology, and every realvalued function being bounded (on a connected domain).
We try to suggest a way to read off these lifting properties from the text of the usual definitions.
We also offer a couple of brief speculations on cognitive and AI aspects of this observation,
particularly that in pointset topology some arguments read as diagram chasing computations
with finite preorders.
An updated version
with new examples in group theoryabelian, perfect, pgroups,
groups of order prime to p, soluble (in finite groups), and FeitThompson theorem reformulated
in terms of lifting properties.
We illustrate the generative power of the lifting property as a means of
defining natural elementary mathematical concepts by giving a number of examples in
various categories, in particular showing that many standard elementary notions
of abstract topology can be defined by applying the lifting property to simple
morphisms of finite topological spaces.
Examples in topology include the notions of: compact, discrete, connected, and
totally disconnected spaces, dense image, induced topology, and separation axioms.
Examples in algebra include: finite groups being
nilpotent, solvable, torsionfree, pgroups, and primetop groups;
injective and projective
modules; injective, surjective,
and split homomorphisms.
We include some speculations on the
wider significance of this, particularly in formalisation of mathematics. A draft. As a text file (more convenient for some readers).
As a tex file.
A draft of a research proposal. Not proofread yet.
We
define fully faithful embeddings of the category of topological spaces and
that of uniform spaces into the category of simplicial objects of the category of filters,
and, based on this, use these two functors to reformulate several elementary notions
including that of being compact, complete, a Cauchy sequence, and equicontinuity.
We also define of quasigeodesic metric spaces with large scale Lipschitz maps,
or rather coarse spaces,
into the category of simplicial objects of a category of filters with another kind of morphisms.
21 page. A draft. Out of date. We give several examples of properties in pointset topology, such as being Hausdorff or that equalizier {x:f(x)=g(x)}
is
being closed for maps to a Hausdorff space,
that translate to diagram chasing rules, and where the lifting property
is
a "category theory negation".
We suggest this observation can be implemented in a problem solver of a kind suggested by M. Ganesalingam and T. Gowers.
This is a preliminary publication.
Fill free to leave a comment here

Tame topology: a naive elementary approach via finite topological spaces. An unproofread draft.
We observe that several elementary properties can be defined
starting from a single morphism by
iterating the Quillen lifting property and restricting to size at most 4.
This includes the properties of a topological space being compact or being discrete,
the separation axioms, a finite group being solvable, a pgroup, a group of order prime to p.
Help in proofreading much appreciated.
 Separation axioms as Quillen lifting properties,
a modified wikipedia page
 Expressing the statement of the FeitThompson theorem
with diagrams in the category of finite groups.
same in djvu,
We reformulate the statement of the FeitThompson theorem
in terms of diagrams in the category of finite groups,
namely iterations of the Quillen lifting property
with respect to particular morphisms.

Elementary general topology as diagram chasing calculations with
finite categories.
same in djvu,
We observe that elementary general topology arguments can be seen
as diagram chasing computations with finite categories,
via a straightforward, naive translation which often involves the
Quillen lifting property
playing the role of negation.
This paper is a draft of a research proposal: we argue
it is worthwhile to
to try to see whether these observations lead to
another axiomatisation of topology and a proof system
amenable to automatic theorem proving.
Help in proofreading much appreciated.

An example of a lifting property,
slides. We explain how an example of a proof in (Ganesalingam, Gowers, {\em A fully
automatic problem solver with humanstyle output} is a sequence of
applications of a single diagram chasing rule, the lifting property.
Their example is: a closed subset of a complete metric space is complete.

Point set topology as diagram chasing computations. Lifting properties as instances of negation.
Older versions:
Point set topology as diagram chasing computations. Lifting properties as instances of negation.
same in djvu, as published in De Morgan Gazette. 8p.
An updated version, 14pp.
Abstract:
We observe that some natural mathematical definitions are lifting properties
relative to simplest counterexamples, namely the definitions of surjectivity and injectivity of maps,
as well as of being connected, separation axioms T0 and T1 in topology,
having dense image, induced (pullback) topology, and every realvalued function being bounded (on a connected domain).
We try to suggest a way to read off these lifting properties from the text of the usual definitions.
We also offer a couple of brief speculations on cognitive and AI aspects of this observation,
particularly that in pointset topology some arguments read as diagram chasing computations
with finite preorders.
An updated version
with new examples in group theoryabelian, perfect, pgroups,
groups of order prime to p, soluble (in finite groups), and FeitThompson theorem reformulated
in terms of lifting properties.
This paper was written for De Morgan Gazette.
 Pointset topology as diagram chasing computations.
same in djvu,
21 page. A draft of a research proposal. Abstract:
We give several examples of properties in pointset topology, such as being Hausdorff or that equalizier {x:f(x)=g(x)}
is
being closed for maps to a Hausdorff space,
that translate to diagram chasing rules, and where the lifting property
is
a "category theory negation".
We suggest this observation can be implemented in a problem solver of a kind suggested by M. Ganesalingam and T. Gowers.
This is a preliminary publication.
I shall be updating this page with (extract of) any related correspondence and keep here a list of references.
Mail me at mo at sdf dot org