Comments? Summary of mathlib

Stream: maths

[Kevin Buzzard]

I just spent an hour proudly looking through the mathlib github repo and summarising the stuff that is there which a mathematician would recognise and think of as "standard" or "important" or whatever. The style of my summary is very much the same style as the course summaries for the courses I attended as an undergraduate. I completely skip all the foundational stuff (e.g. no mathematician wants to hear that we have finset and fintype and finsupp, they won't even understand what that means, these are just "obvious", and they also don't want to know about conditionally complete lattices or monoids because they don't understand their importance). The big question: did I miss anything which a mathematician would find "standard" or "important" or whatever, and which is not trivially implied by things I already wrote?

Algebra:
Groups. Subgroups, quotients, cosets, centralizers, free groups, abelianisation, Sylow 1.
Rings. primes and irreducibles, characteristic of a ring, ideals, fields, Euclidean domains, principal ideal domains, unique factorization domains, Noetherian rings. Ordered rings and fields. Polynomials and power series.
Modules over a ring, direct sums and limits, tensor products, localisation.
Lie algebras (definition and basic properties).
Fields: minimal polynomials, finite extensions, algebraic extensions, splitting fields, perfect closure, finite fields.
Vector spaces, bases, finite-dimensional spaces, matrices, linear maps, dual spaces, bilinear and sesquilinear forms.

Number theory:
The naturals, the integers, the rationals. Primes, uniqueness of factorization. GCDs. Congruences and modular arithmetic. Z is an ED/PID/UFD. Sums of two and four squares, Pell's equation in cases needed for Matiyasevich's theorem (d=a^2-1). Euler's Totient function. Quadratic reciprocity.

Topology:
Metric spaces. Cauchy sequences, Hausdorff distance and Gromov-Hausdorff distance. Completions. Lipschitz continuous functions.
Uniform spaces, uniform continuity, completions.
Topological spaces, open and closed sets, compact sets, continuous maps, homeomorphisms, the compact-open topology. Stone-Cech compactification. Topological fibre bundles.
Presheaves on a topological space, stalks.

Analysis:
The reals and complex numbers.
Basic theory of differentiation of functions of one variable: chain rule, product rule, mean value theorem, C^n and C^infty functions.
Sups and Infs. Sequences and sums. Sum of a GP, exp and log, trig and inverse trig functions, basic properties. Pi.
The complex numbers are algebraically closed.
Definition of real manifold, manifolds with corners.

Measure theory:
Sigma algebras, measure spaces, Borel measurable functions, probability spaces, the Lebesgue integral, L^1 spaces, the Bochner integral, the Giry monad (i.e. measures on a measurable space form a measurable space).

Category theory:
Categories, small and large categories.
Functors, full and faithful functors, natural transformations, the Yoneda lemma. Equivalence of categories, sums, products, limits, adjoints.
The category of commutative rings, the category of modules over a ring, the category of measurable spaces.

Other:
Continued fractions. Turing machines, the Halting problem. Ordinals and Cardinals, Conway games. The Fibonacci sequence. The hyperreals. Cubing a cube.

---

Written in Lean but not (yet?) in Lean's maths library:

Sheaves of rings on a topological spaces, affine schemes, schemes.

Valuations, continuous valuations on a topological ring, Huber rings,
Tate rings, adic spaces, perfectoid spaces.

The Cap Set Problem <link>

Independence of the Continuum Hypothesis <link>

[Johan Commelin]

Modules over a ring, direct sums and limits, tensor products, localisation.

Do we have localisation of modules? I thought only of rings...

[Kevin Buzzard]

We have tensor products and localisation of rings, right?

[Kevin Buzzard]

I can move "localisation" to the rings sentence.

[Johan Commelin]

I think it would (currently) make sense to move it there

[Johan Commelin]

We only have tensor products of modules, not of rings, as far as I know

[Johan Commelin]

At least no tensor product of algebras.

[Johan Commelin]

Someone should do extension of scalars (-;

[Johan Commelin]

Anyway, this list looks pretty good to me.

[Johan Commelin]

Maybe add monoidal cats to the category theory list

[Rob Lewis]

p-adic numbers?

[Rob Lewis]

It looks pretty comprehensive to me.

[Patrick Massot]

What does "Sum of a GP" means?

[Johan Commelin]

Ooops... you missed Hensel

[Sebastien Gouezel]

You mention differentiation of functions in one variable, but we also do several variables, so it is really one or several variables.

[Sebastien Gouezel]

connectedness. Baire theorem. Normed vector spaces and operator norm.

[Patrick Massot]

Kevin, did you read https://github.com/leanprover-community/mathlib/blob/master/docs/theories/topology.md#file-organization while writing this list? There may be a couple more items hidden there.

[Kevin Buzzard]

I didn't read anything -- thanks for these. I knew I would have missed several things. I just had a free hour and thought "I'm going to glance at every file"

[Kevin Buzzard]

Ooops... you missed Hensel

I am kind of stunned I missed p-adics and Hensel because in real life they're some of my favourite things, so I went back to find what I did wrong, and it was that I only glanced at src/data and decided that everything there looked too trivial to mention ;-) I remember distinctly looking at pnat and thinking "nope".

[Patrick Massot]

That data folder will remain a mystery to us, forever.

[David Michael Roberts]

What version of Hensel? The one in Bourbaki? Or just the one for the p-adics?

[Johan Commelin]

We only have the p-adics, hence...

[Johan Commelin]

Well, actually, by now we have local_ring and topological_space and topological_ring and complete_space, so someone can do the more general version (-;

[Johan Commelin]

I think I even saw a branch hensel-ring flying around github