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. There are also constructors for power_basis when adjoining an algebraic element to a ring/field.

Definitions

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] [algebra R S] :
Type 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.

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.findim {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :

TODO: this mixes polynomial and finsupp, we should hide this behind a new function polynomial.of_finsupp.

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 : polynomial R), 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 : polynomial R), 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] [nontrivial S] (pb : power_basis R S) :
pb.dim 0

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 : polynomial R), f.nat_degree < pb.dim y = (polynomial.aeval pb.gen) f

def power_basis.minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain 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.nat_degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

theorem power_basis.minpoly_gen_monic {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

@[simp]
theorem power_basis.aeval_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

theorem power_basis.is_integral_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain 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} [integral_domain A] [algebra A S] (h : power_basis A S) {p : polynomial A} (ne_zero : p 0) (root : (polynomial.aeval h.gen) p = 0) :

@[simp]
theorem power_basis.nat_degree_minpoly {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A 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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly _) = 0) (f : polynomial A) :
(_.constr (λ (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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly _) = 0) :
(_.constr (λ (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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly _) = 0) (x : A) :
(_.constr (λ (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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] (pb : power_basis A S) {y : S'} (hy : (polynomial.aeval y) (minpoly _) = 0) (x x' : S) :
(_.constr (λ (i : fin pb.dim), y ^ i)) (x * x') = ((_.constr (λ (i : fin pb.dim), y ^ i)) x) * (_.constr (λ (i : fin pb.dim), y ^ i)) x'

def power_basis.lift {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly _) = 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.

Equations
@[simp]
theorem power_basis.lift_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly _) = 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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] (pb : power_basis A S) (y : S') (hy : (polynomial.aeval y) (minpoly _) = 0) (f : polynomial A) :

def power_basis.equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] [nontrivial S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly _ = minpoly _) :
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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] [nontrivial S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly _ = minpoly _) (f : polynomial A) :

@[simp]
theorem power_basis.equiv_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] [nontrivial S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly _ = minpoly _) :
(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} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] [nontrivial S] [nontrivial S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly _ = minpoly _) :
(pb.equiv pb' h).symm = pb'.equiv pb _

theorem is_integral_algebra_map_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T] {x : S} (hST : function.injective (algebra_map S T)) :

theorem minpoly.eq_of_algebra_map_eq {S : Type u_2} {T : Type u_3} [comm_ring S] [comm_ring T] [algebra S T] {K : Type u_6} [field K] [algebra K S] [algebra K T] [is_scalar_tower K S T] (hST : function.injective (algebra_map S T)) {x : S} {y : T} (hx : is_integral K x) (hy : is_integral K y) (h : y = (algebra_map S T) x) :

If y is the image of x in an extension, their minimal polynomials coincide.

We take h : y = algebra_map L T x as an argument because rw h typically fails since is_integral R y depends on y.

theorem algebra.mem_span_power_basis {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 : polynomial R), y = (polynomial.aeval x) f) :

theorem algebra.linear_independent_power_basis {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] {x : S} (hx : is_integral K x) :

theorem algebra.power_basis_is_basis {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] {x : S} (hx : is_integral K x) :
is_basis K (λ (i : fin (minpoly hx).nat_degree), x, _⟩ ^ i)

def algebra.adjoin.power_basis {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] {x : S} (hx : is_integral K x) :

The power basis 1, x, ..., x ^ (d - 1) for K[x], where d is the degree of the minimal polynomial of x.

Equations
theorem adjoin_root.power_basis_is_basis {K : Type u_6} [field K] {f : polynomial K} (hf : f 0) :

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

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
theorem intermediate_field.power_basis_is_basis {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] {x : L} (hx : is_integral K x) :

def intermediate_field.adjoin.power_basis {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] {x : L} (hx : is_integral K x) :

The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Equations
theorem intermediate_field.adjoin.finite_dimensional {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] {x : L} (hx : is_integral K x) :

theorem intermediate_field.adjoin.findim {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] {x : L} (hx : is_integral K x) :

def power_basis.equiv_adjoin_simple {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] (pb : power_basis K L) :

pb.equiv_adjoin_simple is the equivalence between K⟮pb.gen⟯ and L itself.

Equations
@[simp]
theorem power_basis.equiv_adjoin_simple_gen {K : Type u_6} {L : Type u_7} [field K] [field L] [algebra K L] (pb : power_basis K L) :

@[simp]