ring_theory.adjoin_root - mathlib3 docs

def adjoin_root {R : Type u} [comm_ring R] (f : polynomial R) :

Adjoin a root of a polynomial f to a commutative ring R. We define the new ring as the quotient of R[X] by the principal ideal generated by f.

Equations

adjoin_root f = (polynomial R ⧸ ideal.span {f})

Instances for adjoin_root

source

@[protected, instance]

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

comm_ring (adjoin_root f)

Equations

adjoin_root.comm_ring f = ideal.quotient.comm_ring (ideal.span {f})

source

@[protected, instance]

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

inhabited (adjoin_root f)

Equations

adjoin_root.inhabited f = {default := 0}

source

@[protected, instance]

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

decidable_eq (adjoin_root f)

Equations

adjoin_root.decidable_eq f = classical.dec_eq (adjoin_root f)

source

@[protected]

theorem adjoin_root.nontrivial {R : Type u} [comm_ring R] (f : polynomial R) [is_domain R] (h : f.degree ≠ 0) :

nontrivial (adjoin_root f)

source

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

polynomial R →+* adjoin_root f

Ring homomorphism from R[x] to adjoin_root f sending X to the root.

Equations

adjoin_root.mk f = ideal.quotient.mk (ideal.span {f})

source

theorem adjoin_root.induction_on {R : Type u} [comm_ring R] (f : polynomial R) {C : adjoin_root f → Prop} (x : adjoin_root f) (ih : ∀ (p : polynomial R), C (⇑(adjoin_root.mk f) p)) :

C x

source

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

R →+* adjoin_root f

Embedding of the original ring R into adjoin_root f.

Equations

adjoin_root.of f = (adjoin_root.mk f).comp polynomial.C

source

@[protected, instance]

noncomputable def adjoin_root.has_smul {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [distrib_smul S R] [is_scalar_tower S R R] :

has_smul S (adjoin_root f)

Equations

adjoin_root.has_smul f = submodule.quotient.has_smul' (ideal.span {f})

source

@[protected, instance]

noncomputable def adjoin_root.distrib_smul {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [distrib_smul S R] [is_scalar_tower S R R] :

distrib_smul S (adjoin_root f)

Equations

adjoin_root.distrib_smul f = submodule.quotient.distrib_smul' (ideal.span {f})

source

@[simp]

theorem adjoin_root.smul_mk {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [distrib_smul S R] [is_scalar_tower S R R] (a : S) (x : polynomial R) :

a • ⇑(adjoin_root.mk f) x = ⇑(adjoin_root.mk f) (a • x)

source

theorem adjoin_root.smul_of {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [distrib_smul S R] [is_scalar_tower S R R] (a : S) (x : R) :

a • ⇑(adjoin_root.of f) x = ⇑(adjoin_root.of f) (a • x)

source

@[protected, instance]

def adjoin_root.is_scalar_tower {R : Type u} [comm_ring R] (R₁ : Type u_1) (R₂ : Type u_2) [has_smul R₁ R₂] [distrib_smul R₁ R] [distrib_smul R₂ R] [is_scalar_tower R₁ R R] [is_scalar_tower R₂ R R] [is_scalar_tower R₁ R₂ R] (f : polynomial R) :

is_scalar_tower R₁ R₂ (adjoin_root f)

source

@[protected, instance]

def adjoin_root.smul_comm_class {R : Type u} [comm_ring R] (R₁ : Type u_1) (R₂ : Type u_2) [distrib_smul R₁ R] [distrib_smul R₂ R] [is_scalar_tower R₁ R R] [is_scalar_tower R₂ R R] [smul_comm_class R₁ R₂ R] (f : polynomial R) :

smul_comm_class R₁ R₂ (adjoin_root f)

source

@[protected, instance]

def adjoin_root.is_scalar_tower_right {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [distrib_smul S R] [is_scalar_tower S R R] :

is_scalar_tower S (adjoin_root f) (adjoin_root f)

source

@[protected, instance]

noncomputable def adjoin_root.distrib_mul_action {R : Type u} {S : Type v} [comm_ring R] [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (f : polynomial R) :

distrib_mul_action S (adjoin_root f)

Equations

adjoin_root.distrib_mul_action f = submodule.quotient.distrib_mul_action' (ideal.span {f})

source

@[protected, instance]

noncomputable def adjoin_root.algebra {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_semiring S] [algebra S R] :

algebra S (adjoin_root f)

Equations

adjoin_root.algebra f = ideal.quotient.algebra S

source

@[simp]

theorem adjoin_root.algebra_map_eq {R : Type u} [comm_ring R] (f : polynomial R) :

algebra_map R (adjoin_root f) = adjoin_root.of f

source

theorem adjoin_root.algebra_map_eq' {R : Type u} (S : Type v) [comm_ring R] (f : polynomial R) [comm_semiring S] [algebra S R] :

algebra_map S (adjoin_root f) = (adjoin_root.of f).comp (algebra_map S R)

source

theorem adjoin_root.finite_type {R : Type u} [comm_ring R] (f : polynomial R) :

algebra.finite_type R (adjoin_root f)

source

theorem adjoin_root.finite_presentation {R : Type u} [comm_ring R] (f : polynomial R) :

algebra.finite_presentation R (adjoin_root f)

source

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

adjoin_root f

The adjoined root.

Equations

adjoin_root.root f = ⇑(adjoin_root.mk f) polynomial.X

source

@[protected, instance]

noncomputable def adjoin_root.has_coe_t {R : Type u} [comm_ring R] {f : polynomial R} :

has_coe_t R (adjoin_root f)

Equations

adjoin_root.has_coe_t = {coe := ⇑(adjoin_root.of f)}

source

@[ext]

theorem adjoin_root.alg_hom_ext {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [semiring S] [algebra R S] {g₁ g₂ : adjoin_root f →ₐ[R] S} (h : ⇑g₁ (adjoin_root.root f) = ⇑g₂ (adjoin_root.root f)) :

g₁ = g₂

Two R-alg_hom from adjoin_root f to the same R-algebra are the same iff they agree on root f.

source

@[simp]

theorem adjoin_root.mk_eq_mk {R : Type u} [comm_ring R] {f g h : polynomial R} :

⇑(adjoin_root.mk f) g = ⇑(adjoin_root.mk f) h ↔ f ∣ g - h

source

@[simp]

theorem adjoin_root.mk_eq_zero {R : Type u} [comm_ring R] {f g : polynomial R} :

⇑(adjoin_root.mk f) g = 0 ↔ f ∣ g

source

@[simp]

theorem adjoin_root.mk_self {R : Type u} [comm_ring R] {f : polynomial R} :

⇑(adjoin_root.mk f) f = 0

source

@[simp]

theorem adjoin_root.mk_C {R : Type u} [comm_ring R] {f : polynomial R} (x : R) :

⇑(adjoin_root.mk f) (⇑polynomial.C x) = ↑x

source

@[simp]

theorem adjoin_root.mk_X {R : Type u} [comm_ring R] {f : polynomial R} :

⇑(adjoin_root.mk f) polynomial.X = adjoin_root.root f

source

theorem adjoin_root.mk_ne_zero_of_degree_lt {R : Type u} [comm_ring R] {f : polynomial R} (hf : f.monic) {g : polynomial R} (h0 : g ≠ 0) (hd : g.degree < f.degree) :

⇑(adjoin_root.mk f) g ≠ 0

source

theorem adjoin_root.mk_ne_zero_of_nat_degree_lt {R : Type u} [comm_ring R] {f : polynomial R} (hf : f.monic) {g : polynomial R} (h0 : g ≠ 0) (hd : g.nat_degree < f.nat_degree) :

⇑(adjoin_root.mk f) g ≠ 0

source

@[simp]

theorem adjoin_root.aeval_eq {R : Type u} [comm_ring R] {f : polynomial R} (p : polynomial R) :

⇑(polynomial.aeval (adjoin_root.root f)) p = ⇑(adjoin_root.mk f) p

source

theorem adjoin_root.adjoin_root_eq_top {R : Type u} [comm_ring R] {f : polynomial R} :

algebra.adjoin R {adjoin_root.root f} = ⊤

source

@[simp]

theorem adjoin_root.eval₂_root {R : Type u} [comm_ring R] (f : polynomial R) :

polynomial.eval₂ (adjoin_root.of f) (adjoin_root.root f) f = 0

source

theorem adjoin_root.is_root_root {R : Type u} [comm_ring R] (f : polynomial R) :

(polynomial.map (adjoin_root.of f) f).is_root (adjoin_root.root f)

source

theorem adjoin_root.is_algebraic_root {R : Type u} [comm_ring R] {f : polynomial R} (hf : f ≠ 0) :

is_algebraic R (adjoin_root.root f)

source

theorem adjoin_root.of.injective_of_degree_ne_zero {R : Type u} [comm_ring R] {f : polynomial R} [is_domain R] (hf : f.degree ≠ 0) :

function.injective ⇑(adjoin_root.of f)

source

noncomputable def adjoin_root.lift {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] (i : R →+* S) (x : S) (h : polynomial.eval₂ i x f = 0) :

adjoin_root f →+* S

Lift a ring homomorphism i : R →+* S to adjoin_root f →+* S.

Equations

adjoin_root.lift i x h = ideal.quotient.lift (ideal.span {f}) (polynomial.eval₂_ring_hom i x) _

source

@[simp]

theorem adjoin_root.lift_mk {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : polynomial.eval₂ i a f = 0) (g : polynomial R) :

⇑(adjoin_root.lift i a h) (⇑(adjoin_root.mk f) g) = polynomial.eval₂ i a g

source

@[simp]

theorem adjoin_root.lift_root {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : polynomial.eval₂ i a f = 0) :

⇑(adjoin_root.lift i a h) (adjoin_root.root f) = a

source

@[simp]

theorem adjoin_root.lift_of {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : polynomial.eval₂ i a f = 0) {x : R} :

⇑(adjoin_root.lift i a h) ↑x = ⇑i x

source

@[simp]

theorem adjoin_root.lift_comp_of {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : polynomial.eval₂ i a f = 0) :

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

source

noncomputable def adjoin_root.lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [algebra R S] (x : S) (hfx : ⇑(polynomial.aeval x) f = 0) :

adjoin_root f →ₐ[R] S

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

Equations

adjoin_root.lift_hom f x hfx = {to_fun := (adjoin_root.lift (algebra_map R S) x hfx).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem adjoin_root.coe_lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [algebra R S] (x : S) (hfx : ⇑(polynomial.aeval x) f = 0) :

↑(adjoin_root.lift_hom f x hfx) = adjoin_root.lift (algebra_map R S) x hfx

source

@[simp]

theorem adjoin_root.aeval_alg_hom_eq_zero {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [algebra R S] (ϕ : adjoin_root f →ₐ[R] S) :

⇑(polynomial.aeval (⇑ϕ (adjoin_root.root f))) f = 0

source

@[simp]

theorem adjoin_root.lift_hom_eq_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (f : polynomial R) (ϕ : adjoin_root f →ₐ[R] S) :

adjoin_root.lift_hom f (⇑ϕ (adjoin_root.root f)) _ = ϕ

source

@[simp]

theorem adjoin_root.lift_hom_mk {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : ⇑(polynomial.aeval a) f = 0) {g : polynomial R} :

⇑(adjoin_root.lift_hom f a hfx) (⇑(adjoin_root.mk f) g) = ⇑(polynomial.aeval a) g

source

@[simp]

theorem adjoin_root.lift_hom_root {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : ⇑(polynomial.aeval a) f = 0) :

⇑(adjoin_root.lift_hom f a hfx) (adjoin_root.root f) = a

source

@[simp]

theorem adjoin_root.lift_hom_of {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : ⇑(polynomial.aeval a) f = 0) {x : R} :

⇑(adjoin_root.lift_hom f a hfx) (⇑(adjoin_root.of f) x) = ⇑(algebra_map R S) x

source

@[simp]

theorem adjoin_root.root_is_inv {R : Type u} [comm_ring R] (r : R) :

⇑(adjoin_root.of (⇑polynomial.C r * polynomial.X - 1)) r * adjoin_root.root (⇑polynomial.C r * polynomial.X - 1) = 1

source

theorem adjoin_root.alg_hom_subsingleton {R : Type u} [comm_ring R] {S : Type u_1} [comm_ring S] [algebra R S] {r : R} :

subsingleton (adjoin_root (⇑polynomial.C r * polynomial.X - 1) →ₐ[R] S)

source

theorem adjoin_root.is_domain_of_prime {R : Type u} [comm_ring R] {f : polynomial R} (hf : prime f) :

is_domain (adjoin_root f)

source

theorem adjoin_root.no_zero_smul_divisors_of_prime_of_degree_ne_zero {R : Type u} [comm_ring R] {f : polynomial R} [is_domain R] (hf : prime f) (hf' : f.degree ≠ 0) :

no_zero_smul_divisors R (adjoin_root f)

source

@[protected, instance]

def adjoin_root.span_maximal_of_irreducible {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :

(ideal.span {f}).is_maximal

source

@[protected, instance]

noncomputable def adjoin_root.field {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :

field (adjoin_root f)

Equations

adjoin_root.field = {add := comm_ring.add (adjoin_root.comm_ring f), add_assoc := _, zero := comm_ring.zero (adjoin_root.comm_ring f), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (adjoin_root.comm_ring f), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (adjoin_root.comm_ring f), sub := comm_ring.sub (adjoin_root.comm_ring f), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (adjoin_root.comm_ring f), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast (adjoin_root.comm_ring f), nat_cast := comm_ring.nat_cast (adjoin_root.comm_ring f), one := comm_ring.one (adjoin_root.comm_ring f), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul (adjoin_root.comm_ring f), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow (adjoin_root.comm_ring f), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := group_with_zero.inv (ideal.quotient.group_with_zero (ideal.span {f})), div := group_with_zero.div (ideal.quotient.group_with_zero (ideal.span {f})), div_eq_mul_inv := _, zpow := group_with_zero.zpow (ideal.quotient.group_with_zero (ideal.span {f})), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := λ (a : ℚ), ⇑(adjoin_root.of f) ↑a, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := has_smul.smul (adjoin_root.has_smul f), qsmul_eq_mul' := _}

source

theorem adjoin_root.coe_injective {K : Type w} [field K] {f : polynomial K} (h : f.degree ≠ 0) :

function.injective coe

source

theorem adjoin_root.coe_injective' {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :

function.injective coe

source

theorem adjoin_root.mul_div_root_cancel {K : Type w} [field K] (f : polynomial K) [fact (irreducible f)] :

(polynomial.X - ⇑polynomial.C (adjoin_root.root f)) * (polynomial.map (adjoin_root.of f) f / (polynomial.X - ⇑polynomial.C (adjoin_root.root f))) = polynomial.map (adjoin_root.of f) f

source

@[protected, instance]

def adjoin_root.is_noetherian_ring {R : Type u} [comm_ring R] [is_noetherian_ring R] {f : polynomial R} :

is_noetherian_ring (adjoin_root f)

source

theorem adjoin_root.is_integral_root' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

is_integral R (adjoin_root.root g)

source

noncomputable def adjoin_root.mod_by_monic_hom {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

adjoin_root g →ₗ[R] polynomial R

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

This is a well-defined right inverse to adjoin_root.mk, see adjoin_root.mk_left_inverse.

Equations

adjoin_root.mod_by_monic_hom hg = ((submodule.restrict_scalars R (ideal.span {g})).liftq g.mod_by_monic_hom _).comp (submodule.quotient.restrict_scalars_equiv R (ideal.span {g})).symm.to_linear_map

source

@[simp]

theorem adjoin_root.mod_by_monic_hom_mk {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (f : polynomial R) :

⇑(adjoin_root.mod_by_monic_hom hg) (⇑(adjoin_root.mk g) f) = f %ₘ g

source

theorem adjoin_root.mk_left_inverse {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

function.left_inverse ⇑(adjoin_root.mk g) ⇑(adjoin_root.mod_by_monic_hom hg)

source

theorem adjoin_root.mk_surjective {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

function.surjective ⇑(adjoin_root.mk g)

source

noncomputable def adjoin_root.power_basis_aux' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

basis (fin g.nat_degree) R (adjoin_root g)

The elements 1, root g, ..., root g ^ (d - 1) form a basis for adjoin_root g, where g is a monic polynomial of degree d.

Equations

adjoin_root.power_basis_aux' hg = basis.of_equiv_fun {to_fun := λ (f : adjoin_root g) (i : fin g.nat_degree), (⇑(adjoin_root.mod_by_monic_hom hg) f).coeff ↑i, map_add' := _, map_smul' := _, inv_fun := λ (c : fin g.nat_degree → R), ⇑(adjoin_root.mk g) (finset.univ.sum (λ (i : fin g.nat_degree), ⇑(polynomial.monomial ↑i) (c i))), left_inv := _, right_inv := _}

source

@[simp]

theorem adjoin_root.power_basis_aux'_repr_symm_apply {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (c : fin g.nat_degree →₀ R) :

⇑((adjoin_root.power_basis_aux' hg).repr.symm) c = ⇑(adjoin_root.mk g) (finset.univ.sum (λ (i : fin g.nat_degree), ⇑(polynomial.monomial ↑i) (⇑c i)))

This lemma could be autogenerated by @[simps] but unfortunately that would require unfolding that causes a timeout.

source

@[simp]

theorem adjoin_root.power_basis_aux'_repr_apply_to_fun {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (f : adjoin_root g) (i : fin g.nat_degree) :

⇑(⇑((adjoin_root.power_basis_aux' hg).repr) f) i = (⇑(adjoin_root.mod_by_monic_hom hg) f).coeff ↑i

This lemma could be autogenerated by @[simps] but unfortunately that would require unfolding that causes a timeout.

source

@[simp]

theorem adjoin_root.power_basis'_dim {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

(adjoin_root.power_basis' hg).dim = g.nat_degree

source

noncomputable def adjoin_root.power_basis' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

power_basis R (adjoin_root g)

The power basis 1, root g, ..., root g ^ (d - 1) for adjoin_root g, where g is a monic polynomial of degree d.

Equations

adjoin_root.power_basis' hg = {gen := adjoin_root.root g, dim := g.nat_degree, basis := adjoin_root.power_basis_aux' hg, basis_eq_pow := _}

source

@[simp]

theorem adjoin_root.power_basis'_gen {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

(adjoin_root.power_basis' hg).gen = adjoin_root.root g

source

theorem adjoin_root.is_integral_root {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

is_integral K (adjoin_root.root f)

source

theorem adjoin_root.minpoly_root {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

minpoly K (adjoin_root.root f) = f * ⇑polynomial.C (f.leading_coeff)⁻¹

source

noncomputable def adjoin_root.power_basis_aux {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

basis (fin f.nat_degree) K (adjoin_root f)

The elements 1, root f, ..., root f ^ (d - 1) form a basis for adjoin_root f, where f is an irreducible polynomial over a field of degree d.

Equations

adjoin_root.power_basis_aux hf = let f' : polynomial K := f * ⇑polynomial.C (f.leading_coeff)⁻¹ in basis.mk _ _

source

@[simp]

theorem adjoin_root.power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

(adjoin_root.power_basis hf).gen = adjoin_root.root f

source

noncomputable def adjoin_root.power_basis {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

power_basis K (adjoin_root f)

The power basis 1, root f, ..., root f ^ (d - 1) for adjoin_root f, where f is an irreducible polynomial over a field of degree d.

Equations

adjoin_root.power_basis hf = {gen := adjoin_root.root f, dim := f.nat_degree, basis := adjoin_root.power_basis_aux hf, basis_eq_pow := _}

source

@[simp]

theorem adjoin_root.power_basis_dim {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

(adjoin_root.power_basis hf).dim = f.nat_degree

source

theorem adjoin_root.minpoly_power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :

minpoly K (adjoin_root.power_basis hf).gen = f * ⇑polynomial.C (f.leading_coeff)⁻¹

source

theorem adjoin_root.minpoly_power_basis_gen_of_monic {K : Type w} [field K] {f : polynomial K} (hf : f.monic) (hf' : f ≠ 0 := _) :

minpoly K (adjoin_root.power_basis hf').gen = f

source

@[simp]

theorem adjoin_root.minpoly.to_adjoin_apply (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) (ᾰ : adjoin_root (minpoly R x)) :

⇑(adjoin_root.minpoly.to_adjoin R x) ᾰ = ⇑(adjoin_root.lift (algebra_map R ↥(algebra.adjoin R {x})) ⟨x, _⟩ _) ᾰ

source

noncomputable def adjoin_root.minpoly.to_adjoin (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) :

adjoin_root (minpoly R x) →ₐ[R] ↥(algebra.adjoin R {x})

The surjective algebra morphism R[X]/(minpoly R x) → R[x]. If R is a GCD domain and x is integral, this is an isomorphism, see adjoin_root.minpoly.equiv_adjoin.

Equations

adjoin_root.minpoly.to_adjoin R x = adjoin_root.lift_hom (minpoly R x) ⟨x, _⟩ _

source

theorem adjoin_root.minpoly.to_adjoin_apply' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} (a : adjoin_root (minpoly R x)) :

⇑(adjoin_root.minpoly.to_adjoin R x) a = ⇑(adjoin_root.lift_hom (minpoly R x) ⟨x, _⟩ _) a

source

theorem adjoin_root.minpoly.to_adjoin.apply_X {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} :

⇑(adjoin_root.minpoly.to_adjoin R x) (⇑(adjoin_root.mk (minpoly R x)) polynomial.X) = ⟨x, _⟩

source

theorem adjoin_root.minpoly.to_adjoin.surjective (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) :

function.surjective ⇑(adjoin_root.minpoly.to_adjoin R x)

source

@[simp]

theorem adjoin_root.equiv'_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : ⇑(polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : ⇑(polynomial.aeval pb.gen) g = 0) :

⇑((adjoin_root.equiv' g pb h₁ h₂).symm) = ⇑(pb.lift (adjoin_root.root g) h₁)

source

noncomputable def adjoin_root.equiv' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : ⇑(polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : ⇑(polynomial.aeval pb.gen) g = 0) :

adjoin_root g ≃ₐ[R] S

If S is an extension of R with power basis pb and g is a monic polynomial over R such that pb.gen has a minimal polynomial g, then S is isomorphic to adjoin_root g.

Compare power_basis.equiv_of_root, which would require h₂ : aeval pb.gen (minpoly R (root g)) = 0; that minimal polynomial is not guaranteed to be identical to g.

Equations

adjoin_root.equiv' g pb h₁ h₂ = {to_fun := ⇑(adjoin_root.lift_hom g pb.gen h₂), inv_fun := ⇑(pb.lift (adjoin_root.root g) h₁), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem adjoin_root.equiv'_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : ⇑(polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : ⇑(polynomial.aeval pb.gen) g = 0) :

⇑(adjoin_root.equiv' g pb h₁ h₂) = ⇑(adjoin_root.lift_hom g pb.gen h₂)

source

@[simp]

theorem adjoin_root.equiv'_to_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : ⇑(polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : ⇑(polynomial.aeval pb.gen) g = 0) :

(adjoin_root.equiv' g pb h₁ h₂).to_alg_hom = adjoin_root.lift_hom g pb.gen h₂

source

@[simp]

theorem adjoin_root.equiv'_symm_to_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : ⇑(polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : ⇑(polynomial.aeval pb.gen) g = 0) :

(adjoin_root.equiv' g pb h₁ h₂).symm.to_alg_hom = pb.lift (adjoin_root.root g) h₁

source

noncomputable def adjoin_root.equiv (L : Type u_1) (F : Type u_2) [field F] [field L] [algebra F L] (f : polynomial F) (hf : f ≠ 0) :

(adjoin_root f →ₐ[F] L) ≃ {x // x ∈ (polynomial.map (algebra_map F L) f).roots}

If L is a field extension of F and f is a polynomial over F then the set of maps from F[x]/(f) into L is in bijection with the set of roots of f in L.

Equations

adjoin_root.equiv L F f hf = (adjoin_root.power_basis hf).lift_equiv'.trans ((equiv.refl L).subtype_equiv _)

source

noncomputable def adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

adjoin_root f ⧸ ideal.map (adjoin_root.of f) I ≃+* adjoin_root f ⧸ ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I)

The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f)) for α a root of f : R[X] and I : ideal R.

See adjoin_root.quot_map_of_equiv for the isomorphism with (R/I)[X] / (f mod I).

Equations

adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f = ideal.quot_equiv_of_eq _

source

@[simp]

theorem adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) (x : adjoin_root f) :

⇑(adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f) (⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) x) = ⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) x

source

theorem adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk_symm_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) (x : adjoin_root f) :

⇑((adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f).symm) (⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) x) = ⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) x

source

noncomputable def adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

adjoin_root f ⧸ ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I) ≃+* (polynomial R ⧸ ideal.map polynomial.C I) ⧸ ideal.map (ideal.quotient.mk (ideal.map polynomial.C I)) (ideal.span {f})

The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : R[X] and I : ideal R

Equations

adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f = double_quot.quot_quot_equiv_comm (ideal.span {f}) (ideal.map polynomial.C I)

source

@[simp]

theorem adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑(adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f) (⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) (⇑(adjoin_root.mk f) p)) = ⇑(double_quot.quot_quot_mk (ideal.map polynomial.C I) (ideal.span {f})) p

source

@[simp]

theorem adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_symm_quot_quot_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑((adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f).symm) (⇑(double_quot.quot_quot_mk (ideal.map polynomial.C I) (ideal.span {f})) p) = ⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) (⇑(adjoin_root.mk f) p)

source

noncomputable def adjoin_root.polynomial.quot_quot_equiv_comm {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f} ≃+* (polynomial R ⧸ ideal.map polynomial.C I) ⧸ ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f}

The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : R[X] and I : ideal R

Equations

adjoin_root.polynomial.quot_quot_equiv_comm I f = (ideal.span {polynomial.map (ideal.quotient.mk I) f}).quotient_equiv (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f}) I.polynomial_quotient_equiv_quotient_polynomial _

source

@[simp]

theorem adjoin_root.polynomial.quot_quot_equiv_comm_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑(adjoin_root.polynomial.quot_quot_equiv_comm I f) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)) = ⇑(ideal.quotient.mk (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f})) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) p)

source

@[simp]

theorem adjoin_root.polynomial.quot_quot_equiv_comm_symm_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑((adjoin_root.polynomial.quot_quot_equiv_comm I f).symm) (⇑(ideal.quotient.mk (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f})) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) p)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)

source

noncomputable def adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

adjoin_root f ⧸ ideal.map (adjoin_root.of f) I ≃+* polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f}

The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : R[X] and I : ideal R.

Equations

adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f = (adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f).trans ((adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f).trans ((ideal.quot_equiv_of_eq _).trans (adjoin_root.polynomial.quot_quot_equiv_comm I f).symm))

source

@[simp]

theorem adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_mk_of {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑(adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f) (⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) p)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)

source

@[simp]

theorem adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_symm_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :

⇑((adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f).symm) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)) = ⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) p)

source

@[simp]

theorem adjoin_root.quot_equiv_quot_map_apply {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) (ᾰ : adjoin_root f ⧸ ideal.map (adjoin_root.of f) I) :

⇑(adjoin_root.quot_equiv_quot_map f I) ᾰ = ⇑(adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f) ᾰ

source

@[simp]

theorem adjoin_root.quot_equiv_quot_map_symm_apply {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) (ᾰ : polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f}) :

⇑((adjoin_root.quot_equiv_quot_map f I).symm) ᾰ = ⇑((adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f).symm) ᾰ

source

noncomputable def adjoin_root.quot_equiv_quot_map {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) :

(adjoin_root f ⧸ ideal.map (adjoin_root.of f) I) ≃ₐ[R] polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f}

Promote adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot to an alg_equiv.

Equations

adjoin_root.quot_equiv_quot_map f I = alg_equiv.of_ring_equiv _

source

@[simp]

theorem adjoin_root.quot_equiv_quot_map_apply_mk {R : Type u} [comm_ring R] (f g : polynomial R) (I : ideal R) :

⇑(adjoin_root.quot_equiv_quot_map f I) (⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) g)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) g)

source

@[simp]

theorem adjoin_root.quot_equiv_quot_map_symm_apply_mk {R : Type u} [comm_ring R] (f g : polynomial R) (I : ideal R) :

⇑((adjoin_root.quot_equiv_quot_map f I).symm) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) g)) = ⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) g)

source

noncomputable def power_basis.quotient_equiv_quotient_minpoly_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (I : ideal R) :

(S ⧸ ideal.map (algebra_map R S) I) ≃ₐ[R] polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) (minpoly R pb.gen)}

Let α have minimal polynomial f over R and I be an ideal of R, then R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p).

Equations

pb.quotient_equiv_quotient_minpoly_map I = (alg_equiv.of_ring_equiv _).trans (adjoin_root.quot_equiv_quot_map (minpoly R pb.gen) I)

source

@[simp]

theorem power_basis.quotient_equiv_quotient_minpoly_map_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (I : ideal R) (ᾰ : S ⧸ ideal.map (algebra_map R S) I) :

⇑(pb.quotient_equiv_quotient_minpoly_map I) ᾰ = ⇑(adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I (minpoly R pb.gen)) (⇑((ideal.map (adjoin_root.of (minpoly R pb.gen)) I).quotient_map ↑(↑(adjoin_root.equiv' (minpoly R pb.gen) pb _ _).symm) _) ᾰ)

source

@[simp]

theorem power_basis.quotient_equiv_quotient_minpoly_map_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (I : ideal R) (ᾰ : polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) (minpoly R pb.gen)}) :

⇑((pb.quotient_equiv_quotient_minpoly_map I).symm) ᾰ = ⇑(↑(alg_equiv.of_ring_equiv _).symm) (⇑(↑(adjoin_root.quot_equiv_quot_map (minpoly R pb.gen) I).symm) ᾰ)

source

@[simp]

theorem power_basis.quotient_equiv_quotient_minpoly_map_apply_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (I : ideal R) (g : polynomial R) :

⇑(pb.quotient_equiv_quotient_minpoly_map I) (⇑(ideal.quotient.mk (ideal.map (algebra_map R S) I)) (⇑(polynomial.aeval pb.gen) g)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) (minpoly R pb.gen)})) (polynomial.map (ideal.quotient.mk I) g)

source

@[simp]

theorem power_basis.quotient_equiv_quotient_minpoly_map_symm_apply_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (I : ideal R) (g : polynomial R) :

⇑((pb.quotient_equiv_quotient_minpoly_map I).symm) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) (minpoly R pb.gen)})) (polynomial.map (ideal.quotient.mk I) g)) = ⇑(ideal.quotient.mk (ideal.map (algebra_map R S) I)) (⇑(polynomial.aeval pb.gen) g)

mathlib3 documentation

Adjoining roots of polynomials #

Main definitions and results #