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 human-style 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.
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 T
We also offer a couple of brief speculations on cognitive and AI aspects of this observation, particularly that in point-set topology some arguments read as diagram chasing computations with finite preorders.
An updated version with new examples in group theory--abelian, perfect, p-groups, groups of order prime to p, soluble (in finite groups), and Feit-Thompson theorem reformulated in terms of lifting properties. This paper was written for De Morgan Gazette.
We give several examples of properties in point-set 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 m