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?