Group and CommGroup: is this what coercions do?

Stream: new members

[Robert Culling]

Kia ora :nerd:

My code is below, but my question is this: If I prove a bunch of theorems about groups, then do I have to write some sort of coercion to use those theorems to prove facts about Abelian groups?

With the following definitions I prove some elementary theorems in group theory:

-- Magma are a type (set) with a single binary operation.
class Magma (α : Type) where
  bop : α → α → α

instance [Magma α] : HMul α α α where
  hMul := Magma.bop

open Magma

-- Semirgroups are a Magma whose binary operation is associative.
class Semigroup (G : Type) extends Magma G where
  bop_assoc : ∀ x y z : G, (x * y) * z = x * (y * z)

open Semigroup

-- Monoids are Semigroups with an identity.
class Monoid (G : Type) extends Semigroup G where
  e : G
  id_bop : ∀ x : G, e * x = x

open Monoid

-- Groups are Monoids with inverses.
class Group (G : Type) extends Monoid G where
  inv : G → G
  inv_bop : ∀ x : G, (inv x) * x = e

postfix: 100 " ⁻¹ " => Group.inv

open Group

Including the fact that ∀ x : G, x * e = x

theorem bop_id (G : Type) (t : Group G) :
  ∀ x : G, x * e = x :=
    by
      intro g
      calc g * e
        _ = g * (g⁻¹ * g)     := by rw [inv_bop]
        _ = (g * g⁻¹) * g     := by rw [bop_assoc]
        _ = e * g             := by rw [bop_inv]
        _ = g                 := by rw [id_bop]

When I add in the class of Abelian groups

-- Abelian Groups are Groups whose binary operation is commutative.
class AbelianGroup (G : Type) extends Group G where
  bop_comm : ∀ x y : G, x * y = y * x

open AbelianGroup

theorem commbop_id (G : Type) (t : AbelianGroup G) :
  ∀ x : G, (x * e) = x :=
    by
      intro g
      rw [bop_comm, id_bop]

I can prove the same theorem with a simpler argument. But If I wanted to employ all the theorems I have proven about groups more generally, then do I need to employ a coercion from AbelianGroup to Group? If so, how does that work?

Thanks!

[N Gelwan]

If you use an instance implicit argument (ex theorem bop_id (G : Type) [Group G] : ...) then lean will use the extends clause that you have in your AbelianGroup class definition to automatically synthesize a Group instance from an AbelianGroup instance, and you should get your theorems for free.

[N Gelwan]

I think this covers it: https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html#basics