mathlib3 documentation

ring_theory.is_adjoin_root

A predicate on adjoining roots of polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a predicate is_adjoin_root 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 ring_theory.adjoin_root, in order to provide an easier way to translate results from one to the other.

Motivation #

adjoin_root presents one construction of a ring R[α]. However, it is possible to obtain rings of this form in many ways, such as number_field.ring_of_integers ℚ(√-5), or algebra.adjoin R {α, α^2}, or intermediate_field.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:

Using is_adjoin_root to map into S:

Using is_adjoin_root to map out of S:

Main results #

@[nolint]
structure is_adjoin_root {R : Type u} (S : Type v) [comm_semiring R] [semiring S] [algebra R S] (f : polynomial R) :
Type (max u v)

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

Compare power_basis 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 adjoin_root which constructs a new type.

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

Instances for is_adjoin_root
  • is_adjoin_root.has_sizeof_inst
@[nolint]
structure is_adjoin_root_monic {R : Type u} (S : Type v) [comm_semiring R] [semiring S] [algebra R S] (f : polynomial R) :
Type (max u v)

is_adjoin_root_monic 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 mod_by_monic_hom and coeff). In particular, we have is_adjoin_root_monic.power_basis.

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.

Instances for is_adjoin_root_monic
  • is_adjoin_root_monic.has_sizeof_inst
noncomputable def is_adjoin_root.root {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) :
S

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

Equations
theorem is_adjoin_root.subsingleton {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) [subsingleton R] :
theorem is_adjoin_root.algebra_map_apply {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) (x : R) :
@[simp]
theorem is_adjoin_root.mem_ker_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) {p : polynomial R} :
theorem is_adjoin_root.map_eq_zero_iff {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) {p : polynomial R} :
(h.map) p = 0 f p
@[simp]
theorem is_adjoin_root.map_X {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) :
@[simp]
theorem is_adjoin_root.map_self {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) :
(h.map) f = 0
@[simp]
theorem is_adjoin_root.aeval_eq {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) (p : polynomial R) :
@[simp]
theorem is_adjoin_root.aeval_root {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) :
noncomputable def is_adjoin_root.repr {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) (x : S) :

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

If f is monic, use is_adjoin_root_monic.mod_by_monic_hom for a unique choice of representative.

Equations
theorem is_adjoin_root.map_repr {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) (x : S) :
(h.map) (h.repr x) = x
theorem is_adjoin_root.repr_zero_mem_span {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root S f) :

repr preserves zero, up to multiples of f

theorem is_adjoin_root.repr_add_sub_repr_add_repr_mem_span {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root 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

theorem is_adjoin_root.ext_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h h' : is_adjoin_root S f) (eq : (x : polynomial R), (h.map) x = (h'.map) x) :
h = h'

Extensionality of the is_adjoin_root structure itself. See is_adjoin_root_monic.ext_elem for extensionality of the ring elements.

@[ext]
theorem is_adjoin_root.ext {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h h' : is_adjoin_root S f) (eq : h.root = h'.root) :
h = h'

Extensionality of the is_adjoin_root structure itself. See is_adjoin_root_monic.ext_elem for extensionality of the ring elements.

theorem is_adjoin_root.eval₂_repr_eq_eval₂_of_map_eq {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) (z : S) (w : polynomial R) (hzw : (h.map) w = z) :

Auxiliary lemma for is_adjoin_root.lift

noncomputable def is_adjoin_root.lift {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] (i : R →+* T) (x : T) (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) :
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
@[simp]
theorem is_adjoin_root.lift_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) (z : polynomial R) :
@[simp]
theorem is_adjoin_root.lift_root {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) :
@[simp]
theorem is_adjoin_root.lift_algebra_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) (a : R) :
(is_adjoin_root.lift i x hx h) ((algebra_map R S) a) = i a
theorem is_adjoin_root.apply_eq_lift {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) (g : S →+* T) (hmap : (a : R), g ((algebra_map R S) a) = i a) (hroot : g h.root = x) (a : S) :
g a = (is_adjoin_root.lift i x hx h) a

Auxiliary lemma for apply_eq_lift

theorem is_adjoin_root.eq_lift {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {i : R →+* T} {x : T} (hx : polynomial.eval₂ i x f = 0) (h : is_adjoin_root S f) (g : S →+* T) (hmap : (a : R), g ((algebra_map R S) a) = i a) (hroot : g h.root = x) :

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

noncomputable def is_adjoin_root.lift_hom {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] (x : T) [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) :

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
@[simp]
theorem is_adjoin_root.coe_lift_hom {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {x : T} [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) :
theorem is_adjoin_root.lift_algebra_map_apply {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {x : T} [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) (z : S) :
@[simp]
theorem is_adjoin_root.lift_hom_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {x : T} [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) (z : polynomial R) :
@[simp]
theorem is_adjoin_root.lift_hom_root {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {x : T} [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) :
theorem is_adjoin_root.eq_lift_hom {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [comm_ring T] {x : T} [algebra R T] (hx' : (polynomial.aeval x) f = 0) (h : is_adjoin_root S f) (g : S →ₐ[R] T) (hroot : g h.root = x) :

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

@[protected]
noncomputable def adjoin_root.is_adjoin_root {R : Type u} [comm_ring R] (f : polynomial R) :

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

Equations
@[protected]
noncomputable def adjoin_root.is_adjoin_root_monic {R : Type u} [comm_ring R] (f : polynomial R) (hf : f.monic) :

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

Equations
noncomputable def is_adjoin_root_monic.mod_by_monic_hom {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) :

is_adjoin_root.mod_by_monic_hom sends the equivalence class of f mod g to f %ₘ g.

Equations
@[simp]
noncomputable def is_adjoin_root_monic.basis {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) :

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

Auxiliary definition for is_adjoin_root_monic.power_basis.

Equations
@[simp]
theorem is_adjoin_root_monic.basis_apply {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (i : fin f.nat_degree) :
theorem is_adjoin_root_monic.deg_pos {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] [nontrivial S] (h : is_adjoin_root_monic S f) :
theorem is_adjoin_root_monic.deg_ne_zero {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] [nontrivial S] (h : is_adjoin_root_monic S f) :
noncomputable def is_adjoin_root_monic.power_basis {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) :

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

Equations
@[simp]
@[simp]
@[simp]
theorem is_adjoin_root_monic.basis_repr {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (x : S) (i : fin f.nat_degree) :
theorem is_adjoin_root_monic.basis_one {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (hdeg : 1 < f.nat_degree) :
noncomputable def is_adjoin_root_monic.lift_polyₗ {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [add_comm_group T] [module R T] (h : is_adjoin_root_monic S f) (g : polynomial R →ₗ[R] T) :

is_adjoin_root_monic.lift_polyₗ lifts a linear map on polynomials to a linear map on S.

Equations
@[simp]
theorem is_adjoin_root_monic.lift_polyₗ_apply {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] {T : Type u_1} [add_comm_group T] [module R T] (h : is_adjoin_root_monic S f) (g : polynomial R →ₗ[R] T) (ᾰ : S) :
noncomputable def is_adjoin_root_monic.coeff {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) :

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

Equations
theorem is_adjoin_root_monic.coeff_apply_lt {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (z : S) (i : ) (hi : i < f.nat_degree) :
(h.coeff) z i = ((h.basis.repr) z) i, hi⟩
theorem is_adjoin_root_monic.coeff_apply_coe {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (z : S) (i : fin f.nat_degree) :
(h.coeff) z i = ((h.basis.repr) z) i
theorem is_adjoin_root_monic.coeff_apply_le {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (z : S) (i : ) (hi : f.nat_degree i) :
(h.coeff) z i = 0
theorem is_adjoin_root_monic.coeff_apply {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (z : S) (i : ) :
(h.coeff) z i = dite (i < f.nat_degree) (λ (hi : i < f.nat_degree), ((h.basis.repr) z) i, hi⟩) (λ (hi : ¬i < f.nat_degree), 0)
theorem is_adjoin_root_monic.coeff_root_pow {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) {n : } (hn : n < f.nat_degree) :
theorem is_adjoin_root_monic.coeff_one {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] [nontrivial S] (h : is_adjoin_root_monic S f) :
(h.coeff) 1 = pi.single 0 1
theorem is_adjoin_root_monic.coeff_root {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) (hdeg : 1 < f.nat_degree) :
theorem is_adjoin_root_monic.coeff_algebra_map {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] [nontrivial S] (h : is_adjoin_root_monic S f) (x : R) :
theorem is_adjoin_root_monic.ext_elem {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) ⦃x y : S⦄ (hxy : (i : ), i < f.nat_degree (h.coeff) x i = (h.coeff) y i) :
x = y
theorem is_adjoin_root_monic.ext_elem_iff {R : Type u} {S : Type v} [comm_ring R] [ring S] {f : polynomial R} [algebra R S] (h : is_adjoin_root_monic S f) {x y : S} :
x = y (i : ), i < f.nat_degree (h.coeff) x i = (h.coeff) y i
@[simp]
theorem is_adjoin_root.lift_self_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} (h : is_adjoin_root S f) (x : S) :
noncomputable def is_adjoin_root.aequiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) :

Adjoining a root gives a unique ring up to algebra isomorphism.

This is the converse of is_adjoin_root.of_equiv: this turns an is_adjoin_root into an alg_equiv, and is_adjoin_root.of_equiv turns an alg_equiv into an is_adjoin_root.

Equations
@[simp]
theorem is_adjoin_root.aequiv_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (z : polynomial R) :
(h.aequiv h') ((h.map) z) = (h'.map) z
@[simp]
theorem is_adjoin_root.aequiv_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) :
(h.aequiv h') h.root = h'.root
@[simp]
theorem is_adjoin_root.aequiv_self {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} (h : is_adjoin_root S f) :
@[simp]
theorem is_adjoin_root.aequiv_symm {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) :
(h.aequiv h').symm = h'.aequiv h
@[simp]
theorem is_adjoin_root.lift_aequiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (i : R →+* U) (x : U) (hx : polynomial.eval₂ i x f = 0) (z : S) :
(is_adjoin_root.lift i x hx h') ((h.aequiv h') z) = (is_adjoin_root.lift i x hx h) z
@[simp]
theorem is_adjoin_root.lift_hom_aequiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] [algebra R U] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (x : U) (hx : (polynomial.aeval x) f = 0) (z : S) :
@[simp]
theorem is_adjoin_root.aequiv_aequiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] [algebra R U] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (h'' : is_adjoin_root U f) (x : S) :
(h'.aequiv h'') ((h.aequiv h') x) = (h.aequiv h'') x
@[simp]
theorem is_adjoin_root.aequiv_trans {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] [algebra R U] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (h'' : is_adjoin_root U f) :
(h.aequiv h').trans (h'.aequiv h'') = h.aequiv h''
noncomputable def is_adjoin_root.of_equiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (e : S ≃ₐ[R] T) :

Transfer is_adjoin_root across an algebra isomorphism.

This is the converse of is_adjoin_root.aequiv: this turns an alg_equiv into an is_adjoin_root, and is_adjoin_root.aequiv turns an is_adjoin_root into an alg_equiv.

Equations
@[simp]
theorem is_adjoin_root.of_equiv_map_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (e : S ≃ₐ[R] T) (ᾰ : polynomial R) :
((h.of_equiv e).map) = e ((h.map) ᾰ)
@[simp]
theorem is_adjoin_root.of_equiv_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] (h : is_adjoin_root S f) (e : S ≃ₐ[R] T) :
@[simp]
theorem is_adjoin_root.aequiv_of_equiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] [algebra R U] (h : is_adjoin_root S f) (h' : is_adjoin_root T f) (e : T ≃ₐ[R] U) :
h.aequiv (h'.of_equiv e) = (h.aequiv h').trans e
@[simp]
theorem is_adjoin_root.of_equiv_aequiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {f : polynomial R} {T : Type u_1} [comm_ring T] [algebra R T] {U : Type u_2} [comm_ring U] [algebra R U] (h : is_adjoin_root S f) (h' : is_adjoin_root U f) (e : S ≃ₐ[R] T) :
(h.of_equiv e).aequiv h' = e.symm.trans (h.aequiv h')