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 anxand annsuch that1, x, ..., x^nis a basis for theR-algebraA(viewed as anR-module). -
finrank (hf : f ≠ 0) : finite_dimensional.finrank K (adjoin_root f) = f.nat_degree, the dimension ofadjoin_root fequals 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.gentoy -
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
comm_ring with is_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
- 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 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.
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.
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.
See 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
maps sending pb.gen to that root.
This is the bundled equiv version of power_basis.lift.
If the codomain of the alg_homs is an integral domain, then the roots form a multiset,
see lift_equiv' for the corresponding statement.
pb.lift_equiv' states that elements of the root set of the minimal
polynomial of pb.gen correspond to maps sending pb.gen to that root.
Equations
- pb.lift_equiv' = pb.lift_equiv.trans ((equiv.refl B).subtype_equiv _)
There are finitely many algebra homomorphisms S →ₐ[A] B if S is of the form A[x]
and B is an integral domain.
Equations
- power_basis.alg_hom.fintype pb = let _inst : decidable_eq B := classical.dec_eq B in fintype.of_equiv {y // y ∈ (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots} pb.lift_equiv'.symm
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.
See also power_basis.equiv_of_minpoly which takes the hypothesis that the
minimal polynomials are identical.
Equations
- pb.equiv_of_root pb' h₁ h₂ = alg_equiv.of_alg_hom (pb.lift pb'.gen h₂) (pb'.lift pb.gen h₁) _ _
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.
See also 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.
Equations
- pb.equiv_of_minpoly pb' h = pb.equiv_of_root pb' _ _
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 e pb.gen.