# Zulip Chat Archive

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

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

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

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

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