# mathlibdocumentation

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 #

• power_basis R A: a structure containing an x and an n such that 1, x, ..., x^n is a basis for the R-algebra A (viewed as an R-module).

• finrank (hf : f ≠ 0) : finite_dimensional.finrank K (adjoin_root f) = f.nat_degree, the dimension of adjoin_root f equals the degree of f

• power_basis.lift (pb : power_basis R S): if y : S' satisfies the same equations as pb.gen, this is the map S →ₐ[R] S' sending pb.gen to y

• power_basis.equiv: if two power bases satisfy the same equations, they are equivalent as algebras

## Implementation notes #

Throughout this file, R, S, ... are comm_rings, A, B, ... are integral_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] [ 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] [ S] (pb : 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] [ S] (pb : 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] [ S] (pb : S) :
theorem power_basis.mem_span_pow' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {x y : S} {d : } :
y (set.range (λ (i : fin d), x ^ i)) ∃ (f : , f.degree < d y = f
theorem power_basis.mem_span_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {x y : S} {d : } (hd : d 0) :
y (set.range (λ (i : fin d), x ^ i)) ∃ (f : , f.nat_degree < d y = f
theorem power_basis.dim_ne_zero {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] [h : nontrivial S] (pb : S) :
pb.dim 0
theorem power_basis.dim_pos {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] [nontrivial S] (pb : S) :
0 < pb.dim
theorem power_basis.exists_eq_aeval {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] [nontrivial S] (pb : S) (y : S) :
∃ (f : , 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] [ S] (pb : S) (y : S) :
∃ (f : , 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] [ S] {S' : Type u_3} [semiring S'] [ S'] (pb : S) ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) :
f = g
def power_basis.minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : 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.degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
@[simp]
theorem power_basis.nat_degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
theorem power_basis.minpoly_gen_monic {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
@[simp]
theorem power_basis.aeval_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
theorem power_basis.is_integral_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
pb.gen
theorem power_basis.dim_le_nat_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (h : S) {p : polynomial A} (ne_zero : p 0) (root : p = 0) :
theorem power_basis.dim_le_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (h : S) {p : polynomial A} (ne_zero : p 0) (root : p = 0) :
@[simp]
theorem power_basis.nat_degree_minpoly {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] (pb : S) :
@[simp]
theorem power_basis.minpoly_gen_eq {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [ S] (pb : S) :
theorem power_basis.nat_degree_lt_nat_degree {R : Type u_1} [comm_ring R] {p q : polynomial R} (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} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) {y : S'} (hy : (minpoly A pb.gen) = 0) (f : polynomial A) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) ((polynomial.aeval pb.gen) f) = f
theorem power_basis.constr_pow_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) {y : S'} (hy : (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} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) {y : S'} (hy : (minpoly A pb.gen) = 0) (x : A) :
((pb.basis.constr A) (λ (i : fin pb.dim), y ^ i)) ( S) x) = S') x
theorem power_basis.constr_pow_mul {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) {y : S'} (hy : (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'
def power_basis.lift {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (y : S') (hy : (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} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (y : S') (hy : (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} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (y : S') (hy : (minpoly A pb.gen) = 0) (f : polynomial A) :
(pb.lift y hy) ((polynomial.aeval pb.gen) f) = f
@[simp]
theorem power_basis.lift_equiv_apply_coe {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : 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} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (y : {y // (minpoly A pb.gen) = 0}) :
(pb.lift_equiv.symm) y = pb.lift y _
def power_basis.lift_equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) :
(S →ₐ[A] S') {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} [ B] [ S] (pb : 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} [ B] [ S] (pb : S) (ᾰ : {y // y (polynomial.map B) (minpoly A pb.gen)).roots}) :
((pb.lift_equiv'.symm) ᾰ) = ((pb.basis.constr A) (λ (i : fin pb.dim), ^ i))
def power_basis.lift_equiv' {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [ B] [ S] (pb : S) :
(S →ₐ[A] B) {y // y (polynomial.map 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
def power_basis.alg_hom.fintype {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [ B] [ S] (pb : 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
def power_basis.equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) :
S ≃ₐ[A] S'

pb.equiv pb' h is an equivalence of algebras with the same power basis.

Equations
@[simp]
theorem power_basis.equiv_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) (f : polynomial A) :
@[simp]
theorem power_basis.equiv_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) :
(pb.equiv pb' h) pb.gen = pb'.gen
@[simp]
theorem power_basis.equiv_symm {S : Type u_2} [comm_ring S] {A : Type u_4} [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) :
(pb.equiv pb' h).symm = pb'.equiv pb _
theorem is_integral.linear_independent_pow {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [ S] {x : S} (hx : x) :
(λ (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] [ S] [nontrivial R] {x y : S} (hx : x) (hy : ∃ (f : , y = f) :
y (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] [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : 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] [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (e : S ≃ₐ[R] S') :
(pb.map e).dim = pb.dim
def power_basis.map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : S) (e : S ≃ₐ[R] S') :
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] [ S] {S' : Type u_8} [comm_ring S'] [ S'] (pb : 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} {S' : Type u_8} [comm_ring S'] [ S] [ S'] (pb : S) (e : S ≃ₐ[A] S') :
@[simp]
theorem power_basis.equiv_map {S : Type u_2} [comm_ring S] {A : Type u_4} {S' : Type u_8} [comm_ring S'] [ S] [ S'] (pb : S) (e : S ≃ₐ[A] S') (h : pb.gen = (pb.map e).gen) :
pb.equiv (pb.map e) h = e