Zulip Chat Archive

Stream: condensed mathematics

Topic: bumping mathlib


view this post on Zulip Johan Commelin (Jan 27 2021 at 16:16):

If someone feels like it, we can bump mathlib and get access to lean-3.26.0.

view this post on Zulip Johan Commelin (Jan 27 2021 at 16:16):

The lean-3.24.0 branch should stay on the final commit that uses that version of lean. And we can create a new lean-3.26.0 branch to track the new version.

view this post on Zulip Johan Commelin (Jan 27 2021 at 16:17):

I'll have dinner first (-;

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:25):

:warning: done

view this post on Zulip Johan Commelin (Jan 27 2021 at 17:26):

so make sure to run leanproject get-mathlib-cache after git pulling

view this post on Zulip Damiano Testa (Feb 22 2021 at 09:18):

Johan and I just bumped mathlib

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 10:01):

Nice! Did you also do it for the toric branch? That might get rid of the red x.

view this post on Zulip Johan Commelin (Feb 22 2021 at 10:44):

yup, we are working on toric right now

view this post on Zulip Johan Commelin (Feb 22 2021 at 10:45):

and it has a :check: now on github

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 11:14):

Nice! I'm still working on the is_scalar_tower issue. From a ring-theoretic perspective the issue is simple: if R is an A-algebra and M, N are two R-modules then Hom_R(M,N) is an R-algebra and an A-algebra and we are missing the is_scalar_tower instance which guarantees that the two actions coincide (A acts because is_scalar_tower A R N gives an A-action on Hom_R(M,N)). I tried to generalise this to A a monoid acting on a comm_semiring R blah blah blah you can guess the story, but Eric pointed out that something even more general is true: A can be a B-algebra and then the actions of A and B on Hom_R(M,N) are compatible. I've just got this working. Once 6331 is accepted, there's a random is_scalar_tower instance in toric.lean which can be removed (I just checked).

view this post on Zulip Johan Commelin (Feb 22 2021 at 11:28):

We just pushed a bunch of stuff

view this post on Zulip Johan Commelin (Feb 22 2021 at 11:28):

@Kevin Buzzard so be sure to pull (-;

view this post on Zulip Johan Commelin (Feb 23 2021 at 08:28):

I just did another mathlib bump, deleting 415 lines of stuff that has moved from the repo to mathlib

view this post on Zulip Johan Commelin (Feb 25 2021 at 13:45):

sorry, I broke the build in my previous push, it should be fixed now

view this post on Zulip Johan Commelin (Feb 26 2021 at 08:23):

I bumped mathlib and in the process bumped lean to 3.27.0c.
Be sure to leanproject get-mathlib-cache after pulling.

view this post on Zulip Adam Topaz (Feb 28 2021 at 06:08):

@Johan Commelin I have the defn of system_of_complexes.completion ready to push to master. Just double checking it's okay to bump mathlib in the process....

view this post on Zulip Adam Topaz (Feb 28 2021 at 06:30):

Okay, pushed.

view this post on Zulip Adam Topaz (Feb 28 2021 at 06:30):

With a mathlib bump!

view this post on Zulip Adam Topaz (Feb 28 2021 at 06:35):

Is there a webhook or something we can set up that will announce something every time leanpkg.toml is updated on master?

view this post on Zulip Johan Commelin (Mar 02 2021 at 07:04):

mathlib bump bumps mathlib

view this post on Zulip Johan Commelin (Mar 05 2021 at 05:03):

another bump, updates to the new filter.tendsto names after @Heather Macbeth fixed the namespace issue in mathlib

view this post on Zulip Johan Commelin (Mar 11 2021 at 21:06):

I made a trivial but nontrivial mathlib bump

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:03):

I've tried bumping mathlib, but there is a nasty error in breen_deligne/universal

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:03):

two instances for scalar multiplication are not defeq )-;

view this post on Zulip Johan Commelin (Mar 16 2021 at 19:03):

The rest of the fixes were quite straightforward. I have pushed to bump-mathlib

view this post on Zulip Johan Commelin (Mar 17 2021 at 07:51):

I've pushed to latest mathlib, and hence we are now on lean 3.28.0c.

There was one regression, in breen_deligne/universal.lean. I've commented that out for now.
universal_map_equiv_functorial_map is a huge monster of a declaration. @Kevin Buzzard would you mind taking a look? I guess it makes sense to cut it into 4 pieces or so.

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:15):

I'm looking now.

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:30):

Some default bub instance had changed to some new with_zero bub so I had to change some type class hackery. All the work is proofs, the definitions are small, I could factor out the four proofs if you like.

view this post on Zulip Johan Commelin (Mar 17 2021 at 10:31):

It just might be a bit easier to maintain that way

view this post on Zulip Damiano Testa (Mar 17 2021 at 10:33):

Ah, this might be the smul_with_zero class that I introduced? It caused (very) minor issues on mathlib, where some proofs required an extra rw smul_eq_mul, an extra by exact instead of a fully term-mode proof, or a convert instead of an exact.

I hope that the kind of fixes here were of a similar, small nature. Sorry for the extra work.

view this post on Zulip Damiano Testa (Mar 17 2021 at 10:34):

I can probably dig out the exact changes that were needed in 3 cases for the introduction, in case it helps: CI documented this pretty explicitly!

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:58):

It's OK, I fixed it already.

view this post on Zulip Johan Commelin (Mar 17 2021 at 11:00):

thanks!

view this post on Zulip Johan Commelin (Mar 25 2021 at 07:37):

Last night fact was made irreducible in mathlib:

$ git diff --stat
 leanpkg.toml                                      |  2 +-
 src/Mbar/Mbar_le.lean                             |  6 +++---
 src/Mbar/basic.lean                               |  8 ++++----
 src/Mbar/bounded.lean                             |  6 +++---
 src/combinatorial_lemma.lean                      |  2 +-
 src/facts/int.lean                                |  2 +-
 src/facts/nnreal.lean                             | 56 +++++++++++++++++++++++++++++++-------------------------
 src/facts/normed_group.lean                       |  2 +-
 src/locally_constant/Vhat.lean                    |  3 ++-
 src/normed_group/rescale.lean                     |  6 +++---
 src/normed_snake.lean                             |  8 ++++----
 src/normed_spectral.lean                          | 18 +++++++++---------
 src/polyhedral_lattice/Hom.lean                   |  2 +-
 src/polyhedral_lattice/cosimplicial.lean          |  6 ++++--
 src/polyhedral_lattice/pseudo_normed_group.lean   |  4 ++--
 src/polyhedral_lattice/rescale.lean               |  4 ++--
 src/pseudo_normed_group/Tinv.lean                 |  4 ++--
 src/pseudo_normed_group/basic.lean                |  2 +-
 src/pseudo_normed_group/profinitely_filtered.lean | 20 ++++++++++----------
 src/pseudo_normed_group/rescale.lean              |  4 ++--
 src/pseudo_normed_group/system_of_complexes.lean  |  8 ++++----
 src/pseudo_normed_group/with_Tinv.lean            |  2 +-
 src/system_of_complexes/basic.lean                | 23 ++++++++++++-----------
 src/system_of_complexes/completion.lean           | 26 ++++++++++++++------------
 src/system_of_complexes/double.lean               | 14 +++++++-------
 src/system_of_complexes/rescale.lean              | 10 +++++-----
 src/thm95/constants.lean                          | 10 +++++-----
 src/thm95/default.lean                            |  2 +-
 28 files changed, 136 insertions(+), 124 deletions(-)

view this post on Zulip Peter Scholze (Mar 25 2021 at 08:44):

How many faces does a 66-dimensional cube have? I think that's 363^6 -- a mere 729729. Ah, who would be afraid of that :-D

view this post on Zulip Johan Commelin (Apr 03 2021 at 13:37):

slightly non-trivial mathlib bump

view this post on Zulip Johan Commelin (Apr 13 2021 at 15:04):

I just bumped mathlib

view this post on Zulip Johan Commelin (Apr 15 2021 at 04:35):

I'm going to try bumping mathlib to the version that changes the definition of add_monoid. Wish me luck.

view this post on Zulip Johan Commelin (Apr 15 2021 at 04:51):

I've hit a first diamond:

 @eq.{u_1+1}
    (@add_monoid_hom.{u_1 0} Λ int
       (@add_monoid.to_add_zero_class.{u_1} Λ
          (@sub_neg_monoid.to_add_monoid.{u_1} Λ
             (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
       (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
    (@has_scalar.smul.{0 u_1} nat
       (@add_monoid_hom.{u_1 0} Λ int
          (@add_monoid.to_add_zero_class.{u_1} Λ
             (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
          (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
       (@smul_with_zero.to_has_scalar.{0 u_1} nat
          (@add_monoid_hom.{u_1 0} Λ int
             (@add_monoid.to_add_zero_class.{u_1} Λ
                (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                   (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
             (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
          (@mul_zero_class.to_has_zero.{0} nat
             (@monoid_with_zero.to_mul_zero_class.{0} nat (@semiring.to_monoid_with_zero.{0} nat nat.semiring)))
          (@add_zero_class.to_has_zero.{u_1}
             (@add_monoid_hom.{u_1 0} Λ int
                (@add_monoid.to_add_zero_class.{u_1} Λ
                   (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                      (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
             (@add_monoid.to_add_zero_class.{u_1}
                (@add_monoid_hom.{u_1 0} Λ int
                   (@add_monoid.to_add_zero_class.{u_1} Λ
                      (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                         (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                   (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                (@add_comm_monoid.to_add_monoid.{u_1}
                   (@add_monoid_hom.{u_1 0} Λ int
                      (@add_monoid.to_add_zero_class.{u_1} Λ
                         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                      (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                   (@add_monoid_hom.add_comm_monoid.{u_1 0} Λ int
                      (@add_monoid.to_add_zero_class.{u_1} Λ
                         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                      int.add_comm_monoid))))
          (@mul_action_with_zero.to_smul_with_zero.{0 u_1} nat
             (@add_monoid_hom.{u_1 0} Λ int
                (@add_monoid.to_add_zero_class.{u_1} Λ
                   (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                      (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
             (@semiring.to_monoid_with_zero.{0} nat nat.semiring)
             (@add_zero_class.to_has_zero.{u_1}
                (@add_monoid_hom.{u_1 0} Λ int
                   (@add_monoid.to_add_zero_class.{u_1} Λ
                      (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                         (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                   (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                (@add_monoid.to_add_zero_class.{u_1}
                   (@add_monoid_hom.{u_1 0} Λ int
                      (@add_monoid.to_add_zero_class.{u_1} Λ
                         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                      (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                   (@add_comm_monoid.to_add_monoid.{u_1}
                      (@add_monoid_hom.{u_1 0} Λ int
                         (@add_monoid.to_add_zero_class.{u_1} Λ
                            (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                               (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                         (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                      (@add_monoid_hom.add_comm_monoid.{u_1 0} Λ int
                         (@add_monoid.to_add_zero_class.{u_1} Λ
                            (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                               (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                         int.add_comm_monoid))))
             (@semimodule.to_mul_action_with_zero.{0 u_1} nat
                (@add_monoid_hom.{u_1 0} Λ int
                   (@add_monoid.to_add_zero_class.{u_1} Λ
                      (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                         (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                   (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                nat.semiring
                (@add_monoid_hom.add_comm_monoid.{u_1 0} Λ int
                   (@add_monoid.to_add_zero_class.{u_1} Λ
                      (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                         (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                   int.add_comm_monoid)
                (@add_monoid_hom.semimodule.{0 u_1 0} nat Λ int nat.semiring
                   (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                      (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1)))
                   int.add_comm_monoid
                   (@add_comm_monoid.nat_semimodule.{0} int int.add_comm_monoid)))))
       n
       f)
    (@has_scalar.smul.{0 u_1} nat
       (@add_monoid_hom.{u_1 0} Λ int
          (@add_monoid.to_add_zero_class.{u_1} Λ
             (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
          (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
       (@add_monoid.has_scalar_nat.{u_1}
          (@add_monoid_hom.{u_1 0} Λ int
             (@add_monoid.to_add_zero_class.{u_1} Λ
                (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                   (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
             (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
          (@sub_neg_monoid.to_add_monoid.{u_1}
             (@add_monoid_hom.{u_1 0} Λ int
                (@add_monoid.to_add_zero_class.{u_1} Λ
                   (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                      (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
             (@add_group.to_sub_neg_monoid.{u_1}
                (@add_monoid_hom.{u_1 0} Λ int
                   (@add_monoid.to_add_zero_class.{u_1} Λ
                      (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                         (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                   (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                (@add_comm_group.to_add_group.{u_1}
                   (@add_monoid_hom.{u_1 0} Λ int
                      (@add_monoid.to_add_zero_class.{u_1} Λ
                         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                      (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
                   (@add_monoid_hom.add_comm_group.{u_1 0} Λ int
                      (@add_monoid.to_add_zero_class.{u_1} Λ
                         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                      (@normed_group.to_add_comm_group.{0} int
                         (@normed_ring.to_normed_group.{0} int
                            (@normed_comm_ring.to_normed_ring.{0} int int.normed_comm_ring))))))))
       n
       f)

view this post on Zulip Johan Commelin (Apr 15 2021 at 05:02):

Weird...

import algebra.module.basic

variables (Λ : Type*) [add_comm_monoid Λ]

example :
  @smul_with_zero.to_has_scalar  (Λ →+ ) _ _ _
  =
  @add_monoid.has_scalar_nat (Λ →+ ) _
  := rfl

-- This just works

view this post on Zulip Johan Commelin (Apr 15 2021 at 05:06):

Hmmm, I might have found the issue. Some files just compiled fine, but are still causing trouble further down the road.

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:06):

MWE

import analysis.normed_space.basic

variables (Λ : Type*) [add_comm_group Λ]

example :
(@add_monoid_hom.semimodule.{0 u_1 0}
  nat Λ int nat.semiring
    (@sub_neg_monoid.to_add_monoid.{u_1} Λ
       (@add_group.to_sub_neg_monoid.{u_1} Λ
         (@add_comm_group.to_add_group.{u_1} Λ _inst_1)))
    int.add_comm_monoid
    (@add_comm_monoid.nat_semimodule.{0} int int.add_comm_monoid))
  =
(@add_comm_monoid.nat_semimodule.{u_1}
   (@add_monoid_hom.{u_1 0} Λ int
      (@add_monoid.to_add_zero_class.{u_1} Λ
         (@sub_neg_monoid.to_add_monoid.{u_1} Λ
            (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
      (@add_monoid.to_add_zero_class.{0} int int.add_monoid))
   (@add_monoid_hom.add_comm_monoid.{u_1 0} Λ int
                (@add_monoid.to_add_zero_class.{u_1} Λ
                   (@sub_neg_monoid.to_add_monoid.{u_1} Λ
                      (@add_group.to_sub_neg_monoid.{u_1} Λ (@add_comm_group.to_add_group.{u_1} Λ _inst_1))))
                int.add_comm_monoid))
  := rfl -- fails

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:06):

This probably requires a fix to mathlib

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:07):

I haven't debugged this further, but this is what diff told me

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:10):

It's the crucial diff in the pp.all of

import analysis.normed_space.basic

variables (Λ : Type*) [add_comm_group Λ]

example : mul_action_with_zero.to_smul_with_zero  (Λ →+ ) =
  add_monoid.to_smul_with_zero (Λ →+ ) := rfl -- fails

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:10):

The normed_space import is also important. If you replace it by module.basic then the rfl works

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 06:17):

When I've got my daughter out the door in about an hour I can look at this

view this post on Zulip Scott Morrison (Apr 15 2021 at 06:17):

and this is post #7084?

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:18):

Yes, I'm bumping the project to "post #7084 mathlib"

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:20):

Unfortunately, that PR also removed

instance add_comm_monoid.nat_semimodule.subsingleton : subsingleton (semimodule  M)

view this post on Zulip Scott Morrison (Apr 15 2021 at 06:20):

Did I write that once upon a time? I seem to remember that. :-)

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:25):

I think it should be brought back. At least as lemma, maybe as instance.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 06:28):

Isn't the idea that you're not supposed to put it back but instead are supposed to fix the bad instance by supplying a less pathological nat action?

view this post on Zulip Johan Commelin (Apr 15 2021 at 06:29):

That's why it maybe doesn't have to be an instance. But it would be nice if we could just use this decl as a tmp fix until mathlib is fixed.

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:27):

@Sebastien Gouezel Let me ping you here (-;

view this post on Zulip Johan Commelin (Apr 15 2021 at 07:27):

I haven't made progress yet...

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 07:39):

OK I've made it to my desk, I'll have a look

view this post on Zulip Sebastien Gouezel (Apr 15 2021 at 07:39):

Found it, and fixing it.

view this post on Zulip Sebastien Gouezel (Apr 15 2021 at 08:53):

#7201

view this post on Zulip Johan Commelin (Apr 15 2021 at 08:59):

Thanks a lot!

view this post on Zulip Johan Commelin (Apr 15 2021 at 09:16):

n ^ 0 is no longer defeq to 1... but I'm very very happy that 2 ^ 0 is still defeq to 1.

view this post on Zulip Johan Commelin (Apr 15 2021 at 09:22):

I used a hack in one file which can be removed once #7201 lands in mathlib.
For now, here's your latest mathlib bump:

 leanpkg.toml                                      |  2 +-
 src/Mbar/basic.lean                               |  7 +++----
 src/breen_deligne/category.lean                   | 13 +++++++------
 src/combinatorial_lemma.lean                      | 35 +++++++++++++++++------------------
 src/for_mathlib/add_monoid_hom.lean               |  9 +++++----
 src/polyhedral_lattice/basic.lean                 |  9 ++++-----
 src/polyhedral_lattice/cech.lean                  | 13 ++++---------
 src/polyhedral_lattice/direct_sum.lean            |  2 +-
 src/polyhedral_lattice/finsupp.lean               |  7 +++----
 src/polyhedral_lattice/int.lean                   |  2 +-
 src/pseudo_normed_group/profinitely_filtered.lean |  5 +++--
 src/rescale/basic.lean                            |  2 +-
 src/rescale/normed_group.lean                     |  2 +-
 src/rescale/polyhedral_lattice.lean               |  5 ++---
 src/toric/lem97.lean                              | 84 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------
 src/toric/module_regular.lean                     |  2 +-
 16 files changed, 111 insertions(+), 88 deletions(-)

view this post on Zulip Eric Wieser (Apr 15 2021 at 13:21):

I commented in the original PR that we probably don't want to delete that subsingleton instance, but it was after we'd already decided to merge

view this post on Zulip Johan Commelin (Apr 16 2021 at 03:54):

@Sebastien Gouezel I'm very happy to say that

-- TODO: remove this once a bug in mathlib is fixed
lemma hack : mul_action_with_zero.to_smul_with_zero  (Λ →+ ) =
  add_monoid.to_smul_with_zero (Λ →+ ) :=
begin
  sorry
end

can now be removed

view this post on Zulip Johan Commelin (Apr 26 2021 at 06:10):

I'm now bumping mathlib. We're in for some big changes (-;
The int-smul refactor has landed, and we no longer have semimodule.

view this post on Zulip Johan Commelin (Apr 26 2021 at 06:22):

I'm just going to do the minimal bump to make the project compile again. But once we are done, we should adjust the add_comm_group instance for Mbar so that it takes advantage of the new int-smul refactor.

view this post on Zulip Patrick Massot (Apr 26 2021 at 07:18):

The semimodule refactor shouldn't be too bad. I did in two projects and it was only a sed away.

view this post on Zulip Kevin Buzzard (Apr 26 2021 at 08:26):

There is one proof which is timing out but other than that the refactor seems to have gone well

view this post on Zulip Johan Commelin (Apr 26 2021 at 09:01):

I finished the mathlib bump. Just pushed to master.

view this post on Zulip Johan Commelin (Apr 26 2021 at 11:33):

I just refactored the add_comm_group instance on Mbar to make use of the new nsmul/gsmul-powers

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 18:51):

I just bumped mathlib so I could get to a couple of Eric Wieser's recent PR's

view this post on Zulip Johan Commelin (Apr 28 2021 at 18:52):

Thanks a lot!

view this post on Zulip Johan Commelin (Apr 28 2021 at 18:52):

I was just thinking about doing that :smiley:

view this post on Zulip Johan Commelin (May 03 2021 at 06:47):

FYI: I just bumped mathlib

view this post on Zulip Peter Scholze (May 03 2021 at 07:26):

Johan, you are working at crazy times!

view this post on Zulip Johan Commelin (May 03 2021 at 07:37):

Ooh, the mathlib bump was only 15 minutes. I didn't start early today (-;

view this post on Zulip Peter Scholze (May 03 2021 at 07:38):

Well, I meant your first messages to David ;-)

view this post on Zulip Patrick Massot (May 03 2021 at 07:39):

Johan works in a weird time zone which has nothing to do with its geographical time zone.

view this post on Zulip Patrick Massot (May 03 2021 at 07:39):

His dinner time is even weirder.

view this post on Zulip Johan Commelin (May 03 2021 at 07:41):

Ooh lol. 6:44... My son woke me up at 6:15.

view this post on Zulip Johan Commelin (May 03 2021 at 07:44):

@Patrick Massot My wife grew up in a village with a lot of industry and farms. On week days everyone there wakes up < 6:00 and starts work 7:00 - 7:30. They are all done between 16:00 and 17:00 and have dinner around 17:15. Be kind of stuck with that. (They might go back to work at 19:00...)

view this post on Zulip Johan Commelin (May 03 2021 at 07:44):

But my neighbour here in Germany works in road construction, and he seems to be on an even earlier schedule.

view this post on Zulip Peter Scholze (May 03 2021 at 07:48):

@David Michael Roberts While I did not follow the actual code being written, I tried to keep up with which parts of the argument have been formalized.

The (very) good news: To me, all the really critical parts of the argument have been formalized, the completion of the homotopy argument being the last sticking point. Of course, there's still a chance that there's a missing link somewhere... that seems unlikely to me, but we should definitely finish this formalization!

So what is missing in order to finish LTE? Well, first the few things Johan mentioned: Gordan's lemma, some lemmas about polyhedral lattices, and (and this is the most critical of those, regarding the actual checking of the argument) the line of arguments from 8.19 --> 9.2 --> checking the column exactness (condition (2) of 9.6) in the proof of 9.5. (all numbers refer to Analytic.pdf)

Once this is done, we have a full proof of 9.5, and 9.4. (By the way, there was a discussion about weak vs strong exactness: We need the version of 9.4 with strong exactness, so we need to leave some of this discussion about strong exactness in. But that's done, just don't delete it :wink:)

But LTE is about 9.1! So what still remains to be done is to prove the implication 9.4 => 9.1. This will require the development of quite a few basics that have just been accomplished (from what I understand): Defining the category of condensed abelian groups, defining Ext-groups in abelian categories, etc. Currently, I don't have a clear picture of how much work remains to be done to get the implication 9.4 => 9.1 to work. (But it is clear that no mistake can hide there.)

view this post on Zulip Peter Scholze (May 03 2021 at 07:50):

(Arguably, there's even another step, comparing the spaces of measures over Z((T))r\mathbb Z((T))_r with the measures Mp\mathcal M_p over R\mathbb R.)

view this post on Zulip Johan Commelin (May 03 2021 at 07:50):

I guess that other step will be third_target :rofl:

view this post on Zulip David Michael Roberts (May 03 2021 at 08:02):

@Peter Scholze ok, excellent. I thought I was missing something, and 9.4=>9.1 was it (I was being lazy and not checking Analytic.pdf line by line, just going on comments/discussion here).

So how are you feeling about all the fiddly explicit constants now, and the possibility you fooled yourself? I guess it's not over until it's over, but things are definitely looking firmer, no?

view this post on Zulip Johan Commelin (May 03 2021 at 08:04):

Well, as you can see from the sorry-list in the other thread, there are still 10 sorries in constants.lean.

view this post on Zulip Johan Commelin (May 03 2021 at 08:05):

So we certainly need to do a bit of work there.

view this post on Zulip Johan Commelin (May 03 2021 at 08:05):

And the Cech part of the proof of 9.5 (which is still to be done) does influence the constants a bit.

view this post on Zulip Johan Commelin (May 03 2021 at 08:05):

I don't expect any surprises, but I think I would rather do that part first, and then pin down the constants after that.

view this post on Zulip Johan Commelin (May 03 2021 at 15:25):

Just for the record: it's dinner time.


Last updated: May 09 2021 at 23:10 UTC