existential statement about group

Stream: new members

[Emmanuel Rauzy]

Hi everyone,
I am interested in implementing embedding theorems for countable groups in Lean 3, starting for instance with: every countable group embeds in a finitely generated group.
But I don't know how to state "there exists a group H" and use the assumption that H is a group, for instance below is one try for the simple statement "every group embeds in a group":

lemma gp_embed_some  (G : Type) [group G] : ∃(H: Type)(hH:group H), ∃(φ : G→* H), function.injective φ

but this is not accepted because H is not seen as a group in the definition of φ.
I have not been able to resolve this problem, can you help me?

[Yaël Dillies]

lemma gp_embed_some  (G : Type*) [group G] :
  ∃ (H : Type*) [group H], by exactI ∃ φ : G→* H, function.injective φ

[Kevin Buzzard]

(typo now fixed)

[Kevin Buzzard]

What's going on here is that when Lean sees G →* H it asks the type class inference system (the square bracket system) to check that G and H are groups, but the type class inference system is initialised only with the square bracket stuff that comes before the colon, so it sees [group G] but not [group H]. The by exactI trick re-initialises the system (it switches to tactic mode and then straight back to term mode).

[Emmanuel Rauzy]

Thank you very much for this!

[Jireh Loreaux]

@Emmanuel Rauzy , even though it is possible to state your theorem this way, it's not the way I would suggest stating it, at least not if you can avoid it. In particular, if the argument manages to construct a finitely generated group from a countable group, then I would create a def for the type housing that finitely generated group, and then put the relevant instances (group and finitely generated) on it. Then construct the group homomorphism from the countable group into this group you constructed.

[Jireh Loreaux]

To be more explicit, I'm suggesting something like this:

variables (G : Type*) [group G] [countable G]

def fg_group := sorry

instance : group (fg_group G) := sorry

instance : group.fg (fg_group G) := sorry

def monoid_hom_fg_group : G →* fg_group G := sorry

lemma monoid_hom_fg_group_injective : function.injective (monoid_hom_fg_group G) := sorry

[Kevin Buzzard]

Basically the question is whether the argument is constructive.