Retraction construction

Stream: Is there code for X?

[Gareth Ma]

Does something like the following exist? The case $G = \mathbb{Q}$ should be fine

[Gareth Ma]

lemma A {H : Type*} [AddCommGroup H] (f : ℚ →+ H) (hf : Function.Injective f) :
    ∃ g : H →+ ℚ, ∀ a : ℚ, g (f a) = a := by
  sorry

[Kevin Buzzard]

Do you really mean (hG : DivisibleBy ℤ ℤ)? This doesn't mention G.

[Gareth Ma]

Oh wait

[Gareth Ma]

I have removed it lol

[Kevin Buzzard]

I need to finish writing tomorrow's lecture but is this related to Q being an injective abelian group / injective Z-module? That might be where to start looking. Sorry if I'm talking nonsense.

[Gareth Ma]

Yes indeed, but I couldn't find anything just now, let me try again.

[Gareth Ma]

(But maybe someone already knows)