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) : Module.Basis (Fin (minpoly K x).natDegree) K ↥(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 = Module.Basis.mk ⋯ ⋯

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 ↥(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 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) : (powerBasis hx).gen = ⟨x, ⋯⟩

@[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) : (powerBasis hx).dim = (minpoly K x).natDegree

noncomputable def PowerBasis.ofAdjoinEqTop {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) (hx' : Algebra.adjoin K {x} = ⊤) : PowerBasis K S

If x generates S over K and is integral over K, then it defines a power basis. See PowerBasis.ofAdjoinEqTop' for a version over a more general base ring.

Equations

• PowerBasis.ofAdjoinEqTop hx hx' = (Algebra.adjoin.powerBasis hx).map (((Algebra.adjoin K {x}).equivOfEq ⊤ hx').trans Subalgebra.topEquiv)

@[simp]

theorem PowerBasis.ofAdjoinEqTop_gen {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) (hx' : Algebra.adjoin K {x} = ⊤) : (ofAdjoinEqTop hx hx').gen = x

@[simp]

theorem PowerBasis.ofAdjoinEqTop_dim {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) (hx' : Algebra.adjoin K {x} = ⊤) : (ofAdjoinEqTop hx hx').dim = (minpoly K x).natDegree

@[deprecated PowerBasis.ofAdjoinEqTop "Use in combination with `PowerBasis.adjoin_eq_top_of_gen_mem_adjoin` to recover the deprecated definition" (since := "2025-09-29")]

def Algebra.PowerBasis.ofGenMemAdjoin {K : Type u_1} {S : Type u_2} [Field K] [CommRing S] [Algebra K S] {x : S} (hx : IsIntegral K x) (hx' : adjoin K {x} = ⊤) : PowerBasis K S

Alias of PowerBasis.ofAdjoinEqTop.

---

If x generates S over K and is integral over K, then it defines a power basis. See PowerBasis.ofAdjoinEqTop' for a version over a more general base ring.

Equations

• @Algebra.PowerBasis.ofGenMemAdjoin = @PowerBasis.ofAdjoinEqTop

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) (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) {x 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) {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 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.