# 7. Hierarchies

We have seen in Chapter 6 how to define the class of groups and build instances of this class, and then how to build an instance of the commutative ring class. But of course there is a hierarchy here: a commutative ring is in particular an additive group. In this chapter we will study how to build such hierarchies. They appear in all branches of mathematics but in this chapter the emphasis will be on algebraic examples.

It may seem premature to discuss how to build hierarchies before more discussions about using existing hierarchies. But some understanding of the technology underlying hierarchies is required to use them. So you should probably still read this chapter, but without trying too hard to remember everything on your first read, then read the following chapters and come back here for a second reading.

In this chapter, we will redefine (simpler versions of) many things that appear in Mathlib so we will used indices to distinguish our version. For instance we will have `Ring₁` as our version of `Ring`. Since we will gradually explain more powerful ways of formalizing structures, those indices will sometimes grow beyond one.

## 7.1. Basics

At the very bottom of all hierarchies in Lean, we find data-carrying classes. The following class records that the given type `α` is endowed with a distinguished element called `one`. At this stage, it has no property at all.

    class One₁ (α : Type) where
      /-- The element one -/
      one : α

Since we’ll make a much heavier use of classes in this chapter, we need to understand some more details about what the `class` command is doing. First, the `class` command above defines a structure `One₁` with parameter `α : Type` and a single field `one`. It also mark this structure as a class so that arguments of type `One₁ α` for some type `α` will be inferrable using the instance resolution procedure, as long as they are marked as instance-implicit, ie appear between square brackets. Those two effects could also have been achieved using the `structure` command with `class` attribute, ie writing `@[class] structure` instance of `class`. But the class command also ensures that `One₁ α` appears as an instance-implicit argument in its own fields. Compare:

    #check One₁.one -- One₁.one {α : Type} [self : One₁ α] : α

    @[class] structure One₂ (α : Type) where
      /-- The element one -/
      one : α

    #check One₂.one

In the second check, we can see that `self : One₂ α` is an explicit argument. Let us make sure the first version is indeed usable without any explicit argument.

    example (α : Type) [One₁ α] : α := One₁.one

Remark: in the above example, the argument `One₁ α` is marked as instance-implicit, which is a bit silly since this affects only uses of the declaration and declaration created by the `example` command cannot be used. However it allows us to avoid giving a name to that argument and, more importantly, it starts installing the good habit of marking `One₁ α` arguments as instance-implicit.

Another remark is that all this will work only when Lean knows what is `α`. In the above example, leaving out the type ascription `: α` would generate an error message like: `typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α)` where `?m.263 α` means “some type depending on `α`” (and 263 is simply an auto-generated index that would be useful to distinguish between several unknown things). Another way to avoid this issue would be to use a type annotation, as in:

    example (α : Type) [One₁ α] := (One₁.one : α)

You may have already encountered that issue when playing with limits of sequences in Section 3.6 if you tried to state for instance that `0 < 1` without telling Lean whether you meant this inequality to be about natural numbers or real numbers.

Our next task is to assign a notation to `One₁.one`. Since we don’t want collisions with the builtin notation for `1`, we will use `𝟙`. This is achieved by the following command where the first line tells Lean to use the documentation of `One₁.one` as documentation for the symbol `𝟙`.

    @[inherit_doc]
    notation "𝟙" => One₁.one

    example {α : Type} [One₁ α] : α := 𝟙

    example {α : Type} [One₁ α] : (𝟙 : α) = 𝟙 := rfl

We now want a data-carrying class recording a binary operation. We don’t want to choose between addition and multiplication for now so we’ll use diamond.

    class Dia₁ (α : Type) where
      dia : α → α → α

    infixl:70 " ⋄ "   => Dia₁.dia

As in the `One₁` example, the operation has no property at all at this stage. Let us now define the class of semigroup structures where the operation is denoted by `⋄`. For now, we define it by hand as a structure with two fields, a `Dia₁` instance and some `Prop`-valued field `dia_assoc` asserting associativity of `⋄`.

    class Semigroup₁ (α : Type) where
      toDia₁ : Dia₁ α
      /-- Diamond is associative -/
      dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Note that while stating dia_assoc, the previously defined field toDia₁ is in the local context hence can be used when Lean searches for an instance of Dia₁ α to make sense of a ⋄ b. However this toDia₁ field does not become part of the type class instances database. Hence doing `example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b` would fail with error message `failed to synthesize instance Dia₁ α`.

We can fix this by adding the `instance` attribute later.

    attribute [instance] Semigroup₁.toDia₁

    example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b

Before building up, we need a more convenient way to extend structures than explicitly writing fields like toDia₁ and adding the instance attribute by hand. The `class` supports this using the `extends` syntax as in:

    class Semigroup₂ (α : Type) extends Dia₁ α where
      /-- Diamond is associative -/
      dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

    example {α : Type} [Semigroup₂ α] (a b : α) : α := a ⋄ b

Note this syntax is also available in the `structure` command, although it that case it fixes only the hurdle of writing fields such as toDia₁ since there is no instance to define in that case.

Let us now try to combine a diamond operation and a distinguished one with axioms saying this element is neutral on both sides.

    class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
      /-- One is a left neutral element for diamond. -/
      one_dia : ∀ a : α, 𝟙 ⋄ a = a
      /-- One is a right neutral element for diamond -/
      dia_one : ∀ a : α, a ⋄ 𝟙 = a

In the next example, we tell Lean that `α` has a `DiaOneClass₁` structure and state a property that uses both a Dia₁ instance and a One₁ instance. In order to see how Lean finds those instances we set a tracing option whose result can be seen in the Infoview. This result is rather terse by default but it can be expanded by clicking on lines ending with black arrows. It includes failed attempts where Lean tried to find instances before having enough type information to succeed. The successful attempts do involve the instances generated by the `extends` syntax.

    set_option trace.Meta.synthInstance true in
    example {α : Type} [DiaOneClass₁ α] (a b : α) : Prop := a ⋄ b = 𝟙

Note that we don’t need to include extra fields where combining existing classes. Hence we can define monoids as:

    class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

While the above definition seems straightforward, it hides an important subtlety. Both `Semigroup₁ α` and `DiaOneClass₁ α` extend `Dia₁ α`, so one could fear that having a `Monoid₁ α` instance gives two unrelated diamond operations on `α`, one coming from a field `Monoid₁.toSemigroup₁` and one coming from a field `Monoid₁.toDiaOneClass₁`.

Indeed if we try to build a monoid class by hand using:

    class Monoid₂ (α : Type) where
      toSemigroup₁ : Semigroup₁ α
      toDiaOneClass₁ : DiaOneClass₁ α

then we get two completely unrelated diamond operations `Monoid₂.toSemigroup₁.toDia₁.dia` and `Monoid₂.toDiaOneClass₁.toDia₁.dia`.

The version generated using the `extends` syntax does not have this defect.

    example {α : Type} [Monoid₁ α] :
      (Monoid₁.toSemigroup₁.toDia₁.dia : α → α → α) = Monoid₁.toDiaOneClass₁.toDia₁.dia := rfl

So the `class` command did some magic for us (and the `structure` command would have done it too). An easy way to see what are the fields of our classes is to check their constructor. Compare:

    /- Monoid₂.mk {α : Type} (toSemigroup₁ : Semigroup₁ α) (toDiaOneClass₁ : DiaOneClass₁ α) : Monoid₂ α -/
    #check Monoid₂.mk

    /- Monoid₁.mk {α : Type} [toSemigroup₁ : Semigroup₁ α] [toOne₁ : One₁ α] (one_dia : ∀ (a : α), 𝟙 ⋄ a = a) (dia_one : ∀ (a : α), a ⋄ 𝟙 = a) : Monoid₁ α -/
    #check Monoid₁.mk

So we see that `Monoid₁` takes `Semigroup₁ α` argument as expected but then it won’t take a would-be overlapping `DiaOneClass₁ α` argument but instead tears it apart and includes only the non-overlapping parts. And it also auto-generated an instance `Monoid₁.toDiaOneClass₁` which is not a field but has the expected signature which, from the end-user point of view, restores the symmetry between the two extended classes `Semigroup₁` and `DiaOneClass₁`.

    #check Monoid₁.toSemigroup₁
    #check Monoid₁.toDiaOneClass₁

We are now very close to defining groups. We could add to the monoid structure a field asserting the existence of an inverse for every element. But then we would need to work to access these inverses. In practice it is more convenient to add it as data. To optimize reusability, we define a new data-carrying class, and then give it some notation.

    class Inv₁ (α : Type) where
      /-- The inversion function -/
      inv : α → α

    @[inherit_doc]
    postfix:max "⁻¹" => Inv₁.inv

    class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
      inv_dia : ∀ a : G, a⁻¹ ⋄ a = 𝟙

The above definition may seem too weak, we only ask that `a⁻¹` is a left-inverse of `a`. But the other side is automatic. In order to prove that, we need a preliminary lemma.

    lemma left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
      rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]

In this lemma, it is pretty annoying to give full names, especially since it requires knowing which part of the hierarchy provides those facts. One way to fix this is to use the `export` command to copy those facts as lemmas in the root name space.

    export DiaOneClass₁ (one_dia dia_one)
    export Semigroup₁ (dia_assoc)
    export Group₁ (inv_dia)

We can then rewrite the above proof as:

    example {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
      rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]

It is now your turn to prove things about our algebraic structures.

    lemma inv_eq_of_dia [Group₁ G] {a b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b :=
      sorry

    lemma dia_inv [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙 :=
      sorry

At this stage we would like to move on to define rings, but there is a serious issue. A ring structure on a type contains both an additive group structure and a multiplicative monoid structure, and some properties about their interaction. But so far we hard-coded a notation `⋄` for all our operations. More fundamentally, the type class system assumes every type has only one instance of each type class. There are various ways to solve this issue. Surprisingly Mathlib uses the naive idea to duplicate everything for additive and multiplicative theories with the help of some code-generating attribute. Structures and classes are defined in both additive and multiplicative notation with an attribute `to_additive` linking them. In case of multiple inheritance like for semi-groups, the auto-generated “symmetry-restoring” instances need also to be marked. This is a bit technical; you don’t need to understand details. The important point is that lemmas are then only stated in multiplicative notation and marked with the attribute `to_additive` to generate the additive version as `left_inv_eq_right_inv'` with its auto-generated additive version `left_neg_eq_right_neg'`. In order to check the name of this additive version we used the `whatsnew in` command on top of `left_inv_eq_right_inv'`.

    class AddSemigroup₃ (α : Type) extends Add α where
    /-- Addition is associative -/
      add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

    @[to_additive AddSemigroup₃]
    class Semigroup₃ (α : Type) extends Mul α where
    /-- Multiplication is associative -/
      mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

    class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

    @[to_additive AddMonoid₃]
    class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

    attribute [to_additive existing] Monoid₃.toMulOneClass

    export Semigroup₃ (mul_assoc₃)
    export AddSemigroup₃ (add_assoc₃)

    whatsnew in
    @[to_additive]
    lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
      rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]

    #check left_neg_eq_right_neg'

Equipped with this technology, we can easily define also commutative semigroups, monoids and groups, and then define rings.

    class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
      add_comm : ∀ a b : α, a + b = b + a

    @[to_additive AddCommSemigroup₃]
    class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
      mul_comm : ∀ a b : α, a * b = b * a

    class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

    @[to_additive AddCommMonoid₃]
    class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

    class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
      neg_add : ∀ a : G, -a + a = 0

    @[to_additive AddGroup₃]
    class Group₃ (G : Type) extends Monoid₃ G, Inv G where
      inv_mul : ∀ a : G, a⁻¹ * a = 1

We should remember to tag lemmas with `simp` when appropriate.

    attribute [simp] Group₃.inv_mul AddGroup₃.neg_add

Then we need to repeat ourselves a bit since we switch to standard notations, but at least `to_additive` does the work of translating from the multiplicative notation to the additive one.

    @[to_additive]
    lemma inv_eq_of_mul [Group₃ G] {a b : G} (h : a * b = 1) : a⁻¹ = b :=
      sorry

Note that `to_additive` can be asked to tag a lemma with `simp` and propagate that attribute to the additive version as follows.

    @[to_additive (attr := simp)]
    lemma Group₃.mul_inv {G : Type} [Group₃ G] {a : G} : a * a⁻¹ = 1 := by
      sorry

    @[to_additive]
    lemma mul_left_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : a * b = a * c) : b = c := by
      sorry

    @[to_additive]
    lemma mul_right_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : b*a = c*a) : b = c := by
      sorry

    class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

    @[to_additive AddCommGroup₃]
    class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G

We are now ready for rings. For demonstration purposes we won’t assume that addition is commutative, and then immediately provide an instance of `AddCommGroup₃`. Mathlib does not play this game, first because in practice this does not make any ring instance easier and also because Mathlib’s algebraic hierarchy goes through semirings which are like rings but without opposites so that the proof below does not work for them. What we gain here, besides a nice exercise if you have never seen it, is an example of building an instance using the syntax that allows to provide a parent structure and some extra fields.

    class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
      /-- Multiplication is left distributive over addition -/
      left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
      /-- Multiplication is right distributive over addition -/
      right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

    instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
    { Ring₃.toAddGroup₃ with
      add_comm := by
        sorry }

Of course we can also build concrete instances, such as a ring structure on integers (of course the instance below uses that all the work is already done in Mathlib).

    instance : Ring₃ ℤ where
      add := (· + ·)
      add_assoc₃ := add_assoc
      zero := 0
      zero_add := by simp
      add_zero := by simp
      neg := (- ·)
      neg_add := by simp
      mul := (· * ·)
      mul_assoc₃ := mul_assoc
      one := 1
      one_mul := by simp
      mul_one := by simp
      zero_mul := by simp
      mul_zero := by simp
      left_distrib := Int.mul_add
      right_distrib := Int.add_mul

As an exercise you can now set up a simple hierarchy for order relations, including a class for ordered commutative monoids, which have both a partial order and a commutative monoid structure such that `∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b`. Of course you need to add fields and maybe `extends` clauses to the following classes.

    class LE₁ (α : Type) where
      /-- The Less-or-Equal relation. -/
      le : α → α → Prop

    @[inherit_doc] infix:50 " ≤₁ " => LE₁.le

    class Preorder₁ (α : Type)

    class PartialOrder₁ (α : Type)

    class OrderedCommMonoid₁ (α : Type)

    instance : OrderedCommMonoid₁ ℕ where

We now want to discuss algebraic structures involving several types. The prime example is modules over rings. If you don’t know what is a module, you can pretend it means vector space and think that all our rings are fields. Those structures are commutative additive groups equipped with a scalar multiplication by elements of some ring.

We first define the data-carrying type class of scalar multiplication by some type `α` on some type `β`, and give it a right associative notation.

    class SMul₃ (α : Type) (β : Type) where
      /-- Scalar multiplication -/
      smul : α → β → β

    infixr:73 " • " => SMul₃.smul

Then we can define modules (again think about vector spaces if you don’t know what is a module).

    class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
      zero_smul : ∀ m : M, (0 : R) • m = 0
      one_smul : ∀ m : M, (1 : R) • m = m
      mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
      add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
      smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

There is something interesting going on here. While it isn’t too surprising that the ring structure on `R` is a parameter in this definition, you probably expected `AddCommGroup₃ M` to be part of the `extends` clause just as `SMul₃ R M` is. Trying to do that would lead to a mysterious sounding error message: `cannot find synthesization order for instance Module₁.toAddCommGroup₃ with type (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M all remaining arguments have metavariables: Ring₃ ?R @Module₁ ?R ?inst✝ M`. In order to understand this message, you need to remember that such an `extends` clause would lead to a field `Module₃.toAddCommGroup₃` marked as an instance. This instance would have the signature appearing in the error message: `(R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M`. With such an instance in the type class database, each time Lean would look for a `AddCommGroup₃ M` instance for some `M`, it would need to go hunting for a completely unspecified type `R` and a `Ring₃ R` instance before embarking on the main quest of finding a `Module₁ R M` instance. Those two side-quests are represented by the meta-variables mentioned in the error message and denoted by `?R` and `?inst✝` there. Such a `Module₃.toAddCommGroup₃` instance would then be a huge trap for the instance resolution procedure and then `class` command refuses to set it up.

What about `extends SMul₃ R M` then? That one creates a field `Module₁.toSMul₃ : {R : Type} → [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M` whose end result `SMul₃ R M` mentions both `R` and `M` so this field can safely be used as an instance. The rule is easy to remember: each class appearing in the `extends` clause should mention every type appearing in the parameters.

Let us create our first module instance: a ring is a module over itself using its multiplication as a scalar multiplication.

    instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
      smul := fun r s ↦ r*s
      zero_smul := zero_mul
      one_smul := one_mul
      mul_smul := mul_assoc₃
      add_smul := Ring₃.right_distrib
      smul_add := Ring₃.left_distrib

As a second example, every abelian group is a module over `ℤ` (this is one of the reason to generalize the theory of vector spaces by allowing non-invertible scalars). First one can define scalar multiplication by a natural number for any type equipped with a zero and an addition: `n • a` is defined as `a + ⋯ + a` where `a` appears `n` times. Then this is extended to scalar multiplication by an integer by ensuring `(-1) • a = -a`.

    def nsmul₁ [Zero M] [Add M] : ℕ → M → M
      | 0, _ => 0
      | n + 1, a => a + nsmul₁ n a

    def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
      | Int.ofNat n, a => nsmul₁ n a
      | Int.negSucc n, a => -nsmul₁ n.succ a

Proving this gives rise to a module structure is a bit tedious and not interesting for the current discussion, so we will sorry all axioms. You are not asked to replace those sorries with proofs. If you insist on doing it then you will probably want to state and prove several intermediate lemmas about `nsmul₁` and `zsmul₁`.

    instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
      smul := zsmul₁
      zero_smul := sorry
      one_smul := sorry
      mul_smul := sorry
      add_smul := sorry
      smul_add := sorry

A much more important issue is that we now have two module structures over the ring `ℤ` for `ℤ` itself: `abGrpModule ℤ` since `ℤ` is a abelian group, and `selfModule ℤ` since `ℤ` is a ring. Those two module structure correspond to the same abelian group structure, but it is not obvious that they have the same scalar multiplication. They actually do, but this isn’t true by definition, it requires a proof. This is very bad news for the type class instance resolution procedure and will lead to very frustrating failures for users of this hierarchy. When directly asked to find an instance, Lean will pick one, and we can see which one using:

    #synth Module₁ ℤ ℤ -- abGrpModule ℤ

But in a more indirect context it can happen that Lean infers the one and then gets confused. This situation is known as a bad diamond. This has nothing to do with the diamond operation we used above, it refers to the way one can draw the paths from `ℤ` to its `Module₁ ℤ` going through either `AddCommGroup₃ ℤ` or `Ring₃ ℤ`.

It is important to understand that not all diamonds are bad. In fact there are diamonds everywhere in Mathlib, and also in this chapter. Already at the very beginning we saw one can go from `Monoid₁ α` to `Dia₁ α` through either `Semigroup₁ α` or `DiaOneClass₁ α` and thanks to the work done by the `class` command, the resulting two `Dia₁ α` instances are definitionally equal. In particular a diamond having a `Prop`-valued class at the bottom cannot be bad since any too proofs of the same statement are definitionally equal.

But the diamond we created with modules is definitely bad. The offending piece is the `smul` field which is data, not a proof, and we have two constructions that are not definitionally equal. The robust way of fixing this issue is to make sure that going from a rich structure to a poor structure is always done by forgetting data, not by defining data. This well-known pattern as been named “forgetful inheritance” and extensively discussed in https://inria.hal.science/hal-02463336.

In our concrete case, we can modify the definition of `AddMonoid₃` to include a `nsmul` data field and some `Prop`-valued fields ensuring this operation is provably the one we constructed above. Those fields are given default values using `:=` after their type in the definition below. Thanks to these default values, most instances would be constructed exactly as with our previous definitions. But in the special case of `ℤ` we will be able to provide specific values.

    class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
      /-- Multiplication by a natural number. -/
      nsmul : ℕ → M → M := nsmul₁
      /-- Multiplication by `(0 : ℕ)` gives `0`. -/
      nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
      /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
      nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

    instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M := ⟨AddMonoid₄.nsmul⟩

Let us check we can still construct a product monoid instance without providing the `nsmul` related fields.

    instance (M N : Type) [AddMonoid₄ M] [AddMonoid₄ N] : AddMonoid₄ (M × N) where
      add := fun p q ↦ (p.1 + q.1, p.2 + q.2)
      add_assoc₃ := fun a b c ↦ by ext <;> apply add_assoc₃
      zero := (0, 0)
      zero_add := fun a ↦ by ext <;> apply zero_add
      add_zero := fun a ↦ by ext <;> apply add_zero

And now let us handle the special case of `ℤ` where we want to build `nsmul` using the coercion of `ℕ` to `ℤ` and the multiplication on `ℤ`. Note in particular how the proof fields contain more work than in the default value above.

    instance : AddMonoid₄ ℤ where
      add := (· + ·)
      add_assoc₃ := Int.add_assoc
      zero := 0
      zero_add := Int.zero_add
      add_zero := Int.add_zero
      nsmul := fun n m ↦ (n : ℤ) * m
      nsmul_zero := Int.zero_mul
      nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
        by rw [Int.add_mul, Int.add_comm, Int.one_mul]

Let us check we solved our issue. Because Lean already has a definition of scalar multiplication of a natural number and an integer, and we want to make sure our instance is used, we won’t use the `•` notation but call `SMul.mul` and explicitly provide our instance defined above.

    example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

This story then continues with incorporating a `zsmul` field into the definition of groups and similar tricks. You are now ready to read the definition of monoids, groups, rings and modules in Mathlib. There are more complicated than what we have seen here, because they are part of a huge hierarchy, but all principles have been explained above.

As an exercise, you can come back to the order relation hierarchy you built above and try to incorporate a type class `LT₁` carrying the Less-Than notation `<₁` and make sure that every preorder comes with a `<₁` which has a default value built from `≤₁` and a `Prop`-valued field asserting the natural relation between those two comparison operators. -/

## 7.2. Morphisms

So far in this chapter, we discussed how to create a hierarchy of mathematical structures. But defining structures is not really completed until we have morphisms. There are two main approaches here. The most obvious one is to define a predicate on functions.

    def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop :=
      f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'

In this definition, it is a bit unpleasant to use a conjunction. In particular users will need to remember the ordering we chose when they want to access the two conditions. So we could use a structure instead.

    structure isMonoidHom₂ [Monoid G] [Monoid H] (f : G → H) : Prop where
      map_one : f 1 = 1
      map_mul : ∀ g g', f (g * g') = f g * f g'

Once we are here, it is even tempting to make it a class and use the type class instance resolution procedure to automatically infer `isMonoidHom₂` for complicated functions out of instances for simpler functions. For instance a composition of monoid morphisms is a monoid morphism and this seems like a useful instance. However such an instance would be very tricky for the resolution procedure since it would need to hunt down `g ∘ f` everywhere. Seeing it failing in `g (f x)` would be very frustrating. More generally one must always keep in mind that recognizing which function is applied in a given expression is a very difficult problem, called the “higher-order unification problem”. So Mathlib does not use this class approach.

A more fundamental question is whether we use predicates as above (using either a `def` or a `structure`) or use structures bundling a function and predicates. This is partly a psychological issue. It is extremely rare to consider a function between monoids that is not a morphism. It really feels like “monoid morphism” is not an adjective you can assign to a bare function, it is a noun. On the other hand one can argue that a continuous function between topological spaces is really a function that happens to be continuous. This is one reason why Mathlib has a `Continuous` predicate. For instance you can write:

    example : Continuous (id : ℝ → ℝ) := continuous_id

We still have bundles continuous functions, which are convenient for instance to put a topology on a space of continuous functions, but they are not the primary tool to work with continuity.

By contrast, morphisms between monoids (or other algebraic structures) are bundled as in:

    @[ext]
    structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H]  where
      toFun : G → H
      map_one : toFun 1 = 1
      map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

Of course we don’t want to type `toFun` everywhere so we register a coercion using the `CoeFun` type class. Its first argument is the type we want to coerce to a function. The second argument describes the target function type. In our case it is always `G → H` for every `f : MonoidHom₁ G H`. We also tag `MonoidHom₁.toFun` with the `coe` attribute to make sure it is displayed almost invisibly in the tactic state, simply by a `↑` prefix.

    instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
      coe := MonoidHom₁.toFun

    attribute [coe] MonoidHom₁.toFun

Let us check we can indeed apply a bundled monoid morphism to an element.

    example [Monoid G] [Monoid H] (f : MonoidHom₁ G H) : f 1 = 1 :=  f.map_one

We can do the same with other kind of morphisms until we reach ring morphisms.

    @[ext]
    structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H]  where
      toFun : G → H
      map_zero : toFun 0 = 0
      map_add : ∀ g g', toFun (g + g') = toFun g + toFun g'

    instance [AddMonoid G] [AddMonoid H] : CoeFun (AddMonoidHom₁ G H) (fun _ ↦ G → H) where
      coe := AddMonoidHom₁.toFun

    attribute [coe] AddMonoidHom₁.toFun

    @[ext]
    structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

There are a couple of issues about this approach. A minor one is we don’t quite know where to put the `coe` attribute since the `RingHom₁.toFun` does not exist, the relevant function is `MonoidHom₁.toFun ∘ RingHom₁.toMonoidHom₁` which is not a declaration that can be tagged with an attribute (but we could still define a `CoeFun (RingHom₁ R S) (fun _ ↦ R → S)` instance). A much more important one is that lemmas about monoid morphisms won’t directly apply to ring morphisms. This leaves the alternative of either juggling with `RingHom₁.toMonoidHom₁` each time we want to apply a monoid morphism lemma or restate every such lemmas for ring morphisms. Neither option is appealing so Mathlib uses a new hierarchy trick here. The idea is to define a type class for objects that are at least monoid morphisms, instantiate that class with both monoid morphisms and ring morphisms and use it to state every lemma. In the definition below, `F` could be `MonoidHom₁ M N`, or `RingHom₁ M N` if `M` and `N` have a ring structure.

    class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] where
      toFun : F → M → N
      map_one : ∀ f : F, toFun f 1 = 1
      map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

However there is a problem with the above implementation. We haven’t registered a coercion to function instance yet. Let us try to do it now.

    def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
      coe := MonoidHomClass₁.toFun

Making this an instance would be bad. When faced with something like `f x` where the type of `f` is not a function type, Lean will try to find a `CoeFun` instance to coerce `f` into a function. The above function has type: `{M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N)` so, when it trying to apply it, it wouldn’t be a priori clear to Lean in which order the unknown types `M`, `N` and `F` should be inferred. This is a kind of bad instance that is slightly different from the one we saw already, but it boils down to the same issue: without knowing `M`, Lean would have to search for a monoid instance on an unknown type, hence hopelessly try every monoid instance in the database. If you are curious to see the effect of such an instance you can type `set_option synthInstance.checkSynthOrder false in` on top of the above declaration, replace `def badInst` with `instance`, and look for random failures in this file.

Here the solution is easy, we need to tell Lean to first search what is `F` and then deduce `M` and `N`. This is done using the `outParam` function. This function is defined as the identity function, but is still recognized by the type class machinery and triggers the desired behavior. Hence we can retry defining our class, paying attention to the `outParam` function:

    class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] where
      toFun : F → M → N
      map_one : ∀ f : F, toFun f 1 = 1
      map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

    instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
      coe := MonoidHomClass₂.toFun

    attribute [coe] MonoidHomClass₂.toFun

Now we can proceed with our plan to instantiate this class.

    instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
      toFun := MonoidHom₁.toFun
      map_one := fun f ↦ f.map_one
      map_mul := fun f ↦ f.map_mul

    instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
      toFun := fun f ↦ f.toMonoidHom₁.toFun
      map_one := fun f ↦ f.toMonoidHom₁.map_one
      map_mul := fun f ↦ f.toMonoidHom₁.map_mul

As promised every lemma we prove about `f : F` assuming an instance of `MonoidHomClass₁ F` will apply both to monoid morphisms and ring morphisms. Let us see an example lemma and check it applies to both situations.

    lemma map_inv_of_inv [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] (f : F) {m m' : M} (h : m*m' = 1) :
        f m * f m' = 1 := by
      rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]

    example [Monoid M] [Monoid N] (f : MonoidHom₁ M N) {m m' : M} (h : m*m' = 1) : f m * f m' = 1 :=
    map_inv_of_inv f h

    example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r*r' = 1) : f r * f r' = 1 :=
    map_inv_of_inv f h

At first sight, it may look like we got back to our old bad idea of making `MonoidHom₁` a class. But we haven’t. Everything is shifted one level of abstraction up. The type class resolution procedure won’t be looking for functions, it will be looking for either `MonoidHom₁` or `RingHom₁`.

One remaining issue with our approach is the presence of repetitive code around the `toFun` field and the corresponding `CoeFun` instance and `coe` attribute. It would also be better to record that this pattern is used only for functions with extra properties, meaning that the coercion to functions should be injective. So Mathlib adds one more layer of abstraction with the base class `DFunLike` (where “DFun” stands for dependent function). Let us redefine our `MonoidHomClass` on top of this base layer.

    class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] extends
        DFunLike F M (fun _ ↦ N) where
      map_one : ∀ f : F, f 1 = 1
      map_mul : ∀ (f : F) g g', f (g * g') = f g * f g'

    instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N where
      coe := MonoidHom₁.toFun
      coe_injective' := MonoidHom₁.ext
      map_one := MonoidHom₁.map_one
      map_mul := MonoidHom₁.map_mul

Of course the hierarchy of morphisms does not stop here. We could go on and define a class `RingHomClass₃` extending `MonoidHomClass₃` and instantiate it on `RingHom` and then later on `AlgebraHom` (algebras are rings with some extra structure). But we’ve covered the main formalization ideas used in Mathlib for morphisms and you should be ready to understand how morphisms are defined in Mathlib.

As an exercise, you should try to define your class of bundled order-preserving function between ordered types, and then order preserving monoid morphisms. This is for training purposes only. Like continuous functions, order preserving functions are primarily unbundled in Mathlib where they are defined by the `Monotone` predicate. Of course you need to complete the class definitions below.

    @[ext]
    structure OrderPresHom (α β : Type) [LE α] [LE β] where
      toFun : α → β
      le_of_le : ∀ a a', a ≤ a' → toFun a ≤ toFun a'

    @[ext]
    structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends
    MonoidHom₁ M N, OrderPresHom M N

    class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β]

    instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where

    instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
        OrderPresHomClass (OrderPresMonoidHom α β) α β where

    instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
        MonoidHomClass₃ (OrderPresMonoidHom α β) α β
      := sorry

## 7.3. Sub-objects

After defining some algebraic structure and its morphisms, the next step is to consider sets that inherit this algebraic structure, for instance subgroups or subrings. This largely overlaps with our previous topic. Indeed a set in `X` is implemented as a function from `X` to `Prop` so sub-objects are function satisfying a certain predicate. Hence we can reuse of lot of the ideas that led to the `DFunLike` class and its descendants. We won’t reuse `DFunLike` itself because this would break the abstraction barrier from `Set X` to `X → Prop`. Instead there is a `SetLike` class. Instead of wrapping an injection into a function type, that class wraps an injection into a `Set` type and defines the corresponding coercion and `Membership` instance.

    @[ext]
    structure Submonoid₁ (M : Type) [Monoid M] where
      /-- The carrier of a submonoid. -/
      carrier : Set M
      /-- The product of two elements of a submonoid belongs to the submonoid. -/
      mul_mem {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
      /-- The unit element belongs to the submonoid. -/
      one_mem : 1 ∈ carrier

    /-- Submonoids in `M` can be seen as sets in `M`. -/
    instance [Monoid M] : SetLike (Submonoid₁ M) M where
      coe := Submonoid₁.carrier
      coe_injective' := Submonoid₁.ext

Equipped with the above `SetLike` instance, we can already state naturally that a submonoid `N` contains `1` without using `N.carrier`. We can also silently treat `N` as a set in `M` as take its direct image under a map.

    example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem

    example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N

We also have a coercion to `Type` which uses `Subtype` so, given a submonoid `N` we can write a parameter `(x : N)` which can be coerced to an element of `M` belonging to `N`.

    example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property

Using this coercion to `Type` we can also tackle the task of equipping a submonoid with a monoid structure. We will use the coercion from the type associated to `N` as above, and the lemma `SetCoe.ext` asserting this coercion is injective. Both are provided by the `SetLike` instance.

    instance SubMonoid₁Monoid [Monoid M] (N : Submonoid₁ M) : Monoid N where
      mul := fun x y ↦ ⟨x*y, N.mul_mem x.property y.property⟩
      mul_assoc := fun x y z ↦ SetCoe.ext (mul_assoc (x : M) y z)
      one := ⟨1, N.one_mem⟩
      one_mul := fun x ↦ SetCoe.ext (one_mul (x : M))
      mul_one := fun x ↦ SetCoe.ext (mul_one (x : M))

Note that, in the above instance, instead of using the coercion to `M` and calling the `property` field, we could have used destructuring binders as follows.

    example [Monoid M] (N : Submonoid₁ M) : Monoid N where
      mul := fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x*y, N.mul_mem hx hy⟩
      mul_assoc := fun ⟨x, _⟩ ⟨y, _⟩ ⟨z, _⟩ ↦ SetCoe.ext (mul_assoc x y z)
      one := ⟨1, N.one_mem⟩
      one_mul := fun ⟨x, _⟩ ↦ SetCoe.ext (one_mul x)
      mul_one := fun ⟨x, _⟩ ↦ SetCoe.ext (mul_one x)

In order to apply lemmas about submonoids to subgroups or subrings, we need a class, just like for morphisms. Note this class take a `SetLike` instance as a parameter so it does not need a carrier field and can use the membership notation in its fields.

    class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop where
      mul_mem : ∀ (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
      one_mem : ∀ s : S, 1 ∈ s

    instance [Monoid M] : SubmonoidClass₁ (Submonoid₁ M) M where
      mul_mem := Submonoid₁.mul_mem
      one_mem := Submonoid₁.one_mem

As an exercise you should define a `Subgroup₁` structure, endow it with a `SetLike` instance and a `SubmonoidClass₁` instance, put a `Group` instance on the subtype associated to a `Subgroup₁` and define a `SubgroupClass₁` class.

Another very important thing to know about subobjects of a given algebraic object in Mathlib always form a complete lattice, and this structure is used a lot. For instance you may look for the lemma saying that an intersection of submonoids is a submonoid. But this won’t be a lemma, this will be an infimum construction. Let us do the case of two submonoids.

    instance [Monoid M] : Inf (Submonoid₁ M) :=
      ⟨fun S₁ S₂ ↦
        { carrier := S₁ ∩ S₂
          one_mem := ⟨S₁.one_mem, S₂.one_mem⟩
          mul_mem := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ ↦ ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

This allows to get the intersections of two submonoids as a submonoid.

    example [Monoid M] (N P : Submonoid₁ M) : Submonoid₁ M := N ⊓ P

You may think it’s a shame that we had to use the inf symbol `⊓` in the above example instead of the intersection symbol `∩`. But think about the supremum. The union of two submonoids is not a submonoid. However submonoids still form a lattice (even a complete one). Actually `N ⊔ P` is the submonoid generated by the union of `N` and `P` and of course it would be very confusing to denote it by `N ∪ P`. So you can see the use of `N ⊓ P` as much more consistent. It is also a lot more consistent across various kind of algebraic structures. It may look a bit weird at first to see the sum of two vector subspace `E` and `F` denoted by `E ⊔ F` instead of `E + F`. But you will get used to it. And soon you will consider the `E + F` notation as a distraction emphasizing the anecdotal fact that elements of `E ⊔ F` can be written as a sum of an element of `E` and an element of `F` instead of emphasizing the fundamental fact that `E ⊔ F` is the smallest vector subspace containing both `E` and `F`.

Our last topic for this chapter is that of quotients. Again we want to explain how convenient notation are built and code duplication is avoided in Mathlib. Here the main device is the `HasQuotient` class which allows notations like `M ⧸ N`. Beware the quotient symbol `⧸` is a special unicode character, not a regular ASCII division symbol.

As an example, we will build the quotient of a commutative monoid by a submonoid, leave proofs to you. In the last example, you can use `Setoid.refl` but it won’t automatically pick up the relevant `Setoid` structure. You can fix this issue by providing all arguments using the `@` syntax, as in `@Setoid.refl M N.Setoid`.

    def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where
      r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x*w = y*z
      iseqv := {
        refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
        symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
        trans := by
          sorry
      }

    instance [CommMonoid M] : HasQuotient M (Submonoid M) where
      quotient' := fun N ↦ Quotient N.Setoid

    def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N := Quotient.mk N.Setoid

    instance [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
      mul := Quotient.map₂' (· * ·) (by
          sorry
            )
      mul_assoc := by
          sorry
      one := QuotientMonoid.mk N 1
      one_mul := by
          sorry
      mul_one := by
          sorry