Zulip Chat Archive

Stream: new members

Topic: Failed to unify, but why


Joachim Breitner (Jan 12 2022 at 22:27):

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 (Jan 12 2022 at 22:29):

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 (Jan 12 2022 at 22:30):

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 (Jan 12 2022 at 22:32):

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

Joachim Breitner (Jan 12 2022 at 22:33):

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 (Jan 12 2022 at 22:33):

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

Floris van Doorn (Jan 12 2022 at 22:33):

You can use docs#multiplicative applied to zmod 2

Alex J. Best (Jan 12 2022 at 22:33):

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

Alex J. Best (Jan 12 2022 at 22:34):

We have two "distinct" classes

Alex J. Best (Jan 12 2022 at 22:34):

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

Alex J. Best (Jan 12 2022 at 22:35):

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 (Jan 12 2022 at 22:35):

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 (Jan 12 2022 at 22:36):

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

Joachim Breitner (Jan 12 2022 at 22:42):

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

Alex J. Best (Jan 12 2022 at 22:43):

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 Z/n\mathbf Z/n

Yakov Pechersky (Jan 12 2022 at 22:43):

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 (Jan 12 2022 at 22:59):

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


Last updated: Dec 20 2023 at 11:08 UTC