Adjoining roots of polynomials

This file defines the commutative ring AdjoinRoot f, the ring R[X]/(f) obtained from a commutative ring R and a polynomial f : R[X]. If furthermore R is a field and f is irreducible, the field structure on AdjoinRoot f is constructed.

We suggest stating results on IsAdjoinRoot instead of AdjoinRoot to achieve higher generality, since IsAdjoinRoot works for all different constructions of R[α] including AdjoinRoot f = R[X]/(f) itself.

Main definitions and results

The main definitions are in the AdjoinRoot namespace.

• mk f : R[X] →+* AdjoinRoot f, the natural ring homomorphism.

• of f : R →+* AdjoinRoot f, the natural ring homomorphism.

• root f : AdjoinRoot f, the image of X in R[X]/(f).

• lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (AdjoinRoot f) →+* S, the ring homomorphism from R[X]/(f) to S extending i : R →+* S and sending X to x.

• lift_hom (x : S) (hfx : aeval x f = 0) : AdjoinRoot f →ₐ[R] S, the algebra homomorphism from R[X]/(f) to S extending algebraMap R S and sending X to x

• equiv : (AdjoinRoot f →ₐ[F] E) ≃ {x // x ∈ f.aroots E} a bijection between algebra homomorphisms from AdjoinRoot and roots of f in S

def AdjoinRoot {R : Type u} [CommRing R] (f : Polynomial R) : Type u

Adjoin a root of a polynomial f to a commutative ring R. We define the new ring as the quotient of R[X] by the principal ideal generated by f.

Equations

• AdjoinRoot f = (Polynomial R ⧸ Ideal.span {f})

instance AdjoinRoot.instCommRing {R : Type u} [CommRing R] (f : Polynomial R) : CommRing (AdjoinRoot f)

Equations

• AdjoinRoot.instCommRing f = Ideal.Quotient.commRing (Ideal.span {f})

instance AdjoinRoot.instInhabited {R : Type u} [CommRing R] (f : Polynomial R) : Inhabited (AdjoinRoot f)

Equations

• AdjoinRoot.instInhabited f = { default := 0 }

instance AdjoinRoot.instDecidableEq {R : Type u} [CommRing R] (f : Polynomial R) : DecidableEq (AdjoinRoot f)

Equations

• AdjoinRoot.instDecidableEq f = Classical.decEq (AdjoinRoot f)

theorem AdjoinRoot.nontrivial {R : Type u} [CommRing R] (f : Polynomial R) [IsDomain R] (h : f.degree ≠ 0) : Nontrivial (AdjoinRoot f)

def AdjoinRoot.mk {R : Type u} [CommRing R] (f : Polynomial R) : Polynomial R →+* AdjoinRoot f

Ring homomorphism from R[x] to AdjoinRoot f sending X to the root.

Equations

• AdjoinRoot.mk f = Ideal.Quotient.mk (Ideal.span {f})

theorem AdjoinRoot.induction_on {R : Type u} [CommRing R] (f : Polynomial R) {C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ (p : Polynomial R), C ((AdjoinRoot.mk f) p)) : C x

def AdjoinRoot.of {R : Type u} [CommRing R] (f : Polynomial R) : R →+* AdjoinRoot f

Embedding of the original ring R into AdjoinRoot f.

Equations

• AdjoinRoot.of f = (AdjoinRoot.mk f).comp Polynomial.C

instance AdjoinRoot.instSMulAdjoinRoot {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f)

Equations

• AdjoinRoot.instSMulAdjoinRoot f = Submodule.Quotient.instSMul' (Ideal.span {f})

instance AdjoinRoot.instDistribSMulOfIsScalarTower {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f)

Equations

• AdjoinRoot.instDistribSMulOfIsScalarTower f = Submodule.Quotient.distribSMul' (Ideal.span {f})

@[simp]

theorem AdjoinRoot.smul_mk {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : Polynomial R) : a • (AdjoinRoot.mk f) x = (AdjoinRoot.mk f) (a • x)

theorem AdjoinRoot.smul_of {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) : a • (AdjoinRoot.of f) x = (AdjoinRoot.of f) (a • x)

instance AdjoinRoot.instIsScalarTower {R : Type u} [CommRing R] (R₁ : Type u_1) (R₂ : Type u_2) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : Polynomial R) : IsScalarTower R₁ R₂ (AdjoinRoot f)

Equations

• ⋯ = ⋯

instance AdjoinRoot.instSMulCommClass {R : Type u} [CommRing R] (R₁ : Type u_1) (R₂ : Type u_2) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R] (f : Polynomial R) : SMulCommClass R₁ R₂ (AdjoinRoot f)

Equations

• ⋯ = ⋯

instance AdjoinRoot.isScalarTower_right {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] : IsScalarTower S (AdjoinRoot f) (AdjoinRoot f)

Equations

• ⋯ = ⋯

instance AdjoinRoot.instDistribMulActionOfIsScalarTower {R : Type u} {S : Type v} [CommRing R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (f : Polynomial R) : DistribMulAction S (AdjoinRoot f)

Equations

• AdjoinRoot.instDistribMulActionOfIsScalarTower f = Submodule.Quotient.distribMulAction' (Ideal.span {f})

instance AdjoinRoot.instAlgebra {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f)

Equations

• AdjoinRoot.instAlgebra f = Ideal.Quotient.algebra S

@[simp]

theorem AdjoinRoot.algebraMap_eq {R : Type u} [CommRing R] (f : Polynomial R) : algebraMap R (AdjoinRoot f) = AdjoinRoot.of f

theorem AdjoinRoot.algebraMap_eq' {R : Type u} (S : Type v) [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] : algebraMap S (AdjoinRoot f) = (AdjoinRoot.of f).comp (algebraMap S R)

theorem AdjoinRoot.finiteType {R : Type u} [CommRing R] (f : Polynomial R) : Algebra.FiniteType R (AdjoinRoot f)

theorem AdjoinRoot.finitePresentation {R : Type u} [CommRing R] (f : Polynomial R) : Algebra.FinitePresentation R (AdjoinRoot f)

def AdjoinRoot.root {R : Type u} [CommRing R] (f : Polynomial R) : AdjoinRoot f

The adjoined root.

Equations

• AdjoinRoot.root f = (AdjoinRoot.mk f) Polynomial.X

instance AdjoinRoot.hasCoeT {R : Type u} [CommRing R] {f : Polynomial R} : CoeTC R (AdjoinRoot f)

Equations

• AdjoinRoot.hasCoeT = { coe := ⇑(AdjoinRoot.of f) }

theorem AdjoinRoot.algHom_ext {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [Semiring S] [Algebra R S] {g₁ : AdjoinRoot f →ₐ[R] S} {g₂ : AdjoinRoot f →ₐ[R] S} (h : g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f)) : g₁ = g₂

Two R-AlgHom from AdjoinRoot f to the same R-algebra are the same iff they agree on root f.

@[simp]

theorem AdjoinRoot.mk_eq_mk {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} {h : Polynomial R} : (AdjoinRoot.mk f) g = (AdjoinRoot.mk f) h ↔ f ∣ g - h

@[simp]

theorem AdjoinRoot.mk_eq_zero {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} : (AdjoinRoot.mk f) g = 0 ↔ f ∣ g

@[simp]

theorem AdjoinRoot.mk_self {R : Type u} [CommRing R] {f : Polynomial R} : (AdjoinRoot.mk f) f = 0

@[simp]

theorem AdjoinRoot.mk_C {R : Type u} [CommRing R] {f : Polynomial R} (x : R) : (AdjoinRoot.mk f) (Polynomial.C x) = (AdjoinRoot.of f) x

@[simp]

theorem AdjoinRoot.mk_X {R : Type u} [CommRing R] {f : Polynomial R} : (AdjoinRoot.mk f) Polynomial.X = AdjoinRoot.root f

theorem AdjoinRoot.mk_ne_zero_of_degree_lt {R : Type u} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g ≠ 0) (hd : g.degree < f.degree) : (AdjoinRoot.mk f) g ≠ 0

theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt {R : Type u} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g ≠ 0) (hd : g.natDegree < f.natDegree) : (AdjoinRoot.mk f) g ≠ 0

@[simp]

theorem AdjoinRoot.aeval_eq {R : Type u} [CommRing R] {f : Polynomial R} (p : Polynomial R) : (Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) p

theorem AdjoinRoot.adjoinRoot_eq_top {R : Type u} [CommRing R] {f : Polynomial R} : Algebra.adjoin R {AdjoinRoot.root f} = ⊤

@[simp]

theorem AdjoinRoot.eval₂_root {R : Type u} [CommRing R] (f : Polynomial R) : Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0

theorem AdjoinRoot.isRoot_root {R : Type u} [CommRing R] (f : Polynomial R) : (Polynomial.map (AdjoinRoot.of f) f).IsRoot (AdjoinRoot.root f)

theorem AdjoinRoot.isAlgebraic_root {R : Type u} [CommRing R] {f : Polynomial R} (hf : f ≠ 0) : IsAlgebraic R (AdjoinRoot.root f)

theorem AdjoinRoot.of.injective_of_degree_ne_zero {R : Type u} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.degree ≠ 0) : Function.Injective ⇑(AdjoinRoot.of f)

def AdjoinRoot.lift {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] (i : R →+* S) (x : S) (h : Polynomial.eval₂ i x f = 0) : AdjoinRoot f →+* S

Lift a ring homomorphism i : R →+* S to AdjoinRoot f →+* S.

Equations

• AdjoinRoot.lift i x h = Ideal.Quotient.lift (Ideal.span {f}) (Polynomial.eval₂RingHom i x) ⋯

@[simp]

theorem AdjoinRoot.lift_mk {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) (g : Polynomial R) : (AdjoinRoot.lift i a h) ((AdjoinRoot.mk f) g) = Polynomial.eval₂ i a g

@[simp]

theorem AdjoinRoot.lift_root {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) : (AdjoinRoot.lift i a h) (AdjoinRoot.root f) = a

@[simp]

theorem AdjoinRoot.lift_of {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) {x : R} : (AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x

@[simp]

theorem AdjoinRoot.lift_comp_of {R : Type u} {S : Type v} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) : (AdjoinRoot.lift i a h).comp (AdjoinRoot.of f) = i

def AdjoinRoot.liftHom {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (x : S) (hfx : (Polynomial.aeval x) f = 0) : AdjoinRoot f →ₐ[R] S

Produce an algebra homomorphism AdjoinRoot f →ₐ[R] S sending root f to a root of f in S.

Equations

• AdjoinRoot.liftHom f x hfx = let __src := AdjoinRoot.lift (algebraMap R S) x hfx; { toRingHom := __src, commutes' := ⋯ }

@[simp]

theorem AdjoinRoot.coe_liftHom {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (x : S) (hfx : (Polynomial.aeval x) f = 0) : ↑(AdjoinRoot.liftHom f x hfx) = AdjoinRoot.lift (algebraMap R S) x hfx

@[simp]

theorem AdjoinRoot.aeval_algHom_eq_zero {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (ϕ : AdjoinRoot f →ₐ[R] S) : (Polynomial.aeval (ϕ (AdjoinRoot.root f))) f = 0

@[simp]

theorem AdjoinRoot.liftHom_eq_algHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R) (ϕ : AdjoinRoot f →ₐ[R] S) : AdjoinRoot.liftHom f (ϕ (AdjoinRoot.root f)) ⋯ = ϕ

@[simp]

theorem AdjoinRoot.liftHom_mk {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {g : Polynomial R} : (AdjoinRoot.liftHom f a hfx) ((AdjoinRoot.mk f) g) = (Polynomial.aeval a) g

@[simp]

theorem AdjoinRoot.liftHom_root {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) : (AdjoinRoot.liftHom f a hfx) (AdjoinRoot.root f) = a

@[simp]

theorem AdjoinRoot.liftHom_of {R : Type u} {S : Type v} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {x : R} : (AdjoinRoot.liftHom f a hfx) ((AdjoinRoot.of f) x) = (algebraMap R S) x

@[simp]

theorem AdjoinRoot.root_isInv {R : Type u} [CommRing R] (r : R) : (AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1

theorem AdjoinRoot.algHom_subsingleton {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] {r : R} : Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)

theorem AdjoinRoot.isDomain_of_prime {R : Type u} [CommRing R] {f : Polynomial R} (hf : Prime f) : IsDomain (AdjoinRoot f)

theorem AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero {R : Type u} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : Prime f) (hf' : f.degree ≠ 0) : NoZeroSMulDivisors R (AdjoinRoot f)

instance AdjoinRoot.span_maximal_of_irreducible {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] : (Ideal.span {f}).IsMaximal

Equations

• ⋯ = ⋯

noncomputable instance AdjoinRoot.instGroupWithZero {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] : GroupWithZero (AdjoinRoot f)

Equations

• AdjoinRoot.instGroupWithZero = Ideal.Quotient.groupWithZero (Ideal.span {f})

noncomputable instance AdjoinRoot.instField {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] : Field (AdjoinRoot f)

Equations

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

theorem AdjoinRoot.coe_injective {K : Type w} [Field K] {f : Polynomial K} (h : f.degree ≠ 0) : Function.Injective ⇑(AdjoinRoot.of f)

theorem AdjoinRoot.coe_injective' {K : Type w} [Field K] {f : Polynomial K} [Fact (Irreducible f)] : Function.Injective ⇑(AdjoinRoot.of f)

theorem AdjoinRoot.mul_div_root_cancel {K : Type w} [Field K] (f : Polynomial K) [Fact (Irreducible f)] : (Polynomial.X - Polynomial.C (AdjoinRoot.root f)) * (Polynomial.map (AdjoinRoot.of f) f / (Polynomial.X - Polynomial.C (AdjoinRoot.root f))) = Polynomial.map (AdjoinRoot.of f) f

instance AdjoinRoot.instIsNoetherianRing {R : Type u} [CommRing R] [IsNoetherianRing R] {f : Polynomial R} : IsNoetherianRing (AdjoinRoot f)

Equations

• ⋯ = ⋯

theorem AdjoinRoot.isIntegral_root' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : IsIntegral R (AdjoinRoot.root g)

def AdjoinRoot.modByMonicHom {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : AdjoinRoot g →ₗ[R] Polynomial R

AdjoinRoot.modByMonicHom sends the equivalence class of f mod g to f %ₘ g.

This is a well-defined right inverse to AdjoinRoot.mk, see AdjoinRoot.mk_leftInverse.

Equations

• AdjoinRoot.modByMonicHom hg = (Submodule.restrictScalars R (Ideal.span {g})).liftQ g.modByMonicHom ⋯ ∘ₗ ↑(Submodule.Quotient.restrictScalarsEquiv R (Ideal.span {g})).symm

@[simp]

theorem AdjoinRoot.modByMonicHom_mk {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : Polynomial R) : (AdjoinRoot.modByMonicHom hg) ((AdjoinRoot.mk g) f) = f %ₘ g

theorem AdjoinRoot.mk_leftInverse {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : Function.LeftInverse ⇑(AdjoinRoot.mk g) ⇑(AdjoinRoot.modByMonicHom hg)

theorem AdjoinRoot.mk_surjective {R : Type u} [CommRing R] {g : Polynomial R} : Function.Surjective ⇑(AdjoinRoot.mk g)

def AdjoinRoot.powerBasisAux' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g)

The elements 1, root g, ..., root g ^ (d - 1) form a basis for AdjoinRoot g, where g is a monic polynomial of degree d.

Equations

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

theorem AdjoinRoot.powerBasisAux'_repr_symm_apply {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R) : (AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i : Fin g.natDegree, (Polynomial.monomial ↑i) (c i))

@[simp]

theorem AdjoinRoot.powerBasisAux'_repr_apply_to_fun {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) : ((AdjoinRoot.powerBasisAux' hg).repr f) i = ((AdjoinRoot.modByMonicHom hg) f).coeff ↑i

@[simp]

theorem AdjoinRoot.powerBasis'_gen {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : (AdjoinRoot.powerBasis' hg).gen = AdjoinRoot.root g

@[simp]

theorem AdjoinRoot.powerBasis'_dim {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : (AdjoinRoot.powerBasis' hg).dim = g.natDegree

def AdjoinRoot.powerBasis' {R : Type u} [CommRing R] {g : Polynomial R} (hg : g.Monic) : PowerBasis R (AdjoinRoot g)

The power basis 1, root g, ..., root g ^ (d - 1) for AdjoinRoot g, where g is a monic polynomial of degree d.

Equations

• AdjoinRoot.powerBasis' hg = { gen := AdjoinRoot.root g, dim := g.natDegree, basis := AdjoinRoot.powerBasisAux' hg, basis_eq_pow := ⋯ }

theorem AdjoinRoot.isIntegral_root {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : IsIntegral K (AdjoinRoot.root f)

theorem AdjoinRoot.minpoly_root {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : minpoly K (AdjoinRoot.root f) = f * Polynomial.C f.leadingCoeff⁻¹

def AdjoinRoot.powerBasisAux {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f)

The elements 1, root f, ..., root f ^ (d - 1) form a basis for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

Equations

• AdjoinRoot.powerBasisAux hf = let f' := f * Polynomial.C f.leadingCoeff⁻¹; let_fun deg_f' := ⋯; let_fun minpoly_eq := ⋯; Basis.mk ⋯ ⋯

@[simp]

theorem AdjoinRoot.powerBasis_gen {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : (AdjoinRoot.powerBasis hf).gen = AdjoinRoot.root f

@[simp]

theorem AdjoinRoot.powerBasis_dim {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : (AdjoinRoot.powerBasis hf).dim = f.natDegree

def AdjoinRoot.powerBasis {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : PowerBasis K (AdjoinRoot f)

The power basis 1, root f, ..., root f ^ (d - 1) for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

Equations

• AdjoinRoot.powerBasis hf = { gen := AdjoinRoot.root f, dim := f.natDegree, basis := AdjoinRoot.powerBasisAux hf, basis_eq_pow := ⋯ }

theorem AdjoinRoot.minpoly_powerBasis_gen {K : Type w} [Field K] {f : Polynomial K} (hf : f ≠ 0) : minpoly K (AdjoinRoot.powerBasis hf).gen = f * Polynomial.C f.leadingCoeff⁻¹

theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic {K : Type w} [Field K] {f : Polynomial K} (hf : f.Monic) (hf' : optParam (f ≠ 0) ⋯) : minpoly K (AdjoinRoot.powerBasis hf').gen = f

@[simp]

theorem AdjoinRoot.Minpoly.toAdjoin_apply (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : S) : ∀ (a : Polynomial R ⧸ Submodule.toAddSubgroup (Ideal.span {minpoly R x})), (AdjoinRoot.Minpoly.toAdjoin R x) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩) ⋯) a

def AdjoinRoot.Minpoly.toAdjoin (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : S) : AdjoinRoot (minpoly R x) →ₐ[R] ↥(Algebra.adjoin R {x})

The surjective algebra morphism R[X]/(minpoly R x) → R[x]. If R is a integrally closed domain and x is integral, this is an isomorphism, see minpoly.equivAdjoin.

Equations

• AdjoinRoot.Minpoly.toAdjoin R x = AdjoinRoot.liftHom (minpoly R x) ⟨x, ⋯⟩ ⋯

theorem AdjoinRoot.Minpoly.toAdjoin_apply' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} (a : AdjoinRoot (minpoly R x)) : (AdjoinRoot.Minpoly.toAdjoin R x) a = (AdjoinRoot.liftHom (minpoly R x) ⟨x, ⋯⟩ ⋯) a

theorem AdjoinRoot.Minpoly.toAdjoin.apply_X {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {x : S} : (AdjoinRoot.Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) Polynomial.X) = ⟨x, ⋯⟩

theorem AdjoinRoot.Minpoly.toAdjoin.surjective (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Function.Surjective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)

@[simp]

theorem AdjoinRoot.equiv'_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ⇑(AdjoinRoot.equiv' g pb h₁ h₂) = ⇑(AdjoinRoot.liftHom g pb.gen h₂)

@[simp]

theorem AdjoinRoot.equiv'_symm_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ⇑(AdjoinRoot.equiv' g pb h₁ h₂).symm = ⇑(pb.lift (AdjoinRoot.root g) h₁)

def AdjoinRoot.equiv' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : AdjoinRoot g ≃ₐ[R] S

If S is an extension of R with power basis pb and g is a monic polynomial over R such that pb.gen has a minimal polynomial g, then S is isomorphic to AdjoinRoot g.

Compare PowerBasis.equivOfRoot, which would require h₂ : aeval pb.gen (minpoly R (root g)) = 0; that minimal polynomial is not guaranteed to be identical to g.

Equations

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

theorem AdjoinRoot.equiv'_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ↑(AdjoinRoot.equiv' g pb h₁ h₂) = AdjoinRoot.liftHom g pb.gen h₂

theorem AdjoinRoot.equiv'_symm_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ↑(AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift (AdjoinRoot.root g) h₁

def AdjoinRoot.equiv (L : Type u_1) (F : Type u_2) [Field F] [CommRing L] [IsDomain L] [Algebra F L] (f : Polynomial F) (hf : f ≠ 0) : (AdjoinRoot f →ₐ[F] L) ≃ { x : L // x ∈ f.aroots L }

If L is a field extension of F and f is a polynomial over F then the set of maps from F[x]/(f) into L is in bijection with the set of roots of f in L.

Equations

• AdjoinRoot.equiv L F f hf = (AdjoinRoot.powerBasis hf).liftEquiv'.trans ((Equiv.refl L).subtypeEquiv ⋯)

def AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I ≃+* AdjoinRoot f ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I)

The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f)) for α a root of f : R[X] and I : Ideal R.

See adjoin_root.quot_map_of_equiv for the isomorphism with (R/I)[X] / (f mod I).

Equations

• AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f = Ideal.quotEquivOfEq ⋯

@[simp]

theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f) : (AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x

theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f) : (AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f).symm ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) x

def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : AdjoinRoot f ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I) ≃+* (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) (Ideal.span {f})

The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : R[X] and I : Ideal R

Equations

• AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f = DoubleQuot.quotQuotEquivComm (Ideal.span {f}) (Ideal.map Polynomial.C I)

theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)) = (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p

@[simp]

theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).symm ((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)

def AdjoinRoot.Polynomial.quotQuotEquivComm {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f} ≃+* (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸ Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}

The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : R[X] and I : Ideal R

Equations

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

@[simp]

theorem AdjoinRoot.Polynomial.quotQuotEquivComm_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.Polynomial.quotQuotEquivComm I f) ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)

@[simp]

theorem AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.Polynomial.quotQuotEquivComm I f).symm ((Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)

def AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I ≃+* Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}

The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : R[X] and I : Ideal R.

Equations

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

@[simp]

theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)

@[simp]

theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) (p : Polynomial R) : (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) p)

@[simp]

theorem AdjoinRoot.quotEquivQuotMap_symm_apply {R : Type u} [CommRing R] (f : Polynomial R) (I : Ideal R) (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}) : (AdjoinRoot.quotEquivQuotMap f I).symm a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm a

@[simp]

theorem AdjoinRoot.quotEquivQuotMap_apply {R : Type u} [CommRing R] (f : Polynomial R) (I : Ideal R) (a : AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I) : (AdjoinRoot.quotEquivQuotMap f I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f) a

noncomputable def AdjoinRoot.quotEquivQuotMap {R : Type u} [CommRing R] (f : Polynomial R) (I : Ideal R) : (AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I) ≃ₐ[R] Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}

Promote AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot to an alg_equiv.

Equations

• AdjoinRoot.quotEquivQuotMap f I = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem AdjoinRoot.quotEquivQuotMap_apply_mk {R : Type u} [CommRing R] (f : Polynomial R) (g : Polynomial R) (I : Ideal R) : (AdjoinRoot.quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)

theorem AdjoinRoot.quotEquivQuotMap_symm_apply_mk {R : Type u} [CommRing R] (f : Polynomial R) (g : Polynomial R) (I : Ideal R) : (AdjoinRoot.quotEquivQuotMap f I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)

@[simp]

theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) : ∀ (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}), (pb.quotientEquivQuotientMinpolyMap I).symm a = (↑↑(AlgEquiv.ofRingEquiv ⋯)).symm ((↑↑(AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)).symm a)

@[simp]

theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) : ∀ (a : S ⧸ Ideal.map (algebraMap R S) I), (pb.quotientEquivQuotientMinpolyMap I) a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I (minpoly R pb.gen)) ((Ideal.quotientMap (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I) ↑(↑(AdjoinRoot.equiv' (minpoly R pb.gen) pb ⋯ ⋯)).symm ⋯) a)

noncomputable def PowerBasis.quotientEquivQuotientMinpolyMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) : (S ⧸ Ideal.map (algebraMap R S) I) ≃ₐ[R] Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}

Let α have minimal polynomial f over R and I be an ideal of R, then R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p).

Equations

• pb.quotientEquivQuotientMinpolyMap I = (AlgEquiv.ofRingEquiv ⋯).trans (AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)

theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) (g : Polynomial R) : (pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)

theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) (I : Ideal R) (g : Polynomial R) : (pb.quotientEquivQuotientMinpolyMap I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)

theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K : Type u_1} {L : Type u_2} [CommRing K] [IsDomain K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] {f : Polynomial L} (hf : Irreducible f) : ∃ (g : Polynomial K), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

If L / K is an integral extension, K is a domain, L is a field, then any irreducible polynomial over L divides some monic irreducible polynomial over K.