Zulip Chat Archive

Stream: maths

Topic: group counterexample


view this post on Zulip Kevin Buzzard (Nov 23 2018 at 07:59):

Q1 part (i) on the 2nd year group theory sheet at Imperial (where GG is a group throughout) is "True or false : If we can find elements gg, hh in GG such that gh=hggh = hg then GG is abelian."

So this is false, and @Amelia Livingston and I were thinking about this question at Xena today. I wanted to formalise the question as closely as possible to the example sheet, so I wanted to write something like

theorem q1p1 : ¬ ( (G : Type*) [group G], ( g h : G, g * h = h * g)  is_abelian G) := sorry

You have to put the negation at the front of everything, so group J is after the colon and Lean doesn't know what * is. So version 2, which typechecks, is

theorem q1p1 : ¬ ( (G : Type*) [group G], by exactI ( g h : G, g * h = h * g)  is_abelian G) :=

But then we run into universe issues in the proof:

theorem q1p1 : ¬ ( (G : Type*) [group G], by exactI ( g h : G, g * h = h * g)  is_abelian G) :=
begin
  intro H
  replace H := H (perm (fin 3)), -- fails

The error is

type mismatch at application
  H (perm (fin 3))
term
  perm (fin 3)
has type
  Type : Type 1
but is expected to have type
  Type u_1 : Type (u_1+1)

I guess I understand that we can't do much about the by exactI stuff, but why can't Lean resolve my universe metavariable? Am I accidentally claiming that there are counterexamples in every universe?

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:01):

Yes you are

view this post on Zulip Johan Commelin (Nov 23 2018 at 08:01):

Take G : Type instead of Type*. I think that will help

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 08:50):

But isn't that cheating?

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 08:51):

How do I formalise the statement that it is not true that for all groups in all universes, some stupid thing holds

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 08:52):

I want the quantifier in the not

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 08:52):

The universe quantifier

view this post on Zulip Mario Carneiro (Nov 23 2018 at 09:08):

impossible

view this post on Zulip Mario Carneiro (Nov 23 2018 at 09:08):

that's existential quantification over universes

view this post on Zulip Mario Carneiro (Nov 23 2018 at 09:09):

What you can do instead is show a counterexample in a particular universe, which of course implies the existential that you can't write

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 09:16):

So do I have to use ulift to get replace H := H (perm (fin 3)) working? I've never used ulift before.


Last updated: May 10 2021 at 07:15 UTC