heartbeats w/ modules over ring quotients

Stream: new members

[Paul Nelson]

This code gives the error "failed to synthesize Module (R ⧸ P) (R ⧸ P)", which goes away if I increase the heartbeat limit substantially. Is there anything obvious that I'm doing wrong?

import Mathlib

-- set_option synthInstance.maxHeartbeats 1000000
-- set_option trace.Meta.synthInstance true in
-- set_option trace.profiler true in
example
  (R : Type) [CommRing R]
  (P : Ideal R) (hP : Ideal.IsMaximal P)
  : 0 = 0 := by
  letI h : Field (R ⧸ P) := Ideal.Quotient.field P
  let M : Submodule (R ⧸ P) (R ⧸ P) := ⊤
  sorry

I can fix this example by swapping the order of the two lines in the proof, but in more complicated situations it would be nice not to have to do that.

[Riccardo Brasca]

To fix it you can do something like

import Mathlib

-- set_option synthInstance.maxHeartbeats 1000000
-- set_option trace.Meta.synthInstance true in
-- set_option trace.profiler true in
example
  (R : Type) [CommRing R]
  (P : Ideal R) (hP : Ideal.IsMaximal P)
  : 0 = 0 := by
  letI h : Field (R ⧸ P) := Ideal.Quotient.field P
  letI ring := Semiring.toModule (R := R ⧸ P)
  let M : Submodule (R ⧸ P) (R ⧸ P) := ⊤
  sorry

[Riccardo Brasca]

But of course this shouldn't happen in the first place. We are aware of these kinds of issues, even if this one looks a little different from the usual ones.

@Matthew Ballard do you recognize a known problem here?

[Riccardo Brasca]

Ah, wait

[Riccardo Brasca]

It is because of the line

letI h : Field (R ⧸ P) := Ideal.Quotient.field P

[Riccardo Brasca]

If you erase it everything is instantaneous. The point is that you are defining a new field structure on R ⧸ P, and now Lean has to realize that the ring induced by this field structure is the same as the original one. I think this is the part that takes a lot of time.

[Riccardo Brasca]

You may use docs#IsField via docs#Ideal.Quotient.maximal_ideal_iff_isField_quotient, but it depends on what you want to prove.

[Paul Nelson]

This arises in a situation where I would like to apply a theorem about modules over fields to say something about more general rings, via passage to quotients by maximal ideals. The theorem that I would like to apply has [Field k] in its hypotheses.

[Matthew Ballard]

There is something suboptimal with Field. I’ll poke at later today.

[Paul Nelson]

Thanks.

it sounds like Ricardo’s suggestion is that I could rewrite the theorem I’m applying to have [CommRing k] (h : IsField k) as its hypothesis?

[Kevin Buzzard]

Yeah but if we think like that then the conclusion is that we should have two versions of every theorem involving a field (and 2^n versions of every theorem involving n fields), which doesn't sound good...

[Kevin Buzzard]

It's better to fix the problem than to work around it.

[Riccardo Brasca]

@Paul Nelson I was suggesting that maybe in your case you can find a workaround using IsField, but of course what you did with Field should 100% work. I think the problem comes from

protected noncomputable def field (I : Ideal R) [hI : I.IsMaximal] : Field (R ⧸ I) :=
  { Quotient.commRing I, Quotient.groupWithZero I with }

that is still the Lean3 way of defining things.

[Riccardo Brasca]

The point is that the way algebraic structures are handled by Lean changed completely between Lean 3 and Lean 4, and even if in theory we can still follow the Lean 3 style, sometimes things become very slow. Here Lean has troubles in checking (the mathematically obvious fact) that the ring induced the field structure is the ring structure you started with. This is because the field structure is defined in a way that is adapted to the Lean 3 way, and we should change it.

We become aware of this during the port, and we fixed the most problematic definition, but not all of them.

[Paul Nelson]

Many thanks for the clarifications

[Riccardo Brasca]

In practice you have to wait a couple of days (maybe a couple of hours) and we will fix the problem. Let me see if I can do something.

[Riccardo Brasca]

#9855 seems enough

[Kevin Buzzard]

I was going to suggest

@[reducible]
protected noncomputable def field (I : Ideal R) [hI : I.IsMaximal] : Field (R ⧸ I) :=
  { toCommRing := Quotient.commRing I
    inv := (Quotient.groupWithZero I).inv
    mul_inv_cancel := (Quotient.groupWithZero I).mul_inv_cancel
    inv_zero := (Quotient.groupWithZero I).inv_zero }
#align ideal.quotient.field Ideal.Quotient.field

Is yours better? Yours still has a let in but I'm now confused about how bad they are. Hmm, I timed them both and they're the same.

[Riccardo Brasca]

I honestly don't know, I just copied how the field instance is defined on AdjointRoot because I remember we spent quite a lot of time on that one

[Kevin Buzzard]

Eric's comment on the PR is beyond my pay grade.