Definition of Group, Abelian Group, Ring and Homomorphisms for them.

AbstractAlgebra.lean

universe u

class Group (G : Type u) extends Add G where
  inv : G → G
  e   : G

  add_assoc     : ∀ a b c : G, (a + b) + c = a + (b + c)
  add_left_inv  : ∀ a : G, (inv a) + a = e
  add_right_inv : ∀ a : G, a + (inv a) = e
  add_left_id   : ∀ a : G, e + a = a
  add_right_id  : ∀ a : G, a + e = a

class AbelianGroup (G : Type u) extends Group G where
  add_comm : ∀ a b : G, a + b = b + a

structure GroupHom (G H : Type u) [Group G] [Group H] where
  toFun : G → H
  map_add : ∀ a b : G, toFun (a + b) = toFun a + toFun b

infixr:25 " →+ " => GroupHom

def GroupHom.comp {G H K : Type u} [Group G] [Group H] [Group K]
  (f : H →+ K) (g : G →+ H) : G →+ K :=
  { toFun := f.toFun ∘ g.toFun, map_add := by simp [f.map_add, g.map_add] }

def GroupHom.id (G : Type u) [Group G] : G →+ G :=
  { toFun := λ a => a, map_add := by simp }

class Ring (R : Type u) extends Add R, Mul R where
  -- add
  zero : R
  neg : R → R

  add_assoc     : ∀ a b c : R, (a + b) + c = a + (b + c)
  add_comm      : ∀ a b : R, a + b = b + a
  add_left_id   : ∀ a : R, zero + a = a
  add_right_id  : ∀ a : R, a + zero = a
  add_left_neg  : ∀ a : R, (neg a) + a = zero
  add_right_neg : ∀ a : R, a + (neg a) = zero

  -- mul
  one : R

  mul_assoc    : ∀ a b c : R, (a * b) * c = a * (b * c)
  mul_left_id  : ∀ a : R, one * a = a
  mul_right_id : ∀ a : R, a * one = a

  -- distributivity
  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)

structure RingHom (R S : Type u) [Ring R] [Ring S] where
  toFun : R → S
  map_add : ∀ a b : R, toFun (a + b) = toFun a + toFun b
  map_mul : ∀ a b : R, toFun (a * b) = toFun a * toFun b
  map_one : toFun Ring.one = Ring.one

infixr:25 " →* " => RingHom

def RingHom.comp {R S T : Type u} [Ring R] [Ring S] [Ring T]
  (f : S →* T) (g : R →* S) : R →* T :=
  { toFun := f.toFun ∘ g.toFun,
    map_add := by simp [f.map_add, g.map_add],
    map_mul := by simp [f.map_mul, g.map_mul],
    map_one := by simp [f.map_one, g.map_one] }

def RingHom.id (R : Type u) [Ring R] : R →* R :=
  { toFun := λ a => a,
    map_add := by simp,
    map_mul := by simp,
    map_one := by simp }

namespace Instances

instance instGroupIntAdd : Group Int where
  add := Int.add
  inv := Int.neg
  e   := 0

  add_assoc     := Int.add_assoc
  add_left_inv  := Int.add_left_neg
  add_right_inv := Int.add_right_neg
  add_left_id   := Int.zero_add
  add_right_id  := Int.add_zero

instance instAbelianGroupIntAdd : AbelianGroup Int where
  add_comm := Int.add_comm

instance instRingInt : Ring Int where
  add := Int.add
  zero := 0
  neg := Int.neg
  mul := Int.mul
  one := 1

  add_assoc     := Int.add_assoc
  add_comm      := Int.add_comm
  add_left_id   := Int.zero_add
  add_right_id  := Int.add_zero
  add_left_neg  := Int.add_left_neg
  add_right_neg := Int.add_right_neg

  mul_assoc    := Int.mul_assoc
  mul_left_id  := Int.one_mul
  mul_right_id := Int.mul_one

  left_distrib  := Int.mul_add
  right_distrib := Int.add_mul

end Instances