Zulip Chat Archive
Stream: condensed mathematics
Topic: toric branch issues
Kevin Buzzard (Apr 18 2021 at 20:46):
I know we have a toric thread already but this isn't about mathematics.
We have tedious infrastructure problems with the toric branch. My observation is that the workflows which seem to work in this project are the following: either incremental pushes to master, or bigger developments which take a while (maybe a week or two) to make but then get merged quickly into master. The toric branch is neither of these. It looks like it is not a branch which is designed for merging, it is a branch which is designed for experimentation and perhaps a future general theory of toric varieties. This is of course fine, but life moves on, and mathlib moves and the definition of a monoid changes, and now if you merge master into toric you get conflicts and a bunch of breakage. We have to decide the purpose of this branch, because it is beginning to rot and there is a whole heap of stuff in it which might be important for toric varieties but which is not important for the main goal, which is to prove the unique sorry in the file toric.lem97 on master. I was hoping to make progress on this today because we're now in good shape in terms of the formalisation: I am now sure that we have all the details of a maths proof, Filippo has reduced everything to Gordan, Eric and Damiano have proved to me that our definition of grading works, and Riccardo and Damiano have started on the details of the one missing proof. But we need this stuff in master. I had hoped to get it done by last week but we had some unexpected problems -- we have highly degraded internet right now and it takes me forever to download oleans so it's really difficult for me to switch between branches if they are on different mathlib commits, and I also had to spend a bunch of time hiring someone last week (we have a new number theory Lean post-doc at Imperial :D but I'll let them introduce themselves when they're ready). It is my top priority now to get this proof into master but I still didn't find the time to sort out the merge conflicts.
My proposal is to leave the toric branch for now, and start moving the stuff we need into master because now is a really good time to finish this part of the story. I should have time over the next few days to nail this but I am going to do the development on master because my main goal is to remove this sorry.
Riccardo Brasca (Apr 18 2021 at 20:51):
Concerning what I did (the monoid algebra is of finite type iff the monoid is finitely generated) I think it is suitable for mathlib and my plan is to PR it. In a few hours bors will have merged all the preliminary lemmas and I can start PRing the real theorem (probably tomorrow).
Kevin Buzzard (Apr 18 2021 at 21:14):
yes that's fine: we can access the theorem if it's in mathlib -- then you're PR'ing it upstream. What I'm worried about is the downstream stuff in the toric branch.
Damiano Testa (Apr 19 2021 at 05:41):
Kevin, sorry, I think that I had not merger master into toric after one of Sébastien's refactor of smul: I just did!
I thought that it was enough to keep merging master into toric to "maintain" it. Is that wrong? I can merge toric into master now, I think, since the merge of master into toric is done!
Johan Commelin (Apr 19 2021 at 05:45):
I just pushed another mathlib bump...
Kevin Buzzard (Apr 19 2021 at 06:29):
Damiano does it compile after the merge? Were there conflicts?
Damiano Testa (Apr 19 2021 at 06:58):
I am having trouble making the towards_Gordan file work: I have is_basis ℤ b as both a goal and as an assumption, but now it no longer works. Note that this had issues from the start: it worked for a bit, but no longer does.
Damiano Testa (Apr 19 2021 at 07:00):
Around this point is where the issue first arose, but was fixed for some time.
Damiano Testa (Apr 19 2021 at 07:04):
There is also a
s: submodule ℚ V
assumption and I am unable to close the goal
⊢ submodule ℤ V
Damiano Testa (Apr 19 2021 at 08:42):
I'm giving up: unfortunately, I had to comment out one of the proofs that Riccardo was able to provide, since I can no longer make it work. I am checking that the rest builds.
Damiano Testa (Apr 19 2021 at 08:57):
Ok, with the exception of the proof that has been problematic since the beginning, the toric branch is works.
Riccardo Brasca (Apr 19 2021 at 09:29):
I am having a look at it... I don't think I will be able to fix if Damiano wasn't but I am curious to see what doesn't work.
Filippo A. E. Nuccio (Apr 19 2021 at 09:30):
Yes, I am also looking into this - let's see.
Filippo A. E. Nuccio (Apr 19 2021 at 09:31):
I guess we're speaking about reduction_to_lattice, right?
Damiano Testa (Apr 19 2021 at 09:32):
Yes, it is reduction_to_lattice. The proof that used to work is commented.
Filippo A. E. Nuccio (Apr 19 2021 at 09:32):
Found it, yes.
Damiano Testa (Apr 19 2021 at 09:34):
On a side note, I have merged the toric branch into master and pushed it to github. This was not intended: my idea was to wait for confirmation that this was something desirable.
If you think that the branches toricand master should continue to run parallel, feel free to undo this merge: I tried doing this myself, but failed.
Kevin Buzzard (Apr 19 2021 at 09:34):
no, if you can fix it, that's great! I just saw conflicts and problems and began to ask myself what the point of the branch was.
Damiano Testa (Apr 19 2021 at 09:35):
Ok, so, on my machine, leanproject build worked on the master_with_toric_merged branch, modulo the single proof reduction_to_lattice. Let's see how CI deals with it!
Riccardo Brasca (Apr 19 2021 at 09:40):
I was able to fix the proof... indeed it was already working, but I was getting a timeout. I increased the limits and it works
Riccardo Brasca (Apr 19 2021 at 09:41):
I am investigating what is causing the timeout
Damiano Testa (Apr 19 2021 at 09:41):
How do you increase the limits of the timeouts? I either get the proofs working fast, or I look for shorter proofs...
Damiano Testa (Apr 19 2021 at 09:42):
Anyway, the toric branch with the commented proof is now merged into master, also on github.
Riccardo Brasca (Apr 19 2021 at 09:43):
It is in VS code (I think that if you compile from the command line there are no limits). Go to setting, search for lean and it is somewhere there
Filippo A. E. Nuccio (Apr 19 2021 at 09:45):
It could be around the linear_independent_iff'.mpr (λ t g hg i hi, _),, possibly. I tried also swapping a bit the goals (without increasing the timeout) and it seems to me that the timeout arises there.
Riccardo Brasca (Apr 19 2021 at 09:46):
elaboration: tactic execution took 24s
num. allocated objects: 5186
num. allocated closures: 5260
num. allocated big nums: 2
24045ms 100.0% tactic.istep
24045ms 100.0% tactic.step
24045ms 100.0% _interaction
24045ms 100.0% tactic.istep._lambda_1
24045ms 100.0% scope_trace
24045ms 100.0% _interaction._lambda_2
24004ms 99.8% tactic.solve1
23971ms 99.7% _interaction._lambda_3
23016ms 95.7% tactic.to_expr
22965ms 95.5% tactic.refine
813ms 3.4% interaction_monad_orelse
811ms 3.4% tactic.focus1
741ms 3.1% tactic.interactive.convert
740ms 3.1% tactic.try
722ms 3.0% tactic.congr'._main._lambda_1
634ms 2.6% tactic.congr_core'
623ms 2.6% tactic.apply_eq_congr_core
602ms 2.5% tactic.mk_specialized_congr_lemma
425ms 1.8% interaction_monad.monad._lambda_9
213ms 0.9% _private.423049959.all_goals'_core._main._lambda_2
213ms 0.9% tactic.all_goals'
213ms 0.9% all_goals'_core
212ms 0.9% rw_core
212ms 0.9% tactic.interactive.propagate_tags
211ms 0.9% interactive.loc.apply
211ms 0.9% interaction_monad.orelse'
208ms 0.9% tactic.rewrite_core
208ms 0.9% tactic.rewrite
192ms 0.8% _private.1221263889.rw_goal._lambda_2
192ms 0.8% tactic.rewrite_target
192ms 0.8% _private.1221263889.rw_goal._lambda_4
166ms 0.7% tactic.apply_core
98ms 0.4% tactic.apply
79ms 0.3% tactic.applyc
70ms 0.3% tactic.interactive.ext
70ms 0.3% tactic.ext_core._main._lambda_3
70ms 0.3% tactic.ext_core
70ms 0.3% tactic.ext1_core
70ms 0.3% tactic.ext
70ms 0.3% tactic.ext1_core._lambda_6
70ms 0.3% tactic.ext1_core._lambda_7
69ms 0.3% tactic.ext1_core._lambda_5
69ms 0.3% tactic.ext1_core._lambda_4
69ms 0.3% tactic.try_core
69ms 0.3% list.any_of
68ms 0.3% _private.2644768123.relation_tactic._lambda_1
68ms 0.3% tactic.ext1_core._lambda_3
68ms 0.3% relation_tactic
40ms 0.2% tactic.rcases._lambda_5
40ms 0.2% tactic.interactive.obtain
38ms 0.2% tactic.assumption._lambda_1
38ms 0.2% tactic.find_same_type
36ms 0.1% tactic.unify
36ms 0.1% tactic.find_same_type._main._lambda_1
33ms 0.1% _interaction._lambda_4
21ms 0.1% tactic.apply_congr_core
19ms 0.1% tactic.rewrite_hyp
19ms 0.1% _private.3791888571.rw_hyp._main._lambda_2
19ms 0.1% _private.3791888571.rw_hyp._main._lambda_3
19ms 0.1% rw_hyp
13ms 0.1% tactic.interactive.exact
10ms 0.0% tactic.apply_heq_congr_core
3ms 0.0% tactic.save_info_with_widgets
3ms 0.0% tactic.replace_target
3ms 0.0% tactic.mk_eq_mpr
3ms 0.0% tactic.infer_type
2ms 0.0% tactic.save_widget
2ms 0.0% tactic.rcases._lambda_2
1ms 0.0% tactic.assertv
1ms 0.0% tactic.rcases_core._main._lambda_7
1ms 0.0% tactic.cleanup
1ms 0.0% tactic.set_goals
1ms 0.0% tactic.rcases._lambda_3
1ms 0.0% _private.2177920635.rw_core._lambda_1
1ms 0.0% tactic.rcases_core._main._lambda_9
1ms 0.0% _private.1387917865.get_pi_arity_aux._main._lambda_1
1ms 0.0% tactic.rcases.process_constructors
1ms 0.0% tactic.save_info_thunk
1ms 0.0% tactic.mk_app
1ms 0.0% tactic.rcases_core._main._lambda_8
1ms 0.0% tactic.ext1_core._lambda_1
1ms 0.0% expr.local_const
1ms 0.0% tactic.interactive.replace._lambda_1
1ms 0.0% tactic.get_arity
1ms 0.0% tactic.exact
1ms 0.0% get_pi_arity_aux
1ms 0.0% tactic.rcases.continue
1ms 0.0% tactic.mk_id_eq
1ms 0.0% tactic.rcases_core._main._lambda_5
1ms 0.0% declaration.univ_params
1ms 0.0% tactic.rcases.continue._main._lambda_4
1ms 0.0% tactic.get_pi_arity
1ms 0.0% tactic.rcases_core
1ms 0.0% tactic.interactive.have._lambda_1
1ms 0.0% tactic.mk_const
Riccardo Brasca (Apr 19 2021 at 09:51):
I think the problem is by convert hb.2. If you put sorry there everything works pretty fast.
Sebastien Gouezel (Apr 19 2021 at 09:51):
Instead of refine, try to do some apply with the right number of underscores.
Sebastien Gouezel (Apr 19 2021 at 09:52):
(I got pretty good at speeding up proofs without understanding what they were doing, so if you give me a pointer I may have a look :-)
Damiano Testa (Apr 19 2021 at 09:53):
Sébastien, the problematic proof is here:
Thank you very much for your interest!
Damiano Testa (Apr 19 2021 at 09:53):
Riccardo, thanks! I think that I found it: it is currently at 100000, which I would have thought was a large number... :wink:
Riccardo Brasca (Apr 19 2021 at 09:53):
I am not completely sure, but I think it's this line that is problematic
https://github.com/leanprover-community/lean-liquid/blob/d001d927182ed5adf98f983befe51a4bd0d5e09d/src/toric/towards_Gordan.lean#L75
Riccardo Brasca (Apr 19 2021 at 09:54):
ops, I didn't see Damiano's message
Filippo A. E. Nuccio (Apr 19 2021 at 09:54):
Yes, I agree with @Riccardo Brasca that the issue seems to come from the convert hb.2.
Riccardo Brasca (Apr 19 2021 at 09:54):
Indeed exact hb.2 should work... but it doesn't
Damiano Testa (Apr 19 2021 at 09:54):
Ok, my pointer was to the whole proof, not to a specific line.
Damiano Testa (Apr 19 2021 at 09:55):
Note that even exact hb looks like it should work...
Filippo A. E. Nuccio (Apr 19 2021 at 09:55):
It really seems a diamond issue to me, no?
Damiano Testa (Apr 19 2021 at 09:59):
Also, the uncommented proof builds with leanproject build on my machine, but does not sit well with CI.
Riccardo Brasca (Apr 19 2021 at 10:01):
If I do exact hb.2 I get an error has type... but it is expected to have type.... The ... are of course extremely long, but here is a diff of the two types
25,30c25
< @submodule.span ℤ V
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@add_comm_group.to_add_comm_monoid V _inst_1)
---
> @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
33,36c28
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
---
> (@ring.to_semiring ℤ int.ring)
62,67c54
< @submodule.span ℤ V
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@add_comm_group.to_add_comm_monoid V _inst_1)
---
> @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
94,99c81
< @submodule.span ℤ V
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@add_comm_group.to_add_comm_monoid V _inst_1)
---
> @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
102,113c84
< (@submodule.restricted_module ℤ ℤ V
< (@comm_ring.to_comm_semiring ℤ
< (@integral_domain.to_comm_ring ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@algebra.id ℤ
< (@comm_ring.to_comm_semiring ℤ
< (@integral_domain.to_comm_ring ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
---
> (@submodule.restricted_module ℤ ℤ V int.comm_semiring int.semiring (@algebra_int ℤ int.ring)
140,145c111
< @submodule.span ℤ V
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@add_comm_group.to_add_comm_monoid V _inst_1)
---
> @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
173,178c139
< @submodule.span ℤ V
< (@ring.to_semiring ℤ
< (@domain.to_ring ℤ
< (@integral_domain.to_domain ℤ
< (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))))
< (@add_comm_group.to_add_comm_monoid V _inst_1)
---
> @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
Sebastien Gouezel (Apr 19 2021 at 10:03):
This is exactly the kind of thing that #7255 is supposed to fix. I would just accept the fact that this proof is super-slow for now, and wait for #7255 to land.
Filippo A. E. Nuccio (Apr 19 2021 at 10:03):
(deleted)
Filippo A. E. Nuccio (Apr 19 2021 at 10:04):
Riccardo Brasca said:
If I do
exact hb.2I get an errorhas type... but it is expected to have type.... The...are of course extremely long, but here is adiffof the two types25,30c25 < @submodule.span ℤ V < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@add_comm_group.to_add_comm_monoid V _inst_1) --- > @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1) 33,36c28 < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) --- > (@ring.to_semiring ℤ int.ring) 62,67c54 < @submodule.span ℤ V < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@add_comm_group.to_add_comm_monoid V _inst_1) --- > @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1) 94,99c81 < @submodule.span ℤ V < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@add_comm_group.to_add_comm_monoid V _inst_1) --- > @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1) 102,113c84 < (@submodule.restricted_module ℤ ℤ V < (@comm_ring.to_comm_semiring ℤ < (@integral_domain.to_comm_ring ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring))) < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@algebra.id ℤ < (@comm_ring.to_comm_semiring ℤ < (@integral_domain.to_comm_ring ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) --- > (@submodule.restricted_module ℤ ℤ V int.comm_semiring int.semiring (@algebra_int ℤ int.ring) 140,145c111 < @submodule.span ℤ V < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@add_comm_group.to_add_comm_monoid V _inst_1) --- > @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1) 173,178c139 < @submodule.span ℤ V < (@ring.to_semiring ℤ < (@domain.to_ring ℤ < (@integral_domain.to_domain ℤ < (@linear_ordered_comm_ring.to_integral_domain ℤ int.linear_ordered_comm_ring)))) < (@add_comm_group.to_add_comm_monoid V _inst_1) --- > @submodule.span ℤ V int.semiring (@add_comm_group.to_add_comm_monoid V _inst_1)
Yes, that's why I was thinking at diamonds.
Damiano Testa (Apr 19 2021 at 10:05):
Ok, I am happy with the strategy of leaving the proof in, commented out and, after each mathlib bump, I can try to remove the comments and see if it builds
Johan Commelin (Apr 19 2021 at 10:05):
Presumably #7255 will land fairly soon.
Damiano Testa (Apr 19 2021 at 10:19):
Ok, my last push to master has been with the proof commented out and there are no further issues.
Once #7255 gets merged into mathlib and bumped into lean-liquid, I will uncomment the proof and give CI another chance!
Damiano Testa (Apr 19 2021 at 10:19):
Thank you all for your support!
Kevin Buzzard (Apr 19 2021 at 10:25):
Thanks for taking this on!
Riccardo Brasca (Apr 19 2021 at 10:28):
I am compiling #7255 inside my local lean_liquid to see if this works (I am not sure I am doing it the right way, but let's see)
Damiano Testa (Apr 19 2021 at 10:30):
Riccardo, I am curious to see what happens on your computer.
When I do leanproject build on master, with the proof that was there already, lean clearly spends some time on reduction_to_lattice, but then moves on without flagging anything. I do not know why the remote CI has issues with it.
Riccardo Brasca (Apr 19 2021 at 10:34):
I went to _target/deps/mathlib and I checked out gsmul_data, that is the mathlib branch of #7255. Now I am doing leanproject build. I hope that once this is finished I will have this version of mathlib in the lean-liquid project. Note that I use Lean on my university machine through SSH, so I don't care if I have to compile it
Riccardo Brasca (Apr 19 2021 at 11:51):
I recompiled mathlib but the proof is still slow. I am not sure I've done this correctly, so this can be my fault.
Riccardo Brasca (Apr 19 2021 at 11:53):
We can probably just wait :grinning:
Damiano Testa (Apr 19 2021 at 12:46):
Thanks a lot for the report, Riccardo!
Sebastien Gouezel (Apr 19 2021 at 13:44):
It probably means that there is a diamond I forgot to solve. If you have a #mwe for mathlib, I can investigate now, or we can wait for #7255 to be merged and investigate then.
Riccardo Brasca (Apr 19 2021 at 14:22):
Here is a working example. Note that I am not sure that the problem is coming from something related to what are you working on and not from submodule.exists_is_basis_of_le_span. It is possible that this is coming from rational vs integer coefficients. I tried to make up a smaller example, without submodule.exists_is_basis_of_le_span, but the problem disappeared.
import linear_algebra.free_module
variables {V ι : Type*} [add_comm_group V] [semimodule ℚ V] [fintype ι] {v : ι → V}
lemma reduction_to_lattice (s : submodule ℚ V) (bv : is_basis ℚ v) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
obtain ⟨n, b, hb⟩ :=
submodule.exists_is_basis_of_le_span (_ : linear_independent ℤ v) inf_le_right,
{ refine ⟨n, b, _, _⟩,
replace hb := hb.1,
refine linear_independent_iff'.mpr (λ t g hg i hi, _),
rw [linear_independent_iff'] at hb,
refine hb t g _ i hi,
convert hg,
ext i,
erw [submodule.coe_smul_of_tower, submodule.coe_smul_of_tower, algebra_map_smul],
{ sorry } },
{ refine linear_independent.restrict_scalars_algebras _ bv.1,
exact λ a b ab, int.cast_inj.mp ab }
end
In your branch gsmul_data. If you replace the sorry with convert hb.2 it works, but it takes a lot of time.
Sebastien Gouezel (Apr 19 2021 at 16:51):
Your problem is that you have an algebra_int and an algebra.id, giving two different ℤ-algebra structures on ℤ. This is unfortunately another problem than what #7255 solves (well, it solves half of the problem, but not all of it). See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.237084/near/234455219 for a discussion of precisely this issue.
Sebastien Gouezel (Apr 19 2021 at 16:54):
Here is a fixed proof disabling locally this instance:
import linear_algebra.free_module
variables {V ι : Type*} [add_comm_group V] [semimodule ℚ V] [fintype ι] {v : ι → V}
local attribute [- instance] algebra_int
lemma reduction_to_lattice (s : submodule ℚ V) (bv : is_basis ℚ v) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
apply submodule.exists_is_basis_of_le_span (_ : linear_independent ℤ v) inf_le_right,
letI : algebra ℤ ℚ := algebra_int _,
refine linear_independent.restrict_scalars_algebras _ bv.1,
exact λ a b ab, int.cast_inj.mp ab
end
All the dance you had to convert stuff disappears, as you can see.
Sebastien Gouezel (Apr 19 2021 at 17:38):
Or better, by adjusting the instance priority:
import linear_algebra.free_module
variables {V ι : Type*} [add_comm_group V] [semimodule ℚ V] [fintype ι] {v : ι → V}
local attribute [instance, priority 99] algebra_int
lemma reduction_to_lattice (s : submodule ℚ V) (bv : is_basis ℚ v) :
∃ (n : ℕ) (vn : fin n → s.restrict_scalars ℤ ⊓ submodule.span ℤ (set.range v)),
is_basis ℤ vn :=
begin
apply submodule.exists_is_basis_of_le_span (_ : linear_independent ℤ v) inf_le_right,
refine linear_independent.restrict_scalars_algebras _ bv.1,
exact λ a b ab, int.cast_inj.mp ab
end
It might be worth doing it in mathlib master, if it doesn't break anything.
Damiano Testa (Apr 19 2021 at 18:59):
Sébastien, thank you very much for unwinding this problem!
Damiano Testa (Apr 19 2021 at 19:38):
The slow proof now works great!
Sébastien: thanks again!
Sebastien Gouezel (Apr 19 2021 at 19:41):
I have adjusted the priorities of algebra_int in the most recent version of #7255, so hopefully you shouldn't have anything special to do on your side once it is merged.
Riccardo Brasca (Apr 26 2021 at 20:05):
@Damiano Testa have you has a look at this now that #7255 has been merged? Otherwise I can try to do it
Damiano Testa (Apr 27 2021 at 07:27):
@Riccardo Brasca I have not tried to fix the toric branch after #7255. Also, I have had a conversation with Kevin where I think that he told me that whatever was needed from this branch to get the algebraic version of Gordan's lemma working is already on master. This takes some pressure off the toric branch.
I would still like to port this stuff to mathlib, but I will probably not have the time to do so soon. If you feel like bumping toric, I would be very grateful! However, as I mentioned, this may not be strictly necessary for the liquid application.
Kevin Buzzard (Apr 27 2021 at 07:47):
Yes, everything from the toric branch which is needed for the algebraic proof of Gordan is now merged into master and as far as I'm concerned the branch can be deleted from the project and parts relevant for toric geometry in general can be ultimately moved into mathlib
Last updated: Dec 20 2023 at 11:08 UTC