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

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

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})

Instances For

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

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

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

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

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

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

source
theorem AdjoinRoot.nontrivial {R : Type u_1} [CommRing R] (f : Polynomial R) [IsDomain R] (h : f.degree ≠ 0) :
Nontrivial (AdjoinRoot f)
source
def AdjoinRoot.mk {R : Type u_1} [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})

Instances For

source
theorem AdjoinRoot.induction_on {R : Type u_1} [CommRing R] (f : Polynomial R) {C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ (p : Polynomial R), C ((mk f) p)) :
C x
source
def AdjoinRoot.of {R : Type u_1} [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

Instances For

source
instance AdjoinRoot.instSMulAdjoinRoot {R : Type u_1} {S : Type u_2} [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})

source
instance AdjoinRoot.instDistribSMulOfIsScalarTower {R : Type u_1} {S : Type u_2} [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})

source
@[simp]
theorem AdjoinRoot.smul_mk {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : Polynomial R) :
a • (mk f) x = (mk f) (a • x)
source
theorem AdjoinRoot.smul_of {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) :
a • (of f) x = (of f) (a • x)
source
instance AdjoinRoot.instIsScalarTower {R : Type u_1} [CommRing R] (R₁ : Type u_5) (R₂ : Type u_6) [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)
source
instance AdjoinRoot.instSMulCommClass {R : Type u_1} [CommRing R] (R₁ : Type u_5) (R₂ : Type u_6) [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)
source
instance AdjoinRoot.isScalarTower_right {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [DistribSMul S R] [IsScalarTower S R R] :
IsScalarTower S (AdjoinRoot f) (AdjoinRoot f)
source
instance AdjoinRoot.instDistribMulActionOfIsScalarTower {R : Type u_1} {S : Type u_2} [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})

source
instance AdjoinRoot.instAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] :
Algebra S (AdjoinRoot f)

`R[x]/(f)` is `R`-algebra

Equations

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

source
def AdjoinRoot.mkₐ {R : Type u_1} [CommRing R] (f : Polynomial R) :
Polynomial R →ₐ[R] AdjoinRoot f

`R`-algebra homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`.

Equations

- AdjoinRoot.mkₐ f = Ideal.Quotient.mkₐ R (Ideal.span {f})

Instances For

source
@[simp]
theorem AdjoinRoot.mkₐ_toRingHom {R : Type u_1} [CommRing R] (f : Polynomial R) :
↑(mkₐ f) = mk f
source
@[simp]
theorem AdjoinRoot.coe_mkₐ {R : Type u_1} [CommRing R] (f : Polynomial R) :
⇑(mkₐ f) = ⇑(mk f)
source
@[simp]
theorem AdjoinRoot.algebraMap_eq {R : Type u_1} [CommRing R] (f : Polynomial R) :
algebraMap R (AdjoinRoot f) = of f
source
theorem AdjoinRoot.algebraMap_eq' {R : Type u_1} (S : Type u_2) [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] :
algebraMap S (AdjoinRoot f) = (of f).comp (algebraMap S R)
source
instance AdjoinRoot.finiteType {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommSemiring S] [Algebra S R] [Algebra.FiniteType S R] :
Algebra.FiniteType S (AdjoinRoot f)
source
instance AdjoinRoot.finitePresentation {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra S R] [Algebra.FinitePresentation S R] :
Algebra.FinitePresentation S (AdjoinRoot f)
source
def AdjoinRoot.root {R : Type u_1} [CommRing R] (f : Polynomial R) :
AdjoinRoot f

The adjoined root.

Equations

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

Instances For

source
@[reducible, inline]
abbrev AdjoinRoot.ofAlgHom {R : Type u_1} (S : Type u_2) [CommRing R] [CommSemiring S] [Algebra S R] (p : Polynomial R) :
R →ₐ[S] AdjoinRoot p

Embedding of the original ring `R` into `AdjoinRoot p`.

Equations

- AdjoinRoot.ofAlgHom S p = Algebra.algHom S R (AdjoinRoot p)

Instances For

source
@[simp]
theorem AdjoinRoot.toRingHom_ofAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommSemiring S] [Algebra S R] (p : Polynomial R) :
↑(ofAlgHom S p) = of p
source
@[simp]
theorem AdjoinRoot.coe_ofAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommSemiring S] [Algebra S R] (p : Polynomial R) :
⇑(ofAlgHom S p) = ⇑(of p)
source
theorem AdjoinRoot.algHom_ext' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommSemiring S] [Semiring T] [Algebra S R] [Algebra S T] (p : Polynomial R) {f g : AdjoinRoot p →ₐ[S] T} (hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)) (hRoot : f (root p) = g (root p)) :
f = g
source
theorem AdjoinRoot.algHom_ext'_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommSemiring S] [Semiring T] [Algebra S R] [Algebra S T] {p : Polynomial R} {f g : AdjoinRoot p →ₐ[S] T} :
f = g ↔ f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p) ∧ f (root p) = g (root p)
source
instance AdjoinRoot.hasCoeT {R : Type u_1} [CommRing R] {f : Polynomial R} :
CoeTC R (AdjoinRoot f)
Equations

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

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

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

source
theorem AdjoinRoot.algHom_ext_iff {R : Type u_1} {S : Type u_2} [CommRing R] {f : Polynomial R} [Semiring S] [Algebra R S] {g₁ g₂ : AdjoinRoot f →ₐ[R] S} :
g₁ = g₂ ↔ g₁ (root f) = g₂ (root f)
source
@[simp]
theorem AdjoinRoot.mk_eq_mk {R : Type u_1} [CommRing R] {f g h : Polynomial R} :
(mk f) g = (mk f) h ↔ f ∣ g - h
source
@[simp]
theorem AdjoinRoot.mk_eq_zero {R : Type u_1} [CommRing R] {f g : Polynomial R} :
(mk f) g = 0 ↔ f ∣ g
source
@[simp]
theorem AdjoinRoot.mk_self {R : Type u_1} [CommRing R] {f : Polynomial R} :
(mk f) f = 0
source
@[simp]
theorem AdjoinRoot.mk_C {R : Type u_1} [CommRing R] {f : Polynomial R} (x : R) :
(mk f) (Polynomial.C x) = (of f) x
source
@[simp]
theorem AdjoinRoot.mk_X {R : Type u_1} [CommRing R] {f : Polynomial R} :
(mk f) Polynomial.X = root f
source
theorem AdjoinRoot.mk_ne_zero_of_degree_lt {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g ≠ 0) (hd : g.degree < f.degree) :
(mk f) g ≠ 0
source
theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (h0 : g ≠ 0) (hd : g.natDegree < f.natDegree) :
(mk f) g ≠ 0
source
theorem AdjoinRoot.aeval_eq_of_algebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial S) (p : Polynomial R) :
(Polynomial.aeval (root f)) p = (mk f) (Polynomial.map (algebraMap R S) p)
source
@[simp]
theorem AdjoinRoot.aeval_eq {R : Type u_1} [CommRing R] {f : Polynomial R} (p : Polynomial R) :
(Polynomial.aeval (root f)) p = (mk f) p
source
theorem AdjoinRoot.adjoinRoot_eq_top {R : Type u_1} [CommRing R] {f : Polynomial R} :
Algebra.adjoin R {root f} = ⊤
source
@[simp]
theorem AdjoinRoot.eval₂_root {R : Type u_1} [CommRing R] (f : Polynomial R) :
Polynomial.eval₂ (of f) (root f) f = 0
source
theorem AdjoinRoot.isRoot_root {R : Type u_1} [CommRing R] (f : Polynomial R) :
(Polynomial.map (of f) f).IsRoot (root f)
source
theorem AdjoinRoot.isAlgebraic_root {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f ≠ 0) :
IsAlgebraic R (root f)
source
theorem AdjoinRoot.of.injective_of_degree_ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.degree ≠ 0) :
Function.Injective ⇑(of f)
source
def AdjoinRoot.lift {R : Type u_1} {S : Type u_2} [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) ⋯

Instances For

source
@[simp]
theorem AdjoinRoot.lift_mk {R : Type u_1} {S : Type u_2} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) (g : Polynomial R) :
(lift i a h) ((mk f) g) = Polynomial.eval₂ i a g
source
@[simp]
theorem AdjoinRoot.lift_root {R : Type u_1} {S : Type u_2} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) :
(lift i a h) (root f) = a
source
@[simp]
theorem AdjoinRoot.lift_of {R : Type u_1} {S : Type u_2} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) {x : R} :
(lift i a h) ((of f) x) = i x
source
@[simp]
theorem AdjoinRoot.lift_comp_of {R : Type u_1} {S : Type u_2} [CommRing R] {f : Polynomial R} [CommRing S] {i : R →+* S} {a : S} (h : Polynomial.eval₂ i a f = 0) :
(lift i a h).comp (of f) = i
source
def AdjoinRoot.liftAlgHom {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) :
AdjoinRoot p →ₐ[S] T

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

Equations

- AdjoinRoot.liftAlgHom p i x h = { toRingHom := AdjoinRoot.lift i.toRingHom x h, commutes' := ⋯ }

Instances For

source
@[simp]
theorem AdjoinRoot.toRingHom_liftAlgHom {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) :
↑(liftAlgHom p i x h) = lift i.toRingHom x h
source
theorem AdjoinRoot.coe_liftAlgHom {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) :
⇑(liftAlgHom p i x h) = ⇑(lift i.toRingHom x h)
source
@[simp]
theorem AdjoinRoot.liftAlgHom_of {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) (r : R) :
(liftAlgHom p i x h) ((of p) r) = i r
source
@[simp]
theorem AdjoinRoot.liftAlgHom_mk {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) (f : Polynomial R) :
(liftAlgHom p i x h) ((mk p) f) = Polynomial.eval₂ (↑i) x f
source
@[simp]
theorem AdjoinRoot.liftAlgHom_root {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra S R] [Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T) (h : Polynomial.eval₂ (↑i) x p = 0) :
(liftAlgHom p i x h) (root p) = x
source
@[deprecated AdjoinRoot.liftAlgHom (since := "2025-10-10")]
def AdjoinRoot.liftHom {R : Type u_1} {S : Type u_2} [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 = AdjoinRoot.liftAlgHom f (Algebra.ofId R S) x hfx

Instances For

source
@[deprecated AdjoinRoot.toRingHom_liftAlgHom (since := "2025-10-10")]
theorem AdjoinRoot.coe_liftHom {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (x : S) (hfx : (Polynomial.aeval x) f = 0) :
↑(liftHom f x hfx) = lift (algebraMap R S) x hfx
source
@[simp]
theorem AdjoinRoot.aeval_algHom_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (ϕ : AdjoinRoot f →ₐ[R] S) :
(Polynomial.aeval (ϕ (root f))) f = 0
source
@[simp]
theorem AdjoinRoot.liftAlgHom_eq_algHom {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (ϕ : AdjoinRoot f →ₐ[R] S) :
liftAlgHom f (Algebra.ofId R S) (ϕ (root f)) ⋯ = ϕ
source
@[deprecated AdjoinRoot.liftAlgHom_eq_algHom (since := "2025-10-10")]
theorem AdjoinRoot.liftHom_eq_algHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R) (ϕ : AdjoinRoot f →ₐ[R] S) :
liftHom f (ϕ (root f)) ⋯ = ϕ
source
@[deprecated AdjoinRoot.liftAlgHom_mk (since := "2025-10-10")]
theorem AdjoinRoot.liftHom_mk {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {g : Polynomial R} :
(liftAlgHom f (Algebra.ofId R S) a hfx) ((mk f) g) = (Polynomial.aeval a) g
source
@[deprecated AdjoinRoot.liftAlgHom_root (since := "2025-10-10")]
theorem AdjoinRoot.liftHom_root {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) :
(liftHom f a hfx) (root f) = a
source
@[deprecated AdjoinRoot.liftAlgHom_of (since := "2025-10-10")]
theorem AdjoinRoot.liftHom_of {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] {a : S} [Algebra R S] (hfx : (Polynomial.aeval a) f = 0) {x : R} :
(liftHom f a hfx) ((of f) x) = (algebraMap R S) x
source
@[simp]
theorem AdjoinRoot.root_isInv {R : Type u_1} [CommRing R] (r : R) :
(of (Polynomial.C r * Polynomial.X - 1)) r * root (Polynomial.C r * Polynomial.X - 1) = 1
source
theorem AdjoinRoot.algHom_subsingleton {R : Type u_1} [CommRing R] {S : Type u_5} [CommRing S] [Algebra R S] {r : R} :
Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)
source
theorem AdjoinRoot.isDomain_of_prime {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : Prime f) :
IsDomain (AdjoinRoot f)
source
theorem AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : Prime f) (hf' : f.degree ≠ 0) :
NoZeroSMulDivisors R (AdjoinRoot f)
source
noncomputable def AdjoinRoot.algHomOfDvd {R : Type u_1} [CommRing R] (f g : Polynomial R) (hgf : g ∣ f) :
AdjoinRoot f →ₐ[R] AdjoinRoot g

The canonical algebraic homomorphism from `AdjoinRoot f` to `AdjoinRoot g`, where the polynomial `g : K[X]` divides `f`.

Equations

- AdjoinRoot.algHomOfDvd f g hgf = AdjoinRoot.liftAlgHom f (Algebra.ofId R (AdjoinRoot g)) (AdjoinRoot.root g) ⋯

Instances For

source
theorem AdjoinRoot.coe_algHomOfDvd {R : Type u_1} [CommRing R] (f g : Polynomial R) (hgf : g ∣ f) :
⇑(algHomOfDvd f g hgf) = ⇑(liftAlgHom f (Algebra.ofId R (AdjoinRoot g)) (root g) ⋯)
source
@[simp]
theorem AdjoinRoot.algHomOfDvd_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hgf : g ∣ f) :
(algHomOfDvd f g hgf) (root f) = root g

`algHomOfDvd` sends `AdjoinRoot.root f` to `AdjoinRoot.root q`.

source
noncomputable def AdjoinRoot.algEquivOfAssociated {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
AdjoinRoot f ≃ₐ[R] AdjoinRoot g

The canonical algebraic equivalence between `AdjoinRoot p` and `AdjoinRoot g`, where the two polynomials `f g : R[X]` are associated.

Equations

- AdjoinRoot.algEquivOfAssociated f g hfg = AlgEquiv.ofAlgHom (AdjoinRoot.algHomOfDvd f g ⋯) (AdjoinRoot.algHomOfDvd g f ⋯) ⋯ ⋯

Instances For

source
theorem AdjoinRoot.coe_algEquivOfAssociated {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
⇑(algEquivOfAssociated f g hfg) = ⇑(algHomOfDvd f g ⋯)
source
@[simp]
theorem AdjoinRoot.algEquivOfAssociated_symm {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
(algEquivOfAssociated f g hfg).symm = algEquivOfAssociated g f ⋯
source
theorem AdjoinRoot.algEquivOfAssociated_toAlgHom {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
↑(algEquivOfAssociated f g hfg) = algHomOfDvd f g ⋯
source
@[simp]
theorem AdjoinRoot.algEquivOfAssociated_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
(algEquivOfAssociated f g hfg) (root f) = root g

`algEquivOfAssociated` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.

source
noncomputable def AdjoinRoot.algEquivOfEq {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
AdjoinRoot f ≃ₐ[R] AdjoinRoot g

The canonical algebraic equivalence between `AdjoinRoot f` and `AdjoinRoot g`, where the two polynomials `f g : R[X]` are equal.

Equations

- AdjoinRoot.algEquivOfEq f g hfg = AdjoinRoot.algEquivOfAssociated f g ⋯

Instances For

source
theorem AdjoinRoot.coe_algEquivOfEq {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
⇑(algEquivOfEq f g hfg) = ⇑(algHomOfDvd f g ⋯)
source
@[simp]
theorem AdjoinRoot.algEquivOfEq_symm {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
(algEquivOfEq f g hfg).symm = algEquivOfEq g f ⋯
source
theorem AdjoinRoot.algEquivOfEq_toAlgHom {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
↑(algEquivOfEq f g hfg) = algHomOfDvd f g ⋯
source
theorem AdjoinRoot.algEquivOfEq_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
(algEquivOfEq f g hfg) (root f) = root g

`algEquivOfEq` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.

source
@[deprecated AdjoinRoot.algHomOfDvd_root (since := "2025-10-10")]
theorem AdjoinRoot.algHomOfDvd_apply_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hgf : g ∣ f) :
(algHomOfDvd f g hgf) (root f) = root g

Alias of `AdjoinRoot.algHomOfDvd_root`.

`algHomOfDvd` sends `AdjoinRoot.root f` to `AdjoinRoot.root q`.

source
@[deprecated AdjoinRoot.algEquivOfEq_root (since := "2025-10-10")]
theorem AdjoinRoot.algEquivOfEq_apply_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : f = g) :
(algEquivOfEq f g hfg) (root f) = root g

Alias of `AdjoinRoot.algEquivOfEq_root`.

`algEquivOfEq` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.

source
@[deprecated AdjoinRoot.algEquivOfAssociated_root (since := "2025-10-10")]
theorem AdjoinRoot.algEquivOfAssociated_apply_root {R : Type u_1} [CommRing R] (f g : Polynomial R) (hfg : Associated f g) :
(algEquivOfAssociated f g hfg) (root f) = root g

Alias of `AdjoinRoot.algEquivOfAssociated_root`.

`algEquivOfAssociated` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.

source
instance AdjoinRoot.span_maximal_of_irreducible {K : Type u_4} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :
(Ideal.span {f}).IsMaximal
source
noncomputable instance AdjoinRoot.instGroupWithZero {K : Type u_4} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :
GroupWithZero (AdjoinRoot f)
Equations

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

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

If `R` is a field and `f` is irreducible, then `AdjoinRoot f` is a field

Equations

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

source
theorem AdjoinRoot.coe_injective {K : Type u_4} [Field K] {f : Polynomial K} (h : f.degree ≠ 0) :
Function.Injective ⇑(of f)
source
theorem AdjoinRoot.coe_injective' {K : Type u_4} [Field K] {f : Polynomial K} [Fact (Irreducible f)] :
Function.Injective ⇑(of f)
source
theorem AdjoinRoot.mul_div_root_cancel {K : Type u_4} [Field K] (f : Polynomial K) [Fact (Irreducible f)] :
(Polynomial.X - Polynomial.C (root f)) * (Polynomial.map (of f) f / (Polynomial.X - Polynomial.C (root f))) = Polynomial.map (of f) f
source
instance AdjoinRoot.instIsNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] {f : Polynomial R} :
IsNoetherianRing (AdjoinRoot f)
source
theorem AdjoinRoot.isIntegral_root' {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
IsIntegral R (root g)
source
def AdjoinRoot.modByMonicHom {R : Type u_1} [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

Instances For

source
@[simp]
theorem AdjoinRoot.modByMonicHom_mk {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : Polynomial R) :
(modByMonicHom hg) ((mk g) f) = f %ₘ g
source
theorem AdjoinRoot.mk_leftInverse {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Function.LeftInverse ⇑(mk g) ⇑(modByMonicHom hg)
source
theorem AdjoinRoot.mk_surjective {R : Type u_1} [CommRing R] {g : Polynomial R} :
Function.Surjective ⇑(mk g)
source
def AdjoinRoot.powerBasisAux' {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Module.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.

Instances For

source
theorem AdjoinRoot.powerBasisAux'_repr_symm_apply {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R) :
(powerBasisAux' hg).repr.symm c = (mk g) (∑ i : Fin g.natDegree, (Polynomial.monomial ↑i) (c i))
source
@[simp]
theorem AdjoinRoot.powerBasisAux'_repr_apply_to_fun {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) :
((powerBasisAux' hg).repr f) i = ((modByMonicHom hg) f).coeff ↑i
source
def AdjoinRoot.powerBasis' {R : Type u_1} [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 := ⋯ }

Instances For

source
@[simp]
theorem AdjoinRoot.powerBasis'_dim {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
(powerBasis' hg).dim = g.natDegree
source
@[simp]
theorem AdjoinRoot.powerBasis'_gen {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
(powerBasis' hg).gen = root g
source
theorem Polynomial.Monic.free_adjoinRoot {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Module.Free R (AdjoinRoot g)
source
theorem Polynomial.Monic.finite_adjoinRoot {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Module.Finite R (AdjoinRoot g)
source
theorem Polynomial.Monic.free_quotient {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Module.Free R (Polynomial R ⧸ Ideal.span {g})

An unwrapped version of `AdjoinRoot.free_of_monic` for better discoverability.

source
theorem Polynomial.Monic.finite_quotient {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) :
Module.Finite R (Polynomial R ⧸ Ideal.span {g})

An unwrapped version of `AdjoinRoot.finite_of_monic` for better discoverability.

source
theorem AdjoinRoot.isIntegral_root {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
IsIntegral K (root f)
source
theorem AdjoinRoot.minpoly_root {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
minpoly K (root f) = f * Polynomial.C f.leadingCoeff⁻¹
source
def AdjoinRoot.powerBasisAux {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
Module.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 = Module.Basis.mk ⋯ ⋯

Instances For

source
def AdjoinRoot.powerBasis {K : Type u_4} [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 := ⋯ }

Instances For

source
@[simp]
theorem AdjoinRoot.powerBasis_gen {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
(powerBasis hf).gen = root f
source
@[simp]
theorem AdjoinRoot.powerBasis_dim {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
(powerBasis hf).dim = f.natDegree
source
theorem AdjoinRoot.minpoly_powerBasis_gen {K : Type u_4} [Field K] {f : Polynomial K} (hf : f ≠ 0) :
minpoly K (powerBasis hf).gen = f * Polynomial.C f.leadingCoeff⁻¹
source
theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic {K : Type u_4} [Field K] {f : Polynomial K} (hf : f.Monic) (hf' : f ≠ 0 := ⋯) :
minpoly K (powerBasis hf').gen = f
source
theorem finrank_quotient_span_eq_natDegree {K : Type u_4} [Field K] {f : Polynomial K} :
Module.finrank K (Polynomial K ⧸ Ideal.span {f}) = f.natDegree

See `finrank_quotient_span_eq_natDegree'` for a version over a ring when `f` is monic.

source
def AdjoinRoot.Minpoly.toAdjoin (R : Type u_1) {S : Type u_2} [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.liftAlgHom (minpoly R x) (Algebra.ofId R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩ ⋯

Instances For

source
@[simp]
theorem AdjoinRoot.Minpoly.coe_toAdjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
⇑(toAdjoin R x) = ⇑(liftAlgHom (minpoly R x) (Algebra.ofId R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩ ⋯)
source
@[deprecated AdjoinRoot.Minpoly.coe_toAdjoin (since := "2025-07-21")]
theorem AdjoinRoot.Minpoly.toAdjoin_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
⇑(toAdjoin R x) = ⇑(liftAlgHom (minpoly R x) (Algebra.ofId R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩ ⋯)

Alias of `AdjoinRoot.Minpoly.coe_toAdjoin`.

source
@[deprecated AdjoinRoot.Minpoly.coe_toAdjoin (since := "2025-07-21")]
theorem AdjoinRoot.Minpoly.toAdjoin_apply' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
⇑(toAdjoin R x) = ⇑(liftAlgHom (minpoly R x) (Algebra.ofId R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩ ⋯)

Alias of `AdjoinRoot.Minpoly.coe_toAdjoin`.

source
theorem AdjoinRoot.Minpoly.coe_toAdjoin_mk_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
↑((toAdjoin R x) ((mk (minpoly R x)) Polynomial.X)) = x
source
@[deprecated AdjoinRoot.Minpoly.coe_toAdjoin_mk_X (since := "2025-07-21")]
theorem AdjoinRoot.Minpoly.toAdjoin.apply_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} :
↑((toAdjoin R x) ((mk (minpoly R x)) Polynomial.X)) = x

Alias of `AdjoinRoot.Minpoly.coe_toAdjoin_mk_X`.

source
theorem AdjoinRoot.Minpoly.toAdjoin.surjective (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) :
Function.Surjective ⇑(toAdjoin R x)
source
def AdjoinRoot.equiv' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (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.

Instances For

source
@[simp]
theorem AdjoinRoot.equiv'_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
⇑(equiv' g pb h₁ h₂).symm = ⇑(pb.lift (root g) h₁)
source
@[simp]
theorem AdjoinRoot.equiv'_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
⇑(equiv' g pb h₁ h₂) = ⇑(liftAlgHom g (Algebra.ofId R S) pb.gen h₂)
source
theorem AdjoinRoot.equiv'_toAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
↑(equiv' g pb h₁ h₂) = liftAlgHom g (Algebra.ofId R S) pb.gen h₂
source
theorem AdjoinRoot.equiv'_symm_toAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
↑(equiv' g pb h₁ h₂).symm = pb.lift (root g) h₁
source
def AdjoinRoot.equiv (L : Type u_5) (F : Type u_6) [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 ⋯)

Instances For

source
def AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) :
AdjoinRoot f ⧸ Ideal.map (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 ⋯

Instances For

source
@[simp]
theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f) :
(quotMapOfEquivQuotMapCMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (of f) I)) x) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) x
source
theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) (x : AdjoinRoot f) :
(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 (of f) I)) x
source
def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk {R : Type u_1} [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)

Instances For

source
theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))) ((mk f) p)) = (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p
source
@[simp]
theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(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))) ((mk f) p)
source
def AdjoinRoot.Polynomial.quotQuotEquivComm {R : Type u_1} [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.

Instances For

source
@[simp]
theorem AdjoinRoot.Polynomial.quotQuotEquivComm_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(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)
source
@[simp]
theorem AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(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)
source
def AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot {R : Type u_1} [CommRing R] (I : Ideal R) (f : Polynomial R) :
AdjoinRoot f ⧸ Ideal.map (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.

Instances For

source
@[simp]
theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(quotAdjoinRootEquivQuotPolynomialQuot I f) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
source
@[simp]
theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk {R : Type u_1} [CommRing R] (I : Ideal R) (f p : Polynomial R) :
(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 (of f) I)) ((mk f) p)
source
noncomputable def AdjoinRoot.quotEquivQuotMap {R : Type u_1} [CommRing R] (f : Polynomial R) (I : Ideal R) :
(AdjoinRoot f ⧸ Ideal.map (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 ⋯

Instances For

source
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_apply {R : Type u_1} [CommRing R] (f : Polynomial R) (I : Ideal R) (a : AdjoinRoot f ⧸ Ideal.map (of f) I) :
(quotEquivQuotMap f I) a = (quotAdjoinRootEquivQuotPolynomialQuot I f) a
source
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_symm_apply {R : Type u_1} [CommRing R] (f : Polynomial R) (I : Ideal R) (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}) :
(quotEquivQuotMap f I).symm a = (quotAdjoinRootEquivQuotPolynomialQuot I f).symm a
source
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_apply_mk {R : Type u_1} [CommRing R] (f g : Polynomial R) (I : Ideal R) :
(quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)
source
theorem AdjoinRoot.quotEquivQuotMap_symm_apply_mk {R : Type u_1} [CommRing R] (f g : Polynomial R) (I : Ideal R) :
(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 (of f) I)) ((mk f) g)
source
noncomputable def PowerBasis.quotientEquivQuotientMinpolyMap {R : Type u_1} {S : Type u_2} [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)

Instances For

source
@[simp]
theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply {R : Type u_1} {S : Type u_2} [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✝)
source
@[simp]
theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply {R : Type u_1} {S : Type u_2} [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✝)
source
theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk {R : Type u_1} {S : Type u_2} [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)
source
theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk {R : Type u_1} {S : Type u_2} [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)
source
theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K : Type u_5} {L : Type u_6} [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`.