```
module Algebra.morphisms where
open import Agda.Primitive using (Level; _β_; lsuc; lzero)
open import Types.relations
open import Types.equality
open import Algebra.groups
open import Algebra.groups2
```

A morphism is a more general concept that applies not only to groups but also to pretty much all algebraic objects. It can be defined as a structure-preserving map. In the context of group-like objects, a morphism between any two objects `X`

and `Y`

embeds `X`

in `Y`

while ensuring the structure of `X`

is preserved.

Let us first define a morphism:

```
module Homomorphism {f t β} (From : Set f) (To : Set t) (_==_ : Rel To β) where
: Set _
Morphism = From β To Morphism
```

In the family of groups, these are the main kinds of morphisms:

- Homomorphism
- Endomorphism
- Isomorphism
- Automorphism

A map (function) `π½`

is a homomorphism if given input `x β (X, β’)`

, where X is a group-like structure, its output `y β (Y, β)`

where Y is also a group-like structure, such that `π½`

preserves the group-like structure of `X`

in `Y`

, i.e.Β it ensures that all relations what were valid in `X`

remain valid in `Y`

. More formally,

Given two groups, `(X, β’)`

and `(Y, β)`

, `π½ : X β Y`

is a homomorphism if:

\[ β xβ, xβ β X, π½β¦ xβ β’ xβ β§ = π½β¦ xβ β§ β π½β¦ xβ β§ \]

The basic rules for any morphism to be a homomorphism are if it:

- Preserves identity

An identity homomorphism when applied to a structure produces the same structure.

```
: Morphism β From β To β Set _
identity-preservation _β§ from to = πβ¦ from β§ == to identity-preservation πβ¦
```

- Composes with operations

If `π½`

is a homomorphism from `X β Y`

, and `β
`

and `β`

are both unary or both binary operations operating on `X`

and `Y`

respectively, then `π½`

composes with the two operations in the following ways:

```
: Morphism β β From β β To β Set _
compose-unary _β§ β_ β_ = β x β πβ¦ β x β§ == ( β πβ¦ x β§ )
compose-unary πβ¦
: Morphism β β
From β β
To β Set _
compose-binary _β§ _β_ _β_ = β x y β πβ¦ x β y β§ == ( πβ¦ x β§ β πβ¦ y β§ ) compose-binary πβ¦
```

Now, we define homomorphisms for various group-like structures we have discussed earlier.

```
module _ {f t ββ ββ} (From : Magma f ββ) (To : Magma t ββ) where
private
module F = Magma From
module T = Magma To
open Homomorphism F.Data T.Data T._==_
record IsMagmaHomomorphism (πβ¦_β§ : Morphism) : Set (f β t β ββ β ββ) where
field
: πβ¦_β§ Preserves F._==_ βΆ T._==_
preserves-congruence : compose-binary πβ¦_β§ F._β_ T._β_ preserves-composition
```

```
module _ {f t ββ ββ} (From : Semigroup f ββ) (To : Semigroup t ββ) where
private
module F = Semigroup From
module T = Semigroup To
open Homomorphism F.Data T.Data T._==_
record IsSemigroupHomomorphism (πβ¦_β§ : Morphism ) : Set (f β t β ββ β ββ) where
field
: IsMagmaHomomorphism F.magma T.magma πβ¦_β§
is-magma-homomorphism
open IsMagmaHomomorphism is-magma-homomorphism public
```

```
module _ {f t ββ ββ} (From : Monoid f ββ) (To : Monoid t ββ) where
private
module F = Monoid From
module T = Monoid To
open Homomorphism F.Data T.Data T._==_
record IsMonoidHomomorphism (πβ¦_β§ : Morphism ) : Set (f β t β ββ β ββ) where
field
: IsSemigroupHomomorphism F.semigroup T.semigroup πβ¦_β§
is-semigroup-homomorphism : identity-preservation πβ¦_β§ F.Ξ΅ T.Ξ΅
preserves-identity
open IsSemigroupHomomorphism is-semigroup-homomorphism public
```

```
module _ {f t ββ ββ} (From : Group f ββ) (To : Group t ββ) where
private
module F = Group From
module T = Group To
open Homomorphism F.Data T.Data T._==_
record IsGroupHomomorphism (πβ¦_β§ : Morphism ) : Set (f β t β ββ β ββ) where
field
: IsMonoidHomomorphism F.monoid T.monoid πβ¦_β§
is-monoid-homomorphism : compose-unary πβ¦_β§ F._β»ΒΉ T._β»ΒΉ
preserves-inverse
open IsMonoidHomomorphism is-monoid-homomorphism public
```

An Endomorphism is a homomorphism where `From`

and `To`

are the same objects.

```
module _ {f β} (Self : Monoid f β) where
private
module S = Monoid Self
open Homomorphism S.Data S.Data S._==_
record IsMonoidAutomorphism (πβ¦_β§ : Morphism) : Set (f β β) where
field
: IsMonoidHomomorphism Self Self πβ¦_β§ is-homomorphism
```

```
module _ {f β} (Self : Group f β) where
private
module S = Group Self
open Homomorphism S.Data S.Data S._==_
record IsGroupAutomorphism (πβ¦_β§ : Morphism) : Set (f β β) where
field
: IsGroupHomomorphism Self Self πβ¦_β§ is-homomorphism
```

An group isomorphism is a homomorphism with an additional property - bijection (one-to-one + onto). Bijection implies an isomorphism is a homomorphism such that the inverse of the homomorphism is also a homomorphism. Practically, an isomorphism is an equivalence relation. Often in mathematics one encounters the phrase βequal upto isomorphismβ meaning isomorphism serves as equality for all practical purposes.

An automorphism is a endomorphism which is also an isomorphism.