# mathlib3documentation

ring_theory.power_basis

# Power basis #

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

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, A, B ... are comm_rings, 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_7) (S : Type u_8) [comm_ring R] [ring S] [ S] :
Type (max u_7 u_8)

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.

Instances for power_basis
• power_basis.has_sizeof_inst
@[simp]
theorem power_basis.coe_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] (pb : S) :
(pb.basis) = λ (i : fin pb.dim), pb.gen ^ i
theorem power_basis.finite_dimensional {S : Type u_2} [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} [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] [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] [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] [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] [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] [ring S] [ S] [nontrivial S] (pb : S) (y : S) :
theorem power_basis.exists_eq_aeval' {R : Type u_1} {S : Type u_2} [comm_ring R] [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] [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
noncomputable def power_basis.minpoly_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :

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

Equations
theorem power_basis.aeval_minpoly_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :
theorem power_basis.minpoly_gen_monic {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :
theorem power_basis.dim_le_nat_degree_of_root {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) {p : polynomial A} (ne_zero : p 0) (root : (polynomial.aeval pb.gen) p = 0) :
theorem power_basis.dim_le_degree_of_root {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (h : S) {p : polynomial A} (ne_zero : p 0) (root : p = 0) :
theorem power_basis.degree_minpoly_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] [nontrivial A] (pb : S) :
theorem power_basis.nat_degree_minpoly_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] [nontrivial A] (pb : S) :
@[simp]
theorem power_basis.minpoly_gen_eq {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :
theorem power_basis.is_integral_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :
pb.gen
@[simp]
theorem power_basis.degree_minpoly {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] [nontrivial A] (pb : S) :
(minpoly A pb.gen).degree = (pb.dim)
@[simp]
theorem power_basis.nat_degree_minpoly {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] [nontrivial A] (pb : S) :
@[protected]
theorem power_basis.left_mul_matrix {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] (pb : S) :
pb.gen = matrix.of (λ (i j : fin pb.dim), ite (j + 1 = pb.dim) (-pb.minpoly_gen.coeff i) (ite (i = j + 1) 1 0))
theorem power_basis.constr_pow_aeval {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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'
noncomputable def power_basis.lift {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (y : {y // (minpoly A pb.gen) = 0}) :
(pb.lift_equiv.symm) y = pb.lift y _
noncomputable def power_basis.lift_equiv {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [ 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} [ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [ 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))
noncomputable def power_basis.lift_equiv' {S : Type u_2} [ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [ 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
noncomputable def power_basis.alg_hom.fintype {S : Type u_2} [ring S] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [is_domain B] [ 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
noncomputable def power_basis.equiv_of_root {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h₁ : (polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (f : polynomial A) :
(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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = 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} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) (f : polynomial A) :
@[simp]
theorem power_basis.equiv_of_minpoly_gen {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) :
(pb.equiv_of_minpoly pb' h) pb.gen = pb'.gen
@[simp]
theorem power_basis.equiv_of_minpoly_symm {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] [ S] {S' : Type u_7} [ring S'] [ S'] (pb : S) (pb' : S') (h : pb.gen = pb'.gen) :
theorem linear_independent_pow {S : Type u_2} [ring S] {K : Type u_6} [field K] [ S] (x : S) :
(λ (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] [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] [ring S] [ S] {S' : Type u_7} [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] [ring S] [ S] {S' : Type u_7} [comm_ring S'] [ S'] (pb : 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] [ring S] [ S] {S' : Type u_7} [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] [ring S] [ S] {S' : Type u_7} [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} [ring S] {A : Type u_4} [comm_ring A] {S' : Type u_7} [comm_ring S'] [ S] [ S'] (pb : S) (e : S ≃ₐ[A] S') :
@[simp]
theorem power_basis.equiv_of_root_map {S : Type u_2} [ring S] {A : Type u_4} [comm_ring A] {S' : Type u_7} [comm_ring S'] [ S] [ S'] (pb : 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} [ring S] {A : Type u_4} [comm_ring A] {S' : Type u_7} [comm_ring S'] [ S] [ S'] (pb : S) (e : S ≃ₐ[A] S') (h : pb.gen = (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] [ring S] [ S] (B : S) :
{B.gen} =
theorem power_basis.adjoin_eq_top_of_gen_mem_adjoin {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {B : S} {x : S} (hx : B.gen {x}) :
{x} =