Contents Previous Next

# Field Morphisms

```
module Algebra.fieldMorphisms where
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.relations
open import Types.equality
open import Types.functions2
open import Algebra.groups
open import Algebra.groups2
open import Algebra.groupMorphisms
open import Algebra.ringMorphisms
open import Algebra.fields
open import Algebra.fields2
```

We keep following the same pattern as we have been doing for groups and rings. A morphisms between two fields is a structure-preserving map in a way that preserves the field properties.

## Field Homomorphism

A field homomorphism between two fields 𝔸 and 𝔹 is a function

`f : 𝔸 → 𝔹`

such that ∀ x, y in 𝔸,

`f`

is congruent over `+`

, or \[f(x + y) = f(x) + f(y)\]
`f`

is congruent over `⋅`

, or \[f( x ⋅ y) = f(x) ⋅ f(y)\]
- Identities are preserved, i.e. \[f(1) = 1\]

The fields are isomorphic if `f`

is bijective.

Numbers