mathlib documentation

ring_theory.power_basis

Power basis #

This file defines a structure power_basis R S, giving a basis of the R-algebra S as a finite list of powers 1, x, ..., x^n. For example, if x is algebraic over a ring/field, adjoining x gives a power_basis structure generated by x.

Definitions #

Implementation notes #

Throughout this file, R, S, ... are comm_rings, A, B, ... are comm_ring with is_domains and K, L, ... are fields. S is an R-algebra, B is an A-algebra, L is a K-algebra.

Tags #

power basis, powerbasis

@[nolint]
structure power_basis (R : Type u_8) (S : Type u_9) [comm_ring R] [ring S] [algebra R S] :
Type (max u_8 u_9)

pb : power_basis R S states that 1, pb.gen, ..., pb.gen ^ (pb.dim - 1) is a basis for the R-algebra S (viewed as R-module).

This is a structure, not a class, since the same algebra can have many power bases. For the common case where S is defined by adjoining an integral element to R, the canonical power basis is given by {algebra,intermediate_field}.adjoin.power_basis.

@[simp]
theorem power_basis.coe_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) :
(pb.basis) = λ (i : fin pb.dim), pb.gen ^ i
theorem power_basis.finite_dimensional {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :

Cannot be an instance because power_basis cannot be a class.

theorem power_basis.finrank {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :
theorem power_basis.mem_span_pow' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x y : S} {d : } :
y submodule.span R (set.range (λ (i : fin d), x ^ i)) ∃ (f : R[X]), f.degree < d y = (polynomial.aeval x) f
theorem power_basis.mem_span_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x y : S} {d : } (hd : d 0) :
y submodule.span R (set.range (λ (i : fin d), x ^ i)) ∃ (f : R[X]), f.nat_degree < d y = (polynomial.aeval x) f
theorem power_basis.dim_ne_zero {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [h : nontrivial S] (pb : power_basis R S) :
pb.dim 0
theorem power_basis.dim_pos {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial S] (pb : power_basis R S) :
0 < pb.dim
theorem power_basis.exists_eq_aeval {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial S] (pb : power_basis R S) (y : S) :
∃ (f : R[X]), f.nat_degree < pb.dim y = (polynomial.aeval pb.gen) f
theorem power_basis.exists_eq_aeval' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (y : S) :
∃ (f : R[X]), y = (polynomial.aeval pb.gen) f
theorem power_basis.alg_hom_ext {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_3} [semiring S'] [algebra R S'] (pb : power_basis R S) ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) :
f = g
noncomputable def power_basis.minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] (pb : power_basis A S) :

pb.minpoly_gen is a minimal polynomial for pb.gen.

If A is not a field, it might not necessarily be the minimal polynomial, however nat_degree_minpoly shows its degree is indeed minimal.

Equations
@[simp]
theorem power_basis.aeval_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] (pb : power_basis A S) :
theorem power_basis.dim_le_nat_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] (h : power_basis A S) {p : A[X]} (ne_zero : p 0) (root : (polynomial.aeval h.gen) p = 0) :
theorem power_basis.dim_le_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] (h : power_basis A S) {p : A[X]} (ne_zero : p 0) (root : (polynomial.aeval h.gen) p = 0) :
@[simp]
theorem power_basis.degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] [is_domain A] (pb : power_basis A S) :
@[simp]
theorem power_basis.nat_degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] [is_domain A] (pb : power_basis A S) :
theorem power_basis.minpoly_gen_monic {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] [is_domain A] (pb : power_basis A S) :
theorem power_basis.is_integral_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] [is_domain A] (pb : power_basis A S) :
@[simp]
theorem power_basis.nat_degree_minpoly {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] [is_domain A] (pb : power_basis A S) :
@[simp]
theorem power_basis.minpoly_gen_eq {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :
theorem power_basis.nat_degree_lt_nat_degree {R : Type u_1} [comm_ring R] {p q : R[X]} (hp : p 0) (hpq : p.degree < q.degree) :
theorem power_basis.constr_pow_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) (f : A[X]) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) ((polynomial.aeval pb.gen) f) = (polynomial.aeval y) f
theorem power_basis.constr_pow_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) pb.gen = y
theorem power_basis.constr_pow_algebra_map {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) (x : A) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) ((algebra_map A S) x) = (algebra_map A S') x
theorem power_basis.constr_pow_mul {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) (x x' : S) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) (x * x') = (((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) x) * ((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) x'
noncomputable def power_basis.lift {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) :
S →ₐ[A] S'

pb.lift y hy is the algebra map sending pb.gen to y, where hy states the higher powers of y are the same as the higher powers of pb.gen.

See power_basis.lift_equiv for a bundled equiv sending ⟨y, hy⟩ to the algebra map.

Equations
@[simp]
theorem power_basis.lift_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) :
(pb.lift y hy) pb.gen = y
@[simp]
theorem power_basis.lift_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly A pb.gen) = 0) (f : A[X]) :
@[simp]
theorem power_basis.lift_equiv_apply_coe {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (f : S →ₐ[A] S') :
((pb.lift_equiv) f) = f pb.gen
@[simp]
theorem power_basis.lift_equiv_symm_apply {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (y : {y // (polynomial.aeval y) (minpoly A pb.gen) = 0}) :
(pb.lift_equiv.symm) y = pb.lift y _
noncomputable def power_basis.lift_equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) :
(S →ₐ[A] S') {y // (polynomial.aeval y) (minpoly A pb.gen) = 0}

pb.lift_equiv states that roots of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

This is the bundled equiv version of power_basis.lift. If the codomain of the alg_homs is an integral domain, then the roots form a multiset, see lift_equiv' for the corresponding statement.

Equations
@[simp]
theorem power_basis.lift_equiv'_apply_coe {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [algebra A B] [algebra A S] [is_domain A] (pb : power_basis A S) (ᾰ : S →ₐ[A] B) :
((pb.lift_equiv') ᾰ) = ᾰ pb.gen
@[simp]
theorem power_basis.lift_equiv'_symm_apply_apply {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [algebra A B] [algebra A S] [is_domain A] (pb : power_basis A S) (ᾰ : {y // y (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots}) :
((pb.lift_equiv'.symm) ᾰ) = ((pb.basis.constr A) (λ (i : fin pb.dim), ^ i))
noncomputable def power_basis.lift_equiv' {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [algebra A B] [algebra A S] [is_domain A] (pb : power_basis A S) :
(S →ₐ[A] B) {y // y (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots}

pb.lift_equiv' states that elements of the root set of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

Equations
noncomputable def power_basis.alg_hom.fintype {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [algebra A B] [algebra A S] [is_domain A] (pb : power_basis A S) :

There are finitely many algebra homomorphisms S →ₐ[A] B if S is of the form A[x] and B is an integral domain.

Equations
noncomputable def power_basis.equiv_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
S ≃ₐ[A] S'

pb.equiv_of_root pb' h₁ h₂ is an equivalence of algebras with the same power basis, where "the same" means that pb is a root of pb's minimal polynomial and vice versa.

See also power_basis.equiv_of_minpoly which takes the hypothesis that the minimal polynomials are identical.

Equations
theorem power_basis.equiv_of_root_apply {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (ᾰ : S) :
(pb.equiv_of_root pb' h₁ h₂) = (pb.lift pb'.gen h₂)
@[simp]
theorem power_basis.equiv_of_root_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (f : A[X]) :
(pb.equiv_of_root pb' h₁ h₂) ((polynomial.aeval pb.gen) f) = (polynomial.aeval pb'.gen) f
@[simp]
theorem power_basis.equiv_of_root_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
(pb.equiv_of_root pb' h₁ h₂) pb.gen = pb'.gen
@[simp]
theorem power_basis.equiv_of_root_symm {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
(pb.equiv_of_root pb' h₁ h₂).symm = pb'.equiv_of_root pb h₂ h₁
noncomputable def power_basis.equiv_of_minpoly {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
S ≃ₐ[A] S'

pb.equiv_of_minpoly pb' h is an equivalence of algebras with the same power basis, where "the same" means that they have identical minimal polynomials.

See also power_basis.equiv_of_root which takes the hypothesis that each generator is a root of the other basis' minimal polynomial; power_basis.equiv_root is more general if A is not a field.

Equations
theorem power_basis.equiv_of_minpoly_apply {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (ᾰ : S) :
(pb.equiv_of_minpoly pb' h) = (pb.lift pb'.gen _)
@[simp]
theorem power_basis.equiv_of_minpoly_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : A[X]) :
@[simp]
theorem power_basis.equiv_of_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
(pb.equiv_of_minpoly pb' h) pb.gen = pb'.gen
@[simp]
theorem power_basis.equiv_of_minpoly_symm {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [is_domain A] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
theorem is_integral.linear_independent_pow {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] {x : S} (hx : is_integral K x) :
linear_independent K (λ (i : fin (minpoly K x).nat_degree), x ^ i)

Useful lemma to show x generates a power basis: the powers of x less than the degree of x's minimal polynomial are linearly independent.

theorem is_integral.mem_span_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial R] {x y : S} (hx : is_integral R x) (hy : ∃ (f : R[X]), y = (polynomial.aeval x) f) :
y submodule.span R (set.range (λ (i : fin (minpoly R x).nat_degree), x ^ i))
@[simp]
theorem power_basis.map_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :
@[simp]
theorem power_basis.map_dim {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :
(pb.map e).dim = pb.dim
noncomputable def power_basis.map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :

power_basis.map pb (e : S ≃ₐ[R] S') is the power basis for S' generated by e pb.gen.

Equations
@[simp]
theorem power_basis.map_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :
(pb.map e).gen = e pb.gen
@[simp]
theorem power_basis.minpoly_gen_map {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] {S' : Type u_8} [comm_ring S'] [algebra A S] [algebra A S'] (pb : power_basis A S) (e : S ≃ₐ[A] S') :
@[simp]
theorem power_basis.equiv_of_root_map {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] {S' : Type u_8} [comm_ring S'] [algebra A S] [algebra A S'] [is_domain A] (pb : power_basis A S) (e : S ≃ₐ[A] S') (h₁ : (polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0) (h₂ : (polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0) :
pb.equiv_of_root (pb.map e) h₁ h₂ = e
@[simp]
theorem power_basis.equiv_of_minpoly_map {S : Type u_2} [comm_ring S] {A : Type u_4} [comm_ring A] {S' : Type u_8} [comm_ring S'] [algebra A S] [algebra A S'] [is_domain A] (pb : power_basis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :
pb.equiv_of_minpoly (pb.map e) h = e
theorem power_basis.adjoin_gen_eq_top {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (B : power_basis R S) :
theorem power_basis.adjoin_eq_top_of_gen_mem_adjoin {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {B : power_basis R S} {x : S} (hx : B.gen algebra.adjoin R {x}) :