Multiplication of sets

Stream: Is there code for X?

[Ashvni Narayanan]

I have

↑q' * ↑q ⊆ {1}

where q and q' are submodules, and the coe lifts them to sets. I want to turn it into

↑(q' * q) ⊆ {1}

I can't seem to find anything of the form coe_mul. Any help is appreciated, thank you!

Edit : It turns out that Lean automatically converts ↑(q' * q) into ↑q' * ↑q. However, I don't see why this is true for submodules.

[Eric Wieser]

In this case Ithink you can just use change ↑(_ * _) ⊆ _ and lean will rewrite along definitions for you

[Adam Topaz]

Can you provide a #mwe ?

[Adam Topaz]

What is the multiplication of submodules? (I assume these are fractional ideals, or something?)

[Ashvni Narayanan]

Eric Wieser said:

In this case Ithink you can just use change ↑(_ * _) ⊆ _ and lean will rewrite along definitions for you

It remains the same..

[Ashvni Narayanan]

Ashvni Narayanan said:

Eric Wieser said:

In this case Ithink you can just use change ↑(_ * _) ⊆ _ and lean will rewrite along definitions for you

It remains the same..

If I write it as ((q' * q) : set _) ⊆ _ , it remains unchanged, however it gives me an error if I use ↑(q' * q) ⊆ {1} instead (I presume that this is because coe is unspecified in this case).

[Reid Barton]

I think you want ((q' * q) : submodule _ _), perhaps with a second cast to set _ if required

[Ashvni Narayanan]

Adam Topaz said:

Can you provide a #mwe ?

https://github.com/leanprover-community/mathlib/blob/5c5c302d2e4e539990e77b68781d024249c50442/src/ring_theory/dedekind_domain.lean#L334

This isn't an mwe, but it is what I am working with.

[Reid Barton]

(Or (q' * q : submodule _ _))

[Kevin Buzzard]

If there is a multiplication defined on set X where X is an R-algebra then it will presumably be pointwise multiplication, and hence will not agree with multiplication of submodules, which will be the submodule generated by the set multiplication

[Ashvni Narayanan]

I managed to get rid of subsets and am working in submodules. Thank you!

[Eric Wieser]

I'm running into something very similar now - is there a lemma like

lemma mul_subset_closure {A : Type*} [monoid A] (s : set A) : s * s ⊆ submonoid.closure s :=
begin
    rw set.subset_def,
    intros x hx,
    rw submonoid.mem_coe,
    obtain ⟨p, q, hp, hq, rfl⟩ := set.mem_mul.mp hx,
    exact submonoid.mul_mem _ (submonoid.subset_closure hp) (submonoid.subset_closure hq),
  end

somewhere in mathlib? If not, is that a suitable name?

[Floris van Doorn]

I would use this:

import algebra.module.submodule algebra.pointwise

open set
namespace submonoid

lemma mul_subset {M : Type*} [monoid M] {s t : set M} {S : submonoid M}
  (hs : s ⊆ S) (ht : t ⊆ S) : s * t ⊆ S :=
by { rintro _ ⟨p, q, hp, hq, rfl⟩, exact submonoid.mul_mem _ (hs hp) (ht hq) }

lemma mul_subset_closure {A : Type*} [monoid A] {s t u : set A}
  (hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ submonoid.closure u :=
mul_subset (subset.trans hs submonoid.subset_closure) (subset.trans ht submonoid.subset_closure)

end submonoid

If you also want the lemma you mentioned, I would call it mul_self_subset_closure.

[Floris van Doorn]

To answer your question explicitly: no, I don't think these lemmas are in mathlib.

[Eric Wieser]

Nice generalizations, thanks

[Eric Wieser]

Would you be willing to PR those, or would you prefer to leave that to me?

[Floris van Doorn]

I did it: #4960