Zulip Chat Archive

Stream: condensed mathematics

Topic: TODOs

Johan Commelin (Jun 07 2021 at 07:44):

  • [ ] 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 (Jun 07 2021 at 07:45):

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

Riccardo Brasca (Jun 07 2021 at 08:38):

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

Riccardo Brasca (Jun 07 2021 at 08:38):

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

Johan Commelin (Jun 07 2021 at 08:40):

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\Z.

Johan Commelin (Jun 07 2021 at 08:40):

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 (Jun 07 2021 at 08:41):

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

Johan Commelin (Jun 07 2021 at 11:11):

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∥+\|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 (Jun 07 2021 at 11:12):

I wanted to ask where this bound_bycame from.

Johan Commelin (Jun 07 2021 at 11:13):

From ignorant me

Riccardo Brasca (Jun 07 2021 at 11:15):

I can work on this refactor

Johan Commelin (Jun 07 2021 at 11:15):

Which one?

Riccardo Brasca (Jun 07 2021 at 11:16):

Let me start with the one about normed_group_hom.bound_by

Johan Commelin (Jun 07 2021 at 11:37):

@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 (Jun 07 2021 at 11:58):

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 (Jun 07 2021 at 11:59):

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

Last updated: Dec 20 2023 at 11:08 UTC