Mathlib.FieldTheory.Minpoly.Field

minpoly.degree_le_of_ne_zero theorem

{p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x p = 0) : degree (minpoly A x) ≤ degree p

Full source

/-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
degree of the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.degree_le_of_ne_zero`
which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`. -/
theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x p = 0) :
    degree (minpoly A x) ≤ degree p :=
  calc
    degree (minpoly A x) ≤ degree (p * C (leadingCoeff p)⁻¹) :=
      min A x (monic_mul_leadingCoeff_inv pnz) (by simp [hp])
    _ = degree p := degree_mul_leadingCoeff_inv p pnz

Degree Comparison Between Minimal Polynomial and Any Nonzero Annihilating Polynomial

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For any element $x \in B$ and any nonzero polynomial $p \in A[X]$, if $x$ is a root of $p$ (i.e., $\text{aeval}_x(p) = 0$), then the degree of the minimal polynomial of $x$ over $A$ is less than or equal to the degree of $p$.

minpoly.ne_zero_of_finite theorem

(e : B) [FiniteDimensional A B] : minpoly A e ≠ 0

Full source

theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpolyminpoly A e ≠ 0 :=
  minpoly.ne_zero <| .of_finite A _

Nonzero Minimal Polynomial in Finite-Dimensional Algebras

Informal description

Let $A$ be a field and $B$ be a finite-dimensional $A$-algebra. For any element $e \in B$, the minimal polynomial of $e$ over $A$ is nonzero.

minpoly.unique theorem

 {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0)
  (pmin : ∀ q : A[X], q.Monic → Polynomial.aeval x q = 0 → degree p ≤ degree q) : p = minpoly A x

Full source

/-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
is equal to the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.Minpoly.unique`
which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`. -/
theorem unique {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0)
    (pmin : ∀ q : A[X], q.Monic → Polynomial.aeval x q = 0 → degree p ≤ degree q) :
    p = minpoly A x := by
  have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
  symm; apply eq_of_sub_eq_zero
  by_contra hnz
  apply degree_le_of_ne_zero A x hnz (by simp [hp]) |>.not_lt
  apply degree_sub_lt _ (minpoly.ne_zero hx)
  · rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
  · exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))

Uniqueness of Minimal Polynomial for Integral Elements

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For an element $x \in B$ integral over $A$, if $p \in A[X]$ is a monic polynomial such that: 1. $p(x) = 0$ (i.e., $x$ is a root of $p$), and 2. For any monic polynomial $q \in A[X]$ with $q(x) = 0$, the degree of $p$ is less than or equal to the degree of $q$, then $p$ is equal to the minimal polynomial of $x$ over $A$.

minpoly.dvd theorem

{p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p

Full source

/-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
See also `minpoly.isIntegrallyClosed_dvd` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`. -/
theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpolyminpoly A x ∣ p := by
  by_cases hp0 : p = 0
  · simp only [hp0, dvd_zero]
  have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩
  rw [← modByMonic_eq_zero_iff_dvd (monic hx)]
  by_contra hnz
  apply degree_le_of_ne_zero A x hnz
    ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp) |>.not_lt
  exact degree_modByMonic_lt _ (monic hx)

Minimal polynomial divides any annihilating polynomial

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$ and any polynomial $p \in A[X]$, if $x$ is a root of $p$ (i.e., $p(x) = 0$), then the minimal polynomial of $x$ over $A$ divides $p$.

minpoly.dvd_iff theorem

{p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0

Full source

lemma dvd_iff {p : A[X]} : minpolyminpoly A x ∣ pminpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
  ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩

Minimal polynomial divides polynomial iff polynomial vanishes at $x$

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For an element $x \in B$ integral over $A$ and any polynomial $p \in A[X]$, the minimal polynomial of $x$ over $A$ divides $p$ if and only if $x$ is a root of $p$ (i.e., the evaluation of $p$ at $x$ is zero).

minpoly.isRadical theorem

[IsReduced B] : IsRadical (minpoly A x)

Full source

theorem isRadical [IsReduced B] : IsRadical (minpoly A x) := fun n p dvd ↦ by
  rw [dvd_iff] at dvd ⊢; rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩

Minimal Polynomial is Radical in Reduced Algebras

Informal description

Let $A$ be a field and $B$ an $A$-algebra that is reduced (i.e., has no nonzero nilpotent elements). For any element $x \in B$ integral over $A$, the minimal polynomial of $x$ over $A$ is a radical element in the polynomial ring $A[X]$. That is, for any polynomial $p \in A[X]$, if the minimal polynomial divides $p^n$ for some $n \in \mathbb{N}$, then it divides $p$.

minpoly.dvd_map_of_isScalarTower theorem

 (A K : Type*) {R : Type*} [CommRing A] [Field K] [Ring R] [Algebra A K] [Algebra A R] [Algebra K R]
  [IsScalarTower A K R] (x : R) : minpoly K x ∣ (minpoly A x).map (algebraMap A K)

Full source

theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [Ring R]
    [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
    minpolyminpoly K x ∣ (minpoly A x).map (algebraMap A K) := by
  refine minpoly.dvd K x ?_
  rw [aeval_map_algebraMap, minpoly.aeval]

Minimal polynomial divisibility in scalar tower extension

Informal description

Let $A$ be a commutative ring, $K$ a field, and $R$ a ring, with $A$-algebra structures on $K$ and $R$, and a $K$-algebra structure on $R$ forming a scalar tower $A \to K \to R$. For any element $x \in R$, the minimal polynomial of $x$ over $K$ divides the image of the minimal polynomial of $x$ over $A$ under the algebra map from $A$ to $K$.

minpoly.dvd_map_of_isScalarTower' theorem

 (R : Type*) {S : Type*} (K L : Type*) [CommRing R] [CommRing S] [Field K] [Ring L] [Algebra R S] [Algebra R K]
  [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) :
  minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (minpoly R s)

Full source

theorem dvd_map_of_isScalarTower' (R : Type*) {S : Type*} (K L : Type*) [CommRing R]
    [CommRing S] [Field K] [Ring L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L]
    [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) :
    minpolyminpoly K (algebraMap S L s) ∣ map (algebraMap R K) (minpoly R s) := by
  apply minpoly.dvd K (algebraMap S L s)
  rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
  rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

Minimal Polynomial Divisibility in Scalar Tower Context

Informal description

Let $R$ be a commutative ring, $S$ a commutative ring, $K$ a field, and $L$ a ring. Suppose we have the following algebra structures: - An $R$-algebra structure on $S$, - An $R$-algebra structure on $K$, - An $S$-algebra structure on $L$, - A $K$-algebra structure on $L$, - An $R$-algebra structure on $L$, such that the scalar tower conditions $R \to K \to L$ and $R \to S \to L$ hold. Then for any element $s \in S$, the minimal polynomial of $s$ over $K$ (when mapped to $L$ via the algebra map $S \to L$) divides the image of the minimal polynomial of $s$ over $R$ under the algebra map $R \to K$.

minpoly.aeval_of_isScalarTower theorem

 (R : Type*) {K T U : Type*} [CommRing R] [Field K] [CommRing T] [Algebra R K] [Algebra K T] [Algebra R T]
  [IsScalarTower R K T] [CommSemiring U] [Algebra K U] [Algebra R U] [IsScalarTower R K U] (x : T) (y : U)
  (hy : Polynomial.aeval y (minpoly K x) = 0) : Polynomial.aeval y (minpoly R x) = 0

Full source

/-- If `y` is a conjugate of `x` over a field `K`, then it is a conjugate over a subring `R`. -/
theorem aeval_of_isScalarTower (R : Type*) {K T U : Type*} [CommRing R] [Field K] [CommRing T]
    [Algebra R K] [Algebra K T] [Algebra R T] [IsScalarTower R K T] [CommSemiring U] [Algebra K U]
    [Algebra R U] [IsScalarTower R K U] (x : T) (y : U)
    (hy : Polynomial.aeval y (minpoly K x) = 0) : Polynomial.aeval y (minpoly R x) = 0 :=
  aeval_map_algebraMap K y (minpoly R x) ▸
    eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (algebraMap K U) y
      (minpoly.dvd_map_of_isScalarTower R K x) hy

Roots of Minimal Polynomials in Scalar Tower Extensions

Informal description

Let $R$ be a commutative ring, $K$ a field, $T$ a commutative ring, and $U$ a commutative semiring. Suppose we have algebra structures: - $R$-algebra on $K$, - $K$-algebra on $T$, - $R$-algebra on $T$ forming a scalar tower $R \to K \to T$, - $K$-algebra on $U$, - $R$-algebra on $U$ forming a scalar tower $R \to K \to U$. For any $x \in T$ and $y \in U$, if $y$ is a root of the minimal polynomial of $x$ over $K$ (i.e., $\text{aeval}_y(\text{minpoly}_K x) = 0$), then $y$ is also a root of the minimal polynomial of $x$ over $R$ (i.e., $\text{aeval}_y(\text{minpoly}_R x) = 0$).

minpoly.map_algebraMap theorem

 {F E A : Type*} [Field F] [Field E] [CommRing A] [Algebra F E] [Algebra E A] [Algebra F A] [IsScalarTower F E A]
  {a : A} (ha : IsIntegral F a) (h : minpoly E a ∈ lifts (algebraMap F E)) :
  (minpoly F a).map (algebraMap F E) = minpoly E a

Full source

/-- If a subfield `F` of `E` contains all the coefficients of `minpoly E a`, then
`minpoly F a` maps to `minpoly E a` via `algebraMap F E`. -/
theorem map_algebraMap {F E A : Type*} [Field F] [Field E] [CommRing A]
    [Algebra F E] [Algebra E A] [Algebra F A] [IsScalarTower F E A]
    {a : A} (ha : IsIntegral F a) (h : minpolyminpoly E a ∈ lifts (algebraMap F E)) :
    (minpoly F a).map (algebraMap F E) = minpoly E a := by
  refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_
  obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)
  rw [natDegree_map, ← hgdeg]
  refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero
  rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]

Minimal Polynomial Compatibility under Field Extension: $\text{minpoly}_F(a) \mapsto \text{minpoly}_E(a)$ via $\text{algebraMap}_{F \to E}$

Informal description

Let $F$ be a subfield of $E$, and $A$ be a commutative ring with $E$-algebra and $F$-algebra structures such that the actions are compatible (i.e., $F \to E \to A$ forms a scalar tower). For an element $a \in A$ that is integral over $F$, if the minimal polynomial of $a$ over $E$ has all its coefficients in the image of the algebra map $F \to E$, then the image of the minimal polynomial of $a$ over $F$ under the algebra map $F \to E$ equals the minimal polynomial of $a$ over $E$. In other words, \[ (\text{minpoly}_F(a)).\text{map}(\text{algebraMap}_{F \to E}) = \text{minpoly}_E(a). \]

minpoly.ker_aeval_eq_span_minpoly theorem

: RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x

Full source

/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`. -/
@[simp]
lemma ker_aeval_eq_span_minpoly :
    RingHom.ker (Polynomial.aeval x) = A[X]A[X] ∙ minpoly A x := by
  ext p
  simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]

Kernel of Evaluation Homomorphism Equals Ideal Generated by Minimal Polynomial

Informal description

Let $A$ be a commutative ring and $x$ be an element of an $A$-algebra. The kernel of the evaluation homomorphism $\text{aeval}_x : A[X] \to B$ (where $B$ is an $A$-algebra containing $x$) is equal to the principal ideal generated by the minimal polynomial $\text{minpoly}_A(x)$ of $x$ over $A$. That is, \[ \ker(\text{aeval}_x) = ( \text{minpoly}_A(x) ). \]

minpoly.add_algebraMap theorem

 {B : Type*} [CommRing B] [Algebra A B] (x : B) (a : A) :
  minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a)

Full source

theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
    (a : A) : minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a) := by
  by_cases hx : IsIntegral A x
  · refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
    · simp [aeval_comp]
    · have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
      have H := minpoly.min A x (qmo.comp_X_add_C _) this
      rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]
      rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H
  · rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
    refine fun h ↦ hx ?_
    simpa only [add_sub_cancel_right] using IsIntegral.sub h (isIntegral_algebraMap (x := a))

Minimal polynomial of $x + \text{algebraMap}(a)$ as composition with $X - C(a)$

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any element $x \in B$ and any $a \in A$, the minimal polynomial of $x + \text{algebraMap}(a)$ over $A$ is equal to the composition of the minimal polynomial of $x$ with the polynomial $X - C(a)$, where $C$ is the constant polynomial embedding and $X$ is the indeterminate.

minpoly.sub_algebraMap theorem

 {B : Type*} [CommRing B] [Algebra A B] (x : B) (a : A) :
  minpoly A (x - algebraMap A B a) = (minpoly A x).comp (X + C a)

Full source

theorem sub_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
    (a : A) : minpoly A (x - algebraMap A B a) = (minpoly A x).comp (X + C a) := by
  simpa [sub_eq_add_neg] using add_algebraMap x (-a)

Minimal polynomial of $x - \text{algebraMap}(a)$ as composition with $X + C(a)$

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any element $x \in B$ and any $a \in A$, the minimal polynomial of $x - \text{algebraMap}(a)$ over $A$ is equal to the composition of the minimal polynomial of $x$ with the polynomial $X + C(a)$, where $C$ is the constant polynomial embedding and $X$ is the indeterminate.

minpoly.neg theorem

 {B : Type*} [Ring B] [Algebra A B] (x : B) :
  minpoly A (-x) = (-1) ^ (natDegree (minpoly A x)) * (minpoly A x).comp (-X)

Full source

theorem neg {B : Type*} [Ring B] [Algebra A B] (x : B) :
    minpoly A (- x) = (-1) ^ (natDegree (minpoly A x)) * (minpoly A x).comp (- X) := by
  by_cases hx : IsIntegral A x
  · refine (minpoly.unique _ _ ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X)
        ?_ fun q qmo hq => ?_).symm
    · simp [aeval_comp]
    · have : (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (- X)) = 0 := by
        simpa [aeval_comp] using hq
      have H := minpoly.min A x qmo.neg_one_pow_natDegree_mul_comp_neg_X this
      have n1 := ((minpoly.monic hx).neg_one_pow_natDegree_mul_comp_neg_X).ne_zero
      have n2 := qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero
      rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree n1, natDegree_mul (by simp) (right_ne_zero_of_mul n1), natDegree_comp]
      rw [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree qmo.neg_one_pow_natDegree_mul_comp_neg_X.ne_zero,
        natDegree_mul (by simp) (right_ne_zero_of_mul n2), natDegree_comp] at H
      simpa using H
  · rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
    · simp only [natDegree_zero, pow_zero, mul_zero]
    · exact IsIntegral.neg_iff.not.mpr hx

Minimal polynomial of $-x$ in terms of minimal polynomial of $x$

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For any element $x \in B$ integral over $A$, the minimal polynomial of $-x$ over $A$ is given by $$ \text{minpoly}_A(-x) = (-1)^{\deg p} \cdot p(-X) $$ where $p = \text{minpoly}_A(x)$ is the minimal polynomial of $x$ over $A$ and $\deg p$ denotes its degree.

minpoly.Fintype.subtypeProd definition

 {E : Type*} {X : Set E} (hX : X.Finite) {L : Type*} (F : E → Multiset L) : Fintype (∀ x : X, { l : L // l ∈ F x })

Full source

/-- A technical finiteness result. -/
noncomputable def Fintype.subtypeProd {E : Type*} {X : Set E} (hX : X.Finite) {L : Type*}
    (F : E → Multiset L) : Fintype (∀ x : X, { l : L // l ∈ F x }) :=
  @Pi.instFintype _ _ _ (Finite.fintype hX) _

Finiteness of dependent functions over finite sets with multiset constraints

Informal description

Given a finite set $X$ in a type $E$ and a family of multisets $(F_x)_{x \in X}$ over a type $L$, the dependent function type $\forall x \in X, \{ l \in L \mid l \in F_x \}$ is finite. This means that the collection of functions assigning to each $x \in X$ an element $l$ from the multiset $F_x$ forms a finite type.

minpoly.rootsOfMinPolyPiType definition

(φ : E →ₐ[F] K) (x : range (Module.finBasis F E : _ → E)) : { l : K // l ∈ (minpoly F x.1).aroots K }

Full source

/-- Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x -/
def rootsOfMinPolyPiType (φ : E →ₐ[F] K)
    (x : range (Module.finBasis F E : _ → E)) :
    { l : K // l ∈ (minpoly F x.1).aroots K } :=
  ⟨φ x, by
    rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
      ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]⟩

Roots of minimal polynomials via algebra homomorphisms

Informal description

Given a field extension $E$ of $F$ and an $F$-algebra homomorphism $\varphi: E \to K$, for each basis vector $x$ in a finite basis of $E$ over $F$, the function maps $\varphi$ to the root $\varphi(x)$ of the minimal polynomial of $x$ over $F$ in $K$. More precisely, for each $x$ in the range of a finite basis of $E$ over $F$, the value $\varphi(x)$ is a root in $K$ of the minimal polynomial of $x$ over $F$, i.e., $\varphi(x)$ satisfies $\text{minpoly}_F(x)(\varphi(x)) = 0$.

minpoly.aux_inj_roots_of_min_poly theorem

: Injective (rootsOfMinPolyPiType F E K)

Full source

theorem aux_inj_roots_of_min_poly : Injective (rootsOfMinPolyPiType F E K) := by
  intro f g h
  -- needs explicit coercion on the RHS
  suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢
  rw [funext_iff] at h
  exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
    Subtype.ext_iff.mp (h ⟨e, he⟩)

Injectivity of Algebra Homomorphisms via Minimal Polynomial Roots

Informal description

The function `rootsOfMinPolyPiType` that maps each $F$-algebra homomorphism $\varphi: E \to K$ to its values on a finite basis of $E$ over $F$ is injective. In other words, if two $F$-algebra homomorphisms $\varphi_1, \varphi_2: E \to K$ agree on all basis vectors of $E$ over $F$, then $\varphi_1 = \varphi_2$.

minpoly.AlgHom.fintype instance

: Fintype (E →ₐ[F] K)

Full source

/-- Given field extensions `E/F` and `K/F`, with `E/F` finite, there are finitely many `F`-algebra
  homomorphisms `E →ₐ[K] K`. -/
noncomputable instance AlgHom.fintype : Fintype (E →ₐ[F] K) :=
  @Fintype.ofInjective _ _
    (Fintype.subtypeProd (finite_range (Module.finBasis F E)) fun e =>
      (minpoly F e).aroots K)
    _ (aux_inj_roots_of_min_poly F E K)

Finiteness of Algebra Homomorphisms Between Finite Field Extensions

Informal description

For finite field extensions $E/F$ and $K/F$, the set of $F$-algebra homomorphisms from $E$ to $K$ is finite.

minpoly.zero theorem

: minpoly A (0 : B) = X

Full source

/-- The minimal polynomial of `0` is `X`. -/
@[simp]
theorem zero : minpoly A (0 : B) = X := by
  simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, RingHom.map_zero] using eq_X_sub_C B (0 : A)

Minimal polynomial of zero is $X$

Informal description

Let $B$ be an algebra over a field $A$. The minimal polynomial of the zero element $0 \in B$ is $X$.

minpoly.one theorem

: minpoly A (1 : B) = X - 1

Full source

/-- The minimal polynomial of `1` is `X - 1`. -/
@[simp]
theorem one : minpoly A (1 : B) = X - 1 := by
  simpa only [RingHom.map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)

Minimal polynomial of unity is $X - 1$

Informal description

Let $A$ be a field and $B$ an $A$-algebra. The minimal polynomial of the multiplicative identity $1 \in B$ over $A$ is $X - 1$.

minpoly.prime theorem

(hx : IsIntegral A x) : Prime (minpoly A x)

Full source

/-- A minimal polynomial is prime. -/
theorem prime (hx : IsIntegral A x) : Prime (minpoly A x) := by
  refine ⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩
  rintro p q ⟨d, h⟩
  have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]
  replace : Polynomial.aevalPolynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
  exact Or.imp (dvd A x) (dvd A x) this

Minimal Polynomial of an Integral Element is Prime

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, the minimal polynomial of $x$ over $A$ is a prime polynomial in $A[X]$.

minpoly.root theorem

{x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y) : algebraMap A B y = x

Full source

/-- If `L/K` is a field extension and an element `y` of `K` is a root of the minimal polynomial
of an element `x ∈ L`, then `y` maps to `x` under the field embedding. -/
theorem root {x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y) :
    algebraMap A B y = x := by
  have key : minpoly A x = X - C y := eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
    (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
      (dvd_iff_isRoot.2 h))
  have := aeval A x
  rwa [key, map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this

Minimal Polynomial Root Maps to Original Element in Field Extension

Informal description

Let $K$ be a field and $L$ a field extension of $K$. For any element $x \in L$ that is integral over $K$, if $y \in K$ is a root of the minimal polynomial of $x$ over $K$, then the image of $y$ under the canonical field embedding $K \hookrightarrow L$ equals $x$. In other words, $\text{algebraMap}_{K \to L}(y) = x$.

minpoly.coeff_zero_eq_zero theorem

(hx : IsIntegral A x) : coeff (minpoly A x) 0 = 0 ↔ x = 0

Full source

/-- The constant coefficient of the minimal polynomial of `x` is `0` if and only if `x = 0`. -/
@[simp]
theorem coeff_zero_eq_zero (hx : IsIntegral A x) : coeffcoeff (minpoly A x) 0 = 0 ↔ x = 0 := by
  constructor
  · intro h
    have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
    rw [← root hx zero_root]
    exact RingHom.map_zero _
  · rintro rfl
    simp

Minimal polynomial constant term vanishes if and only if element is zero

Informal description

Let $A$ be a field and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, the constant coefficient of the minimal polynomial of $x$ over $A$ is zero if and only if $x = 0$.

minpoly.coeff_zero_ne_zero theorem

(hx : IsIntegral A x) (h : x ≠ 0) : coeff (minpoly A x) 0 ≠ 0

Full source

/-- The minimal polynomial of a nonzero element has nonzero constant coefficient. -/
theorem coeff_zero_ne_zero (hx : IsIntegral A x) (h : x ≠ 0) : coeffcoeff (minpoly A x) 0 ≠ 0 := by
  contrapose! h
  simpa only [hx, coeff_zero_eq_zero] using h

Nonzero Elements Have Minimal Polynomials with Nonzero Constant Term

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any nonzero element $x \in B$ that is integral over $A$, the constant coefficient of its minimal polynomial over $A$ is nonzero.

minpoly_algEquiv_toLinearMap theorem

(σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) : minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1

Full source

/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) :
    minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 := by
  refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm
  · rw [map_sub]
    simp [← AlgEquiv.pow_toLinearMap, pow_orderOf_eq_one]
  · intros q hq hs
    rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]
    intro H
    rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs
    simp_rw [← AlgEquiv.pow_toLinearMap] at hs
    apply hq.ne_zero
    simpa using Fintype.linearIndependent_iff.mp
      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_algHom_injective).comp _
        (Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
      (q.coeff ∘ (↑)) hs ⟨_, H⟩

Minimal polynomial of finite-order Galois automorphism is $X^n - 1$

Informal description

Let $L/K$ be a field extension and $\sigma \colon L \to L$ be a $K$-algebra automorphism of finite order. Then the minimal polynomial of $\sigma$ (viewed as a $K$-linear map) is $X^n - 1$, where $n$ is the order of $\sigma$ in the automorphism group $\mathrm{Gal}(L/K)$.

minpoly_algHom_toLinearMap theorem

(σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) : minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1

Full source

/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
lemma minpoly_algHom_toLinearMap (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) :
    minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 := by
  have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by
    rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
    exact (AlgEquiv.algHomUnitsEquiv K L).injective
  rw [this, ← minpoly_algEquiv_toLinearMap]
  · apply congr_arg
    ext
    simp
  · rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]

Minimal polynomial of finite-order algebra homomorphism is $X^n - 1$

Informal description

Let $L/K$ be a field extension and $\sigma \colon L \to L$ be a $K$-algebra homomorphism of finite order. Then the minimal polynomial of $\sigma$ (viewed as a $K$-linear map) is $X^n - 1$, where $n$ is the order of $\sigma$.