TODOs

Stream: condensed mathematics

[Johan Commelin]

• [ ] Give all major decls and all defs proper docstrings
• [ ] Give all files proper module docstrings
• [ ] Setup CI to lint for docstrings
• [ ] Mark major decls in blueprint and lean code
• [ ] Give all decls proper names
• [ ] Document some of the longer proofs (thm98, thm96)
• [ ] Speed up slower proofs (thm98, row_iso, col_exact)
• [ ] Update the blueprint to have a proper proof of col_exact
• [ ] Update the blueprint with final choice of constants
• [ ] Switch BD stuff from free_abelian_group to finsupp
• [ ] Write a tale overview version of the proof (claimed by jmc)

[Johan Commelin]

First thing I'll do now is bumping mathlib. Hasn't happened in 8 days.

[Riccardo Brasca]

Concerning free abelian group we will soon (hopefully) have in mathlib module.free, when #7801 gets merged.

[Riccardo Brasca]

Free abelian groups are exactly (even in Lean) free Z-modules, right?

[Johan Commelin]

I should probably explain what I mean with
Switch BD stuff from free_abelian_group to finsupp

Scott has been working on generalizing the category FreeMat of universal maps (in LTE) to Free _ and Mat _ in mathlib. But Free _ will give the free R-linear category for some ring R (using finsupp).
universal_map is implemented using free_abelian_group which is specific to $\Z$.

[Johan Commelin]

In the end, it will be best to move everything over to Free (Mat _), and a first step would be to migrate from free_abelian_group to finsupp.

[Johan Commelin]

A lot of for_mathlib/free_abelian_group was doing exactly the opposite thing :see_no_evil:

[Johan Commelin]

Here are two other projects:

1. Refactor LTE: instead of normed_group_hom.bound_by, use the operator norm everywhere.
2. Add a class has_nnnorm to mathlib, define an instance for semi_normed_groups. Add notation for it (such as $\|x\|_+$). Refactor mathlib to use this notation. Refactor LTE to use this notation. Add an instance for Mbar, which has the wrong topology to be a semi_normed_group, but nevertheless has a norm.

[Patrick Massot]

I wanted to ask where this bound_bycame from.

[Johan Commelin]

From ignorant me

[Riccardo Brasca]

I can work on this refactor

[Johan Commelin]

Which one?

[Riccardo Brasca]

Let me start with the one about normed_group_hom.bound_by

[Johan Commelin]

@Riccardo Brasca It looks like the definition of bound_by already ended up in mathlib. So probably the best thing to do is to get rid of all uses of bound_by in LTE, and then remove the def from mathlib again

[Riccardo Brasca]

Hmm, yes, I also noticed that. I think that the best thing to do is first of all adding some lemmas to mathlib, for example docs#normed_group_hom.mk_normed_group_hom'_bound_by is used in LTE, and we need the analogue lemma for the operator norm before removing bound_by from LTE.

[Riccardo Brasca]

Ah, it's already there docs#normed_group_hom.mk_normed_group_hom_norm_le