updating beginner material

Stream: general

[Rob Lewis]

I hear there's another Quanta article coming out soon about mathlib(? Lean? ITP? I don't know the scope) that we should be prepared for. The IMO article this week already brought a bit of a spike in Zulip activity.

In particular we should make sure things like the overview and undergrad pages are up to date. https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml https://github.com/leanprover-community/mathlib/blob/master/docs/overview.yaml

[Johan Commelin]

Is https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L55 (minpoly of a matrix) now done? @Aaron Anderson

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L96 (complex roots of unity), @Patrick Massot what do you want here? We have nth_roots (1 : complex). If we link this up with e ^ (2 * pi * I / n), that should be enough, I guess?

[Rob Lewis]

What does examples of groups with small cardinality refer to?

[Johan Commelin]

@Chris Hughes Do we have more on perm (decomposition into transpositions/disjoint cycles)? What happened to the alternating group? https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L98-L103

[Patrick Massot]

Who knows? Probably things like listing all groups with cardinal less than 20 or so.

[Kevin Buzzard]

Rob Lewis said:

What does examples of groups with small cardinality refer to?

At Imperial this means: classification of all groups of order <=6 by hand and order 8 on an example sheet; definitions of finite cyclic, dihedral, symmetric and alternating groups plus computation of their orders.

[Patrick Massot]

Ok, maybe 8 rather than 20 then.

[Kevin Buzzard]

There are something like 20 groups of order 16 and it's hard to tell some of them apart.

[Kevin Buzzard]

But you can go up to 15 no problem. It's easier with Sylow theorems, because they give you groups of order pq quickly

[Patrick Massot]

Yes, this is an finite groups API test, including Sylow.

[Chris Hughes]

I did prove A5 was simple once, but it was a brute forcey proof that Mario didn't approve of. The better way is to classify the conjugacy classes of Sn and An, but this is actually quite difficult. I have some ideas in my head about how to do this though, but I think it's actually a big project.

[Chris Hughes]

There is already some stuff about cycles in there, but I don't think this is a good approach. The better way of thinking about cycle shape of $\sigma$ is as the orbits of the action of the subgroup generated by $\sigma$.

[Mario Carneiro]

I wonder about how to classify groups of order 16 in a way that isn't a giant case bash (it can be a less giant case bash though)

[Reid Barton]

I guess Maschke theorem should point at representation_theory.maschke

[Bryan Gin-ge Chen]

The module doc string of representation_theory.maschke leaves "the usual statement" to future work. I guess this is because we don't have a definition of a representation of a finite group yet?

[Reid Barton]

I would rather say it is because textbooks don't give the real version of the statement, which is the one in this file

[Reid Barton]

The part that's missing doesn't use the hypotheses needed here ($G$ is finite and of invertible order), and instead needs separate hypotheses (finite-dimensionality of the vector space)

[Patrick Massot]

The undergrad list is specifically about usual statement or at least statements that imply usual statements.

[Heather Macbeth]

Does the measure theory section of
https://github.com/leanprover-community/mathlib/blob/master/docs/overview.yaml
need a going-over? @Yury G. Kudryashov

[Reid Barton]

It seems more misleading to leave the Maschke's theorem entry blank--imagine some undergraduate sees that it is "missing" and formalizes a proof, only to discover later that basically all their work is in mathlib already.

[Floris van Doorn]

Heather Macbeth said:

Does the measure theory section of
https://github.com/leanprover-community/mathlib/blob/master/docs/overview.yaml
need a going-over? Yury G. Kudryashov

#4258

[Aaron Anderson]

Johan Commelin said:

Is https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L55 (minpoly of a matrix) now done? Aaron Anderson

We decided against making a specific notation for it. I could still make a PR to add minimal_polynomial M.is_integral or something like that to the relevant yamls

[Johan Commelin]

Johan Commelin said:

https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L96 (complex roots of unity), Patrick Massot what do you want here? We have nth_roots (1 : complex). If we link this up with e ^ (2 * pi * I / n), that should be enough, I guess?

#4260

[Heather Macbeth]

@Patrick Massot I think the "default-expanded" view of the yaml files (as on
https://leanprover-community.github.io/mathlib-overview.html
) is clearer than the "default-collapsed" view (as on
https://leanprover-community.github.io/undergrad.html
). What do others think?

[Heather Macbeth]

If the undergrad page is too long to fully expand, one could also split the difference, showing just the main headings ("linear algebra", "group theory") by default but fully expanding a heading when clicked. (At the moment it takes two clicks to see a list of individual theorems.)

[Floris van Doorn]

@Joseph Myers I've seen a lot of good PRs about Euclidean geometry, could you add some results to https://github.com/leanprover-community/mathlib/blob/master/docs/overview.yaml?

[Heather Macbeth]

(I have an open PR #4284 which includes some trivial edits to the geometry section of the file -- Joseph, feel free to add your edits to that PR, to avoid a merge conflict.)

[Patrick Massot]

I tried to switch to flat views for the undergrad lists. Reverting is easy, this is one commit. Bug hunting is welcome, I did that very quickly and I need to run again right now.

[Heather Macbeth]

It now shows in both ways (i.e., the new/expanded view at the top followed by the old/collapsed view underneath). @Patrick Massot maybe you know this and this is what you meant by

Bug hunting is welcome

? But pointing out in case you missed it.

[Patrick Massot]

Of course it was a mistake.

[Patrick Massot]

This should be fixed very soon (CI has to work a bit). Is there anything else? Do you like it this way?

[Rob Lewis]

I like that it's consistent with the overview and ctrl-f works better, and the length isn't a problem, so thumbs up for the change!

[Rob Lewis]

Random questions about the undergrad list, because I don't know what some of the entries are meant to refer to:

• Is linear algebra -- fundamentals -- direct sum docs#direct_sum.semimodule ?
• is linear algebra -- multilinearity -- special linear group docs#matrix.special_linear_group ? (Does this belong under the "matrices" header?)

[Patrick Massot]

I think the direct sum means the internal thing, expressing that a module is the direct sum of a family of submodule. This is much more common that the external version.

[Patrick Massot]

Special linear group could link to the matrix group, but it would be nicer to have the version for a vector space without a choice of basis. Last time I checked we still didn't have the determinant of an endomorphism. This would be very easy to add.

[Patrick Massot]

It would be nice to have a pass through those extremely low hanging fruits.

[Rob Lewis]

Or to publicize them better for people looking for easy projects, although I don't know the best way to do this.

[Patrick Massot]

Do you mean pointing out easy ones, or better publicizing the whole web page?

[Rob Lewis]

Pointing out easy ones

[Patrick Massot]

@Anne Baanen @Alexander Bentkamp @Aaron Anderson can't we cross out "annihilating polynomials" and "minimal polynomial" now?

[Patrick Massot]

Does any of you want to define the determinant of an endomorphism, taking inspiration from what was done with trace?

[Patrick Massot]

What happened to Alex's attempt to prove the kernels lemma? Certainly it needs annihilating polynomial and direct sums?

[Patrick Massot]

Is it true that we don't have $A[X]$ is UFD when $A$ is UFD?

[Johan Commelin]

Nope :sad: #2871

[Heather Macbeth]

@Johan Commelin the undergrad-todo lists "decomposition of a polynomial into sum of homogeneous polynomials", didn't you do this?

[Johan Commelin]

docs#mv_polynomial.sum_homogeneous_component

[Patrick Massot]

#4290

[Patrick Massot]

I thought I would fill an easy hole instead of working, so I started a tranpose branch. But of course it sounds easy only until you remember the linear algebra mess we have. In particular there seem to be no link between representing a vector of a linear map in a given basis and the theory of dual bases. So I have two nasty sorries in linear_algebra/dual.lean. Everybody should feel free to fix this.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/tranpose/src/linear_algebra/dual.lean#L184-L189

[Patrick Massot]

@Anne Baanen

[Patrick Massot]

I really didn't want to work tonight, so I also tackled the annoying only hole in the "Topology of $\mathbb{R}$" section. I need to go to bed, so anyone is welcome to take over this branch, especially if you like subgroups, casts and floor.

[Heather Macbeth]

Patrick Massot said:

I really didn't want to work tonight, so I also tackled the annoying only hole in the "Topology of $\mathbb{R}$" section. I need to go to bed, so anyone is welcome to take over this branch, especially if you like subgroups, casts and floor.

I did the sorries, it will need quite a bit of cleanup!

[Patrick Massot]

Great! I wanted to avoid https://github.com/leanprover-community/mathlib/commit/e85d9159d675cdda08c3e15b6b963c58a1ac2203#diff-96f4a64568fb76c8b14b87545794d274R336-R337 but it was probably silly since we want that property anyway if it isn't there already. Of course the two aux lemmas should be removed completely since it seems you found them in the library.

[Heather Macbeth]

Yes, I did not figure out how your original proof structure

      { refine ⟨floor (ε/2/g₁) * g₁, _, _, _⟩,
        exact mul_mem _ g₁_in,
        sorry,
        sorry },

was going to go, but feel free to rewrite it this way! (It avoids taking Inf?)

[Alexander Bentkamp]

can't we cross out "annihilating polynomials" and "minimal polynomial" now?

I think we can claim that we have minimal polynomials for endomorphisms. (see Aaron's is_root_of_has_eigenvalue and has_eigenvalue_of_is_root)

I am not aware of anything in the direction of annihilating polynomials.

What happened to Alex's attempt to prove the kernels lemma?

I've added sup_ker_aeval_eq_ker_aeval_mul_of_coprime and disjoint_ker_aeval_of_coprime. Is this what you wanted to see or did you have something else in mind?

Certainly it needs annihilating polynomial and direct sums?

I don't know how annihilating polynomials would help, but yes, It would be nice to have a definition of a direct sum of submodules instead of using ... ⊔ ... = ... and disjoint seperately.

[Anne Baanen]

Patrick Massot said:

I thought I would fill an easy hole instead of working, so I started a tranpose branch. But of course it sounds easy only until you remember the linear algebra mess we have. In particular there seem to be no link between representing a vector of a linear map in a given basis and the theory of dual bases. So I have two nasty sorries in linear_algebra/dual.lean. Everybody should feel free to fix this.

Done: https://github.com/leanprover-community/mathlib/commit/d5a35937fe5986cb9c21ef924a2d30d3182252cc

[Anne Baanen]

My experience is that is_basis.repr has basically no useful properties, and the first step is to rephrase it in terms of finsupp.total instead.

[Anne Baanen]

Of course repr (and equiv_fun) are useful for statements, just not in proofs.

[Patrick Lutz]

Patrick Massot said:

I tried to switch to flat views for the undergrad lists. Reverting is easy, this is one commit. Bug hunting is welcome, I did that very quickly and I need to run again right now.

I just noticed that the footer saying "Suggest edits to this page on GitHub" is missing from the bottom of all the "library overview" pages. Not sure if that's intentional though.

[Patrick Massot]

Anne Baanen said:

Patrick Massot said:

I thought I would fill an easy hole instead of working, so I started a tranpose branch. But of course it sounds easy only until you remember the linear algebra mess we have. In particular there seem to be no link between representing a vector of a linear map in a given basis and the theory of dual bases. So I have two nasty sorries in linear_algebra/dual.lean. Everybody should feel free to fix this.

Done: https://github.com/leanprover-community/mathlib/commit/d5a35937fe5986cb9c21ef924a2d30d3182252cc

Great, thanks!

[Patrick Massot]

@Heather Macbeth I pushed a first round of cleanup. I still need to handle your inf_property lemma.

[Heather Macbeth]

Patrick Massot said:

Heather Macbeth I pushed a first round of cleanup. I still need to handle your inf_property lemma.

Looks great! I won't have any time until tonight, so if you are free before then, feel free to do that.

[Patrick Massot]

The next step is lemma naming, I created a specific discussion since this becomes highly non-trivial.

[Patrick Massot]

Alexander Bentkamp said:

What happened to Alex's attempt to prove the kernels lemma?

I've added sup_ker_aeval_eq_ker_aeval_mul_of_coprime and disjoint_ker_aeval_of_coprime. Is this what you wanted to see or did you have something else in mind?

Sorry I missed this message earlier (I just found it while looking for something else). This is the right result but we want (one statement combining both and) arbitrary finite families of pairwise coprime polynomials.

Certainly it needs annihilating polynomial and direct sums?

I don't know how annihilating polynomials would help, but yes, It would be nice to have a definition of a direct sum of submodules instead of using ... ⊔ ... = ... and disjoint seperately.

If the products is annihilating then you can replace (⇑(polynomial.aeval f) (p * q)).ker by top.

[Patrick Massot]

Arggg, I just understood why defining linear_map.annihilating_polynomials is not straightforward. We don't have the kernel of a ring morphism from a commutative ring to a non-commutative ring. :sad:

[Patrick Massot]

I mean the definition should be

def linear_map.annihilating_polynomials (f : M →ₗ[R] M) : ideal (polynomial R):=
(polynomial.aeval f : polynomial R →ₐ[R] M →ₗ[R] M).to_ring_hom.ker

but this doesn't work because M →ₗ[R] M isn't commutative.

[Patrick Massot]

(presumably the type ascription is useful only to get a somewhat clearer error message).

[Patrick Massot]

And this should go around line 400 of ring_theory/polynomial

[Johan Commelin]

Patrick Massot said:

Arggg, I just understood why defining linear_map.annihilating_polynomials is not straightforward. We don't have the kernel of a ring morphism from a commutative ring to a non-commutative ring. :sad:

I really hope that this is something that can be fixed with a 1-line diff?

[Yury G. Kudryashov]

I almost have convergence test for p-series based on the Cauchy condensation test. Just a few real.rpow-related sorrys left.

[Patrick Massot]

@Yury G. Kudryashov did you setup anything about series in general? The big question is how to handle the fact that some series naturally don't start at index 0.

[Yury G. Kudryashov]

No, I use summable

[Patrick Massot]

Ok, so we still have this big undergrad gap.

[Anatole Dedecker]

If someone states basic definitions for series, I'd be more than happy to translate as much as possible of my series course to mathlib. But that works only if no one needs them soon, since I'm quite busy for the moment so this might take some time :(

[Scott Morrison]

I noticed on the undergraduate list "Ring Theory: Algebra: algebra over a commutative ring." is listed as missing. How are we meant to interpret that? We certainly have the definition, and quite a bit of material about algebras. Should we just link to the definition and be done? Or is there some other milestone that we have or haven't reached?

[Yury G. Kudryashov]

I'd link to the definition.

[Johan Commelin]

Or is this because we don't have the non-unital non-assoc non-comm version of algebras?

[Johan Commelin]

Is sl_2 an algebra over complex? In Lean it can't be with our current definitions.

[Scott Morrison]

We have noncommutative algebras (once upon a time we didn't).

I'm pretty unconvinced that there deserves to be a typeclass uniting associative algebras and Lie algebras.

Our lack of non-unital algebras does have me slightly worried. We bake in unitality very early.

[Yury G. Kudryashov]

Are you going to PR non-unital rings?

[Patrick Massot]

Hint: the list of undergrad math that we do have mentions "associative algebra over a commutative ring" . The key word is associative.

[Patrick Massot]

We can still decide that associative algebra $\cup$ Lie algebra is a good enough approximation, but some people will strongly disagree.

[Yury G. Kudryashov]

What properties (besides definition) do you think are required to claim this item?

[Patrick Massot]

Good question. The honest answer would be to have a definition and to have Lie algebras and associative algebras using it, but that would be a huge refactor and may bring only pain.

[Patrick Massot]

So I guess that having the definition would be good enough.

[Johan Commelin]

Honest math question: do people use non-assoc algebras apart from Lie algebras? I don't think I've ever met one outside of Lie theory.

[Johan Commelin]

Ooh, I guess the octonions are something? But then... I've never used those either.

[Patrick Massot]

Random google answer https://www.math.uci.edu/~brusso/BremnerEtAl35pp.pdf

[Patrick Massot]

But it's a bit silly in the undergrad list, especially since Lie algebra do not appear anywhere in this list.

[Patrick Massot]

The entry in our source list is "Notion d’algèbre (associative ou non) sur un anneau commutatif." But then the only explicit examples of algebras are endomorphisms and polynomials.

[Patrick Massot]

Maybe we should just remove this item, or replace it with Lie algebra since we have associative algebras elsewhere in the list.

[Johan Commelin]

I like the idea of replacing it with Lie algebra

[Johan Commelin]

Let's add a comment in the YAML where we justify that change

[Reid Barton]

What's left for a non-everything algebra $A$? Just an $R$-bilinear map $A \times A \to A$?

[Kevin Buzzard]

Do we have them?

[Reid Barton]

I guess so... we have

/-- Create a bilinear map from a function that is linear in each component. -/
def mk₂ (f : M → N → P)
  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ N →ₗ P := [...]

and

def lift.equiv : (M →ₗ N →ₗ P) ≃ₗ (M ⊗ N →ₗ P) := [...]

[Reid Barton]

I guess what we don't have is the property that an existing map M -> N -> P is bilinear, like you would expect in the algebraic hierarchy: (A : Type) [add_comm_group A] [module R A] [has_mul A] [is_bilinear_mul R A].