## Stream: maths

### Topic: Comments? Summary of mathlib

#### Kevin Buzzard (Nov 26 2019 at 09:48):

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.

Independence of the Continuum Hypothesis <link>

#### Johan Commelin (Nov 26 2019 at 09:50):

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

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

#### Kevin Buzzard (Nov 26 2019 at 09:50):

We have tensor products and localisation of rings, right?

#### Kevin Buzzard (Nov 26 2019 at 09:51):

I can move "localisation" to the rings sentence.

#### Johan Commelin (Nov 26 2019 at 09:52):

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

#### Johan Commelin (Nov 26 2019 at 09:52):

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

#### Johan Commelin (Nov 26 2019 at 09:53):

At least no tensor product of algebras.

#### Johan Commelin (Nov 26 2019 at 09:53):

Someone should do extension of scalars (-;

#### Johan Commelin (Nov 26 2019 at 09:53):

Anyway, this list looks pretty good to me.

#### Johan Commelin (Nov 26 2019 at 09:53):

Maybe add monoidal cats to the category theory list

#### Rob Lewis (Nov 26 2019 at 10:02):

It looks pretty comprehensive to me.

#### Patrick Massot (Nov 26 2019 at 10:02):

What does "Sum of a GP" means?

#### Johan Commelin (Nov 26 2019 at 10:04):

Ooops... you missed Hensel

#### Sebastien Gouezel (Nov 26 2019 at 10:06):

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

#### Sebastien Gouezel (Nov 26 2019 at 10:28):

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

#### Patrick Massot (Nov 26 2019 at 10:34):

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 (Nov 26 2019 at 12:56):

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 (Nov 26 2019 at 22:06):

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 (Nov 26 2019 at 22:22):

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

#### David Michael Roberts (Nov 27 2019 at 05:53):

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

#### Johan Commelin (Nov 27 2019 at 06:11):

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

#### Johan Commelin (Nov 27 2019 at 06:12):

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 (Nov 27 2019 at 06:17):

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

Last updated: May 12 2021 at 08:14 UTC