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
.
Stacks Tag 09FZ (first part)
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
The top IntermediateField
is isomorphic to the field.
This is the intermediate field version of Subalgebra.topEquiv
.
Equations
- IntermediateField.topEquiv = 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.
If E1
and E2
are intermediate fields, and at least one them are algebraic, then the rank of
the compositum of E1
and E2
is less than or equal to the product of that of E1
and E2
.
Note that this result is also true without algebraic assumption,
but the proof becomes very complicated.
If E1
and E2
are intermediate fields, then the Module.finrank
of
the compositum of E1
and E2
is less than or equal to the product of that of E1
and E2
.
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⟮α⟯
Stacks Tag 09G1 (Algebraic case)
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 x
is an algebraic element of field K
, then its minimal polynomial has degree
[K(x) : K]
.
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.
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
.
Stacks Tag 09FZ (second part)
Equations
- S.FG = ∃ (t : Finset E), IntermediateField.adjoin F ↑t = S
Instances For
Alias of IntermediateField.fg_of_fg_toSubalgebra
.
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 ⋯
Instances For
If F
is a field, A
is an F
-algebra with fraction field K
, L
is a field,
g : A →ₐ[F] L
lifts to f : K →ₐ[F] L
,
then the image of f
is the field generated by the image of g
.
Note: this does not require IsScalarTower F A K
.
If F
is a field, A
is an F
-algebra with fraction field K
, L
is a field,
g : A →ₐ[F] L
lifts to f : K →ₐ[F] L
,
s
is a set such that the image of g
is the subalgebra generated by s
,
then the image of f
is the intermediate field generated by s
.
Note: this does not require IsScalarTower F A K
.
The image of IsFractionRing.liftAlgHom
is the intermediate field generated by the image
of the algebra hom.
The image of IsFractionRing.liftAlgHom
is the intermediate field generated by s
,
if the image of the algebra hom is the subalgebra generated by s
.