Documentation

Mathlib.RingTheory.Adjoin.PowerBasis

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
Instances For
    @[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,
    @[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
    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) :

    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
    Instances For
      @[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
      @[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
      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}) :

      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} [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} [IsDomain S] (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 : 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.