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:
is_adjoin_root S f:Sis generated by adjoining a specified root off : R[X]toRis_adjoin_root_monic S f:Sis generated by adjoining a root of the monic polynomialf : R[X]toR
Using is_adjoin_root to map into S:
is_adjoin_root.map: inclusion fromR[X]toSis_adjoin_root.root: the specific root adjoined toRto giveS
Using is_adjoin_root to map out of S:
is_adjoin_root.repr: choose a non-unique representative inR[X]is_adjoin_root.lift,is_adjoin_root.lift_hom: lift a morphismR →+* TtoS →+* Tis_adjoin_root_monic.mod_by_monic_hom: a unique representative inR[X]iffis monic
Main results #
adjoin_root.is_adjoin_rootandadjoin_root.is_adjoin_root_monic:adjoin_rootsatisfies the conditions onis_adjoin_root(_monic)is_adjoin_root_monic.power_basis: therootgenerates a power basis onSoverRis_adjoin_root.aequiv: algebra isomorphism showing adjoining a root gives a unique ring up to isomorphismis_adjoin_root.of_equiv: transferis_adjoin_rootacross an algebra isomorphismis_adjoin_root_eq.minpoly_eq: the minimal polynomial of the adjoined root offis equal tof, iffis irreducible and monic, andRis a GCD domain
@[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)
- map : polynomial R →+* S
- map_surjective : function.surjective ⇑(self.map)
- ker_map : ring_hom.ker self.map = ideal.span {f}
- algebra_map_eq : algebra_map R S = self.map.comp polynomial.C
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)
- to_is_adjoin_root : is_adjoin_root S f
- monic : f.monic
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
- h.root = ⇑(h.map) polynomial.X
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) :
⇑(algebra_map R S) x = ⇑(h.map) (⇑polynomial.C x)
@[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} :
p ∈ ring_hom.ker h.map ↔ f ∣ p
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} :
@[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) :
⇑(h.map) polynomial.X = h.root
@[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) :
@[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) :
⇑(polynomial.aeval h.root) f = 0
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.
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) :
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) :
h.repr 0 ∈ ideal.span {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) :
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) :
polynomial.eval₂ i x (h.repr z) = polynomial.eval₂ i x w
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
- is_adjoin_root.lift i x hx h = {to_fun := λ (z : S), polynomial.eval₂ i x (h.repr z), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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) :
⇑(is_adjoin_root.lift i x hx h) (⇑(h.map) z) = polynomial.eval₂ i x z
@[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) :
⇑(is_adjoin_root.lift i x hx h) h.root = x
@[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) :
g = is_adjoin_root.lift i x hx h
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
- is_adjoin_root.lift_hom x hx' h = {to_fun := (is_adjoin_root.lift (algebra_map R T) x hx' h).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[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) :
↑(is_adjoin_root.lift_hom x hx' h) = is_adjoin_root.lift (algebra_map R T) x hx' h
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) :
⇑(is_adjoin_root.lift (algebra_map R T) x hx' h) z = ⇑(is_adjoin_root.lift_hom x hx' h) z
@[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) :
⇑(is_adjoin_root.lift_hom x hx' h) (⇑(h.map) z) = ⇑(polynomial.aeval x) z
@[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) :
⇑(is_adjoin_root.lift_hom x hx' h) h.root = x
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) :
g = is_adjoin_root.lift_hom x hx' h
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) :
is_adjoin_root (adjoin_root f) f
adjoin_root f is indeed given by adjoining a root of f.
Equations
- adjoin_root.is_adjoin_root f = {map := adjoin_root.mk f, map_surjective := _, ker_map := _, algebra_map_eq := _}
@[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
- adjoin_root.is_adjoin_root_monic f hf = {to_is_adjoin_root := {map := (adjoin_root.is_adjoin_root f).map, map_surjective := _, ker_map := _, algebra_map_eq := _}, monic := hf}
@[simp]
@[simp]
theorem
adjoin_root.is_adjoin_root_monic_map_eq_mk
{R : Type u}
[comm_ring R]
(f : polynomial R)
(hf : f.monic) :
@[simp]
@[simp]
theorem
adjoin_root.is_adjoin_root_monic_root_eq_root
{R : Type u}
[comm_ring R]
(f : polynomial R)
(hf : f.monic) :
theorem
is_adjoin_root_monic.map_mod_by_monic
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R S]
(h : is_adjoin_root_monic S f)
(g : polynomial R) :
⇑(h.to_is_adjoin_root.map) (g %ₘ f) = ⇑(h.to_is_adjoin_root.map) g
theorem
is_adjoin_root_monic.mod_by_monic_repr_map
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R S]
(h : is_adjoin_root_monic S f)
(g : polynomial R) :
h.to_is_adjoin_root.repr (⇑(h.to_is_adjoin_root.map) g) %ₘ f = g %ₘ f
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) :
S →ₗ[R] polynomial R
is_adjoin_root.mod_by_monic_hom sends the equivalence class of f mod g to f %ₘ g.
Equations
- h.mod_by_monic_hom = {to_fun := λ (x : S), h.to_is_adjoin_root.repr x %ₘ f, map_add' := _, map_smul' := _}
@[simp]
theorem
is_adjoin_root_monic.mod_by_monic_hom_map
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R S]
(h : is_adjoin_root_monic S f)
(g : polynomial R) :
⇑(h.mod_by_monic_hom) (⇑(h.to_is_adjoin_root.map) g) = g %ₘ f
@[simp]
theorem
is_adjoin_root_monic.map_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)
(x : S) :
⇑(h.to_is_adjoin_root.map) (⇑(h.mod_by_monic_hom) x) = x
@[simp]
theorem
is_adjoin_root_monic.mod_by_monic_hom_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 : ℕ}
(hdeg : n < f.nat_degree) :
⇑(h.mod_by_monic_hom) (h.to_is_adjoin_root.root ^ n) = polynomial.X ^ n
@[simp]
theorem
is_adjoin_root_monic.mod_by_monic_hom_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) :
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) :
basis (fin f.nat_degree) R S
The basis on S generated by powers of h.root.
Auxiliary definition for is_adjoin_root_monic.power_basis.
Equations
- h.basis = {repr := {to_fun := λ (x : S), finsupp.comap_domain coe (⇑(h.mod_by_monic_hom) x).to_finsupp _, map_add' := _, map_smul' := _, inv_fun := λ (g : fin f.nat_degree →₀ R), ⇑(h.to_is_adjoin_root.map) {to_finsupp := finsupp.map_domain coe g}, left_inv := _, right_inv := _}}
@[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) :
0 < f.nat_degree
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) :
f.nat_degree ≠ 0
@[simp]
theorem
is_adjoin_root_monic.power_basis_gen
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R 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) :
power_basis R S
If f is monic, the powers of h.root form a basis.
Equations
- h.power_basis = {gen := h.to_is_adjoin_root.root, dim := f.nat_degree, basis := h.basis, basis_eq_pow := _}
@[simp]
theorem
is_adjoin_root_monic.power_basis_dim
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R S]
(h : is_adjoin_root_monic S f) :
h.power_basis.dim = f.nat_degree
@[simp]
theorem
is_adjoin_root_monic.power_basis_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) :
h.power_basis.basis = h.basis
@[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
- h.lift_polyₗ g = g.comp h.mod_by_monic_hom
@[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) :
⇑(h.lift_polyₗ g) ᾰ = ⇑g (⇑(h.mod_by_monic_hom) ᾰ)
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
- h.coeff = h.lift_polyₗ {to_fun := polynomial.coeff ring.to_semiring, map_add' := _, map_smul' := _}
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) :
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) :
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) :
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 : ℕ) :
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) :
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.coeff_injective
{R : Type u}
{S : Type v}
[comm_ring R]
[ring S]
{f : polynomial R}
[algebra R S]
(h : is_adjoin_root_monic S f) :
theorem
is_adjoin_root_monic.is_integral_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) :
@[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) :
⇑(is_adjoin_root.lift (algebra_map R S) h.root _ h) x = x
theorem
is_adjoin_root.lift_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) :
is_adjoin_root.lift (algebra_map R S) h.root _ h = ring_hom.id 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.
@[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) :
@[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) :
@[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) :
h.aequiv h = alg_equiv.refl
@[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) :
@[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) :
⇑(is_adjoin_root.lift_hom x hx h') (⇑(h.aequiv h') z) = ⇑(is_adjoin_root.lift_hom x hx h) z
@[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) :
@[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) :
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) :
is_adjoin_root T f
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.
@[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) :
@[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) :
theorem
is_adjoin_root_monic.minpoly_eq
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
[algebra R S]
{f : polynomial R}
[is_domain R]
[is_domain S]
[no_zero_smul_divisors R S]
[is_integrally_closed R]
(h : is_adjoin_root_monic S f)
(hirr : irreducible f) :
minpoly R h.to_is_adjoin_root.root = f
theorem
algebra.adjoin.power_basis'_minpoly_gen
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
[algebra R S]
[is_domain R]
[is_domain S]
[no_zero_smul_divisors R S]
[is_integrally_closed R]
{x : S}
(hx' : is_integral R x) :
minpoly R x = minpoly R (algebra.adjoin.power_basis' hx').gen