# Misha Gavrilovich: Lifting properties as instances of negation. Diagram chasing computations in point-set topology.

## all works on this page are dedicated to the blessed memory of Grigori Mints. We discussed them at an early stage, and he encouraged me to write them down....

oooooooooo

### A naive diagram-chasing approach to formalisation of tame topology. (2018)

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 diagram-chasing approach to the formalisation and foundations of tame topology.

### Point set topology as diagram chasing computations. Lifting properties as instances of negation. (2014)

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 real-valued 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 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.

### The unreasonable power of the lifting property in elementary mathematics. (2017)

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, torsion-free, p-groups, and prime-to-p 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).

### Topological and metric spaces as full subcategories of the category of simplicial objects of the category of filters. (2018)

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 quasi-geodesic 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.

### Point set topology as diagram chasing computations.

21 page. A draft. Out of date. 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.

• 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 p-group, 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 Feit-Thompson theorem with diagrams in the category of finite groups. same in djvu, We reformulate the statement of the Feit-Thompson 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 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.

• 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 real-valued 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 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.

• Point-set topology as diagram chasing computations. same in djvu, 21 page. A draft of a research proposal. Abstract:

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 mo at sdf dot org