Mathlib.RingTheory.PowerBasis

PowerBasis structure

(R S : Type*) [CommRing R] [Ring S] [Algebra R S]

Full source

/-- `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`.
-/
structure PowerBasis (R S : Type*) [CommRing R] [Ring S] [Algebra R S] where
  gen : S
  dim : ℕ
  basis : Basis (Fin dim) R S
  basis_eq_pow : ∀ (i), basis i = gen ^ (i : ℕ)

Power Basis of an Algebra

Informal description

A structure `PowerBasis R S` represents a basis of the `R`-algebra `S` as an `R`-module, consisting of powers of a single element `x = pb.gen`. Specifically, the basis is given by the list `1, x, x^2, ..., x^{n-1}`, where `n = pb.dim` is the dimension of `S` as an `R`-module. This structure is used when `S` is obtained by adjoining an algebraic element `x` to `R`.

PowerBasis.coe_basis theorem

(pb : PowerBasis R S) : ⇑pb.basis = fun i : Fin pb.dim => pb.gen ^ (i : ℕ)

Full source

@[simp]
theorem coe_basis (pb : PowerBasis R S) : ⇑pb.basis = fun i : Fin pb.dim => pb.gen ^ (i : ℕ) :=
  funext pb.basis_eq_pow

Power Basis Vectors as Powers of Generator

Informal description

Let $S$ be an $R$-algebra with a power basis $\text{pb}$ generated by an element $x = \text{pb.gen}$. Then the basis vectors of $\text{pb.basis}$ are given by the powers of $x$, specifically, for each index $i$ in $\text{Fin}(\text{pb.dim})$, the $i$-th basis vector is $x^i$.

PowerBasis.finite theorem

(pb : PowerBasis R S) : Module.Finite R S

Full source

/-- Cannot be an instance because `PowerBasis` cannot be a class. -/
theorem finite (pb : PowerBasis R S) : Module.Finite R S := .of_basis pb.basis

Finiteness of Modules with Power Basis

Informal description

For any power basis `pb` of an `R`-algebra `S`, the algebra `S` is finitely generated as an `R`-module.

PowerBasis.finrank theorem

[StrongRankCondition R] (pb : PowerBasis R S) : Module.finrank R S = pb.dim

Full source

theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) :
    Module.finrank R S = pb.dim := by
  rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]

Finite rank equals dimension for power basis

Informal description

Let $R$ be a commutative ring satisfying the strong rank condition, and let $S$ be an $R$-algebra with a power basis $\text{pb}$. Then the finite rank of $S$ as an $R$-module is equal to the dimension $\text{pb.dim}$ of the power basis.

PowerBasis.mem_span_pow' theorem

 {x y : S} {d : ℕ} :
  y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔ ∃ f : R[X], f.degree < d ∧ y = aeval x f

Full source

theorem mem_span_pow' {x y : S} {d : ℕ} :
    y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ))y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔
      ∃ f : R[X], f.degree < d ∧ y = aeval x f := by
  have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) := by
    ext n
    simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
    exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
  simp only [this, mem_span_image_iff_linearCombination, degree_lt_iff_coeff_zero, Finsupp.support,
    exists_iff_exists_finsupp, coeff, aeval_def, eval₂RingHom', eval₂_eq_sum, Polynomial.sum,
    mem_supported', linearCombination, Finsupp.sum, Algebra.smul_def, eval₂_zero, exists_prop,
    LinearMap.id_coe, eval₂_one, id, not_lt, Finsupp.coe_lsum, LinearMap.coe_smulRight,
    Finset.mem_range, AlgHom.coe_mks, Finset.mem_coe]
  simp_rw [@eq_comm _ y]
  exact Iff.rfl

Characterization of Elements in the Power Span via Polynomial Evaluation

Informal description

Let $R$ be a commutative ring and $S$ an $R$-algebra. For elements $x, y \in S$ and a natural number $d$, the following are equivalent: 1. $y$ belongs to the $R$-submodule spanned by $\{x^i \mid 0 \leq i < d\}$. 2. There exists a polynomial $f \in R[X]$ such that $\deg(f) < d$ and $y = f(x)$ (where $f(x)$ denotes the evaluation of $f$ at $x$ via the algebra structure).

PowerBasis.mem_span_pow theorem

 {x y : S} {d : ℕ} (hd : d ≠ 0) :
  y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔ ∃ f : R[X], f.natDegree < d ∧ y = aeval x f

Full source

theorem mem_span_pow {x y : S} {d : ℕ} (hd : d ≠ 0) :
    y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ))y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔
      ∃ f : R[X], f.natDegree < d ∧ y = aeval x f := by
  rw [mem_span_pow']
  constructor <;>
    · rintro ⟨f, h, hy⟩
      refine ⟨f, ?_, hy⟩
      by_cases hf : f = 0
      · simp only [hf, natDegree_zero, degree_zero] at h ⊢
        first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
      simp_all only [degree_eq_natDegree hf]
      · first | exact WithBot.coe_lt_coe.1 h | exact WithBot.coe_lt_coe.2 h

Polynomial Characterization of Elements in Power Span for Nonzero Degree

Informal description

Let $R$ be a commutative ring and $S$ an $R$-algebra. For elements $x, y \in S$ and a nonzero natural number $d$, the following are equivalent: 1. $y$ belongs to the $R$-submodule spanned by $\{x^i \mid 0 \leq i < d\}$. 2. There exists a polynomial $f \in R[X]$ such that $\text{natDegree}(f) < d$ and $y = f(x)$, where $f(x)$ denotes the evaluation of $f$ at $x$ via the algebra structure.

PowerBasis.dim_ne_zero theorem

[Nontrivial S] (pb : PowerBasis R S) : pb.dim ≠ 0

Full source

theorem dim_ne_zero [Nontrivial S] (pb : PowerBasis R S) : pb.dim ≠ 0 := fun h =>
  not_nonempty_iff.mpr (h.symm ▸ Fin.isEmpty : IsEmpty (Fin pb.dim)) pb.basis.index_nonempty

Nonzero Dimension of Power Basis in Nontrivial Algebra

Informal description

For any nontrivial $R$-algebra $S$ with a power basis $\mathrm{pb}$ over $R$, the dimension $\mathrm{pb}.\mathrm{dim}$ is nonzero.

PowerBasis.dim_pos theorem

[Nontrivial S] (pb : PowerBasis R S) : 0 < pb.dim

Full source

theorem dim_pos [Nontrivial S] (pb : PowerBasis R S) : 0 < pb.dim :=
  Nat.pos_of_ne_zero pb.dim_ne_zero

Positive Dimension of Power Basis in Nontrivial Algebra

Informal description

For any nontrivial $R$-algebra $S$ with a power basis $\mathrm{pb}$ over $R$, the dimension $\mathrm{pb}.\mathrm{dim}$ is strictly positive.

PowerBasis.exists_eq_aeval theorem

[Nontrivial S] (pb : PowerBasis R S) (y : S) : ∃ f : R[X], f.natDegree < pb.dim ∧ y = aeval pb.gen f

Full source

theorem exists_eq_aeval [Nontrivial S] (pb : PowerBasis R S) (y : S) :
    ∃ f : R[X], f.natDegree < pb.dim ∧ y = aeval pb.gen f :=
  (mem_span_pow pb.dim_ne_zero).mp (by simpa using pb.basis.mem_span y)

Polynomial Representation of Elements in Power Basis Algebra

Informal description

Let $S$ be a nontrivial $R$-algebra with a power basis $\mathrm{pb}$ over $R$, generated by an element $x = \mathrm{pb.gen}$. For any element $y \in S$, there exists a polynomial $f \in R[X]$ such that the degree of $f$ is less than the dimension $\mathrm{pb.dim}$ of the power basis and $y = f(x)$, where $f(x)$ denotes the evaluation of $f$ at $x$ via the algebra structure.

PowerBasis.exists_eq_aeval' theorem

(pb : PowerBasis R S) (y : S) : ∃ f : R[X], y = aeval pb.gen f

Full source

theorem exists_eq_aeval' (pb : PowerBasis R S) (y : S) : ∃ f : R[X], y = aeval pb.gen f := by
  nontriviality S
  obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
  exact ⟨f, hf⟩

Polynomial Representation of Elements in Power Basis Algebra (Unrestricted Degree Version)

Informal description

Let $S$ be an $R$-algebra with a power basis $\mathrm{pb}$ over $R$, generated by an element $x = \mathrm{pb.gen}$. For any element $y \in S$, there exists a polynomial $f \in R[X]$ such that $y = f(x)$, where $f(x)$ denotes the evaluation of $f$ at $x$ via the algebra structure.

PowerBasis.algHom_ext theorem

 {S' : Type*} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S) ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) : f = g

Full source

theorem algHom_ext {S' : Type*} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S)
    ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) : f = g := by
  ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

Uniqueness of Algebra Homomorphisms on Power Basis Algebras via Generator Equality

Informal description

Let $S$ be an $R$-algebra with a power basis $\mathrm{pb}$ over $R$, generated by an element $x = \mathrm{pb.gen}$. For any $R$-algebra $S'$ and any two $R$-algebra homomorphisms $f, g: S \to S'$, if $f(x) = g(x)$, then $f = g$.

PowerBasis.exists_smodEq theorem

(pb : PowerBasis A B) (b : B) : ∃ a, SModEq (Ideal.span ({ pb.gen })) b (algebraMap A B a)

Full source

theorem exists_smodEq (pb : PowerBasis A B) (b : B) :
    ∃ a, SModEq (Ideal.span ({pb.gen})) b (algebraMap A B a) := by
  rcases subsingleton_or_nontrivial B
  · exact ⟨0, by rw [SModEq, Subsingleton.eq_zero b, map_zero]⟩
  refine ⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩
  have H := pb.basis.sum_repr b
  rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (not_mem_erase _ _)] at H
  rw [SModEq, ← add_zero (algebraMap _ _ _), Quotient.mk_add]
  nth_rewrite 1 [← H]
  rw [Quotient.mk_add]
  congr 1
  · simp [Algebra.algebraMap_eq_smul_one ((pb.basis.repr b) _)]
  · rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]
    refine sum_mem _ (fun i hi ↦ ?_)
    rw [Algebra.smul_def']
    refine Ideal.mul_mem_left _ _ <| Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ <|
      Nat.pos_of_ne_zero <| fun h ↦ not_mem_erase i univ <| Fin.eq_mk_iff_val_eq.2 h ▸ hi

Existence of Congruent Element in Power Basis Modulo Generator Ideal

Informal description

Let $B$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by $x = \mathrm{pb.gen}$. For any element $b \in B$, there exists an element $a \in A$ such that $b$ is congruent to $\mathrm{algebraMap}_A^B(a)$ modulo the ideal generated by $x$, i.e., $b \equiv a \ [\mathrm{mod}\ (x)]$.

PowerBasis.exists_gen_dvd_sub theorem

(pb : PowerBasis A B) (b : B) : ∃ a, pb.gen ∣ b - algebraMap A B a

Full source

theorem exists_gen_dvd_sub (pb : PowerBasis A B) (b : B) : ∃ a, pb.gen ∣ b - algebraMap A B a := by
  simpa [← Ideal.mem_span_singleton, ← mk_eq_zero, mk_sub, sub_eq_zero] using pb.exists_smodEq b

Divisibility of Differences by Power Basis Generator

Informal description

Let $B$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by $x = \mathrm{pb.gen}$. For any element $b \in B$, there exists an element $a \in A$ such that $x$ divides $b - \mathrm{algebraMap}_A^B(a)$ in $B$.

PowerBasis.minpolyGen definition

(pb : PowerBasis A S) : A[X]

Full source

/-- `pb.minpolyGen` is the minimal polynomial for `pb.gen`. -/
noncomputable def minpolyGen (pb : PowerBasis A S) : A[X] :=
  X ^ pb.dim - ∑ i : Fin pb.dim, C (pb.basis.repr (pb.gen ^ pb.dim) i) * X ^ (i : ℕ)

Minimal polynomial of a power basis generator

Informal description

Given a power basis `pb` of an `A`-algebra `S`, the minimal polynomial of the generator `pb.gen` is defined as the monic polynomial $X^n - \sum_{i=0}^{n-1} c_i X^i$, where $n$ is the dimension of the basis and $c_i$ are the coefficients obtained by expressing $(\text{pb.gen})^n$ in terms of the basis $1, \text{pb.gen}, \ldots, (\text{pb.gen})^{n-1}$.

PowerBasis.aeval_minpolyGen theorem

(pb : PowerBasis A S) : aeval pb.gen (minpolyGen pb) = 0

Full source

theorem aeval_minpolyGen (pb : PowerBasis A S) : aeval pb.gen (minpolyGen pb) = 0 := by
  simp_rw [minpolyGen, map_sub, map_sum, map_mul, map_pow, aeval_C, ← Algebra.smul_def, aeval_X]
  refine sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)
  rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype] <;>
    simp only [pb.coe_basis, zero_smul, eq_self_iff_true, imp_true_iff]

Minimal polynomial of power basis generator vanishes at the generator

Informal description

Let $S$ be an $A$-algebra with a power basis $\text{pb}$ generated by an element $x = \text{pb.gen}$. Then the minimal polynomial $\text{minpolyGen}(\text{pb})$ of $x$ satisfies $\text{aeval}_x(\text{minpolyGen}(\text{pb})) = 0$, where $\text{aeval}_x$ denotes the evaluation of the polynomial at $x$ via the $A$-algebra structure on $S$.

PowerBasis.dim_le_natDegree_of_root theorem

(pb : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0) (root : aeval pb.gen p = 0) : pb.dim ≤ p.natDegree

Full source

theorem dim_le_natDegree_of_root (pb : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0)
    (root : aeval pb.gen p = 0) : pb.dim ≤ p.natDegree := by
  refine le_of_not_lt fun hlt => ne_zero ?_
  rw [p.as_sum_range' _ hlt, Finset.sum_range]
  refine Fintype.sum_eq_zero _ fun i => ?_
  simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root
  have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
  rw [this, monomial_zero_right]

Power Basis Dimension Bounded by Minimal Polynomial Degree

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. For any nonzero polynomial $p \in A[X]$ such that $p(x) = 0$, the dimension of the power basis is less than or equal to the degree of $p$, i.e., \[ \mathrm{pb.dim} \leq \deg(p). \]

PowerBasis.dim_le_degree_of_root theorem

(h : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0) (root : aeval h.gen p = 0) : ↑h.dim ≤ p.degree

Full source

theorem dim_le_degree_of_root (h : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0)
    (root : aeval h.gen p = 0) : ↑h.dim ≤ p.degree := by
  rw [degree_eq_natDegree ne_zero]
  exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

Power Basis Dimension Bounded by Polynomial Degree

Informal description

Let $S$ be an $A$-algebra with a power basis $h$ generated by an element $x = h.\mathrm{gen}$. For any nonzero polynomial $p \in A[X]$ such that $p(x) = 0$, the dimension of the power basis is less than or equal to the degree of $p$, i.e., \[ h.\mathrm{dim} \leq \deg(p). \]

PowerBasis.degree_minpolyGen theorem

[Nontrivial A] (pb : PowerBasis A S) : degree (minpolyGen pb) = pb.dim

Full source

theorem degree_minpolyGen [Nontrivial A] (pb : PowerBasis A S) :
    degree (minpolyGen pb) = pb.dim := by
  unfold minpolyGen
  rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]
  apply degree_sum_fin_lt

Degree of Minimal Polynomial Equals Power Basis Dimension

Informal description

Let $A$ be a nontrivial commutative ring and $S$ an $A$-algebra with a power basis $\mathrm{pb}$. Then the degree of the minimal polynomial of the generator $\mathrm{pb}.\mathrm{gen}$ is equal to the dimension of the power basis, i.e., \[ \deg(\mathrm{minpolyGen}(\mathrm{pb})) = \mathrm{pb}.\mathrm{dim}. \]

PowerBasis.natDegree_minpolyGen theorem

[Nontrivial A] (pb : PowerBasis A S) : natDegree (minpolyGen pb) = pb.dim

Full source

theorem natDegree_minpolyGen [Nontrivial A] (pb : PowerBasis A S) :
    natDegree (minpolyGen pb) = pb.dim :=
  natDegree_eq_of_degree_eq_some pb.degree_minpolyGen

Natural Degree of Minimal Polynomial Equals Power Basis Dimension

Informal description

Let $A$ be a nontrivial commutative ring and $S$ an $A$-algebra with a power basis $\mathrm{pb}$. Then the degree of the minimal polynomial of the generator $\mathrm{pb}.\mathrm{gen}$ (as a natural number) is equal to the dimension of the power basis, i.e., \[ \mathrm{natDegree}(\mathrm{minpolyGen}(\mathrm{pb})) = \mathrm{pb}.\mathrm{dim}. \]

PowerBasis.minpolyGen_eq theorem

(pb : PowerBasis A S) : pb.minpolyGen = minpoly A pb.gen

Full source

@[simp]
theorem minpolyGen_eq (pb : PowerBasis A S) : pb.minpolyGen = minpoly A pb.gen := by
  nontriviality A
  refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
    or_iff_not_imp_left.2 fun hn0 h0 => ?_
  exact (pb.dim_le_degree_of_root hn0 h0).not_lt (pb.degree_minpolyGen ▸ hq)

Equality of Power Basis Minimal Polynomial and Generator's Minimal Polynomial

Informal description

For any power basis $\mathrm{pb}$ of an $A$-algebra $S$, the minimal polynomial $\mathrm{pb}.\mathrm{minpolyGen}$ of the generator $\mathrm{pb}.\mathrm{gen}$ is equal to the minimal polynomial $\mathrm{minpoly}_A(\mathrm{pb}.\mathrm{gen})$ of $\mathrm{pb}.\mathrm{gen}$ over $A$.

PowerBasis.isIntegral_gen theorem

(pb : PowerBasis A S) : IsIntegral A pb.gen

Full source

theorem isIntegral_gen (pb : PowerBasis A S) : IsIntegral A pb.gen :=
  ⟨minpolyGen pb, minpolyGen_monic pb, aeval_minpolyGen pb⟩

Integrality of Power Basis Generator

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$. Then the generator $\mathrm{pb}.\mathrm{gen}$ of the power basis is integral over $A$, i.e., there exists a monic polynomial $p \in A[X]$ such that $p(\mathrm{pb}.\mathrm{gen}) = 0$.

PowerBasis.natDegree_minpoly theorem

[Nontrivial A] (pb : PowerBasis A S) : (minpoly A pb.gen).natDegree = pb.dim

Full source

@[simp]
theorem natDegree_minpoly [Nontrivial A] (pb : PowerBasis A S) :
    (minpoly A pb.gen).natDegree = pb.dim := by rw [← minpolyGen_eq, natDegree_minpolyGen]

Degree of Minimal Polynomial Equals Power Basis Dimension

Informal description

Let $A$ be a nontrivial commutative ring and $S$ an $A$-algebra with a power basis $\mathrm{pb}$. Then the degree of the minimal polynomial of the generator $\mathrm{pb.gen}$ over $A$ is equal to the dimension of the power basis, i.e., \[ \deg(\mathrm{minpoly}_A(\mathrm{pb.gen})) = \mathrm{pb.dim}. \]

PowerBasis.leftMulMatrix theorem

 (pb : PowerBasis A S) :
  Algebra.leftMulMatrix pb.basis pb.gen =
    @Matrix.of (Fin pb.dim) (Fin pb.dim) _ fun i j =>
      if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0

Full source

protected theorem leftMulMatrix (pb : PowerBasis A S) : Algebra.leftMulMatrix pb.basis pb.gen =
    @Matrix.of (Fin pb.dim) (Fin pb.dim) _ fun i j =>
      if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0 := by
  cases subsingleton_or_nontrivial A; · subsingleton
  rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]
  refine pb.basis.ext fun k => ?_
  simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]
  apply (pow_succ' _ _).symm.trans
  split_ifs with h
  · simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]
    convert pb.aeval_minpolyGen
    rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]
  · rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
    · rfl
    intro x hx
    rw [if_neg, zero_smul]
    apply mt Fin.ext hx

Matrix Representation of Left Multiplication in a Power Basis

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$ and dimension $n = \mathrm{pb.dim}$. Then the matrix representation of the left multiplication map $y \mapsto x \cdot y$ with respect to the basis $\{1, x, \ldots, x^{n-1}\}$ is given by the $n \times n$ matrix $M$ defined as: \[ M_{i,j} = \begin{cases} -\mathrm{minpolyGen}(\mathrm{pb}).\mathrm{coeff}(i) & \text{if } j + 1 = n, \\ 1 & \text{if } i = j + 1, \\ 0 & \text{otherwise}, \end{cases} \] where $i, j \in \{0, \ldots, n-1\}$ and $\mathrm{minpolyGen}(\mathrm{pb})$ is the minimal polynomial of $x$.

PowerBasis.constr_pow_aeval theorem

 (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (f : A[X]) :
  pb.basis.constr A (fun i => y ^ (i : ℕ)) (aeval pb.gen f) = aeval y f

Full source

theorem constr_pow_aeval (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0)
    (f : A[X]) : pb.basis.constr A (fun i => y ^ (i : ℕ)) (aeval pb.gen f) = aeval y f := by
  cases subsingleton_or_nontrivial A
  · rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]
  rw [← aeval_modByMonic_eq_self_of_root (minpoly.monic pb.isIntegral_gen) (minpoly.aeval _ _), ←
    @aeval_modByMonic_eq_self_of_root _ _ _ _ _ f _ (minpoly.monic pb.isIntegral_gen) y hy]
  by_cases hf : f %ₘ minpoly A pb.gen = 0
  · simp only [hf, map_zero]
  have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim := by
    rw [← pb.natDegree_minpoly]
    apply natDegree_lt_natDegree hf
    exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
  rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]
  refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_
  rw [Finset.mem_range] at hi
  rw [LinearMap.map_smul]
  congr
  rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]

Evaluation of Polynomials via Power Basis Construction: $\mathrm{constr}_{\mathrm{pb.basis}}^A (\lambda i, y^i) (\mathrm{aeval}_x(f)) = \mathrm{aeval}_y(f)$

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. For any element $y$ in an $A$-algebra $S'$ satisfying $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$ and any polynomial $f \in A[X]$, the linear map constructed from the basis $\mathrm{pb.basis}$ and the function $i \mapsto y^i$ satisfies \[ \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) \left( \mathrm{aeval}_x(f) \right) = \mathrm{aeval}_y(f). \]

PowerBasis.constr_pow_gen theorem

 (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) :
  pb.basis.constr A (fun i => y ^ (i : ℕ)) pb.gen = y

Full source

theorem constr_pow_gen (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) :
    pb.basis.constr A (fun i => y ^ (i : ℕ)) pb.gen = y := by
  convert pb.constr_pow_aeval hy X <;> rw [aeval_X]

Power Basis Construction Maps Generator to Given Element

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. For any element $y$ in an $A$-algebra $S'$ satisfying $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$, the linear map constructed from the basis $\mathrm{pb.basis}$ and the function $i \mapsto y^i$ maps the generator $x$ to $y$, i.e., \[ \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) (x) = y. \]

PowerBasis.constr_pow_algebraMap theorem

 (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (x : A) :
  pb.basis.constr A (fun i => y ^ (i : ℕ)) (algebraMap A S x) = algebraMap A S' x

Full source

theorem constr_pow_algebraMap (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0)
    (x : A) : pb.basis.constr A (fun i => y ^ (i : ℕ)) (algebraMap A S x) = algebraMap A S' x := by
  convert pb.constr_pow_aeval hy (C x) <;> rw [aeval_C]

Power Basis Construction Preserves Algebra Map: $\mathrm{constr}_{\mathrm{pb.basis}}^A (\lambda i, y^i) \circ \mathrm{algebraMap}_A^S = \mathrm{algebraMap}_A^{S'}$

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. For any element $y$ in an $A$-algebra $S'$ satisfying $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$ and any element $x \in A$, the linear map constructed from the basis $\mathrm{pb.basis}$ and the function $i \mapsto y^i$ satisfies \[ \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) \left( \mathrm{algebraMap}_A^S(x) \right) = \mathrm{algebraMap}_A^{S'}(x). \]

PowerBasis.constr_pow_mul theorem

 (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (x x' : S) :
  pb.basis.constr A (fun i => y ^ (i : ℕ)) (x * x') =
    pb.basis.constr A (fun i => y ^ (i : ℕ)) x * pb.basis.constr A (fun i => y ^ (i : ℕ)) x'

Full source

theorem constr_pow_mul (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0)
    (x x' : S) : pb.basis.constr A (fun i => y ^ (i : ℕ)) (x * x') =
      pb.basis.constr A (fun i => y ^ (i : ℕ)) x * pb.basis.constr A (fun i => y ^ (i : ℕ)) x' := by
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
  simp only [← aeval_mul, pb.constr_pow_aeval hy]

Multiplicativity of Power Basis Construction: $\mathrm{constr}_{\mathrm{pb.basis}}^A (\lambda i, y^i)$ Preserves Products

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. For any element $y$ in an $A$-algebra $S'$ satisfying $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$ and any elements $x, x' \in S$, the linear map constructed from the basis $\mathrm{pb.basis}$ and the function $i \mapsto y^i$ satisfies \[ \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) (x \cdot x') = \left( \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) x \right) \cdot \left( \mathrm{pb.basis.constr}_A \left( \lambda i, y^i \right) x' \right). \]

PowerBasis.lift definition

(pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) : S →ₐ[A] S'

Full source

/-- `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.
-/
noncomputable def lift (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) :
    S →ₐ[A] S' :=
  { pb.basis.constr A fun i => y ^ (i : ℕ) with
    map_one' := by convert pb.constr_pow_algebraMap hy 1 using 2 <;> rw [RingHom.map_one]
    map_zero' := by convert pb.constr_pow_algebraMap hy 0 using 2 <;> rw [RingHom.map_zero]
    map_mul' := pb.constr_pow_mul hy
    commutes' := pb.constr_pow_algebraMap hy }

Lift of a power basis homomorphism

Informal description

Given a power basis `pb` for an `A`-algebra `S` with generator `x = pb.gen`, and an element `y` in another `A`-algebra `S'` satisfying `aeval y (minpoly A x) = 0`, the function `pb.lift y hy` is the unique `A`-algebra homomorphism from `S` to `S'` that maps `x` to `y`. More precisely, this homomorphism is constructed by extending the linear map defined on the basis `1, x, x², ..., x^{n-1}` of `S` (as an `A`-module) by sending each basis element `x^i` to `y^i`, and then verifying that this map preserves the multiplicative and additive structure of `S`.

PowerBasis.lift_gen theorem

(pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) : pb.lift y hy pb.gen = y

Full source

@[simp]
theorem lift_gen (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) :
    pb.lift y hy pb.gen = y :=
  pb.constr_pow_gen hy

Power Basis Lift Maps Generator to Target Element

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. Given an element $y$ in another $A$-algebra $S'$ satisfying $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$, the $A$-algebra homomorphism $\mathrm{pb.lift}\, y\, hy$ maps the generator $x$ to $y$, i.e., \[ \mathrm{pb.lift}\, y\, hy (x) = y. \]

PowerBasis.lift_aeval theorem

 (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) (f : A[X]) :
  pb.lift y hy (aeval pb.gen f) = aeval y f

Full source

@[simp]
theorem lift_aeval (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) (f : A[X]) :
    pb.lift y hy (aeval pb.gen f) = aeval y f :=
  pb.constr_pow_aeval hy f

Evaluation of Polynomials via Power Basis Lift: $\mathrm{lift}(y)(\mathrm{aeval}_x(f)) = \mathrm{aeval}_y(f)$

Informal description

Let $S$ be an $A$-algebra with a power basis $\mathrm{pb}$ generated by an element $x = \mathrm{pb.gen}$. Given an element $y$ in an $A$-algebra $S'$ such that $\mathrm{aeval}_y(\mathrm{minpoly}_A(x)) = 0$ and any polynomial $f \in A[X]$, the homomorphism $\mathrm{pb.lift}\, y\, hy$ satisfies \[ \mathrm{pb.lift}\, y\, hy \left( \mathrm{aeval}_x(f) \right) = \mathrm{aeval}_y(f). \]

PowerBasis.liftEquiv definition

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

Full source

/-- `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.
-/
@[simps]
noncomputable def liftEquiv (pb : PowerBasis A S) :
    (S →ₐ[A] S') ≃ { y : S' // aeval y (minpoly A pb.gen) = 0 } where
  toFun f := ⟨f pb.gen, by rw [aeval_algHom_apply, minpoly.aeval, map_zero]⟩
  invFun y := pb.lift y y.2
  left_inv _ := pb.algHom_ext <| lift_gen _ _ _
  right_inv y := Subtype.ext <| lift_gen _ _ y.prop

Equivalence between algebra homomorphisms and roots of the minimal polynomial

Informal description

Given a power basis `pb` for an `A`-algebra `S`, there is a bijection between `A`-algebra homomorphisms from `S` to another `A`-algebra `S'` and elements $y \in S'$ that are roots of the minimal polynomial of the generator `pb.gen` of the power basis. More precisely, the equivalence maps: 1. Any algebra homomorphism $f : S \to S'$ to the element $f(\text{pb.gen}) \in S'$, which satisfies $\text{aeval}\, (f(\text{pb.gen}))\, (\text{minpoly}_A\, \text{pb.gen}) = 0$. 2. Any root $y \in S'$ of $\text{minpoly}_A\, \text{pb.gen}$ back to the unique algebra homomorphism $S \to S'$ sending $\text{pb.gen}$ to $y$ (as constructed by `pb.lift`).

PowerBasis.liftEquiv' definition

[IsDomain B] (pb : PowerBasis A S) : (S →ₐ[A] B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B }

Full source

/-- `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. -/
@[simps! -fullyApplied]
noncomputable def liftEquiv' [IsDomain B] (pb : PowerBasis A S) :
    (S →ₐ[A] B) ≃ { y : B // y ∈ (minpoly A pb.gen).aroots B } :=
  pb.liftEquiv.trans ((Equiv.refl _).subtypeEquiv fun x => by
    rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
    · simp
    · exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen))

Equivalence between algebra homomorphisms and roots in an integral domain

Informal description

Given a power basis `pb` for an `A`-algebra `S` and an integral domain `B`, there is a bijection between `A`-algebra homomorphisms from `S` to `B` and the roots in `B` of the minimal polynomial of the generator `pb.gen`. More precisely, the equivalence maps: 1. Any algebra homomorphism $f : S \to B$ to the element $f(\text{pb.gen}) \in B$, which is a root of $\text{minpoly}_A\, \text{pb.gen}$ in $B$. 2. Any root $y \in B$ of $\text{minpoly}_A\, \text{pb.gen}$ back to the unique algebra homomorphism $S \to B$ sending $\text{pb.gen}$ to $y$ (as constructed by `pb.lift`).

PowerBasis.AlgHom.fintype definition

[IsDomain B] (pb : PowerBasis A S) : Fintype (S →ₐ[A] B)

Full source

/-- There are finitely many algebra homomorphisms `S →ₐ[A] B` if `S` is of the form `A[x]`
and `B` is an integral domain. -/
noncomputable def AlgHom.fintype [IsDomain B] (pb : PowerBasis A S) : Fintype (S →ₐ[A] B) :=
  letI := Classical.decEq B
  Fintype.ofEquiv _ pb.liftEquiv'.symm

Finiteness of algebra homomorphisms from a power basis to an integral domain

Informal description

Given a power basis `pb` for an `A`-algebra `S` and an integral domain `B`, the set of `A`-algebra homomorphisms from `S` to `B` is finite. More precisely, this finiteness result follows from the bijection between such homomorphisms and the roots in `B` of the minimal polynomial of the generator `pb.gen` (via `pb.liftEquiv'`), combined with the fact that a polynomial has finitely many roots in an integral domain.

PowerBasis.equivOfRoot definition

 (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
  (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) : S ≃ₐ[A] S'

Full source

/-- `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.
-/
@[simps! -isSimp apply]
noncomputable def equivOfRoot (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
    S ≃ₐ[A] S' :=
  AlgEquiv.ofAlgHom (pb.lift pb'.gen h₂) (pb'.lift pb.gen h₁)
    (by
      ext x
      obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x
      simp)
    (by
      ext x
      obtain ⟨f, hf, rfl⟩ := pb.exists_eq_aeval' x
      simp)

Algebra equivalence of power bases with mutually root generators

Informal description

Given two power bases `pb` and `pb'` for `A`-algebras `S` and `S'` respectively, if the generator `pb.gen` of `pb` is a root of the minimal polynomial of `pb'.gen` and vice versa, then there exists an algebra equivalence `S ≃ₐ[A] S'` that maps `pb.gen` to `pb'.gen`. More precisely, this equivalence is constructed by composing the algebra homomorphisms `pb.lift pb'.gen` and `pb'.lift pb.gen`, which are well-defined due to the root conditions `h₁` and `h₂`.

PowerBasis.equivOfRoot_aeval theorem

 (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
  (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) (f : A[X]) : pb.equivOfRoot pb' h₁ h₂ (aeval pb.gen f) = aeval pb'.gen f

Full source

@[simp]
theorem equivOfRoot_aeval (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0)
    (f : A[X]) : pb.equivOfRoot pb' h₁ h₂ (aeval pb.gen f) = aeval pb'.gen f :=
  pb.lift_aeval _ h₂ _

Polynomial Evaluation under Power Basis Equivalence: $\mathrm{equivOfRoot}(\mathrm{aeval}_x(f)) = \mathrm{aeval}_{x'}(f)$

Informal description

Let $S$ and $S'$ be $A$-algebras with power bases $\mathrm{pb}$ and $\mathrm{pb'}$ generated by elements $x = \mathrm{pb.gen}$ and $x' = \mathrm{pb'.gen}$ respectively. Suppose $x$ is a root of the minimal polynomial of $x'$ over $A$ and vice versa. Then for any polynomial $f \in A[X]$, the algebra equivalence $\mathrm{pb.equivOfRoot\, pb'\, h_1\, h_2}$ satisfies \[ \mathrm{pb.equivOfRoot\, pb'\, h_1\, h_2} \left( \mathrm{aeval}_x(f) \right) = \mathrm{aeval}_{x'}(f). \]

PowerBasis.equivOfRoot_gen theorem

 (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
  (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) : pb.equivOfRoot pb' h₁ h₂ pb.gen = pb'.gen

Full source

@[simp]
theorem equivOfRoot_gen (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
    pb.equivOfRoot pb' h₁ h₂ pb.gen = pb'.gen :=
  pb.lift_gen _ h₂

Power basis equivalence maps generator to generator

Informal description

Let $S$ and $S'$ be $A$-algebras with power bases $\mathrm{pb}$ and $\mathrm{pb}'$ generated by elements $x = \mathrm{pb.gen}$ and $y = \mathrm{pb}'.gen$ respectively. If $x$ is a root of the minimal polynomial of $y$ over $A$ and $y$ is a root of the minimal polynomial of $x$ over $A$, then the algebra equivalence $\mathrm{pb.equivOfRoot}\, \mathrm{pb}'\, h_1\, h_2$ maps the generator $x$ to $y$, i.e., \[ \mathrm{pb.equivOfRoot}\, \mathrm{pb}'\, h_1\, h_2 (x) = y. \]

PowerBasis.equivOfRoot_symm theorem

 (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
  (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) : (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁

Full source

@[simp]
theorem equivOfRoot_symm (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0) (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) :
    (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁ :=
  rfl

Symmetry of Algebra Equivalence for Power Bases with Mutually Root Generators

Informal description

Let $A$ be a commutative ring, and let $S$ and $S'$ be $A$-algebras with power bases $\mathrm{pb}$ and $\mathrm{pb}'$ respectively. Suppose that the generator $\mathrm{pb}.\mathrm{gen}$ of $\mathrm{pb}$ is a root of the minimal polynomial of $\mathrm{pb}'.\mathrm{gen}$ over $A$, and vice versa. Then the algebra equivalence $S \simeq_A S'$ induced by these conditions has its inverse equal to the algebra equivalence $S' \simeq_A S$ obtained by swapping the roles of $\mathrm{pb}$ and $\mathrm{pb}'$.

PowerBasis.equivOfMinpoly definition

(pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) : S ≃ₐ[A] S'

Full source

/-- `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.
-/
@[simps! -isSimp apply]
noncomputable def equivOfMinpoly (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h : minpoly A pb.gen = minpoly A pb'.gen) : S ≃ₐ[A] S' :=
  pb.equivOfRoot pb' (h ▸ minpoly.aeval _ _) (h.symm ▸ minpoly.aeval _ _)

Algebra equivalence of power bases with identical minimal polynomials

Informal description

Given two power bases `pb` and `pb'` for `A`-algebras `S` and `S'` respectively, if the minimal polynomials of their generators `pb.gen` and `pb'.gen` over `A` are equal, then there exists an algebra equivalence `S ≃ₐ[A] S'` between the two algebras.

PowerBasis.equivOfMinpoly_aeval theorem

 (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : A[X]) :
  pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f

Full source

@[simp]
theorem equivOfMinpoly_aeval (pb : PowerBasis A S) (pb' : PowerBasis A S')
    (h : minpoly A pb.gen = minpoly A pb'.gen) (f : A[X]) :
    pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f :=
  pb.equivOfRoot_aeval pb' _ _ _

Polynomial Evaluation under Power Basis Equivalence with Identical Minimal Polynomials

Informal description

Let $S$ and $S'$ be $A$-algebras with power bases $\mathrm{pb}$ and $\mathrm{pb'}$ respectively, where the generators $\mathrm{pb.gen}$ and $\mathrm{pb'.gen}$ have the same minimal polynomial over $A$. Then for any polynomial $f \in A[X]$, the algebra equivalence $\mathrm{pb.equivOfMinpoly\, pb'\, h}$ satisfies \[ \mathrm{pb.equivOfMinpoly\, pb'\, h} \left( \mathrm{aeval}_{\mathrm{pb.gen}}(f) \right) = \mathrm{aeval}_{\mathrm{pb'.gen}}(f). \]

PowerBasis.equivOfMinpoly_gen theorem

 (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

Full source

@[simp]
theorem equivOfMinpoly_gen (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 :=
  pb.equivOfRoot_gen pb' _ _

Power Basis Equivalence Maps Generator to Generator When Minimal Polynomials Coincide

Informal description

Let $A$ be a commutative ring and let $S$ and $S'$ be $A$-algebras with power bases $\mathrm{pb}$ and $\mathrm{pb}'$ generated by elements $x = \mathrm{pb.gen}$ and $y = \mathrm{pb}'.gen$ respectively. If the minimal polynomials of $x$ and $y$ over $A$ are equal, then the algebra equivalence $\mathrm{pb.equivOfMinpoly}\, \mathrm{pb}'\, h$ maps the generator $x$ to $y$, i.e., \[ \mathrm{pb.equivOfMinpoly}\, \mathrm{pb}'\, h (x) = y. \]

PowerBasis.equivOfMinpoly_symm theorem

 (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 h.symm

Full source

@[simp]
theorem equivOfMinpoly_symm (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 h.symm :=
  rfl

Inverse of Power Basis Algebra Equivalence with Identical Minimal Polynomials

Informal description

Let $A$ be a commutative ring, and let $S$ and $S'$ be $A$-algebras with power bases $\text{pb}$ and $\text{pb}'$ respectively. If the minimal polynomials of the generators $\text{pb.gen}$ and $\text{pb}'.gen$ over $A$ are equal, then the inverse of the algebra equivalence $\text{pb.equivOfMinpoly}\ \text{pb}'\ h$ is equal to the algebra equivalence $\text{pb}'.equivOfMinpoly\ \text{pb}\ h^{-1}$.

linearIndependent_pow theorem

[Algebra K S] (x : S) : LinearIndependent K fun i : Fin (minpoly K x).natDegree => x ^ (i : ℕ)

Full source

/-- 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 linearIndependent_pow [Algebra K S] (x : S) :
    LinearIndependent K fun i : Fin (minpoly K x).natDegree => x ^ (i : ℕ) := by
  by_cases h : IsIntegral K x; swap
  · rw [minpoly.eq_zero h, natDegree_zero]
    exact linearIndependent_empty_type
  refine Fintype.linearIndependent_iff.2 fun g hg i => ?_
  simp only at hg
  simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg
  apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_lt).mtr
  · simp_rw [← C_mul_X_pow_eq_monomial]
    exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
  · apply_fun lcoeff K i at h0
    simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0
    exact (if_pos <| Finset.mem_univ _).symm.trans h0

Linear Independence of Powers Below Minimal Polynomial Degree

Informal description

Let $K$ be a field and $S$ be a $K$-algebra. For any element $x \in S$ that is integral over $K$, the set of powers $\{x^i \mid 0 \leq i < \text{deg}(p)\}$ is linearly independent over $K$, where $p$ is the minimal polynomial of $x$ over $K$.

IsIntegral.mem_span_pow theorem

 [Nontrivial R] {x y : S} (hx : IsIntegral R x) (hy : ∃ f : R[X], y = aeval x f) :
  y ∈ Submodule.span R (Set.range fun i : Fin (minpoly R x).natDegree => x ^ (i : ℕ))

Full source

theorem IsIntegral.mem_span_pow [Nontrivial R] {x y : S} (hx : IsIntegral R x)
    (hy : ∃ f : R[X], y = aeval x f) :
    y ∈ Submodule.span R (Set.range fun i : Fin (minpoly R x).natDegree => x ^ (i : ℕ)) := by
  obtain ⟨f, rfl⟩ := hy
  apply mem_span_pow'.mpr _
  have := minpoly.monic hx
  refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩
  conv_lhs => rw [← modByMonic_add_div f this]
  simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]

Integral Elements and Their Polynomial Evaluations Span Power Basis Module

Informal description

Let $R$ be a nontrivial commutative ring and $S$ an $R$-algebra. For any integral element $x \in S$ over $R$ and any element $y \in S$ that can be expressed as $y = f(x)$ for some polynomial $f \in R[X]$, we have that $y$ belongs to the $R$-submodule spanned by $\{x^i \mid 0 \leq i < \text{deg}(p)\}$, where $p$ is the minimal polynomial of $x$ over $R$.

PowerBasis.map definition

(pb : PowerBasis R S) (e : S ≃ₐ[R] S') : PowerBasis R S'

Full source

/-- `PowerBasis.map pb (e : S ≃ₐ[R] S')` is the power basis for `S'` generated by `e pb.gen`. -/
@[simps dim gen basis]
noncomputable def map (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : PowerBasis R S' where
  dim := pb.dim
  basis := pb.basis.map e.toLinearEquiv
  gen := e pb.gen
  basis_eq_pow i := by rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]

Transformation of Power Basis via Algebra Equivalence

Informal description

Given a power basis `pb` for an `R`-algebra `S` and an algebra equivalence `e : S ≃ₐ[R] S'`, the function `PowerBasis.map` constructs a new power basis for `S'` where the generator is the image of `pb.gen` under `e`. The new basis vectors are obtained by applying `e` to each vector in the original basis, and the dimension remains unchanged. Specifically, if the original basis was `1, x, x², ..., x^{n-1}`, then the new basis is `1, e(x), e(x)², ..., e(x)^{n-1}`.

PowerBasis.minpolyGen_map theorem

(pb : PowerBasis A S) (e : S ≃ₐ[A] S') : (pb.map e).minpolyGen = pb.minpolyGen

Full source

theorem minpolyGen_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') :
    (pb.map e).minpolyGen = pb.minpolyGen := by
  dsimp only [minpolyGen, map_dim]
  -- Turn `Fin (pb.map e).dim` into `Fin pb.dim`
  simp only [LinearEquiv.trans_apply, map_basis, Basis.map_repr, map_gen,
    AlgEquiv.toLinearEquiv_apply, e.toLinearEquiv_symm, map_pow,
    AlgEquiv.symm_apply_apply, sub_right_inj]

Invariance of Minimal Polynomial under Power Basis Transformation

Informal description

Let $S$ and $S'$ be $A$-algebras, and let $pb$ be a power basis of $S$ over $A$. Given an $A$-algebra equivalence $e : S \simeq_A S'$, the minimal polynomial of the generator of the transformed power basis $pb.map\ e$ is equal to the minimal polynomial of the generator of $pb$.

PowerBasis.equivOfRoot_map theorem

(pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ h₂) : pb.equivOfRoot (pb.map e) h₁ h₂ = e

Full source

@[simp]
theorem equivOfRoot_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ h₂) :
    pb.equivOfRoot (pb.map e) h₁ h₂ = e := by
  ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  simp [aeval_algEquiv]

Equality of Power Basis Equivalence and Given Algebra Isomorphism

Informal description

Let $S$ and $S'$ be $A$-algebras with a power basis $\mathrm{pb}$ for $S$ and an algebra equivalence $e : S \simeq_A S'$. If $h_1$ and $h_2$ are proofs that $\mathrm{pb.gen}$ is a root of the minimal polynomial of $(\mathrm{pb.map}\, e).\mathrm{gen}$ and vice versa, then the algebra equivalence $\mathrm{pb.equivOfRoot}\, (\mathrm{pb.map}\, e)\, h_1\, h_2$ is equal to $e$.

PowerBasis.equivOfMinpoly_map theorem

 (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

Full source

@[simp]
theorem equivOfMinpoly_map (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 :=
  pb.equivOfRoot_map _ _ _

Equality of Power Basis Equivalence and Given Algebra Isomorphism via Minimal Polynomial

Informal description

Let $S$ and $S'$ be $A$-algebras with a power basis $\mathrm{pb}$ for $S$ and an algebra equivalence $e : S \simeq_A S'$. If the minimal polynomials of $\mathrm{pb.gen}$ and $(\mathrm{pb.map}\, e).\mathrm{gen}$ over $A$ are equal, then the algebra equivalence $\mathrm{pb.equivOfMinpoly}\, (\mathrm{pb.map}\, e)\, h$ is equal to $e$.

PowerBasis.adjoin_gen_eq_top theorem

(B : PowerBasis R S) : adjoin R ({ B.gen } : Set S) = ⊤

Full source

theorem adjoin_gen_eq_top (B : PowerBasis R S) : adjoin R ({B.gen} : Set S) = ⊤ := by
  rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]
  rintro x ⟨i, rfl⟩
  rw [B.basis_eq_pow i]
  exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Adjoining Generator of Power Basis Yields Entire Algebra

Informal description

For any power basis $B$ of the $R$-algebra $S$, the algebra generated by $R$ and the element $B.\text{gen}$ is equal to the entire algebra $S$. In other words, $\text{adjoin}_R(\{B.\text{gen}\}) = S$.

PowerBasis.adjoin_eq_top_of_gen_mem_adjoin theorem

{B : PowerBasis R S} {x : S} (hx : B.gen ∈ adjoin R ({ x } : Set S)) : adjoin R ({ x } : Set S) = ⊤

Full source

theorem adjoin_eq_top_of_gen_mem_adjoin {B : PowerBasis R S} {x : S}
    (hx : B.gen ∈ adjoin R ({x} : Set S)) : adjoin R ({x} : Set S) = ⊤ := by
  rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]
  refine adjoin_le ?_
  simp [hx]

Generator in Adjoined Element Implies Full Adjoin

Informal description

Let $B$ be a power basis of the $R$-algebra $S$, and let $x \in S$ be an element such that the generator $B.\text{gen}$ of the power basis lies in the algebra generated by $R$ and $x$. Then the algebra generated by $R$ and $x$ is equal to the entire algebra $S$, i.e., $\text{adjoin}_R(\{x\}) = S$.

Mathlib.RingTheory.PowerBasis

Definitions

Implementation notes

Tags