# Power basis for Algebra.adjoin R {x}#

This file defines the canonical power basis on Algebra.adjoin R {x}, where x is an integral element over R.

noncomputable def Algebra.adjoin.powerBasisAux {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
Basis (Fin ()) K { x // x Algebra.adjoin K {x} }

The elements 1, x, ..., x ^ (d - 1) for a basis for the K-module K[x], where d is the degree of the minimal polynomial of x.

Instances For
@[simp]
theorem Algebra.adjoin.powerBasis_dim {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
().dim =
@[simp]
theorem Algebra.adjoin.powerBasis_gen {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
().gen = { val := x, property := (_ : x ↑(Algebra.adjoin K {x})) }
noncomputable def Algebra.adjoin.powerBasis {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
PowerBasis K { x // x 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. See Algebra.adjoin.powerBasis' for a version over a more general base ring.

Instances For
@[simp]
theorem PowerBasis.ofGenMemAdjoin_gen {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin K {x}) :
(PowerBasis.ofGenMemAdjoin B hint hx).gen = x
@[simp]
theorem PowerBasis.ofGenMemAdjoin_dim {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin K {x}) :
noncomputable def PowerBasis.ofGenMemAdjoin {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin K {x}) :

The power basis given by x if B.gen ∈ adjoin K {x}. See PowerBasis.ofGenMemAdjoin' for a version over a more general base ring.

Instances For
theorem PowerBasis.repr_gen_pow_isIntegral {S : Type u_2} [] {R : Type u_3} [] [Algebra R S] {A : Type u_4} [] [Algebra R A] [Algebra S A] [] {B : } (hB : IsIntegral R B.gen) [] (hmin : minpoly S B.gen = Polynomial.map () (minpoly R B.gen)) (n : ) (i : Fin B.dim) :
IsIntegral R (↑(B.basis.repr (B.gen ^ n)) i)

If B : PowerBasis S A is such that IsIntegral R B.gen, then IsIntegral R (B.basis.repr (B.gen ^ n) i) for all i if minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S). This is the case if R is a GCD domain and S is its fraction ring.

theorem PowerBasis.repr_mul_isIntegral {S : Type u_2} [] {R : Type u_3} [] [Algebra R S] {A : Type u_4} [] [Algebra R A] [Algebra S A] [] {B : } (hB : IsIntegral R B.gen) [] {x : A} {y : A} (hx : ∀ (i : Fin B.dim), IsIntegral R (↑(B.basis.repr x) i)) (hy : ∀ (i : Fin B.dim), IsIntegral R (↑(B.basis.repr y) i)) (hmin : minpoly S B.gen = Polynomial.map () (minpoly R B.gen)) (i : Fin B.dim) :
IsIntegral R (↑(B.basis.repr (x * y)) i)

Let B : PowerBasis S A be such that IsIntegral R B.gen, and let x y : A be elements with integral coordinates in the base B.basis. Then IsIntegral R ((B.basis.repr (x * y) i) for all i if minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S). This is the case if R is a GCD domain and S is its fraction ring.

theorem PowerBasis.repr_pow_isIntegral {S : Type u_2} [] {R : Type u_3} [] [Algebra R S] {A : Type u_4} [] [Algebra R A] [Algebra S A] [] {B : } (hB : IsIntegral R B.gen) [] {x : A} (hx : ∀ (i : Fin B.dim), IsIntegral R (↑(B.basis.repr x) i)) (hmin : minpoly S B.gen = Polynomial.map () (minpoly R B.gen)) (n : ) (i : Fin B.dim) :
IsIntegral R (↑(B.basis.repr (x ^ n)) i)

Let B : PowerBasis S A be such that IsIntegral R B.gen, and let x : A be an element with integral coordinates in the base B.basis. Then IsIntegral R ((B.basis.repr (x ^ n) i) for all i and all n if minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S). This is the case if R is a GCD domain and S is its fraction ring.

theorem PowerBasis.toMatrix_isIntegral {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {R : Type u_3} [] [Algebra R S] [Algebra R K] [] {B : } {B' : } {P : } (h : ↑(Polynomial.aeval B.gen) P = B'.gen) (hB : IsIntegral R B.gen) (hmin : minpoly K B.gen = Polynomial.map () (minpoly R B.gen)) (i : Fin B.dim) (j : Fin B'.dim) :
IsIntegral R (Basis.toMatrix B.basis (B'.basis) i j)

Let B B' : PowerBasis K S be such that IsIntegral R B.gen, and let P : R[X] be such that aeval B.gen P = B'.gen. Then IsIntegral R (B.basis.to_matrix B'.basis i j) for all i and j if minpoly K B.gen = (minpoly R B.gen).map (algebraMap R L). This is the case if R is a GCD domain and K is its fraction ring.