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
power_basis R A: a structure containing anxand annsuch that1, x, ..., x^nis a basis for theR-algebraA(viewed as anR-module).findim (hf : f ≠ 0) : finite_dimensional.findim K (adjoin_root f) = f.nat_degree, the dimension ofadjoin_root fequals the degree offpower_basis.lift (pb : power_basis R S): ify : S'satisfies the same equations aspb.gen, this is the mapS →ₐ[R] S'sendingpb.gentoypower_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]
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) :
finite_dimensional.findim K S = pb.dim
theorem
power_basis.polynomial.mem_supported_range
{R : Type u_1}
[comm_ring R]
{f : polynomial R}
{d : ℕ} :
f ∈ finsupp.supported R R ↑(finset.range d) ↔ f.degree < ↑d
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 : ℕ}
(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) :
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 (⇑(⇑(_.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 _).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 _) = 0)
(f : polynomial A) :
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) :
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) :
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) :
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) :
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.
@[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) :
@[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) :
⇑(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 _ = minpoly _) :
pb.equiv pb' h is an equivalence of algebras with the same power basis.
@[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) :
⇑(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 _ = minpoly _) :
@[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 _) :
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)) :
is_integral R (⇑(algebra_map S T) x) ↔ is_integral R x
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) :
y ∈ submodule.span R (set.range (λ (i : fin (minpoly hx).nat_degree), x ^ ↑i))
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) :
linear_independent K (λ (i : fin (minpoly hx).nat_degree), x ^ ↑i)
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) :
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) :
power_basis K ↥(algebra.adjoin 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
- algebra.adjoin.power_basis hx = {gen := ⟨x, _⟩, dim := (minpoly hx).nat_degree, is_basis := _}
theorem
adjoin_root.power_basis_is_basis
{K : Type u_6}
[field K]
{f : polynomial K}
(hf : f ≠ 0) :
is_basis K (λ (i : fin f.nat_degree), adjoin_root.root f ^ i.val)
def
adjoin_root.power_basis
{K : Type u_6}
[field K]
{f : polynomial K}
(hf : f ≠ 0) :
power_basis K (adjoin_root f)
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
- adjoin_root.power_basis hf = {gen := adjoin_root.root f, dim := f.nat_degree, is_basis := _}
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) :
is_basis K (λ (i : fin (minpoly hx).nat_degree), intermediate_field.adjoin_simple.gen K x ^ ↑i)
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) :
power_basis K ↥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
- intermediate_field.adjoin.power_basis hx = {gen := intermediate_field.adjoin_simple.gen K x, dim := (minpoly hx).nat_degree, is_basis := _}
@[simp]
theorem
intermediate_field.adjoin.power_basis.gen_eq
{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.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) :
finite_dimensional.findim K ↥K⟮x⟯ = (minpoly hx).nat_degree
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_aeval
{K : Type u_6}
{L : Type u_7}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L)
(f : polynomial K) :
⇑(pb.equiv_adjoin_simple) (⇑(polynomial.aeval (intermediate_field.adjoin_simple.gen K pb.gen)) f) = ⇑(polynomial.aeval pb.gen) f
@[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) :
⇑(pb.equiv_adjoin_simple) (intermediate_field.adjoin_simple.gen K pb.gen) = pb.gen
@[simp]
theorem
power_basis.equiv_adjoin_simple_symm_aeval
{K : Type u_6}
{L : Type u_7}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L)
(f : polynomial K) :
⇑(pb.equiv_adjoin_simple.symm) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval (intermediate_field.adjoin_simple.gen K pb.gen)) f
@[simp]
theorem
power_basis.equiv_adjoin_simple_symm_gen
{K : Type u_6}
{L : Type u_7}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L) :
⇑(pb.equiv_adjoin_simple.symm) pb.gen = intermediate_field.adjoin_simple.gen K pb.gen