Zulip Chat Archive

Stream: condensed mathematics

Topic: for_mathlib

Kevin Buzzard (Feb 05 2021 at 17:55):

OK so we're not quite at lean-perfectoid-space levels yet,but with 14 files in for_mathlib we are beginning to walk into the same trap which Johan, Patrick and I walked into in 2019, generating a whole bunch of stuff which was _clearly_ for mathlib, much of it even mathlib-ready, and then not PR'ing it and then it rotted and the work we put in there was, arguably, wasted (although of course it fulfilled the role of helping us formalise perfectoid spaces). Do we have a plan here, or are we just going to watch this directory fill up and then go "oh look it happened again"? There are over 1300 lines of code in that directory so far.

Patrick Massot (Feb 05 2021 at 17:57):

My opinion is we should explicitly state that everything in the folder can be PRed to mathlib by anyone. If it means someone feel they lose credit then it means they should have made the PRing effort. Of course when things do not get PRed then the author should still be the only one to feel bad.

Johan Commelin (Feb 05 2021 at 18:03):

yes, I very much agree with what Patrick said.

Kevin Buzzard (Feb 05 2021 at 18:03):

I personally never feel that it is about "credit". However when I was making the universal_universe branch on this repo I didn't put anything in for_mathlib, I just made notes of what needed to be PR'ed and am slowly PR'ing it myself. I did the same today. I think there is a risk that nobody does it. Of course anyone can feel free to do it, but we all know it's hard work. I am wondering if we need a better plan than this. Or do you think I'm overreacting and it doesn't matter?

Chris Hughes has long argued that free_abelian_group should be defined via finsupp. I see now that Johan has just made the interface relating the current definition to finsupp. Chris won't be happy because he wanted the equality to be definitional, but I am less excited by definitional equality than he is. This is 300 lines of code though. It probably should not be lost!

Johan Commelin (Feb 05 2021 at 18:10):

I agree that we should work on PRing things. But on the other hand, momentum is also a weird concept... once I have momentum working on a project like this, I just want to march forward, and not be blocked by PRs.

Johan Commelin (Feb 05 2021 at 18:10):

Something I would like to experiment with, is whether we can do some sort of for_mathlib PR sprints.

Johan Commelin (Feb 05 2021 at 18:11):

Once we reach some sort of intermediate milestone/target, we just take a step back, and create 37 PRs to mathlib. And after that we plunge forward to the next target.

Kevin Buzzard (Feb 05 2021 at 18:27):

Johan this is exactly how I felt with perfectoid. Once I could see that it was possible to do this kind of mathematics in Lean (because in 2018 this was not yet clear, as you well remember!), I would just throw myself into a lot of focussed coding with clear well-defined goals in mind and fill up for_mathlib and just not worry. All three of us were doing it, and then Patrick suddenly saw sense and PR'd a whole bunch of topology into mathlib (all the Bourbaki stuff which he'd done) -- but I can't remember whether this was during the sprint to the def or after we had the def.

Patrick Massot (Feb 05 2021 at 18:47):

It was during the sprint, but there was a special trick. mathlib had stuff about this, but it wasn't good enough and was actually getting in our way. That's why I was force to work on the mathlib side.

Scott Morrison (Feb 05 2021 at 22:29):

I'm glad there's consensus that "anyone should feel free to make the PRs from for_mathlib". This is a chore that I don't find particularly tedious, and will make some effort at it after the weekend!

Johan Commelin (Feb 10 2021 at 12:46):

Anyone looking for some PRs to make:

$ find src/for_mathlib/ -name '*.lean' | xargs wc -l
  189 src/for_mathlib/sequences.lean
   21 src/for_mathlib/category_theory.lean
   34 src/for_mathlib/tsum.lean
   31 src/for_mathlib/extend_from_nat.lean
  403 src/for_mathlib/normed_group_hom.lean
   55 src/for_mathlib/equalizers.lean
  114 src/for_mathlib/topology.lean
   18 src/for_mathlib/linear_algebra.lean
   19 src/for_mathlib/topological_group.lean
   62 src/for_mathlib/locally_constant.lean
  362 src/for_mathlib/free_abelian_group.lean
   40 src/for_mathlib/compact.lean
   92 src/for_mathlib/add_monoid_hom.lean
 1440 total

Johan Commelin (Feb 10 2021 at 12:47):

I think I'll take on free_abelian_group and locally_constant

Riccardo Brasca (Feb 10 2021 at 12:50):

I can do sequences

Riccardo Brasca (Feb 10 2021 at 12:55):

Ops, it depends on locally_constant, it is better to wait.

Kevin Buzzard (Feb 10 2021 at 13:52):

I made a PR to free_abelian_group recently, which came out of the universal maps stuff. #6062. It's waiting for epsilon more work by me.

Johan Commelin (Feb 10 2021 at 21:37):

I ended up working on for_mathlib/compact first...

Johan Commelin (Feb 10 2021 at 21:37):

I hope to tackle locally_constant asap

Johan Commelin (Feb 11 2021 at 21:47):

for_mathlib/locally_constant has now been PRd

Johan Commelin (Feb 23 2021 at 08:45):

#6375 PRs most of normed_group_hom to mathlib. About 20% of for_mathlib (-;

Johan Commelin (Mar 10 2021 at 06:38):

This PR has now been merged, and so ~370 lines of for_mathlib were deleted this morning.

Johan Commelin (Mar 10 2021 at 06:38):

Be sure to git pull before you work on master

Johan Commelin (Mar 10 2021 at 06:39):

What is left:

  185 src/for_mathlib/sequences.lean
   34 src/for_mathlib/tsum.lean
   31 src/for_mathlib/extend_from_nat.lean
   55 src/for_mathlib/equalizers.lean
  114 src/for_mathlib/topology.lean
   14 src/for_mathlib/pi_nat_apply.lean
   18 src/for_mathlib/linear_algebra.lean
   19 src/for_mathlib/topological_group.lean
  362 src/for_mathlib/free_abelian_group.lean
  319 src/for_mathlib/normed_group_quotient.lean
   92 src/for_mathlib/add_monoid_hom.lean
 1243 total

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

Things deteriorated quickly after our previous for_mathlib sprint :see_no_evil: 

$ git ls-files | rg "[.]lean$" | rg "for_mathlib" | xargs wc -l
    94 src/for_mathlib/Cech/adjunction.lean
   229 src/for_mathlib/Cech/split.lean
   635 src/for_mathlib/Gordan.lean
   314 src/for_mathlib/Profinite/arrow_limit.lean
   770 src/for_mathlib/Profinite/clopen_limit.lean
   151 src/for_mathlib/Profinite/compat_discrete_quotient.lean
    37 src/for_mathlib/Profinite/fibprod.lean
    36 src/for_mathlib/Profinite/locally_constant.lean
    75 src/for_mathlib/arrow.lean
    16 src/for_mathlib/arrow/iso_mk.lean
    19 src/for_mathlib/arrow/split.lean
    11 src/for_mathlib/coe_nat_abs.lean
   124 src/for_mathlib/data_setoid_partition.lean
    74 src/for_mathlib/discrete_quotient.lean
    47 src/for_mathlib/fin.lean
   137 src/for_mathlib/finite_free.lean
    18 src/for_mathlib/finsupp.lean
   385 src/for_mathlib/free_abelian_group.lean
   721 src/for_mathlib/grading.lean
   104 src/for_mathlib/grading_examples.lean
   477 src/for_mathlib/grading_zero_subring.lean
    93 src/for_mathlib/homological_complex.lean
    56 src/for_mathlib/homotopy.lean
    87 src/for_mathlib/is_locally_constant.lean
    90 src/for_mathlib/kronecker.lean
    65 src/for_mathlib/linear_algebra.lean
   593 src/for_mathlib/nnrat.lean
    20 src/for_mathlib/nnreal.lean
   158 src/for_mathlib/normed_group.lean
    91 src/for_mathlib/normed_group_hom.lean
    99 src/for_mathlib/normed_group_hom_bound_by.lean
   174 src/for_mathlib/normed_group_hom_completion.lean
    96 src/for_mathlib/normed_group_hom_equalizer.lean
    89 src/for_mathlib/order.lean
    34 src/for_mathlib/pseudo_metric.lean
    21 src/for_mathlib/quotient.lean
   566 src/for_mathlib/rational_cones.lean
    43 src/for_mathlib/simplicial/augmented.lean
   161 src/for_mathlib/simplicial/complex.lean
    64 src/for_mathlib/simplicial/iso.lean
    72 src/for_mathlib/specific_limit.lean
   219 src/for_mathlib/topology.lean
    34 src/for_mathlib/tsum.lean
   275 src/for_mathlib/unused/Profinite/functorial_limit.lean
    69 src/for_mathlib/unused/Profinite/nhds.lean
    45 src/for_mathlib/unused/Top.lean
    42 src/for_mathlib/unused/dfinsupp.lean
    55 src/for_mathlib/unused/equalizers.lean
    54 src/for_mathlib/wide_pullback.lean
  7939 total

Patrick Massot (Jun 07 2021 at 11:11):

I'll work on the topology and normed group stuff.

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

I think that normed_group_hom_bound_by is probably not for_mathlib... we should have used the operator norm everywhere. But I didn't know enough functional analysis and/or mathlib. So I blundered in with my own definition :see_no_evil:

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

@Bhavik Mehta @Yaël Dillies Are you planning on PRing the rational cones / Gordan stuff to mathlib?

Bhavik Mehta (Jun 07 2021 at 11:20):

Certainly not immediately - I think a good portion of it ought to be generalised to the nonnegative parts of an ordered field (I did it for nonneg rationals using nnrat, but the nnreal version is useful too) so I've been waiting for the ordered refactor to go through first

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

Ok, that certainly makes sense

Adam Topaz (Jun 07 2021 at 13:05):

@Patrick Massot the two lemmas about topological bases in for_mathlib/topology are already in mathlib (in more general form). I've also been (slowly) getting the Profinite stuff in PRs

Yaël Dillies (Jun 07 2021 at 19:20):

I can definitely PR exposed faces already. Then Krein-Milman will only need Bhavik's Hahn-Banach PR.

Adam Topaz (Jun 07 2021 at 23:20):

Here is a PR with the theorem about clopen sets in cofiltered limits of profinite sets: #7837

Adam Topaz (Jun 10 2021 at 15:25):

#7837 should be ready to review, in case anyone has some time...

Johan Commelin (Jun 10 2021 at 15:39):

Looks good to me, but the proof is somewhat long. Are there no reusable sublemmas?

Adam Topaz (Jun 10 2021 at 15:51):

I don't think there are any reusable subclaims that are worth splitting off, tbh. The proof looks long, but there are really just a few main steps and followed by several annoying formalization things. I can add a few inline comments explaining the argument

Patrick Massot (Jun 10 2021 at 15:52):

Adding comments explaining the argument is always nice

Adam Topaz (Jun 10 2021 at 16:07):

Patrick Massot said:

Adding comments explaining the argument is always nice

Done

Patrick Massot (Jun 10 2021 at 16:10):

Why do you use rotate everywhere? Does it help with meta-variables?

Patrick Massot (Jun 10 2021 at 16:11):

Do you know you can put type ascriptions in obtain and rintros? This both documents the proof and avoids change or dsimp.

Patrick Massot (Jun 10 2021 at 16:12):

let j : S → J := λ s, (hS s.2).some,
  let V : Π (s : S), set (F.obj (j s)) := λ s, (hS s.2).some_spec.some,
  have hV : ∀ (s : S), is_clopen (V s) ∧ s.1 = C.π.app (j s) ⁻¹' (V s) :=
    λ s, (hS s.2).some_spec.some_spec,

feels like you could use choose

Adam Topaz (Jun 10 2021 at 16:20):

I tried using choose, but it makes it much more annnoying to define G later on, so I don't think it's worth it

Patrick Massot (Jun 10 2021 at 16:21):

Did you try choose!? Note that I'm writing random comments without having run the code.

Adam Topaz (Jun 10 2021 at 16:21):

I didn't try choose!

Adam Topaz (Jun 10 2021 at 16:21):

let me try it now

Adam Topaz (Jun 10 2021 at 16:22):

Nope, same issue. Essentially I want to consider the type associated to the set (of sets) S, and choose gives me a slightly different function as a result

Adam Topaz (Jun 10 2021 at 16:25):

In the line let j : S \to J, choose(!) gives me a function of the form \forall {A : set ..}, A \in S \to J. Later on I get a finset in the type associated to S, so it's much more convenient to just start with a function of the form j : S \to J.

Adam Topaz (Jun 10 2021 at 16:26):

As for the rotate, I only use it because in the have ... clause I introduce two new goals which I want to take care of immediately

Adam Topaz (Jun 10 2021 at 16:30):

The two dsimp's were optional, so I just got rid of them

Adam Topaz (Jun 10 2021 at 16:31):

And the first change is a bit of a sneaky hack, since I know the topological space of an object X of Profinite is defeq to the topological space associated to Profinite_to_Top.obj X, and lean needs a bit of a hint to figure this out. I hope you'll let me get away with this ;)

Patrick Massot (Jun 12 2021 at 19:40):

I just bumped mathlib, incorporating #7858

Patrick Massot (Jun 12 2021 at 20:32):

I tried to cleanup some more but only managed a tiny commit because I wasn't able to easily use Adam's recent merged cofiltered limits stuff.

Patrick Massot (Jun 12 2021 at 20:33):

@Adam Topaz could you now clean up clopen_limit?

Patrick Massot (Jun 12 2021 at 20:34):

One apparent obstacle is that docs#category_theory.is_cofiltered_of_semilattice_inf_bot asks for some bot element that isn't assumed in LTE.

Adam Topaz (Jun 12 2021 at 20:34):

Oh, it should have one. I'll take a look

Adam Topaz (Jun 12 2021 at 20:36):

oh, that's silly. The system comes from discrete_quotient which is a semilattice_inf_top, and the bot in that instance is only to obtain a nonempty instance. So we need some more instances like is_cofiltered_of_semilattice_inf_top

Adam Topaz (Jun 12 2021 at 20:38):

Let me make a quick mathlib PR with these missing instances right now...

Adam Topaz (Jun 12 2021 at 20:41):

#7909

Patrick Massot (Jun 12 2021 at 20:41):

Oh I understand. I thought this bot requirement was weird...

Patrick Massot (Jun 12 2021 at 20:42):

Why can't we just have a nonempty type class parameter?

Patrick Massot (Jun 12 2021 at 20:42):

and instanced saying those lattice are nonempty?

Adam Topaz (Jun 12 2021 at 20:45):

good point

Adam Topaz (Jun 12 2021 at 20:48):

It's a bit strange that there is no 

instance has_top_nonempty (α : Type u) [has_top α] : nonempty α := ⟨⊤⟩
instance has_bot_nonempty (α : Type u) [has_bot α] : nonempty α := ⟨⊥⟩

Adam Topaz (Jun 12 2021 at 20:48):

Is there a good reason not to have this?

Patrick Massot (Jun 12 2021 at 20:49):

weird

Patrick Massot (Jun 12 2021 at 20:49):

I don't see why there shouldn't be here (with low priority as usual for catch-all instances)

Adam Topaz (Jun 12 2021 at 20:55):

Okay, I'll update that PR soon

Adam Topaz (Jun 12 2021 at 21:07):

Okay, #7909 is updated. Should be ready to review

Patrick Massot (Jun 12 2021 at 21:28):

Another LTE PR: #7910

Patrick Massot (Jun 12 2021 at 21:37):

and #7911 to empty a stupid file containing a single stupid lemma

Adam Topaz (Jun 13 2021 at 18:29):

Doing another mathlib bump right now, and cleaning up the exists_clopen mess...

Adam Topaz (Jun 13 2021 at 18:33):

 leanpkg.toml                                |   2 +-
 src/for_mathlib/Profinite/clopen_limit.lean | 351 +++---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 2 files changed, 6 insertions(+), 347 deletions(-)

Johan Commelin (Jun 15 2021 at 04:59):

If anyone wants to do another mathlib bump, please go ahead. Otherwise, I'll do it later today.

Johan Commelin (Jun 15 2021 at 05:00):

I will also try to PR

    93 src/for_mathlib/homological_complex.lean
    56 src/for_mathlib/homotopy.lean

today

Johan Commelin (Jun 15 2021 at 06:34):

Ooh, looks like Scott already did the first file :smiley:

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

#7491 is the 2nd file

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

I'm starting the mathlib bump now

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

Done. That was easy.

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

Probably there is more that can be cleaned up from recent PRs, but the project compiles with latest mathlib.

Filippo A. E. Nuccio (Jun 16 2021 at 07:41):

I can go on making both kronecker and linear_algebra land into mathlib, if that has not already been done.

Filippo A. E. Nuccio (Jun 16 2021 at 16:19):

Created #7963 for for_mathlib/finsupp.lean (in LTE the sum_ version is needed, in the PR I have created the prod_ and marked @additive)

Filippo A. E. Nuccio (Jun 16 2021 at 16:20):

Also, I am done with a PR for for_mathlib/linear_algebra.lean but I have noticed the the lemma reindex_linear_equiv_sum_empty_symm is never used, so I am wondering whether to PR it as well. I have created a branch of lean-liquid to test the whole project with the above lemma commented.

Johan Commelin (Jun 16 2021 at 16:21):

If we no longer use that lemma, feel free to leave it out of the PR. It's quite specialized.

Eric Wieser (Jun 16 2021 at 16:26):

I think I made a (now-merged) PR to change the API around reindex_linear_equiv a while ago, and my intent was that in most cases the lemmas just be stated about docs#matrix.reindex and the linear_equiv version be unfolded before applying more lemmas

Eric Wieser (Jun 16 2021 at 16:27):

Maybe that was the wrong choice, and it's easier to just copy every lemma about reindex

Filippo A. E. Nuccio (Jun 16 2021 at 16:30):

You mean that every lemma should somehow follow from the reindex version?

Eric Wieser (Jun 16 2021 at 16:30):

Yes, I think so

Filippo A. E. Nuccio (Jun 16 2021 at 16:31):

I will give it a try.

Eric Wieser (Jun 16 2021 at 16:32):

Any lemma where the equality is between matrices should have a proof which is just exact the_reindex_lemma

Eric Wieser (Jun 16 2021 at 16:33):

Or possibly even exact the_minor_lemma

Filippo A. E. Nuccio (Jun 16 2021 at 16:35):

Oh sure, you mean to pass from a lemma about two reindexing equivalence being equal and the application of the equality to a matrix? I agree.

Filippo A. E. Nuccio (Jun 16 2021 at 16:37):

I will try to implement these ideas in the PR.

Filippo A. E. Nuccio (Jun 16 2021 at 17:22):

Johan Commelin said:

If we no longer use that lemma, feel free to leave it out of the PR. It's quite specialized.

Indeed, it is not used; I'll leave it out.

Johan Commelin (Jun 29 2021 at 06:52):

Big thanks to everyone who's been helping with making PRs to mathlib!

Here's the latest status of for_mathlib/:

     3 src/for_mathlib/int_norm.lean
     8 src/for_mathlib/int_basic.lean
    14 src/for_mathlib/nat_abs.lean
    18 src/for_mathlib/simplicial/augmented.lean
    19 src/for_mathlib/arrow/split.lean
    20 src/for_mathlib/nnreal.lean
    21 src/for_mathlib/finite.lean
    21 src/for_mathlib/quotient.lean
    34 src/for_mathlib/tsum.lean
    48 src/for_mathlib/is_locally_constant.lean
    54 src/for_mathlib/wide_pullback.lean
    60 src/for_mathlib/normed_group.lean
    64 src/for_mathlib/simplicial/iso.lean
    65 src/for_mathlib/order.lean
    74 src/for_mathlib/discrete_quotient.lean
    87 src/for_mathlib/Cech/adjunction.lean
    89 src/for_mathlib/finite_free.lean
    90 src/for_mathlib/kronecker.lean
    90 src/for_mathlib/normed_group_hom.lean
    92 src/for_mathlib/normed_group_hom_equalizer.lean
   118 src/for_mathlib/Profinite/compat_discrete_quotient.lean
   122 src/for_mathlib/Profinite/clopen_limit.lean
   126 src/for_mathlib/data_setoid_partition.lean
   160 src/for_mathlib/SemiNormedGroup_Completion.lean
   161 src/for_mathlib/simplicial/complex.lean
   210 src/for_mathlib/normed_group_hom_completion.lean
   227 src/for_mathlib/Cech/split.lean
   283 src/for_mathlib/SemiNormedGroup.lean
   316 src/for_mathlib/Profinite/arrow_limit.lean
   382 src/for_mathlib/free_abelian_group.lean
   565 src/for_mathlib/rational_cones.lean
   593 src/for_mathlib/nnrat.lean
   634 src/for_mathlib/Gordan.lean
  4868 total

Filippo A. E. Nuccio (Jun 29 2021 at 06:56):

What is the small blue number on the left?

Kevin Buzzard (Jun 29 2021 at 06:58):

Number of lines in the file?

Filippo A. E. Nuccio (Jun 29 2021 at 06:58):

Oh, well, the 3 in src/for_mathlib/int_norm.lean would have never made me guess so. Not a huge one...

Filippo A. E. Nuccio (Jun 29 2021 at 06:59):

(I was thinking at number of occurrences of some other file in the repository to a certain file, or something like this)

Johan Commelin (Jun 29 2021 at 13:59):

#8117 takes care of 3 src/for_mathlib/int_norm.lean

Johan Commelin (Jun 29 2021 at 14:09):

#8118 takes care of src/for_mathlib/int_basic.lean

Johan Commelin (Jun 29 2021 at 14:26):

#8120 and #8121 take care of src/for_mathlib/nat_abs.lean

Patrick Massot (Jun 29 2021 at 14:29):

Are you sure I didn't do that already?

Johan Commelin (Jun 29 2021 at 14:29):

No

Johan Commelin (Jun 29 2021 at 14:30):

I completely lost track of what has been done :oops: :see_no_evil:

Patrick Massot (Jun 29 2021 at 14:31):

The one I did about nat_abs is #7911

Johan Commelin (Jun 29 2021 at 14:34):

I see. But that one is different from what I did. There are too many stupid lemmas about nat_abs (-;

Adam Topaz (Jun 29 2021 at 14:34):

We have docs#real.norm_eq_abs and docs#complex.norm_eq_abs so it's probably okay to have the int version as well

Johan Commelin (Jun 29 2021 at 19:20):

A bit of progress:

     8 src/for_mathlib/int_basic.lean
    10 src/for_mathlib/finite.lean
    14 src/for_mathlib/nat_abs.lean
    18 src/for_mathlib/simplicial/augmented.lean
    19 src/for_mathlib/arrow/split.lean
    20 src/for_mathlib/nnreal.lean
    34 src/for_mathlib/tsum.lean
    45 src/for_mathlib/is_locally_constant.lean
    54 src/for_mathlib/wide_pullback.lean
    60 src/for_mathlib/normed_group.lean
    64 src/for_mathlib/simplicial/iso.lean
    65 src/for_mathlib/order.lean
    74 src/for_mathlib/discrete_quotient.lean
    87 src/for_mathlib/Cech/adjunction.lean
    89 src/for_mathlib/finite_free.lean
    90 src/for_mathlib/kronecker.lean
    90 src/for_mathlib/normed_group_hom.lean
    92 src/for_mathlib/normed_group_hom_equalizer.lean
   118 src/for_mathlib/Profinite/compat_discrete_quotient.lean
   122 src/for_mathlib/Profinite/clopen_limit.lean
   160 src/for_mathlib/SemiNormedGroup_Completion.lean
   161 src/for_mathlib/simplicial/complex.lean
   210 src/for_mathlib/normed_group_hom_completion.lean
   227 src/for_mathlib/Cech/split.lean
   270 src/for_mathlib/free_abelian_group.lean
   283 src/for_mathlib/SemiNormedGroup.lean
   316 src/for_mathlib/Profinite/arrow_limit.lean
   565 src/for_mathlib/rational_cones.lean
   593 src/for_mathlib/nnrat.lean
   634 src/for_mathlib/Gordan.lean
  4592 total

Eric Rodriguez (Jun 29 2021 at 22:35):

for_mathlib/augmented.lean seems to already be in mathlib here

Adam Topaz (Jun 29 2021 at 22:43):

Thanks! I'll get rid of it

Johan Commelin (Jul 01 2021 at 19:06):

Adam brought us under < 4500

     8 src/for_mathlib/nat_abs.lean
    19 src/for_mathlib/arrow/split.lean
    20 src/for_mathlib/nnreal.lean
    34 src/for_mathlib/tsum.lean
    45 src/for_mathlib/is_locally_constant.lean
    60 src/for_mathlib/normed_group.lean
    64 src/for_mathlib/simplicial/iso.lean
    65 src/for_mathlib/order.lean
    74 src/for_mathlib/discrete_quotient.lean
    85 src/for_mathlib/Cech/adjunction.lean
    89 src/for_mathlib/finite_free.lean
    90 src/for_mathlib/kronecker.lean
    90 src/for_mathlib/normed_group_hom.lean
    92 src/for_mathlib/normed_group_hom_equalizer.lean
   118 src/for_mathlib/Profinite/compat_discrete_quotient.lean
   122 src/for_mathlib/Profinite/clopen_limit.lean
   160 src/for_mathlib/SemiNormedGroup_Completion.lean
   161 src/for_mathlib/simplicial/complex.lean
   210 src/for_mathlib/normed_group_hom_completion.lean
   227 src/for_mathlib/Cech/split.lean
   270 src/for_mathlib/free_abelian_group.lean
   283 src/for_mathlib/SemiNormedGroup.lean
   295 src/for_mathlib/Profinite/arrow_limit.lean
   565 src/for_mathlib/rational_cones.lean
   593 src/for_mathlib/nnrat.lean
   634 src/for_mathlib/Gordan.lean
  4473 total

Adam Topaz (Jul 01 2021 at 19:07):

A big chunk of for_mathlib/Profinite/arrow_limit is about how limits commute with the Cech nerve construction, which should be done more generally if/when it's added to mathlib. I'll try to do that at some point soon.

Adam Topaz (Jul 01 2021 at 19:08):

Didn't the stuff from free_abelian_group get merged?

Johan Commelin (Jul 01 2021 at 19:08):

half of it

Adam Topaz (Jul 01 2021 at 19:08):

ah

Johan Commelin (Jul 01 2021 at 19:08):

the other half is actually quite specific, and I'm not sure if it should go to mathlib :see_no_evil:

Johan Commelin (Jul 03 2021 at 07:11):

Could someone please take a look at #8136 ? I think it's ready for merging.

Riccardo Brasca (Jul 08 2021 at 16:52):

@Johan Commelin do you want to PR finite_free.lean? Otherwise I can do it tomorrow.

Johan Commelin (Jul 08 2021 at 16:58):

@Riccardo Brasca I think that Scott has some ideas how to simplify the contents, see also https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/free.20module/near/243507549

Riccardo Brasca (Jul 08 2021 at 17:00):

Ah let's wait for him then

Patrick Massot (Jul 15 2021 at 08:27):

I tried to bump mathlib to handle my PR from yesterday but there are now errors in the new stuff, starting with:

/home/pmassot/lean/liquid/src/condensed/proetale_site.lean:31:30: error: type mismatch at application
  CompHaus.mk punit
term
  punit
has type
  Sort ? : Type ?
but is expected to have type
  Top : Type (u+1)

Eric Rodriguez (Jul 15 2021 at 08:28):

looks related to #8134 #8314 (numbers are not cooperating with me this morning...)

Johan Commelin (Jul 15 2021 at 11:25):

Did you get any further here? Can you push your fixes to a branch, then I can work on whatever remains.

Patrick Massot (Jul 15 2021 at 11:29):

Are you asking me? I didn't try to go further. I just pushed to bump-normed, but my work is trivial: remove one file and remove all corresponding import lines.

Johan Commelin (Jul 15 2021 at 11:46):

@Patrick Massot Thanks. I've fixed the remaining errors, and pushed to master.

Patrick Massot (Jul 15 2021 at 11:49):

About other PRs, I opened #8317 which should be rather easy to review. I'm currently contemplating the tsum file that you wrote. I can see you forced your way there, but clearly that's not quite the right way to do it. I think there are lemmas in mathlib's tsum file that are stated and proved for groups and should be about cancellative monoids. So I think PRing this file is pointless, there should be more changes in mathlib.

Johan Commelin (Jul 15 2021 at 11:58):

I can certainly believe that I didn't do the tsum stuff in the right generality

Johan Commelin (Jul 15 2021 at 12:05):

I left a review on #8317

Patrick Massot (Jul 15 2021 at 12:17):

Thanks. Your questions there prove I may have been too lazy by not tackling an older issue: topology.algebra.group_completion is ancient. It does not feature bundled group homs.

Patrick Massot (Jul 15 2021 at 12:18):

And I think we still don't have bundled continuous group homs. LTE jumped directly to bundled normed groups homs.

Patrick Massot (Jul 15 2021 at 12:18):

Specifically I mean https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/group_completion.lean#L97-L98

Johan Commelin (Jul 15 2021 at 12:18):

Hmm, do we want bundled continuous group homs?

Johan Commelin (Jul 15 2021 at 12:19):

It's not clear to me when continuity should or should not be bundled.

Patrick Massot (Jul 15 2021 at 12:22):

For now we could turn those lemmas into lemmas taking as input a bundled group hom and a continuity assumption and output a bundled group hom and an extra lemma asserting continuity.

Patrick Massot (Jul 15 2021 at 12:36):

I'll think I'll do that, so let's put that PR on hold. For the nnreal sum lemmas, it seems the right conditions to make it work are a bit tricky, and there may be no example beyond subtypes of topological groups, so maybe that the correct generality. I clearly won't have time for that soon, so let's say we shouldn't PR that tsum file for now.

Johan Commelin (Jul 15 2021 at 12:37):

Ok, feel free to copy-paste your thoughts at the top of that file.

Riccardo Brasca (Jul 15 2021 at 14:43):

I've just bumped mathlib. for_mathlib/normed_group_hom_equalizer.lean is gone.

Riccardo Brasca (Jul 29 2021 at 10:00):

Now that #7628 is merged, I think that part of for_mathlib/SemiNormedGroup.lean can be removed. I tried to do it, but I wasn't able to do it. In particular, with f : A ⟶ B and A B : SemiNormedGroup, if I write category_theory.limits.cokernel f I get

failed to synthesize type class instance for
A B : SemiNormedGroup,
f : A ⟶ B
⊢ limits.has_cokernel f

and I don't know how to use docs#SemiNormedGroup.category_theory.limits.has_cokernels to prove it. This is surely because I am not use to category theory in mathlib...

Johan Commelin (Jul 29 2021 at 10:48):

@Scott Morrison Do you have some time to look at this maybe?

Filippo A. E. Nuccio (Jul 29 2021 at 11:01):

Skimming through for_mathlib, I have seen the files discrete_quotient (by @Adam Topaz ) and is_locally_constant (by @Patrick Massot ) and they both look quite short and easy to integrate directly in mathlib. Is there any specific reason why they're still there, or can I try to merge them?

Patrick Massot (Jul 29 2021 at 11:18):

On my side there is a very clear reason. I started to PR stuff in this direction but I met so much obstruction from Eric Wieser that I gave up.

Adam Topaz (Jul 29 2021 at 12:22):

@Riccardo Brasca I can take a look at the cokernel thing this morning. Where does the error occur?

Riccardo Brasca (Jul 29 2021 at 12:26):

Everything compiles with the latest mathlib. But in for_mathlib/SemiNormedGroup.lean there is

section cokernels

variables {A B C : SemiNormedGroup.{u}}

/-- The cokernel of a morphism of seminormed groups. -/
@[simp]
noncomputable
def coker (f : A ⟶ B) : SemiNormedGroup := SemiNormedGroup.of $
  quotient_add_group.quotient f.range

/-- The projection onto the cokernel. -/
@[simp]
noncomputable
def coker.π {f : A ⟶ B} : B ⟶ coker f :=
f.range.normed_mk

(and other lemmas) that I think are useless now that we have docs#SemiNormedGroup.category_theory.limits.has_cokernels. In particular, LTE uses now its own cokernel and not mathlib's one.

Riccardo Brasca (Jul 29 2021 at 12:28):

It's possible that in LTE we want the "standard" cokernel, meaning the one in SemiNormedGroup₁, I am not sure.

Riccardo Brasca (Jul 29 2021 at 12:28):

(deleted)

Adam Topaz (Jul 29 2021 at 12:28):

Ah I see. I think those may need to stick around. The cokernels you get as a colimit from the category theory library don't give you any control over the norms (since you can compose with an isomorphism which rescaled the norm).

Adam Topaz (Jul 29 2021 at 12:30):

But I'll try to get rid of that code and see what breaks

Johan Commelin (Jul 29 2021 at 12:33):

Ooh yes, it's the norm issue again.

Riccardo Brasca (Jul 29 2021 at 12:40):

Maybe what we want is something like cokernel₁, the image of the cokernel in SemiNormedGroup₁ under the forgetful functor. This is a cokernel in SemiNormedGroup, so it should be possible to use all the general results, but moreover it has a nice norm.

Filippo A. E. Nuccio (Jul 29 2021 at 12:44):

Patrick Massot said:

On my side there is a very clear reason. I started to PR stuff in this direction but I met so much obstruction from Eric Wieser that I gave up.

Oh, I see. Do you have the PR number so I can have a look?

Eric Wieser (Jul 29 2021 at 12:45):

I think Patrick is referring to #7910 which is now merged? Sorry for the friction there, I tried to alleviate it by making the changes Bhavik and I were asking for myself rather than burdening you with them.

Johan Commelin (Jul 29 2021 at 12:46):

Riccardo Brasca said:

Maybe what we want is something like cokernel₁, the image of the cokernel in SemiNormedGroup₁ under the forgetful functor. This is a cokernel in SemiNormedGroup, so it should be possible to use all the general results, but moreover it has a nice norm.

But you can only do this for norm-nonincreasing maps. So it's not a solution for the generic morphism.

Riccardo Brasca (Jul 29 2021 at 12:48):

Ah, of course

Patrick Massot (Jul 29 2021 at 12:49):

Yes #7910 was the main one in this direction. Unfortunately the fact that it is now merge doesn't mean the next one won't be bikeshed to death.

Adam Topaz (Jul 29 2021 at 13:00):

Defining the cokernels as a bounded colimit of some sort would probably solve the issue, but the infrastructure around that doesn't exist so I don't think it's worth it.

Adam Topaz (Jul 29 2021 at 13:02):

@Filippo A. E. Nuccio I just added for_mathlib/discrete_quotient a couple of days ago, which is why it's still there. Feel free to make a mathlib PR with that, if you would like.

Riccardo Brasca (Jul 29 2021 at 13:08):

I can be very wrong, but I now think that SemiNormedGroup (I mean, the category) is something that will be rarely used outside LTE. Someone doing analysis will absolutely not care about the fact the the kernel of a continuous linear map is the equalizer of something. And the fact that the natural map from the kernel can not preserve the norm is ridiculous for an analyst. So in my opinion what should go to mathlib is something like f.cokernel where f : normed_group_hom A B. Note that for kernel and range we already have that

Riccardo Brasca (Jul 29 2021 at 13:10):

Concretely this means that for_mathlib/SemiNormedGroup.lean should go to mathlib, independently of #7268

Filippo A. E. Nuccio (Jul 29 2021 at 13:10):

Just one small thought: with all the Liquid philosophy, isn't it possible that at a certain point people doing analysis will start caring about something being an equalizer?

Riccardo Brasca (Jul 29 2021 at 13:13):

I am not sure :grinning_face_with_smiling_eyes:

Riccardo Brasca (Jul 29 2021 at 13:15):

Seriously, doing analysis, the kernel is one particular model of the equalizer, not any equalizer. It's really a non categorical notion

Filippo A. E. Nuccio (Jul 29 2021 at 13:16):

You mean that you can put several equivalent norms on an equalizer to end up with several objects and the kernel is one choice?

Riccardo Brasca (Jul 29 2021 at 13:18):

Yes, if f : normed_group_hom A B you can put the "natural" norm on ker f and multiply it by 37. This is still a kernel

Filippo A. E. Nuccio (Jul 29 2021 at 13:18):

Yes, yes, I agree and I see your point.

Adam Topaz (Jul 29 2021 at 13:26):

This was exactly what these semi_normed_category gadgets were supposed to solve.

Adam Topaz (Jul 29 2021 at 14:08):

Well, it looks like the immediate error that @Riccardo Brasca ran into is due to some universe nonsense. E.g. this works: 

instance foo : _root_.category_theory.limits.has_cokernels SemiNormedGroup.{u} :=
SemiNormedGroup.category_theory.limits.has_cokernels.{u u}

example (f : A ⟶ B) : SemiNormedGroup := category_theory.limits.cokernel f

Adam Topaz (Jul 29 2021 at 14:09):

We should probably add some universe annotations to the definition of this instance in mathlib

Filippo A. E. Nuccio (Jul 29 2021 at 14:53):

Adam Topaz said:

Filippo A. E. Nuccio I just added for_mathlib/discrete_quotient a couple of days ago, which is why it's still there. Feel free to make a mathlib PR with that, if you would like.

Done! #8464.

Adam Topaz (Jul 29 2021 at 16:29):

#8467 fixes the universe issue and adds some API for an explicit cokernels in SemiNormedGroup which has the desired norm properties.

Filippo A. E. Nuccio (Aug 04 2021 at 11:34):

I've just bumped mathlib. for_mathlib/discrete_quotient.lean is gone.

Riccardo Brasca (Sep 07 2021 at 12:37):

for_mathlib/normed_group_hom_completion.lean is gone (it was already in mathlib).

Riccardo Brasca (Sep 07 2021 at 12:50):

If everybody agrees I am going to PR for_mathlib/finite_free.lean (after generalization). The relevant results are

lemma module.finite.of_basis {ι : Type*} [fintype ι] (b : basis ι R M) : module.finite R M

instance [nontrivial R] [module.finite R M] [module.free R M] :
  fintype (module.free.choose_basis_index R M)

instance : module.finite ℤ (M →+ ℤ) :=

instance : module.free ℤ (M →+ ℤ) :=

I think the original plan was to wait for some refactor of finite/finite_dimensional, but I think we can just have these results in mathlib and doing the refactor later.

Johan Commelin (Sep 07 2021 at 12:53):

That refactor has been done. (Anne refactored basis: now it's a bundled map.)

Johan Commelin (Sep 07 2021 at 12:53):

So please go ahead!

Scott Morrison (Mar 08 2022 at 07:30):

I wonder if lean-liquid needs a really_for_mathlib folder, containing the stuff that is already polished and nice, and just needs someone to make a PR.

Scott Morrison (Mar 08 2022 at 07:30):

I was just having another look through today (fearing that I was doing something that already existed....)

Scott Morrison (Mar 08 2022 at 07:30):

and there is a lot of stuff which I would hit bors merge on right away!

Johan Commelin (Mar 08 2022 at 07:35):

Yeah, we should probably organize another sprint. But I'm very short on time these days.

Johan Commelin (Mar 08 2022 at 07:36):

All the free time that I have, I want to spend on finishing LTE.

Scott Morrison (Mar 12 2022 at 06:24):

You can delete for_mathlib/endomorphisms.lean. It is already in mathlib as karoubi.

Scott Morrison (Mar 12 2022 at 06:26):

(and apparently not used in lean-liquid at present)

Scott Morrison (Mar 12 2022 at 07:46):

(deleted)

Johan Commelin (Mar 12 2022 at 07:48):

@Scott Morrison It is indeed not used. And we will not need it. But it's not the same as karoubi, right? Because we don't require that the endomorphism is idempotent.

Scott Morrison (Mar 12 2022 at 07:48):

Oh, you're right, I'm not paying attention sorry.

Scott Morrison (Mar 12 2022 at 07:49):

I seem to remember having made exactly this same mistake previously, actually.

Scott Morrison (Mar 12 2022 at 07:49):

:face_palm:

Last updated: Dec 20 2023 at 11:08 UTC