Power basis #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a structure
power_basis 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
power_basis structure generated by
power_basis R A: a structure containing an
1, x, ..., x^nis a basis for the
A(viewed as an
power_basis.equiv: if two power bases satisfy the same equations, they are equivalent as algebras
Implementation notes #
power basis, powerbasis
- gen : S
- dim : ℕ
- basis : basis (fin self.dim) R S
- basis_eq_pow : ∀ (i : fin self.dim), ⇑(self.basis) i = self.gen ^ ↑i
pb : power_basis R S states that
1, pb.gen, ..., pb.gen ^ (pb.dim - 1)
is a basis for the
S (viewed as
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
pb.minpoly_gen is the minimal polynomial for
pb.lift y hy is the algebra map sending
hy states the higher powers of
y are the same as the higher powers of
power_basis.lift_equiv for a bundled equiv sending
⟨y, hy⟩ to the algebra map.
pb.lift_equiv states that roots of the minimal polynomial of
pb.gen correspond to
pb.gen to that root.
pb.lift_equiv' states that elements of the root set of the minimal
pb.gen correspond to maps sending
pb.gen to that root.
There are finitely many algebra homomorphisms
S →ₐ[A] B if
S is of the form
B is an integral domain.
pb.equiv_of_root 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.
power_basis.equiv_of_minpoly which takes the hypothesis that the
minimal polynomials are identical.
pb.equiv_of_minpoly pb' h is an equivalence of algebras with the same power basis,
where "the same" means that they have identical minimal polynomials.
power_basis.equiv_of_root which takes the hypothesis that each generator is a root of the
other basis' minimal polynomial;
power_basis.equiv_root is more general if
A is not a field.
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.
power_basis.map pb (e : S ≃ₐ[R] S') is the power basis for
S' generated by