introduction myself (jt)

Stream: new members

[Justin Thomas]

Hello,
My name is Justin Thomas. I have a PhD but now do software for a living. I have seen some others here with similar stories, which is very cool. I have been nosing around the website for a while and thought maybe I should introduce myself. I am currently working through the tutorial. I have in the past played around with coq, using https://softwarefoundations.cis.upenn.edu/, but saw a talk by Kevin Buzzard (https://www.youtube.com/watch?v=Dp-mQ3HxgDE) that pulled me over to Lean. I don't have some grand picture of what I want to contribute, so I am happy to take a look at some of the "boring but not too hard" things others just haven't had time for. My PhD work involved algebraic topology, homotopy theory, operads and the like. Those are my interests mathematically, but I also have quite a bit of programming experience now, so I feel there are many ways I can contribute. Anywho, I'll just keep working through the tutorial. If anyone has any suggestions of low-hanging fruit, I'd love to contribute sooner rather than later.

[Patrick Massot]

Did you see the undergrad TODO list?

[Patrick Massot]

And the wiki pages at https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets and https://github.com/leanprover-community/mathlib/wiki/Undergrad-low-hanging-fruits ? Those seem to fit your description ""boring but not too hard" things others just haven't had time for" pretty well

[Justin Thomas]

@Patrick Massot I did not see those. thank you.

[Matt Yan]

@Patrick Massot From what I read earlier, people are trying to implement very general theorems and "overkill" the easy ones. Will that make the specialized theorems obselete? Are they still of value?

[Patrick Massot]

There are many easy things on those lists that won't get killed by sophisticated versions

[Patrick Massot]

And I think it's not a problem is something eventually gets replaced by a more general version.

[Patrick Massot]

Especially if part of your motivation is to learn how to use Lean better.

[Justin Thomas]

I understand generalities might replace specialized statements. That seems like the natural way of things. For learning, it seems like some specializations are actually preferred. At least that is my first impression.

Anyway, I got to spend a half hour or so looking at the Undergrad TODO trivial targets. From what I understand, Zulip is the right place for the following questions.

I am focusing on what looks the simplest:
Linear algebra / finite rank of a set of vectors.

From what I can tell, I would put a def somewhere in linear_algebra.finite_dimensional. Perhaps near the line
/-- The submodule generated by a single element is finite-dimensional. -/
Then I would update undergrad.yaml to point to this definition.

After that, clean up style, naming, documentation, make pull request, yadda yadda?

[Riccardo Brasca]

This is more or less what one is supposed to do. But if you write a newdef, you should also provide a basic API. This means essentially making the definition useful for other, proving trivial results. (And I really mean trivial, something like "the rank of a family is the dimension of the span, or whatever". This is of course true by definition, but it is useful to have it). Also very easy lemmas (like the rank of the zero vector is zero and so on) will be appreciated.

[Riccardo Brasca]

To have an idea you can have a look at the results the follow a definition you understand

[Eric Rodriguez]

by the way, Justin, that statement seems to already be there: docs#finite_dimensional.submodule.span.finite_dimensional

[Patrick Massot]

Of course the first step is to check that the list is up to date and nobody did this item already. I have a vague memory of someone doing that one.

[Patrick Massot]

And indeed it appears on https://leanprover-community.github.io/undergrad.html so the wiki page needs updating, sorry about that.

[Justin Thomas]

@Eric Rodriguez @Patrick Massot thanks. I see it now. Thanks for the heads-up. If it is always as easy as just trying something and it magically appearing I could get to like this.

[Justin Thomas]

A cursory search for an existing definition of annihilating polynomials (https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets#endomorphism-polynomials) seems to show this one is not done yet. Let me know if I missed it.

[Yimu Yin]

Hi,
I have just finished the natural number game. What should I do next?

I want to work in a particular area of applied model theory, which talks a lot about real fields, valued fields, etc., these seem to be well represented in the library. But there isn't any work on the first order logic? Say, the first order compactness theorem?

Yimu Yin

[Yaël Dillies]

Hey! First order logic is well developed in the Flypitch project. They are currently in the process of moving the code to mathliob.

[Justin Thomas]

I found minpoly.lean, which seams to have the content in https://en.wikipedia.org/wiki/Minimal_polynomial_(linear_algebra)#Formal_definition, which is the link found here https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets#endomorphism-polynomials. Now I am not sure if this is covered with minpoly or if there is some other source of content wanted here.

[Johan Commelin]

I think @Patrick Massot wants a specialized definition for endomorphisms of vector spaces, where you apply minpoly to that endomorphism.

[Eric Rodriguez]

There is actually some nice low hanging fruit from minpolys, which would be genuinely helpful for the flt-regular project; upgrading results from it from gcd-domains to integrally closed domains. Riccardo did an issue here which also has a proof, and I'm more than happy to help with this as I want this result!

[Eric Rodriguez]

(upgrading Gauss' lemma lets us make docs#gcd_domain_dvd actually for integrally closed domains)

[Riccardo Brasca]

For that we need Vieta's formulas I am afraid

[Riccardo Brasca]

Or at least that the coefficients can be written as a polynomial (no matter which one) in the roots

[Eric Rodriguez]

ahh, I noticed https://leanprover-community.github.io/mathlib_docs/ring_theory/polynomial/vieta.html before but looking at it closer that doesn't seem to be exactly what's needed

[Riccardo Brasca]

Ah, that didn't exist last time I checked!

[Patrick Massot]

Justin Thomas said:

I found minpoly.lean, which seams to have the content in https://en.wikipedia.org/wiki/Minimal_polynomial_(linear_algebra)#Formal_definition, which is the link found here https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets#endomorphism-polynomials. Now I am not sure if this is covered with minpoly or if there is some other source of content wanted here.

It defines minpoly but not what is denoted by $I_T$ in the wikipedia page.

[Patrick Massot]

The expected type is:

import linear_algebra
import data.polynomial

variables (A : Type*) {M : Type*} [comm_ring A] [add_comm_group M] [module A M]

def annihilating_ideal (u : M →ₗ[A] M) : ideal (polynomial A) :=
sorry

and then some lemma saying that if A is a field then this is spanned by minpoly

[Eric Rodriguez]

oh! this is the ideal we were talking about here

[Eric Rodriguez]

do you know if the basis results that we were talking about there are true more generally Patrick?

[Patrick Massot]

I don't have time to read the whole thread. But the minpoly doesn't have good properties if you can't link it to that ideal.

[Justin Thomas]

thank you all for the input. Not much to say from me right now except that I am definition-chasing at the moment around minpoly / linear_algebra / data.polynomial land to try to narrow the scope of this in my mind. The syntax in the statement of the expected type above is super helpful

[Justin Thomas]

(not sure if it is time for me to start a new thread...)
I am still working to add some simple results about annihilating ideal. I cannot seem to find some existing code showing k[x] is a PID if k is a field. Seems there are a lot of things close to this, but I just can't seem to get the hang of searching for existing results.

[Eric Rodriguez]

this should hold automatically from type-class inference

[Eric Rodriguez]

if you've got some code I'm glad to check it out as I want this result too ^^

[Justin Thomas]

@Eric Rodriguez
I only just managed to define

/- An A-module endomorphism u gives an ideal in the polynomial algebra
{ p ∈ A[x] | p(u) = 0 }, where p(u) is defined above in `polynomial_endomorphism` -/
noncomputable def annihilating_ideal (u: M →ₗ[A] M) : ideal (polynomial A) :=
  ring_hom.ker (polynomial_endomorphism u).to_ring_hom

From this I am trying to specialize to the case A = \bbk, a field, then say minpoly u generates the annihilating ideal.
This has not gotten very far though. For the first step, I am trying to use some existing code to grab the annihilating ideal generator:

variable {𝕜 : Type*}
variables [field 𝕜]
noncomputable def annihiliating_ideal_generator (u: M →ₗ[A] M) : polynomial A :=
  submodule.is_principal.generator (annihilating_ideal u)

But this complains failed to synthesize type class instance for ... I assume it cannot infer submodule.is_principal, so I tried to convince it that \bbk [x] satisfies is_principal_ideal_ring. This is the part I thought I could find somewhere already.
I am still learning how to read lean error messages, and how unification and type-classes work, so I am not sure I am on the right track here

Update: silly error. I switched to k as the field name but left A in the def. After putting k in the def. It seems happy.

[Eric Rodriguez]

great when errors work themselves out! :D

[Justin Thomas]

I'd like to get some review on this implementation of annihilating ideal. I started a pull request just as an easy way to see the diffs. I actually meant to leave the pull request in my twoquarterrican fork of the repo, but messed up. Anyway, I can move it if need be.

Main points:

1. Had a lot of trouble getting types to line up for alg_hom versus ring_hom and for with_bot \nat versus \nat. I would love some help on how to handle this better. Currently there are simple lemmas added in a couple places since that is the try among dozens of things that actually worked.
2. Have annihilating_ideal defined. The names are pretty long. I see abbreviations are common in the code, but a lot of them don't make sense to me so I think I need some help on how to name things better.
3. I just covered the very basic goal of showing that the minpoly generates the annihilating ideal in the \bbk [x] case. Surely there are some other things I can add to fill it out a bit more.
4. Proofs use only the few tactics I know. They appear longer and accomplish less than most other proofs I have seen. I don't mind it though. I like running through the tactics when they do a little bit at a time. It is fun. Anyway, I can make these more sleek with help and a good reason to.
   https://github.com/leanprover-community/mathlib/pull/12135/files

[Justin Thomas]

Thanks all for the helpful comments. I am suffering from documentation overload, so bear with me :)

1. I would like to request permission to push to non-master branches of the mathlib repo. My username is twoquarterrican.
2. I haven't seen any requirements on rebasing versus merging. I have just been merging. I can rebase and squash if need be.
3. I saw that the commit conventions in https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md apply to PR messages. Do they also apply to all commit messages in my branch? Do I need to reword all of my commits?

[Johan Commelin]

@Justin Thomas https://github.com/leanprover-community/mathlib/invitations

[Johan Commelin]

Re (2): Merging is completely fine.
Re (3): Only to the PR message. PRs are merged using squash commits, so you don't have to worry about how you name intermediate commits.

[Justin Thomas]

@Johan Commelin thanks.
closed previous PR. opened new one. pipeline running now. https://github.com/leanprover-community/mathlib/pull/12140
AFAIK all the comments from my first PR attempt have been addressed

[Junyan Xu]

(deleted)