Failed to unify, but why

Stream: new members

[Joachim Breitner]

This time with #mwe :-)
In this code

import group_theory.subgroup.basic
import group_theory.is_free_group
import data.zmod.basic

namespace is_free_group
universe u
example {G : Type u} [group G] [is_free_group G]
  : (generators G → zmod 2) ≃ (G →* zmod 2) :=
begin
    apply is_free_group.lift,

end

the apply fails with

invalid apply tactic, failed to unify
  (generators G → zmod 2) ≃ (G →* zmod 2)
with
  (generators ?m_1 → ?m_4) ≃ (?m_1 →* ?m_4)
state:
G : Type u,
_inst_1 : group G,
_inst_2 : is_free_group G
⊢ (generators G → zmod 2) ≃ (G →* zmod 2)

Now, these look like they should unify to me, but probably something implicit does not line up. But what? (The universe u is cargo-culted from is_free_group.lean, and may well be wrong).

[Yakov Pechersky]

import group_theory.subgroup.basic
import group_theory.is_free_group
import data.zmod.basic

namespace is_free_group

universe u
example {G : Type u} [group G] [is_free_group G] :
  (generators G → zmod 2) ≃ (G →* zmod 2) :=
@is_free_group.lift G (zmod 2) _ _
  /-
  failed to synthesize type class instance for
  G : Type u,
  _inst_1 : group G,
  _inst_2 : is_free_group G
  ⊢ group (zmod 2)
  -/

[Joachim Breitner]

Ah, maybe because of

failed to synthesize type class instance for
⊢ group (zmod 2)

when I try to instantiate lift manually? Ah, I was too slow :-)

[Alex J. Best]

zmod 2 is an docs#add_group but not a group.

[Joachim Breitner]

Hmm, https://leanprover-community.github.io/mathlib_docs/group_theory/specific_groups/cyclic.html says “For the concrete cyclic group of order n, see data.zmod.basic.”, but that was misleading it seems.

[Alex J. Best]

You can use multiplicative (zmod 2) to make a multiplicative version of it

[Floris van Doorn]

You can use docs#multiplicative applied to zmod 2

[Alex J. Best]

Lean's handling of groups with add and mul is a bit funny

[Alex J. Best]

We have two "distinct" classes

[Alex J. Best]

And so every group is either written with a + or a *

[Alex J. Best]

And zmod 2 is a ring, so the * refers to the multiplication 0x0 = 0, 1x 1 = 1, which is a monoid (or even a docs#group_with_zero) but no inverses

[Yakov Pechersky]

import group_theory.subgroup.basic
import group_theory.is_free_group

namespace is_free_group

local notation `g` n := multiplicative (fin n)

universe u
noncomputable example {G : Type u} [group G] [is_free_group G] :
  (generators G → g 2) ≃ (G →* g 2) :=
is_free_group.lift

[Yakov Pechersky]

Not to bikeshed whether fin 2 or zmod 2 is more appropriate here, just to show that it works

[Joachim Breitner]

Anything I should know about fin vs. zmod? :-)

[Alex J. Best]

zmod is more algebraic (it has the ring structure for instance).
fin is more counting-y, we have maps from fin n \to fin (n + 1) which don't really make sense if you think of it as $\mathbf Z/n$

[Yakov Pechersky]

We probably have more proofs about moving between fin n and fin (n + 1), cons, succ, snoc, cast_succ, things of that nature, usually used to represent a finite type of explicit cardinality. It just happens to also have the same exact comm_ring structure as zmod

[Joachim Breitner]

Since I really only need fin 2 ≃ bool (or #fin 2 = 2), that should do