# 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 (minpoly K x).natDegree) K (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.

Equations
• = let_fun hST := ; let_fun hx' := ; Basis.mk
Instances For
@[simp]
theorem Algebra.adjoin.powerBasis_dim {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
.dim = (minpoly K x).natDegree
@[simp]
theorem Algebra.adjoin.powerBasis_gen {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :
.gen = x,
noncomputable def Algebra.adjoin.powerBasis {K : Type u_1} {S : Type u_2} [] [] [Algebra K S] {x : S} (hx : ) :

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.

Equations
• = { gen := x, , dim := (minpoly K x).natDegree, basis := , basis_eq_pow := }
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}) :
@[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}) :
(B.ofGenMemAdjoin hint hx).dim = (minpoly K x).natDegree
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.

Equations
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 (B.basis.toMatrix (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.