Power basis #
This file defines a structure
PowerBasis R S, giving a basis of the
S as a finite list of powers
1, x, ..., x^n.
For example, if
x is algebraic over a ring/field, adjoining
PowerBasis structure generated by
PowerBasis R A: a structure containing an
1, x, ..., x^nis a basis for the
A(viewed as an
PowerBasis.equiv: if two power bases satisfy the same equations, they are equivalent as algebras
Implementation notes #
power basis, powerbasis
- gen : S
- dim : ℕ
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
the canonical power basis is given by
PowerBasis.liftEquiv for a bundled equiv sending
⟨y, hy⟩ to the algebra map.
There are finitely many algebra homomorphisms
S →ₐ[A] B if
S is of the form
B is an integral domain.
pb.equivOfRoot 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.
PowerBasis.equivOfMinpoly which takes the hypothesis that the
minimal polynomials are identical.
pb.equivOfMinpoly pb' h is an equivalence of algebras with the same power basis,
where "the same" means that they have identical minimal polynomials.