submonoid.map_closure

Stream: Is there code for X?

[Nikolas Kuhn]

Do we have some result stating that the image of a submonoid generated by a set s under a monoid homomorphism is equal to the submonoid generated by the image of s ?

The statement should be something like this:

import group_theory.submonoid.operations

lemma submonoid.map_closure {M N : Type} [monoid M] [monoid N] (f: M →* N) (s  : set M) :
  (submonoid.closure s).map f = (submonoid.closure $ f '' s) :=
  sorry

[Andrew Yang]

I cannot find it either, but there is a one-liner

lemma submonoid.map_closure {M N : Type} [monoid M] [monoid N] (f: M →* N) (s  : set M) :
  (submonoid.closure s).map f = (submonoid.closure $ f '' s) :=
(galois_connection.l_comm_of_u_comm (submonoid.gi M).gc (submonoid.gi N).gc (submonoid.gc_map_comap f)
  (@set.image_preimage _ _ f) (λ _, rfl)).symm

[Eric Wieser]

We have two versions of this for submodules, docs#submodule.map_span and docs#submodule.span_image