decidable_eq in quotient module

Stream: new members

[Jack J Garzella]

Hello,

I'm trying to formalize the statement of Nakayama's Lemma, part (8) in the link. I'm struggling with the hypothesis "the images of $x_1, \ldots, x_n$ generate $M/IM$". My attempt is to use finset M for the set $x_1, \ldots, x_n$, and the #mwe looks like this:

 lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
(hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (S : finset M)
-- here is the hypothesis I can't quite figure out
(hIM : submodule.span (R ⧸ I) ↑(S.image (@submodule.quotient.mk R M _ _ _ (I • (⊤ : submodule R M)))) =
(⊤ : submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M)))))
-- end hypothesis I can't figure out
: (submodule.span R ↑S = (⊤ : submodule R M)) := sorry

The error says failed to synthesize type class instance for ... ⊢ decidable_eq (M ⧸ I • ⊤).
Where did decidability come into the picture for this statement about modules? And how do I convince lean that whatever needs to be decidable is indeed decidable and/or is there a better way to formalize this assumption?

[Alex J. Best]

Try open_locale classical before your lemma

[Adam Topaz]

(deleted)

[Adam Topaz]

(deleted)

[Adam Topaz]

Sorry, I missed that you wanted statement (8)

[Adam Topaz]

Anyway, it's probably better to formulate the finitely-generated assumption using docs#module.finite

[Adam Topaz]

Alex J. Best said:

Try open_locale classical before your lemma

This should work, or alternatively you can try to add the necessary decidable_eq assumptions needed by docs#finset.image

[Adam Topaz]

At least on my end, it seems that Lean is also unhappy about $M/I \cdot M$ being an $R/I$-module. Is this in some import that I'm missing?

[Eric Wieser]

Can you make that mwe a #mwe? It doesn't have any imports or variables, so lean doesn't understand any of it!

[Junyan Xu]

Maybe you can use docs#set.finite instead of docs#finset; docs#set.image doesn't require decidable_eq. If you want to do induction there is docs#set.finite.induction_on.

[Jack J Garzella]

Eric Wieser said:

Can you make that mwe a #mwe? It doesn't have any imports or variables, so lean doesn't understand any of it!

So sorry, looks like I forgot to paste the top of the file. Edited now so it should actually be a #mwe

[Jack J Garzella]

Adam Topaz said:

At least on my end, it seems that Lean is also unhappy about $M/I \cdot M$ being an $R/I$-module. Is this in some import that I'm missing?

This seems to be hidden in algebra.module.torsion, see for example here. See also updated the original post.

[Eric Wieser]

Replacing with set.image makes your error go away

[Eric Wieser]

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

open ideal

lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
  (hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (S : finset M)
  -- here is the hypothesis I can't quite figure out
  (hIM : submodule.span (R ⧸ I) (submodule.quotient.mk '' ↑S) =
    (⊤ : submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M))))) :
  -- end hypothesis I can't figure out
  submodule.span R ↑S = (⊤ : submodule R M) := sorry