Additive/Multiplicative closure

Stream: Is there code for X?

[Riccardo Brasca]

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.

[Adam Topaz]

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

[Adam Topaz]

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

[Damiano Testa]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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)

[Riccardo Brasca]

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

[Scott Morrison]

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

[Riccardo Brasca]

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.