Conjugate roots

Given two elements x and y of some K-algebra, these two elements are conjugate roots over K if they have the same minimal polynomial over K.

Main definitions

• IsConjRoot: IsConjRoot K x y means y is a conjugate root of x over K.

Main results

• isConjRoot_iff_exists_algEquiv: Let L / K be a normal field extension. For any two elements x and y in L, IsConjRoot K x y is equivalent to the existence of an algebra equivalence σ : L ≃ₐ[K] L such that y = σ x.
• notMem_iff_exists_ne_and_isConjRoot: Let L / K be a field extension. If x is a separable element over K and the minimal polynomial of x splits in L, then x is not in the K iff there exists a different conjugate root of x in L over K.

TODO

• Move IsConjRoot to earlier files and refactor the theorems in field theory using IsConjRoot.

• Prove IsConjRoot.smul, if x and y are conjugate roots, then so are r • x and r • y.

Tags

conjugate root, minimal polynomial

def IsConjRoot (R : Type u_1) {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] (x y : A) : Prop

We say that y is a conjugate root of x over K if the minimal polynomial of x is the same as the minimal polynomial of y.

Equations

• IsConjRoot R x y = (minpoly R x = minpoly R y)

theorem isConjRoot_def {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x y : A} : IsConjRoot R x y ↔ minpoly R x = minpoly R y

The definition of conjugate roots.

theorem IsConjRoot.refl {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x : A} : IsConjRoot R x x

Every element is a conjugate root of itself.

theorem IsConjRoot.symm {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x y : A} (h : IsConjRoot R x y) : IsConjRoot R y x

If y is a conjugate root of x, then x is also a conjugate root of y.

theorem IsConjRoot.trans {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x y z : A} (h₁ : IsConjRoot R x y) (h₂ : IsConjRoot R y z) : IsConjRoot R x z

If y is a conjugate root of x and z is a conjugate root of y, then z is a conjugate root of x.

def IsConjRoot.setoid (R : Type u_1) (A : Type u_5) [CommRing R] [Ring A] [Algebra R A] : Setoid A

The setoid structure on A defined by the equivalence relation of IsConjRoot R · ·.

Equations

• IsConjRoot.setoid R A = { r := IsConjRoot R, iseqv := ⋯ }

theorem IsConjRoot.aeval_eq_zero {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x y : A} (h : IsConjRoot R x y) : (Polynomial.aeval y) (minpoly R x) = 0

Let p be the minimal polynomial of x. If y is a conjugate root of x, then p y = 0.

theorem IsConjRoot.add_algebraMap {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] {x y : S} (r : K) (h : IsConjRoot K x y) : IsConjRoot K (x + (algebraMap K S) r) (y + (algebraMap K S) r)

Let r be an element of the base ring. If y is a conjugate root of x, then y + r is a conjugate root of x + r.

theorem IsConjRoot.sub_algebraMap {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] {x y : S} (r : K) (h : IsConjRoot K x y) : IsConjRoot K (x - (algebraMap K S) r) (y - (algebraMap K S) r)

Let r be an element of the base ring. If y is a conjugate root of x, then y - r is a conjugate root of x - r.

theorem IsConjRoot.neg {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] {x y : S} (h : IsConjRoot K x y) : IsConjRoot K (-x) (-y)

If y is a conjugate root of x, then -y is a conjugate root of -x.

theorem isConjRoot_algHom_iff_of_injective {R : Type u_1} {A : Type u_5} {B : Type u_6} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {x y : A} {f : A →ₐ[R] B} (hf : Function.Injective ⇑f) : IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y

A variant of isConjRoot_algHom_iff, only assuming Function.Injective f, instead of DivisionRing A. If y is a conjugate root of x and f is an injective R-algebra homomorphism, then f y is a conjugate root of f x.

theorem isConjRoot_algHom_iff {R : Type u_1} {B : Type u_6} [CommRing R] [Ring B] [Algebra R B] {A : Type u_7} [DivisionRing A] [Algebra R A] [Nontrivial B] {x y : A} (f : A →ₐ[R] B) : IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y

If y is a conjugate root of x in some division ring and f is a R-algebra homomorphism, then f y is a conjugate root of f x.

theorem isConjRoot_of_aeval_eq_zero {K : Type u_2} {A : Type u_5} [Ring A] [Field K] [Algebra K A] [IsDomain A] {x y : A} (hx : IsIntegral K x) (h : (Polynomial.aeval y) (minpoly K x) = 0) : IsConjRoot K x y

Let p be the minimal polynomial of an integral element x. If p y = 0, then y is a conjugate root of x.

theorem isConjRoot_iff_aeval_eq_zero {K : Type u_2} {A : Type u_5} [Ring A] [Field K] [Algebra K A] [IsDomain A] {x y : A} (h : IsIntegral K x) : IsConjRoot K x y ↔ (Polynomial.aeval y) (minpoly K x) = 0

Let p be the minimal polynomial of an integral element x. Then y is a conjugate root of x if and only if p y = 0.

@[simp]

theorem isConjRoot_of_algEquiv {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] (x : A) (s : A ≃ₐ[R] A) : IsConjRoot R x (s x)

Let s be an R-algebra isomorphism. Then s x is a conjugate root of x.

@[simp]

theorem isConjRoot_of_algEquiv' {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] (x : A) (s : A ≃ₐ[R] A) : IsConjRoot R (s x) x

A variant of isConjRoot_of_algEquiv. Let s be an R-algebra isomorphism. Then x is a conjugate root of s x.

@[simp]

theorem isConjRoot_of_algEquiv₂ {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] (x : A) (s₁ s₂ : A ≃ₐ[R] A) : IsConjRoot R (s₁ x) (s₂ x)

Let s₁ and s₂ be two R-algebra isomorphisms. Then s₂ x is a conjugate root of s₁ x.

theorem IsConjRoot.exists_algEquiv {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [Normal K L] {x y : L} (h : IsConjRoot K x y) : ∃ (σ : L ≃ₐ[K] L), σ y = x

Let L / K be a normal field extension. For any two elements x and y in L, if y is a conjugate root of x, then there exists a K-automorphism σ : L ≃ₐ[K] L such that σ y = x.

theorem isConjRoot_iff_exists_algEquiv {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [Normal K L] {x y : L} : IsConjRoot K x y ↔ ∃ (σ : L ≃ₐ[K] L), σ y = x

Let L / K be a normal field extension. For any two elements x and y in L, y is a conjugate root of x if and only if there exists a K-automorphism σ : L ≃ₐ[K] L such that σ y = x.

theorem isConjRoot_iff_orbitRel {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [Normal K L] {x y : L} : IsConjRoot K x y ↔ (MulAction.orbitRel (L ≃ₐ[K] L) L) x y

Let L / K be a normal field extension. For any two elements x and y in L, y is a conjugate root of x if and only if x and y falls in the same orbit of the action of Galois group.

theorem IsConjRoot.of_isScalarTower {K : Type u_2} {L : Type u_3} {S : Type u_4} [CommRing S] [Field K] [Field L] [Algebra K S] [Algebra K L] [Algebra L S] [IsDomain S] [IsScalarTower K L S] {x y : S} (hx : IsIntegral K x) (h : IsConjRoot L x y) : IsConjRoot K x y

Let S / L / K be a tower of extensions. For any two elements y and x in S, if y is a conjugate root of x over L, then y is also a conjugate root of x over K.

theorem isConjRoot_iff_mem_minpoly_aroots {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x y : S} (h : IsIntegral K x) : IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S

y is a conjugate root of x over K if and only if y is a root of the minimal polynomial of x. This is variant of isConjRoot_iff_aeval_eq_zero.

theorem isConjRoot_iff_mem_minpoly_rootSet {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x y : S} (h : IsIntegral K x) : IsConjRoot K x y ↔ y ∈ (minpoly K x).rootSet S

y is a conjugate root of x over K if and only if y is a root of the minimal polynomial of x. This is variant of isConjRoot_iff_aeval_eq_zero.

theorem IsConjRoot.isIntegral {R : Type u_1} {A : Type u_5} [CommRing R] [Ring A] [Algebra R A] {x y : A} (hx : IsIntegral R x) (h : IsConjRoot R x y) : IsIntegral R y

If y is a conjugate root of an integral element x over R, then y is also integral over R.

theorem IsConjRoot.eq_algebraMap_of_injective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] [NoZeroSMulDivisors R S] {r : R} {x : S} (h : IsConjRoot R ((algebraMap R S) r) x) (hf : Function.Injective ⇑(algebraMap R S)) : x = (algebraMap R S) r

A variant of IsConjRoot.eq_of_isConjRoot_algebraMap, only assuming Nontrivial R, NoZeroSMulDivisors R A and Function.Injective (algebraMap R A) instead of Field R. If x is a conjugate root of some element algebraMap R S r in the image of the base ring, then x = algebraMap R S r.

theorem IsConjRoot.eq_algebraMap {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {r : K} {x : S} (h : IsConjRoot K ((algebraMap K S) r) x) : x = (algebraMap K S) r

If x is a conjugate root of some element algebraMap R S r in the image of the base ring, then x = algebraMap R S r.

theorem IsConjRoot.eq_zero_of_injective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] [NoZeroSMulDivisors R S] {x : S} (h : IsConjRoot R 0 x) (hf : Function.Injective ⇑(algebraMap R S)) : x = 0

A variant of IsConjRoot.eq_zero, only assuming Nontrivial R, NoZeroSMulDivisors R A and Function.Injective (algebraMap R A) instead of Field R. If x is a conjugate root of 0, then x = 0.

theorem IsConjRoot.eq_zero {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x : S} (h : IsConjRoot K 0 x) : x = 0

If x is a conjugate root of 0, then x = 0.

theorem isConjRoot_iff_eq_algebraMap_of_injective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] [NoZeroSMulDivisors R S] {r : R} {x : S} (hf : Function.Injective ⇑(algebraMap R S)) : IsConjRoot R ((algebraMap R S) r) x ↔ x = (algebraMap R S) r

A variant of IsConjRoot.eq_of_isConjRoot_algebraMap, only assuming Nontrivial R, NoZeroSMulDivisors R A and Function.Injective (algebraMap R A) instead of Field R. If x is a conjugate root of some element algebraMap R S r in the image of the base ring, then x = algebraMap R S r.

@[simp]

theorem isConjRoot_iff_eq_algebraMap {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {r : K} {x : S} : IsConjRoot K ((algebraMap K S) r) x ↔ x = (algebraMap K S) r

An element x is a conjugate root of some element algebraMap R S r in the image of the base ring if and only if x = algebraMap R S r.

@[simp]

theorem isConjRoot_iff_eq_algebraMap' {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {r : K} {x : S} : IsConjRoot K x ((algebraMap K S) r) ↔ x = (algebraMap K S) r

A variant of isConjRoot_iff_eq_algebraMap. an element algebraMap R S r in the image of the base ring is a conjugate root of an element x if and only if x = algebraMap R S r.

theorem isConjRoot_zero_iff_eq_zero_of_injective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] {x : S} [NoZeroSMulDivisors R S] (hf : Function.Injective ⇑(algebraMap R S)) : IsConjRoot R 0 x ↔ x = 0

A variant of IsConjRoot.iff_eq_zero, only assuming Nontrivial R, NoZeroSMulDivisors R A and Function.Injective (algebraMap R A) instead of Field R. x is a conjugate root of 0 if and only if x = 0.

@[simp]

theorem isConjRoot_zero_iff_eq_zero {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x : S} : IsConjRoot K 0 x ↔ x = 0

x is a conjugate root of 0 if and only if x = 0.

@[simp]

theorem isConjRoot_zero_iff_eq_zero' {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x : S} : IsConjRoot K x 0 ↔ x = 0

A variant of IsConjRoot.iff_eq_zero. 0 is a conjugate root of x if and only if x = 0.

theorem IsConjRoot.ne_zero_of_injective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [Nontrivial R] [NoZeroSMulDivisors R S] {x y : S} (hx : x ≠ 0) (h : IsConjRoot R x y) (hf : Function.Injective ⇑(algebraMap R S)) : y ≠ 0

A variant of IsConjRoot.ne_zero, only assuming Nontrivial R, NoZeroSMulDivisors R A and Function.Injective (algebraMap R A) instead of Field R. If y is a conjugate root of a nonzero element x, then y is not zero.

theorem IsConjRoot.ne_zero {K : Type u_2} {S : Type u_4} [CommRing S] [Field K] [Algebra K S] [IsDomain S] {x y : S} (hx : x ≠ 0) (h : IsConjRoot K x y) : y ≠ 0

If y is a conjugate root of a nonzero element x, then y is not zero.

theorem notMem_iff_exists_ne_and_isConjRoot {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (h : IsSeparable K x) (sp : Polynomial.Splits (algebraMap K L) (minpoly K x)) : x ∉ ⊥ ↔ ∃ (y : L), x ≠ y ∧ IsConjRoot K x y

Let L / K be a field extension. If x is a separable element over K and the minimal polynomial of x splits in L, then x is not in K if and only if there exists a conjugate root of x over K in L which is not equal to x itself.

@[deprecated notMem_iff_exists_ne_and_isConjRoot (since := "2025-05-23")]

theorem not_mem_iff_exists_ne_and_isConjRoot {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (h : IsSeparable K x) (sp : Polynomial.Splits (algebraMap K L) (minpoly K x)) : x ∉ ⊥ ↔ ∃ (y : L), x ≠ y ∧ IsConjRoot K x y

Alias of notMem_iff_exists_ne_and_isConjRoot.

---

Let L / K be a field extension. If x is a separable element over K and the minimal polynomial of x splits in L, then x is not in K if and only if there exists a conjugate root of x over K in L which is not equal to x itself.