# Zulip Chat Archive

## Stream: general

### Topic: updating beginner material

#### Rob Lewis (Sep 25 2020 at 14:41):

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 (Sep 25 2020 at 14:47):

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

#### Johan Commelin (Sep 25 2020 at 14:50):

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 (Sep 25 2020 at 14:51):

What does `examples of groups with small cardinality`

refer to?

#### Johan Commelin (Sep 25 2020 at 14:52):

@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 (Sep 25 2020 at 14:55):

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

#### Kevin Buzzard (Sep 25 2020 at 14:55):

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 (Sep 25 2020 at 14:55):

Ok, maybe 8 rather than 20 then.

#### Kevin Buzzard (Sep 25 2020 at 14:55):

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

#### Kevin Buzzard (Sep 25 2020 at 14:55):

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 (Sep 25 2020 at 14:56):

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

#### Chris Hughes (Sep 25 2020 at 14:58):

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 (Sep 25 2020 at 15:00):

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 (Sep 25 2020 at 15:01):

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 (Sep 25 2020 at 15:01):

I guess `Maschke theorem`

should point at `representation_theory.maschke`

#### Bryan Gin-ge Chen (Sep 25 2020 at 15:04):

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 (Sep 25 2020 at 15:05):

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 (Sep 25 2020 at 15:08):

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 (Sep 25 2020 at 15:14):

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

#### Heather Macbeth (Sep 25 2020 at 15:24):

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 (Sep 25 2020 at 16:12):

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 (Sep 25 2020 at 17:57):

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

#### Aaron Anderson (Sep 25 2020 at 20:12):

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 `yaml`

s

#### Johan Commelin (Sep 25 2020 at 20:30):

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?

#### Heather Macbeth (Sep 25 2020 at 20:58):

@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 (Sep 25 2020 at 21:00):

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 (Sep 27 2020 at 04:58):

@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 (Sep 27 2020 at 05:04):

(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 (Sep 27 2020 at 09:07):

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 (Sep 27 2020 at 14:19):

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 (Sep 27 2020 at 14:53):

Of course it was a mistake.

#### Patrick Massot (Sep 27 2020 at 14:55):

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

#### Rob Lewis (Sep 27 2020 at 16:06):

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 (Sep 27 2020 at 16:13):

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 (Sep 27 2020 at 16:24):

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 (Sep 27 2020 at 16:27):

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 (Sep 27 2020 at 16:28):

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

#### Rob Lewis (Sep 27 2020 at 16:39):

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

#### Patrick Massot (Sep 27 2020 at 16:41):

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

#### Rob Lewis (Sep 27 2020 at 16:42):

Pointing out easy ones

#### Patrick Massot (Sep 27 2020 at 16:49):

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

#### Patrick Massot (Sep 27 2020 at 16:50):

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

#### Patrick Massot (Sep 27 2020 at 16:50):

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

#### Patrick Massot (Sep 27 2020 at 16:54):

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

#### Johan Commelin (Sep 27 2020 at 17:28):

Nope :sad: #2871

#### Heather Macbeth (Sep 27 2020 at 17:50):

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

#### Johan Commelin (Sep 27 2020 at 17:53):

docs#mv_polynomial.sum_homogeneous_component

#### Patrick Massot (Sep 27 2020 at 18:05):

#### Patrick Massot (Sep 27 2020 at 19:42):

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 (Sep 27 2020 at 19:42):

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

#### Patrick Massot (Sep 27 2020 at 19:42):

@Anne Baanen

#### Patrick Massot (Sep 27 2020 at 21:29):

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 (Sep 28 2020 at 06:05):

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 (Sep 28 2020 at 07:50):

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 (Sep 28 2020 at 07:57):

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 (Sep 28 2020 at 08:31):

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 (Sep 28 2020 at 09:42):

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 (Sep 28 2020 at 09:45):

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 (Sep 28 2020 at 09:46):

Of course `repr`

(and `equiv_fun`

) are useful for statements, just not in proofs.

#### Patrick Lutz (Sep 28 2020 at 10:15):

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 (Sep 28 2020 at 14:05):

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 (Sep 28 2020 at 14:46):

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

lemma.

#### Heather Macbeth (Sep 28 2020 at 15:05):

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 (Sep 28 2020 at 15:09):

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

#### Patrick Massot (Sep 28 2020 at 19:35):

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 (Sep 28 2020 at 20:03):

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 (Sep 28 2020 at 20:07):

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 (Sep 28 2020 at 20:08):

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

#### Patrick Massot (Sep 28 2020 at 20:09):

And this should go around line 400 of `ring_theory/polynomial`

#### Johan Commelin (Sep 29 2020 at 04:50):

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 (Sep 29 2020 at 09:17):

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

-related `sorry`

s left.

#### Patrick Massot (Sep 29 2020 at 11:11):

@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 (Sep 29 2020 at 11:48):

No, I use `summable`

#### Patrick Massot (Sep 29 2020 at 11:51):

Ok, so we still have this big undergrad gap.

#### Anatole Dedecker (Sep 29 2020 at 19:45):

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 (Oct 03 2020 at 01:16):

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 (Oct 03 2020 at 01:40):

I'd link to the definition.

#### Johan Commelin (Oct 03 2020 at 04:07):

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

#### Johan Commelin (Oct 03 2020 at 04:07):

Is `sl_2`

an *algebra* over `complex`

? In Lean it can't be with our current definitions.

#### Scott Morrison (Oct 03 2020 at 04:20):

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 (Oct 03 2020 at 06:32):

Are you going to PR non-unital rings?

#### Patrick Massot (Oct 03 2020 at 08:20):

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

#### Patrick Massot (Oct 03 2020 at 08:21):

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

#### Yury G. Kudryashov (Oct 03 2020 at 08:25):

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

#### Patrick Massot (Oct 03 2020 at 08:27):

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 (Oct 03 2020 at 08:27):

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

#### Johan Commelin (Oct 03 2020 at 08:28):

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 (Oct 03 2020 at 08:29):

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

#### Patrick Massot (Oct 03 2020 at 08:29):

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

#### Patrick Massot (Oct 03 2020 at 08:30):

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

#### Patrick Massot (Oct 03 2020 at 08:32):

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 (Oct 03 2020 at 08:33):

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

#### Johan Commelin (Oct 03 2020 at 08:36):

I like the idea of replacing it with Lie algebra

#### Johan Commelin (Oct 03 2020 at 08:36):

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

#### Reid Barton (Oct 03 2020 at 12:36):

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

#### Kevin Buzzard (Oct 03 2020 at 12:37):

Do we have them?

#### Reid Barton (Oct 03 2020 at 12:43):

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 (Oct 03 2020 at 12:54):

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]`

.

Last updated: Dec 20 2023 at 11:08 UTC