groups and rings in mathlib

Stream: maths

[Bulhwi Cha]

The graph below shows how (additive) groups and rings are defined in Mathlib: groups_and_rings.jpg

[Jireh Loreaux]

Looks very nice. Did you do the layout manually I suppose?

[Yury G. Kudryashov]

What did you use to draw this?

[Bulhwi Cha]

Jireh Loreaux said:

Looks very nice. Did you do the layout manually I suppose?

Yes. I used my iPad Mini, Apple Pencil, and GoodNotes to make the diagram. Next time, I should use Graphviz instead.

[Yury G. Kudryashov]

Is there an editable version?

[Bulhwi Cha]

I'm afraid you can edit GoodNotes documents only with the GoodNotes app.

• groups_and_rings.goodnotes
• groups_and_rings.pdf

[Scott Morrison]

Would it be helpful to have some dotted arrows indicating extra instances?

For example looking at this diagram one might be mislead about whether having a Ring gives you a NonAssocRing.

[Bulhwi Cha]

Hmm, I guess so. It's hard to draw dotted arrows on GoodNotes.

[Bulhwi Cha]

The code below lists the axioms of each algebraic structure:

Lean code

import Mathlib.Algebra.Ring.Defs

noncomputable section

opaque S : Type u
axiom S_add : S → S → S

instance : Add S where
  add := S_add

axiom S_add_assoc : ∀ a b c : S, a + b + c = a + (b + c)

instance : AddSemigroup S where
  add := S_add
  add_assoc := S_add_assoc

axiom S_zero : S

instance : Zero S where
  zero := S_zero

axiom S_zero_add : ∀ a : S, 0 + a = a
axiom S_add_zero : ∀ a : S, a + 0 = a

instance : AddMonoid S where
  add := S_add
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero

axiom S_add_comm : ∀ a b : S, a + b = b + a

instance : AddCommMonoid S where
  add := S_add
  add_comm  := S_add_comm
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero

axiom S_mul : S → S → S

instance : Mul S where
  mul := S_mul

axiom S_mul_assoc : ∀ a b c : S, a * b * c = a * (b * c)

instance : Semigroup S where
  mul := S_mul
  mul_assoc := S_mul_assoc

axiom S_one : S

instance : One S where
  one := S_one

axiom S_one_mul : ∀ a : S, 1 * a = a
axiom S_mul_one : ∀ a : S, a * 1 = a

instance : Monoid S where
  mul := S_mul
  mul_assoc := S_mul_assoc
  one := S_one
  one_mul := S_one_mul
  mul_one := S_mul_one

axiom S_left_distrib  : ∀ a b c : S, a * (b + c) = a * b + a * c
axiom S_right_distrib : ∀ a b c : S, (a + b) * c = a * c + b * c
axiom S_zero_mul : ∀ a : S, 0 * a = 0
axiom S_mul_zero : ∀ a : S, a * 0 = 0

instance : Semiring S where
  -- `(S, +)` is a commutative monoid
  add := S_add
  add_comm  := S_add_comm
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero
  -- `(S, *)` is a monoid
  mul := S_mul
  mul_assoc := S_mul_assoc
  one := S_one
  one_mul := S_one_mul
  mul_one := S_mul_one
  -- multiplication distributes over addition
  left_distrib  := S_left_distrib
  right_distrib := S_right_distrib
  -- multiplication by `0` annihilates `S`
  zero_mul := S_zero_mul
  mul_zero := S_mul_zero

axiom S_neg : S → S

instance : Neg S where
  neg := S_neg

axiom S_add_left_neg : ∀ a : S, -a + a = 0

instance : AddGroup S where
  add := S_add
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero
  neg := S_neg
  add_left_neg := S_add_left_neg
  sub := fun a b : S ↦ a + -b

instance : AddCommGroup S where
  add := S_add
  add_comm  := S_add_comm
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero
  neg := S_neg
  add_left_neg := S_add_left_neg
  sub := fun a b : S ↦ a + -b

instance : Ring S where
  -- `(S, +)` is a commutative group
  add := S_add
  add_comm  := S_add_comm
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero
  neg := S_neg
  add_left_neg := S_add_left_neg
  sub := fun a b : S ↦ a + -b
  -- `(S, *)` is a monoid
  mul := S_mul
  mul_assoc := S_mul_assoc
  one := S_one
  one_mul := S_one_mul
  mul_one := S_mul_one
  -- multiplication distributes over addition
  left_distrib  := S_left_distrib
  right_distrib := S_right_distrib
  -- multiplication by `0` annihilates `S`
  zero_mul := S_zero_mul
  mul_zero := S_mul_zero

axiom S_mul_comm : ∀ a b : S, a * b = b * a

instance : CommRing S where
  -- `(S, +)` is a commutative group
  add := S_add
  add_comm := S_add_comm
  add_assoc := S_add_assoc
  zero := S_zero
  zero_add := S_zero_add
  add_zero := S_add_zero
  neg := S_neg
  add_left_neg := S_add_left_neg
  sub := fun a b : S ↦ a + -b
  -- `(S, *)` is a commutative monoid
  mul := S_mul
  mul_comm := S_mul_comm
  mul_assoc := S_mul_assoc
  one := S_one
  one_mul := S_one_mul
  mul_one := S_mul_one
  -- multiplication distributes over addition
  left_distrib  := S_left_distrib
  right_distrib := S_right_distrib
  -- multiplication by `0` annihilates `S`
  zero_mul := S_zero_mul
  mul_zero := S_mul_zero

end