## Stream: Is there code for X?

### Topic: Multiplication of sets

#### Ashvni Narayanan (Nov 09 2020 at 17:54):

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 (Nov 09 2020 at 17:55):

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

#### Adam Topaz (Nov 09 2020 at 17:56):

Can you provide a #mwe ?

#### Adam Topaz (Nov 09 2020 at 17:57):

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

#### Ashvni Narayanan (Nov 09 2020 at 17:58):

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 (Nov 09 2020 at 18:00):

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 (Nov 09 2020 at 18:08):

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

#### Ashvni Narayanan (Nov 09 2020 at 18:08):

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 (Nov 09 2020 at 18:08):

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

#### Kevin Buzzard (Nov 09 2020 at 18:18):

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 (Nov 09 2020 at 19:14):

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

#### Eric Wieser (Nov 09 2020 at 20:55):

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 (Nov 09 2020 at 23:06):

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 (Nov 09 2020 at 23:07):

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

#### Eric Wieser (Nov 09 2020 at 23:09):

Nice generalizations, thanks

#### Eric Wieser (Nov 09 2020 at 23:11):

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

#### Floris van Doorn (Nov 09 2020 at 23:27):

I did it: #4960

Last updated: May 16 2021 at 05:21 UTC