On undergraduate topics missing in mathlib

Stream: maths

[Stepan Nesterov]

I am looking at the page https://leanprover-community.github.io/undergrad_todo.html and I think I found a bunch of things which have been already added to mathlib since. For example:
Duality: orthognality at ## Mathlib.Analysis.InnerProductSpace.Orthogonal
Multilinearity: special linear group at ## Mathlib.LinearAlgebra.SpecialLinearGroup
Classical automorphism groups:  special unitary group at ## Mathlib.LinearAlgebra.UnitaryGroup
Representation theory of finite groups: Fourier transform for finite abelian groups at ## Mathlib.Analysis.Fourier.FourierTransform
Algebra: algebra over a commutative ring
at ## Mathlib.Algebra.Algebra.Defs
Orthogonality: Sylvester's law of inertia, real classification, complex classification at ## Mathlib.LinearAlgebra.QuadraticForm.Real and ## Mathlib.LinearAlgebra.QuadraticForm.Complex
Is the page outdated or is there in some sense not enough theory for these topics?

[Yury G. Kudryashov]

If you want to link to a file, you can use file#Mathlib/Algebra/Algebra/Defs

[Eric Wieser]

The algebra and Sylvester's law of inertia topics are disputed

[Yury G. Kudryashov]

Should we split them into subtopics, one for what's in Mathlib and one clearly stating what's missing?

[Moritz Doll]

The representation theory Fourier transform is different from the Fourier transform in file#Mathlib/Analysis/Fourier/FourierTransform

[Eric Wieser]

I think the action here is to add some fields to the TODO list so that we can elaborate on exactly what is missing

[Yaël Dillies]

Yes, we don't have the representation theory Fourier transform of finite abelian groups in mathlib. We do have a version of it in APAP though: LeanAPAP#cft

[Moritz Doll]

Do we have the Pontryagin dual for locally compact Abelian groups? That should be the main thing defining the FT in general (unless you want non-Abelian FT, which I know nothing about)

[Yaël Dillies]

Unfortunately for you, I mostly care about compact non-abelian groups, rather than locally compact abelian groups. I will soon start a project to formalise the Fourier transform in that setting

[Yaël Dillies]

Simultaneously, @Andrew Yang and I might formalise the Fourier transform in locally compact abelian groups for FLT, but this isn't relevant to my PhD so will be contingent on my availability

[Moritz Doll]

The main thing I care about is the Fourier transform on $\mathbb{R}^n$, so don't worry about me :smile:

[David Loeffler]

Eric Wieser said:

The algebra and Sylvester's law of inertia topics are disputed

Re Sylvester: what is the "dispute"? My understanding is that Mathlib has half of the statement: docs#QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared shows that (for a quadratic form over R) a basis exists in which the quadratic form is diagonal with all diag entries {0, 1, -1}; but mathlib does not currently have a proof that the numbers of 0's, 1's and -1's in such a representation are uniquely determined.

One of my ETH students has proved this uniqueness statement as part of his Master's project, and I hope this will find its way into Mathlib in due course.

[Pepa Montero Jimena]

Hi! I have a similar question. I was looking specifically at Duality: Orthogonality and saw that the current link sends you to Wikipedia's entry for Quotient spaces and annihilators.

After taking a look at Mathlib/LinearAlgebra/Dual, it seems this topic is covered already. I will paste below a summary of the results that seem to cover the topic.

Is this TODO entry outdated, or is there a specific missing result that the item was referring to?

[Pepa Montero Jimena]

-- Mathlib/LinearAlgebra/Dual/Basic.lean

def Submodule.dualAnnihilator
    (W : Submodule R M) :
    Submodule R (Module.Dual R M) :=
  LinearMap.ker W.dualRestrict

-- Galois connection
Module.dualAnnihilator_gc R M

-- Basic lattice properties
theorem dualAnnihilator_bot :
  (⊥ : Submodule R M).dualAnnihilator = ⊤

theorem dualAnnihilator_top :
  (⊤ : Submodule R M).dualAnnihilator = ⊥

theorem sup_dualAnnihilator_le_inf :
  U.dualAnnihilator ⊔ V.dualAnnihilator ≤
    (U ⊓ V).dualAnnihilator

theorem dualAnnihilator_iSup_eq :
  (⨆ i, U i).dualAnnihilator =
    ⨅ i, (U i).dualAnnihilator

-- Mathlib/LinearAlgebra/Dual/Lemmas.lean

-- Double annihilator (finite dimensional)
Subspace.dualAnnihilator_dualCoannihilator_eq

-- Galois coinsertion in finite dimension
Subspace.dualAnnihilator_gci

-- Quotient dual equivalence
def Submodule.dualQuotEquivDualAnnihilator :
  Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator

[Michael Rothgang]

Usually, it's the latter --- but I don't know about this particular item in detail.

[Stepan Nesterov]

Calling it "orthogonality" and linking to annihilators is especially confusing. Maybe the analogous facts about orthogonal complements wrt bilinear forms are not in Mathlib, and that's what "orthogonality" refers to?

[Pepa Montero Jimena]

Hmm. I'll try to take a look at that but I'm also not an expert on the topic haha. I'm actually trying to start a small lean project for students who are learning lean and Mathlib, and I thought the undergrad not in Mathlib might be a good place to start looking, but I'm not so sure now since it seems it is not very precise

[Kevin Buzzard]

I think the undergrad not in mathlib is actually a very bad place to start looking -- about 7 years after the undergraduate project started, if there are still things on that list that aren't in mathlib yet, this is probably for a good reason.

I would suggest coming up with a coherent project where students can work together and things aren't too tricky, even if the results are already in mathlib. Contributing to mathlib is becoming quite difficult in some sense, but hopefully writing lean code is becoming easier

[Patrick Massot]

Stepan Nesterov said:

Calling it "orthogonality" and linking to annihilators is especially confusing. Maybe the analogous facts about orthogonal complements wrt bilinear forms are not in Mathlib, and that's what "orthogonality" refers to?

This may be a translation issue. As explained on the website, this list is a direct translation of the curriculum of a French exam. And the French way to talk about this uses “orthogonalité” and nothing that sounds like “annihilator”.

[Patrick Massot]

@Pepa Montero Jimena a pull-request filling that entry with Submodule.dualAnnihilator is definitely welcome.