# Power basis #

This file defines a structure `PowerBasis 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 `PowerBasis` structure generated by `x`.

## Definitions #

- `PowerBasis 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) : Module.finrank K (AdjoinRoot f) = f.natDegree`, the dimension of `AdjoinRoot f` equals the degree of `f`

- `PowerBasis.lift (pb : PowerBasis R S)`: if `y : S'` satisfies the same equations as `pb.gen`, this is the map `S →ₐ[R] S'` sending `pb.gen` to `y`

- `PowerBasis.equiv`: if two power bases satisfy the same equations, they are equivalent as algebras

## Implementation notes #

Throughout this file, `R`, `S`, `A`, `B` ... are `CommRing`s, and `K`, `L`, ... are `Field`s. `S` is an `R`-algebra, `B` is an `A`-algebra, `L` is a `K`-algebra.

## Tags #

power basis, powerbasis

source
structure PowerBasis (R : Type u_7) (S : Type u_8) [CommRing R] [Ring S] [Algebra R S] :
Type (max u_7 u_8)

`pb : PowerBasis 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,IntermediateField}.adjoin.powerBasis`.

- gen : S
- dim : ℕ
- basis : Module.Basis (Fin self.dim) R S
- basis_eq_pow (i : Fin self.dim) : self.basis i = self.gen ^ ↑i

Instances For

source
@[simp]
theorem PowerBasis.coe_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) :
⇑pb.basis = fun (i : Fin pb.dim) => pb.gen ^ ↑i
source
theorem PowerBasis.finite {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) :
Module.Finite R S

Cannot be an instance because `PowerBasis` cannot be a class.

source
def Module.Basis.PowerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_7} [Fintype ι] (B : Basis ι R S) {x : S} (e : ι ≃ Fin (Fintype.card ι)) (hx : ∀ (i : ι), B i = x ^ ↑(e i)) :
PowerBasis R S

Construct a power basis from a basis consisting of powers of an element.

Equations

- B.PowerBasis e hx = { gen := x, dim := Fintype.card ι, basis := B.reindex e, basis_eq_pow := ⋯ }

Instances For

source
@[simp]
theorem Module.Basis.PowerBasis_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_7} [Fintype ι] (B : Basis ι R S) {x : S} (e : ι ≃ Fin (Fintype.card ι)) (hx : ∀ (i : ι), B i = x ^ ↑(e i)) :
(B.PowerBasis e hx).gen = x
source
theorem PowerBasis.finrank {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [StrongRankCondition R] (pb : PowerBasis R S) :
Module.finrank R S = pb.dim
source
theorem PowerBasis.mem_span_pow' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x y : S} {d : ℕ} :
y ∈ Submodule.span R (Set.range fun (i : Fin d) => x ^ ↑i) ↔ ∃ (f : Polynomial R), f.degree < ↑d ∧ y = (Polynomial.aeval x) f
source
theorem PowerBasis.mem_span_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x y : S} {d : ℕ} (hd : d ≠ 0) :
y ∈ Submodule.span R (Set.range fun (i : Fin d) => x ^ ↑i) ↔ ∃ (f : Polynomial R), f.natDegree < d ∧ y = (Polynomial.aeval x) f
source
theorem PowerBasis.dim_ne_zero {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) :
pb.dim ≠ 0
source
theorem PowerBasis.dim_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) :
0 < pb.dim
source
theorem PowerBasis.exists_eq_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) (y : S) :
∃ (f : Polynomial R), f.natDegree < pb.dim ∧ y = (Polynomial.aeval pb.gen) f
source
theorem PowerBasis.exists_eq_aeval' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) (y : S) :
∃ (f : Polynomial R), y = (Polynomial.aeval pb.gen) f
source
theorem PowerBasis.algHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S) ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) :
f = g
source
theorem PowerBasis.exists_smodEq {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (pb : PowerBasis A B) (b : B) :
∃ (a : A), b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
source
theorem PowerBasis.exists_gen_dvd_sub {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (pb : PowerBasis A B) (b : B) :
∃ (a : A), pb.gen ∣ b - (algebraMap A B) a
source
noncomputable def PowerBasis.minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
Polynomial A

`pb.minpolyGen` is the minimal polynomial for `pb.gen`.

Equations

- pb.minpolyGen = Polynomial.X ^ pb.dim - ∑ i : Fin pb.dim, Polynomial.C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * Polynomial.X ^ ↑i

Instances For

source
theorem PowerBasis.aeval_minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
(Polynomial.aeval pb.gen) pb.minpolyGen = 0
source
theorem PowerBasis.minpolyGen_monic {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
pb.minpolyGen.Monic
source
theorem PowerBasis.dim_le_natDegree_of_root {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) {p : Polynomial A} (ne_zero : p ≠ 0) (root : (Polynomial.aeval pb.gen) p = 0) :
pb.dim ≤ p.natDegree
source
theorem PowerBasis.dim_le_degree_of_root {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (h : PowerBasis A S) {p : Polynomial A} (ne_zero : p ≠ 0) (root : (Polynomial.aeval h.gen) p = 0) :
↑h.dim ≤ p.degree
source
theorem PowerBasis.degree_minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
pb.minpolyGen.degree = ↑pb.dim
source
theorem PowerBasis.natDegree_minpolyGen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
pb.minpolyGen.natDegree = pb.dim
source
@[simp]
theorem PowerBasis.minpolyGen_eq {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
pb.minpolyGen = minpoly A pb.gen
source
theorem PowerBasis.isIntegral_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
IsIntegral A pb.gen
source
@[simp]
theorem PowerBasis.degree_minpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
(minpoly A pb.gen).degree = ↑pb.dim
source
@[simp]
theorem PowerBasis.natDegree_minpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) :
(minpoly A pb.gen).natDegree = pb.dim
source
theorem PowerBasis.leftMulMatrix {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] (pb : PowerBasis A S) :
(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun (i j : Fin pb.dim) => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
source
theorem PowerBasis.constr_pow_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A) :
((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
source
theorem PowerBasis.constr_pow_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) :
((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) pb.gen = y
source
theorem PowerBasis.constr_pow_algebraMap {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (x : A) :
((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x
source
theorem PowerBasis.constr_pow_mul {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (x x' : S) :
((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) (x * x') = ((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) x * ((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i) x'
source
noncomputable def PowerBasis.lift {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) :
S →ₐ[A] S'

`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 `PowerBasis.liftEquiv` for a bundled equiv sending `⟨y, hy⟩` to the algebra map.

Equations

- pb.lift y hy = { toFun := ((pb.basis.constr A) fun (i : Fin pb.dim) => y ^ ↑i).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem PowerBasis.lift_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) :
(pb.lift y hy) pb.gen = y
source
@[simp]
theorem PowerBasis.lift_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis 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
source
noncomputable def PowerBasis.liftEquiv {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) :
(S →ₐ[A] S') ≃ { y : S' // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }

`pb.liftEquiv` 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 `PowerBasis.lift`. If the codomain of the `AlgHom`s is an integral domain, then the roots form a multiset, see `liftEquiv'` for the corresponding statement.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem PowerBasis.liftEquiv_symm_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : { y : S' // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }) :
pb.liftEquiv.symm y = pb.lift ↑y ⋯
source
@[simp]
theorem PowerBasis.liftEquiv_apply_coe {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (f : S →ₐ[A] S') :
↑(pb.liftEquiv f) = f pb.gen
source
noncomputable def PowerBasis.liftEquiv' {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra A S] [IsDomain B] (pb : PowerBasis A S) :
(S →ₐ[A] B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B }

`pb.liftEquiv'` 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.liftEquiv' = pb.liftEquiv.trans ((Equiv.refl B).subtypeEquiv ⋯)

Instances For

source
@[simp]
theorem PowerBasis.liftEquiv'_symm_apply_apply {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra A S] [IsDomain B] (pb : PowerBasis A S) (a✝ : { y : B // y ∈ (minpoly A pb.gen).aroots B }) :
⇑(pb.liftEquiv'.symm a✝) = ⇑((pb.basis.constr A) fun (i : Fin pb.dim) => ↑a✝ ^ ↑i)
source
@[simp]
theorem PowerBasis.liftEquiv'_apply_coe {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra A S] [IsDomain B] (pb : PowerBasis A S) (a✝ : S →ₐ[A] B) :
↑(pb.liftEquiv' a✝) = a✝ pb.gen
source
noncomputable def PowerBasis.AlgHom.fintype {S : Type u_2} [Ring S] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra A S] [IsDomain B] (pb : PowerBasis 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

- PowerBasis.AlgHom.fintype pb = Fintype.ofEquiv { y : B // y ∈ (minpoly A pb.gen).aroots B } pb.liftEquiv'.symm

Instances For

source
noncomputable def PowerBasis.equivOfRoot {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
S ≃ₐ[A] S'

`pb.equivOfRoot pb' h₁ h₂` is an equivalence of algebras with the same power basis, where "the same" means that `pb` is a root of `pb'`s minimal polynomial and vice versa.

See also `PowerBasis.equivOfMinpoly` which takes the hypothesis that the minimal polynomials are identical.

Equations

- pb.equivOfRoot pb' h₁ h₂ = AlgEquiv.ofAlgHom (pb.lift pb'.gen h₂) (pb'.lift pb.gen h₁) ⋯ ⋯

Instances For

source
theorem PowerBasis.equivOfRoot_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (a : S) :
(pb.equivOfRoot pb' h₁ h₂) a = (pb.lift pb'.gen h₂) a
source
@[simp]
theorem PowerBasis.equivOfRoot_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (f : Polynomial A) :
(pb.equivOfRoot pb' h₁ h₂) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
source
@[simp]
theorem PowerBasis.equivOfRoot_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
(pb.equivOfRoot pb' h₁ h₂) pb.gen = pb'.gen
source
@[simp]
theorem PowerBasis.equivOfRoot_symm {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) :
(pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁
source
noncomputable def PowerBasis.equivOfMinpoly {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
S ≃ₐ[A] S'

`pb.equivOfMinpoly pb' h` is an equivalence of algebras with the same power basis, where "the same" means that they have identical minimal polynomials.

See also `PowerBasis.equivOfRoot` which takes the hypothesis that each generator is a root of the other basis' minimal polynomial; `PowerBasis.equivOfRoot` is more general if `A` is not a field.

Equations

- pb.equivOfMinpoly pb' h = pb.equivOfRoot pb' ⋯ ⋯

Instances For

source
theorem PowerBasis.equivOfMinpoly_apply {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (a : S) :
(pb.equivOfMinpoly pb' h) a = (pb.lift pb'.gen ⋯) a
source
@[simp]
theorem PowerBasis.equivOfMinpoly_aeval {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : Polynomial A) :
(pb.equivOfMinpoly pb' h) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
source
@[simp]
theorem PowerBasis.equivOfMinpoly_gen {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
(pb.equivOfMinpoly pb' h) pb.gen = pb'.gen
source
@[simp]
theorem PowerBasis.equivOfMinpoly_symm {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] [Algebra A S] {S' : Type u_7} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
(pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb ⋯
source
theorem linearIndependent_pow {S : Type u_2} [Ring S] {K : Type u_6} [Field K] [Algebra K S] (x : S) :
LinearIndependent K fun (i : Fin (minpoly K x).natDegree) => 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.

source
theorem IsIntegral.mem_span_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial R] {x y : S} (hx : IsIntegral R x) (hy : ∃ (f : Polynomial R), y = (Polynomial.aeval x) f) :
y ∈ Submodule.span R (Set.range fun (i : Fin (minpoly R x).natDegree) => x ^ ↑i)
source
noncomputable def PowerBasis.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
PowerBasis R S'

`PowerBasis.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.toLinearEquiv, basis_eq_pow := ⋯ }

Instances For

source
@[simp]
theorem PowerBasis.map_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
(pb.map e).basis = pb.basis.map e.toLinearEquiv
source
@[simp]
theorem PowerBasis.map_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
(pb.map e).gen = e pb.gen
source
@[simp]
theorem PowerBasis.map_dim {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') :
(pb.map e).dim = pb.dim
source
theorem PowerBasis.minpolyGen_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') :
(pb.map e).minpolyGen = pb.minpolyGen
source
@[simp]
theorem PowerBasis.equivOfRoot_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0) (h₂ : (Polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0) :
pb.equivOfRoot (pb.map e) h₁ h₂ = e
source
@[simp]
theorem PowerBasis.equivOfMinpoly_map {S : Type u_2} [Ring S] {A : Type u_4} [CommRing A] {S' : Type u_7} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :
pb.equivOfMinpoly (pb.map e) h = e
source
theorem PowerBasis.adjoin_gen_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (B : PowerBasis R S) :
Algebra.adjoin R {B.gen} = ⊤
source
theorem PowerBasis.adjoin_eq_top_of_gen_mem_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {B : PowerBasis R S} {x : S} (hx : B.gen ∈ Algebra.adjoin R {x}) :
Algebra.adjoin R {x} = ⊤