# Morphisms

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
Morphism : Set _
Morphism = From β To

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

1. Homomorphism
2. Endomorphism
3. Isomorphism
4. Automorphism

## Homomorphisms

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:

1. Preserves identity

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

  identity-preservation : Morphism β From β To β Set _
identity-preservation πβ¦_β§ from to = πβ¦ from β§ == to
1. 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:

  compose-unary : Morphism β β  From β β  To β Set _
compose-unary πβ¦_β§ β_ β_ = β x β πβ¦ β x β§ == ( β πβ¦ x β§ )

compose-binary : Morphism β β From β β To β Set _
compose-binary πβ¦_β§ _β_ _β_ = β x y β πβ¦ x β y β§ == ( πβ¦ x β§ β πβ¦ y β§ )

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

### Magma homomorphism

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-congruence    : πβ¦_β§ Preserves F._==_ βΆ T._==_
preserves-composition   : compose-binary πβ¦_β§ F._β_ T._β_

### Semigroup homomorphism

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
is-magma-homomorphism  : IsMagmaHomomorphism F.magma T.magma πβ¦_β§

open IsMagmaHomomorphism is-magma-homomorphism public

### Monoid Homomorphism

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
is-semigroup-homomorphism  : IsSemigroupHomomorphism F.semigroup T.semigroup πβ¦_β§
preserves-identity         : identity-preservation πβ¦_β§ F.Ξ΅ T.Ξ΅

open IsSemigroupHomomorphism is-semigroup-homomorphism public

### Group Homomorphism

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
is-monoid-homomorphism  : IsMonoidHomomorphism F.monoid T.monoid πβ¦_β§
preserves-inverse       : compose-unary πβ¦_β§ F._β»ΒΉ T._β»ΒΉ

open IsMonoidHomomorphism is-monoid-homomorphism public

## Endomorphism

An Endomorphism is a homomorphism where From and To are the same objects.

### Monoid endomorphism

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
is-homomorphism : IsMonoidHomomorphism Self Self πβ¦_β§

### Group endomorphism

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
is-homomorphism : IsGroupHomomorphism Self Self πβ¦_β§

## Isomorphism

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.

## Automorphism

An automorphism is a endomorphism which is also an isomorphism.

Rings and family