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 anx
and ann
such that1, x, ..., x^n
is 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 f
equals the degree off
power_basis.lift (pb : power_basis R S)
: ify : S'
satisfies the same equations aspb.gen
, this is the mapS →ₐ[R] S'
sendingpb.gen
toy
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_ring
s, A
, B
, ... are
integral_domain
s and K
, L
, ... are field
s.
S
is an R
-algebra, B
is an A
-algebra, L
is a K
-algebra.
Tags
power basis, powerbasis
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
.
Cannot be an instance because power_basis
cannot be a class.
TODO: this mixes polynomial
and finsupp
, we should hide this behind a
new function polynomial.of_finsupp
.
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
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
.
pb.equiv pb' h
is an equivalence of algebras with the same power basis.
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.
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 := _}
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 := _}
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 := _}
pb.equiv_adjoin_simple
is the equivalence between K⟮pb.gen⟯
and L
itself.