mathlib3 documentation

ring_theory.adjoin.power_basis

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.

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

Equations
source
noncomputable def power_basis.of_gen_mem_adjoin {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [algebra K S] {x : S} (B : power_basis K S) (hint : is_integral K x) (hx : B.gen ∈ algebra.adjoin K {x}) :
power_basis K 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
source
@[simp]
theorem power_basis.of_gen_mem_adjoin_gen {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [algebra K S] {x : S} (B : power_basis K S) (hint : is_integral K x) (hx : B.gen ∈ algebra.adjoin K {x}) :
(B.of_gen_mem_adjoin hint hx).gen = x
source
@[simp]
theorem power_basis.of_gen_mem_adjoin_dim {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [algebra K S] {x : S} (B : power_basis K S) (hint : is_integral K x) (hx : B.gen ∈ algebra.adjoin K {x}) :
(B.of_gen_mem_adjoin hint hx).dim = (minpoly K x).nat_degree
source
theorem power_basis.repr_gen_pow_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [algebra R S] {A : Type u_4} [comm_ring A] [algebra R A] [algebra S A] [is_scalar_tower R S A] {B : power_basis S A} (hB : is_integral R B.gen) [is_domain S] (hmin : minpoly S B.gen = polynomial.map (algebra_map R S) (minpoly R B.gen)) (n : ℕ) (i : fin B.dim) :
is_integral R (⇑(⇑(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.

source
theorem power_basis.repr_mul_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [algebra R S] {A : Type u_4} [comm_ring A] [algebra R A] [algebra S A] [is_scalar_tower R S A] {B : power_basis S A} (hB : is_integral R B.gen) [is_domain S] {x y : A} (hx : ∀ (i : fin B.dim), is_integral R (⇑(⇑(B.basis.repr) x) i)) (hy : ∀ (i : fin B.dim), is_integral R (⇑(⇑(B.basis.repr) y) i)) (hmin : minpoly S B.gen = polynomial.map (algebra_map R S) (minpoly R B.gen)) (i : fin B.dim) :
is_integral R (⇑(⇑(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.

source
theorem power_basis.repr_pow_is_integral {S : Type u_2} [comm_ring S] {R : Type u_3} [comm_ring R] [algebra R S] {A : Type u_4} [comm_ring A] [algebra R A] [algebra S A] [is_scalar_tower R S A] {B : power_basis S A} (hB : is_integral R B.gen) [is_domain S] {x : A} (hx : ∀ (i : fin B.dim), is_integral R (⇑(⇑(B.basis.repr) x) i)) (hmin : minpoly S B.gen = polynomial.map (algebra_map R S) (minpoly R B.gen)) (n : ℕ) (i : fin B.dim) :
is_integral R (⇑(⇑(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.

source
theorem power_basis.to_matrix_is_integral {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [algebra K S] {R : Type u_3} [comm_ring R] [algebra R S] [algebra R K] [is_scalar_tower R K S] {B B' : power_basis K S} {P : polynomial R} (h : ⇑(polynomial.aeval B.gen) P = B'.gen) (hB : is_integral R B.gen) (hmin : minpoly K B.gen = polynomial.map (algebra_map R K) (minpoly R B.gen)) (i : fin B.dim) (j : fin B'.dim) :
is_integral R (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.