Image of subgroup under homomorphism

Stream: Is there code for X?

[Michael Stoll]

How do I express the image of an additive subgroup of some additive group under a given group homomorphism (as a subgroup of the target)?
@loogle AddMonoidHom, "image"

[loogle]

:search: AddMonoidHom.closure_preimage_le, AddSubgroup.closure_preimage_eq_top, and 5 more

[Michael Stoll]

@loogle AddMonoidHom, Submonoid

[loogle]

:search: Localization.mkAddMonoidHom, Localization.mkAddMonoidHom_apply, and 3 more

[Michael Stoll]

@loogle AddMonoidHom, Subgroup

[loogle]

:search: MonoidHom.coe_toAdditive_range, MonoidHom.coe_toMultiplicative_range, and 13 more

[Michael Stoll]

None of these looks promising...

[Junyan Xu]

docs#AddSubgroup.map

[Michael Stoll]

@loogle AddMonoidHom, AddSubgroup

[loogle]

:search: AddMonoidHom.ker, AddMonoidHom.range, and 282 more

[Michael Stoll]

OK, I should have thought of adding "Add"... Thanks!

[Michael Stoll]

Follow-up question: How do I write the sum of two additive subgroups of an additive group? Apparently there is no Add instance on AddSubgroup A (even with open scoped Pointwise).

[Michael Stoll]

Maybe sup?

[Michael Stoll]

At least this gives no error.

[Eric Wieser]

Do you mean Subgroup or AddSubgroup?

[Michael Stoll]

AddSubgroup of course (edited above).

[Eric Wieser]

Ideally we'd have docs#Submodule.idemSemiring for AddSubgroup

[Eric Wieser]

In the meantime you could work with Int-modules...

[Michael Stoll]

In any case, it would be nice to be able to use + here, as this is the usual notation in mathematical contexts.

[Eric Wieser]

Like I say, what you're asking for already exists on Submodule Int _

[Michael Stoll]

So I should work with ℤ-modules and linear maps instead of additive groups and group homomorphisms...

[Yury G. Kudryashov]

Or add a Semiring instance for AddSubgroups

[Michael Stoll]

That's what Eric suggests above, I think.

[Junyan Xu]

There are certain lemmas about pointwise addition of subgroups like docs#AddSubgroup.add_normal, but they're stated using pointwise addition of sets, because the sum isn't necessarily a subgroup, unless the ambient group is commutative.