mathlib documentation

ring_theory.power_basis

Power basis #

This file defines a structure power_basis R S, giving a basis of the R-algebra S as a finite list of powers 1, x, ..., x^n. For example, if x is algebraic over a ring/field, adjoining x gives a power_basis structure generated by x.

Definitions #

power_basis R A: a structure containing an x and an n such that 1, x, ..., x^n is a basis for the R-algebra A (viewed as an R-module).
finrank (hf : f ≠ 0) : finite_dimensional.finrank K (adjoin_root f) = f.nat_degree, the dimension of adjoin_root f equals the degree of f
power_basis.lift (pb : power_basis R S): if y : S' satisfies the same equations as pb.gen, this is the map S →ₐ[R] S' sending pb.gen to y
power_basis.equiv: if two power bases satisfy the same equations, they are equivalent as algebras

Implementation notes #

Throughout this file, R, S, ... are comm_rings, A, B, ... are integral_domains and K, L, ... are fields. S is an R-algebra, B is an A-algebra, L is a K-algebra.

Tags #

power basis, powerbasis

@[nolint]

structure power_basis (R : Type u_8) (S : Type u_9) [comm_ring R] [ring S] [algebra R S] :

Type (max u_8 u_9)

gen : S
dim : ℕ
basis : basis (fin self.dim) R S
basis_eq_pow : ∀ (i : fin self.dim), ⇑(self.basis) i = self.gen ^ ↑i

pb : power_basis R S states that 1, pb.gen, ..., pb.gen ^ (pb.dim - 1) is a basis for the R-algebra S (viewed as R-module).

This is a structure, not a class, since the same algebra can have many power bases. For the common case where S is defined by adjoining an integral element to R, the canonical power basis is given by {algebra,intermediate_field}.adjoin.power_basis.

@[simp]

theorem power_basis.coe_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) :

⇑(pb.basis) = λ (i : fin pb.dim), pb.gen ^ ↑i

theorem power_basis.finite_dimensional {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :

finite_dimensional K S

Cannot be an instance because power_basis cannot be a class.

theorem power_basis.finrank {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :

finite_dimensional.finrank K S = pb.dim

theorem power_basis.mem_span_pow' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x y : S} {d : ℕ} :

y ∈ submodule.span R (set.range (λ (i : fin d), x ^ ↑i)) ↔ ∃ (f : polynomial R), f.degree < ↑d ∧ y = ⇑(polynomial.aeval x) f

theorem power_basis.mem_span_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {x y : S} {d : ℕ} (hd : d ≠ 0) :

y ∈ submodule.span R (set.range (λ (i : fin d), x ^ ↑i)) ↔ ∃ (f : polynomial R), f.nat_degree < d ∧ y = ⇑(polynomial.aeval x) f

theorem power_basis.dim_ne_zero {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [h : nontrivial S] (pb : power_basis R S) :

pb.dim ≠ 0

theorem power_basis.dim_pos {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial S] (pb : power_basis R S) :

0 < pb.dim

theorem power_basis.exists_eq_aeval {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial S] (pb : power_basis R S) (y : S) :

∃ (f : polynomial R), f.nat_degree < pb.dim ∧ y = ⇑(polynomial.aeval pb.gen) f

theorem power_basis.exists_eq_aeval' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (pb : power_basis R S) (y : S) :

∃ (f : polynomial R), y = ⇑(polynomial.aeval pb.gen) f

theorem power_basis.alg_hom_ext {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_3} [semiring S'] [algebra R S'] (pb : power_basis R S) ⦃f g : S →ₐ[R] S'⦄ (h : ⇑f pb.gen = ⇑g pb.gen) :

f = g

def power_basis.minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

pb.minpoly_gen is a minimal polynomial for pb.gen.

If A is not a field, it might not necessarily be the minimal polynomial, however nat_degree_minpoly shows its degree is indeed minimal.

Equations

pb.minpoly_gen = polynomial.X ^ pb.dim - ∑ (i : fin pb.dim), (⇑polynomial.C (⇑(⇑(pb.basis.repr) (pb.gen ^ pb.dim)) i)) * polynomial.X ^ ↑i

@[simp]

theorem power_basis.degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

pb.minpoly_gen.degree = ↑(pb.dim)

@[simp]

theorem power_basis.nat_degree_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

pb.minpoly_gen.nat_degree = pb.dim

theorem power_basis.minpoly_gen_monic {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

pb.minpoly_gen.monic

@[simp]

theorem power_basis.aeval_minpoly_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

⇑(polynomial.aeval pb.gen) pb.minpoly_gen = 0

theorem power_basis.is_integral_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

is_integral A pb.gen

theorem power_basis.dim_le_nat_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (h : power_basis A S) {p : polynomial A} (ne_zero : p ≠ 0) (root : ⇑(polynomial.aeval h.gen) p = 0) :

h.dim ≤ p.nat_degree

theorem power_basis.dim_le_degree_of_root {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (h : power_basis A S) {p : polynomial A} (ne_zero : p ≠ 0) (root : ⇑(polynomial.aeval h.gen) p = 0) :

↑(h.dim) ≤ p.degree

@[simp]

theorem power_basis.nat_degree_minpoly {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] (pb : power_basis A S) :

(minpoly A pb.gen).nat_degree = pb.dim

@[simp]

theorem power_basis.minpoly_gen_eq {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] (pb : power_basis K S) :

pb.minpoly_gen = minpoly K pb.gen

theorem power_basis.nat_degree_lt_nat_degree {R : Type u_1} [comm_ring R] {p q : polynomial R} (hp : p ≠ 0) (hpq : p.degree < q.degree) :

p.nat_degree < q.nat_degree

theorem power_basis.constr_pow_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) (f : polynomial A) :

⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval y) f

theorem power_basis.constr_pow_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) :

⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) pb.gen = y

theorem power_basis.constr_pow_algebra_map {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) (x : A) :

⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) (⇑(algebra_map A S) x) = ⇑(algebra_map A S') x

theorem power_basis.constr_pow_mul {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) {y : S'} (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) (x x' : S) :

⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) (x * x') = (⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) x) * ⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)) x'

def power_basis.lift {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (y : S') (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) :

pb.lift y hy is the algebra map sending pb.gen to y, where hy states the higher powers of y are the same as the higher powers of pb.gen.

See power_basis.lift_equiv for a bundled equiv sending ⟨y, hy⟩ to the algebra map.

Equations

pb.lift y hy = {to_fun := (⇑(pb.basis.constr A) (λ (i : fin pb.dim), y ^ ↑i)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

@[simp]

theorem power_basis.lift_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (y : S') (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) :

⇑(pb.lift y hy) pb.gen = y

@[simp]

theorem power_basis.lift_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (y : S') (hy : ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0) (f : polynomial A) :

⇑(pb.lift y hy) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval y) f

@[simp]

theorem power_basis.lift_equiv_apply_coe {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (f : S →ₐ[A] S') :

↑(⇑(pb.lift_equiv) f) = ⇑f pb.gen

@[simp]

theorem power_basis.lift_equiv_symm_apply {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (y : {y // ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0}) :

⇑(pb.lift_equiv.symm) y = pb.lift ↑y _

def power_basis.lift_equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) :

(S →ₐ[A] S') ≃ {y // ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0}

pb.lift_equiv states that roots of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

This is the bundled equiv version of power_basis.lift. If the codomain of the alg_homs is an integral domain, then the roots form a multiset, see lift_equiv' for the corresponding statement.

Equations

pb.lift_equiv = {to_fun := λ (f : S →ₐ[A] S'), ⟨⇑f pb.gen, _⟩, inv_fun := λ (y : {y // ⇑(polynomial.aeval y) (minpoly A pb.gen) = 0}), pb.lift ↑y _, left_inv := _, right_inv := _}

@[simp]

theorem power_basis.lift_equiv'_apply_coe {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [integral_domain A] [integral_domain B] [algebra A B] [algebra A S] (pb : power_basis A S) (ᾰ : S →ₐ[A] B) :

↑(⇑(pb.lift_equiv') ᾰ) = ⇑ᾰ pb.gen

@[simp]

theorem power_basis.lift_equiv'_symm_apply_apply {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [integral_domain A] [integral_domain B] [algebra A B] [algebra A S] (pb : power_basis A S) (ᾰ : {y // y ∈ (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots}) :

⇑(⇑(pb.lift_equiv'.symm) ᾰ) = ⇑(⇑(pb.basis.constr A) (λ (i : fin pb.dim), ↑ᾰ ^ ↑i))

def power_basis.lift_equiv' {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [integral_domain A] [integral_domain B] [algebra A B] [algebra A S] (pb : power_basis A S) :

(S →ₐ[A] B) ≃ {y // y ∈ (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots}

pb.lift_equiv' states that elements of the root set of the minimal polynomial of pb.gen correspond to maps sending pb.gen to that root.

Equations

pb.lift_equiv' = pb.lift_equiv.trans ((equiv.refl B).subtype_equiv _)

def power_basis.alg_hom.fintype {S : Type u_2} [comm_ring S] {A : Type u_4} {B : Type u_5} [integral_domain A] [integral_domain B] [algebra A B] [algebra A S] (pb : power_basis A S) :

fintype (S →ₐ[A] B)

There are finitely many algebra homomorphisms S →ₐ[A] B if S is of the form A[x] and B is an integral domain.

Equations

power_basis.alg_hom.fintype pb = let _inst : decidable_eq B := classical.dec_eq B in fintype.of_equiv {y // y ∈ (polynomial.map (algebra_map A B) (minpoly A pb.gen)).roots} pb.lift_equiv'.symm

def power_basis.equiv {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :

pb.equiv pb' h is an equivalence of algebras with the same power basis.

Equations

pb.equiv pb' h = alg_equiv.of_alg_hom (pb.lift pb'.gen _) (pb'.lift pb.gen _) _ _

@[simp]

theorem power_basis.equiv_aeval {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : polynomial A) :

⇑(pb.equiv pb' h) (⇑(polynomial.aeval pb.gen) f) = ⇑(polynomial.aeval pb'.gen) f

@[simp]

theorem power_basis.equiv_gen {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :

⇑(pb.equiv pb' h) pb.gen = pb'.gen

@[simp]

theorem power_basis.equiv_symm {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] [algebra A S] {S' : Type u_8} [comm_ring S'] [algebra A S'] (pb : power_basis A S) (pb' : power_basis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :

(pb.equiv pb' h).symm = pb'.equiv pb _

theorem is_integral.linear_independent_pow {S : Type u_2} [comm_ring S] {K : Type u_6} [field K] [algebra K S] {x : S} (hx : is_integral K x) :

linear_independent K (λ (i : fin (minpoly K x).nat_degree), x ^ ↑i)

Useful lemma to show x generates a power basis: the powers of x less than the degree of x's minimal polynomial are linearly independent.

theorem is_integral.mem_span_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [nontrivial R] {x y : S} (hx : is_integral R x) (hy : ∃ (f : polynomial R), y = ⇑(polynomial.aeval x) f) :

y ∈ submodule.span R (set.range (λ (i : fin (minpoly R x).nat_degree), x ^ ↑i))

@[simp]

theorem power_basis.map_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :

(pb.map e).basis = pb.basis.map e.to_linear_equiv

@[simp]

theorem power_basis.map_dim {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :

(pb.map e).dim = pb.dim

def power_basis.map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :

power_basis R S'

power_basis.map pb (e : S ≃ₐ[R] S') is the power basis for S' generated by e pb.gen.

Equations

pb.map e = {gen := ⇑e pb.gen, dim := pb.dim, basis := pb.basis.map e.to_linear_equiv, basis_eq_pow := _}

@[simp]

theorem power_basis.map_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {S' : Type u_8} [comm_ring S'] [algebra R S'] (pb : power_basis R S) (e : S ≃ₐ[R] S') :

(pb.map e).gen = ⇑e pb.gen

@[simp]

theorem power_basis.minpoly_gen_map {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] {S' : Type u_8} [comm_ring S'] [algebra A S] [algebra A S'] (pb : power_basis A S) (e : S ≃ₐ[A] S') :

(pb.map e).minpoly_gen = pb.minpoly_gen

@[simp]

theorem power_basis.equiv_map {S : Type u_2} [comm_ring S] {A : Type u_4} [integral_domain A] {S' : Type u_8} [comm_ring S'] [algebra A S] [algebra A S'] (pb : power_basis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :

pb.equiv (pb.map e) h = e