# Relative Algebraic Closure #

In this file we construct the relative algebraic closure of a field extension.

## Main Definitions #

`algebraicClosure F E`

is the relative algebraic closure (i.e. the maximal algebraic subextension) of the field extension`E / F`

, which is defined to be the integral closure of`F`

in`E`

.

The *relative algebraic closure* of a field `F`

in a field extension `E`

,
also called the *maximal algebraic subextension* of `E / F`

,
is defined to be the subalgebra `integralClosure F E`

upgraded to an intermediate field (since `F`

and `E`

are both fields).
This is exactly the intermediate field of `E / F`

consisting of all integral/algebraic elements.

## Equations

## Instances For

An element is contained in the algebraic closure of `F`

in `E`

if and only if
it is an integral element.

An element is contained in the algebraic closure of `F`

in `E`

if and only if
it is an algebraic element.

If `i`

is an `F`

-algebra homomorphism from `E`

to `K`

, then `i x`

is contained in
`algebraicClosure F K`

if and only if `x`

is contained in `algebraicClosure F E`

.

If `i`

is an `F`

-algebra homomorphism from `E`

to `K`

, then the preimage of
`algebraicClosure F K`

under the map `i`

is equal to `algebraicClosure F E`

.

If `i`

is an `F`

-algebra homomorphism from `E`

to `K`

, then the image of `algebraicClosure F E`

under the map `i`

is contained in `algebraicClosure F K`

.

If `K / E / F`

is a field extension tower, such that `K / E`

has no non-trivial algebraic
subextensions (this means that it is purely transcendental),
then the image of `algebraicClosure F E`

in `K`

is equal to `algebraicClosure F K`

.

If `i`

is an `F`

-algebra isomorphism of `E`

and `K`

, then the image of `algebraicClosure F E`

under the map `i`

is equal to `algebraicClosure F K`

.

If `E`

and `K`

are isomorphic as `F`

-algebras, then `algebraicClosure F E`

and
`algebraicClosure F K`

are also isomorphic as `F`

-algebras.

## Equations

## Instances For

**Alias** of `algebraicClosure.algEquivOfAlgEquiv`

.

If `E`

and `K`

are isomorphic as `F`

-algebras, then `algebraicClosure F E`

and
`algebraicClosure F K`

are also isomorphic as `F`

-algebras.

## Instances For

The algebraic closure of `F`

in `E`

is algebraic over `F`

.

## Equations

- ⋯ = ⋯

The algebraic closure of `F`

in `E`

is the integral closure of `F`

in `E`

.

## Equations

- ⋯ = ⋯

An intermediate field of `E / F`

is contained in the algebraic closure of `F`

in `E`

if all of its elements are algebraic over `F`

.

An intermediate field of `E / F`

is contained in the algebraic closure of `F`

in `E`

if it is algebraic over `F`

.

An intermediate field of `E / F`

is contained in the algebraic closure of `F`

in `E`

if and only if it is algebraic over `F`

.

The algebraic closure in `E`

of the algebraic closure of `F`

in `E`

is equal to itself.

The normal closure in `E/F`

of the algebraic closure of `F`

in `E`

is equal to itself.

If `E / F`

is a field extension and `E`

is algebraically closed, then the algebraic closure
of `F`

in `E`

is equal to `F`

if and only if `F`

is algebraically closed.

`F(S) / F`

is a algebraic extension if and only if all elements of `S`

are
algebraic elements.

If `E`

is algebraically closed, then the algebraic closure of `F`

in `E`

is an absolute
algebraic closure of `F`

.

## Equations

- ⋯ = ⋯

The algebraic closure of `F`

in `E`

is equal to `E`

if and only if `E / F`

is
algebraic.

If `K / E / F`

is a field extension tower, then `algebraicClosure F K`

is contained in
`algebraicClosure E K`

.

If `K / E / F`

is a field extension tower, such that `E / F`

is algebraic, then
`algebraicClosure F K`

is equal to `algebraicClosure E K`

.

If `K / E / F`

is a field extension tower, then `E`

adjoin `algebraicClosure F K`

is contained
in `algebraicClosure E K`

.

Let `E / F`

be a field extension. If a polynomial `p`

splits in `E`

, then it splits in the relative algebraic closure of `F`

in `E`

already.