Introducing Lean to undergraduates: elementary group theory

Stream: new members

[Isak Colboubrani]

I am preparing a demonstration of Lean for fellow undergraduate students who are taking their first course in abstract algebra.

My goal is to show them how to formally state and prove (really) basic group theoretic results that they are expected to know, all derived directly and quite straightforwardly from the group axioms.

I plan to begin with familiar propositions such as "the identity element is unique" and "if $g^2=g$ for every $g \in G$, then the group is abelian."

Below is my initial list of statements in Lean. Are they stated in an idiomatic, "exact?-compatible" manner? Additionally, which other elementary results would be good to include? All input appreciated!

#mwe

import Mathlib

variable (G : Type) [Group G]

example (e : G) : ∀ g : G, g * e = g → e = 1 := by sorry
example (g : G) : ∀ h : G, g * h = 1 → h = g⁻¹ := by sorry
example (g : G) : (g⁻¹)⁻¹ = g := by sorry
example (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by sorry
example (a b c d e : G) : a * ((b * c) * (d * e)) = a * (b * (c * (d * e))) := by sorry
example (a b c d e : G) : (a * b * c * d * e)⁻¹ = e⁻¹ * d⁻¹ * c⁻¹ * b⁻¹ * a⁻¹ := by sorry
example (a u v : G) : a * u = a * v → u = v := by sorry
example (b u v : G) : u * b = v * b → u = v := by sorry
example (a b : G) : ∃! x : G, a * x = b := by sorry
example (a b : G) : ∃! y : G, y * a = b := by sorry
example (a : G) (n : ℤ) : a ^ (-n) = (a ^ n)⁻¹ := by sorry
example (a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ (m + n) := by sorry
example (a : G) (m n : ℤ) : (a ^ m) ^ n = a ^ (m * n) := by sorry
example (CG : Type) [CommGroup CG] (a b : CG) (n : ℤ) : (a * b) ^ n = a^n * b^n := by sorry
example : ∀ g : G, g^1 = 1 → g = 1 := by sorry
example (h : ∀ x : G, x * x = 1) : ∀ g h : G, g * h = h * g := by sorry
example : (1 : G)⁻¹ = 1 := by sorry
example (g : G) (n : ℕ) : (g ^ n)⁻¹ = g⁻¹ ^ n := by sorry
example (g : G) : g⁻¹ = 1 → g = 1 := by sorry
example (a b : G) : (a * b) ^ 2 = a^2 * b^2 → a * b = b * a := by sorry
example (h : ∀ g : G, orderOf g = 2) : ∀ g h : G, g * h = h * g := by sorry
example [Fintype G] (g : G) : orderOf g ∣ Fintype.card G := by sorry
example (g : G) : orderOf g = orderOf g⁻¹ := by sorry
example [Fintype G] (x : G) (m s : ℕ) : x ^ s = 1 ↔ m ∣ s := by sorry

[Aaron Liu]

You have some statements with binders on the right. I think it would be better if you moved those binders to the left.
ex. instead of

example (e : G) : ∀ g : G, g * e = g → e = 1 := by sorry

you should do

example (e g : G) (he : g * e = g) : e = 1 := by sorry

[Aaron Liu]

Mathlib doesn't seems to have many theorems for docs#ExistsUnique. Maybe you should make separate existence and the uniqueness lemmas.

[Derek Rhodes]

by the way, @Isak Colboubrani, if you have not already seen it, you may be interested in checking out section 5 of 2024 version of the course formalizing mathematics which covers some group theory, (also, section 7 has exercises on subgroups.)

[Thomas Browning]

One small thing is that the group theory library mostly uses [Finite G] and Nat.card G instead of [Fintype G] and Fintype.card G (one reason for this is that it often allows you to drop finiteness assumptions altogether).

[Kevin Buzzard]

Some of these are one-liners from the axioms, some are very long from the axioms (eg the ones that use finiteness). The last one looks like nonsense: it says that for all x, m and s, x^s=1 iff m divides s.

[Isak Colboubrani]

@Kevin Buzzard Oh, thanks! The last one should probably be

import Mathlib
variable (G : Type) [Group G]
example [Finite G] (x : G) (s : ℕ) : x ^ s = 1 ↔ orderOf x ∣ s := by sorry

Is that the idiomatic phrasing of "Let x be an element of order m in a finite group G. Then x^s = 1 in G if and only if s is a multiple of m."?

I'm not entirely sure whether I should break apart iff statements when giving the demonstration. From what I understand, splitting the proof into forward and backward implications is considered more idiomatic within Mathlib, even though stating the result with ↔ is closer to the usual textbook formulation which the audience is used to. Any advice on which approach to adopt?

[Kevin Buzzard]

I am completely confused about what you are doing so am not really able to give advice. Many of these results are already proved in mathlib, is the point to demonstrate the proof or to do the proof again, and if you're doing the proof again then what are you allowed to assume? I'm not clear about what you are trying to teach them. orderOf has got a bunch of API, much of it hard-won and a long way from the axioms of a group.

[Isak Colboubrani]

In my previous post, I was somewhat imprecise (and I didn't even mention that I planned to use existing Mathlib results in some cases!), and I apologize for that.

My primary goal is to show my fellow undergraduates how to formally state various results—ranging from trivial to non-trivial—that they may recall from the group theory section of our introductory abstract algebra course.

The secondary goal is to demonstrate how a selected subset of these results can be proved directly from the group axioms (i.e., from first principles), while the proofs of the more challenging results can be obtained by invoking existing theorems in Mathlib.

The overall goal is to inspire and engage students in the formalization of mathematics using Lean and Mathlib.

[Isak Colboubrani]

This is my updated list of items to demonstrate. The plan is to show how to translate statements from their 'textbook formulation' to their 'Lean formulation.' I will prove the simpler ones directly from the axioms and tackle the more challenging ones using theorems from Mathlib (including an explanation of how to find them).

Does this look reasonable? What can be improved? Anything non-idiomatic?

import Mathlib

variable (G : Type) [Group G]

example (e g : G) (h1 : g * e = g) : e = 1 := by sorry
example (g h : G) (h1 : g * h = 1) : h = g⁻¹ := by sorry
example (g : G) : (g⁻¹)⁻¹ = g := by sorry
example (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by sorry
example (a b c d e : G) : a * ((b * c) * (d * e)) = a * (b * (c * (d * e))) := by sorry
example (a b c d e : G) : (a * b * c * d * e)⁻¹ = e⁻¹ * d⁻¹ * c⁻¹ * b⁻¹ * a⁻¹ := by sorry
example (a u v : G) (h : a * u = a * v) : u = v := by sorry
example (b u v : G) (h : u * b = v * b): u = v := by sorry
example (a b : G) : ∃! x : G, a * x = b := by sorry
example (a b : G) : ∃! y : G, y * a = b := by sorry
example (a : G) (n : ℤ) : a^(-n) = (a^n)⁻¹ := by sorry
example (a : G) (m n : ℤ) : a^m * a^n = a^(m + n) := by sorry
example (a : G) (m n : ℤ) : (a^m)^n = a^(m * n) := by sorry
example (CG : Type) [CommGroup CG] (a b : CG) (n : ℤ) : (a * b)^n = a^n * b^n := by sorry
example (g : G) : g^0 = 1 := by sorry
example (g : G) (h1 : g^1 = 1) : g = 1 := by sorry
example (h1 : ∀ x : G, x * x = 1) : ∀ g h : G, g * h = h * g := by sorry
example : (1 : G)⁻¹ = 1 := by sorry
example (g : G) (n : ℕ) : (g^n)⁻¹ = (g⁻¹)^n := by sorry
example (g : G) : g⁻¹ = 1 → g = 1 := by sorry
example (a b : G) (n : ℤ) : (a * b)^n = (a * b)^n := by sorry
example (a b : G) : (a * b)^2 = a^2 * b^2 → a * b = b * a := by sorry
example (h1 : ∀ g : G, orderOf g = 2) : ∀ g h : G, g * h = h * g := by sorry
example [Finite G] (g : G) : orderOf g ∣ Nat.card G := by sorry
example (g : G) : orderOf g = orderOf g⁻¹ := by sorry
example [Finite G] (x : G) (s : ℕ) : x^s = 1 ↔ (orderOf x) ∣ s := by sorry
example [Finite G] (x : G) : x^(orderOf x) = 1 := by sorry

[Edward van de Meent]

Uniqueness of "one" is formulated slightly different from what i had expected...

Usually 1 is specified as having the property "for any g, g * 1 = g" rather than "there exists g, s.t. g * 1 = g" Of course in a group, where multiplication has an inverse, these are provably equivalent. However, it doesn't generalize to monoids.

[Edward van de Meent]

As such, I'd say uniqueness of "one" is better formalized as example (e : G) (h1 : ∀ g : G, g * e = g) : e = 1 := by sorry

[Kevin Buzzard]

example (g : G) (h1 : g^1 = 1) : g = 1 := by sorry

should probably just be g^1 = g.

example (h1 : ∀ g : G, orderOf g = 2) : ∀ g h : G, g * h = h * g := by sorry

can't ever happen because orderOf 1 = 1.

example [Finite G] (x : G) (s : ℕ) : x^s = 1 ↔ (orderOf x) ∣ s := by sorry

I doubt you need finiteness for that or for the next one. In fact I don't think you need finiteness in any of the three places you assume it.