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 CommRings, and K, L, ... are Fields. S is an R-algebra, B is an A-algebra, L is a K-algebra.

Tags

power basis, powerbasis

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

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

@[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

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.

noncomputable def Module.Basis.PowerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_6} [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 := ⋯ }

@[simp]

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

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

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

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

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

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

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

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

theorem PowerBasis.algHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_6} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S) ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) : f = g

theorem PowerBasis.exists_smodEq {A : Type u_3} {B : Type u_4} [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}]

theorem PowerBasis.exists_gen_dvd_sub {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (pb : PowerBasis A B) (b : B) : ∃ (a : A), pb.gen ∣ b - (algebraMap A B) a

noncomputable def PowerBasis.minpolyGen {S : Type u_2} [Ring S] {A : Type u_3} [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

theorem PowerBasis.aeval_minpolyGen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) : (Polynomial.aeval pb.gen) pb.minpolyGen = 0

theorem PowerBasis.minpolyGen_monic {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) : pb.minpolyGen.Monic

theorem PowerBasis.dim_le_natDegree_of_root {S : Type u_2} [Ring S] {A : Type u_3} [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

theorem PowerBasis.dim_le_degree_of_root {S : Type u_2} [Ring S] {A : Type u_3} [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

theorem PowerBasis.degree_minpolyGen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) : pb.minpolyGen.degree = ↑pb.dim

theorem PowerBasis.natDegree_minpolyGen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) : pb.minpolyGen.natDegree = pb.dim

@[simp]

theorem PowerBasis.minpolyGen_eq {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) : pb.minpolyGen = minpoly A pb.gen

theorem PowerBasis.isIntegral_gen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) : IsIntegral A pb.gen

@[simp]

theorem PowerBasis.degree_minpoly {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) : (minpoly A pb.gen).degree = ↑pb.dim

@[simp]

theorem PowerBasis.natDegree_minpoly {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] [Nontrivial A] (pb : PowerBasis A S) : (minpoly A pb.gen).natDegree = pb.dim

theorem PowerBasis.leftMulMatrix {S : Type u_2} [Ring S] {A : Type u_3} [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

theorem PowerBasis.constr_pow_aeval {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

theorem PowerBasis.constr_pow_gen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

theorem PowerBasis.constr_pow_algebraMap {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

theorem PowerBasis.constr_pow_mul {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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'

noncomputable def PowerBasis.lift {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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' := ⋯ }

@[simp]

theorem PowerBasis.lift_gen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.lift_aeval {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

noncomputable def PowerBasis.liftEquiv {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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 AlgHoms 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.

@[simp]

theorem PowerBasis.liftEquiv_symm_apply {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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 ⋯

@[simp]

theorem PowerBasis.liftEquiv_apply_coe {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (f : S →ₐ[A] S') : ↑(pb.liftEquiv f) = f pb.gen

noncomputable def PowerBasis.liftEquiv' {S : Type u_2} [Ring S] {A : Type u_3} {B : Type u_4} [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 ⋯)

@[simp]

theorem PowerBasis.liftEquiv'_symm_apply_apply {S : Type u_2} [Ring S] {A : Type u_3} {B : Type u_4} [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)

@[simp]

theorem PowerBasis.liftEquiv'_apply_coe {S : Type u_2} [Ring S] {A : Type u_3} {B : Type u_4} [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

@[instance_reducible]

noncomputable def PowerBasis.AlgHom.fintype {S : Type u_2} [Ring S] {A : Type u_3} {B : Type u_4} [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

noncomputable def PowerBasis.equivOfRoot {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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₁) ⋯ ⋯

theorem PowerBasis.equivOfRoot_apply {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfRoot_aeval {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfRoot_gen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfRoot_symm {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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₁

noncomputable def PowerBasis.equivOfMinpoly {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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' ⋯ ⋯

theorem PowerBasis.equivOfMinpoly_apply {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfMinpoly_aeval {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfMinpoly_gen {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfMinpoly_symm {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [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 ⋯

theorem linearIndependent_pow {S : Type u_2} [Ring S] {K : Type u_5} [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.

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)

noncomputable def PowerBasis.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_6} [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, basis_eq_pow := ⋯ }

@[simp]

theorem PowerBasis.map_dim {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_6} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).dim = pb.dim

@[simp]

theorem PowerBasis.map_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_6} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).gen = e pb.gen

@[simp]

theorem PowerBasis.map_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_6} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).basis = pb.basis.map ↑e

theorem PowerBasis.minpolyGen_map {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] {S' : Type u_6} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') : (pb.map e).minpolyGen = pb.minpolyGen

@[simp]

theorem PowerBasis.equivOfRoot_map {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] {S' : Type u_6} [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

@[simp]

theorem PowerBasis.equivOfMinpoly_map {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] {S' : Type u_6} [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

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) : R[B.gen] = ⊤

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 ∈ R[x]) : R[x] = ⊤