Mathlib.RingTheory.AdjoinRoot

AdjoinRoot definition

[CommRing R] (f : R[X]) : Type u

Full source

/-- 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`. -/
def AdjoinRoot [CommRing R] (f : R[X]) : Type u :=
  PolynomialPolynomial R ⧸ (span {f} : Ideal R[X])

Adjoining a root of a polynomial to a commutative ring

Informal description

Given a commutative ring $R$ and a polynomial $f \in R[X]$, the structure `AdjoinRoot f` represents the quotient ring $R[X]/(f)$, where $(f)$ is the principal ideal generated by $f$. This construction adjoins a root of $f$ to $R$.

AdjoinRoot.instCommRing instance

: CommRing (AdjoinRoot f)

Full source

instance instCommRing : CommRing (AdjoinRoot f) :=
  Ideal.Quotient.commRing _

Commutative Ring Structure on Adjoined Root

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ is a commutative ring.

AdjoinRoot.instInhabited instance

: Inhabited (AdjoinRoot f)

Full source

instance : Inhabited (AdjoinRoot f) :=
  ⟨0⟩

Inhabitedness of the Adjoined Root Ring

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ is inhabited (i.e., contains at least one element).

AdjoinRoot.instDecidableEq instance

: DecidableEq (AdjoinRoot f)

Full source

instance : DecidableEq (AdjoinRoot f) :=
  Classical.decEq _

Decidable Equality for Adjoined Roots of Polynomials

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ has decidable equality.

AdjoinRoot.nontrivial theorem

[IsDomain R] (h : degree f ≠ 0) : Nontrivial (AdjoinRoot f)

Full source

protected theorem nontrivial [IsDomain R] (h : degreedegree f ≠ 0) : Nontrivial (AdjoinRoot f) :=
  Ideal.Quotient.nontrivial
    (by
      simp_rw [Ne, span_singleton_eq_top, Polynomial.isUnit_iff, not_exists, not_and]
      rintro x hx rfl
      exact h (degree_C hx.ne_zero))

Nontriviality of Adjoined Root Ring for Nonconstant Polynomials

Informal description

Let $R$ be an integral domain and $f \in R[X]$ a polynomial of nonzero degree. Then the quotient ring $R[X]/(f)$ is nontrivial (i.e., contains more than one element).

AdjoinRoot.mk definition

: R[X] →+* AdjoinRoot f

Full source

/-- Ring homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`. -/
def mk : R[X]R[X] →+* AdjoinRoot f :=
  Ideal.Quotient.mk _

Quotient map from polynomials to adjoined root ring

Informal description

The natural ring homomorphism from the polynomial ring $ R[X] $ to the quotient ring $ R[X]/(f) $, which sends each polynomial $ p \in R[X] $ to its equivalence class modulo the principal ideal $ (f) $.

AdjoinRoot.induction_on theorem

{C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ p : R[X], C (mk f p)) : C x

Full source

@[elab_as_elim]
theorem induction_on {C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ p : R[X], C (mk f p)) :
    C x :=
  Quotient.inductionOn' x ih

Induction Principle for Adjoined Root Ring

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. For any property $C$ on the quotient ring $R[X]/(f)$ and any element $x \in R[X]/(f)$, if $C$ holds for the image of every polynomial $p \in R[X]$ under the quotient map $R[X] \to R[X]/(f)$, then $C$ holds for $x$.

AdjoinRoot.of definition

: R →+* AdjoinRoot f

Full source

/-- Embedding of the original ring `R` into `AdjoinRoot f`. -/
def of : R →+* AdjoinRoot f :=
  (mk f).comp C

Embedding of base ring into adjoined root ring

Informal description

The natural ring homomorphism from the commutative ring $R$ to the quotient ring $R[X]/(f)$, which sends each element $r \in R$ to the equivalence class of the constant polynomial $r$ modulo the principal ideal $(f)$. This embedding maps $R$ into the adjoined root ring.

AdjoinRoot.instSMulAdjoinRoot instance

[DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f)

Full source

instance instSMulAdjoinRoot [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
  Submodule.Quotient.instSMul' _

Scalar Multiplication on Adjoined Root Ring

Informal description

For any commutative ring $R$, polynomial $f \in R[X]$, and scalar multiplication structure $S$ on $R$ that is distributive and forms a scalar tower with $R$, the quotient ring $R[X]/(f)$ inherits a scalar multiplication operation from $S$.

AdjoinRoot.instDistribSMulOfIsScalarTower instance

[DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f)

Full source

instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
  Submodule.Quotient.distribSMul' _

Distributive Scalar Multiplication on Adjoined Root Ring

Informal description

For any commutative ring $R$, polynomial $f \in R[X]$, and scalar multiplication structure $S$ on $R$ that is distributive and forms a scalar tower with $R$, the quotient ring $R[X]/(f)$ inherits a distributive scalar multiplication operation from $S$.

AdjoinRoot.smul_mk theorem

[DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R[X]) : a • mk f x = mk f (a • x)

Full source

@[simp]
theorem smul_mk [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R[X]) :
    a • mk f x = mk f (a • x) :=
  rfl

Scalar Multiplication Commutes with Quotient Map in Adjoined Root Ring

Informal description

Let $R$ be a commutative ring, $f \in R[X]$ a polynomial, and $S$ a scalar multiplication structure on $R$ that is distributive and forms a scalar tower with $R$. Then for any scalar $a \in S$ and polynomial $x \in R[X]$, the scalar multiplication of $a$ with the equivalence class of $x$ in $R[X]/(f)$ is equal to the equivalence class of the scalar multiplication $a \cdot x$ in $R[X]/(f)$. In other words, $a \cdot [x] = [a \cdot x]$, where $[x]$ denotes the equivalence class of $x$ modulo $(f)$.

AdjoinRoot.smul_of theorem

[DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) : a • of f x = of f (a • x)

Full source

theorem smul_of [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) :
    a • of f x = of f (a • x) := by rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]

Scalar Multiplication Commutes with Base Ring Embedding in Adjoined Root Ring

Informal description

Let $R$ be a commutative ring, $f \in R[X]$ a polynomial, and $S$ a scalar multiplication structure on $R$ that is distributive and forms a scalar tower with $R$. Then for any scalar $a \in S$ and element $x \in R$, the scalar multiplication of $a$ with the image of $x$ under the natural embedding $R \to R[X]/(f)$ is equal to the image of the scalar multiplication $a \cdot x$ under the same embedding. In other words, $a \cdot \iota(x) = \iota(a \cdot x)$, where $\iota: R \to R[X]/(f)$ denotes the natural ring homomorphism.

AdjoinRoot.instIsScalarTower instance

 (R₁ R₂ : Type*) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R]
  [IsScalarTower R₁ R₂ R] (f : R[X]) : IsScalarTower R₁ R₂ (AdjoinRoot f)

Full source

instance (R₁ R₂ : Type*) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R]
    [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : R[X]) :
    IsScalarTower R₁ R₂ (AdjoinRoot f) :=
  Submodule.Quotient.isScalarTower _ _

Scalar Tower Structure on Adjoined Root Ring

Informal description

For any commutative ring $R$, polynomial $f \in R[X]$, and scalar multiplication structures $R₁$ and $R₂$ on $R$ that are distributive and form scalar towers with $R$, the quotient ring $R[X]/(f)$ inherits a scalar tower structure from $R₁$ and $R₂$. Specifically, for any $a \in R₁$, $b \in R₂$, and $x \in R[X]/(f)$, we have $(a \cdot b) \cdot x = a \cdot (b \cdot x)$.

AdjoinRoot.instSMulCommClass instance

 (R₁ R₂ : Type*) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R]
  [SMulCommClass R₁ R₂ R] (f : R[X]) : SMulCommClass R₁ R₂ (AdjoinRoot f)

Full source

instance (R₁ R₂ : Type*) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R]
    [IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R] (f : R[X]) :
    SMulCommClass R₁ R₂ (AdjoinRoot f) :=
  Submodule.Quotient.smulCommClass _ _

Commutativity of Scalar Multiplication on Adjoined Root Ring

Informal description

For any commutative ring $R$, polynomial $f \in R[X]$, and scalar multiplication structures $R₁$ and $R₂$ on $R$ that are distributive and form scalar towers with $R$, if the scalar multiplications $R₁$ and $R₂$ commute on $R$, then they also commute on the quotient ring $R[X]/(f)$. Specifically, for any $a \in R₁$, $b \in R₂$, and $x \in R[X]/(f)$, we have $a \cdot (b \cdot x) = b \cdot (a \cdot x)$.

AdjoinRoot.isScalarTower_right instance

[DistribSMul S R] [IsScalarTower S R R] : IsScalarTower S (AdjoinRoot f) (AdjoinRoot f)

Full source

instance isScalarTower_right [DistribSMul S R] [IsScalarTower S R R] :
    IsScalarTower S (AdjoinRoot f) (AdjoinRoot f) :=
  Ideal.Quotient.isScalarTower_right

Scalar Tower Structure on Adjoined Root Ring

Informal description

For any commutative ring $R$, polynomial $f \in R[X]$, and scalar multiplication structure $S$ on $R$ that is distributive and forms a scalar tower with $R$, the quotient ring $R[X]/(f)$ inherits a scalar tower structure from $S$. Specifically, for any $a \in S$ and $x, y \in R[X]/(f)$, we have $a \cdot (x + y) = a \cdot x + a \cdot y$.

AdjoinRoot.instDistribMulActionOfIsScalarTower instance

[Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (f : R[X]) : DistribMulAction S (AdjoinRoot f)

Full source

instance [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (f : R[X]) :
    DistribMulAction S (AdjoinRoot f) :=
  Submodule.Quotient.distribMulAction' _

Distributive Multiplicative Action on Adjoined Root

Informal description

For any monoid $S$ acting distributively on a commutative ring $R$ with the scalar tower property $S \to R \to R$, and any polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ inherits a distributive multiplicative action from $S$.

AdjoinRoot.instAlgebra instance

[CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f)

Full source

/-- `R[x]/(f)` is `R`-algebra -/
@[stacks 09FX "second part"]
instance [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f) :=
  Ideal.Quotient.algebra S

$S$-Algebra Structure on Adjoined Root

Informal description

For any commutative semiring $S$ and $S$-algebra $R$, the quotient ring $R[X]/(f)$ is naturally an $S$-algebra for any polynomial $f \in R[X]$.

AdjoinRoot.algebraMap_eq theorem

: algebraMap R (AdjoinRoot f) = of f

Full source

@[simp]
theorem algebraMap_eq : algebraMap R (AdjoinRoot f) = of f :=
  rfl

Equality of Algebra Map and Natural Homomorphism in Adjoined Root Construction

Informal description

The algebra map from the commutative ring $R$ to the quotient ring $R[X]/(f)$ coincides with the natural ring homomorphism $\text{of } f : R \to R[X]/(f)$. That is, $\text{algebraMap}_{R \to R[X]/(f)} = \text{of } f$.

AdjoinRoot.algebraMap_eq' theorem

[CommSemiring S] [Algebra S R] : algebraMap S (AdjoinRoot f) = (of f).comp (algebraMap S R)

Full source

theorem algebraMap_eq' [CommSemiring S] [Algebra S R] :
    algebraMap S (AdjoinRoot f) = (of f).comp (algebraMap S R) :=
  rfl

Compatibility of Algebra Maps in Adjoined Root Construction

Informal description

Let $S$ be a commutative semiring and $R$ an $S$-algebra. For any polynomial $f \in R[X]$, the algebra map from $S$ to the quotient ring $R[X]/(f)$ is equal to the composition of the embedding $\text{of } f : R \to R[X]/(f)$ with the algebra map from $S$ to $R$. That is, the following diagram commutes: \[ \text{algebraMap}_{S \to R[X]/(f)} = (\text{of } f) \circ \text{algebraMap}_{S \to R} \]

AdjoinRoot.finiteType theorem

: Algebra.FiniteType R (AdjoinRoot f)

Full source

theorem finiteType : Algebra.FiniteType R (AdjoinRoot f) :=
  (Algebra.FiniteType.polynomial R).of_surjective _ (Ideal.Quotient.mkₐ_surjective R _)

Finite Generation of Adjoined Root Algebra

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ is finitely generated as an $R$-algebra.

AdjoinRoot.finitePresentation theorem

: Algebra.FinitePresentation R (AdjoinRoot f)

Full source

theorem finitePresentation : Algebra.FinitePresentation R (AdjoinRoot f) :=
  (Algebra.FinitePresentation.polynomial R).quotient (Submodule.fg_span_singleton f)

Finite Presentation of Adjoined Root Algebra

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ is finitely presented as an $R$-algebra.

AdjoinRoot.root definition

: AdjoinRoot f

Full source

/-- The adjoined root. -/
def root : AdjoinRoot f :=
  mk f X

Adjoined root of a polynomial

Informal description

The element `root f` in the ring `AdjoinRoot f` is the image of the polynomial variable $X$ under the quotient map $R[X] \to R[X]/(f)$. In other words, it represents the adjoined root of the polynomial $f$ in the quotient ring.

AdjoinRoot.hasCoeT instance

: CoeTC R (AdjoinRoot f)

Full source

instance hasCoeT : CoeTC R (AdjoinRoot f) :=
  ⟨of f⟩

Canonical Embedding of Base Ring into Adjoined Root Ring

Informal description

For any commutative ring $R$ and polynomial $f \in R[X]$, there is a canonical embedding of $R$ into the quotient ring $R[X]/(f)$, where each element $r \in R$ is mapped to the equivalence class of the constant polynomial $r$ modulo the principal ideal $(f)$.

AdjoinRoot.algHom_ext theorem

[Semiring S] [Algebra R S] {g₁ g₂ : AdjoinRoot f →ₐ[R] S} (h : g₁ (root f) = g₂ (root f)) : g₁ = g₂

Full source

/-- Two `R`-`AlgHom` from `AdjoinRoot f` to the same `R`-algebra are the same iff
    they agree on `root f`. -/
@[ext]
theorem algHom_ext [Semiring S] [Algebra R S] {g₁ g₂ : AdjoinRootAdjoinRoot f →ₐ[R] S}
    (h : g₁ (root f) = g₂ (root f)) : g₁ = g₂ :=
  Ideal.Quotient.algHom_ext R <| Polynomial.algHom_ext h

Uniqueness of Algebra Homomorphisms from Adjoined Root via Root Agreement

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. For any $R$-algebra $S$ and any two $R$-algebra homomorphisms $g_1, g_2 \colon R[X]/(f) \to S$, if $g_1$ and $g_2$ agree on the adjoined root $\text{root}\, f$, then $g_1 = g_2$.

AdjoinRoot.mk_eq_mk theorem

{g h : R[X]} : mk f g = mk f h ↔ f ∣ g - h

Full source

@[simp]
theorem mk_eq_mk {g h : R[X]} : mkmk f g = mk f h ↔ f ∣ g - h :=
  Ideal.Quotient.eq.trans Ideal.mem_span_singleton

Equality in Quotient Ring via Polynomial Divisibility

Informal description

For any polynomials $g, h \in R[X]$, the equivalence classes of $g$ and $h$ in the quotient ring $R[X]/(f)$ are equal if and only if $f$ divides $g - h$ in $R[X]$. In other words, $\overline{g} = \overline{h} \iff f \mid (g - h)$.

AdjoinRoot.mk_eq_zero theorem

{g : R[X]} : mk f g = 0 ↔ f ∣ g

Full source

@[simp]
theorem mk_eq_zero {g : R[X]} : mkmk f g = 0 ↔ f ∣ g :=
  mk_eq_mk.trans <| by rw [sub_zero]

Vanishing Criterion in Quotient Ring via Divisibility

Informal description

For any polynomial $g \in R[X]$, the equivalence class of $g$ in the quotient ring $R[X]/(f)$ is zero if and only if $f$ divides $g$ in $R[X]$. In other words, $\overline{g} = 0 \iff f \mid g$.

AdjoinRoot.mk_self theorem

: mk f f = 0

Full source

@[simp]
theorem mk_self : mk f f = 0 :=
  Quotient.sound' <| QuotientAddGroup.leftRel_apply.mpr (mem_span_singleton.2 <| by simp)

Vanishing of Polynomial in its Own Quotient Ring

Informal description

The equivalence class of the polynomial $f$ in the quotient ring $R[X]/(f)$ is equal to zero, i.e., $\overline{f} = 0$.

AdjoinRoot.mk_C theorem

(x : R) : mk f (C x) = x

Full source

@[simp]
theorem mk_C (x : R) : mk f (C x) = x :=
  rfl

Image of Constant Polynomial in Quotient Ring Equals Original Element

Informal description

For any element $x \in R$, the equivalence class of the constant polynomial $C(x)$ in the quotient ring $R[X]/(f)$ is equal to $x$ under the natural embedding of $R$ into $R[X]/(f)$. In other words, $\overline{C(x)} = x$ where $\overline{C(x)}$ denotes the equivalence class of $C(x)$ modulo $(f)$.

AdjoinRoot.mk_X theorem

: mk f X = root f

Full source

@[simp]
theorem mk_X : mk f X = root f :=
  rfl

Image of $X$ in $R[X]/(f)$ is the Adjoined Root

Informal description

The image of the polynomial variable $X$ under the quotient map $R[X] \to R[X]/(f)$ is equal to the adjoined root $\text{root}(f)$ in the quotient ring $R[X]/(f)$. In other words, $\overline{X} = \text{root}(f)$ where $\overline{X}$ denotes the equivalence class of $X$ modulo $(f)$.

AdjoinRoot.mk_ne_zero_of_degree_lt theorem

(hf : Monic f) {g : R[X]} (h0 : g ≠ 0) (hd : degree g < degree f) : mk f g ≠ 0

Full source

theorem mk_ne_zero_of_degree_lt (hf : Monic f) {g : R[X]} (h0 : g ≠ 0) (hd : degree g < degree f) :
    mkmk f g ≠ 0 :=
  mk_eq_zero.not.2 <| hf.not_dvd_of_degree_lt h0 hd

Non-vanishing of polynomials with degree less than monic generator in quotient ring

Informal description

Let $f \in R[X]$ be a monic polynomial and $g \in R[X]$ be a nonzero polynomial such that $\deg g < \deg f$. Then the equivalence class of $g$ in the quotient ring $R[X]/(f)$ is nonzero, i.e., $\overline{g} \neq 0$.

AdjoinRoot.mk_ne_zero_of_natDegree_lt theorem

(hf : Monic f) {g : R[X]} (h0 : g ≠ 0) (hd : natDegree g < natDegree f) : mk f g ≠ 0

Full source

theorem mk_ne_zero_of_natDegree_lt (hf : Monic f) {g : R[X]} (h0 : g ≠ 0)
    (hd : natDegree g < natDegree f) : mkmk f g ≠ 0 :=
  mk_eq_zero.not.2 <| hf.not_dvd_of_natDegree_lt h0 hd

Non-vanishing of polynomials of lower degree in $R[X]/(f)$

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a monic polynomial. For any nonzero polynomial $g \in R[X]$ such that the natural degree of $g$ is less than the natural degree of $f$, the equivalence class of $g$ in the quotient ring $R[X]/(f)$ is nonzero, i.e., $\overline{g} \neq 0$.

AdjoinRoot.aeval_eq theorem

(p : R[X]) : aeval (root f) p = mk f p

Full source

@[simp]
theorem aeval_eq (p : R[X]) : aeval (root f) p = mk f p :=
  Polynomial.induction_on p
    (fun x => by
      rw [aeval_C]
      rfl)
    (fun p q ihp ihq => by rw [map_add, RingHom.map_add, ihp, ihq]) fun n x _ => by
    rw [map_mul, aeval_C, map_pow, aeval_X, RingHom.map_mul, mk_C, RingHom.map_pow, mk_X]
    rfl

Evaluation at Adjoined Root Equals Quotient Map

Informal description

For any polynomial $p \in R[X]$, the evaluation of $p$ at the adjoined root $\text{root}(f)$ via the algebra homomorphism $\text{aeval}$ is equal to the equivalence class of $p$ in the quotient ring $R[X]/(f)$. In other words, $\text{aeval}(\text{root}(f), p) = \overline{p}$ where $\overline{p}$ denotes the image of $p$ under the quotient map $R[X] \to R[X]/(f)$.

AdjoinRoot.adjoinRoot_eq_top theorem

: Algebra.adjoin R ({root f} : Set (AdjoinRoot f)) = ⊤

Full source

theorem adjoinRoot_eq_top : Algebra.adjoin R ({root f} : Set (AdjoinRoot f)) = ⊤ := by
  refine Algebra.eq_top_iff.2 fun x => ?_
  induction x using AdjoinRoot.induction_on with
    | ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

Adjoined Root Generates the Quotient Ring $R[X]/(f)$

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. The $R$-algebra generated by the adjoined root $\text{root}(f)$ in the quotient ring $R[X]/(f)$ is equal to the entire ring $R[X]/(f)$. In other words, $\text{Algebra.adjoin}_R(\{\text{root}(f)\}) = R[X]/(f)$.

AdjoinRoot.eval₂_root theorem

(f : R[X]) : f.eval₂ (of f) (root f) = 0

Full source

@[simp]
theorem eval₂_root (f : R[X]) : f.eval₂ (of f) (root f) = 0 := by
  rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]

Adjoined Root Satisfies the Polynomial Equation: $f(\text{root}(f)) = 0$

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. The evaluation of $f$ at the adjoined root $\text{root}(f)$ via the ring homomorphism $\text{of } f : R \to R[X]/(f)$ is zero, i.e., $f(\text{root}(f)) = 0$ in $R[X]/(f)$.

AdjoinRoot.isRoot_root theorem

(f : R[X]) : IsRoot (f.map (of f)) (root f)

Full source

theorem isRoot_root (f : R[X]) : IsRoot (f.map (of f)) (root f) := by
  rw [IsRoot, eval_map, eval₂_root]

Adjoined Root is a Root of the Polynomial

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. The adjoined root $\text{root}(f)$ in the quotient ring $R[X]/(f)$ is a root of the polynomial $f$ when mapped through the natural ring homomorphism $\text{of } f : R \to R[X]/(f)$. That is, $f(\text{root}(f)) = 0$ in $R[X]/(f)$.

AdjoinRoot.isAlgebraic_root theorem

(hf : f ≠ 0) : IsAlgebraic R (root f)

Full source

theorem isAlgebraic_root (hf : f ≠ 0) : IsAlgebraic R (root f) :=
  ⟨f, hf, eval₂_root f⟩

Algebraicity of Adjoined Root for Nonzero Polynomials

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a nonzero polynomial. Then the adjoined root $\text{root}(f)$ in the ring $R[X]/(f)$ is algebraic over $R$, meaning there exists a nonzero polynomial $g \in R[X]$ such that $g(\text{root}(f)) = 0$.

AdjoinRoot.of.injective_of_degree_ne_zero theorem

[IsDomain R] (hf : f.degree ≠ 0) : Function.Injective (AdjoinRoot.of f)

Full source

theorem of.injective_of_degree_ne_zero [IsDomain R] (hf : f.degree ≠ 0) :
    Function.Injective (AdjoinRoot.of f) := by
  rw [injective_iff_map_eq_zero]
  intro p hp
  rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp
  by_cases h : f = 0
  · exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))
  · contrapose! hf with h_contra
    rw [← degree_C h_contra]
    apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _
    rwa [degree_C h_contra, zero_le_degree_iff]

Injectivity of Base Ring Embedding in Adjoined Root Ring for Non-Constant Polynomials

Informal description

Let $R$ be an integral domain and $f \in R[X]$ a polynomial with $\deg(f) \neq 0$. Then the natural ring homomorphism $R \to R[X]/(f)$ is injective.

AdjoinRoot.lift definition

(i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : AdjoinRoot f →+* S

Full source

/-- Lift a ring homomorphism `i : R →+* S` to `AdjoinRoot f →+* S`. -/
def lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : AdjoinRootAdjoinRoot f →+* S := by
  apply Ideal.Quotient.lift _ (eval₂RingHom i x)
  intro g H
  rcases mem_span_singleton.1 H with ⟨y, hy⟩
  rw [hy, RingHom.map_mul, coe_eval₂RingHom, h, zero_mul]

Lifting of ring homomorphism to adjoined root

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, and a ring homomorphism $i: R \to S$, for any element $x \in S$ satisfying $f(i)(x) = 0$, there exists a unique ring homomorphism $\text{AdjoinRoot}\, f \to S$ extending $i$ and mapping the root of $f$ in $\text{AdjoinRoot}\, f$ to $x$.

AdjoinRoot.lift_mk theorem

(g : R[X]) : lift i a h (mk f g) = g.eval₂ i a

Full source

@[simp]
theorem lift_mk (g : R[X]) : lift i a h (mk f g) = g.eval₂ i a :=
  Ideal.Quotient.lift_mk _ _ _

Evaluation of Lift Homomorphism on Quotient Polynomial

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. Given a ring homomorphism $i: R \to S$, an element $a \in S$ satisfying $f(i)(a) = 0$, and any polynomial $g \in R[X]$, the lift homomorphism $\text{lift}\, i\, a\, h$ applied to the image of $g$ in $\text{AdjoinRoot}\, f$ equals the evaluation of $g$ at $a$ via $i$, i.e., \[ \text{lift}\, i\, a\, h\, (\text{mk}\, f\, g) = g.eval₂\, i\, a. \]

AdjoinRoot.lift_root theorem

: lift i a h (root f) = a

Full source

@[simp]
theorem lift_root : lift i a h (root f) = a := by rw [root, lift_mk, eval₂_X]

Lift Homomorphism Maps Adjoined Root to Given Root

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, a ring homomorphism $i: R \to S$, and an element $a \in S$ satisfying $f(i)(a) = 0$, the lift homomorphism $\text{lift}\, i\, a\, h$ maps the adjoined root $\text{root}\, f$ in $\text{AdjoinRoot}\, f$ to $a$, i.e., \[ \text{lift}\, i\, a\, h\, (\text{root}\, f) = a. \]

AdjoinRoot.lift_of theorem

{x : R} : lift i a h x = i x

Full source

@[simp]
theorem lift_of {x : R} : lift i a h x = i x := by rw [← mk_C x, lift_mk, eval₂_C]

Lift Homomorphism Commutes with Base Ring Embedding

Informal description

For any element $x \in R$, the lift homomorphism $\text{lift}\, i\, a\, h$ applied to $x$ (via the natural embedding $\text{of}\, f$) equals the image of $x$ under the ring homomorphism $i: R \to S$, i.e., \[ \text{lift}\, i\, a\, h\, (x) = i(x). \]

AdjoinRoot.lift_comp_of theorem

: (lift i a h).comp (of f) = i

Full source

@[simp]
theorem lift_comp_of : (lift i a h).comp (of f) = i :=
  RingHom.ext fun _ => @lift_of _ _ _ _ _ _ _ h _

Composition of Lift Homomorphism with Base Embedding Equals Original Homomorphism

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, a ring homomorphism $i: R \to S$, and an element $a \in S$ satisfying $f(i)(a) = 0$, the composition of the lift homomorphism $\text{lift}\, i\, a\, h$ with the natural embedding $\text{of}\, f$ equals $i$, i.e., \[ (\text{lift}\, i\, a\, h) \circ (\text{of}\, f) = i. \]

AdjoinRoot.liftHom definition

(x : S) (hfx : aeval x f = 0) : AdjoinRoot f →ₐ[R] S

Full source

/-- Produce an algebra homomorphism `AdjoinRoot f →ₐ[R] S` sending `root f` to
a root of `f` in `S`. -/
def liftHom (x : S) (hfx : aeval x f = 0) : AdjoinRootAdjoinRoot f →ₐ[R] S :=
  { lift (algebraMap R S) x hfx with
    commutes' := fun r => show lift _ _ hfx r = _ from lift_of hfx }

Lifting of algebra homomorphism to adjoined root

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, and an $R$-algebra $S$, for any element $x \in S$ satisfying $f(x) = 0$ (where $f$ is evaluated in $S$ via the algebra map), there exists a unique $R$-algebra homomorphism $\text{AdjoinRoot}\, f \to S$ extending the canonical algebra map $R \to S$ and mapping the root of $f$ in $\text{AdjoinRoot}\, f$ to $x$.

AdjoinRoot.coe_liftHom theorem

(x : S) (hfx : aeval x f = 0) : (liftHom f x hfx : AdjoinRoot f →+* S) = lift (algebraMap R S) x hfx

Full source

@[simp]
theorem coe_liftHom (x : S) (hfx : aeval x f = 0) :
    (liftHom f x hfx : AdjoinRootAdjoinRoot f →+* S) = lift (algebraMap R S) x hfx :=
  rfl

Underlying Ring Homomorphism of Lifted Algebra Homomorphism Equals Lifted Ring Homomorphism

Informal description

Let $R$ be a commutative ring, $f \in R[X]$ a polynomial, and $S$ an $R$-algebra. For any $x \in S$ satisfying $f(x) = 0$ (where $f$ is evaluated in $S$ via the algebra map $R \to S$), the underlying ring homomorphism of the algebra homomorphism $\text{liftHom}_f(x, h_{fx}) : \text{AdjoinRoot}\, f \to S$ is equal to $\text{lift}_f(\text{algebraMap}\, R\, S, x, h_{fx})$.

AdjoinRoot.aeval_algHom_eq_zero theorem

(ϕ : AdjoinRoot f →ₐ[R] S) : aeval (ϕ (root f)) f = 0

Full source

@[simp]
theorem aeval_algHom_eq_zero (ϕ : AdjoinRootAdjoinRoot f →ₐ[R] S) : aeval (ϕ (root f)) f = 0 := by
  have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
  rw [aeval_def, ← h, ← RingHom.map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]
  rfl

Adjoined Root Satisfies Polynomial Equation under Algebra Homomorphism

Informal description

For any $R$-algebra homomorphism $\phi : R[X]/(f) \to S$, the evaluation of the polynomial $f$ at $\phi(\text{root}(f))$ is zero, i.e., $f(\phi(\text{root}(f))) = 0$.

AdjoinRoot.liftHom_eq_algHom theorem

(f : R[X]) (ϕ : AdjoinRoot f →ₐ[R] S) : liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ) = ϕ

Full source

@[simp]
theorem liftHom_eq_algHom (f : R[X]) (ϕ : AdjoinRootAdjoinRoot f →ₐ[R] S) :
    liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ) = ϕ := by
  suffices AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ)) = ⊤ by
    exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm
  rw [eq_top_iff, ← adjoinRoot_eq_top, Algebra.adjoin_le_iff, Set.singleton_subset_iff]
  exact (@lift_root _ _ _ _ _ _ _ (aeval_algHom_eq_zero f ϕ)).symm

Uniqueness of Algebra Homomorphism from Adjoined Root: $\text{liftHom}_f(\phi(\text{root}\, f), h) = \phi$

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. For any $R$-algebra homomorphism $\phi: R[X]/(f) \to S$, the algebra homomorphism $\text{liftHom}_f(\phi(\text{root}\, f), h)$ (where $h$ is the proof that $\phi(\text{root}\, f)$ is a root of $f$ in $S$) equals $\phi$.

AdjoinRoot.liftHom_mk theorem

{g : R[X]} : liftHom f a hfx (mk f g) = aeval a g

Full source

@[simp]
theorem liftHom_mk {g : R[X]} : liftHom f a hfx (mk f g) = aeval a g :=
  lift_mk hfx g

Evaluation of Lift Homomorphism on Quotient Polynomial

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ a polynomial. Given an $R$-algebra $S$, an element $a \in S$ satisfying $f(a) = 0$, and any polynomial $g \in R[X]$, the algebra homomorphism $\text{liftHom}_f(a, h_{fx})$ applied to the image of $g$ in $R[X]/(f)$ equals the evaluation of $g$ at $a$, i.e., \[ \text{liftHom}_f(a, h_{fx})(\overline{g}) = g(a). \]

AdjoinRoot.liftHom_root theorem

: liftHom f a hfx (root f) = a

Full source

@[simp]
theorem liftHom_root : liftHom f a hfx (root f) = a :=
  lift_root hfx

Lift Homomorphism Maps Adjoined Root to Given Root

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, an $R$-algebra $S$, and an element $a \in S$ such that $f(a) = 0$, the algebra homomorphism $\text{liftHom}_f(a, h_{fx})$ maps the adjoined root $\text{root}\, f$ in $\text{AdjoinRoot}\, f$ to $a$, i.e., \[ \text{liftHom}_f(a, h_{fx})(\text{root}\, f) = a. \]

AdjoinRoot.liftHom_of theorem

{x : R} : liftHom f a hfx (of f x) = algebraMap _ _ x

Full source

@[simp]
theorem liftHom_of {x : R} : liftHom f a hfx (of f x) = algebraMap _ _ x :=
  lift_of hfx

Lift Homomorphism Commutes with Base Ring Embedding in Adjoined Root

Informal description

For any element $x \in R$, the algebra homomorphism $\text{liftHom}_f(a, h_{fx})$ applied to the image of $x$ under the natural embedding $\text{of}\, f : R \to \text{AdjoinRoot}\, f$ equals the image of $x$ under the canonical algebra map $R \to S$, i.e., \[ \text{liftHom}_f(a, h_{fx})(\text{of}\, f\, x) = \text{algebraMap}\, R\, S\, x. \]

AdjoinRoot.root_isInv theorem

(r : R) : of _ r * root (C r * X - 1) = 1

Full source

@[simp]
theorem root_isInv (r : R) : of _ r * root (C r * X - 1) = 1 := by
  convert sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1) <;>
    simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

Multiplicative Inverse of Adjoined Root for Linear Polynomial $rX - 1$

Informal description

Let $R$ be a commutative ring and let $r \in R$. In the ring $R[X]/(rX - 1)$, the product of the image of $r$ under the natural embedding $\text{of}\, (rX - 1) : R \to R[X]/(rX - 1)$ and the adjoined root $\text{root}\, (rX - 1)$ equals the multiplicative identity $1$. In other words, the element $\overline{r} \cdot \alpha = 1$ in $R[X]/(rX - 1)$, where $\overline{r}$ is the image of $r$ and $\alpha$ is the root of the polynomial $rX - 1$ in the quotient ring.

AdjoinRoot.algHom_subsingleton theorem

{S : Type*} [CommRing S] [Algebra R S] {r : R} : Subsingleton (AdjoinRoot (C r * X - 1) →ₐ[R] S)

Full source

theorem algHom_subsingleton {S : Type*} [CommRing S] [Algebra R S] {r : R} :
    Subsingleton (AdjoinRootAdjoinRoot (C r * X - 1) →ₐ[R] S) :=
  ⟨fun f g =>
    algHom_ext
      (@inv_unique _ _ (algebraMap R S r) _ _
        (by rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one])
        (by rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]))⟩

Uniqueness of Algebra Homomorphisms from $R[X]/(rX - 1)$ to $S$

Informal description

Let $R$ be a commutative ring and $S$ a commutative $R$-algebra. For any element $r \in R$, the set of $R$-algebra homomorphisms from the quotient ring $R[X]/(rX - 1)$ to $S$ has at most one element. In other words, there is at most one $R$-algebra homomorphism $\phi \colon R[X]/(rX - 1) \to S$.

AdjoinRoot.isDomain_of_prime theorem

(hf : Prime f) : IsDomain (AdjoinRoot f)

Full source

theorem isDomain_of_prime (hf : Prime f) : IsDomain (AdjoinRoot f) :=
  (Ideal.Quotient.isDomain_iff_prime (span {f} : Ideal R[X])).mpr <|
    (Ideal.span_singleton_prime hf.ne_zero).mpr hf

Quotient Ring by Prime Polynomial is Integral Domain

Informal description

Let $R$ be a commutative ring and $f \in R[X]$ be a prime polynomial. Then the quotient ring $R[X]/(f)$ is an integral domain.

AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero theorem

[IsDomain R] (hf : Prime f) (hf' : f.degree ≠ 0) : NoZeroSMulDivisors R (AdjoinRoot f)

Full source

theorem noZeroSMulDivisors_of_prime_of_degree_ne_zero [IsDomain R] (hf : Prime f)
    (hf' : f.degree ≠ 0) : NoZeroSMulDivisors R (AdjoinRoot f) :=
  haveI := isDomain_of_prime hf
  NoZeroSMulDivisors.iff_algebraMap_injective.mpr (of.injective_of_degree_ne_zero hf')

No Zero Divisors in Adjoined Root Ring for Prime Polynomials of Nonzero Degree

Informal description

Let $R$ be an integral domain and $f \in R[X]$ be a prime polynomial with $\deg(f) \neq 0$. Then the quotient ring $R[X]/(f)$ has no zero divisors when considered as an $R$-module, meaning that for any $r \in R$ and $g \in R[X]/(f)$, if $r \cdot g = 0$ then either $r = 0$ or $g = 0$.

AdjoinRoot.span_maximal_of_irreducible instance

[Fact (Irreducible f)] : (span { f }).IsMaximal

Full source

instance span_maximal_of_irreducible [Fact (Irreducible f)] : (span {f}).IsMaximal :=
  PrincipalIdealRing.isMaximal_of_irreducible <| Fact.out

Maximality of the Ideal Generated by an Irreducible Polynomial

Informal description

For any irreducible polynomial $f$ over a commutative ring $R$, the ideal $\langle f \rangle$ in $R[X]$ is maximal.

AdjoinRoot.instGroupWithZero instance

[Fact (Irreducible f)] : GroupWithZero (AdjoinRoot f)

Full source

noncomputable instance instGroupWithZero [Fact (Irreducible f)] : GroupWithZero (AdjoinRoot f) :=
  Quotient.groupWithZero (span {f} : Ideal K[X])

Group with Zero Structure on Adjoined Root of Irreducible Polynomial

Informal description

For any irreducible polynomial $f$ over a commutative ring $R$, the quotient ring $R[X]/(f)$ is a group with zero.

AdjoinRoot.instField instance

[Fact (Irreducible f)] : Field (AdjoinRoot f)

Full source

/-- If `R` is a field and `f` is irreducible, then `AdjoinRoot f` is a field -/
@[stacks 09FX "first part, see also 09FI"]
noncomputable instance instField [Fact (Irreducible f)] : Field (AdjoinRoot f) where
  __ := instCommRing _
  __ := instGroupWithZero
  nnqsmul := (· • ·)
  qsmul := (· • ·)
  nnratCast_def q := by
    rw [← map_natCast (of f), ← map_natCast (of f), ← map_div₀, ← NNRat.cast_def]; rfl
  ratCast_def q := by
    rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]; rfl
  nnqsmul_def q x :=
    AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by
      simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.nnqsmul_eq_C_mul]
  qsmul_def q x :=
    -- Porting note: I gave the explicit motive and changed `rw` to `simp`.
    AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by
      simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.qsmul_eq_C_mul]

Field Structure on Adjoined Root of Irreducible Polynomial

Informal description

For any field $K$ and irreducible polynomial $f \in K[X]$, the quotient ring $K[X]/(f)$ is a field.

AdjoinRoot.coe_injective theorem

(h : degree f ≠ 0) : Function.Injective ((↑) : K → AdjoinRoot f)

Full source

theorem coe_injective (h : degreedegree f ≠ 0) : Function.Injective ((↑) : K → AdjoinRoot f) :=
  have := AdjoinRoot.nontrivial f h
  (of f).injective

Injectivity of the Canonical Embedding into the Adjoined Root Ring for Nonconstant Polynomials

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial of nonzero degree. Then the canonical embedding $K \hookrightarrow K[X]/(f)$ is injective.

AdjoinRoot.coe_injective' theorem

[Fact (Irreducible f)] : Function.Injective ((↑) : K → AdjoinRoot f)

Full source

theorem coe_injective' [Fact (Irreducible f)] : Function.Injective ((↑) : K → AdjoinRoot f) :=
  (of f).injective

Injectivity of Canonical Embedding for Adjoined Root of Irreducible Polynomial

Informal description

For any field $K$ and irreducible polynomial $f \in K[X]$, the canonical embedding $K \hookrightarrow K[X]/(f)$ is injective.

AdjoinRoot.mul_div_root_cancel theorem

[Fact (Irreducible f)] : (X - C (root f)) * ((f.map (of f)) / (X - C (root f))) = f.map (of f)

Full source

theorem mul_div_root_cancel [Fact (Irreducible f)] :
    (X - C (root f)) * ((f.map (of f)) / (X - C (root f))) = f.map (of f) :=
  mul_div_eq_iff_isRoot.2 <| isRoot_root _

Factorization of Polynomial in Adjoined Root Ring: $(X - \alpha) \cdot (f/(X - \alpha)) = f$

Informal description

Let $K$ be a field and $f \in K[X]$ an irreducible polynomial. In the quotient ring $K[X]/(f)$, the polynomial $f$ (mapped via the natural homomorphism) factors as $(X - \text{root}(f))$ times the quotient of $f$ divided by $(X - \text{root}(f))$, i.e., $$(X - C(\text{root}(f))) \cdot \left(\frac{f \text{ (mapped)}}{X - C(\text{root}(f))}\right) = f \text{ (mapped)}.$$

AdjoinRoot.instIsNoetherianRing instance

[CommRing R] [IsNoetherianRing R] {f : R[X]} : IsNoetherianRing (AdjoinRoot f)

Full source

instance [CommRing R] [IsNoetherianRing R] {f : R[X]} : IsNoetherianRing (AdjoinRoot f) :=
  Ideal.Quotient.isNoetherianRing _

Noetherian Property of Adjoined Root Rings

Informal description

For any commutative ring $R$ that is Noetherian and any polynomial $f \in R[X]$, the quotient ring $R[X]/(f)$ is also Noetherian.

AdjoinRoot.isIntegral_root' theorem

(hg : g.Monic) : IsIntegral R (root g)

Full source

theorem isIntegral_root' (hg : g.Monic) : IsIntegral R (root g) :=
  ⟨g, hg, eval₂_root g⟩

Integrality of Adjoined Root for Monic Polynomials

Informal description

Let $R$ be a commutative ring and $g \in R[X]$ a monic polynomial. The adjoined root $\text{root}(g)$ in the quotient ring $R[X]/(g)$ is integral over $R$.

AdjoinRoot.modByMonicHom definition

(hg : g.Monic) : AdjoinRoot g →ₗ[R] R[X]

Full source

/-- `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`. -/
def modByMonicHom (hg : g.Monic) : AdjoinRootAdjoinRoot g →ₗ[R] R[X] :=
  (Submodule.liftQ _ (Polynomial.modByMonicHom g)
        fun f (hf : f ∈ (Ideal.span {g}).restrictScalars R) =>
        (mem_ker_modByMonic hg).mpr (Ideal.mem_span_singleton.mp hf)).comp <|
    (Submodule.Quotient.restrictScalarsEquiv R (Ideal.span {g} : Ideal R[X])).symm.toLinearMap

Modular projection homomorphism for monic polynomials

Informal description

Given a monic polynomial $g \in R[X]$, the function `AdjoinRoot.modByMonicHom hg` maps an equivalence class $[f]$ in the quotient ring $R[X]/(g)$ to the remainder $f \mod g$ in $R[X]$. This is a well-defined right inverse to the natural projection map `AdjoinRoot.mk g : R[X] → R[X]/(g)`.

AdjoinRoot.modByMonicHom_mk theorem

(hg : g.Monic) (f : R[X]) : modByMonicHom hg (mk g f) = f %ₘ g

Full source

@[simp]
theorem modByMonicHom_mk (hg : g.Monic) (f : R[X]) : modByMonicHom hg (mk g f) = f %ₘ g :=
  rfl

Modular Projection Homomorphism Maps Equivalence Class to Remainder

Informal description

Let $R$ be a commutative ring and $g \in R[X]$ a monic polynomial. For any polynomial $f \in R[X]$, the modular projection homomorphism $\operatorname{modByMonicHom}_{hg}$ applied to the equivalence class $[f]$ in $R[X]/(g)$ equals the remainder $f \mod g$ in $R[X]$.

AdjoinRoot.mk_leftInverse theorem

(hg : g.Monic) : Function.LeftInverse (mk g) (modByMonicHom hg)

Full source

theorem mk_leftInverse (hg : g.Monic) : Function.LeftInverse (mk g) (modByMonicHom hg) := by
  intro f
  induction f using AdjoinRoot.induction_on
  rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel_left,
    dvd_neg]
  apply dvd_mul_right

Quotient Map is Left Inverse of Modular Projection for Monic Polynomials

Informal description

Let $R$ be a commutative ring and $g \in R[X]$ a monic polynomial. Then the quotient map $\operatorname{mk}_g : R[X] \to R[X]/(g)$ is a left inverse of the modular projection homomorphism $\operatorname{modByMonicHom}_{hg} : R[X]/(g) \to R[X]$. That is, for any equivalence class $[f] \in R[X]/(g)$, we have $\operatorname{mk}_g(\operatorname{modByMonicHom}_{hg}([f])) = [f]$.

AdjoinRoot.mk_surjective theorem

: Function.Surjective (mk g)

Full source

theorem mk_surjective : Function.Surjective (mk g) :=
  Ideal.Quotient.mk_surjective

Surjectivity of the Quotient Map to Adjoined Root Ring

Informal description

The natural ring homomorphism $\operatorname{mk}_g : R[X] \to R[X]/(g)$ is surjective, meaning that for every element $y$ in the quotient ring $R[X]/(g)$, there exists a polynomial $f \in R[X]$ such that $\operatorname{mk}_g(f) = y$.

AdjoinRoot.powerBasisAux' definition

(hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g)

Full source

/-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`. -/
def powerBasisAux' (hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g) :=
  Basis.ofEquivFun
    { toFun := fun f i => (modByMonicHom hg f).coeff i
      invFun := fun c => mk g <| ∑ i : Fin g.natDegree, monomial i (c i)
      map_add' := fun f₁ f₂ =>
        funext fun i => by simp only [(modByMonicHom hg).map_add, coeff_add, Pi.add_apply]
      map_smul' := fun f₁ f₂ =>
        funext fun i => by
          simp only [(modByMonicHom hg).map_smul, coeff_smul, Pi.smul_apply, RingHom.id_apply]
      -- Porting note: another proof that I converted to tactic mode
      left_inv := by
        intro f
        induction f using AdjoinRoot.induction_on
        simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]
        refine (mk_eq_mk.mpr ?_).symm
        rw [modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel]
        exact dvd_mul_right _ _
      right_inv := fun x =>
        funext fun i => by
          nontriviality R
          simp only [modByMonicHom_mk]
          rw [(modByMonic_eq_self_iff hg).mpr, finset_sum_coeff]
          · simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
          · simp_rw [← C_mul_X_pow_eq_monomial]
            exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _ }

Basis of powers of root for adjoined root ring

Informal description

Given a monic polynomial $ g \in R[X] $ of degree $ d $, the set $\{1, \text{root}(g), \ldots, \text{root}(g)^{d-1}\}$ forms a basis for the $ R $-module $ R[X]/(g) $, where $ \text{root}(g) $ denotes the image of $ X $ in the quotient ring $ R[X]/(g) $. More precisely, the basis is indexed by $ \text{Fin}(d) $, and the representation of an element $ f \in R[X]/(g) $ in this basis is given by the coefficients of the remainder when $ f $ is divided by $ g $.

AdjoinRoot.powerBasisAux'_repr_symm_apply theorem

 (hg : g.Monic) (c : Fin g.natDegree →₀ R) : (powerBasisAux' hg).repr.symm c = mk g (∑ i : Fin _, monomial i (c i))

Full source

theorem powerBasisAux'_repr_symm_apply (hg : g.Monic) (c : FinFin g.natDegree →₀ R) :
    (powerBasisAux' hg).repr.symm c = mk g (∑ i : Fin _, monomial i (c i)) :=
  rfl

Inverse Basis Representation for Adjoined Root Ring

Informal description

Let $R$ be a commutative ring and $g \in R[X]$ a monic polynomial of degree $d$. For any finitely supported function $c : \text{Fin}(d) \to R$, the inverse of the basis representation map applied to $c$ equals the image in $R[X]/(g)$ of the polynomial $\sum_{i \in \text{Fin}(d)} c(i) X^i$. In other words, given the basis $\{1, \alpha, \ldots, \alpha^{d-1}\}$ where $\alpha$ is a root of $g$ in $R[X]/(g)$, the element corresponding to coefficients $c(0), c(1), \ldots, c(d-1)$ in this basis is exactly the equivalence class of $\sum_{i=0}^{d-1} c(i)X^i$ modulo $(g)$.

AdjoinRoot.powerBasisAux'_repr_apply_to_fun theorem

 (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) : (powerBasisAux' hg).repr f i = (modByMonicHom hg f).coeff ↑i

Full source

@[simp]
theorem powerBasisAux'_repr_apply_to_fun (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) :
    (powerBasisAux' hg).repr f i = (modByMonicHom hg f).coeff ↑i :=
  rfl

Coefficient Representation in Power Basis for Adjoined Root Ring

Informal description

Let $R$ be a commutative ring and $g \in R[X]$ a monic polynomial of degree $d$. For any element $f \in R[X]/(g)$ and any index $i \in \text{Fin}(d)$, the $i$-th coefficient of the representation of $f$ in the basis $\{1, \text{root}(g), \ldots, \text{root}(g)^{d-1}\}$ is equal to the $i$-th coefficient of the remainder when $f$ is divided by $g$. Here, $\text{root}(g)$ denotes the image of $X$ in the quotient ring $R[X]/(g)$, and $\text{Fin}(d)$ is the finite type of size $d$.

AdjoinRoot.powerBasis' definition

(hg : g.Monic) : PowerBasis R (AdjoinRoot g)

Full source

/-- The power basis `1, root g, ..., root g ^ (d - 1)` for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`. -/
@[simps]
def powerBasis' (hg : g.Monic) : PowerBasis R (AdjoinRoot g) where
  gen := root g
  dim := g.natDegree
  basis := powerBasisAux' hg
  basis_eq_pow i := by
    simp only [powerBasisAux', Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk]
    rw [Finset.sum_eq_single i]
    · rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
    · intro j _ hj
      rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]
    -- Fix `DecidableEq` mismatch
    · intros
      have := Finset.mem_univ i
      contradiction

Power basis for adjoined root of a monic polynomial

Informal description

Given a monic polynomial $ g \in R[X] $ of degree $ d $, the structure `AdjoinRoot.powerBasis' hg` represents the power basis $\{1, \alpha, \alpha^2, \ldots, \alpha^{d-1}\}$ for the $ R $-algebra $ R[X]/(g) $, where $ \alpha $ is the image of $ X $ in the quotient ring $ R[X]/(g) $ (i.e., the adjoined root of $ g $). Here, `gen` is $ \alpha $, `dim` is $ d $, and `basis` is the basis constructed from the powers of $ \alpha $.

Polynomial.Monic.free_adjoinRoot theorem

(hg : g.Monic) : Module.Free R (AdjoinRoot g)

Full source

lemma _root_.Polynomial.Monic.free_adjoinRoot (hg : g.Monic) : Module.Free R (AdjoinRoot g) :=
  .of_basis (powerBasis' hg).basis

Freeness of the Adjoined Root Module for a Monic Polynomial

Informal description

For any monic polynomial $g \in R[X]$ over a commutative ring $R$, the $R$-module $R[X]/(g)$ is free.

Polynomial.Monic.finite_adjoinRoot theorem

(hg : g.Monic) : Module.Finite R (AdjoinRoot g)

Full source

lemma _root_.Polynomial.Monic.finite_adjoinRoot (hg : g.Monic) : Module.Finite R (AdjoinRoot g) :=
  .of_basis (powerBasis' hg).basis

Finitely generated module structure for adjoined root of a monic polynomial

Informal description

For any monic polynomial $ g \in R[X] $, the $ R $-module $ R[X]/(g) $ is finitely generated.

Polynomial.Monic.free_quotient theorem

(hg : g.Monic) : Module.Free R (R[X] ⧸ Ideal.span { g })

Full source

/-- An unwrapped version of `AdjoinRoot.free_of_monic` for better discoverability. -/
lemma _root_.Polynomial.Monic.free_quotient (hg : g.Monic) :
    Module.Free R (R[X]R[X] ⧸ Ideal.span {g}) :=
  hg.free_adjoinRoot

Freeness of the Quotient Module by a Monic Polynomial Ideal

Informal description

For any monic polynomial $g \in R[X]$ over a commutative ring $R$, the quotient module $R[X]/(g)$ is free as an $R$-module.

Polynomial.Monic.finite_quotient theorem

(hg : g.Monic) : Module.Finite R (R[X] ⧸ Ideal.span { g })

Full source

/-- An unwrapped version of `AdjoinRoot.finite_of_monic` for better discoverability. -/
lemma _root_.Polynomial.Monic.finite_quotient (hg : g.Monic) :
    Module.Finite R (R[X]R[X] ⧸ Ideal.span {g}) :=
  hg.finite_adjoinRoot

Finitely Generated Quotient Module for Monic Polynomials

Informal description

For any monic polynomial $g \in R[X]$, the quotient module $R[X]/(g)$ is finitely generated as an $R$-module.

AdjoinRoot.isIntegral_root theorem

(hf : f ≠ 0) : IsIntegral K (root f)

Full source

theorem isIntegral_root (hf : f ≠ 0) : IsIntegral K (root f) :=
  (isAlgebraic_root hf).isIntegral

Integrality of Adjoined Root over Field for Nonzero Polynomials

Informal description

Let $K$ be a field and $f \in K[X]$ a nonzero polynomial. Then the adjoined root $\text{root}(f)$ in the ring $K[X]/(f)$ is integral over $K$, meaning there exists a monic polynomial $g \in K[X]$ such that $g(\text{root}(f)) = 0$.

AdjoinRoot.minpoly_root theorem

(hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff⁻¹

Full source

theorem minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff⁻¹ := by
  have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
  refine (minpoly.unique K _ f'_monic ?_ ?_).symm
  · rw [map_mul, aeval_eq, mk_self, zero_mul]
  intro q q_monic q_aeval
  have commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f := by
    ext
    · simp only [RingHom.comp_apply, mk_C, lift_of]
      rfl
    · simp only [RingHom.comp_apply, mk_X, lift_root]
  rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
    Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]
  · apply natDegree_le_of_dvd
    · have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
      exact mk_eq_zero.1 this
    · exact q_monic.ne_zero
  · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Minimal Polynomial of Adjoined Root: $\text{minpoly}_K(\text{root}(f)) = f \cdot C(f_{\text{leadingCoeff}}^{-1})$

Informal description

Let $K$ be a field and $f \in K[X]$ be a nonzero polynomial. The minimal polynomial of the adjoined root $\text{root}(f)$ in the extension $K[X]/(f)$ is given by $f$ multiplied by the inverse of its leading coefficient, i.e., \[ \text{minpoly}_K(\text{root}(f)) = f \cdot C(f_{\text{leadingCoeff}}^{-1}). \]

AdjoinRoot.powerBasisAux definition

(hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f)

Full source

/-- 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`. -/
def powerBasisAux (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f) := by
  let f' := f * C f.leadingCoeff⁻¹
  have deg_f' : f'.natDegree = f.natDegree := by
    rw [natDegree_mul hf, natDegree_C, add_zero]
    · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
  have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
  apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
  · rw [← deg_f', ← minpoly_eq]
    exact linearIndependent_pow (root f)
  · rintro y -
    rw [← deg_f', ← minpoly_eq]
    apply (isIntegral_root hf).mem_span_pow
    obtain ⟨g⟩ := y
    use g
    rw [aeval_eq]
    rfl

Power basis for $K[X]/(f)$

Informal description

Given a field $K$ and a nonzero polynomial $f \in K[X]$ of degree $d$, the set $\{1, \alpha, \alpha^2, \ldots, \alpha^{d-1}\}$ forms a basis for the $K$-vector space $K[X]/(f)$, where $\alpha$ is the image of $X$ in the quotient ring (i.e., $\alpha$ is a root of $f$). Here, the basis vectors are the powers of $\alpha$ from $0$ to $d-1$.

AdjoinRoot.powerBasis definition

(hf : f ≠ 0) : PowerBasis K (AdjoinRoot f)

Full source

/-- 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`. -/
@[simps!]
def powerBasis (hf : f ≠ 0) : PowerBasis K (AdjoinRoot f) where
  gen := root f
  dim := f.natDegree
  basis := powerBasisAux hf
  basis_eq_pow := by simp [powerBasisAux]

Power basis for $K[X]/(f)$

Informal description

Given a field $K$ and a nonzero polynomial $f \in K[X]$, the power basis for the quotient ring $K[X]/(f)$ is the basis $\{1, \alpha, \alpha^2, \ldots, \alpha^{d-1}\}$, where $\alpha$ is the image of $X$ in the quotient ring (i.e., $\alpha$ is a root of $f$) and $d = \deg f$ is the degree of $f$. This basis makes $K[X]/(f)$ into a $K$-vector space of dimension $d$.

AdjoinRoot.minpoly_powerBasis_gen theorem

(hf : f ≠ 0) : minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹

Full source

theorem minpoly_powerBasis_gen (hf : f ≠ 0) :
    minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹ := by
  rw [powerBasis_gen, minpoly_root hf]

Minimal Polynomial of Power Basis Generator: $\text{minpoly}_K(\alpha) = f \cdot C(f_{\text{leadingCoeff}}^{-1})$

Informal description

Let $K$ be a field and $f \in K[X]$ be a nonzero polynomial. The minimal polynomial of the generator of the power basis for $K[X]/(f)$ is given by $f$ multiplied by the inverse of its leading coefficient, i.e., \[ \text{minpoly}_K(\alpha) = f \cdot C(f_{\text{leadingCoeff}}^{-1}), \] where $\alpha$ is the generator of the power basis (the image of $X$ in $K[X]/(f)$).

AdjoinRoot.Minpoly.toAdjoin definition

: AdjoinRoot (minpoly R x) →ₐ[R] adjoin R ({ x } : Set S)

Full source

/-- 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`. -/
@[simps!]
def Minpoly.toAdjoin : AdjoinRootAdjoinRoot (minpoly R x) →ₐ[R] adjoin R ({x} : Set S) :=
  liftHom _ ⟨x, self_mem_adjoin_singleton R x⟩
    (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe])

Algebra homomorphism from adjoined minimal polynomial to generated subalgebra

Informal description

The surjective algebra homomorphism from the quotient ring $R[X]/(\text{minpoly}_R x)$ to the $R$-algebra generated by $x$ in $S$, where $\text{minpoly}_R x$ is the minimal polynomial of $x$ over $R$. If $R$ is an integrally closed domain and $x$ is integral over $R$, this homomorphism is an isomorphism.

AdjoinRoot.Minpoly.toAdjoin_apply' theorem

 (a : AdjoinRoot (minpoly R x)) :
  Minpoly.toAdjoin R x a =
    liftHom (minpoly R x) (⟨x, self_mem_adjoin_singleton R x⟩ : adjoin R ({ x } : Set S))
      (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]) a

Full source

theorem Minpoly.toAdjoin_apply' (a : AdjoinRoot (minpoly R x)) :
    Minpoly.toAdjoin R x a =
      liftHom (minpoly R x) (⟨x, self_mem_adjoin_singleton R x⟩ : adjoin R ({x} : Set S))
        (by simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]) a :=
  rfl

Evaluation of Minimal Polynomial Adjoin Homomorphism

Informal description

For any element $a$ in the quotient ring $R[X]/(\text{minpoly}_R x)$, the algebra homomorphism $\text{Minpoly.toAdjoin}\, R\, x$ evaluated at $a$ is equal to the lift of the algebra homomorphism $\text{liftHom}$ applied to the minimal polynomial $\text{minpoly}_R x$, the element $\langle x, \text{self\_mem\_adjoin\_singleton}\, R\, x \rangle$ in the subalgebra generated by $x$, and the proof that $x$ is a root of $\text{minpoly}_R x$ in the subalgebra.

AdjoinRoot.Minpoly.toAdjoin.apply_X theorem

: Minpoly.toAdjoin R x (mk (minpoly R x) X) = ⟨x, self_mem_adjoin_singleton R x⟩

Full source

theorem Minpoly.toAdjoin.apply_X :
    Minpoly.toAdjoin R x (mk (minpoly R x) X) = ⟨x, self_mem_adjoin_singleton R x⟩ := by
  simp [toAdjoin]

Image of $X$ under minimal polynomial adjoin homomorphism

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, and $x \in S$ an element with minimal polynomial $\text{minpoly}_R x \in R[X]$. Then the algebra homomorphism $\text{Minpoly.toAdjoin}\, R\, x$ maps the equivalence class of $X$ in $R[X]/(\text{minpoly}_R x)$ to the element $\langle x, \text{self\_mem\_adjoin\_singleton}\, R\, x \rangle$ in the $R$-subalgebra generated by $x$.

AdjoinRoot.Minpoly.toAdjoin.surjective theorem

: Function.Surjective (Minpoly.toAdjoin R x)

Full source

theorem Minpoly.toAdjoin.surjective : Function.Surjective (Minpoly.toAdjoin R x) := by
  rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]
  exact adjoin_le fun ⟨y₁, y₂⟩ h ↦ ⟨mk (minpoly R x) X, by simpa [toAdjoin] using h.symm⟩

Surjectivity of the Minimal Polynomial Adjoin Homomorphism

Informal description

The algebra homomorphism $\text{Minpoly.toAdjoin}\, R\, x$ from the quotient ring $R[X]/(\text{minpoly}_R x)$ to the $R$-subalgebra generated by $x$ in $S$ is surjective. Here, $\text{minpoly}_R x$ denotes the minimal polynomial of $x$ over $R$.

AdjoinRoot.equiv' definition

(h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) : AdjoinRoot g ≃ₐ[R] S

Full source

/-- 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`. -/
@[simps -fullyApplied]
def equiv' (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
    AdjoinRootAdjoinRoot g ≃ₐ[R] S :=
  { AdjoinRoot.liftHom g pb.gen h₂ with
    toFun := AdjoinRoot.liftHom g pb.gen h₂
    invFun := pb.lift (root g) h₁
    -- Porting note: another term-mode proof converted to tactic-mode.
    left_inv := fun x => by
      induction x using AdjoinRoot.induction_on
      rw [liftHom_mk, pb.lift_aeval, aeval_eq]
    right_inv := fun x => by
      nontriviality S
      obtain ⟨f, _hf, rfl⟩ := pb.exists_eq_aeval x
      rw [pb.lift_aeval, aeval_eq, liftHom_mk] }

Isomorphism between adjoined root and algebra with power basis

Informal description

Given a commutative ring $R$, a monic polynomial $g \in R[X]$, and a power basis $\text{pb}$ for an $R$-algebra $S$ with generator $\text{pb.gen}$, if the following conditions hold: 1. The adjoined root $\text{root}\, g$ satisfies $\text{aeval}\, (\text{root}\, g)\, (\text{minpoly}_R\, \text{pb.gen}) = 0$, 2. The generator $\text{pb.gen}$ satisfies $\text{aeval}\, \text{pb.gen}\, g = 0$, then there exists an $R$-algebra isomorphism $\text{AdjoinRoot}\, g \simeq S$ between the quotient ring $R[X]/(g)$ and $S$. The isomorphism is constructed by lifting the algebra homomorphism $\text{AdjoinRoot.liftHom}\, g\, \text{pb.gen}\, h_2$ and its inverse $\text{pb.lift}\, (\text{root}\, g)\, h_1$.

AdjoinRoot.equiv'_toAlgHom theorem

 (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
  (equiv' g pb h₁ h₂).toAlgHom = AdjoinRoot.liftHom g pb.gen h₂

Full source

theorem equiv'_toAlgHom (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
    (equiv' g pb h₁ h₂).toAlgHom = AdjoinRoot.liftHom g pb.gen h₂ :=
  rfl

Algebra Homomorphism Component of Adjoined Root Isomorphism Equals Lifted Homomorphism

Informal description

Given a commutative ring $R$, a monic polynomial $g \in R[X]$, and a power basis $\text{pb}$ for an $R$-algebra $S$ with generator $\text{pb.gen}$, if: 1. The adjoined root $\text{root}\, g$ satisfies $\text{aeval}\, (\text{root}\, g)\, (\text{minpoly}_R\, \text{pb.gen}) = 0$, 2. The generator $\text{pb.gen}$ satisfies $\text{aeval}\, \text{pb.gen}\, g = 0$, then the algebra homomorphism component of the isomorphism $\text{equiv'}\, g\, \text{pb}\, h_1\, h_2$ is equal to the lifted algebra homomorphism $\text{AdjoinRoot.liftHom}\, g\, \text{pb.gen}\, h_2$.

AdjoinRoot.equiv'_symm_toAlgHom theorem

 (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
  (equiv' g pb h₁ h₂).symm.toAlgHom = pb.lift (root g) h₁

Full source

theorem equiv'_symm_toAlgHom (h₁ : aeval (root g) (minpoly R pb.gen) = 0)
    (h₂ : aeval pb.gen g = 0) : (equiv' g pb h₁ h₂).symm.toAlgHom = pb.lift (root g) h₁ :=
  rfl

Inverse of Adjoined Root-Power Basis Isomorphism via Lift

Informal description

Given a commutative ring $R$, a monic polynomial $g \in R[X]$, and a power basis $\text{pb}$ for an $R$-algebra $S$ with generator $\text{pb.gen}$, if the following conditions hold: 1. The adjoined root $\text{root}\, g$ satisfies $\text{aeval}\, (\text{root}\, g)\, (\text{minpoly}_R\, \text{pb.gen}) = 0$, 2. The generator $\text{pb.gen}$ satisfies $\text{aeval}\, \text{pb.gen}\, g = 0$, then the inverse of the $R$-algebra isomorphism $\text{AdjoinRoot}\, g \simeq S$ is given by the algebra homomorphism $\text{pb.lift}\, (\text{root}\, g)\, h_1$.

AdjoinRoot.equiv definition

(f : F[X]) (hf : f ≠ 0) : (AdjoinRoot f →ₐ[F] L) ≃ { x // x ∈ f.aroots L }

Full source

/-- 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`. -/
def equiv (f : F[X]) (hf : f ≠ 0) :
    (AdjoinRoot f →ₐ[F] L) ≃ { x // x ∈ f.aroots L } :=
  (powerBasis hf).liftEquiv'.trans
    ((Equiv.refl _).subtypeEquiv fun x => by
      rw [powerBasis_gen, minpoly_root hf, aroots_mul, aroots_C, add_zero, Equiv.refl_apply]
      exact (monic_mul_leadingCoeff_inv hf).ne_zero)

Bijection between algebra homomorphisms from $ F[X]/(f) $ and roots of $ f $ in $ L $

Informal description

Given a field extension $ L $ of $ F $ and a nonzero polynomial $ f \in F[X] $, there is a bijection between $ F $-algebra homomorphisms from $ F[X]/(f) $ to $ L $ and the roots of $ f $ in $ L $. More precisely, the bijection maps: 1. Any $ F $-algebra homomorphism $ \phi : F[X]/(f) \to L $ to the element $ \phi(\overline{X}) \in L $, which is a root of $ f $ in $ L $. 2. Any root $ x \in L $ of $ f $ back to the unique $ F $-algebra homomorphism $ F[X]/(f) \to L $ sending $ \overline{X} $ to $ x $.

AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk definition

: AdjoinRoot f ⧸ I.map (of f) ≃+* AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span { f }))

Full source

/-- 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)`. -/
def quotMapOfEquivQuotMapCMapSpanMk :
    AdjoinRootAdjoinRoot f ⧸ I.map (of f)AdjoinRoot f ⧸ I.map (of f) ≃+*
      AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span {f})) :=
  Ideal.quotEquivOfEq (by rw [of, AdjoinRoot.mk, Ideal.map_map])

Isomorphism of quotient rings for adjoined roots

Informal description

The natural ring isomorphism between the quotient rings $R[\alpha]/(I[\alpha])$ and $R[\alpha]/((I[x] \sqcup (f))/(f))$, where $\alpha$ is a root of the polynomial $f \in R[X]$ and $I$ is an ideal of $R$. Here, $I[\alpha]$ denotes the image of $I$ under the natural embedding $R \to R[\alpha]$, and $(I[x] \sqcup (f))/(f)$ represents the ideal generated by $I$ in $R[X]$ combined with the principal ideal $(f)$, then quotiented by $(f)$.

AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk theorem

 (x : AdjoinRoot f) :
  quotMapOfEquivQuotMapCMapSpanMk I f (Ideal.Quotient.mk (I.map (of f)) x) =
    Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span { f })) (I.map (C : R →+* R[X]))) x

Full source

@[simp]
theorem quotMapOfEquivQuotMapCMapSpanMk_mk (x : AdjoinRoot f) :
    quotMapOfEquivQuotMapCMapSpanMk I f (Ideal.Quotient.mk (I.map (of f)) x) =
      Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (I.map (C : R →+* R[X]))) x := rfl

Commutativity of Quotient Maps for Adjoined Root Ring

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any element $x$ in the quotient ring $R[X]/(f)$, the image of $x$ under the quotient map $\text{AdjoinRoot f} \to \text{AdjoinRoot f}/(I[\alpha])$ corresponds to the image of $x$ under the quotient map $\text{AdjoinRoot f} \to \text{AdjoinRoot f}/((I[X] + (f))/(f))$ via the isomorphism between these quotient rings. Here: - $I[\alpha]$ denotes the image of $I$ under the embedding $R \to R[X]/(f)$ - $(I[X] + (f))/(f)$ is the ideal generated by $I$ in $R[X]$ combined with the principal ideal $(f)$, then quotiented by $(f)$

AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk theorem

 (x : AdjoinRoot f) :
  (quotMapOfEquivQuotMapCMapSpanMk I f).symm
      (Ideal.Quotient.mk ((I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span { f }))) x) =
    Ideal.Quotient.mk (I.map (of f)) x

Full source

theorem quotMapOfEquivQuotMapCMapSpanMk_symm_mk (x : AdjoinRoot f) :
    (quotMapOfEquivQuotMapCMapSpanMk I f).symm
        (Ideal.Quotient.mk ((I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span {f}))) x) =
      Ideal.Quotient.mk (I.map (of f)) x := by
  rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]
  exact Ideal.quotEquivOfEq_mk _ _

Inverse Isomorphism Property for Quotient Polynomial Rings: $\Phi^{-1}(\overline{\overline{x}}) = \overline{x}$

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any element $x$ in the quotient ring $R[X]/(f)$, the inverse of the isomorphism $$(R[X]/(f))/(I) \cong (R[X]/I[X])/(f)$$ maps the equivalence class of $x$ in $(R[X]/I[X])/(f)$ to the equivalence class of $x$ in $R[X]/(f)$ modulo the ideal generated by $I$. In symbols: $$\Phi^{-1}(\overline{\overline{x}}) = \overline{x}$$ where $\Phi$ is the isomorphism and the bars denote the respective quotient maps.

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk definition

 :
  AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span ({ f } : Set R[X]))) ≃+*
    (R[X] ⧸ I.map (C : R →+* R[X])) ⧸ (span ({ f } : Set R[X])).map (Ideal.Quotient.mk (I.map (C : R →+* R[X])))

Full source

/-- 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` -/
def quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk :
    AdjoinRootAdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span ({f} : Set R[X])))AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span ({f} : Set R[X]))) ≃+*
      (R[X] ⧸ I.map (C : R →+* R[X])) ⧸
        (span ({f} : Set R[X])).map (Ideal.Quotient.mk (I.map (C : R →+* R[X]))) :=
  quotQuotEquivComm (Ideal.span ({f} : Set R[X])) (I.map (C : R →+* R[X]))

Isomorphism between quotients of polynomial rings by ideals and polynomials

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. There is a natural ring isomorphism between: 1. The quotient of $R[X]/(f)$ by the ideal generated by $I$ in this quotient ring 2. The quotient of $R[X]/I[X]$ by the ideal generated by $f$ in this quotient ring In symbols: $$(R[X]/(f))/(I) \cong (R[X]/I[X])/(f)$$ where $(I)$ denotes the image of $I$ in $R[X]/(f)$ and $I[X]$ is the ideal of polynomials with coefficients in $I$.

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk theorem

 (p : R[X]) :
  quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f (Ideal.Quotient.mk _ (mk f p)) = quotQuotMk (I.map C) (span { f }) p

Full source

theorem quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk (p : R[X]) :
    quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f (Ideal.Quotient.mk _ (mk f p)) =
      quotQuotMk (I.map C) (span {f}) p :=
  rfl

Isomorphism Property for Quotient Polynomial Rings: $\Phi(\overline{\overline{p}}) = \overline{\overline{p}}$

Informal description

For any polynomial $p \in R[X]$, the isomorphism $$(R[X]/(f))/(I) \cong (R[X]/I[X])/(f)$$ maps the equivalence class of $p$ in $R[X]/(f)$ modulo the ideal generated by $I$ to the equivalence class of $p$ in $(R[X]/I[X])/(f)$. In symbols: $$\Phi(\overline{\overline{p}}) = \overline{\overline{p}}$$ where $\Phi$ is the isomorphism and the bars denote the respective quotient maps.

AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk theorem

 (p : R[X]) :
  (quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).symm (quotQuotMk (I.map C) (span { f }) p) =
    Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span { f })) (I.map (C : R →+* R[X]))) (mk f p)

Full source

@[simp]
theorem quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk (p : R[X]) :
    (quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).symm (quotQuotMk (I.map C) (span {f}) p) =
      Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (I.map (C : R →+* R[X])))
        (mk f p) :=
  rfl

Inverse Isomorphism Property for Quotient Polynomial Rings

Informal description

For any polynomial $p \in R[X]$, the inverse of the isomorphism $$(R[X]/(f))/(I) \cong (R[X]/I[X])/(f)$$ maps the equivalence class of $p$ in $(R[X]/I[X])/(f)$ to the equivalence class of the image of $p$ in $R[X]/(f)$ modulo the ideal generated by $I$ in $R[X]/(f)$. In symbols, for $p \in R[X]$, we have: $$\Phi^{-1}(\overline{\overline{p}}) = \overline{\overline{p}}$$ where $\Phi$ is the isomorphism and the bars denote the respective quotient maps.

AdjoinRoot.Polynomial.quotQuotEquivComm definition

 :
  (R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))) ≃+*
    (R[X] ⧸ (I.map C)) ⧸ span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C)))

Full source

/-- 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` -/
def Polynomial.quotQuotEquivComm :
    (R ⧸ I)[X](R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I)))(R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))) ≃+*
      (R[X] ⧸ (I.map C)) ⧸ span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))) :=
  quotientEquiv (span ({f.map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
    (span {Ideal.Quotient.mk (I.map Polynomial.C) f}) (polynomialQuotientEquivQuotientPolynomial I)
    (by
      rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f])

Isomorphism of Quotient Polynomial Rings Modulo Ideals

Informal description

The natural isomorphism between the quotient rings $(R/I)[x]/(f \mod I)$ and $(R[x]/(I \cdot R[x]))/(f \mod I[x])$, where $f$ is a polynomial in $R[x]$ and $I$ is an ideal of $R$. Here, $f \mod I$ denotes the image of $f$ under the quotient map $R[x] \to (R/I)[x]$, and $I \cdot R[x]$ is the ideal of $R[x]$ generated by $I$.

AdjoinRoot.Polynomial.quotQuotEquivComm_mk theorem

 (p : R[X]) :
  (Polynomial.quotQuotEquivComm I f) (Ideal.Quotient.mk _ (p.map (Ideal.Quotient.mk I))) =
    Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))))
      (Ideal.Quotient.mk (I.map C) p)

Full source

@[simp]
theorem Polynomial.quotQuotEquivComm_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f) (Ideal.Quotient.mk _ (p.map (Ideal.Quotient.mk I))) =
      Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X]R[X] ⧸ (I.map C))))
      (Ideal.Quotient.mk (I.map C) p) := by
  simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
    polynomialQuotientEquivQuotientPolynomial_map_mk]

Isomorphism Property for Quotient Polynomial Rings: Image of Polynomial Class

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any polynomial $p \in R[X]$, the isomorphism $\Phi : (R/I)[X]/(f \mod I) \to (R[X]/(I \cdot R[X]))/(f)$ maps the equivalence class of $p \mod I$ in $(R/I)[X]$ to the equivalence class of $p$ modulo $(I \cdot R[X] + (f))$ in $R[X]/(I \cdot R[X])$. In symbols: $$\Phi\left(\overline{p \mod I}\right) = \overline{\overline{p}}$$ where: - $\overline{p \mod I}$ denotes the equivalence class of $p \mod I$ in $(R/I)[X]/(f \mod I)$, - $\overline{\overline{p}}$ denotes the equivalence class of $\overline{p}$ in $(R[X]/(I \cdot R[X]))/(f)$, - $p \mod I$ is the image of $p$ under the quotient map $R[X] \to (R/I)[X]$.

AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk theorem

 (p : R[X]) :
  (Polynomial.quotQuotEquivComm I f).symm
      (Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))))
        (Ideal.Quotient.mk (I.map C) p)) =
    Ideal.Quotient.mk (span {f.map (Ideal.Quotient.mk I)}) (p.map (Ideal.Quotient.mk I))

Full source

@[simp]
theorem Polynomial.quotQuotEquivComm_symm_mk_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f).symm (Ideal.Quotient.mk (span
    ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X]R[X] ⧸ (I.map C)))) (Ideal.Quotient.mk (I.map C) p)) =
      Ideal.Quotient.mk (span {f.map (Ideal.Quotient.mk I)}) (p.map (Ideal.Quotient.mk I)) := by
  simp only [Polynomial.quotQuotEquivComm, quotientEquiv_symm_mk,
    polynomialQuotientEquivQuotientPolynomial_symm_mk]

Inverse Image of Quotient Polynomial under Ring Isomorphism

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any polynomial $p \in R[X]$, the inverse of the isomorphism $\text{quotQuotEquivComm}$ maps the equivalence class of $p$ modulo $(I \cdot R[X] + (f))$ to the equivalence class of $p \mod I$ modulo $(f \mod I)$ in $(R/I)[X]$. More precisely, given $p \in R[X]$, we have: $$(\text{quotQuotEquivComm}\, I\, f)^{-1}\left(\overline{\overline{p}}\right) = \overline{p \mod I}$$ where: - $\overline{\overline{p}}$ denotes the equivalence class of $\overline{p}$ in $(R[X]/(I \cdot R[X]))/(f)$, - $\overline{p \mod I}$ denotes the equivalence class of $p \mod I$ in $(R/I)[X]/(f \mod I)$, - $p \mod I$ is the image of $p$ under the quotient map $R[X] \to (R/I)[X]$.

AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot definition

: AdjoinRoot f ⧸ I.map (of f) ≃+* (R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])

Full source

/-- The natural isomorphism `R[α]/I[α] ≅ (R/I)[X]/(f mod I)` for `α` a root of `f : R[X]`
  and `I : Ideal R`. -/
def quotAdjoinRootEquivQuotPolynomialQuot :
    AdjoinRootAdjoinRoot f ⧸ I.map (of f)AdjoinRoot f ⧸ I.map (of f) ≃+*
    (R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]) :=
  (quotMapOfEquivQuotMapCMapSpanMk I f).trans
    ((quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).trans
      ((Ideal.quotEquivOfEq (by rw [map_span, Set.image_singleton])).trans
        (Polynomial.quotQuotEquivComm I f).symm))

Isomorphism between quotient of adjoined root ring and quotient polynomial ring

Informal description

Given a commutative ring $R$, an ideal $I$ of $R$, and a polynomial $f \in R[X]$, there is a natural ring isomorphism between: 1. The quotient ring $(R[X]/(f))/(I \cdot R[X]/(f))$, where $I \cdot R[X]/(f)$ is the image of $I$ in $R[X]/(f)$ under the natural embedding $R \to R[X]/(f)$. 2. The quotient ring $(R/I)[X]/(\overline{f})$, where $\overline{f}$ is the image of $f$ under the quotient map $R[X] \to (R/I)[X]$. In symbols: $$(R[\alpha]/I[\alpha]) \cong (R/I)[X]/(\overline{f})$$ where $\alpha$ is a root of $f$ and $I[\alpha]$ denotes the image of $I$ in $R[\alpha] = R[X]/(f)$.

AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of theorem

 (p : R[X]) :
  quotAdjoinRootEquivQuotPolynomialQuot I f (Ideal.Quotient.mk (I.map (of f)) (mk f p)) =
    Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I))

Full source

@[simp]
theorem quotAdjoinRootEquivQuotPolynomialQuot_mk_of (p : R[X]) :
    quotAdjoinRootEquivQuotPolynomialQuot I f (Ideal.Quotient.mk (I.map (of f)) (mk f p)) =
      Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]))
      (p.map (Ideal.Quotient.mk I)) := rfl

Isomorphism Maps Quotient of Adjoined Root Ring to Quotient Polynomial Ring

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any polynomial $p \in R[X]$, the isomorphism $\text{quotAdjoinRootEquivQuotPolynomialQuot}$ maps the equivalence class of $p$ in $R[X]/(f)$ modulo $I \cdot R[X]/(f)$ to the equivalence class of $p \mod I$ in $(R/I)[X]/(f \mod I)$. In symbols: $$\Phi\left(\overline{p} \mod I[\alpha]\right) = \overline{p \mod I} \mod \overline{f}$$ where: - $\Phi$ is the isomorphism $(R[\alpha]/I[\alpha]) \cong (R/I)[X]/(\overline{f})$, - $\overline{p}$ denotes the image of $p$ in $R[X]/(f)$, - $I[\alpha]$ denotes the image of $I$ in $R[X]/(f)$, - $p \mod I$ is the image of $p$ under the quotient map $R[X] \to (R/I)[X]$, - $\overline{f}$ is the image of $f$ in $(R/I)[X]$.

AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk theorem

 (p : R[X]) :
  (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      (Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I))) =
    Ideal.Quotient.mk (I.map (of f)) (mk f p)

Full source

@[simp]
theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) :
    (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
        (Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]))
        (p.map (Ideal.Quotient.mk I))) =
      Ideal.Quotient.mk (I.map (of f)) (mk f p) := by
  rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply,
    RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
    Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
    RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
    quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk,
    quotMapOfEquivQuotMapCMapSpanMk_symm_mk]

Inverse Isomorphism Property for Quotient Rings: $\Phi^{-1}(\overline{\overline{p}}) = \overline{p}$

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f \in R[X]$ a polynomial. For any polynomial $p \in R[X]$, the inverse of the isomorphism $$(R[X]/(f))/(I) \cong (R/I)[X]/(\overline{f})$$ maps the equivalence class of $\overline{p}$ in $(R/I)[X]/(\overline{f})$ to the equivalence class of $p$ in $R[X]/(f)$ modulo the ideal generated by $I$. Here $\overline{p}$ denotes the image of $p$ under the quotient map $R[X] \to (R/I)[X]$, and $\overline{f}$ is the image of $f$ under this map.

AdjoinRoot.quotEquivQuotMap definition

 (f : R[X]) (I : Ideal R) :
  (AdjoinRoot f ⧸ Ideal.map (of f) I) ≃ₐ[R]
    (R ⧸ I)[X] ⧸ Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X])

Full source

/-- Promote `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot` to an alg_equiv. -/
@[simps!]
noncomputable def quotEquivQuotMap (f : R[X]) (I : Ideal R) :
    (AdjoinRoot f ⧸ Ideal.map (of f) I) ≃ₐ[R]
      (R ⧸ I)[X] ⧸ Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X]) :=
  AlgEquiv.ofRingEquiv
    (show ∀ x, (quotAdjoinRootEquivQuotPolynomialQuot I f) (algebraMap R _ x) = algebraMap R _ x
      from fun x => by
      have :
        algebraMap R (AdjoinRootAdjoinRoot f ⧸ Ideal.map (of f) I) x =
          Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I) ((mk f) (C x)) :=
        rfl
      rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C]
      -- Porting note: the following `rfl` was not needed
      rfl)

Isomorphism between quotient of adjoined root ring and quotient polynomial ring

Informal description

Given a commutative ring $R$, a polynomial $f \in R[X]$, and an ideal $I$ of $R$, there is an algebra isomorphism between: 1. The quotient ring $(R[X]/(f))/(I \cdot R[X]/(f))$, where $I \cdot R[X]/(f)$ is the image of $I$ under the natural embedding $R \to R[X]/(f)$. 2. The quotient ring $(R/I)[X]/(\overline{f})$, where $\overline{f}$ is the image of $f$ under the quotient map $R[X] \to (R/I)[X]$. In symbols: $$(R[\alpha]/I[\alpha]) \cong (R/I)[X]/(\overline{f})$$ where $\alpha$ is a root of $f$ and $I[\alpha]$ denotes the image of $I$ in $R[\alpha] = R[X]/(f)$.

AdjoinRoot.quotEquivQuotMap_apply_mk theorem

 (f g : R[X]) (I : Ideal R) :
  AdjoinRoot.quotEquivQuotMap f I (Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g)) =
    Ideal.Quotient.mk (Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X]))
      (g.map (Ideal.Quotient.mk I))

Full source

@[simp]
theorem quotEquivQuotMap_apply_mk (f g : R[X]) (I : Ideal R) :
    AdjoinRoot.quotEquivQuotMap f I (Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g)) =
      Ideal.Quotient.mk (Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X]))
      (g.map (Ideal.Quotient.mk I)) := by
  rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]

Isomorphism Maps Quotient Class to Polynomial Quotient Class

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $f, g \in R[X]$ polynomials. The isomorphism $\text{quotEquivQuotMap}$ maps the equivalence class of $g$ in $R[X]/(f)$ modulo $I \cdot R[X]/(f)$ to the equivalence class of $g \mod I$ in $(R/I)[X]/(f \mod I)$. In symbols: $$\Phi\left(\overline{g} \mod I[\alpha]\right) = \overline{g \mod I} \mod \overline{f}$$ where: - $\Phi$ is the isomorphism $(R[\alpha]/I[\alpha]) \cong (R/I)[X]/(\overline{f})$, - $\overline{g}$ denotes the image of $g$ in $R[X]/(f)$, - $I[\alpha]$ denotes the image of $I$ in $R[X]/(f)$, - $g \mod I$ is the image of $g$ under the quotient map $R[X] \to (R/I)[X]$, - $\overline{f}$ is the image of $f$ in $(R/I)[X]$.

AdjoinRoot.quotEquivQuotMap_symm_apply_mk theorem

 (f g : R[X]) (I : Ideal R) :
  (AdjoinRoot.quotEquivQuotMap f I).symm (Ideal.Quotient.mk _ (Polynomial.map (Ideal.Quotient.mk I) g)) =
    Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g)

Full source

theorem quotEquivQuotMap_symm_apply_mk (f g : R[X]) (I : Ideal R) :
    (AdjoinRoot.quotEquivQuotMap f I).symm (Ideal.Quotient.mk _
      (Polynomial.map (Ideal.Quotient.mk I) g)) =
        Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g) := by
  rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
    AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]

Inverse Isomorphism Property for Quotient Rings: $\Phi^{-1}(\overline{g}) = \overline{g}$

Informal description

Let $R$ be a commutative ring, $f, g \in R[X]$ polynomials, and $I$ an ideal of $R$. The inverse of the algebra isomorphism $$(R[X]/(f))/(I) \cong (R/I)[X]/(\overline{f})$$ maps the equivalence class of $\overline{g}$ in $(R/I)[X]/(\overline{f})$ to the equivalence class of $g$ in $R[X]/(f)$ modulo the ideal generated by $I$. Here $\overline{g}$ denotes the image of $g$ under the quotient map $R[X] \to (R/I)[X]$, and $\overline{f}$ is the image of $f$ under this map.

PowerBasis.quotientEquivQuotientMinpolyMap definition

 (pb : PowerBasis R S) (I : Ideal R) :
  (S ⧸ I.map (algebraMap R S)) ≃ₐ[R]
    Polynomial (R ⧸ I) ⧸ Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I)))

Full source

/-- 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)`. -/
@[simps!]
noncomputable def quotientEquivQuotientMinpolyMap (pb : PowerBasis R S) (I : Ideal R) :
    (S ⧸ I.map (algebraMap R S)) ≃ₐ[R]
      Polynomial (R ⧸ I) ⧸
        Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))) :=
  (ofRingEquiv
        (show ∀ x,
            (Ideal.quotientEquiv _ (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I)
                  (AdjoinRoot.equiv' (minpoly R pb.gen) pb
                        (by rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self])
                        (minpoly.aeval _ _)).symm.toRingEquiv
                  (by rw [Ideal.map_map, AlgEquiv.toRingEquiv_eq_coe,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]))
                (algebraMap R (S ⧸ I.map (algebraMap R S)) x) = algebraMap R _ x from fun x => by
                  rw [← Ideal.Quotient.mk_algebraMap, Ideal.quotientEquiv_apply,
                    RingHom.toFun_eq_coe, Ideal.quotientMap_mk, AlgEquiv.toRingEquiv_eq_coe,
                    RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
                    Quotient.mk_algebraMap])).trans (AdjoinRoot.quotEquivQuotMap _ _)

Isomorphism between quotient of algebra and quotient polynomial ring modulo minimal polynomial

Informal description

Given a power basis $\text{pb}$ for an $R$-algebra $S$ with generator $\text{pb.gen}$ and an ideal $I$ of $R$, there is an algebra isomorphism between: 1. The quotient algebra $S / (I \cdot S)$, where $I \cdot S$ is the extension of $I$ via the algebra map $R \to S$. 2. The quotient ring $(R/I)[X] / (\overline{f})$, where $\overline{f}$ is the image of the minimal polynomial $f = \text{minpoly}_R\, \text{pb.gen}$ under the quotient map $R[X] \to (R/I)[X]$. In symbols: $$S / I \cdot S \cong (R/I)[X] / (\overline{f})$$

PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk theorem

 (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
  pb.quotientEquivQuotientMinpolyMap I (Ideal.Quotient.mk (I.map (algebraMap R S)) (aeval pb.gen g)) =
    Ideal.Quotient.mk (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
      (g.map (Ideal.Quotient.mk I))

Full source

theorem quotientEquivQuotientMinpolyMap_apply_mk (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
    pb.quotientEquivQuotientMinpolyMap I (Ideal.Quotient.mk (I.map (algebraMap R S))
      (aeval pb.gen g)) = Ideal.Quotient.mk
        (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
          (g.map (Ideal.Quotient.mk I)) := by
  rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply,
    quotientEquiv_mk, AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval,
    AdjoinRoot.aeval_eq, AdjoinRoot.quotEquivQuotMap_apply_mk]

Isomorphism Maps Evaluation Class to Polynomial Quotient Class

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$, and $I$ an ideal of $R$. For any polynomial $g \in R[X]$, the isomorphism $$S / (I \cdot S) \cong (R/I)[X] / (\overline{f})$$ (where $f = \mathrm{minpoly}_R(x)$ and $\overline{f}$ is its image in $(R/I)[X]$) maps the equivalence class of $\mathrm{aeval}_x(g)$ in $S/(I \cdot S)$ to the equivalence class of $g \mod I$ in $(R/I)[X]/(\overline{f})$. In symbols: $$\Phi\left(\overline{\mathrm{aeval}_x(g)}\right) = \overline{g \mod I} \mod \overline{f}$$ where: - $\Phi$ is the isomorphism $S/(I \cdot S) \cong (R/I)[X]/(\overline{f})$, - $\overline{\mathrm{aeval}_x(g)}$ denotes the image of $\mathrm{aeval}_x(g)$ in $S/(I \cdot S)$, - $g \mod I$ is the image of $g$ under the quotient map $R[X] \to (R/I)[X]$, - $\overline{f}$ is the image of $f$ in $(R/I)[X]$.

PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk theorem

 (pb : PowerBasis R S) (I : Ideal R) (g : R[X]) :
  (pb.quotientEquivQuotientMinpolyMap I).symm
      (Ideal.Quotient.mk (Ideal.span ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
        (g.map (Ideal.Quotient.mk I))) =
    Ideal.Quotient.mk (I.map (algebraMap R S)) (aeval pb.gen g)

Full source

theorem quotientEquivQuotientMinpolyMap_symm_apply_mk (pb : PowerBasis R S) (I : Ideal R)
    (g : R[X]) :
    (pb.quotientEquivQuotientMinpolyMap I).symm (Ideal.Quotient.mk (Ideal.span
      ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
        (g.map (Ideal.Quotient.mk I))) = Ideal.Quotient.mk (I.map (algebraMap R S))
          (aeval pb.gen g) := by
  simp only [quotientEquivQuotientMinpolyMap, toRingEquiv_eq_coe, symm_trans_apply,
    quotEquivQuotMap_symm_apply_mk, ofRingEquiv_symm_apply, quotientEquiv_symm_mk,
    toRingEquiv_symm, RingEquiv.symm_symm, AdjoinRoot.equiv'_apply, coe_ringEquiv, liftHom_mk,
    symm_toRingEquiv]

Inverse Isomorphism Property for Quotient Algebras: $\Phi^{-1}(\overline{g}) = \overline{\text{aeval}\, \text{pb.gen}\, g}$

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with a power basis $\text{pb}$ generated by $\text{pb.gen}$, and $I$ an ideal of $R$. For any polynomial $g \in R[X]$, the inverse of the algebra isomorphism $$S / I \cdot S \cong (R/I)[X] / (\overline{f})$$ (where $f = \text{minpoly}_R\, \text{pb.gen}$ and $\overline{f}$ is the image of $f$ under $R[X] \to (R/I)[X]$) maps the equivalence class of $\overline{g}$ in $(R/I)[X] / (\overline{f})$ to the equivalence class of $\text{aeval}\, \text{pb.gen}\, g$ in $S / I \cdot S$.

Irreducible.exists_dvd_monic_irreducible_of_isIntegral theorem

 {K L : Type*} [CommRing K] [IsDomain K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] {f : L[X]}
  (hf : Irreducible f) : ∃ g : K[X], g.Monic ∧ Irreducible g ∧ f ∣ g.map (algebraMap K L)

Full source

/-- 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`. -/
theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K L : Type*}
    [CommRing K] [IsDomain K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] {f : L[X]}
    (hf : Irreducible f) : ∃ g : K[X], g.Monic ∧ Irreducible g ∧ f ∣ g.map (algebraMap K L) := by
  haveI := Fact.mk hf
  have h := hf.ne_zero
  have h2 := isIntegral_trans (R := K) _ (AdjoinRoot.isIntegral_root h)
  have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
  exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩

Existence of Monic Irreducible Divisor for Integral Field Extensions: $f \mid g^L$ with $g \in K[X]$ monic irreducible

Informal description

Let $K$ be a commutative domain, $L$ a field extension of $K$ that is integral over $K$, and $f \in L[X]$ an irreducible polynomial. Then there exists a monic irreducible polynomial $g \in K[X]$ such that $f$ divides the polynomial obtained by applying the algebra homomorphism $K \to L$ to the coefficients of $g$.

Polynomial.exists_dvd_map_of_isAlgebraic theorem

 [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] [Algebra.IsAlgebraic R S] (f : S[X]) (hf : f ≠ 0) :
  ∃ g : R[X], g ≠ 0 ∧ f ∣ g.map (algebraMap R S)

Full source

theorem Polynomial.exists_dvd_map_of_isAlgebraic [CommRing R] [CommRing S] [NoZeroDivisors S]
    [Algebra R S] [Algebra.IsAlgebraic R S] (f : S[X]) (hf : f ≠ 0) :
    ∃ g : R[X], g ≠ 0 ∧ f ∣ g.map (algebraMap R S) :=
  have ⟨g, ne, eq⟩ := (id ⟨f, hf, by simp⟩ : IsAlgebraic S (AdjoinRoot.root f)).restrictScalars R
  ⟨g, ne, by rwa [aeval_def, IsScalarTower.algebraMap_eq R S, ← eval₂_map, ← aeval_def,
    AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero] at eq⟩

Existence of Divisor Polynomial for Algebraic Elements in Extension Rings

Informal description

Let $R$ and $S$ be commutative rings with $S$ having no zero divisors, and let $S$ be an $R$-algebra where every element of $S$ is algebraic over $R$. For any nonzero polynomial $f \in S[X]$, there exists a nonzero polynomial $g \in R[X]$ such that $f$ divides the polynomial obtained by applying the algebra homomorphism $R \to S$ to the coefficients of $g$.

Main definitions and results