Zulip Chat Archive
Stream: condensed mathematics
Topic: bumping mathlib
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.
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.
Johan Commelin (Jan 27 2021 at 16:17):
I'll have dinner first (-;
Johan Commelin (Jan 27 2021 at 17:25):
:warning: done
Johan Commelin (Jan 27 2021 at 17:26):
so make sure to run leanproject get-mathlib-cache after git pulling
Damiano Testa (Feb 22 2021 at 09:18):
Johan and I just bumped mathlib
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.
Johan Commelin (Feb 22 2021 at 10:44):
yup, we are working on toric right now
Johan Commelin (Feb 22 2021 at 10:45):
and it has a :check: now on github
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).
Johan Commelin (Feb 22 2021 at 11:28):
We just pushed a bunch of stuff
Johan Commelin (Feb 22 2021 at 11:28):
@Kevin Buzzard so be sure to pull (-;
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
Johan Commelin (Feb 25 2021 at 13:45):
sorry, I broke the build in my previous push, it should be fixed now
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.
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....
Adam Topaz (Feb 28 2021 at 06:30):
Okay, pushed.
Adam Topaz (Feb 28 2021 at 06:30):
With a mathlib bump!
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?
Johan Commelin (Mar 02 2021 at 07:04):
mathlib bump bumps mathlib
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
Johan Commelin (Mar 11 2021 at 21:06):
I made a trivial but nontrivial mathlib bump
Johan Commelin (Mar 16 2021 at 19:03):
I've tried bumping mathlib, but there is a nasty error in breen_deligne/universal
Johan Commelin (Mar 16 2021 at 19:03):
two instances for scalar multiplication are not defeq )-;
Johan Commelin (Mar 16 2021 at 19:03):
The rest of the fixes were quite straightforward. I have pushed to bump-mathlib
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.
Kevin Buzzard (Mar 17 2021 at 10:15):
I'm looking now.
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.
Johan Commelin (Mar 17 2021 at 10:31):
It just might be a bit easier to maintain that way
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.
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!
Kevin Buzzard (Mar 17 2021 at 10:58):
It's OK, I fixed it already.
Johan Commelin (Mar 17 2021 at 11:00):
thanks!
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(-)
Peter Scholze (Mar 25 2021 at 08:44):
How many faces does a -dimensional cube have? I think that's -- a mere . Ah, who would be afraid of that :-D
Johan Commelin (Apr 03 2021 at 13:37):
slightly non-trivial mathlib bump
Johan Commelin (Apr 13 2021 at 15:04):
I just bumped mathlib
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.
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)
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
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.
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
Johan Commelin (Apr 15 2021 at 06:06):
This probably requires a fix to mathlib
Johan Commelin (Apr 15 2021 at 06:07):
I haven't debugged this further, but this is what diff told me
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
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
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
Scott Morrison (Apr 15 2021 at 06:17):
and this is post #7084?
Johan Commelin (Apr 15 2021 at 06:18):
Yes, I'm bumping the project to "post #7084 mathlib"
Johan Commelin (Apr 15 2021 at 06:20):
Unfortunately, that PR also removed
instance add_comm_monoid.nat_semimodule.subsingleton : subsingleton (semimodule ℕ M)
Scott Morrison (Apr 15 2021 at 06:20):
Did I write that once upon a time? I seem to remember that. :-)
Johan Commelin (Apr 15 2021 at 06:25):
I think it should be brought back. At least as lemma, maybe as instance.
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?
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.
Johan Commelin (Apr 15 2021 at 07:27):
@Sebastien Gouezel Let me ping you here (-;
Johan Commelin (Apr 15 2021 at 07:27):
I haven't made progress yet...
Kevin Buzzard (Apr 15 2021 at 07:39):
OK I've made it to my desk, I'll have a look
Sebastien Gouezel (Apr 15 2021 at 07:39):
Found it, and fixing it.
Sebastien Gouezel (Apr 15 2021 at 08:53):
Johan Commelin (Apr 15 2021 at 08:59):
Thanks a lot!
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.
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(-)
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
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
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.
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.
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.
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
Johan Commelin (Apr 26 2021 at 09:01):
I finished the mathlib bump. Just pushed to master.
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
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
Johan Commelin (Apr 28 2021 at 18:52):
Thanks a lot!
Johan Commelin (Apr 28 2021 at 18:52):
I was just thinking about doing that :smiley:
Johan Commelin (May 03 2021 at 06:47):
FYI: I just bumped mathlib
Peter Scholze (May 03 2021 at 07:26):
Johan, you are working at crazy times!
Johan Commelin (May 03 2021 at 07:37):
Ooh, the mathlib bump was only 15 minutes. I didn't start early today (-;
Peter Scholze (May 03 2021 at 07:38):
Well, I meant your first messages to David ;-)
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.
Patrick Massot (May 03 2021 at 07:39):
His dinner time is even weirder.
Johan Commelin (May 03 2021 at 07:41):
Ooh lol. 6:44... My son woke me up at 6:15.
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...)
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.
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.)
Peter Scholze (May 03 2021 at 07:50):
(Arguably, there's even another step, comparing the spaces of measures over with the measures over .)
Johan Commelin (May 03 2021 at 07:50):
I guess that other step will be third_target :rofl:
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?
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.
Johan Commelin (May 03 2021 at 08:05):
So we certainly need to do a bit of work there.
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.
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.
Johan Commelin (May 03 2021 at 15:25):
Just for the record: it's dinner time.
Johan Commelin (Jun 07 2021 at 09:58):
commit 86cfda45062f555f73efd9361ab9f35630f4a718 (HEAD -> master)
Author: Johan Commelin <johan@commelin.net>
Date: Mon Jun 7 09:57:21 2021 +0000
bump mathlib
leanpkg.toml | 2 +-
src/for_mathlib/Cech/adjunction.lean | 107 -------------------------------------------------------------------------------------------
src/for_mathlib/SemiNormedGroup.lean | 23 --------------------
src/for_mathlib/connected.lean | 14 ------------
src/for_mathlib/finite_free.lean | 2 +-
src/for_mathlib/grading_zero_subring.lean | 4 ++--
src/for_mathlib/homological_complex.lean | 34 -----------------------------
src/for_mathlib/nnrat.lean | 2 +-
src/for_mathlib/norm_nsmul.lean | 32 ---------------------------
src/for_mathlib/unused/to_int_linear_map.lean | 14 ------------
src/normed_spectral.lean | 5 +++--
src/polyhedral_lattice/quotient.lean | 4 +---
src/prop819.lean | 1 -
src/prop819/completion.lean | 13 ++++++-----
src/prop819/strict_complex_iso.lean | 4 ++--
src/prop_92/prop_92.lean | 5 +++--
src/thm95/col_exact.lean | 2 +-
src/thm95/col_exact_prep.lean | 2 --
18 files changed, 21 insertions(+), 249 deletions(-)
jmc@atarrimbo:~/data/math/lean-liquid$ git push
Enumerating objects: 47, done.
Kevin Buzzard (Jun 07 2021 at 10:21):
Note that the vast majority of the main is coming from for_mathlib. Well done Johan, thanks a lot for this.
Johan Commelin (Jun 07 2021 at 10:55):
Well, thanks to @Scott Morrison and @Adam Topaz for making a whole bunch of PRs out of for_mathlib
Last updated: Dec 20 2023 at 11:08 UTC