Zulip Chat Archive

Stream: maths

Topic: quotient_module breakage


view this post on Zulip Kevin Buzzard (Sep 20 2018 at 18:01):

import data.set.basic
import linear_algebra.quotient_module

example (R : Type*) (S : set R) [ring S] : S :=
begin
  exact (4 : S)
end

/-

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
state:
R : Type ?,
S : set R,
_inst_1 : ring ↥S
⊢ ↥S

-/

What is going on here? If I remove the import of linear_algebra.quotient_module then this compiles fine. @Chris Hughes you thought about quotient module instances maybe -- do you know how to diagnose these things?

Related -- I have to ask here because I cannot diagnose the issue myself. I cannot read the trace.class_instances output and I would really love to be able to. For what it's worth, just before it chokes it looks like this gist (and it's quite funny, manifestly something has gone wrong and it's a nice change from the usual, it's not a loop, it's a recursive hell).

https://gist.github.com/kbuzzard/2582db6593c7b7467f3e0020909af467

view this post on Zulip Patrick Massot (Sep 20 2018 at 18:02):

nice picture

view this post on Zulip Patrick Massot (Sep 20 2018 at 18:03):

Could you give a more realistic example?

view this post on Zulip Patrick Massot (Sep 20 2018 at 18:03):

Is R actually a ring and S a subring?

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:03):

I don't understand why that would compile. If S is empty, it's trivial to get a contradiction from this.

view this post on Zulip Patrick Massot (Sep 20 2018 at 18:04):

Also note I had to modify stuff like this recently in the perfectoid project

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:12):

There's nothing wrong with the statement of the theorem. It is a set with a ring structure, which is therefore nonempty and has a 4

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:15):

As usual, modules are acting up because of the search for a ring instance

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 18:16):

Chris : you're happy with (x : nat) (h : x > 4), right? But if x was 2 it's trivial to get a contradiction from this.

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:16):

As long as it's a nonempty set there is a ring structure on it and a 4

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:17):

and being a ring implies it is nonempty

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 18:17):

Patrick -- it was trying to fix up the perfectoid project which led me to this. We need p in R^o for the definition to be OK. The statement that p divides something in R is vacuous because p is a unit in R -- R is like Q_p and R^o is like Z_p

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:17):

I don't think the offending instances are in quotient_module. Do you get the same problem with algebra.pi_instances and algebra.module?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:18):

anyway this is yet another problem that will be solved by my refactor

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 18:19):

OK, I can definitely wait. I was planning on spending tomorrow thinking about the perfectoid project in a top-down way; this issue came up because the definition of a perfectoid ring is currently broken :-)

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 18:30):

I'm having a day off real life tomorrow; my last day off for a while.

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:27):

Patrick -- it was trying to fix up the perfectoid project which led me to this. We need p in R^o for the definition to be OK. The statement that p divides something in R is vacuous because p is a unit in R -- R is like Q_p and R^o is like Z_p

I told you to carefully review that PR. I fixed the compilation error but I was really unsure I didn't change the maths

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:27):

I'm having a day off real life tomorrow; my last day off for a while.

Do you mean you'll have a Lean day or a no-Lean day?

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:30):

anyway this is yet another problem that will be solved by my refactor

Do you have any estimation about when this refactor will be ready for use?

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 19:36):

I am going to have a Lean day, but it's a bit cheeky -- I should really be doing other things.

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:37):

Do you have stuff you can do without modules? Do you want to have fun with uniform spaces?

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 19:38):

ha ha, I have been working from the bottom up during the little time I've had over the last month or so. I was going to try defining the presheaf on Spa(A), sorrying whatever I couldn't do.

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:38):

Great!

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:39):

It gets my vote


Last updated: May 18 2021 at 07:19 UTC