learning math with mathlib

Stream: general

[Bulhwi Cha]

Starting next week, I'll learn abstract algebra and mathematical logic while looking up Mathlib and the Lean 4 Logic Formalization project.

The following are some of the textbooks I'll refer to. I'll read carefully two of them: "Abstract Algebra: Theory and Applications" and "Mathematical Logic and Computation." I'm curious how my attempt to use Mathlib for learning mathematics will turn out.

Abstract Algebra

• "Abstract Algebra: Theory and Applications" by Thomas W. Judson: https://judsonbooks.org/aata/
• "Algebra" by Larry C. Grove: https://store.doverpublications.com/collections/math-algebra/products/9780486439471
• "Algebra: Chapter 0" by Paolo Aluffi: https://bookstore.ams.org/gsm-104/

Mathematical Logic

• "Mathematical Logic and Computation" by Jeremy Avigad: https://doi.org/10.1017/9781108778756
• "The Open Logic Text" by the Open Logic Project: https://openlogicproject.org/

[Lingwei Peng (彭灵伟)]

I think having a clean algebra code project in Lean would be really helpful. Do you know of any open-source projects that I could explore? I’ve written some initial code, and I believe it shouldn’t be too difficult to continue from there.

namespace MyAlgebra

universe u

class Magma (α : Type u) where
  op : α → α → α
infixl:70 " * " => Magma.op

class Neutral (α : Type u) where
  neutral : α
instance (priority := 300) Neutral.toOfNat1 {α} [Neutral α] : OfNat α (nat_lit 1) where
  ofNat := ‹Neutral α›.neutral
instance (priority := 200) Neutral.ofOfNat1 {α} [OfNat α (nat_lit 1)] : Neutral α where
  neutral := 1

class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

class Semigroup (G : Type u) extends Magma G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class Monoid (G : Type u) extends Semigroup G, Neutral G where
  one_mul : ∀ a : G, (1 : G) * a = a
  mul_one : ∀ a : G, a * (1 : G) = a

class Group (G : Type u) extends Monoid G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1
  mul_inv : ∀ a : G, a * a⁻¹ = 1

class CommMagma (α : Type u) extends Magma α where
  mul_comm : ∀ a b : α, a * b = b * a
class CommSemigroup (G : Type u) extends Semigroup G, CommMagma G where
class CommMonoid (G : Type u) extends Monoid G, CommSemigroup G
class CommGroup (G : Type u) extends Group G, CommSemigroup G

theorem Monoid.unique_left_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, e * a = a) : e = 1 := by
  rw [← h 1, mul_one]
theorem Monoid.unique_right_neutral {G : Type u} [Monoid G] (e : G) (h : ∀ a : G, a * e = a) : e = 1 := by
  rw [← h 1, one_mul]

class LeftGroup (G : Type u) extends Semigroup G, Neutral G, Inv G where
  one_mul : ∀ a : G, (1 : G) * a = a
  inv_mul : ∀ a : G, a⁻¹ * a = 1
theorem LeftGroup.self_op_self_eq_one (G : Type u) [lg : LeftGroup G] (a : G) (h : a * a = a) : a = 1 := by
  rw [← lg.one_mul a]
  apply Eq.subst (motive := fun x => x * a = 1 ) (lg.inv_mul a)
  rw [lg.mul_assoc, h]
  exact lg.inv_mul a
theorem LeftGroup.mul_inv (G : Type u) [lg : LeftGroup G] (a : G) : a * a⁻¹ = 1 := by
  apply lg.self_op_self_eq_one
  rw [lg.mul_assoc]
  apply Eq.subst (motive := fun (x : G) => a * x = a * a⁻¹) (lg.mul_assoc a⁻¹ a a⁻¹)
  rw [lg.inv_mul, lg.one_mul]
theorem LeftGroup.mul_one (G : Type u) [lg : LeftGroup G] (a : G) : a * (1 : G) = a := by
  rw [← lg.inv_mul a, ← lg.mul_assoc, lg.mul_inv, lg.one_mul]
instance LeftGroup.toGroup (G : Type u) [lg : LeftGroup G] : Group G where
  one_mul := lg.one_mul
  inv_mul := lg.inv_mul
  mul_inv := lg.mul_inv
  mul_one := lg.mul_one

theorem Group.unique_left_inv {G : Type u} [g : Group G] (a b : G) (h : a * b = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.one_mul b⁻¹)
  rw [← h, g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.unique_right_inv {G : Type u} [g : Group G] (a b : G) (h : b * a = 1) : a = b⁻¹ := by
  apply Eq.subst (motive := fun x => a = x) (g.mul_one b⁻¹)
  rw [← h, ← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.inv_inv (G : Type u) [g : Group G] (a : G) : a⁻¹⁻¹ = a := by
  apply Eq.symm
  apply g.unique_right_inv
  exact g.inv_mul a
theorem Group.inv_self_mul {G : Type u} [g : Group G] (a b : G) : a⁻¹ * (a * b) = b := by
  rw [← g.mul_assoc, g.inv_mul, g.one_mul]
theorem Group.self_inv_mul {G : Type u} [g : Group G] (a b : G) : a * (a⁻¹ * b) = b := by
  rw [← g.mul_assoc, g.mul_inv, g.one_mul]
theorem Group.mul_self_inv {G : Type u} [g : Group G] (a b : G) : a * b * b⁻¹ = a := by
  rw [g.mul_assoc, g.mul_inv, g.mul_one]
theorem Group.mul_inv_self {G : Type u} [g : Group G] (a b : G) : a * b⁻¹ * b = a := by
  rw [g.mul_assoc, g.inv_mul, g.mul_one]
theorem Group.inv_mul_inv {G : Type u} [g : Group G] (a b : G) : a⁻¹ * b⁻¹ = (b * a)⁻¹ := by
  apply g.unique_left_inv
  rw [g.mul_assoc, g.inv_self_mul, g.inv_mul]
theorem Group.cancel_left (G : Type u) [g : Group G] (a b c : G) (h : a * b = a * c) : b = c := by
  rw [← g.inv_self_mul a b, h, g.inv_self_mul]
theorem Group.cancel_right (G : Type u) [g : Group G] (a b c : G) (h : b * a = c * a) : b = c := by
  rw [← g.mul_self_inv b a, h, g.mul_self_inv]

end MyAlgebra

[Bulhwi Cha]

Lingwei Peng (彭灵伟) said:

I think having a clean algebra code project in Lean would be really helpful. Do you know of any open-source projects that I could explore? I’ve written some initial code, and I believe it shouldn’t be too difficult to continue from there.

Sorry for the late reply. I'm not into defining algebraic structures from scratch since Mathlib already has all I need. I'm not sure if there are Lean projects that attempt to do this.

[Ben Selfridge]

I just did this with a tiny portion of abstract algebra. I can give you my notes in Lean if you want.

[Lingwei Peng (彭灵伟)]

Great! Are your notes based on a specific algebra course or textbook?

[Ben Selfridge]

Nope, they are my own synthesis of the material in a somewhat quirky way, but they're pretty good visually for just reading: https://github.com/benjaminselfridge/group-theory-course/tree/main/GroupTheoryCourse/Completed