A predicate on adjoining roots of polynomial

This file defines a predicate IsAdjoinRoot S f, which states that the ring S can be constructed by adjoining a specified root of the polynomial f : R[X] to R. This predicate is useful when the same ring can be generated by adjoining the root of different polynomials, and you want to vary which polynomial you're considering.

The results in this file are intended to mirror those in RingTheory.AdjoinRoot, in order to provide an easier way to translate results from one to the other.

Motivation

AdjoinRoot presents one construction of a ring R[α]. However, it is possible to obtain rings of this form in many ways, such as NumberField.ringOfIntegers ℚ(√-5), or Algebra.adjoin R {α, α^2}, or IntermediateField.adjoin R {α, 2 - α}, or even if we want to view ℂ as adjoining a root of X^2 + 1 to ℝ.

Main definitions

The two main predicates in this file are:

• IsAdjoinRoot S f: S is generated by adjoining a specified root of f : R[X] to R
• IsAdjoinRootMonic S f: S is generated by adjoining a root of the monic polynomial f : R[X] to R

Using IsAdjoinRoot to map into S:

• IsAdjoinRoot.map: inclusion from R[X] to S
• IsAdjoinRoot.root: the specific root adjoined to R to give S

Using IsAdjoinRoot to map out of S:

• IsAdjoinRoot.repr: choose a non-unique representative in R[X]
• IsAdjoinRoot.lift, IsAdjoinRoot.liftHom: lift a morphism R →+* T to S →+* T
• IsAdjoinRootMonic.modByMonicHom: a unique representative in R[X] if f is monic

Main results

• AdjoinRoot.isAdjoinRoot and AdjoinRoot.isAdjoinRootMonic: AdjoinRoot satisfies the conditions on IsAdjoinRoot(Monic)
• IsAdjoinRootMonic.powerBasis: the root generates a power basis on S over R
• IsAdjoinRoot.algEquiv: algebra isomorphism showing adjoining a root gives a unique ring up to isomorphism
• IsAdjoinRoot.ofAlgEquiv: transfer IsAdjoinRoot across an algebra isomorphism
• IsAdjoinRootMonic.minpoly_eq: the minimal polynomial of the adjoined root of f is equal to f, if f is irreducible and monic, and R is a GCD domain

structure IsAdjoinRoot {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S] (f : Polynomial R) : Type (max u v)

IsAdjoinRoot S f states that the ring S can be constructed by adjoining a specified root of the polynomial f : R[X] to R.

Compare PowerBasis R S, which does not explicitly specify which polynomial we adjoin a root of (in particular f does not need to be the minimal polynomial of the root we adjoin), and AdjoinRoot which constructs a new type.

This is not a typeclass because the choice of root given S and f is not unique.

• map : Polynomial R →ₐ[R] S
• map_surjective : Function.Surjective ⇑self.map
• ker_map : RingHom.ker self.map = Ideal.span {f}

structure IsAdjoinRootMonic {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S] (f : Polynomial R) extends IsAdjoinRoot S f : Type (max u v)

IsAdjoinRootMonic S f states that the ring S can be constructed by adjoining a specified root of the monic polynomial f : R[X] to R.

As long as f is monic, there is a well-defined representation of elements of S as polynomials in R[X] of degree lower than deg f (see modByMonicHom and coeff). In particular, we have IsAdjoinRootMonic.powerBasis.

Bundling Monic into this structure is very useful when working with explicit fs such as X^2 - C a * X - C b since it saves you carrying around the proofs of monicity.

• map : Polynomial R →ₐ[R] S
• map_surjective : Function.Surjective ⇑self.map
• ker_map : RingHom.ker self.map = Ideal.span {f}
• monic : f.Monic

@[deprecated IsAdjoinRootMonic.monic (since := "2025-07-26")]

theorem IsAdjoinRootMonic.Monic {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {f : Polynomial R} (self : IsAdjoinRootMonic S f) : f.Monic

Alias of IsAdjoinRootMonic.monic.

def IsAdjoinRoot.root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : S

(h : IsAdjoinRoot S f).root is the root of f that can be adjoined to generate S.

Equations

• h.root = h.map Polynomial.X

theorem IsAdjoinRoot.subsingleton {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) [Subsingleton R] : Subsingleton S

theorem IsAdjoinRoot.algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : R) : (algebraMap R S) x = h.map (Polynomial.C x)

theorem IsAdjoinRoot.mem_ker_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} : p ∈ RingHom.ker h.map ↔ f ∣ p

@[simp]

theorem IsAdjoinRoot.map_eq_zero_iff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {p : Polynomial R} : h.map p = 0 ↔ f ∣ p

@[simp]

theorem IsAdjoinRoot.map_X {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.map Polynomial.X = h.root

@[simp]

theorem IsAdjoinRoot.map_self {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.map f = 0

@[simp]

theorem IsAdjoinRoot.aeval_root_eq_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : Polynomial.aeval h.root = h.map

@[deprecated IsAdjoinRoot.aeval_root_eq_map (since := "2025-07-23")]

theorem IsAdjoinRoot.aeval_eq {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : Polynomial.aeval h.root = h.map

Alias of IsAdjoinRoot.aeval_root_eq_map.

theorem IsAdjoinRoot.aeval_root_self {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : (Polynomial.aeval h.root) f = 0

@[deprecated IsAdjoinRoot.aeval_root_self (since := "2025-07-23")]

theorem IsAdjoinRoot.aeval_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : (Polynomial.aeval h.root) f = 0

Alias of IsAdjoinRoot.aeval_root_self.

theorem IsAdjoinRoot.adjoin_root_eq_top {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : Algebra.adjoin R {h.root} = ⊤

theorem IsAdjoinRoot.ext_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h h' : IsAdjoinRoot S f) (eq : ∀ (x : Polynomial R), h.map x = h'.map x) : h = h'

Extensionality of the IsAdjoinRoot structure itself. See IsAdjoinRootMonic.ext_elem for extensionality of the ring elements.

theorem IsAdjoinRoot.ext {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h'

Extensionality of the IsAdjoinRoot structure itself. See IsAdjoinRootMonic.ext_elem for extensionality of the ring elements.

theorem IsAdjoinRoot.ext_iff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] {h h' : IsAdjoinRoot S f} : h = h' ↔ h.root = h'.root

def IsAdjoinRoot.repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) : Polynomial R

Choose an arbitrary representative so that h.map (h.repr x) = x.

If f is monic, use IsAdjoinRootMonic.modByMonicHom for a unique choice of representative.

Equations

• h.repr x = ⋯.choose

@[simp]

theorem IsAdjoinRoot.map_repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x : S) : h.map (h.repr x) = x

theorem IsAdjoinRoot.repr_zero_mem_span {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.repr 0 ∈ Ideal.span {f}

repr preserves zero, up to multiples of f

theorem IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (x y : S) : h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}

repr preserves addition, up to multiples of f

def IsAdjoinRoot.adjoinRootAlgEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : AdjoinRoot f ≃ₐ[R] S

Algebra isomorphism with R[X]/(f).

Equations

• h.adjoinRootAlgEquiv = (Ideal.quotientEquivAlgOfEq R ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)

@[simp]

theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (g : Polynomial R) : h.adjoinRootAlgEquiv ((AdjoinRoot.mk f) g) = h.map g

theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (a : AdjoinRoot f) : h.adjoinRootAlgEquiv a = h.map ⋯.choose

theorem IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (a : S) : h.adjoinRootAlgEquiv.symm a = (AdjoinRoot.mk f) (h.repr a)

@[simp]

theorem IsAdjoinRoot.adjoinRootAlgEquiv_apply_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.adjoinRootAlgEquiv (AdjoinRoot.root f) = h.root

@[simp]

theorem IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.adjoinRootAlgEquiv.symm h.root = AdjoinRoot.root f

def IsAdjoinRoot.algEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : S ≃ₐ[R] T

Adjoining a root gives a unique algebra up to isomorphism.

This is the converse of IsAdjoinRoot.ofAlgEquiv: this turns an IsAdjoinRoot into an AlgEquiv, and IsAdjoinRoot.ofAlgEquiv turns an AlgEquiv into an IsAdjoinRoot.

Equations

• h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv

@[deprecated IsAdjoinRoot.algEquiv (since := "2025-08-13")]

def IsAdjoinRoot.aequiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : S ≃ₐ[R] T

Alias of IsAdjoinRoot.algEquiv.

---

Adjoining a root gives a unique algebra up to isomorphism.

This is the converse of IsAdjoinRoot.ofAlgEquiv: this turns an IsAdjoinRoot into an AlgEquiv, and IsAdjoinRoot.ofAlgEquiv turns an AlgEquiv into an IsAdjoinRoot.

Equations

• @IsAdjoinRoot.aequiv = @IsAdjoinRoot.algEquiv

theorem IsAdjoinRoot.algEquiv_def {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv

@[simp]

theorem IsAdjoinRoot.algEquiv_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (h.algEquiv h') h.root = h'.root

@[deprecated IsAdjoinRoot.algEquiv_root (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (h.algEquiv h') h.root = h'.root

Alias of IsAdjoinRoot.algEquiv_root.

@[simp]

theorem IsAdjoinRoot.algEquiv_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (↑(h.algEquiv h')).comp h.map = h'.map

@[deprecated IsAdjoinRoot.algEquiv_map (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (↑(h.algEquiv h')).comp h.map = h'.map

Alias of IsAdjoinRoot.algEquiv_map.

@[simp]

theorem IsAdjoinRoot.algEquiv_apply_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) (z : Polynomial R) : (h.algEquiv h') (h.map z) = h'.map z

@[simp]

theorem IsAdjoinRoot.algEquiv_self {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.algEquiv h = AlgEquiv.refl

@[deprecated IsAdjoinRoot.algEquiv_self (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_self {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) : h.algEquiv h = AlgEquiv.refl

Alias of IsAdjoinRoot.algEquiv_self.

@[simp]

theorem IsAdjoinRoot.algEquiv_symm {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (h.algEquiv h').symm = h'.algEquiv h

@[deprecated IsAdjoinRoot.algEquiv_symm (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_symm {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) : (h.algEquiv h').symm = h'.algEquiv h

Alias of IsAdjoinRoot.algEquiv_symm.

@[simp]

theorem IsAdjoinRoot.algEquiv_algEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (x : S) : (h'.algEquiv h'') ((h.algEquiv h') x) = (h.algEquiv h'') x

@[deprecated IsAdjoinRoot.algEquiv_algEquiv (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_aequiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (x : S) : (h'.algEquiv h'') ((h.algEquiv h') x) = (h.algEquiv h'') x

Alias of IsAdjoinRoot.algEquiv_algEquiv.

@[simp]

theorem IsAdjoinRoot.algEquiv_trans {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) : (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''

@[deprecated IsAdjoinRoot.algEquiv_trans (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_trans {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) : (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''

Alias of IsAdjoinRoot.algEquiv_trans.

def IsAdjoinRoot.ofAlgEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) : IsAdjoinRoot T f

Transfer IsAdjoinRoot across an algebra isomorphism.

This is the converse of IsAdjoinRoot.algEquiv: this turns an AlgEquiv into an IsAdjoinRoot, and IsAdjoinRoot.algEquiv turns an IsAdjoinRoot into an AlgEquiv.

Equations

• h.ofAlgEquiv e = { map := (↑e).comp h.map, map_surjective := ⋯, ker_map := ⋯ }

@[simp]

theorem IsAdjoinRoot.ofAlgEquiv_map_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) (a✝ : Polynomial R) : (h.ofAlgEquiv e).map a✝ = e (h.map a✝)

@[deprecated IsAdjoinRoot.ofAlgEquiv (since := "2025-08-13")]

def IsAdjoinRoot.ofEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) : IsAdjoinRoot T f

Alias of IsAdjoinRoot.ofAlgEquiv.

---

Transfer IsAdjoinRoot across an algebra isomorphism.

This is the converse of IsAdjoinRoot.algEquiv: this turns an AlgEquiv into an IsAdjoinRoot, and IsAdjoinRoot.algEquiv turns an IsAdjoinRoot into an AlgEquiv.

Equations

• @IsAdjoinRoot.ofEquiv = @IsAdjoinRoot.ofAlgEquiv

@[simp]

theorem IsAdjoinRoot.ofAlgEquiv_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).root = e h.root

@[deprecated IsAdjoinRoot.ofAlgEquiv_root (since := "2025-08-13")]

theorem IsAdjoinRoot.ofEquiv_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).root = e h.root

Alias of IsAdjoinRoot.ofAlgEquiv_root.

@[simp]

theorem IsAdjoinRoot.algEquiv_ofAlgEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (e : T ≃ₐ[R] U) : h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e

@[deprecated IsAdjoinRoot.algEquiv_ofAlgEquiv (since := "2025-08-13")]

theorem IsAdjoinRoot.aequiv_ofEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [Ring U] [Algebra R U] (e : T ≃ₐ[R] U) : h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e

Alias of IsAdjoinRoot.algEquiv_ofAlgEquiv.

@[simp]

theorem IsAdjoinRoot.ofAlgEquiv_algEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')

@[deprecated IsAdjoinRoot.ofAlgEquiv_algEquiv (since := "2025-08-13")]

theorem IsAdjoinRoot.ofEquiv_aequiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [Ring T] [Algebra R T] {U : Type u_2} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')

Alias of IsAdjoinRoot.ofAlgEquiv_algEquiv.

theorem IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (z : S) (w : Polynomial R) (hzw : h.map w = z) : Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w

Auxiliary lemma for IsAdjoinRoot.lift

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

Lift a ring homomorphism R →+* T to S →+* T by specifying a root x of f in T, where S is given by adjoining a root of f to R.

Equations

• h.lift i x hx = { toFun := fun (z : S) => Polynomial.eval₂ i x (h.repr z), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem IsAdjoinRoot.lift_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (z : Polynomial R) : (h.lift i x hx) (h.map z) = Polynomial.eval₂ i x z

@[simp]

theorem IsAdjoinRoot.lift_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) : (h.lift i x hx) h.root = x

@[simp]

theorem IsAdjoinRoot.lift_algebraMap {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (a : R) : (h.lift i x hx) ((algebraMap R S) a) = i a

theorem IsAdjoinRoot.apply_eq_lift {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (g : S →+* T) (hmap : ∀ (a : R), g ((algebraMap R S) a) = i a) (hroot : g h.root = x) (a : S) : g a = (h.lift i x hx) a

Auxiliary lemma for apply_eq_lift

theorem IsAdjoinRoot.eq_lift {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0) (g : S →+* T) (hmap : ∀ (a : R), g ((algebraMap R S) a) = i a) (hroot : g h.root = x) : g = h.lift i x hx

Unicity of lift: a map that agrees on R and h.root agrees with lift everywhere.

def IsAdjoinRoot.liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] (x : T) [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) : S →ₐ[R] T

Lift the algebra map R → T to S →ₐ[R] T by specifying a root x of f in T, where S is given by adjoining a root of f to R.

Equations

• h.liftHom x hx' = { toRingHom := h.lift (algebraMap R T) x hx', commutes' := ⋯ }

@[simp]

theorem IsAdjoinRoot.coe_liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) : ↑(h.liftHom x hx') = h.lift (algebraMap R T) x hx'

theorem IsAdjoinRoot.lift_algebraMap_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (z : S) : (h.lift (algebraMap R T) x hx') z = (h.liftHom x hx') z

@[simp]

theorem IsAdjoinRoot.liftHom_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (z : Polynomial R) : (h.liftHom x hx') (h.map z) = (Polynomial.aeval x) z

@[simp]

theorem IsAdjoinRoot.liftHom_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) : (h.liftHom x hx') h.root = x

theorem IsAdjoinRoot.eq_liftHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] {x : T} [Algebra R T] (hx' : (Polynomial.aeval x) f = 0) (g : S →ₐ[R] T) (hroot : g h.root = x) : g = h.liftHom x hx'

Unicity of liftHom: a map that agrees on h.root agrees with liftHom everywhere.

theorem IsAdjoinRoot.isAlgebraic_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRoot S f) (hf : f ≠ 0) : IsAlgebraic R h.root

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

AdjoinRoot f is indeed given by adjoining a root of f.

Equations

• AdjoinRoot.isAdjoinRoot f = { map := AdjoinRoot.mkₐ f, map_surjective := ⋯, ker_map := ⋯ }

def AdjoinRoot.isAdjoinRootMonic {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) : IsAdjoinRootMonic (AdjoinRoot f) f

AdjoinRoot f is indeed given by adjoining a root of f. If f is monic this is more powerful than AdjoinRoot.isAdjoinRoot.

Equations

• AdjoinRoot.isAdjoinRootMonic f hf = { toIsAdjoinRoot := AdjoinRoot.isAdjoinRoot f, monic := hf }

@[simp]

theorem AdjoinRoot.isAdjoinRootMonic_toAdjoinRoot {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) : (AdjoinRoot.isAdjoinRootMonic f hf).toIsAdjoinRoot = AdjoinRoot.isAdjoinRoot f

theorem AdjoinRoot.isAdjoinRoot_map_eq_mkₐ {R : Type u} [CommRing R] (f : Polynomial R) : (AdjoinRoot.isAdjoinRoot f).map = mkₐ f

@[deprecated AdjoinRoot.isAdjoinRoot_map_eq_mkₐ (since := "2025-08-07")]

theorem AdjoinRoot.isAdjoinRoot_map_eq_mk {R : Type u} [CommRing R] (f : Polynomial R) : (AdjoinRoot.isAdjoinRoot f).map = mkₐ f

Alias of AdjoinRoot.isAdjoinRoot_map_eq_mkₐ.

@[deprecated "Use `simp` and `isAdjoinRoot_map_eq_mkₐ` instead" (since := "2025-08-07")]

theorem AdjoinRoot.isAdjoinRootMonic_map_eq_mk {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) : ↑(AdjoinRoot.isAdjoinRootMonic f hf).map = mk f

@[simp]

theorem AdjoinRoot.isAdjoinRoot_root_eq_root {R : Type u} [CommRing R] (f : Polynomial R) : (AdjoinRoot.isAdjoinRoot f).root = root f

@[deprecated "Use `simp` instead" (since := "2025-08-07")]

theorem AdjoinRoot.isAdjoinRootMonic_root_eq_root {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.Monic) : (AdjoinRoot.isAdjoinRootMonic f hf).root = root f

@[reducible, inline]

abbrev IsAdjoinRoot.ofAdjoinRootEquiv {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (e : AdjoinRoot f ≃ₐ[R] S) : IsAdjoinRoot S f

If S is R-isomorphic to R[X]/(f), then S is given by adjoining a root of f.

Equations

• IsAdjoinRoot.ofAdjoinRootEquiv e = (AdjoinRoot.isAdjoinRoot f).ofAlgEquiv e

theorem IsAdjoinRootMonic.map_modByMonic {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.map (g %ₘ f) = h.map g

theorem IsAdjoinRootMonic.modByMonic_repr_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.repr (h.map g) %ₘ f = g %ₘ f

def IsAdjoinRootMonic.modByMonicHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : S →ₗ[R] Polynomial R

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

Equations

• h.modByMonicHom = { toFun := fun (x : S) => h.repr x %ₘ f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem IsAdjoinRootMonic.modByMonicHom_map {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (g : Polynomial R) : h.modByMonicHom (h.map g) = g %ₘ f

@[simp]

theorem IsAdjoinRootMonic.map_modByMonicHom {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (x : S) : h.map (h.modByMonicHom x) = x

@[simp]

theorem IsAdjoinRootMonic.modByMonicHom_root_pow {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {n : ℕ} (hdeg : n < f.natDegree) : h.modByMonicHom (h.root ^ n) = Polynomial.X ^ n

@[simp]

theorem IsAdjoinRootMonic.modByMonicHom_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) : h.modByMonicHom h.root = Polynomial.X

def IsAdjoinRootMonic.basis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : Module.Basis (Fin f.natDegree) R S

The basis on S generated by powers of h.root.

Auxiliary definition for IsAdjoinRootMonic.powerBasis.

Equations

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

@[simp]

theorem IsAdjoinRootMonic.basis_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (i : Fin f.natDegree) : h.basis i = h.root ^ ↑i

theorem IsAdjoinRootMonic.deg_pos {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) [Nontrivial S] : 0 < f.natDegree

theorem IsAdjoinRootMonic.deg_ne_zero {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) [Nontrivial S] : f.natDegree ≠ 0

def IsAdjoinRootMonic.powerBasis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : PowerBasis R S

If f is monic, the powers of h.root form a basis.

Equations

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

@[simp]

theorem IsAdjoinRootMonic.powerBasis_gen {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : h.powerBasis.gen = h.root

@[simp]

theorem IsAdjoinRootMonic.powerBasis_basis {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : h.powerBasis.basis = h.basis

@[simp]

theorem IsAdjoinRootMonic.powerBasis_dim {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : h.powerBasis.dim = f.natDegree

@[simp]

theorem IsAdjoinRootMonic.basis_repr {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (x : S) (i : Fin f.natDegree) : (h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i

theorem IsAdjoinRootMonic.basis_one {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) : h.basis ⟨1, hdeg⟩ = h.root

theorem IsAdjoinRootMonic.finite {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : Module.Finite R S

theorem IsAdjoinRootMonic.finrank {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) [StrongRankCondition R] : Module.finrank R S = f.natDegree

def IsAdjoinRootMonic.liftPolyₗ {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {T : Type u_1} [AddCommGroup T] [Module R T] (g : Polynomial R →ₗ[R] T) : S →ₗ[R] T

IsAdjoinRootMonic.liftPolyₗ lifts a linear map on polynomials to a linear map on S.

Equations

• h.liftPolyₗ g = g ∘ₗ h.modByMonicHom

@[simp]

theorem IsAdjoinRootMonic.liftPolyₗ_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {T : Type u_1} [AddCommGroup T] [Module R T] (g : Polynomial R →ₗ[R] T) (a✝ : S) : (h.liftPolyₗ g) a✝ = g (h.modByMonicHom a✝)

def IsAdjoinRootMonic.coeff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : S →ₗ[R] ℕ → R

IsAdjoinRootMonic.coeff h x i is the ith coefficient of the representative of x : S.

Equations

• h.coeff = h.liftPolyₗ { toFun := Polynomial.coeff, map_add' := ⋯, map_smul' := ⋯ }

theorem IsAdjoinRootMonic.coeff_apply_lt {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : i < f.natDegree) : h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

theorem IsAdjoinRootMonic.coeff_apply_coe {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : Fin f.natDegree) : h.coeff z ↑i = (h.basis.repr z) i

theorem IsAdjoinRootMonic.coeff_apply_le {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : f.natDegree ≤ i) : h.coeff z i = 0

theorem IsAdjoinRootMonic.coeff_apply {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) : h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

theorem IsAdjoinRootMonic.coeff_root_pow {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {n : ℕ} (hn : n < f.natDegree) : h.coeff (h.root ^ n) = Pi.single n 1

theorem IsAdjoinRootMonic.coeff_one {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) [Nontrivial S] : h.coeff 1 = Pi.single 0 1

theorem IsAdjoinRootMonic.coeff_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree) : h.coeff h.root = Pi.single 1 1

theorem IsAdjoinRootMonic.coeff_algebraMap {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) [Nontrivial S] (x : R) : h.coeff ((algebraMap R S) x) = Pi.single 0 x

theorem IsAdjoinRootMonic.ext_elem {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) ⦃x y : S⦄ (hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i) : x = y

theorem IsAdjoinRootMonic.ext_elem_iff {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) {x y : S} : x = y ↔ ∀ i < f.natDegree, h.coeff x i = h.coeff y i

theorem IsAdjoinRootMonic.coeff_injective {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : Function.Injective ⇑h.coeff

theorem IsAdjoinRootMonic.isIntegral_root {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R} [Algebra R S] (h : IsAdjoinRootMonic S f) : IsIntegral R h.root

@[simp]

theorem IsAdjoinRoot.lift_self_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) (x : S) : (h.lift (algebraMap R S) h.root ⋯) x = x

theorem IsAdjoinRoot.lift_self {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) : h.lift (algebraMap R S) h.root ⋯ = RingHom.id S

def IsAdjoinRoot.mkOfAdjoinEqTop {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {α : S} (hα : IsIntegral R α) (hα₂ : Algebra.adjoin R {α} = ⊤) : IsAdjoinRoot S (minpoly R α)

If α generates S as an algebra, then S is given by adjoining a root of minpoly R α.

Equations

• IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂ = { map := Polynomial.aeval α, map_surjective := ⋯, ker_map := ⋯ }

@[reducible, inline]

abbrev IsAdjoinRootMonic.mkOfAdjoinEqTop {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {α : S} (hα : IsIntegral R α) (hα₂ : Algebra.adjoin R {α} = ⊤) : IsAdjoinRootMonic S (minpoly R α)

If α generates S as an algebra, then S is given by adjoining a root of minpoly R α.

Equations

• IsAdjoinRootMonic.mkOfAdjoinEqTop hα hα₂ = { toIsAdjoinRoot := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂, monic := ⋯ }

@[simp]

theorem IsAdjoinRoot.mkOfAdjoinEqTop_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {α : S} {hα : IsIntegral R α} {hα₂ : Algebra.adjoin R {α} = ⊤} : (mkOfAdjoinEqTop hα hα₂).root = α

@[simp]

theorem IsAdjoinRoot.lift_algEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [CommRing U] (i : R →+* U) (x : U) (hx : Polynomial.eval₂ i x f = 0) (z : S) : (h'.lift i x hx) ((h.algEquiv h') z) = (h.lift i x hx) z

@[deprecated IsAdjoinRoot.lift_algEquiv (since := "2025-08-13")]

theorem IsAdjoinRoot.lift_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [CommRing U] (i : R →+* U) (x : U) (hx : Polynomial.eval₂ i x f = 0) (z : S) : (h'.lift i x hx) ((h.algEquiv h') z) = (h.lift i x hx) z

Alias of IsAdjoinRoot.lift_algEquiv.

@[simp]

theorem IsAdjoinRoot.liftHom_algEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [CommRing U] [Algebra R U] (x : U) (hx : (Polynomial.aeval x) f = 0) (z : S) : (h'.liftHom x hx) ((h.algEquiv h') z) = (h.liftHom x hx) z

@[deprecated IsAdjoinRoot.liftHom_algEquiv (since := "2025-08-13")]

theorem IsAdjoinRoot.liftHom_aequiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot S f) {T : Type u_1} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2} [CommRing U] [Algebra R U] (x : U) (hx : (Polynomial.aeval x) f = 0) (z : S) : (h'.liftHom x hx) ((h.algEquiv h') z) = (h.liftHom x hx) z

Alias of IsAdjoinRoot.liftHom_algEquiv.

theorem IsAdjoinRootMonic.minpoly_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic S f) [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] (hirr : Irreducible f) : minpoly R h.root = f

theorem Algebra.adjoin.powerBasis'_minpoly_gen {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx' : IsIntegral R x) : minpoly R x = minpoly R (powerBasis' hx').gen

theorem IsAdjoinRoot.primitive_element_root {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {f : Polynomial F} (h : IsAdjoinRoot E f) : F⟮h.root⟯ = ⊤

@[reducible, inline]

abbrev IsAdjoinRoot.mkOfPrimitiveElement {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) : IsAdjoinRoot E (minpoly F α)

If α is primitive in E/f, then E is given by adjoining a root of minpoly F α.

Equations

• IsAdjoinRoot.mkOfPrimitiveElement hα hα₂ = IsAdjoinRoot.mkOfAdjoinEqTop hα ⋯

@[reducible, inline]

abbrev IsAdjoinRootMonic.mkOfPrimitiveElement {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) : IsAdjoinRootMonic E (minpoly F α)

If α is primitive in E/f, then E is given by adjoining a root of minpoly F α.

Equations

• IsAdjoinRootMonic.mkOfPrimitiveElement hα hα₂ = { toIsAdjoinRoot := IsAdjoinRoot.mkOfPrimitiveElement hα hα₂, monic := ⋯ }