Zulip Chat Archive

Stream: Is there code for X?

Topic: Additive/Multiplicative closure


view this post on Zulip 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) :
  (submonoid.closure S).to_add_submonoid = add_submonoid.closure (additive.of_mul '' S) := sorry

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.

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

view this post on Zulip Adam Topaz (Apr 14 2021 at 15:31):

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

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

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

view this post on Zulip 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) :
  (S.to_add_submonoid : set (additive M)) = additive.of_mul '' S :=
begin
  rw equiv.image_eq_preimage,
  ext,
  simp only [submonoid.to_add_submonoid, set_like.mem_coe],
  refl
end

view this post on Zulip Eric Wieser (Apr 14 2021 at 15:44):

golfed:

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

view this post on Zulip Riccardo Brasca (Apr 14 2021 at 15:49):

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

view this post on Zulip Scott Morrison (Apr 14 2021 at 23:19):

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

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