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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def algebra.adjoin.power_basis_aux {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
basis (fin (minpoly K x).nat_degree) 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
@[simp]
theorem algebra.adjoin.power_basis_gen {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
= x, _⟩
@[simp]
theorem algebra.adjoin.power_basis_dim {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
noncomputable def algebra.adjoin.power_basis {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
{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.power_basis' for a version over a more general base ring.

Equations
noncomputable def power_basis.of_gen_mem_adjoin {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (B : S) (hint : x) (hx : B.gen {x}) :
S

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

Equations
@[simp]
theorem power_basis.of_gen_mem_adjoin_gen {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (B : S) (hint : x) (hx : B.gen {x}) :
@[simp]
theorem power_basis.of_gen_mem_adjoin_dim {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (B : S) (hint : x) (hx : B.gen {x}) :
theorem power_basis.repr_gen_pow_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [ S] {A : Type u_4} [comm_ring A] [ A] [ A] [ A] {B : A} (hB : B.gen) [is_domain S] (hmin : B.gen = (minpoly R B.gen)) (n : ) (i : fin B.dim) :
(((B.basis.repr) (B.gen ^ n)) i)

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

theorem power_basis.repr_mul_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [ S] {A : Type u_4} [comm_ring A] [ A] [ A] [ A] {B : A} (hB : B.gen) [is_domain S] {x y : A} (hx : (i : fin B.dim), (((B.basis.repr) x) i)) (hy : (i : fin B.dim), (((B.basis.repr) y) i)) (hmin : B.gen = (minpoly R B.gen)) (i : fin B.dim) :
(((B.basis.repr) (x * y)) i)

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

theorem power_basis.repr_pow_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [ S] {A : Type u_4} [comm_ring A] [ A] [ A] [ A] {B : A} (hB : B.gen) [is_domain S] {x : A} (hx : (i : fin B.dim), (((B.basis.repr) x) i)) (hmin : B.gen = (minpoly R B.gen)) (n : ) (i : fin B.dim) :
(((B.basis.repr) (x ^ n)) i)

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

theorem power_basis.to_matrix_is_integral {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {R : Type u_3} [comm_ring R] [ S] [ K] [ S] {B B' : S} {P : polynomial R} (h : P = B'.gen) (hB : B.gen) (hmin : B.gen = (minpoly R B.gen)) (i : fin B.dim) (j : fin B'.dim) :
(B.basis.to_matrix (B'.basis) i j)

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