Code review: group structure

Stream: new members

[Isak Colboubrani]

For educational purposes I'm building a group structure from scratch with the goal of a.) writing it in fully idiomatic Lean 4 code while b.) still understanding all the code I've written (not just copy and pasting).

Currently I have this code:

-- A magma is a set equipped with a binary operation.
class Magma (α : Type) extends Mul α

-- A semigroup is a magma whose binary operation is associative.
class Semigroup (α : Type) extends Magma α where
  mul_assoc: ∀ g h k : α, (g * h) * k = g * (h * k)

-- A monoid is a semigroup with an identity element for the binary operation.
class One (α : Type) where
  one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1
class Monoid (α : Type) extends Semigroup α, One α where
  one_mul : ∀ g : α, 1 * g = g
  mul_one : ∀ g : α, g * 1 = g

-- A group is a monoid with an inverse for every element.
class Inv (α : Type) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv
class Group (α : Type) extends Monoid α, Inv α where
  mul_left_inv: ∀ g : α, g⁻¹ * g = 1
  mul_right_inv : ∀ g : α, g * g⁻¹ = 1

-- An abelian group is a group whose binary operation is commutative.
class AbelianGroup (α : Type) extends Group α where
  mul_comm: ∀ g h : α, g * h = h * g

Questions:

1.

Is there anything I can improve in the above to make it more idiomatic?

(I understand that extending Mul to introduce the name Magma is a bit odd, but for pedagogical reasons I'd like to spell out every part of the structure from magma and up.)

2.

I'm not fully comfortable with the following code snippet:

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

It feels somewhat magic. How should I understand it?

Previously I used …

class HasIdentityElement (α : Type) where
  e : α
notation "e" => HasIdentityElement.e

… which feels much more self-explaining, but I guess I must use One.toOfNat1 to get 1 instead of e for the identity?

[Riccardo Brasca]

Why not introducing Magma from scratch? Copying the definition of Mul.

[Isak Colboubrani]

Like this?

-- A magma is a set equipped with a binary operation.
class Magma (α : Type) where
  mul: α → α → α
infixl:70 (priority := high) "*" => Magma.mul

[Riccardo Brasca]

Ah, Mul is in Prelude, so you cannot not import it, and now your notation might conflict with the built in *.

[Riccardo Brasca]

Indeed using an high priority might work, but your first solution was probably better.

[Riccardo Brasca]

But I would use a notation for Magma, instead of a new class.

[Riccardo Brasca]

With

class Magma (α : Type) extends Mul α

if h : Magma α, then h.1 : Mul α, and to get to the operation you have to write h.1.1 (this is rarely needed of course, but still).

[Riccardo Brasca]

Something like local notation "Magma" α => Mul α if you don't want to use Mul everywhere.

[Riccardo Brasca]

(you can also play the game of #mil chapter 7 and use a different symbol for the operation)

[Riccardo Brasca]

Concerning

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

you can just ignore it. The point is that Lean treats numerals in a special way (so that if you type 452353245324653456435 it understands it as a natural number, even if of course this one has never been defined explicitly). That code just set up a notation 1 : α for the element One.one : α.

[Isak Colboubrani]

Another question: in Lean code I often see notation defined as this: infixl:70 … " * " => ….

Is that equivalent to infixl:70 … "*" => … (note the lack of spaces)? Are the spaces ignored?

[Eric Wieser]

The spaces are used when printing

[Isak Colboubrani]

Which of these formulations is the idiomatic one?

class Group (α : Type) extends Monoid α, Inv α where …
class Group (α : Type u) extends Monoid α, Inv α where …
class Group (G : Type) extends Monoid G, Inv G where …
class Group (G : Type u) extends Monoid G, Inv G where …

[Riccardo Brasca]

Surely Type u is more general.

[Riccardo Brasca]

For the other choice it really depends, mathlib goes via crazy classes like docs#MulOneClass

[Riccardo Brasca]

anything should be fine at the beginning.

[Kevin Buzzard]

When I'm teaching I don't introduce universes at all. It's just one less thing to worry about. People are total universe fanatics here ("they're in the language so why not use them") but for teaching purposes I've never seen the point of them.

[Kevin Buzzard]

And I always use sensible notation not alpha. The whole alpha thing was just how mathlib was initially developed in 2017 and there's still plenty of it around but I found it obfuscated things in algebra files because you can't tell what assumptions there are on a type when it's called alpha, whereas in a group theory file you can start guessing that M is a monoid, G and H are groups, A is an abelian group etc

[Isak Colboubrani]

Thanks a lot for the helpful hints @Riccardo Brasca and @Kevin Buzzard! I'm now using Type instead of Type … throughout. I've also switched from the alpha thing to M, G, H, A, etc.

I've now reached the stage where I'm ready to define Ring.

I'm doing:

-- A ring is a set equipped with two binary operations, addition and
-- multiplication, where addition forms an abelian group, multiplication
-- forms a monoid, and multiplication is distributive over addition.
class Ring₁ (R : Type) extends AdditiveAbelianGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c)
  right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c)

class Ring₂ (R : Type) extends AdditiveAbelianGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

Ring₁ compiles whereas Ring₂ fails with failed to synthesize instance HAdd R R ?m.[…].

My questions:

1. Does Ring₁ look correct?
2. How can I make Ring₂ compile?

Full #mwe:

-- A magma is a set equipped with a binary operation.
class Magma (M : Type) where
  mul: M → M → M
infixl:70 (priority := high) " * " => Magma.mul
class AdditiveMagma (AM : Type) where
  add: AM → AM → AM
infixl:70 (priority := high) " + " => AdditiveMagma.add

-- A semigroup is a magma whose binary operation is associative.
class Semigroup (S : Type) extends Magma S where
  mul_assoc: ∀ g h k : S, (g * h) * k = g * (h * k)
class AdditiveSemigroup (AS : Type) extends AdditiveMagma AS where
  add_assoc: ∀ g h k : AS, (g + h) + k = g + (h + k)

-- A monoid is a semigroup with an identity element for the binary operation.
class One (O : Type) where
  one : O
instance One.toOfNat1 {O} [One O] : OfNat O (nat_lit 1) where
  ofNat := ‹One O›.1
class Monoid (M : Type) extends Semigroup M, One M where
  one_mul : ∀ g : M, 1 * g = g
  mul_one : ∀ g : M, g * 1 = g
class Zero (Z : Type) where
  zero : Z
instance Zero.toOfNat0 {Z} [Zero Z] : OfNat Z (nat_lit 0) where
  ofNat := ‹Zero Z›.1
class AdditiveMonoid (AM : Type) extends AdditiveSemigroup AM, Zero AM where
  one_add : ∀ g : AM, 0 + g = g
  add_one : ∀ g : AM, g + 0 = g

-- A group is a monoid with an inverse for every element.
class Inverse (I : Type) where
  inv : I → I
postfix:max "⁻¹" => Inverse.inv
class Group (G : Type) extends Monoid G, Inverse G where
  mul_left_inv: ∀ g : G, g⁻¹ * g = 1
  mul_right_inv : ∀ g : G, g * g⁻¹ = 1
class AdditiveInverse (AI : Type) where
  inv : AI → AI
prefix:max "-" => AdditiveInverse.inv
class AdditiveGroup (AG : Type) extends AdditiveMonoid AG, AdditiveInverse AG where
  add_left_inv: ∀ g : AG, (-g) + g = 0
  add_right_inv : ∀ g : AG, g + (-g) = 0

-- An abelian group is a group whose binary operation is commutative.
class AbelianGroup (A : Type) extends Group A where
  mul_comm: ∀ g h : A, g * h = h * g
class AdditiveAbelianGroup (AA : Type) extends AdditiveGroup AA where
  add_comm: ∀ g h : AA, g + h = h + g

-- A ring is a set equipped with two binary operations, addition and
-- multiplication, where addition forms an abelian group, multiplication
-- forms a monoid, and multiplication is distributive over addition.
class Ring₁ (R : Type) extends AdditiveAbelianGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c)
  right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c)

class Ring₂ (R : Type) extends AdditiveAbelianGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

[Riccardo Brasca]

Change infixl:70 (priority := high) " + " => AdditiveMagma.add to something like infixl:65 (priority := high) " + " => AdditiveMagma.add. Multiplication should have an higher priority than addition.

[Riccardo Brasca]

Otherwise the parenthesis are wrong in Ring₂ (the fact that Lean gives you an error rather than simply using the wrong parenthesis is a little subtler, I suggest you to ignore it for the moment).

[Isak Colboubrani]

Ah of course! Thanks!

After …

-infixl:70 (priority := high) " + " => AdditiveMagma.add
+infixl:65 (priority := high) " + " => AdditiveMagma.add

… I'm now doing …

class Ring (R : Type) extends AdditiveAbelianGroup R, Monoid R where
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

… which works!

[Riccardo Brasca]

If you want to see something slightly different try modules!

[Riccardo Brasca]

The basic class is docs#SMul

[Isak Colboubrani]

@Riccardo Brasca That's a good idea. Thanks! My current plan is to work myself up to Field and then tackle "two sets with operations": I'm thinking module, vector space and then inner product space.

I've proceeded with Field doing:

-- A commutative ring is a ring in which the multiplication operation is
-- commutative.
class CommutativeRing (CR : Type) extends Ring CR where
  mul_comm: ∀ g h : CR, g * h = h * g

-- A field is a commutative ring which contains a multiplicative inverse
-- for every nonzero element.
class Field (F : Type) extends CommutativeRing F where
  mul_inv : ∀ a : F, a ≠ 0 → ∃ b : F, a * b = 1

Looks correct?

I'm not sure if my definition of Field, Zero and One currently implies 0 ≠ 1 (or if/when it should). I guess I could make (0 : F) ≠ 1 explicit in Field. Should I and would that be the appropriate way to handle that?

[Riccardo Brasca]

Following standard mathematical terminology, in a field 0 ≠ 1, and the trivial ring surely satisfies

∀ a : F, a ≠ 0 → ∃ b : F, a * b = 1

(since there are no a ≠ 0), so you should change the definition. I mean, yours has a (small) mathematical problem.

[Riccardo Brasca]

What is your goal, to learn how to set things up?

[Riccardo Brasca]

Anyway, for groups you followed the approva via Inv, you can do the same with fields: it gives you the same advantages (i.e. the notation ⁻¹).

[Kevin Buzzard]

Note that for Inv it's convenient in type theory to allow Inv 0 to make sense, and in mathlib we define it to be 0. The problem with ∀ a : F, a ≠ 0 → ∃ b : F, a * b = 1 is the same as the problem you avoided by not writing ∀ g : G, ∃ h : G, g * h = 1 for group inverses. If you use this as definition of inverse then you realise that it's not a definition, you have to use the axiom of choice to get the h(g) you want for all g, and things are much more inconvenient. It's easier to define an Inv function on groups sending an element g to Inv g and then demanding g * Inv g = 1 (and also setting up notation $g^{-1}$ for Inv g of course). The same is true for fields; don't just demand an inverse exists, ask for a function, and demand it has good properties, because in practice you want the function, not just some abstract existence statement. This involves defining Inv 0 and the easiest solution is to just let it be 0, because you can't make Lean "crash" by dividing by 0.

[Isak Colboubrani]

Riccardo Brasca said:

What is your goal, to learn how to set things up?

Good question! My goal is to learn how to formalize first-year undergraduate abstract algebra from scratch in Lean 4 with an initial focus on group theory.

[Patrick Massot]

Did you read Chapter 7 of #mil?

[Isak Colboubrani]

@Patrick Massot I've skimmed it and looked at the code before, but now I have read it. Thanks for writing it! It is a great learning resource. I like it a lot.

This is my attempt at extracting the group theory part of chapter 7.1 and then removing all dependencies on Mathlib and Prelude.lean to make it fully self-contained:

namespace GroupTheoryFromMILChapter7

class Mul₁ (α : Type) where
  mul : α → α → α
infixl:70 (priority := high) " * " => Mul₁.mul
class Semigroup₁ (α : Type) extends Mul₁ α where
  mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
class One₁ (α : Type) where
  one : α
instance One₁.toOfNat1 {O} [One₁ O] : OfNat O (nat_lit 1) where
  ofNat := ‹One₁ O›.1
class MulOneClass₁ (α : Type) extends One₁ α, Mul₁ α where
  one_mul : ∀ a : α, 1 * a = a
  mul_one : ∀ a : α, a * 1 = a
class Monoid₁ (M : Type) extends Semigroup₁ M, MulOneClass₁ M
class Inv₁ (α : Type) where
  inv : α → α
postfix:max "⁻¹" => Inv₁.inv
class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1
  mul_inv : ∀ a : G, a * a⁻¹ = 1
class AbelianGroup₁ (A : Type) extends Group₁ A where
  mul_comm : ∀ a b : A, a * b = b * a

Let me know if anything looks odd.

[Isak Colboubrani]

I noticed that my code still seems to work as expected after doing the following:

-instance One₁.toOfNat1 {O} [One₁ O] : OfNat O (nat_lit 1) where ofNat := ‹One₁ O›.1
+instance {O} [One₁ O] : OfNat O (nat_lit 1) where ofNat := ‹One₁ O›.1

When should I include the function name argument ("One₁.toOfNat1" in this case) and when is it okay to omit it?

[Kevin Buzzard]

If you omit it then it will be named automatically, and possibly poorly. You can see what it was named by typing whatsnew in before the instance.

[Isak Colboubrani]

@Riccardo Brasca @Kevin Buzzard Thanks for the hints regarding the field definition.

Here is my new try:

-- A commutative ring is a ring in which the multiplication operation is
-- commutative.
class CommutativeRing (R : Type) extends Ring R where
  mul_comm : ∀ a b : R, a * b = b * a

-- A field is a commutative ring which contains a multiplicative inverse
-- for every nonzero element.
class Field (F : Type) extends CommutativeRing F, Inverse F where
  zero_ne_one : (0 : F) ≠ 1
  mul_inv_cancel : ∀ a : F, a ≠ 0 → a * a⁻¹ = 1
  inv_zero : (0 : F)⁻¹ = 0

Let me know if anything looks odd.

[Kevin Buzzard]

Looks good to me at first glance!