principal submodules

Stream: new members

[Damiano Testa]

Dear All,

I am trying to work with ideals generated by a single element, but I am having issues getting Lean to realize that they are principal. More specifically, I suspect that the issue is that Lean does not recognize the element that I use to define the ideal to be the generator guaranteed by the is_principal property. I am aware of the existence of this lemma (in /src/ring_theory/principal_ideal_domain.lean), which is what I would like to apply:

lemma mem_iff_eq_smul_generator {R : Type u} [comm_ring R] (S : submodule R R) [S.is_principal] {x : R} :
  x ∈ S ↔ ∃ s : R, x = s • submodule.is_principal.generator S :=
by simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]

and this is my attempt

import algebra.module.basic
import ring_theory.principal_ideal_domain

universe u

lemma myprinc  {R : Type u} [comm_ring R] {x g : R} :
  x ∈ (submodule.span R {g} : submodule R R) → ∃ s : R, x = s • g :=
begin
    intro sh,
    let Rg : ideal R := (submodule.span R {g} : submodule R R),
    have : submodule.is_principal Rg,
        {
            refine {principal := _},
            use g,
        },
--  library_search fails
    sorry,
end

[Reid Barton]

Try haveI?

[Reid Barton]

(Why is is_principal a class anyways?)

[Damiano Testa]

Reid Barton said:

Try haveI?

Do you mean to simply type haveI to try to finish the goal?

[Damiano Testa]

I get an error:

'«:=»' expected

[Reid Barton]

instead of have. But now I think you might need letI

[Damiano Testa]

(I suspect that you are underestimating my incompetence with Lean... ahahaa)

I understand what you meant now!

[Reid Barton]

actually no, it is a Prop so haveI should be fine, but the proof still won't work

[Damiano Testa]

I tried with letI after, as Reid Barton said, haveI did not work. It still does not find a solution with library_search, but now the output makes me suspect that Lean knows what generator I am talking about

[Reid Barton]

Damiano Testa said:

More specifically, I suspect that the issue is that Lean does not recognize the element that I use to define the ideal to be the generator guaranteed by the is_principal property.

Yes, generator is just some arbitrary choice of generator and you can't force it to be your g, so the lemma doesn't apply.

[Damiano Testa]

Reid Barton said:

Damiano Testa said:

More specifically, I suspect that the issue is that Lean does not recognize the element that I use to define the ideal to be the generator guaranteed by the is_principal property.

Yes, generator is just some arbitrary choice of generator and you can't force it to be your g, so the lemma doesn't apply.

Ok, this sucks, though...

[Reid Barton]

it's not a problem, just use a different lemma

[Reid Barton]

for example mem_span_singleton which appears in its proof looks relevant

[Damiano Testa]

I will keep trying, but I have failed with many lemmas...

[Damiano Testa]

in particular, the mwe produced above might work with mem_span_singleton, but I am not sure that the actual instance that I have will

[Damiano Testa]

I need to see

[Johan Commelin]

@Damiano Testa Want to share your screen and prove this together?

[Damiano Testa]

sure, but I will not be able to talk while sharing the screen, since my computer does not have a mic

[Damiano Testa]

(also, where do you want to share my screen?)

[Johan Commelin]

Aha... let's see how it goes... you could write a chat in the comment blocks

[Damiano Testa]

(I should say: I am able to talk, just you will not be able to listen to me...)

[Damiano Testa]

for the record: the mwe could be solved as follows

lemma myprinc {x s : R} :
  s ∈ (submodule.span R ({x} : set R)) → ∃ r : R, s = r • x :=
-- x ∣ s :=
begin
rw submodule.mem_span_singleton,
simp only [eq_comm],
exact id,
end

thanks to all who pointed me towards the right lemma!