Adjoining Elements to Fields #
This file contains many results about adjoining elements to fields.
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
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
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
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)
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.
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.
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)
:
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)
:
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)
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)
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)
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
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].
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
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
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)
:
@[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 = ⊥
@[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 = ⊥
@[simp]
theorem
IntermediateField.rank_bot
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Module.rank F ↥⊥ = 1
@[simp]
theorem
IntermediateField.finrank_bot
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Module.finrank F ↥⊥ = 1
@[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
@[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
@[simp]
theorem
IntermediateField.rank_top
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Module.rank (↥⊤) E = 1
@[simp]
theorem
IntermediateField.finrank_top
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Module.finrank (↥⊤) E = 1
@[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
@[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
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)
:
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)
:
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.
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)
:
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
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⟮α⟯
Stacks Tag 09G1 (Algebraic case)
Equations
Instances For
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 α
@[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 α)
theorem
IntermediateField.adjoin_root_eq_top
{K : Type u}
[Field K]
(p : Polynomial K)
[Fact (Irreducible p)]
:
K⟮AdjoinRoot.root p⟯ = ⊤
noncomputable def
IntermediateField.powerBasisAux
{K : Type u}
[Field K]
{L : Type u_3}
[Field L]
[Algebra K L]
{x : L}
(hx : IsIntegral 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
Instances For
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
@[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
@[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
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⟯
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⟯
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].
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 = ⊤)
:
If K / E / F is a field extension tower, S ⊂ K is such that F(S) = K,
then E(S) = K.
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.
instance
IntermediateField.instFiniteSubtypeMemBot
(F : Type u_1)
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
:
Module.Finite F ↥⊥
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.
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
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)
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].
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
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)
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.
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 α)
:
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
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
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 of algebra homomorphism F⟮α⟯ →ₐ[F] K
Equations
Instances For
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 α))
:
Fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
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.
noncomputable def
AdjoinRoot.algHomOfDvd
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hpq : q ∣ p)
:
AdjoinRoot p →ₐ[K] AdjoinRoot q
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
theorem
AdjoinRoot.coe_algHomOfDvd
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hpq : q ∣ p)
:
(↑↑(algHomOfDvd hpq).toRingHom).toFun = ⇑(liftHom p (root q) ⋯)
theorem
AdjoinRoot.algHomOfDvd_apply_root
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hpq : q ∣ p)
:
(algHomOfDvd hpq) (root p) = root q
algHomOfDvd sends AdjoinRoot.root p to AdjoinRoot.root q.
noncomputable def
AdjoinRoot.algEquivOfEq
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(h_eq : p = q)
:
AdjoinRoot p ≃ₐ[K] AdjoinRoot 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
theorem
AdjoinRoot.coe_algEquivOfEq
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(h_eq : p = q)
:
(algEquivOfEq hp h_eq).toFun = ⇑(liftHom p (root q) ⋯)
theorem
AdjoinRoot.algEquivOfEq_toAlgHom
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(h_eq : p = q)
:
↑(algEquivOfEq hp h_eq) = liftHom p (root q) ⋯
theorem
AdjoinRoot.algEquivOfEq_apply_root
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(h_eq : p = q)
:
(algEquivOfEq hp h_eq) (root p) = root q
algEquivOfEq sends AdjoinRoot.root p to AdjoinRoot.root q.
noncomputable def
AdjoinRoot.algEquivOfAssociated
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(hpq : Associated p q)
:
AdjoinRoot p ≃ₐ[K] AdjoinRoot 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
theorem
AdjoinRoot.coe_algEquivOfAssociated
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(hpq : Associated p q)
:
(algEquivOfAssociated hp hpq).toFun = ⇑(liftHom p (root q) ⋯)
theorem
AdjoinRoot.algEquivOfAssociated_toAlgHom
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(hpq : Associated p q)
:
↑(algEquivOfAssociated hp hpq) = liftHom p (root q) ⋯
theorem
AdjoinRoot.algEquivOfAssociated_apply_root
{K : Type u_1}
[Field K]
{p q : Polynomial K}
(hp : p ≠ 0)
(hpq : Associated p q)
:
(algEquivOfAssociated hp hpq) (root p) = root q
algEquivOfAssociated sends AdjoinRoot.root p to AdjoinRoot.root q.
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)
:
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
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⟯.
noncomputable def
PowerBasis.equivAdjoinSimple
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(pb : PowerBasis K L)
:
pb.equivAdjoinSimple is the equivalence between K⟮pb.gen⟯ and L itself.
Equations
- pb.equivAdjoinSimple = (IntermediateField.adjoin.powerBasis ⋯).equivOfMinpoly pb ⋯
Instances For
@[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
@[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
@[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
@[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
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) ≤ Cardinal.mk F ⊔ Cardinal.mk ↑s ⊔ Cardinal.aleph0