Zulip Chat Archive

Stream: Is there code for X?

Topic: Multiplication of sets


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 09 2020 at 17:56):

Can you provide a #mwe ?

view this post on Zulip Adam Topaz (Nov 09 2020 at 17:57):

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

view this post on Zulip 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..

view this post on Zulip 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).

view this post on Zulip Reid Barton (Nov 09 2020 at 18:08):

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

view this post on Zulip Ashvni Narayanan (Nov 09 2020 at 18:08):

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.

view this post on Zulip Reid Barton (Nov 09 2020 at 18:08):

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

view this post on Zulip 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

view this post on Zulip Ashvni Narayanan (Nov 09 2020 at 19:14):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Nov 09 2020 at 23:07):

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

view this post on Zulip Eric Wieser (Nov 09 2020 at 23:09):

Nice generalizations, thanks

view this post on Zulip Eric Wieser (Nov 09 2020 at 23:11):

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

view this post on Zulip Floris van Doorn (Nov 09 2020 at 23:27):

I did it: #4960


Last updated: May 16 2021 at 05:21 UTC