## Stream: Is there code for X?

#### Riccardo Brasca (Apr 14 2021 at 15:26):

Do we have something like the following?

import algebra.monoid_algebra

lemma submonoid.closure.to_add_submonoid {M : Type*} [monoid M] (S : set M) :


I am not even sure this is the correct way of stating what I want: the multiplicative submonoid generated by S is the same as the additive submonoid generated by S inside additive M.

#### Adam Topaz (Apr 14 2021 at 15:30):

We must have the equivalence between the lattice of submomoids of M and the subadditivemonoids of additive M.

#### Adam Topaz (Apr 14 2021 at 15:31):

IIRC the subfoo generated by a set is usually defined as an Inf in such lattices

#### Damiano Testa (Apr 14 2021 at 15:34):

I recently added a proof that the additive closure of a multiplicative submonoid is a subsemiring. However, I am not sure that this is what you are asking...

#### Riccardo Brasca (Apr 14 2021 at 15:35):

There is docs#submonoid.add_submonoid_equiv, but I don't see anything relating the two lattices

#### Eric Wieser (Apr 14 2021 at 15:38):

It seems like we're missing

lemma submonoid.to_add_submonoid_coe {M : Type*} [monoid M] (S : submonoid M) :
begin
rw equiv.image_eq_preimage,
ext,
refl
end


#### Eric Wieser (Apr 14 2021 at 15:44):

golfed:

lemma submonoid.to_add_submonoid_coe {M : Type*} [monoid M] (S : submonoid M) :
eq.symm (set.image_id S)


#### Riccardo Brasca (Apr 14 2021 at 15:49):

Thank's! I will prove my lemma by hand :unamused:

#### Scott Morrison (Apr 14 2021 at 23:19):

Surely it makes more sense to prove the equivalence of lattices first?

#### Riccardo Brasca (Apr 15 2021 at 07:40):

Yes, that's the way I did it. It's from the LTE, here
https://github.com/leanprover-community/lean-liquid/blob/riccardobrasca/src/toric/theorem2.lean
I am going to PR all of this.

Last updated: May 16 2021 at 05:21 UTC