Adjoining Elements to Fields #
In this file we introduce the notion of adjoining elements to fields.
This isn't quite the same as adjoining elements to rings.
For example, Algebra.adjoin K {x}
might not include x⁻¹
.
Main results #
adjoin_adjoin_left
: adjoining S and then T is the same as adjoiningS ∪ T
.bot_eq_top_of_rank_adjoin_eq_one
: ifF⟮x⟯
has dimension1
overF
for everyx
inE
thenF = E
Notation #
F⟮α⟯
: adjoin a single elementα
toF
(in scopeIntermediateField
).
adjoin F S
extends a field F
by adjoining a set S ⊆ E
.
Equations
- IntermediateField.adjoin F S = { toSubsemiring := (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)).toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }
Instances For
Galois insertion between adjoin
and coe
.
Equations
- IntermediateField.gi = { choice := fun (s : Set E) (hs : ↑(IntermediateField.adjoin F s) ≤ s) => (IntermediateField.adjoin F s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Equations
- IntermediateField.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- IntermediateField.instUnique = { toInhabited := inferInstanceAs (Inhabited (IntermediateField F F)), uniq := ⋯ }
Construct an algebra isomorphism from an equality of intermediate fields
Equations
- IntermediateField.equivOfEq h = S.equivOfEq T.toSubalgebra ⋯
Instances For
The bottom intermediate_field is isomorphic to the field.
Equations
- IntermediateField.botEquiv F E = (⊥.equivOfEq ⊥ ⋯).trans (Algebra.botEquiv F E)
Instances For
Equations
- ⋯ = ⋯
The top IntermediateField
is isomorphic to the field.
This is the intermediate field version of Subalgebra.topEquiv
.
Instances For
An intermediate field is isomorphic to its image under an AlgHom
(which is automatically injective)
Equations
- L.equivMap f = (AlgEquiv.ofInjective (f.comp L.val) ⋯).trans (IntermediateField.equivOfEq ⋯)
Instances For
Equations
- IntermediateField.adjoin.fieldCoe F S = { coe := fun (x : F) => ⟨(algebraMap F E) x, ⋯⟩ }
Equations
- IntermediateField.adjoin.setCoe F S = { coe := fun (x : ↑S) => ⟨↑x, ⋯⟩ }
If K
is a field with F ⊆ K
and S ⊆ K
then adjoin F S ≤ K
.
F[S][T] = F[S ∪ T]
If E / L / F
and E / L' / F
are two field extension towers, L ≃ₐ[F] L'
is an isomorphism
compatible with E / L
and E / L'
, then for any subset S
of E
, L(S)
and L'(S)
are
equal as intermediate fields of E / F
.
If x₁ x₂ ... xₙ : E
then F⟮x₁,x₂,...,xₙ⟯
is the IntermediateField F E
generated by these elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
generator of F⟮α⟯
Equations
- IntermediateField.AdjoinSimple.gen F α = ⟨α, ⋯⟩
Instances For
Characterize IsSplittingField
with IntermediateField.adjoin
instead of Algebra.adjoin
.
The compositum of two intermediate fields is equal to the compositum of them as subalgebras, if one of them is algebraic over the base field.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A compositum of splitting fields is a splitting field
If K / E / F
is a field extension tower, L
is an intermediate field of K / F
, such that
either E / F
or L / F
is algebraic, then E(L) = E[L]
.
If K / E / F
is a field extension tower, L
is an intermediate field of K / F
, such that
either E / F
or L / F
is algebraic, then [E(L) : E] ≤ [L : F]
. A corollary of
Subalgebra.adjoin_rank_le
since in this case E(L) = E[L]
.
If F⟮x⟯
has dimension ≤1
over F
for every x ∈ E
then F = E
.
algebra isomorphism between AdjoinRoot
and F⟮α⟯
Equations
Instances For
The elements 1, x, ..., x ^ (d - 1)
form a basis for K⟮x⟯
,
where d
is the degree of the minimal polynomial of x
.
Equations
- IntermediateField.powerBasisAux hx = (AdjoinRoot.powerBasis ⋯).basis.map (IntermediateField.adjoinRootEquivAdjoin K hx).toLinearEquiv
Instances For
The power basis 1, x, ..., x ^ (d - 1)
for K⟮x⟯
,
where d
is the degree of the minimal polynomial of x
.
Equations
- IntermediateField.adjoin.powerBasis hx = { gen := IntermediateField.AdjoinSimple.gen K x, dim := (minpoly K x).natDegree, basis := IntermediateField.powerBasisAux hx, basis_eq_pow := ⋯ }
Instances For
If K / E / F
is a field extension tower, S ⊂ K
is such that F(S) = K
,
then E(S) = K
.
If E / F
is a finite extension such that E = F(α)
, then for any intermediate field K
, the
F
adjoin the coefficients of minpoly K α
is equal to K
itself.
Equations
- ⋯ = ⋯
If E / F
is an infinite algebraic extension, then there exists an intermediate field
L / F
with arbitrarily large finite extension degree.
If x : L
is an integral element in a field extension L
over K
, then the degree of the
minimal polynomial of x
over K
divides [L : K]
.
A compositum of algebraic extensions is algebraic
If L / K
is a field extension, S
is a finite subset of L
, such that every element of S
is integral (= algebraic) over K
, then K(S) / K
is a finite extension.
A direct corollary of finiteDimensional_iSup_of_finite
.
Algebra homomorphism F⟮α⟯ →ₐ[F] K
are in bijection with the set of roots
of minpoly α
in K
.
Equations
- IntermediateField.algHomAdjoinIntegralEquiv F h = (IntermediateField.adjoin.powerBasis h).liftEquiv'.trans ((Equiv.refl K).subtypeEquiv ⋯)
Instances For
Fintype of algebra homomorphism F⟮α⟯ →ₐ[F] K
Equations
Instances For
Let f, g
be monic polynomials over K
. If f
is irreducible, and g(x) - α
is irreducible
in K⟮α⟯
with α
a root of f
, then f(g(x))
is irreducible.
An intermediate field S
is finitely generated if there exists t : Finset E
such that
IntermediateField.adjoin F t = S
.
Equations
- S.FG = ∃ (t : Finset E), IntermediateField.adjoin F ↑t = S
Instances For
The canonical algebraic homomorphism from AdjoinRoot p
to AdjoinRoot q
, where
the polynomial q : K[X]
divides p
.
Equations
- AdjoinRoot.algHomOfDvd hpq = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯
Instances For
algHomOfDvd
sends AdjoinRoot.root p
to AdjoinRoot.root q
.
The canonical algebraic equivalence between AdjoinRoot p
and AdjoinRoot q
, where
the two polynomials p q : K[X]
are equal.
Equations
- AdjoinRoot.algEquivOfEq hp h_eq = AlgEquiv.ofAlgHom (AdjoinRoot.algHomOfDvd ⋯) (AdjoinRoot.algHomOfDvd ⋯) ⋯ ⋯
Instances For
algEquivOfEq
sends AdjoinRoot.root p
to AdjoinRoot.root q
.
The canonical algebraic equivalence between AdjoinRoot p
and AdjoinRoot q
,
where the two polynomials p q : K[X]
are associated.
Equations
- AdjoinRoot.algEquivOfAssociated hp hpq = AlgEquiv.ofAlgHom (AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯) (AdjoinRoot.liftHom q (AdjoinRoot.root p) ⋯) ⋯ ⋯
Instances For
algEquivOfAssociated
sends AdjoinRoot.root p
to AdjoinRoot.root q
.
The canonical algEquiv
between K⟮x⟯
and K⟮y⟯
, sending x
to y
, where x
and y
have
the same minimal polynomial over K
.
Equations
- minpoly.algEquiv hx h_mp = (IntermediateField.adjoinRootEquivAdjoin K ⋯).symm.trans ((AdjoinRoot.algEquivOfEq ⋯ h_mp).trans (IntermediateField.adjoinRootEquivAdjoin K ⋯))
Instances For
minpoly.algEquiv
sends the generator of K⟮x⟯
to the generator of K⟮y⟯
.
pb.equivAdjoinSimple
is the equivalence between K⟮pb.gen⟯
and L
itself.
Equations
- pb.equivAdjoinSimple = (IntermediateField.adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯