Zulip Chat Archive

Stream: maths

Topic: Comments? Summary of mathlib


view this post on Zulip 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.

The Cap Set Problem <link>

Independence of the Continuum Hypothesis <link>

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Nov 26 2019 at 09:50):

We have tensor products and localisation of rings, right?

view this post on Zulip Kevin Buzzard (Nov 26 2019 at 09:51):

I can move "localisation" to the rings sentence.

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:52):

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

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:52):

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

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:53):

At least no tensor product of algebras.

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:53):

Someone should do extension of scalars (-;

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:53):

Anyway, this list looks pretty good to me.

view this post on Zulip Johan Commelin (Nov 26 2019 at 09:53):

Maybe add monoidal cats to the category theory list

view this post on Zulip Rob Lewis (Nov 26 2019 at 10:02):

p-adic numbers?

view this post on Zulip Rob Lewis (Nov 26 2019 at 10:02):

It looks pretty comprehensive to me.

view this post on Zulip Patrick Massot (Nov 26 2019 at 10:02):

What does "Sum of a GP" means?

view this post on Zulip Johan Commelin (Nov 26 2019 at 10:04):

Ooops... you missed Hensel

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Nov 26 2019 at 10:28):

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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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".

view this post on Zulip Patrick Massot (Nov 26 2019 at 22:22):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 27 2019 at 06:11):

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

view this post on Zulip 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 (-;

view this post on Zulip 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