# Adjoining Elements to Fields #

This file contains many results about adjoining elements to fields.

source
theorem IntermediateField.restrictScalars_le_iff (K : Type u_1) {L : Type u_2} {E : Type u_3} [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] {E₁ E₂ : IntermediateField L E} :
restrictScalars K E₁ ≤ restrictScalars K E₂ ↔ E₁ ≤ E₂
source
theorem IntermediateField.FG.of_restrictScalars {K : Type u_1} {L : Type u_2} {E : Type u_3} [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] {E' : IntermediateField L E} (H : (restrictScalars K E').FG) :
E'.FG
source
theorem IntermediateField.mem_adjoin_range_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} (i : ι → E) (x : E) :
x ∈ adjoin F (Set.range i) ↔ ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F), x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s
source
theorem IntermediateField.mem_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (x : E) :
x ∈ adjoin F S ↔ ∃ (r : MvPolynomial (↑S) F) (s : MvPolynomial (↑S) F), x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
source
theorem IntermediateField.mem_adjoin_simple_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (x : E) :
x ∈ F⟮α⟯ ↔ ∃ (r : Polynomial F) (s : Polynomial F), x = (Polynomial.aeval α) r / (Polynomial.aeval α) s
source
instance IntermediateField.finiteDimensional_sup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2] :
FiniteDimensional K ↥(E1 ⊔ E2)
source
theorem IntermediateField.rank_sup_le_of_isAlgebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) (halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2) :
Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

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.

source
theorem IntermediateField.finrank_sup_le {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) :
Module.finrank K ↥(E1 ⊔ E2) ≤ Module.finrank K ↥E1 * Module.finrank K ↥E2

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`.

source
theorem IntermediateField.coe_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} [Nonempty ι] (dir : Directed (fun (x1 x2 : IntermediateField K L) => x1 ≤ x2) t) :
↑(iSup t) = ⋃ (i : ι), ↑(t i)
source
theorem IntermediateField.toSubalgebra_iSup_of_directed {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} (dir : Directed (fun (x1 x2 : IntermediateField K L) => x1 ≤ x2) t) :
(iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
source
instance IntermediateField.finiteDimensional_iSup_of_finite {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} [h : Finite ι] [∀ (i : ι), FiniteDimensional K ↥(t i)] :
FiniteDimensional K ↥(⨆ (i : ι), t i)
source
instance IntermediateField.finiteDimensional_iSup_of_finset {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {s : Finset ι} [∀ (i : ι), FiniteDimensional K ↥(t i)] :
FiniteDimensional K ↥(⨆ i ∈ s, t i)

See `finiteDimensional_iSup_of_finset'` for a stronger version, that was the one used in mathlib3.

source
theorem IntermediateField.finiteDimensional_iSup_of_finset' {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {s : Finset ι} (h : ∀ i ∈ s, FiniteDimensional K ↥(t i)) :
FiniteDimensional K ↥(⨆ i ∈ s, t i)
source
theorem IntermediateField.isSplittingField_iSup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type u_5} {t : ι → IntermediateField K L} {p : ι → Polynomial K} {s : Finset ι} (h0 : ∏ i ∈ s, p i ≠ 0) (h : ∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)) :
Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

A compositum of splitting fields is a splitting field

source
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L) :
Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥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]`.

source
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_left {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] :
Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
source
theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_right {F : Type u_1} [Field F] (E : Type u_2) [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F ↥L] :
Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
source
theorem IntermediateField.adjoin_simple_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : E) :
CompleteLattice.IsCompactElement F⟮x⟯

Adjoining a single element is compact in the lattice of intermediate fields.

source
theorem IntermediateField.adjoin_finset_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Finset E) :
CompleteLattice.IsCompactElement (adjoin F ↑S)

Adjoining a finite subset is compact in the lattice of intermediate fields.

source
theorem IntermediateField.adjoin_finite_isCompactElement {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} (h : S.Finite) :
CompleteLattice.IsCompactElement (adjoin F S)

Adjoining a finite subset is compact in the lattice of intermediate fields.

source
instance IntermediateField.instIsCompactlyGenerated {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
IsCompactlyGenerated (IntermediateField F E)

The lattice of intermediate fields is compactly generated.

source
theorem IntermediateField.exists_finset_of_mem_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ (i : ι), f i) :
∃ (s : Finset ι), x ∈ ⨆ i ∈ s, f i
source
theorem IntermediateField.exists_finset_of_mem_supr' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ (i : ι), f i) :
∃ (s : Finset ((i : ι) × ↥(f i))), x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯
source
theorem IntermediateField.exists_finset_of_mem_supr'' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Type u_3} {f : ι → IntermediateField F E} (h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)) {x : E} (hx : x ∈ ⨆ (i : ι), f i) :
∃ (s : Finset ((i : ι) × ↥(f i))), x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet E)
source
theorem IntermediateField.exists_finset_of_mem_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
∃ (T : Finset E), ↑T ⊆ S ∧ x ∈ adjoin F ↑T
source
@[simp]
theorem IntermediateField.rank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :
Module.rank F ↥K = 1 ↔ K = ⊥
source
@[simp]
theorem IntermediateField.finrank_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :
Module.finrank F ↥K = 1 ↔ K = ⊥
source
@[simp]
theorem IntermediateField.rank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.rank F ↥⊥ = 1
source
@[simp]
theorem IntermediateField.finrank_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.finrank F ↥⊥ = 1
source
@[simp]
theorem IntermediateField.rank_bot' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.rank (↥⊥) E = Module.rank F E
source
@[simp]
theorem IntermediateField.finrank_bot' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.finrank (↥⊥) E = Module.finrank F E
source
@[simp]
theorem IntermediateField.rank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.rank (↥⊤) E = 1
source
@[simp]
theorem IntermediateField.finrank_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.finrank (↥⊤) E = 1
source
@[simp]
theorem IntermediateField.rank_top' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.rank F ↥⊤ = Module.rank F E
source
@[simp]
theorem IntermediateField.finrank_top' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.finrank F ↥⊤ = Module.finrank F E
source
theorem IntermediateField.finrank_eq_one_iff_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} :
Module.finrank (↥K) E = 1 ↔ K = ⊤
source
theorem IntermediateField.bot_eq_top_iff_finrank_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
⊥ = ⊤ ↔ Module.finrank F E = 1
source
theorem IntermediateField.isSimpleOrder_of_finrank_prime (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] (hp : Nat.Prime (Module.finrank F E)) :
IsSimpleOrder (IntermediateField F E)
source
theorem IntermediateField.rank_adjoin_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :
Module.rank F ↥(adjoin F S) = 1 ↔ S ⊆ ↑⊥
source
theorem IntermediateField.rank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :
Module.rank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
source
theorem IntermediateField.finrank_adjoin_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :
Module.finrank F ↥(adjoin F S) = 1 ↔ S ⊆ ↑⊥
source
theorem IntermediateField.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :
Module.finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
source
theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1) :
⊥ = ⊤

If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`.

source
theorem IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ = 1) :
⊥ = ⊤
source
theorem IntermediateField.subsingleton_of_rank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1) :
Subsingleton (IntermediateField F E)
source
theorem IntermediateField.subsingleton_of_finrank_adjoin_eq_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ = 1) :
Subsingleton (IntermediateField F E)
source
theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ ≤ 1) :
⊥ = ⊤

If `F⟮x⟯` has dimension `≤1` over `F` for every `x ∈ E` then `F = E`.

source
theorem IntermediateField.subsingleton_of_finrank_adjoin_le_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ ≤ 1) :
Subsingleton (IntermediateField F E)
source
theorem IntermediateField.minpoly_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
minpoly F (AdjoinSimple.gen F α) = minpoly F α
source
theorem IntermediateField.aeval_gen_minpoly (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :
(Polynomial.aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0
source
noncomputable def IntermediateField.adjoinRootEquivAdjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :
AdjoinRoot (minpoly F α) ≃ₐ[F] ↥F⟮α⟯

algebra isomorphism between `AdjoinRoot` and `F⟮α⟯`

Equations

- IntermediateField.adjoinRootEquivAdjoin F h = AlgEquiv.ofBijective (AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (IntermediateField.AdjoinSimple.gen F α) ⋯) ⋯

Instances For

source
theorem IntermediateField.adjoinRootEquivAdjoin_apply_root (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :
(adjoinRootEquivAdjoin F h) (AdjoinRoot.root (minpoly F α)) = AdjoinSimple.gen F α
source
@[simp]
theorem IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} (h : IsIntegral F α) :
(adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)
source
theorem IntermediateField.adjoin_root_eq_top {K : Type u} [Field K] (p : Polynomial K) [Fact (Irreducible p)] :
K⟮AdjoinRoot.root p⟯ = ⊤
source
noncomputable def IntermediateField.powerBasisAux {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
Module.Basis (Fin (minpoly K x).natDegree) K ↥K⟮x⟯

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).reindex (finCongr ⋯)

Instances For

source
noncomputable def IntermediateField.adjoin.powerBasis {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
PowerBasis K ↥K⟮x⟯

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

source
@[simp]
theorem IntermediateField.adjoin.powerBasis_dim {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
(powerBasis hx).dim = (minpoly K x).natDegree
source
@[simp]
theorem IntermediateField.adjoin.powerBasis_gen {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
(powerBasis hx).gen = AdjoinSimple.gen K x
source
theorem IntermediateField.adjoin.finiteDimensional {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
FiniteDimensional K ↥K⟮x⟯
source
theorem IntermediateField.isAlgebraic_adjoin_simple {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
Algebra.IsAlgebraic K ↥K⟮x⟯
source
theorem IntermediateField.adjoin.finrank {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

If `x` is an algebraic element of field `K`, then its minimal polynomial has degree `[K(x) : K]`.

source
theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] {S : Set K} (hprim : adjoin F S = ⊤) :
adjoin E S = ⊤

If `K / E / F` is a field extension tower, `S ⊂ K` is such that `F(S) = K`, then `E(S) = K`.

source
theorem IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} [FiniteDimensional F E] (hprim : F⟮α⟯ = ⊤) (K : IntermediateField F E) :
adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = 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.

source
instance IntermediateField.instFiniteSubtypeMemBot (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Module.Finite F ↥⊥
source
theorem IntermediateField.exists_lt_finrank_of_infinite_dimensional {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (hnfd : ¬FiniteDimensional F E) (n : ℕ) :
∃ (L : IntermediateField F E), FiniteDimensional F ↥L ∧ n < Module.finrank F ↥L

If `E / F` is an infinite algebraic extension, then there exists an intermediate field `L / F` with arbitrarily large finite extension degree.

source
theorem minpoly.natDegree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :
(minpoly K x).natDegree ≤ Module.finrank K L
source
theorem minpoly.degree_le {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] :
(minpoly K x).degree ≤ ↑(Module.finrank K L)
source
theorem minpoly.degree_dvd {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
(minpoly K x).natDegree ∣ Module.finrank K L

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]`.

source
theorem IntermediateField.isAlgebraic_iSup {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {ι : Type u_4} {t : ι → IntermediateField K L} (h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)) :
Algebra.IsAlgebraic K ↥(⨆ (i : ι), t i)

A compositum of algebraic extensions is algebraic

source
theorem IntermediateField.isAlgebraic_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) :
Algebra.IsAlgebraic K ↥(adjoin K S)
source
theorem IntermediateField.finiteDimensional_adjoin {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {S : Set L} [Finite ↑S] (hS : ∀ x ∈ S, IsIntegral K x) :
FiniteDimensional K ↥(adjoin K S)

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`.

source
noncomputable def IntermediateField.algHomAdjoinIntegralEquiv (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) :
(↥F⟮α⟯ →ₐ[F] K) ≃ { x : K // x ∈ (minpoly F α).aroots K }

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

source
theorem IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (x : { x : K // x ∈ (minpoly F α).aroots K }) :
((algHomAdjoinIntegralEquiv F h).symm x) (AdjoinSimple.gen F α) = ↑x
source
noncomputable def IntermediateField.fintypeOfAlgHomAdjoinIntegral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) :
Fintype (↥F⟮α⟯ →ₐ[F] K)

Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K`

Equations

- IntermediateField.fintypeOfAlgHomAdjoinIntegral F h = PowerBasis.AlgHom.fintype (IntermediateField.adjoin.powerBasis h)

Instances For

source
theorem IntermediateField.card_algHom_adjoin_integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)) :
Nat.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
source
theorem Polynomial.irreducible_comp {K : Type u} [Field K] {f g : Polynomial K} (hfm : f.Monic) (hgm : g.Monic) (hf : Irreducible f) (hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (map (algebraMap K ↥K⟮x⟯) g - C (IntermediateField.AdjoinSimple.gen K x))) :
Irreducible (f.comp g)

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.

source
theorem minpoly.eq_of_root {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_ev : (Polynomial.aeval y) (minpoly K x) = 0) :
minpoly K y = minpoly K x

If `y : L` is a root of `minpoly K x`, then `minpoly K y = minpoly K x`.

source
noncomputable def minpoly.algEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯

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

- One or more equations did not get rendered due to their size.

Instances For

source
theorem minpoly.algEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
(algEquiv hx h_mp) (IntermediateField.AdjoinSimple.gen K x) = IntermediateField.AdjoinSimple.gen K y

`minpoly.algEquiv` sends the generator of `K⟮x⟯` to the generator of `K⟮y⟯`.

source
noncomputable def PowerBasis.equivAdjoinSimple {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
↥K⟮pb.gen⟯ ≃ₐ[K] L

`pb.equivAdjoinSimple` is the equivalence between `K⟮pb.gen⟯` and `L` itself.

Equations

- pb.equivAdjoinSimple = (IntermediateField.adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯

Instances For

source
@[simp]
theorem PowerBasis.equivAdjoinSimple_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :
pb.equivAdjoinSimple ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) = (Polynomial.aeval pb.gen) f
source
@[simp]
theorem PowerBasis.equivAdjoinSimple_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
pb.equivAdjoinSimple (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen
source
@[simp]
theorem PowerBasis.equivAdjoinSimple_symm_aeval {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) (f : Polynomial K) :
pb.equivAdjoinSimple.symm ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f
source
@[simp]
theorem PowerBasis.equivAdjoinSimple_symm_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) :
pb.equivAdjoinSimple.symm pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen
source
theorem IntermediateField.lift_cardinalMk_adjoin_le (F : Type u) [Field F] {E : Type v} [Field E] [Algebra F E] (s : Set E) :
Cardinal.lift.{u, v} (Cardinal.mk ↥(adjoin F s)) ≤ max (max (Cardinal.lift.{v, u} (Cardinal.mk F)) (Cardinal.lift.{u, v} (Cardinal.mk ↑s))) Cardinal.aleph0
source
theorem IntermediateField.cardinalMk_adjoin_le (F : Type u) [Field F] {E : Type u} [Field E] [Algebra F E] (s : Set E) :
Cardinal.mk ↥(adjoin F s) ≤ max (max (Cardinal.mk F) (Cardinal.mk ↑s)) Cardinal.aleph0
source
theorem IntermediateField.isAlgebraic_adjoin_pair {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsIntegral K x) (hy : IsIntegral K y) :
Algebra.IsAlgebraic K ↥K⟮x, y⟯
source
theorem IntermediateField.finiteDimensional_adjoin_pair {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsIntegral K x) (hy : IsIntegral K y) :
FiniteDimensional K ↥K⟮x, y⟯
source
theorem IntermediateField.mem_adjoin_pair_left (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
x ∈ K⟮x, y⟯
source
theorem IntermediateField.mem_adjoin_pair_right (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
y ∈ K⟮x, y⟯
source
def IntermediateField.AdjoinPair.gen₁ (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
↥K⟮x, y⟯

The first generator of an intermediate field of the form `K⟮x, y⟯`.

Equations

- IntermediateField.AdjoinPair.gen₁ K x y = ⟨x, ⋯⟩

Instances For

source
def IntermediateField.AdjoinPair.gen₂ (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
↥K⟮x, y⟯

The second generator of an intermediate field of the form `K⟮x, y⟯`.

Equations

- IntermediateField.AdjoinPair.gen₂ K x y = ⟨y, ⋯⟩

Instances For

source
theorem IntermediateField.AdjoinPair.algebraMap_gen₁ (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
(algebraMap (↥K⟮x, y⟯) L) (gen₁ K x y) = x
source
theorem IntermediateField.AdjoinPair.algebraMap_gen₂ (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : L) :
(algebraMap (↥K⟮x, y⟯) L) (gen₂ K x y) = y