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 #

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

Type (max u_8 u_9)

gen : S
dim : ℕ
basis : basis (fin c.dim) R S
basis_eq_pow : ∀ (i : fin c.dim), ⇑(c.basis) i = c.gen ^ ↑i

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) :

finite_dimensional 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) :

finite_dimensional.finrank K S = pb.dim

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.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 : 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

pb.minpoly_gen = polynomial.X ^ pb.dim - ∑ (i : fin pb.dim), (⇑polynomial.C (⇑(⇑(pb.basis.repr) (pb.gen ^ pb.dim)) i)) * polynomial.X ^ ↑i

@[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) :

pb.minpoly_gen.nat_degree = pb.dim

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) :

pb.minpoly_gen.monic

@[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) :

⇑(polynomial.aeval pb.gen) pb.minpoly_gen = 0

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) :

is_integral A pb.gen

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) :

h.dim ≤ p.nat_degree

@[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) :

(minpoly A pb.gen).nat_degree = pb.dim

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) :

p.nat_degree < q.nat_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 A pb.gen) = 0) (f : polynomial A) :

⇑(⇑(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} [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 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} [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 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} [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 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} [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 A pb.gen) = 0) :

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

pb.lift y hy = {to_fun := (⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[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 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} [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 A pb.gen) = 0) (f : polynomial A) :

⇑(pb.lift y hy) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval y) f

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 A pb.gen = minpoly A pb'.gen) :

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

Equations

pb.equiv pb' h = alg_equiv.of_alg_hom (pb.lift pb'.gen _) (pb'.lift pb.gen _) _ _

@[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 A pb.gen = minpoly A pb'.gen) (f : polynomial A) :

⇑(pb.equiv pb' h) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval pb'.gen) f

@[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 A pb.gen = minpoly A 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} [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 A pb.gen = minpoly A 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] [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 : polynomial R), y = ⇑(polynomial.aeval x) f) :

y ∈ submodule.span R (set.range (λ (i : fin (minpoly R x).nat_degree), x ^ ↑i))