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} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) : 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

• Algebra.adjoin.powerBasisAux hx = let_fun hST := ⋯; let_fun hx' := ⋯; Basis.mk ⋯ ⋯

@[simp]

theorem Algebra.adjoin.powerBasis_dim {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) : (Algebra.adjoin.powerBasis hx).dim = (minpoly K x).natDegree

@[simp]

theorem Algebra.adjoin.powerBasis_gen {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) : (Algebra.adjoin.powerBasis hx).gen = ⟨x, ⋯⟩

noncomputable def Algebra.adjoin.powerBasis {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) : PowerBasis K ↥(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.

Equations

• Algebra.adjoin.powerBasis hx = { gen := ⟨x, ⋯⟩, dim := (minpoly K x).natDegree, basis := Algebra.adjoin.powerBasisAux hx, basis_eq_pow := ⋯ }

@[simp]

theorem PowerBasis.ofGenMemAdjoin_gen {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (B : PowerBasis K S) (hint : IsIntegral K x) (hx : B.gen ∈ Algebra.adjoin K {x}) : (B.ofGenMemAdjoin hint hx).gen = x

@[simp]

theorem PowerBasis.ofGenMemAdjoin_dim {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (B : PowerBasis K S) (hint : IsIntegral K x) (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} [Field K] [CommRing S] [Algebra K S] {x : S} (B : PowerBasis K S) (hint : IsIntegral K x) (hx : B.gen ∈ Algebra.adjoin K {x}) : PowerBasis K S

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

• B.ofGenMemAdjoin hint hx = (Algebra.adjoin.powerBasis hint).map (((Algebra.adjoin K {x}).equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv)

theorem PowerBasis.repr_gen_pow_isIntegral {S : Type u_2} [CommRing S] {R : Type u_3} [CommRing R] [Algebra R S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A} (hB : IsIntegral R B.gen) [IsDomain S] (hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (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} [CommRing S] {R : Type u_3} [CommRing R] [Algebra R S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A} (hB : IsIntegral R B.gen) [IsDomain S] {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 (algebraMap R S) (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} [CommRing S] {R : Type u_3} [CommRing R] [Algebra R S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A} (hB : IsIntegral R B.gen) [IsDomain S] {x : A} (hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) (hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (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} [Field K] [CommRing S] [Algebra K S] {R : Type u_3} [CommRing R] [Algebra R S] [Algebra R K] [IsScalarTower R K S] {B : PowerBasis K S} {B' : PowerBasis K S} {P : Polynomial R} (h : (Polynomial.aeval B.gen) P = B'.gen) (hB : IsIntegral R B.gen) (hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (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.