Hom(Z,A)

Stream: Is there code for X?

[Adam Topaz]

Does anyone know whether we have the isomorphism between $Hom(\mathbb{Z},A)$ and $A$ for an additive group $A$? Ideally I would like an add_equiv.

[Heather Macbeth]

docs#zmultiples_add_hom , assuming commutativity (not sure if it's needed)

[Adam Topaz]

Thanks!

[Heather Macbeth]

with thanks to

import tactic

example {A : Type*} [add_comm_group A] : (ℤ →+ A) ≃+ A := by library_search

[Adam Topaz]

While you're here.... do you know if we have the iso between \top : subgroup G and G?

[Adam Topaz]

library search comes up short on that...

[Heather Macbeth]

I found it for submodules: docs#submodule.top_equiv_self

[Heather Macbeth]

(this time by googling for ↥⊤ through the whole documentation)

[Heather Macbeth]

You could build it from docs#add_monoid_hom.cod_restrict and docs#add_monoid_hom.restrict (as I'm sure you know perfectly well).

[Eric Wieser]

There's an open PR for that, #12658

[Kevin Buzzard]

Heh yeah this came up on the discord yesterday