Conjugate root classes

In this file, we define the ConjRootClass of a field extension L / K as the quotient of L by the relation IsConjRoot K.

def ConjRootClass (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Type u_2

ConjRootClass K L is the quotient of L by the relation IsConjRoot K.

Equations

• ConjRootClass K L = Quotient (IsConjRoot.setoid K L)

def ConjRootClass.mk (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) : ConjRootClass K L

The canonical quotient map from a field K into the ConjRootClass of the field extension L / K.

Equations

• ConjRootClass.mk K x = ⟦x⟧

@[simp]

theorem ConjRootClass.mk_def (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} : ⟦x⟧ = mk K x

instance ConjRootClass.instZero (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] : Zero (ConjRootClass K L)

Equations

• ConjRootClass.instZero K = { zero := ConjRootClass.mk K 0 }

theorem ConjRootClass.ind (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] {motive : ConjRootClass K L → Prop} (h : ∀ (x : L), motive (mk K x)) (c : ConjRootClass K L) : motive c

@[simp]

theorem ConjRootClass.mk_eq_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} : mk K x = mk K y ↔ IsConjRoot K x y

@[simp]

theorem ConjRootClass.mk_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : mk K 0 = 0

@[simp]

theorem ConjRootClass.mk_eq_zero_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) : mk K x = 0 ↔ x = 0

instance ConjRootClass.instDecidableEqOfNormalOfFintypeAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] : DecidableEq (ConjRootClass K L)

Equations

• ConjRootClass.instDecidableEqOfNormalOfFintypeAlgEquiv = Quotient.decidableEq

def ConjRootClass.carrier {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (c : ConjRootClass K L) : Set L

c.carrier is the set of conjugates represented by c.

Equations

• c.carrier = ConjRootClass.mk K ⁻¹' {c}

@[simp]

theorem ConjRootClass.mem_carrier {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {c : ConjRootClass K L} : x ∈ c.carrier ↔ mk K x = c

@[simp]

theorem ConjRootClass.carrier_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : carrier 0 = {0}

theorem ConjRootClass.carrier_inj {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Function.Injective carrier

instance ConjRootClass.instNeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Neg (ConjRootClass K L)

Equations

• ConjRootClass.instNeg = { neg := Quotient.map (fun (x : L) => -x) ⋯ }

theorem ConjRootClass.mk_neg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) : -mk K x = mk K (-x)

instance ConjRootClass.instInvolutiveNeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : InvolutiveNeg (ConjRootClass K L)

Equations

• ConjRootClass.instInvolutiveNeg = { toNeg := ConjRootClass.instNeg, neg_neg := ⋯ }

@[simp]

theorem ConjRootClass.carrier_neg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (c : ConjRootClass K L) : (-c).carrier = -c.carrier

theorem ConjRootClass.exists_mem_carrier_add_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x y : ConjRootClass K L) : (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y

instance ConjRootClass.instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (c : ConjRootClass K L) : DecidablePred fun (x : L) => x ∈ c.carrier

Equations

• c.instDecidablePredMemSetCarrierOfNormalOfDecidableEqOfFintypeAlgEquiv x = decidable_of_iff (ConjRootClass.mk K x = c) ⋯

instance ConjRootClass.instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (c : ConjRootClass K L) : Fintype ↑c.carrier

Equations

• c.instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv = Quotient.recOnSubsingleton c fun (x : L) => Fintype.ofFinset (Finset.image (fun (x_1 : L ≃ₐ[K] L) => x_1 x) Finset.univ) ⋯

noncomputable def ConjRootClass.minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : ConjRootClass K L → Polynomial K

c.minpoly is the minimal polynomial of the conjugates.

Equations

• ConjRootClass.minpoly = Quotient.lift (minpoly K) ⋯

@[simp]

theorem ConjRootClass.minpoly_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) : (mk K x).minpoly = minpoly K x

@[simp]

theorem ConjRootClass.minpoly_inj {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {c d : ConjRootClass K L} : c.minpoly = d.minpoly ↔ c = d

theorem ConjRootClass.minpoly_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Function.Injective ConjRootClass.minpoly

theorem ConjRootClass.splits_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [n : Normal K L] (c : ConjRootClass K L) : Polynomial.Splits (algebraMap K L) c.minpoly

theorem ConjRootClass.monic_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (c : ConjRootClass K L) : c.minpoly.Monic

theorem ConjRootClass.minpoly_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (c : ConjRootClass K L) : c.minpoly ≠ 0

theorem ConjRootClass.irreducible_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (c : ConjRootClass K L) : Irreducible c.minpoly

theorem ConjRootClass.aeval_minpoly_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (x : L) (c : ConjRootClass K L) : (Polynomial.aeval x) c.minpoly = 0 ↔ mk K x = c

theorem ConjRootClass.rootSet_minpoly_eq_carrier {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (c : ConjRootClass K L) : c.minpoly.rootSet L = c.carrier

theorem ConjRootClass.separable_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] (c : ConjRootClass K L) : c.minpoly.Separable

theorem ConjRootClass.nodup_aroots_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] (c : ConjRootClass K L) : (c.minpoly.aroots L).Nodup

theorem ConjRootClass.aroots_minpoly_eq_carrier_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] (c : ConjRootClass K L) [Fintype ↑c.carrier] : c.minpoly.aroots L = c.carrier.toFinset.val

theorem ConjRootClass.carrier_eq_mk_aroots_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] (c : ConjRootClass K L) [Fintype ↑c.carrier] : c.carrier.toFinset = { val := c.minpoly.aroots L, nodup := ⋯ }

theorem ConjRootClass.minpoly.map_eq_prod {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsSeparable K L] [Normal K L] (c : ConjRootClass K L) [Fintype ↑c.carrier] : Polynomial.map (algebraMap K L) c.minpoly = ∏ x ∈ c.carrier.toFinset, (Polynomial.X - Polynomial.C x)