# 8. Groups and Rings

We saw in Section 2.2 how to reason about operations in groups and rings. Later, in Section 6.2, we saw how to define abstract algebraic structures, such as group structures, as well as concrete instances such as the ring structure on the Gaussian integers. Chapter 7 explained how hierarchies of abstract structures are handled in Mathlib.

In this chapter we work with groups and rings in more detail. We won’t be able to cover every aspect of the treatment of these topics in Mathlib, especially since Mathlib is constantly growing. But we will provide entry points to the library and show how the essential concepts are used. There is some overlap with the discussion of Chapter 7, but here we will focus on how to use Mathlib instead of the design decisions behind the way the topics are treated. So making sense of some of the examples may require reviewing the background from Chapter 7.

## 8.1. Monoids and Groups

### 8.1.1. Monoids and their morphisms

Courses in abstract algebra often start with groups and
then progress to rings, fields, and vector spaces. This involves some contortions when discussing
multiplication on rings since the multiplication operation does not come from a group structure
but many of the proofs carry over verbatim from group theory to this new setting.
The most common fix, when doing mathematics with pen and paper,
is to leave those proofs as exercises. A less efficient but safer and
more formalization-friendly way of proceeding is to use monoids. A *monoid* structure on a type M
is an internal composition law that is associative and has a neutral element.
Monoids are used primarily to accommodate both groups and the multiplicative structure of
rings. But there are also a number of natural examples; for instance, the set of natural numbers
equipped with addition forms a monoid.

From a practical point of view, you can mostly ignore monoids when using Mathlib. But you need to know they exist when you are looking for a lemma by browsing Mathlib files. Otherwise, you might end up looking for a statement in the group theory files when it is actually in the found with monoids because it does not require elements to be invertible.

The type of monoid structures on a type `M`

is written `Monoid M`

.
The function `Monoid`

is a type class so it will almost always appear as an instance implicit
argument (in other words, in square brackets).
By default, `Monoid`

uses multiplicative notation for the operation; for additive notation
use `AddMonoid`

instead.
The commutative versions of these structures add the prefix `Comm`

before `Monoid`

.

```
example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y
```

Note that although `AddMonoid`

is found in the library,
it is generally confusing to use additive notation with a non-commutative operation.

The type of morphisms between monoids `M`

and `N`

is called `MonoidHom M N`

and written
`M →* N`

. Lean will automatically see such a morphism as a function from `M`

to `N`

when
we apply it to elements of `M`

. The additive version is called `AddMonoidHom`

and written
`M →+ N`

.

```
example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
f.map_mul x y
example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
f.map_zero
```

These morphisms are bundled maps, i.e. they package together a map and some of its properties.
Remember that Section 7.2 explains bundled maps;
here we simply note the slightly unfortunate consequence that we cannot use ordinary function
composition to compose maps. Instead, we need to use `MonoidHom.comp`

and `AddMonoidHom.comp`

.

```
example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
(f : M →+ N) (g : N →+ P) : M →+ P := g.comp f
```

### 8.1.2. Groups and their morphisms

We will have much more to say about groups, which are monoids with the extra property that every element has an inverse.

```
example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_self x
```

Similar to the `ring`

tactic that we saw earlier, there is a `group`

tactic that proves
any identity that holds in any group. (Equivalently, it proves the identities that hold in
free groups.)

```
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
group
```

There is also a tactic for identities in commutative additive groups called `abel`

.

```
example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
abel
```

Interestingly, a group
morphism is nothing more than a monoid morphism between groups. So we can copy and paste one of our
earlier examples, replacing `Monoid`

with `Group`

.

```
example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
f.map_mul x y
```

Of course we do get some new properties, such as this one:

```
example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
f.map_inv x
```

You may be worried that constructing group morphisms will require us to do unnecessary work since the definition of monoid morphism enforces that neutral elements are sent to neutral elements while this is automatic in the case of group morphisms. In practice the extra work is not hard, but, to avoid it, there is a function building a group morphism from a function between groups that is compatible with the composition laws.

```
example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
G →* H :=
MonoidHom.mk' f h
```

There is also a type `MulEquiv`

of group (or monoid) isomorphisms denoted by `≃*`

(and
`AddEquiv`

denoted by `≃+`

in additive notation).
The inverse of `f : G ≃* H`

is `MulEquiv.symm f : H ≃* G`

,
composition of `f`

and `g`

is `MulEquiv.trans f g`

, and
the identity isomorphism of `G`

is `M̀ulEquiv.refl G`

.
Using anonymous projector notation, the first two can be written `f.symm`

and
`f.trans g`

respectively.
Elements of this type are automatically coerced to morphisms and functions when necessary.

```
example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
f.trans f.symm = MulEquiv.refl G :=
f.self_trans_symm
```

One can use `MulEquiv.ofBijective`

to build an isomorphism from a bijective morphism.
Doing so makes the inverse function noncomputable.

```
noncomputable example {G H : Type*} [Group G] [Group H]
(f : G →* H) (h : Function.Bijective f) :
G ≃* H :=
MulEquiv.ofBijective f h
```

### 8.1.3. Subgroups

Just as group morphisms are bundled, a subgroup of `G`

is also a bundled structure consisting of
a set in `G`

with the relevant closure properties.

```
example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
x * y ∈ H :=
H.mul_mem hx hy
example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
x⁻¹ ∈ H :=
H.inv_mem hx
```

In the example above, it is important to understand that `Subgroup G`

is the type of subgroups
of `G`

, rather than a predicate `IsSubgroup H`

where `H`

is an element of `Set G`

.
`Subgroup G`

is endowed with a coercion to `Set G`

and a membership predicate on `G`

.
See Section 7.3 for an explanation of how and why this is done.

Of course, two subgroups are the same if and only if they have the same elements. This fact
is registered for use with the `ext`

tactic, which can be used to prove two subgroups are
equal in the same way it is used to prove that two sets are equal.

To state and prove, for example, that `ℤ`

is an additive subgroup of `ℚ`

,
what we really want is to construct a term of type `AddSubgroup ℚ`

whose projection to
`Set ℚ`

is `ℤ`

, or, more precisely, the image of `ℤ`

in `ℚ`

.

```
example : AddSubgroup ℚ where
carrier := Set.range ((↑) : ℤ → ℚ)
add_mem' := by
rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
use n + m
simp
zero_mem' := by
use 0
simp
neg_mem' := by
rintro _ ⟨n, rfl⟩
use -n
simp
```

Using type classes, Mathlib knows that a subgroup of a group inherits a group structure.

```
example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance
```

This example is subtle. The object `H`

is not a type, but Lean automatically coerces it to
a type by interpreting it as a subtype of `G`

.
So the above example can be restated more explicitly as:

```
example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance
```

An important benefit of having a type `Subgroup G`

instead of a predicate
`IsSubgroup : Set G → Prop`

is that one can easily endow `Subgroup G`

with additional structure.
Importantly, it has the structure of a complete lattice structure with respect to
inclusion. For instance, instead of having a lemma stating that an intersection of
two subgroups of `G`

is again a subgroup, we
have used the lattice operation `⊓`

to construct the intersection. We can then apply arbitrary
lemmas about lattices to the construction.

Let us check that the set underlying the infimum of two subgroups is indeed, by definition, their intersection.

```
example {G : Type*} [Group G] (H H' : Subgroup G) :
((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl
```

It may look strange to have a different notation for what amounts to the intersection of the
underlying sets, but the correspondence does not carry over to the supremum operation and set
union, since a union of subgroups is not, in general, a subgroup.
Instead one needs to use the subgroup generated by the union, which is done
using `Subgroup.closure`

.

```
example {G : Type*} [Group G] (H H' : Subgroup G) :
((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
rw [Subgroup.sup_eq_closure]
```

Another subtlety is that `G`

itself does not have type `Subgroup G`

,
so we need a way to talk about `G`

seen as a subgroup of `G`

.
This is also provided by the lattice structure: the full subgroup is the top element of
this lattice.

```
example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial
```

Similarly the bottom element of this lattice is the subgroup whose only element is the neutral element.

```
example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot
```

As an exercise in manipulating groups and subgroups, you can define the conjugate of a subgroup by an element of the ambient group.

```
def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
one_mem' := by
dsimp
sorry
inv_mem' := by
dsimp
sorry
mul_mem' := by
dsimp
sorry
```

Tying the previous two topics together, one can push forward and pull back subgroups using
group morphisms. The naming convention in Mathlib is to call those operations `map`

and `comap`

.
These are not the common mathematical terms, but they have the advantage of being
shorter than “pushforward” and “direct image.”

```
example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
Subgroup.map f G'
example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
Subgroup.comap f H'
#check Subgroup.mem_map
#check Subgroup.mem_comap
```

In particular, the preimage of the bottom subgroup under a morphism `f`

is a subgroup called
the *kernel* of `f`

, and the range of `f`

is also a subgroup.

```
example {G H : Type*} [Group G] [Group H] (f : G →* H) (g : G) :
g ∈ MonoidHom.ker f ↔ f g = 1 :=
f.mem_ker
example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) :
h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h :=
f.mem_range
```

As exercises in manipulating group morphisms and subgroups, let us prove some elementary properties.
They are already proved in Mathlib, so do not use `exact?`

too quickly if you want to benefit
from these exercises.

```
section exercises
variable {G H : Type*} [Group G] [Group H]
open Subgroup
example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
sorry
example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
sorry
variable {K : Type*} [Group K]
-- Remember you can use the `ext` tactic to prove an equality of subgroups.
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
comap (ψ.comp φ) U = comap φ (comap ψ U) := by
sorry
-- Pushing a subgroup along one homomorphism and then another is equal to
-- pushing it forward along the composite of the homomorphisms.
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
map (ψ.comp φ) S = map ψ (S.map φ) := by
sorry
end exercises
```

Let us finish this introduction to subgroups in Mathlib with two very classical results. Lagrange theorem states the cardinality of a subgroup of a finite group divides the cardinality of the group. Sylow’s first theorem is a famous partial converse to Lagrange’s theorem.

While this corner of Mathlib is partly set up to allow computation, we can tell
Lean to use nonconstructive logic anyway using the following `open scoped`

command.

```
open scoped Classical
open Fintype
example {G : Type*} [Group G] [Fintype G] (G' : Subgroup G) : card G' ∣ card G :=
⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩
open Subgroup
example {G : Type*} [Group G] [Fintype G] (p : ℕ) {n : ℕ} [Fact p.Prime]
(hdvd : p ^ n ∣ card G) : ∃ K : Subgroup G, card K = p ^ n :=
Sylow.exists_subgroup_card_pow_prime p hdvd
```

The next two exercises derive a corollary of Lagrange’s lemma. (This is also already in Mathlib,
so do not use `exact?`

too quickly.)

```
lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} [Fintype H] :
H = ⊥ ↔ card H = 1 := by
suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
simpa [eq_bot_iff_forall, card_eq_one_iff]
sorry
#check card_dvd_of_le
lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K]
(h : (card H).Coprime (card K)) : H ⊓ K = ⊥ := by
sorry
```

### 8.1.4. Concrete groups

One can also manipulate concrete groups in Mathlib, although this is typically more complicated
than working with the abstract theory.
For instance, given any type `X`

, the group of permutations of `X`

is `Equiv.Perm X`

.
In particular the symmetric group \(\mathfrak{S}_n\) is `Equiv.Perm (Fin n)`

.
One can state abstract results about this group, for instance saying that `Equiv.Perm X`

is
generated by cycles if `X`

is finite.

```
open Equiv
example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
Perm.closure_isCycle
```

One can be fully concrete and compute actual products of cycles. Below we use the `#simp`

command,
which calls the `simp`

tactic on a given expression. The notation `c[]`

is used to define a
cyclic permutation. In the example, the result is a permutation of `ℕ`

. One could use a type
ascription such as `(1 : Fin 5)`

on the first number appearing to make it a computation in
`Perm (Fin 5)`

.

```
#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]
```

Another way to work with concrete groups is to use free groups and group presentations.
The free group on a type `α`

is `FreeGroup α`

and the inclusion map is
`FreeGroup.of : α → FreeGroup α`

. For instance let us define a type `S`

with three elements denoted
by `a`

, `b`

and `c`

, and the element `ab⁻¹`

of the corresponding free group.

```
section FreeGroup
inductive S | a | b | c
open S
def myElement : FreeGroup S := (.of a) * (.of b)⁻¹
```

Note that we gave the expected type of the definition so that Lean knows that `.of`

means
`FreeGroup.of`

.

The universal property of free groups is embodied as the equivalence `FreeGroup.lift`

.
For example, let us define the group morphism from `FreeGroup S`

to `Perm (Fin 5)`

that
sends `a`

to `c[1, 2, 3]`

, `b`

to `c[2, 3, 1]`

, and `c`

to `c[2, 3]`

,

```
def myMorphism : FreeGroup S →* Perm (Fin 5) :=
FreeGroup.lift fun | .a => c[1, 2, 3]
| .b => c[2, 3, 1]
| .c => c[2, 3]
```

As a last concrete example, let us see how to define a group generated by a single element whose
cube is one (so that group will be isomorphic to \(\mathbb{Z}/3\)) and build a morphism
from that group to `Perm (Fin 5)`

.

As a type with exactly one element, we will use `Unit`

whose
only element is denoted by `()`

. The function `PresentedGroup`

takes a set of relations,
i.e. a set of elements of some free group, and returns a group that is this free group quotiented
by a normal subgroup generated by relations. (We will see how to handle more general quotients
in Section 8.1.6.) Since we somehow hide this behind a definition, we use `deriving Group`

to force creation
of a group instance on `myGroup`

.

```
def myGroup := PresentedGroup {.of () ^ 3} deriving Group
```

The universal property of presented groups ensures that morphisms out of this group can be built
from functions that send the relations to the neutral element of the target group.
So we need such a function and a proof that the condition holds. Then we can feed this proof
to `PresentedGroup.toGroup`

to get the desired group morphism.

```
def myMap : Unit → Perm (Fin 5)
| () => c[1, 2, 3]
lemma compat_myMap :
∀ r ∈ ({.of () ^ 3} : Set (FreeGroup Unit)), FreeGroup.lift myMap r = 1 := by
rintro _ rfl
simp
decide
def myNewMorphism : myGroup →* Perm (Fin 5) := PresentedGroup.toGroup compat_myMap
end FreeGroup
```

### 8.1.5. Group actions

One important way that group theory interacts with the rest of mathematics is through
the use of group actions.
An action of a group `G`

on some type `X`

is nothing more than a morphism from `G`

to
`Equiv.Perm X`

. So in a sense group actions are already covered by the previous discussion.
But we don’t want to carry this morphism around; instead, we want it to be inferred automatically
by Lean as much as possible. So we have a type class for this, which is `MulAction G X`

.
The downside of this setup is that having multiple actions of the same group on the same type
requires some contortions, such as defining type synonyms, each of which carries different
type class instances.

This allows us in particular to use `g • x`

to denote the action of a group element `g`

on
a point `x`

.

```
noncomputable section GroupActions
example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
g • (g' • x) = (g * g') • x :=
(mul_smul g g' x).symm
```

There is also a version for additive group called `AddAction`

, where the action is denoted by
`+ᵥ`

. This is used for instance in the definition of affine spaces.

```
example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
(add_vadd g g' x).symm
```

The underlying group morphism is called `MulAction.toPermHom`

.

```
open MulAction
example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
toPermHom G X
```

As an illustration let us see how to define the Cayley isomorphism embedding of any group `G`

into
a permutation group, namely `Perm G`

.

```
def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
Equiv.Perm.subgroupOfMulAction G G
```

Note that nothing before the above definition required having a group rather than a monoid (or any type endowed with a multiplication operation really).

The group condition really enters the picture when we will want to partition `X`

into orbits.
The corresponding equivalence relation on `X`

is called `MulAction.orbitRel`

.
It is not declared as a global instance.

```
example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X
```

Using this we can state that `X`

is partitioned into orbits under the action of `G`

.
More precisely, we get a bijection between `X`

and the dependent product
`(ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω))`

where `Quotient.out' ω`

simply chooses an element that projects to `ω`

.
Recall that elements of this dependent product are pairs `⟨ω, x⟩`

where the type
`orbit G (Quotient.out' ω)`

of `x`

depends on `ω`

.

```
example {G X : Type*} [Group G] [MulAction G X] :
X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) :=
MulAction.selfEquivSigmaOrbits G X
```

In particular, when X is finite, this can be combined with `Fintype.card_congr`

and
`Fintype.card_sigma`

to deduce that the cardinality of `X`

is the sum of the cardinalities
of the orbits.
Furthermore, the orbits are in bijection with the quotient of `G`

under the action of the
stabilizers by left translation.
This action of a subgroup by left-translation is used to define quotients of a group by a
subgroup with notation / so we can use the following concise statement.

```
example {G X : Type*} [Group G] [MulAction G X] (x : X) :
orbit G x ≃ G ⧸ stabilizer G x :=
MulAction.orbitEquivQuotientStabilizer G x
```

An important special case of combining the above two results is when `X`

is a group `G`

equipped with the action of a subgroup `H`

by translation.
In this case all stabilizers are trivial so every orbit is in bijection with `H`

and we get:

```
example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H :=
groupEquivQuotientProdSubgroup
```

This is the conceptual variant of the version of Lagrange theorem that we saw above. Note this version makes no finiteness assumption.

As an exercise for this section, let us build the action of a group on its subgroup by
conjugation, using our definition of `conjugate`

from a previous exercise.

```
variable {G : Type*} [Group G]
lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
sorry
instance : MulAction G (Subgroup G) where
smul := conjugate
one_smul := by
sorry
mul_smul := by
sorry
end GroupActions
```

### 8.1.6. Quotient groups

In the above discussion of subgroups acting on groups, we saw the quotient `G ⧸ H`

appear.
In general this is only a type. It can be endowed with a group structure such that the quotient
map is a group morphism if and only if `H`

is a normal subgroup (and this group structure is
then unique).

The normality assumption is a type class `Subgroup.Normal`

so that type class inference can use it
to derive the group structure on the quotient.

```
noncomputable section QuotientGroup
example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance
example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
QuotientGroup.mk' H
```

The universal property of quotient groups is accessed through `QuotientGroup.lift`

:
a group morphism `φ`

descends to `G ⧸ N`

as soon as its kernel contains `N`

.

```
example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
[Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
QuotientGroup.lift N φ h
```

The fact that the target group is called `M`

is the above snippet is a clue that having a
monoid structure on `M`

would be enough.

An important special case is when `N = ker φ`

. In that case the descended morphism is
injective and we get a group isomorphism onto its image. This result is often called
the first isomorphism theorem.

```
example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
G ⧸ MonoidHom.ker φ →* MonoidHom.range φ :=
QuotientGroup.quotientKerEquivRange φ
```

Applying the universal property to a composition of a morphism `φ : G →* G'`

with a quotient group projection `Quotient.mk' N'`

,
we can also aim for a morphism from `G ⧸ N`

to `G' ⧸ N'`

.
The condition required on `φ`

is usually formulated by saying “`φ`

should send `N`

inside
`N'`

.” But this is equivalent to asking that `φ`

should pull `N'`

back inside
`N`

, and the latter condition is nicer to work with since the definition of pullback does not
involve an existential quantifier.

```
example {G G': Type*} [Group G] [Group G']
{N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal]
{φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G' ⧸ N':=
QuotientGroup.map N N' φ h
```

One subtle point to keep in mind is that the type `G ⧸ N`

really depends on `N`

(up to definitional equality), so having a proof that two normal subgroups `N`

and `M`

are equal
is not enough to make the corresponding quotients equal. However the universal properties does give
an isomorphism in this case.

```
example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
[N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h
```

As a final series of exercises for this section, we will prove that if `H`

and `K`

are disjoint
normal subgroups of a finite group `G`

such that the product of their cardinalities is equal to
the cardinality of `G`

then `G`

is isomorphic to `H × K`

. Recall that disjoint in this context means `H ⊓ K = ⊥`

.

We start with playing a bit with Lagrange’s lemma, without assuming the subgroups are normal or disjoint.

```
section
variable {G : Type*} [Group G] {H K : Subgroup G}
open MonoidHom
#check card_pos -- The nonempty argument will be automatically inferred for subgroups
#check Subgroup.index_eq_card
#check Subgroup.index_mul_card
#check Nat.eq_of_mul_eq_mul_right
-- The following line is working around a Lean bug that will be fixed very soon.
attribute [-instance] Subtype.instInhabited
lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G ⧸ H) = card K := by
sorry
```

From now on, we assume that our subgroups are normal and disjoint, and we assume the cardinality condition. Now we construct the first building block of the desired isomorphism.

```
variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K)
#check bijective_iff_injective_and_card
#check ker_eq_bot_iff
#check restrict
#check ker_restrict
def iso₁ [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) : K ≃* G ⧸ H := by
sorry
```

Now we can define our second building block.
We will need `MonoidHom.prod`

, which builds a morphism from `G₀`

to `G₁ × G₂`

out of
morphisms from `G₀`

to `G₁`

and `G₂`

.

```
def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
sorry
```

We are ready to put all pieces together.

```
#check MulEquiv.prodCongr
def finalIso : G ≃* H × K :=
sorry
```

## 8.2. Rings

### 8.2.1. Rings, their units, morphisms and subrings

The type of ring structures on a type `R`

is `Ring R`

. The variant where multiplication is
assumed to be commutative is `CommRing R`

. We have already seen that the `ring`

tactic will
prove any equality that follows from the axioms of a commutative ring.

```
example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
```

More exotic variants do not require that the addition on `R`

forms a group but only an additive
monoid. The corresponding type classes are `Semiring R`

and `CommSemiring R`

.
The type of natural numbers is an important instance of `CommSemiring R`

, as is any type
of functions taking values in the natural numbers.
Another important example is the type of ideals in a ring, which will be discussed below.
The name of the `ring`

tactic is doubly misleading, since it assumes commutativity but works
in semirings as well. In other words, it applies to any `CommSemiring`

.

```
example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
```

There are also versions of the ring and semiring classes that do not assume the existence of a multiplicative unit or the associativity of multiplication. We will not discuss those here.

Some concepts that are traditionally taught in an introduction to ring theory are actually about
the underlying multiplicative monoid.
A prominent example is the definition of the units of a ring. Every (multiplicative) monoid `M`

has a predicate `IsUnit : M → Prop`

asserting existence of a two-sided inverse, a
type `Units M`

of units with notation `Mˣ`

, and a coercion to `M`

.
The type `Units M`

bundles an invertible element with its inverse as well as properties than ensure
that each is indeed the inverse of the other.
This implementation detail is relevant mainly when defining computable functions. In most
situations one can use `IsUnit.unit {x : M} : IsUnit x → Mˣ`

to build a unit.
In the commutative case, one also has `Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ`

which builds `x`

seen as unit.

```
example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x
example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x
example {M : Type*} [Monoid M] : Group Mˣ := inferInstance
```

The type of ring morphisms between two (semi)-rings `R`

and `S`

is `RingHom R S`

,
with notation `R →+* S`

.

```
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) :
f (x + y) = f x + f y := f.map_add x y
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ :=
Units.map f
```

The isomorphism variant is `RingEquiv`

, with notation `≃+*`

.

As with submonoids and subgroups, there is a `Subring R`

type for subrings of a ring `R`

,
but this type is a lot less useful than the type of subgroups since one cannot quotient a ring by
a subring.

```
example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance
```

Also notice that `RingHom.range`

produces a subring.

### 8.2.2. Ideals and quotients

For historical reasons, Mathlib only has a theory of ideals for commutative rings.
(The ring library was originally developed to make quick progress toward the foundations of modern
algebraic geometry.) So in this section we will work with commutative (semi)rings.
Ideals of `R`

are defined as submodules of `R`

seen as `R`

-modules. Modules will
be covered later in a chapter on linear algebra, but this implementation detail can mostly be
safely ignored since most (but not all) relevant lemmas are restated in the special context of
ideals. But anonymous projection notation won’t always work as expected. For instance,
one cannot replace `Ideal.Quotient.mk I`

by `I.Quotient.mk`

in the snippet below because there
are two `.``s and so it will parse as ``(Ideal.Quotient I).mk`

; but `Ideal.Quotient`

by itself
doesn’t exist.

```
example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
Ideal.Quotient.mk I
example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
Ideal.Quotient.eq_zero_iff_mem
```

The universal property of quotient rings is `Ideal.Quotient.lift`

.

```
example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
(H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
Ideal.Quotient.lift I f H
```

In particular it leads to the first isomorphism theorem for rings.

```
example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) :
R ⧸ RingHom.ker f ≃+* f.range :=
RingHom.quotientKerEquivRange f
```

Ideals form a complete lattice structure with the inclusion relation, as well as a semiring structure. These two structures interact nicely.

```
variable {R : Type*} [CommRing R] {I J : Ideal R}
example : I + J = I ⊔ J := rfl
example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
simp [Submodule.mem_sup]
example : I * J ≤ J := Ideal.mul_le_left
example : I * J ≤ I := Ideal.mul_le_right
example : I * J ≤ I ⊓ J := Ideal.mul_le_inf
```

One can use ring morphisms to push ideals forward and pull them back using `Ideal.map`

and
`Ideal.comap`

, respectively. As usual,
the latter is more convenient to use since it does not involve an existential quantifier.
This explains why it is used to state the condition that allows us to build morphisms between
quotient rings.

```
example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
(H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
Ideal.quotientMap J f H
```

One subtle point is that the type `R ⧸ I`

really depends on `I`

(up to definitional equality), so having a proof that two ideals `I`

and `J`

are equal is not
enough to make the corresponding quotients equal. However, the universal properties do provide
an isomorphism in this case.

```
example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
Ideal.quotEquivOfEq h
```

We can now present the Chinese remainder isomorphism as an example. Pay attention to the difference
between the indexed infimum symbol `⨅`

and the big product of types symbol `Π`

. Depending on
your font, those can be pretty hard to distinguish.

```
example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R)
(hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
Ideal.quotientInfRingEquivPiQuotient f hf
```

The elementary version of the Chinese remainder theorem, a statement about `ZMod`

, can be easily
deduced from the previous one:

```
open BigOperators PiNotation
example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
ZMod.prodEquivPi a coprime
```

As a series of exercises, we will reprove the Chinese remainder theorem in the general case.

We first need to define the map appearing in the theorem, as a ring morphism, using the universal property of quotient rings.

```
variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function
#check Pi.ringHom
#check ker_Pi_Quotient_mk
/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
Remainder Theorem. -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
sorry
```

Make sure the following next two lemmas can be proven by `rfl`

.

```
lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
sorry
lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
chineseMap I (mk _ x) i = mk (I i) x :=
sorry
```

The next lemma proves the easy half of the Chinese remainder theorem, without any assumption on the family of ideals. The proof is less than one line long.

```
#check injective_lift_iff
lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
sorry
```

We are now ready for the heart of the theorem, which will show the surjectivity
of our `chineseMap`

. First we need to know the different ways one can express the coprimality
(also called co-maximality assumption). Only the first two will be needed below.

```
#check IsCoprime
#check isCoprime_iff_add
#check isCoprime_iff_exists
#check isCoprime_iff_sup_eq
#check isCoprime_iff_codisjoint
```

We take the opportunity to use induction on `Finset`

. Relevant lemmas on `Finset`

are given
below.
Remember that the `ring`

tactic works for semirings and that the ideals of a ring form a semiring.

```
#check Finset.mem_insert_of_mem
#check Finset.mem_insert_self
theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
(hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty =>
simp
| @insert i s _ hs =>
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
set K := ⨅ j ∈ s, J j
calc
1 = I + K := sorry
_ = I + K * (I + J i) := sorry
_ = (1 + K) * I + K * J i := sorry
_ ≤ I + K ⊓ J i := sorry
```

We can now prove surjectivity of the map appearing in the Chinese remainder theorem.

```
lemma chineseMap_surj [Fintype ι] {I : ι → Ideal R}
(hI : ∀ i j, i ≠ j → IsCoprime (I i) (I j)) : Surjective (chineseMap I) := by
classical
intro g
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
intro i
have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
sorry
sorry
choose e he using key
use mk _ (∑ i, f i * e i)
sorry
```

Now all the pieces come together in the following:

```
noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
(hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
{ Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
chineseMap f with }
```

### 8.2.3. Algebras and polynomials

Given a commutative (semi)ring `R`

, an *algebra over* `R`

is a semiring `A`

equipped
with a ring morphism whose image commutes with every element of `A`

. This is encoded as
a type class `Algebra R A`

.
The morphism from `R`

to `A`

is called the structure map and is denoted
`algebraMap R A : R →+* A`

in Lean.
Multiplication of `a : A`

by `algebraMap R A r`

for some `r : R`

is called the scalar
multiplication of `a`

by `r`

and denoted by `r • a`

.
Note that this notion of algebra is sometimes called an *associative unital algebra* to emphasize the
existence of more general notions of algebra.

The fact that `algebraMap R A`

is ring morphism packages together a lot of properties of scalar
multiplication, such as the following:

```
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
(r + r') • a = r • a + r' • a :=
add_smul r r' a
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
(r * r') • a = r • r' • a :=
mul_smul r r' a
```

The morphisms between two `R`

-algebras `A`

and `B`

are ring morphisms
which commute with scalar multiplication by elements of `R`

. They are bundled morphisms
with type `AlgHom R A B`

, which is denoted by `A →ₐ[R] B`

.

Important examples of non-commutative algebras include algebras of endomorphisms and algebras of square matrices, both of which will be covered in the chapter on linear algebra. In this chapter we will discuss one of the most important examples of a commutative algebra, namely, polynomial algebras.

The algebra of univariate polynomials with coefficients in `R`

is called `Polynomial R`

,
which can be written as `R[X]`

as soon as one opens the `Polynomial`

namespace.
The algebra structure map from `R`

to `R[X]`

is denoted by `C`

,
which stands for “constant” since the corresponding
polynomial functions are always constant. The indeterminate is denoted by `X`

.

```
open Polynomial
example {R : Type*} [CommRing R] : R[X] := X
example {R : Type*} [CommRing R] (r : R) := X - C r
```

In the first example above, it is crucial that we give Lean the expected type since it cannot be
determined from the body of the definition. In the second example, the target polynomial
algebra can be inferred from our use of `C r`

since the type of `r`

is known.

Because `C`

is a ring morphism from `R`

to `R[X]`

, we can use all ring morphisms lemmas
such as `map_zero`

, `map_one`

, `map_mul`

, and `map_pow`

before computing in the ring
`R[X]`

. For example:

```
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
rw [C.map_pow]
ring
```

You can access coefficients using `Polynomial.coeff`

```
example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp
example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp
```

Defining the degree of a polynomial is always tricky because of the special case of the zero
polynomial. Mathlib has two variants: `Polynomial.natDegree : R[X] → ℕ`

assigns degree
`0`

to the zero polynomial, and `Polynomial.degree : R[X] → WithBot ℕ`

assigns `⊥`

.
In the latter, `WithBot ℕ`

can be seen as `ℕ ∪ {-∞}`

, except that `-∞`

is denoted `⊥`

,
the same symbol as the bottom element in a complete lattice. This special value is used as the
degree of the zero polynomial, and it is absorbent for addition. (It is almost absorbent for
multiplication, except that `⊥ * 0 = 0`

.)

Morally speaking, the `degree`

version is the correct one. For instance, it allows us to state
the expected formula for the degree of a product (assuming the base ring has no zero divisor).

```
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
degree (p * q) = degree p + degree q :=
Polynomial.degree_mul
```

Whereas the version for `natDegree`

needs to assume non-zero polynomials.

```
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) :
natDegree (p * q) = natDegree p + natDegree q :=
Polynomial.natDegree_mul hp hq
```

However, `ℕ`

is much nicer to use than `WithBot ℕ`

, so Mathlib makes both versions available
and provides lemmas to convert between them. Also, `natDegree`

is the more convenient definition
to use when computing the degree of a composition. Composition of polynomial is `Polynomial.comp`

and we have:

```
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
natDegree (comp p q) = natDegree p * natDegree q :=
Polynomial.natDegree_comp
```

Polynomials give rise to polynomial functions: any polynomial can be evaluated on `R`

using `Polynomial.eval`

.

```
example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x
example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp
```

In particular, there is a predicate, `IsRoot`

, that holds for elements `r`

in `R`

where a
polynomial vanishes.

```
example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl
```

We would like to say that, assuming `R`

has no zero divisor, a polynomial has at most as many
roots as its degree, where the roots are counted with multiplicities.
But once again the case of the zero polynomial is painful.
So Mathlib defines `Polynomial.roots`

to send a polynomial `P`

to a multiset,
i.e. the finite set that is defined to be empty if `P`

is zero and the roots of `P`

,
with multiplicities, otherwise. This is defined only when the underlying ring is a domain
since otherwise the definition does not have good properties.

```
example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
roots_X_sub_C r
example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
((X - C r) ^ n).roots = n • {r} :=
by simp
```

Both `Polynomial.eval`

and `Polynomial.roots`

consider only the coefficients ring. They do not
allow us to say that `X ^ 2 - 2 : ℚ[X]`

has a root in `ℝ`

or that `X ^ 2 + 1 : ℝ[X]`

has a root in
`ℂ`

. For this, we need `Polynomial.aeval`

, which will evaluate `P : R[X]`

in any `R`

-algebra.
More precisely, given a semiring `A`

and an instance of `Algebra R A`

, `Polynomial.aeval`

sends
every element of `a`

along the `R`

-algebra morphism of evaluation at `a`

. Since `AlgHom`

has a coercion to functions, one can apply it to a polynomial.
But `aeval`

does not have a polynomial as an argument, so one cannot use dot notation like in
`P.eval`

above.

```
example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp
```

The function corresponding to `roots`

in this context is `aroots`

which takes a polynomial
and then an algebra and outputs a multiset (with the same caveat about the zero polynomial as
for `roots`

).

```
open Complex Polynomial
example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
rw [C_neg]
linear_combination show (C I * C I : ℂ[X]) = -1 by simp [← C_mul]
have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
intro H
apply_fun eval 0 at H
simp [eval] at H
simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
rfl
-- Mathlib knows about D'Alembert-Gauss theorem: ``ℂ`` is algebraically closed.
example : IsAlgClosed ℂ := inferInstance
```

More generally, given an ring morphism `f : R →+* S`

one can evaluate `P : R[X]`

at a point
in `S`

using `Polynomial.eval₂`

. This one produces an actual function from `R[X]`

to `S`

since it does not assume the existence of a `Algebra R S`

instance, so dot notation works as
you would expect.

```
#check (Complex.ofReal : ℝ →+* ℂ)
example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp
```

Let us end by mentioning multivariate polynomials briefly. Given a commutative semiring `R`

,
the `R`

-algebra of polynomials with coefficients in `R`

and indeterminates indexed by
a type `σ`

is `MVPolynomial σ R`

. Given `i : σ`

, the corresponding polynomial is
`MvPolynomial.X i`

. (As usual, one can open the `MVPolynomial`

namespace to shorten this
to `X i`

.)
For instance, if we want two indeterminates we can use
`Fin 2`

as `σ`

and write the polynomial defining the unit circle in \(\mathbb{R}^2\) as:

```
open MvPolynomial
def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1
```

Recall that function application has a very high precedence so the expression above is read as
`(X 0) ^ 2 + (X 1) ^ 2 - 1`

.
We can evaluate it to make sure the point with coordinates \((1, 0)\) is on the circle.
Recall the `![...]`

notation denotes elements of `Fin n → X`

for some natural number `n`

determined by the number of arguments and some type `X`

determined by the type of arguments.

```
example : MvPolynomial.eval ![0, 1] circleEquation = 0 := by simp [circleEquation]
```