## Stream: maths

### Topic: group counterexample

#### Kevin Buzzard (Nov 23 2018 at 07:59):

Q1 part (i) on the 2nd year group theory sheet at Imperial (where $G$ is a group throughout) is "True or false : If we can find elements $g$, $h$ in $G$ such that $gh = hg$ then $G$ 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?

Yes you are

#### Johan Commelin (Nov 23 2018 at 08:01):

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

#### Kevin Buzzard (Nov 23 2018 at 08:50):

But isn't that cheating?

#### 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

#### Kevin Buzzard (Nov 23 2018 at 08:52):

I want the quantifier in the not

#### Kevin Buzzard (Nov 23 2018 at 08:52):

The universe quantifier

impossible

#### Mario Carneiro (Nov 23 2018 at 09:08):

that's existential quantification over universes

#### 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

#### 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