doc-next-gen

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Module docstring

{"# Adjoining Elements to Fields

This file contains many results about adjoining elements to fields. "}

IntermediateField.mem_adjoin_range_iff theorem
{ι : Type*} (i : ι → E) (x : E) : x ∈ adjoin F (Set.range i) ↔ ∃ r s : MvPolynomial ι F, x = MvPolynomial.aeval i r / MvPolynomial.aeval i s
Full source 
theorem mem_adjoin_range_iff {ι : Type*} (i : ι → E) (x : E) :
    x ∈ adjoin F (Set.range i)x ∈ adjoin F (Set.range i) ↔ ∃ r s : MvPolynomial ι F,
      x = MvPolynomial.aeval i r / MvPolynomial.aeval i s := by
  simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]
Characterization of Elements in the Adjoint Field $F(\text{range}(i))$ via Polynomial Evaluation
Informal description
Let $E$ be a field extension of $F$, and let $i : \iota \to E$ be a family of elements in $E$. For any $x \in E$, we have $x \in F(\text{range}(i))$ if and only if there exist multivariate polynomials $r, s \in F[X_1, \dots, X_n]$ such that $x = \frac{r(i_1, \dots, i_n)}{s(i_1, \dots, i_n)}$, where $r(i_1, \dots, i_n)$ and $s(i_1, \dots, i_n)$ denote the evaluation of $r$ and $s$ at the elements $i_1, \dots, i_n \in E$.
IntermediateField.mem_adjoin_iff theorem
(x : E) : x ∈ adjoin F S ↔ ∃ r s : MvPolynomial S F, x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s
Full source 
theorem mem_adjoin_iff (x : E) :
    x ∈ adjoin F Sx ∈ adjoin F S ↔ ∃ r s : MvPolynomial S F,
      x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s := by
  rw [← mem_adjoin_range_iff, Subtype.range_coe]
Characterization of Elements in the Adjoint Field $F(S)$ via Polynomial Evaluation
Informal description
Let $E$ be a field extension of $F$ and $S \subseteq E$ a subset. For any $x \in E$, we have $x \in F(S)$ if and only if there exist multivariate polynomials $r, s \in F[X_s]_{s \in S}$ such that $x = \frac{r(s_1, \dots, s_n)}{s(s_1, \dots, s_n)}$, where $r(s_1, \dots, s_n)$ and $s(s_1, \dots, s_n)$ denote the evaluation of $r$ and $s$ at the elements $s_1, \dots, s_n \in S$.
IntermediateField.mem_adjoin_simple_iff theorem
{α : E} (x : E) : x ∈ adjoin F { α } ↔ ∃ r s : F[X], x = aeval α r / aeval α s
Full source 
theorem mem_adjoin_simple_iff {α : E} (x : E) :
    x ∈ adjoin F {α}x ∈ adjoin F {α} ↔ ∃ r s : F[X], x = aeval α r / aeval α s := by
  simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]
Characterization of Elements in $F(\alpha)$ via Rational Polynomial Evaluation
Informal description
Let $E$ be a field extension of $F$ and $\alpha \in E$. An element $x \in E$ belongs to the adjoint field $F(\alpha)$ if and only if there exist polynomials $r, s \in F[X]$ such that $x = \frac{r(\alpha)}{s(\alpha)}$, where $r(\alpha)$ and $s(\alpha)$ denote the evaluation of $r$ and $s$ at $\alpha$.
IntermediateField.finiteDimensional_sup instance
[FiniteDimensional K E1] [FiniteDimensional K E2] : FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L)
Full source 
instance finiteDimensional_sup [FiniteDimensional K E1] [FiniteDimensional K E2] :
    FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) := by
  let g := Algebra.TensorProduct.productMap E1.val E2.val
  suffices g.range = (E1 ⊔ E2).toSubalgebra by
    have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
    rwa [this] at h
  rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
Finite-Dimensionality of the Join of Intermediate Fields
Informal description
For any field extension $L$ of $K$ and any finite-dimensional intermediate fields $E_1$ and $E_2$ of $L$ over $K$, the join $E_1 \sqcup E_2$ is also finite-dimensional over $K$.
IntermediateField.rank_sup_le_of_isAlgebraic theorem
(halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) : Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K E1 * Module.rank K E2
Full source 
/-- If `E1` and `E2` are intermediate fields, and at least one them are algebraic, then the rank of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`.
Note that this result is also true without algebraic assumption,
but the proof becomes very complicated. -/
theorem rank_sup_le_of_isAlgebraic
    (halg : Algebra.IsAlgebraicAlgebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
    Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K E1 * Module.rank K E2 := by
  have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra
  rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this
Rank Inequality for Compositum of Algebraic Intermediate Fields: $\text{rank}_K(E_1 \sqcup E_2) \leq \text{rank}_K(E_1) \cdot \text{rank}_K(E_2)$
Informal description
Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If at least one of $E_1$ or $E_2$ is algebraic over $K$, then the rank of the compositum $E_1 \sqcup E_2$ over $K$ satisfies the inequality: \[ \text{rank}_K(E_1 \sqcup E_2) \leq \text{rank}_K(E_1) \cdot \text{rank}_K(E_2). \]
IntermediateField.finrank_sup_le theorem
: finrank K ↥(E1 ⊔ E2) ≤ finrank K E1 * finrank K E2
Full source 
/-- If `E1` and `E2` are intermediate fields, then the `Module.finrank` of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`. -/
theorem finrank_sup_le :
    finrank K ↥(E1 ⊔ E2) ≤ finrank K E1 * finrank K E2 := by
  by_cases h : FiniteDimensional K E1
  · have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra
    change _ ≤ finrank K E1 * finrank K E2 at this
    rwa [← sup_toSubalgebra_of_left] at this
  rw [FiniteDimensional, ← rank_lt_aleph0_iff, not_lt] at h
  have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show Subalgebra.toSubmodule E1.toSubalgebra ≤ Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra by
      simp
  rw [show finrank K E1 = 0 from Cardinal.toNat_apply_of_aleph0_le h,
    show finrank K ↥(E1 ⊔ E2) = 0 from Cardinal.toNat_apply_of_aleph0_le (h.trans this), zero_mul]
Finite Rank Bound for Compositum of Intermediate Fields: $\text{finrank}_K(E_1 \sqcup E_2) \leq \text{finrank}_K(E_1) \cdot \text{finrank}_K(E_2)$
Informal description
For any intermediate fields $E_1$ and $E_2$ between fields $K$ and $L$, the finite rank of the compositum $E_1 \sqcup E_2$ over $K$ is bounded above by the product of the finite ranks of $E_1$ and $E_2$ over $K$, i.e., \[ \text{finrank}_K(E_1 \sqcup E_2) \leq \text{finrank}_K(E_1) \cdot \text{finrank}_K(E_2). \]
IntermediateField.coe_iSup_of_directed theorem
[Nonempty ι] (dir : Directed (· ≤ ·) t) : ↑(iSup t) = ⋃ i, (t i : Set L)
Full source 
theorem coe_iSup_of_directed [Nonempty ι] (dir : Directed (· ≤ ·) t) :
    ↑(iSup t) = ⋃ i, (t i : Set L) :=
  let M : IntermediateField K L :=
    { __ := Subalgebra.copy _ _ (Subalgebra.coe_iSup_of_directed dir).symm
      inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (t i).inv_mem hi⟩ }
  have : iSup t = M := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (t i : Set L)) i) (Set.iUnion_subset fun _ ↦ le_iSup t _)
  this.symm ▸ rfl
Supremum of Directed Family of Intermediate Fields Equals Union
Informal description
Let $K$ and $L$ be fields with $K \subseteq L$, and let $\{E_i\}_{i \in \iota}$ be a nonempty directed family of intermediate fields between $K$ and $L$ (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $E_i \subseteq E_k$ and $E_j \subseteq E_k$). Then the underlying set of the supremum $\bigsqcup_{i \in \iota} E_i$ is equal to the union $\bigcup_{i \in \iota} E_i$ as subsets of $L$.
IntermediateField.toSubalgebra_iSup_of_directed theorem
(dir : Directed (· ≤ ·) t) : (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
Full source 
theorem toSubalgebra_iSup_of_directed (dir : Directed (· ≤ ·) t) :
    (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra := by
  cases isEmpty_or_nonempty ι
  · simp_rw [iSup_of_empty, bot_toSubalgebra]
  · exact SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)
Supremum of Directed Family of Intermediate Fields Preserves Subalgebra Structure
Informal description
Let $K$ and $L$ be fields with $K \subseteq L$, and let $\{E_i\}_{i \in \iota}$ be a directed family of intermediate fields between $K$ and $L$ (i.e., for any $i, j \in \iota$, there exists $k \in \iota$ such that $E_i \subseteq E_k$ and $E_j \subseteq E_k$). Then the underlying subalgebra of the supremum $\bigsqcup_{i \in \iota} E_i$ is equal to the supremum of the underlying subalgebras $\bigsqcup_{i \in \iota} (E_i).toSubalgebra$.
IntermediateField.finiteDimensional_iSup_of_finite instance
[h : Finite ι] [∀ i, FiniteDimensional K (t i)] : FiniteDimensional K (⨆ i, t i : IntermediateField K L)
Full source 
instance finiteDimensional_iSup_of_finite [h : Finite ι] [∀ i, FiniteDimensional K (t i)] :
    FiniteDimensional K (⨆ i, t i : IntermediateField K L) := by
  rw [← iSup_univ]
  induction Set.univ, Set.finite_univ (α := ι) using Set.Finite.induction_on with
  | empty =>
    rw [iSup_emptyset]
    exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional
  | insert s hs =>
    rw [iSup_insert]
    exact IntermediateField.finiteDimensional_sup _ _
Finite-Dimensionality of the Supremum of a Finite Family of Intermediate Fields
Informal description
For any field extension $L$ of $K$ and any finite family $\{E_i\}_{i \in \iota}$ of intermediate fields between $K$ and $L$, if each $E_i$ is finite-dimensional over $K$, then the supremum $\bigsqcup_{i \in \iota} E_i$ is also finite-dimensional over $K$.
IntermediateField.finiteDimensional_iSup_of_finset instance
{s : Finset ι} [∀ i, FiniteDimensional K (t i)] : FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L)
Full source 
/-- See `finiteDimensional_iSup_of_finset'` for a stronger version,
that was the one used in mathlib3. -/
instance finiteDimensional_iSup_of_finset
    {s : Finset ι} [∀ i, FiniteDimensional K (t i)] :
    FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L) :=
  iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite
Finite-Dimensionality of the Compositum of a Finite Family of Intermediate Fields
Informal description
For any field extension $L$ of $K$ and any finite set $s$ of indices, if each intermediate field $t_i$ (for $i \in s$) is finite-dimensional over $K$, then the compositum $\bigsqcup_{i \in s} t_i$ is also finite-dimensional over $K$.
IntermediateField.finiteDimensional_iSup_of_finset' theorem
{s : Finset ι} (h : ∀ i ∈ s, FiniteDimensional K (t i)) : FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L)
Full source 
theorem finiteDimensional_iSup_of_finset'
    {s : Finset ι} (h : ∀ i ∈ s, FiniteDimensional K (t i)) :
    FiniteDimensional K (⨆ i ∈ s, t i : IntermediateField K L) :=
  have := Subtype.forall'.mp h
  iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite
Finite-dimensionality of compositum of finitely many finite-dimensional intermediate fields
Informal description
Let $K$ be a field and $L$ a field extension of $K$. For any finite set $s$ of indices and any family $\{E_i\}_{i \in s}$ of intermediate fields between $K$ and $L$, if each $E_i$ is finite-dimensional over $K$, then the compositum $\bigsqcup_{i \in s} E_i$ is also finite-dimensional over $K$.
IntermediateField.isSplittingField_iSup theorem
{p : ι → K[X]} {s : Finset ι} (h0 : ∏ i ∈ s, p i ≠ 0) (h : ∀ i ∈ s, (p i).IsSplittingField K (t i)) : (∏ i ∈ s, p i).IsSplittingField K (⨆ i ∈ s, t i : IntermediateField K L)
Full source 
/-- A compositum of splitting fields is a splitting field -/
theorem isSplittingField_iSup {p : ι → K[X]}
    {s : Finset ι} (h0 : ∏ i ∈ s, p i∏ i ∈ s, p i ≠ 0) (h : ∀ i ∈ s, (p i).IsSplittingField K (t i)) :
    (∏ i ∈ s, p i).IsSplittingField K (⨆ i ∈ s, t i : IntermediateField K L) := by
  let F : IntermediateField K L := ⨆ i ∈ s, t i
  have hF : ∀ i ∈ s, t i ≤ F := fun i hi ↦ le_iSup_of_le i (le_iSup (fun _ ↦ t i) hi)
  simp only [isSplittingField_iff] at h ⊢
  refine
    ⟨splits_prod (algebraMap K F) fun i hi ↦
        splits_comp_of_splits (algebraMap K (t i)) (inclusion (hF i hi)).toRingHom
          (h i hi).1,
      ?_⟩
  simp only [rootSet_prod p s h0, ← Set.iSup_eq_iUnion, (@gc K _ L _ _).l_iSup₂]
  exact iSup_congr fun i ↦ iSup_congr fun hi ↦ (h i hi).2
Compositum of Splitting Fields is a Splitting Field for the Product Polynomial
Informal description
Let $K$ be a field and $L$ a field extension of $K$. For a finite set $s$ of indices and a family of polynomials $\{p_i\}_{i \in s}$ in $K[X]$ such that $\prod_{i \in s} p_i \neq 0$, suppose each $p_i$ has $t_i$ as a splitting field over $K$. Then the compositum $\bigsqcup_{i \in s} t_i$ is a splitting field over $K$ for the product polynomial $\prod_{i \in s} p_i$.
IntermediateField.adjoin_rank_le_of_isAlgebraic theorem
(L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) : Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L
Full source 
/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `[E(L) : E] ≤ [L : F]`. A corollary of
`Subalgebra.adjoin_rank_le` since in this case `E(L) = E[L]`. -/
theorem adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
    (halg : Algebra.IsAlgebraicAlgebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L := by
  have h : (adjoin E (L.toSubalgebra : Set K)).toSubalgebra =
      Algebra.adjoin E (L.toSubalgebra : Set K) :=
    L.adjoin_toSubalgebra_of_isAlgebraic E halg
  have := L.toSubalgebra.adjoin_rank_le E
  rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this
Inequality of Extension Degrees in Algebraic Field Towers: $[E(L) : E] \leq [L : F]$
Informal description
Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If either $E/F$ or $L/F$ is algebraic, then the dimension of the field extension $E(L)/E$ is at most the dimension of $L/F$, i.e., \[ [E(L) : E] \leq [L : F]. \]
IntermediateField.adjoin_rank_le_of_isAlgebraic_left theorem
(L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] : Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L
Full source 
theorem adjoin_rank_le_of_isAlgebraic_left (L : IntermediateField F K)
    [halg : Algebra.IsAlgebraic F E] :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
  adjoin_rank_le_of_isAlgebraic E L (Or.inl halg)
Inequality of Extension Degrees in Algebraic Field Towers (Left Case): $[E(L) : E] \leq [L : F]$
Informal description
Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If $E/F$ is algebraic, then the dimension of the field extension $E(L)/E$ is at most the dimension of $L/F$, i.e., \[ [E(L) : E] \leq [L : F]. \]
IntermediateField.adjoin_rank_le_of_isAlgebraic_right theorem
(L : IntermediateField F K) [halg : Algebra.IsAlgebraic F L] : Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L
Full source 
theorem adjoin_rank_le_of_isAlgebraic_right (L : IntermediateField F K)
    [halg : Algebra.IsAlgebraic F L] :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
  adjoin_rank_le_of_isAlgebraic E L (Or.inr halg)
Inequality of extension degrees: $[E(L) : E] \leq [L : F]$ when $L/F$ is algebraic
Informal description
Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If $L/F$ is algebraic, then the dimension of the field extension $E(L)/E$ is at most the dimension of $L/F$, i.e., \[ [E(L) : E] \leq [L : F]. \]
IntermediateField.adjoin_simple_isCompactElement theorem
(x : E) : IsCompactElement F⟮x⟯
Full source 
/-- Adjoining a single element is compact in the lattice of intermediate fields. -/
theorem adjoin_simple_isCompactElement (x : E) : IsCompactElement F⟮x⟯ := by
  simp_rw [isCompactElement_iff_le_of_directed_sSup_le,
    adjoin_simple_le_iff, sSup_eq_iSup', ← exists_prop]
  intro s hne hs hx
  have := hne.to_subtype
  rwa [← SetLike.mem_coe, coe_iSup_of_directed hs.directed_val, mem_iUnion, Subtype.exists] at hx
Compactness of Simple Field Extensions in the Lattice of Intermediate Fields
Informal description
For any element $x$ in a field extension $E$ of $F$, the intermediate field $F(x)$ obtained by adjoining $x$ to $F$ is a compact element in the complete lattice of intermediate fields between $F$ and $E$. This means that for any family of intermediate fields $\{K_i\}_{i \in I}$ such that $F(x) \subseteq \bigvee_{i \in I} K_i$, there exists a finite subset $J \subseteq I$ such that $F(x) \subseteq \bigvee_{i \in J} K_i$.
IntermediateField.adjoin_finset_isCompactElement theorem
(S : Finset E) : IsCompactElement (adjoin F S : IntermediateField F E)
Full source 
/-- Adjoining a finite subset is compact in the lattice of intermediate fields. -/
theorem adjoin_finset_isCompactElement (S : Finset E) :
    IsCompactElement (adjoin F S : IntermediateField F E) := by
  rw [← biSup_adjoin_simple]
  simp_rw [Finset.mem_coe, ← Finset.sup_eq_iSup]
  exact isCompactElement_finsetSup S fun x _ => adjoin_simple_isCompactElement x
Compactness of Finite Field Adjoinings in the Lattice of Intermediate Fields
Informal description
For any finite subset $S$ of a field extension $E$ over $F$, the intermediate field $F(S)$ obtained by adjoining $S$ to $F$ is a compact element in the complete lattice of intermediate fields between $F$ and $E$. This means that for any family of intermediate fields $\{K_i\}_{i \in I}$ such that $F(S) \subseteq \bigvee_{i \in I} K_i$, there exists a finite subset $J \subseteq I$ such that $F(S) \subseteq \bigvee_{i \in J} K_i$.
IntermediateField.adjoin_finite_isCompactElement theorem
{S : Set E} (h : S.Finite) : IsCompactElement (adjoin F S)
Full source 
/-- Adjoining a finite subset is compact in the lattice of intermediate fields. -/
theorem adjoin_finite_isCompactElement {S : Set E} (h : S.Finite) : IsCompactElement (adjoin F S) :=
  Finite.coe_toFinset h ▸ adjoin_finset_isCompactElement h.toFinset
Compactness of Finite Field Adjoinings in the Lattice of Intermediate Fields
Informal description
For any finite subset $S$ of a field extension $E$ over $F$, the intermediate field $F(S)$ obtained by adjoining $S$ to $F$ is a compact element in the complete lattice of intermediate fields between $F$ and $E$. This means that for any family of intermediate fields $\{K_i\}_{i \in I}$ such that $F(S) \subseteq \bigvee_{i \in I} K_i$, there exists a finite subset $J \subseteq I$ such that $F(S) \subseteq \bigvee_{i \in J} K_i$.
IntermediateField.instIsCompactlyGenerated instance
: IsCompactlyGenerated (IntermediateField F E)
Full source 
/-- The lattice of intermediate fields is compactly generated. -/
instance : IsCompactlyGenerated (IntermediateField F E) :=
  ⟨fun s =>
    ⟨(fun x => F⟮x⟯) '' s,
      ⟨by rintro t ⟨x, _, rfl⟩; exact adjoin_simple_isCompactElement x,
        sSup_image.trans <| (biSup_adjoin_simple _).trans <|
          le_antisymm (adjoin_le_iff.mpr le_rfl) <| subset_adjoin F (s : Set E)⟩⟩⟩
The Lattice of Intermediate Fields is Compactly Generated
Informal description
The complete lattice of intermediate fields between fields $F$ and $E$ is compactly generated. This means that every intermediate field $K$ can be expressed as the supremum of all compact intermediate fields contained in $K$, where an intermediate field is compact if it is finitely generated over $F$.
IntermediateField.exists_finset_of_mem_iSup theorem
{ι : Type*} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ i, f i) : ∃ s : Finset ι, x ∈ ⨆ i ∈ s, f i
Full source 
theorem exists_finset_of_mem_iSup {ι : Type*} {f : ι → IntermediateField F E} {x : E}
    (hx : x ∈ ⨆ i, f i) : ∃ s : Finset ι, x ∈ ⨆ i ∈ s, f i := by
  have := (adjoin_simple_isCompactElement x).exists_finset_of_le_iSup (IntermediateField F E) f
  simp only [adjoin_simple_le_iff] at this
  exact this hx
Finite approximation property for elements in the supremum of intermediate fields
Informal description
Let $F$ be a field and $E$ a field extension of $F$. For any family of intermediate fields $\{K_i\}_{i \in \iota}$ between $F$ and $E$ and any element $x \in E$ such that $x$ belongs to the supremum $\bigvee_{i \in \iota} K_i$ of the family in the complete lattice of intermediate fields, there exists a finite subset $s \subseteq \iota$ such that $x \in \bigvee_{i \in s} K_i$.
IntermediateField.exists_finset_of_mem_supr' theorem
{ι : Type*} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, F⟮(i.2 : E)⟯
Full source 
theorem exists_finset_of_mem_supr' {ι : Type*} {f : ι → IntermediateField F E} {x : E}
    (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, F⟮(i.2 : E)⟯ := by
  refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)
  exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)
Finite Approximation Property for Elements in the Supremum of Intermediate Fields via Adjoined Elements
Informal description
Let $F$ be a field and $E$ a field extension of $F$. For any family of intermediate fields $\{K_i\}_{i \in \iota}$ between $F$ and $E$ and any element $x \in E$ such that $x$ belongs to the supremum $\bigvee_{i \in \iota} K_i$ of the family in the complete lattice of intermediate fields, there exists a finite subset $s \subseteq \bigsqcup_{i \in \iota} K_i$ such that $x$ belongs to the supremum of the fields $F(\alpha)$ for each $\alpha$ in $s$.
IntermediateField.exists_finset_of_mem_supr'' theorem
{ι : Type*} {f : ι → IntermediateField F E} (h : ∀ i, Algebra.IsAlgebraic F (f i)) {x : E} (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet E)
Full source 
theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F E}
    (h : ∀ i, Algebra.IsAlgebraic F (f i)) {x : E} (hx : x ∈ ⨆ i, f i) :
    ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet E) := by
  refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i x1 hx1 => ?_)) hx)
  refine SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ ?_)
    (subset_adjoin F (rootSet (minpoly F x1) E) ?_)
  · rw [IntermediateField.minpoly_eq, Subtype.coe_mk]
  · rw [mem_rootSet_of_ne, minpoly.aeval]
    exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))
Finite Approximation Property for Algebraic Elements in the Supremum of Intermediate Fields via Minimal Polynomial Roots
Informal description
Let $F$ be a field and $E$ a field extension of $F$. Given a family of intermediate fields $\{K_i\}_{i \in \iota}$ between $F$ and $E$ such that each $K_i$ is algebraic over $F$, and an element $x \in E$ that belongs to the supremum $\bigvee_{i \in \iota} K_i$ of the family in the complete lattice of intermediate fields, there exists a finite subset $s \subseteq \bigsqcup_{i \in \iota} K_i$ such that $x$ belongs to the adjunction $F(R)$, where $R$ is the set of roots in $E$ of the minimal polynomials over $F$ of the elements in $s$.
IntermediateField.exists_finset_of_mem_adjoin theorem
{S : Set E} {x : E} (hx : x ∈ adjoin F S) : ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E)
Full source 
theorem exists_finset_of_mem_adjoin {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
    ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E) := by
  simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx
  obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx
  classical
  refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
  rintro _ h _ rfl
  exact subset_adjoin F _ ⟨_, h, rfl⟩
Finite approximation property for elements in the adjunction $F(S)$
Informal description
For any subset $S$ of a field extension $E$ over $F$ and any element $x \in E$ that lies in the adjunction $F(S)$, there exists a finite subset $T \subseteq S$ such that $x \in F(T)$.
IntermediateField.rank_eq_one_iff theorem
: Module.rank F K = 1 ↔ K = ⊥
Full source 
@[simp]
theorem rank_eq_one_iff : Module.rankModule.rank F K = 1 ↔ K = ⊥ := by
  rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]
Rank-One Characterization of Trivial Intermediate Field
Informal description
For an intermediate field $K$ between fields $F$ and $E$, the rank of $K$ as an $F$-module is equal to 1 if and only if $K$ is the trivial intermediate field (i.e., $K = \bot$).
IntermediateField.finrank_eq_one_iff theorem
: finrank F K = 1 ↔ K = ⊥
Full source 
@[simp]
theorem finrank_eq_one_iff : finrankfinrank F K = 1 ↔ K = ⊥ := by
  rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]
Finite Rank-One Characterization for Intermediate Fields
Informal description
For an intermediate field $K$ between fields $F$ and $E$, the finite rank of $K$ as an $F$-vector space is equal to 1 if and only if $K$ is the trivial intermediate field (i.e., $K = \bot$).
IntermediateField.rank_bot theorem
: Module.rank F (⊥ : IntermediateField F E) = 1
Full source 
@[simp]
protected theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by
  rw [rank_eq_one_iff]
Rank of Trivial Intermediate Field is One
Informal description
For fields $F$ and $E$ with $F$ a subfield of $E$, the rank of the trivial intermediate field $\bot$ (which is $F$ itself) as an $F$-module is equal to $1$.
IntermediateField.finrank_bot theorem
: finrank F (⊥ : IntermediateField F E) = 1
Full source 
@[simp]
protected theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by
  rw [finrank_eq_one_iff]
Finite Rank of Trivial Intermediate Field is One
Informal description
For any field extension $E$ of a field $F$, the finite rank of the trivial intermediate field $\bot$ (the smallest intermediate field between $F$ and $E$) as an $F$-vector space is equal to 1, i.e., $\text{finrank}_F (\bot) = 1$.
IntermediateField.rank_bot' theorem
: Module.rank (⊥ : IntermediateField F E) E = Module.rank F E
Full source 
@[simp] theorem rank_bot' : Module.rank (⊥ : IntermediateField F E) E = Module.rank F E := by
  rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
Rank Preservation over Trivial Intermediate Field: $\operatorname{rank}_F E = \operatorname{rank}_F E$
Informal description
For fields $F \subseteq E$, the rank of $E$ as a module over the trivial intermediate field $\bot$ (which is $F$ itself) is equal to the rank of $E$ as an $F$-module, i.e., \[ \operatorname{rank}_F E = \operatorname{rank}_F E. \]
IntermediateField.finrank_bot' theorem
: finrank (⊥ : IntermediateField F E) E = finrank F E
Full source 
@[simp] theorem finrank_bot' : finrank (⊥ : IntermediateField F E) E = finrank F E :=
  congr(Cardinal.toNat $(rank_bot'))
Finite Rank Preservation over Trivial Intermediate Field: $\text{finrank}_F E = \text{finrank}_F E$
Informal description
For a field extension $E$ over $F$, the finite rank of $E$ as a vector space over the trivial intermediate field $\bot$ (which is $F$ itself) is equal to the finite rank of $E$ as an $F$-vector space, i.e., \[ \text{finrank}_F E = \text{finrank}_F E. \]
IntermediateField.rank_top theorem
: Module.rank (⊤ : IntermediateField F E) E = 1
Full source 
@[simp] protected theorem rank_top : Module.rank (⊤ : IntermediateField F E) E = 1 :=
  Subalgebra.bot_eq_top_iff_rank_eq_one.mp <| top_le_iff.mp fun x _ ↦ ⟨⟨x, trivial⟩, rfl⟩
Rank of Field Extension over Top Intermediate Field: $\text{rank}_{\top} E = 1$
Informal description
For any field extension $E$ over $F$, the rank of $E$ as a module over the top intermediate field $\top$ (which is $E$ itself) is equal to $1$.
IntermediateField.finrank_top theorem
: finrank (⊤ : IntermediateField F E) E = 1
Full source 
@[simp] protected theorem finrank_top : finrank (⊤ : IntermediateField F E) E = 1 :=
  rank_eq_one_iff_finrank_eq_one.mp IntermediateField.rank_top
Finite Rank of Field Extension over Itself is One
Informal description
For any field extension $E$ over $F$, the finite rank of $E$ as a vector space over the top intermediate field $\top$ (which is $E$ itself) is equal to $1$, i.e., $\text{finrank}_E E = 1$.
IntermediateField.rank_top' theorem
: Module.rank F (⊤ : IntermediateField F E) = Module.rank F E
Full source 
@[simp] theorem rank_top' : Module.rank F (⊤ : IntermediateField F E) = Module.rank F E :=
  rank_top F E
Rank of Top Intermediate Field Equals Rank of Extension Field
Informal description
For fields $F \subseteq E$, the rank of the top intermediate field $\top$ (which is $E$ itself) as an $F$-module is equal to the rank of $E$ as an $F$-module, i.e., $\text{rank}_F(E) = \text{rank}_F(E)$.
IntermediateField.finrank_top' theorem
: finrank F (⊤ : IntermediateField F E) = finrank F E
Full source 
@[simp] theorem finrank_top' : finrank F (⊤ : IntermediateField F E) = finrank F E :=
  finrank_top F E
Finite Dimension of Top Intermediate Field Equals Finite Dimension of Extension
Informal description
For any field extension $E$ over $F$, the finite dimension of the top intermediate field (i.e., $E$ itself) over $F$ is equal to the finite dimension of $E$ over $F$, i.e., $\text{finrank}_F(E) = \text{finrank}_F(E)$.
IntermediateField.rank_adjoin_eq_one_iff theorem
: Module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E)
Full source 
theorem rank_adjoin_eq_one_iff : Module.rankModule.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
  Iff.trans rank_eq_one_iff adjoin_eq_bot_iff
Rank-One Characterization of Field Adjoin: $\text{rank}_F(F(S)) = 1 \leftrightarrow S \subseteq F$
Informal description
For a field extension $E$ of $F$ and a subset $S \subseteq E$, the rank of the field extension $F(S)$ over $F$ is equal to 1 if and only if $S$ is contained in the base field $F$ (i.e., $S \subseteq F$).
IntermediateField.rank_adjoin_simple_eq_one_iff theorem
: Module.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E)
Full source 
theorem rank_adjoin_simple_eq_one_iff :
    Module.rankModule.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E) := by
  rw [rank_adjoin_eq_one_iff]; exact Set.singleton_subset_iff
Rank-One Characterization of Simple Field Extension: $\text{rank}_F(F(\alpha)) = 1 \leftrightarrow \alpha \in F$
Informal description
For a field extension $E$ of $F$ and an element $\alpha \in E$, the rank of the field extension $F(\alpha)$ over $F$ is equal to 1 if and only if $\alpha$ belongs to the base field $F$ (i.e., $\alpha \in F$).
IntermediateField.finrank_adjoin_eq_one_iff theorem
: finrank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E)
Full source 
theorem finrank_adjoin_eq_one_iff : finrankfinrank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
  Iff.trans finrank_eq_one_iff adjoin_eq_bot_iff
Finite Dimension-One Characterization for Field Adjunction: $\text{dim}_F F(S) = 1 \leftrightarrow S \subseteq F$
Informal description
For a field extension $E$ of $F$ and a subset $S \subseteq E$, the finite dimension of $F(S)$ as a vector space over $F$ is equal to 1 if and only if $S$ is contained in the base field $F$ (i.e., $S \subseteq F$). In other words: $$\text{dim}_F F(S) = 1 \leftrightarrow S \subseteq F$$
IntermediateField.finrank_adjoin_simple_eq_one_iff theorem
: finrank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E)
Full source 
theorem finrank_adjoin_simple_eq_one_iff :
    finrankfinrank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E) := by
  rw [finrank_adjoin_eq_one_iff]; exact Set.singleton_subset_iff
Finite Dimension-One Characterization for Simple Field Extension: $\text{dim}_F F(\alpha) = 1 \leftrightarrow \alpha \in F$
Informal description
For a field extension $E$ of $F$ and an element $\alpha \in E$, the finite dimension of $F(\alpha)$ as a vector space over $F$ is equal to 1 if and only if $\alpha$ belongs to the base field $F$. In other words: $$\text{dim}_F F(\alpha) = 1 \leftrightarrow \alpha \in F$$
IntermediateField.bot_eq_top_of_rank_adjoin_eq_one theorem
(h : ∀ x : E, Module.rank F F⟮x⟯ = 1) : (⊥ : IntermediateField F E) = ⊤
Full source 
/-- If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`. -/
theorem bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) :
    (⊥ : IntermediateField F E) = ⊤ := by
  ext y
  rw [iff_true_right IntermediateField.mem_top]
  exact rank_adjoin_simple_eq_one_iff.mp (h y)
Field Equality from Dimension-One Adjoints: $F = E$ when $\dim_F F(x) = 1$ for all $x \in E$
Informal description
Let $E$ be a field extension of $F$. If for every element $x \in E$, the field extension $F(x)$ has dimension $1$ over $F$, then the smallest intermediate field $\bot$ (which is $F$ itself) is equal to the largest intermediate field $\top$ (which is $E$). In other words, $F = E$.
IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one theorem
(h : ∀ x : E, finrank F F⟮x⟯ = 1) : (⊥ : IntermediateField F E) = ⊤
Full source 
theorem bot_eq_top_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) :
    (⊥ : IntermediateField F E) = ⊤ := by
  ext y
  rw [iff_true_right IntermediateField.mem_top]
  exact finrank_adjoin_simple_eq_one_iff.mp (h y)
Field Equality Criterion via Finite-Dimensional Simple Extensions: $F = E$ when all $F(x)$ have dimension 1
Informal description
For a field extension $E$ of $F$, if for every element $x \in E$ the finite dimension of $F(x)$ as a vector space over $F$ is equal to 1, then the smallest intermediate field $\bot$ (which is $F$ itself) is equal to the largest intermediate field $\top$ (which is $E$). In other words: $$(\forall x \in E,\ \text{dim}_F F(x) = 1) \implies F = E$$
IntermediateField.subsingleton_of_rank_adjoin_eq_one theorem
(h : ∀ x : E, Module.rank F F⟮x⟯ = 1) : Subsingleton (IntermediateField F E)
Full source 
theorem subsingleton_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) :
    Subsingleton (IntermediateField F E) :=
  subsingleton_of_bot_eq_top (bot_eq_top_of_rank_adjoin_eq_one h)
Subsingleton of Intermediate Fields When All Simple Extensions Have Dimension One
Informal description
Let $E$ be a field extension of $F$. If for every element $x \in E$, the dimension of the field extension $F(x)$ over $F$ is equal to $1$, then the collection of intermediate fields between $F$ and $E$ is a subsingleton (i.e., has at most one element).
IntermediateField.subsingleton_of_finrank_adjoin_eq_one theorem
(h : ∀ x : E, finrank F F⟮x⟯ = 1) : Subsingleton (IntermediateField F E)
Full source 
theorem subsingleton_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) :
    Subsingleton (IntermediateField F E) :=
  subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_eq_one h)
Subsingleton Lattice of Intermediate Fields When All Simple Extensions Have Dimension 1
Informal description
For a field extension $E$ of $F$, if for every element $x \in E$ the finite dimension of the field extension $F(x)$ over $F$ is equal to 1, then the lattice of intermediate fields between $F$ and $E$ is a subsingleton (i.e., has at most one element).
IntermediateField.bot_eq_top_of_finrank_adjoin_le_one theorem
[FiniteDimensional F E] (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : (⊥ : IntermediateField F E) = ⊤
Full source 
/-- If `F⟮x⟯` has dimension `≤1` over `F` for every `x ∈ E` then `F = E`. -/
theorem bot_eq_top_of_finrank_adjoin_le_one [FiniteDimensional F E]
    (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : (⊥ : IntermediateField F E) = ⊤ := by
  apply bot_eq_top_of_finrank_adjoin_eq_one
  exact fun x => by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]
Field Equality Criterion via Finite-Dimensional Simple Extensions: $F = E$ when all $F(x)$ have dimension $\leq 1$
Informal description
Let $E$ be a finite-dimensional field extension of $F$. If for every element $x \in E$, the finite dimension of the field extension $F(x)$ over $F$ is at most $1$, then the smallest intermediate field $\bot$ (which is $F$ itself) is equal to the largest intermediate field $\top$ (which is $E$). In other words: $$(\forall x \in E,\ \text{dim}_F F(x) \leq 1) \implies F = E$$
IntermediateField.subsingleton_of_finrank_adjoin_le_one theorem
[FiniteDimensional F E] (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : Subsingleton (IntermediateField F E)
Full source 
theorem subsingleton_of_finrank_adjoin_le_one [FiniteDimensional F E]
    (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : Subsingleton (IntermediateField F E) :=
  subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_le_one h)
Subsingleton Lattice of Intermediate Fields When All Simple Extensions Have Dimension $\leq 1$
Informal description
Let $E$ be a finite-dimensional field extension of $F$. If for every element $x \in E$, the dimension of the field extension $F(x)$ over $F$ is at most $1$, then the lattice of intermediate fields between $F$ and $E$ is a subsingleton (i.e., has at most one element).
IntermediateField.minpoly_gen theorem
(α : E) : minpoly F (AdjoinSimple.gen F α) = minpoly F α
Full source 
theorem minpoly_gen (α : E) :
    minpoly F (AdjoinSimple.gen F α) = minpoly F α := by
  rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]
Minimal Polynomial of Generator in Field Extension Equals Minimal Polynomial of Adjoined Element
Informal description
For any element $\alpha$ in a field extension $E$ of $F$, the minimal polynomial of the generator $\text{AdjoinSimple.gen}(F, \alpha)$ in the field extension $F(\alpha)$ is equal to the minimal polynomial of $\alpha$ over $F$, i.e., \[ \text{minpoly}_F(\text{AdjoinSimple.gen}(F, \alpha)) = \text{minpoly}_F(\alpha). \]
IntermediateField.aeval_gen_minpoly theorem
(α : E) : aeval (AdjoinSimple.gen F α) (minpoly F α) = 0
Full source 
theorem aeval_gen_minpoly (α : E) : aeval (AdjoinSimple.gen F α) (minpoly F α) = 0 := by
  ext
  convert minpoly.aeval F α
  conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]
  exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm
Minimal Polynomial Vanishes at Generator of Adjoined Field
Informal description
For any element $\alpha$ in a field extension $E$ of $F$, the evaluation of the minimal polynomial of $\alpha$ over $F$ at the generator of the field extension $F(\alpha)$ is zero, i.e., $\text{aeval}_{F(\alpha)}(\text{minpoly}_F(\alpha)) = 0$.
IntermediateField.adjoinRootEquivAdjoin definition
(h : IsIntegral F α) : AdjoinRoot (minpoly F α) ≃ₐ[F] F⟮α⟯
Full source 
/-- algebra isomorphism between `AdjoinRoot` and `F⟮α⟯` -/
@[stacks 09G1 "Algebraic case"]
noncomputable def adjoinRootEquivAdjoin (h : IsIntegral F α) :
    AdjoinRootAdjoinRoot (minpoly F α) ≃ₐ[F] F⟮α⟯ :=
  AlgEquiv.ofBijective
    (AdjoinRoot.liftHom (minpoly F α) (AdjoinSimple.gen F α) (aeval_gen_minpoly F α))
    (by
      set f := AdjoinRoot.lift _ _ (aeval_gen_minpoly F α :)
      haveI := Fact.mk (minpoly.irreducible h)
      constructor
      · exact RingHom.injective f
      · suffices F⟮α⟯.toSubfield ≤ RingHom.fieldRange (F⟮α⟯.toSubfield.subtype.comp f) by
          intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩
        refine Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)
        · obtain ⟨y, hy⟩ := hx
          refine ⟨y, ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_of (aeval_gen_minpoly F α)]
          exact hy
        · refine Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]
          rfl)
Isomorphism between Adjoined Root and Field Extension \( F(\alpha) \)
Informal description
Given a field extension \( E \) of \( F \) and an element \( \alpha \in E \) that is integral over \( F \), there exists an \( F \)-algebra isomorphism between the ring \( \text{AdjoinRoot}(\text{minpoly}_F(\alpha)) \) (which adjoins a root of the minimal polynomial of \( \alpha \) over \( F \)) and the field \( F(\alpha) \). This isomorphism maps the root of the minimal polynomial in \( \text{AdjoinRoot}(\text{minpoly}_F(\alpha)) \) to the generator \( \alpha \) of \( F(\alpha) \).
IntermediateField.adjoinRootEquivAdjoin_apply_root theorem
(h : IsIntegral F α) : adjoinRootEquivAdjoin F h (AdjoinRoot.root (minpoly F α)) = AdjoinSimple.gen F α
Full source 
theorem adjoinRootEquivAdjoin_apply_root (h : IsIntegral F α) :
    adjoinRootEquivAdjoin F h (AdjoinRoot.root (minpoly F α)) = AdjoinSimple.gen F α :=
  AdjoinRoot.lift_root (aeval_gen_minpoly F α)
Isomorphism Maps Adjoined Root to Generator in Field Extension \( F(\alpha) \)
Informal description
Given a field extension \( E \) of \( F \) and an element \( \alpha \in E \) that is integral over \( F \), the isomorphism \( \text{adjoinRootEquivAdjoin}_F h \) maps the adjoined root of the minimal polynomial \( \text{minpoly}_F(\alpha) \) in \( \text{AdjoinRoot}(\text{minpoly}_F(\alpha)) \) to the generator \( \alpha \) of the field extension \( F(\alpha) \). In other words, \[ \text{adjoinRootEquivAdjoin}_F h \left( \text{root}(\text{minpoly}_F(\alpha)) \right) = \text{gen}_F(\alpha). \]
IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen theorem
(h : IsIntegral F α) : (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)
Full source 
@[simp]
theorem adjoinRootEquivAdjoin_symm_apply_gen (h : IsIntegral F α) :
    (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α) := by
  rw [AlgEquiv.symm_apply_eq, adjoinRootEquivAdjoin_apply_root]
Inverse Isomorphism Maps Generator to Adjoined Root in Field Extension \( F(\alpha) \)
Informal description
Given a field extension \( E \) of \( F \) and an element \( \alpha \in E \) that is integral over \( F \), the inverse of the isomorphism \( \text{adjoinRootEquivAdjoin}_F h \) maps the generator \( \alpha \) of the field extension \( F(\alpha) \) to the adjoined root of the minimal polynomial \( \text{minpoly}_F(\alpha) \) in \( \text{AdjoinRoot}(\text{minpoly}_F(\alpha)) \). In other words, \[ (\text{adjoinRootEquivAdjoin}_F h)^{-1}(\text{gen}_F(\alpha)) = \text{root}(\text{minpoly}_F(\alpha)). \]
IntermediateField.adjoin_root_eq_top theorem
(p : K[X]) [Fact (Irreducible p)] : K⟮AdjoinRoot.root p⟯ = ⊤
Full source 
theorem adjoin_root_eq_top (p : K[X]) [Fact (Irreducible p)] : K⟮AdjoinRoot.root p⟯ = ⊤ :=
  (eq_adjoin_of_eq_algebra_adjoin K _ ⊤ (AdjoinRoot.adjoinRoot_eq_top (f := p)).symm).symm
Field Extension Generated by Adjoined Root of Irreducible Polynomial Equals Quotient Field
Informal description
Let $K$ be a field and $p \in K[X]$ an irreducible polynomial. Then the field extension $K(\alpha)$ generated by adjoining a root $\alpha$ of $p$ to $K$ is equal to the entire field $K[X]/(p)$, i.e., $K(\alpha) = K[X]/(p)$.
IntermediateField.powerBasisAux definition
{x : L} (hx : IsIntegral K x) : Basis (Fin (minpoly K x).natDegree) K K⟮x⟯
Full source 
/-- The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`. -/
noncomputable def powerBasisAux {x : L} (hx : IsIntegral K x) :
    Basis (Fin (minpoly K x).natDegree) K K⟮x⟯ :=
  (AdjoinRoot.powerBasis (minpoly.ne_zero hx)).basis
    |>.map (adjoinRootEquivAdjoin K hx).toLinearEquiv
    |>.reindex (finCongr rfl)
Power basis for \( K(x) \) over \( K \)
Informal description
Given a field extension \( L \) of \( K \) and an element \( x \in L \) that is integral over \( K \), the set \(\{1, x, \ldots, x^{d-1}\}\) forms a basis for the field extension \( K(x) \) as a \( K \)-vector space, where \( d \) is the degree of the minimal polynomial of \( x \) over \( K \). This basis is constructed by first taking the power basis of the adjoined root of the minimal polynomial of \( x \), then mapping it via the linear equivalence between the adjoined root and \( K(x) \), and finally reindexing the basis to match the degree of the minimal polynomial.
IntermediateField.adjoin.powerBasis definition
{x : L} (hx : IsIntegral K x) : PowerBasis K K⟮x⟯
Full source 
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`. -/
@[simps]
noncomputable def adjoin.powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K K⟮x⟯ where
  gen := AdjoinSimple.gen K x
  dim := (minpoly K x).natDegree
  basis := powerBasisAux hx
  basis_eq_pow i := by
    rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow,
      finCongr_symm, finCongr_apply, Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply,
      map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root]
Power basis for \( K(x) \) over \( K \)
Informal description
Given a field extension \( L \) of \( K \) and an element \( x \in L \) that is integral over \( K \), the power basis for the field extension \( K(x) \) over \( K \) is given by the basis \(\{1, x, \ldots, x^{d-1}\}\), where \( d \) is the degree of the minimal polynomial of \( x \) over \( K \). The generator of this power basis is the element \( x \) itself, and the dimension of the basis is equal to the degree of the minimal polynomial. The basis vectors are precisely the powers of \( x \) up to \( x^{d-1} \).
IntermediateField.adjoin.finiteDimensional theorem
{x : L} (hx : IsIntegral K x) : FiniteDimensional K K⟮x⟯
Full source 
theorem adjoin.finiteDimensional {x : L} (hx : IsIntegral K x) : FiniteDimensional K K⟮x⟯ :=
  (adjoin.powerBasis hx).finite
Finite-dimensionality of simple algebraic field extensions
Informal description
Let $L$ be a field extension of $K$ and let $x \in L$ be an element integral over $K$. Then the field extension $K(x)$ obtained by adjoining $x$ to $K$ is finite-dimensional as a vector space over $K$.
IntermediateField.isAlgebraic_adjoin_simple theorem
{x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K K⟮x⟯
Full source 
theorem isAlgebraic_adjoin_simple {x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K K⟮x⟯ :=
  have := adjoin.finiteDimensional hx; Algebra.IsAlgebraic.of_finite K K⟮x⟯
Algebraicity of Simple Algebraic Field Extensions
Informal description
Let $L$ be a field extension of $K$ and let $x \in L$ be an element integral over $K$. Then the field extension $K(x)$ obtained by adjoining $x$ to $K$ is algebraic over $K$.
IntermediateField.adjoin.finrank theorem
{x : L} (hx : IsIntegral K x) : Module.finrank K K⟮x⟯ = (minpoly K x).natDegree
Full source 
/-- If `x` is an algebraic element of field `K`, then its minimal polynomial has degree
`[K(x) : K]`. -/
@[stacks 09GN]
theorem adjoin.finrank {x : L} (hx : IsIntegral K x) :
    Module.finrank K K⟮x⟯ = (minpoly K x).natDegree := by
  rw [PowerBasis.finrank (adjoin.powerBasis hx :)]
  rfl
Degree of Simple Algebraic Extension Equals Minimal Polynomial Degree
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$, the degree of the field extension $K(x)/K$ equals the degree of the minimal polynomial of $x$ over $K$, i.e., \[ [K(x) : K] = \deg(\text{minpoly}_K(x)). \]
IntermediateField.adjoin_eq_top_of_adjoin_eq_top theorem
[Algebra E K] [IsScalarTower F E K] {S : Set K} (hprim : adjoin F S = ⊤) : adjoin E S = ⊤
Full source 
/-- If `K / E / F` is a field extension tower, `S ⊂ K` is such that `F(S) = K`,
then `E(S) = K`. -/
theorem adjoin_eq_top_of_adjoin_eq_top [Algebra E K] [IsScalarTower F E K]
    {S : Set K} (hprim : adjoin F S = ⊤) : adjoin E S = ⊤ :=
  restrictScalars_injective F <| by
    rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
      coe_restrictScalars, ← adjoin_le_iff]
Field Adjoin Equality in Tower Extensions: $E(S) = K$ when $F(S) = K$
Informal description
Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $S$ be a subset of $K$ such that the field adjunction $F(S) = K$. Then the field adjunction $E(S)$ is also equal to $K$.
IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element theorem
[FiniteDimensional F E] (hprim : adjoin F { α } = ⊤) (K : IntermediateField F E) : adjoin F ((minpoly K α).map (algebraMap K E)).coeffs = K
Full source 
/-- If `E / F` is a finite extension such that `E = F(α)`, then for any intermediate field `K`, the
`F` adjoin the coefficients of `minpoly K α` is equal to `K` itself. -/
theorem adjoin_minpoly_coeff_of_exists_primitive_element
    [FiniteDimensional F E] (hprim : adjoin F {α} = ⊤) (K : IntermediateField F E) :
    adjoin F ((minpoly K α).map (algebraMap K E)).coeffs = K := by
  set g := (minpoly K α).map (algebraMap K E)
  set K' : IntermediateField F E := adjoin F g.coeffs
  have hsub : K' ≤ K := by
    refine adjoin_le_iff.mpr fun x ↦ ?_
    rw [Finset.mem_coe, mem_coeffs_iff]
    rintro ⟨n, -, rfl⟩
    rw [coeff_map]
    apply Subtype.mem
  have dvd_g : minpolyminpoly K' α ∣ g.toSubring K'.toSubring (subset_adjoin F _) := by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map]
    erw [g.map_toSubring K'.toSubring]
    rw [eval_map, ← aeval_def]
    exact minpoly.aeval K α
  have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) := by
    intro K
    have := adjoin.finrank (.of_finite K α)
    rw [adjoin_eq_top_of_adjoin_eq_top F hprim] at this
    erw [finrank_top K E] at this
    exact this
  refine eq_of_le_of_finrank_le' hsub ?_
  simp_rw [finrank_eq]
  convert natDegree_le_of_dvd dvd_g
    ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero using 1
  rw [natDegree_toSubring, natDegree_map]
Adjoining Minimal Polynomial Coefficients Preserves Intermediate Field in Primitive Extension
Informal description
Let $F \subseteq E$ be a finite field extension such that $E = F(\alpha)$ for some $\alpha \in E$. Then for any intermediate field $K$ between $F$ and $E$, the field obtained by adjoining to $F$ the coefficients of the minimal polynomial of $\alpha$ over $K$ is equal to $K$ itself. In symbols: \[ F\big(\text{coeffs}(\text{minpoly}_K(\alpha))\big) = K \]
IntermediateField.instFiniteSubtypeMemBot instance
: Module.Finite F (⊥ : IntermediateField F E)
Full source 
instance : Module.Finite F (⊥ : IntermediateField F E) := Subalgebra.finite_bot
Finite Generation of the Bottom Intermediate Field
Informal description
The bottom intermediate field $\bot$ between fields $F$ and $E$ is finitely generated as an $F$-module.
IntermediateField.exists_lt_finrank_of_infinite_dimensional theorem
[Algebra.IsAlgebraic F E] (hnfd : ¬FiniteDimensional F E) (n : ℕ) : ∃ L : IntermediateField F E, FiniteDimensional F L ∧ n < finrank F L
Full source 
/-- If `E / F` is an infinite algebraic extension, then there exists an intermediate field
`L / F` with arbitrarily large finite extension degree. -/
theorem exists_lt_finrank_of_infinite_dimensional
    [Algebra.IsAlgebraic F E] (hnfd : ¬ FiniteDimensional F E) (n : ℕ) :
    ∃ L : IntermediateField F E, FiniteDimensional F L ∧ n < finrank F L := by
  induction' n with n ih
  · exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
  obtain ⟨L, fin, hn⟩ := ih
  obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
    contrapose! hnfd
    rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
    exact topEquiv.toLinearEquiv.finiteDimensional
  let L' := L ⊔ F⟮x⟯
  haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
  refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
  have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
  have h2 : F⟮x⟯ ≤ L' := le_sup_right
  exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
Existence of Intermediate Fields with Arbitrarily Large Finite Degree in Infinite Algebraic Extensions
Informal description
Let $E/F$ be an infinite algebraic field extension. Then for any natural number $n$, there exists an intermediate field $L$ between $F$ and $E$ such that $L/F$ is finite-dimensional and $n < [L : F]$.
minpoly.natDegree_le theorem
(x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ finrank K L
Full source 
theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] :
    (minpoly K x).natDegree ≤ finrank K L :=
  le_of_eq_of_le (IntermediateField.adjoin.finrank (.of_finite _ _)).symm
    K⟮x⟯.toSubmodule.finrank_le
Minimal Polynomial Degree Bound in Finite Extensions
Informal description
Let $K$ be a field and $L$ a finite-dimensional field extension of $K$. For any element $x \in L$, the degree of the minimal polynomial of $x$ over $K$ is less than or equal to the dimension of $L$ as a vector space over $K$, i.e., \[ \deg(\text{minpoly}_K(x)) \leq [L : K]. \]
minpoly.degree_le theorem
(x : L) [FiniteDimensional K L] : (minpoly K x).degree ≤ finrank K L
Full source 
theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] :
    (minpoly K x).degree ≤ finrank K L :=
  degree_le_of_natDegree_le (minpoly.natDegree_le x)
Degree Bound for Minimal Polynomial in Finite Extensions
Informal description
Let $K$ be a field and $L$ a finite-dimensional field extension of $K$. For any element $x \in L$, the degree of the minimal polynomial of $x$ over $K$ is less than or equal to the dimension of $L$ as a vector space over $K$, i.e., \[ \deg(\text{minpoly}_K(x)) \leq [L : K]. \]
minpoly.degree_dvd theorem
{x : L} (hx : IsIntegral K x) : (minpoly K x).natDegree ∣ finrank K L
Full source 
/-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the
  minimal polynomial of `x` over `K` divides `[L : K]`. -/
theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) :
    (minpoly K x).natDegree ∣ finrank K L := by
  rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx]
  use finrank K⟮x⟯ L
  rw [mul_comm, finrank_mul_finrank]
Degree of Minimal Polynomial Divides Extension Degree
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$, the degree of the minimal polynomial of $x$ over $K$ divides the degree of the field extension $[L : K]$. In other words, \[ \deg(\text{minpoly}_K(x)) \mid [L : K]. \]
IntermediateField.isAlgebraic_iSup theorem
{ι : Type*} {t : ι → IntermediateField K L} (h : ∀ i, Algebra.IsAlgebraic K (t i)) : Algebra.IsAlgebraic K (⨆ i, t i : IntermediateField K L)
Full source 
/-- A compositum of algebraic extensions is algebraic -/
theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L}
    (h : ∀ i, Algebra.IsAlgebraic K (t i)) :
    Algebra.IsAlgebraic K (⨆ i, t i : IntermediateField K L) := by
  constructor
  rintro ⟨x, hx⟩
  obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx
  rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := (· ∈ _)) x hx, ← isAlgebraic_iff]
  haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
    adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))
  apply IsAlgebraic.of_finite
Compositum of Algebraic Extensions is Algebraic
Informal description
Let $K$ be a field and $L$ a field extension of $K$. Given a family of intermediate fields $\{t_i\}_{i \in \iota}$ between $K$ and $L$, if each $t_i$ is algebraic over $K$, then the compositum $\bigsqcup_{i \in \iota} t_i$ is also algebraic over $K$.
IntermediateField.isAlgebraic_adjoin theorem
{S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) : Algebra.IsAlgebraic K (adjoin K S)
Full source 
theorem isAlgebraic_adjoin {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) :
    Algebra.IsAlgebraic K (adjoin K S) := by
  rw [← biSup_adjoin_simple, ← iSup_subtype'']
  exact isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)
Algebraicity of Field Extensions Obtained by Adjoining Integral Elements
Informal description
Let $K$ be a field and $L$ a field extension of $K$. For any subset $S \subseteq L$ such that every element $x \in S$ is integral over $K$, the field extension $K(S)/K$ obtained by adjoining $S$ to $K$ is algebraic over $K$.
IntermediateField.finiteDimensional_adjoin theorem
{S : Set L} [Finite S] (hS : ∀ x ∈ S, IsIntegral K x) : FiniteDimensional K (adjoin K S)
Full source 
/-- If `L / K` is a field extension, `S` is a finite subset of `L`, such that every element of `S`
is integral (= algebraic) over `K`, then `K(S) / K` is a finite extension.
A direct corollary of `finiteDimensional_iSup_of_finite`. -/
theorem finiteDimensional_adjoin {S : Set L} [Finite S] (hS : ∀ x ∈ S, IsIntegral K x) :
    FiniteDimensional K (adjoin K S) := by
  rw [← biSup_adjoin_simple, ← iSup_subtype'']
  haveI (x : S) := adjoin.finiteDimensional (hS x.1 x.2)
  exact finiteDimensional_iSup_of_finite
Finite-dimensionality of field extensions obtained by adjoining finitely many integral elements
Informal description
Let $L/K$ be a field extension and $S$ a finite subset of $L$. If every element of $S$ is integral over $K$, then the field extension $K(S)/K$ is finite-dimensional.
IntermediateField.algHomAdjoinIntegralEquiv definition
(h : IsIntegral F α) : (F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K }
Full source 
/-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
of `minpoly α` in `K`. -/
noncomputable def algHomAdjoinIntegralEquiv (h : IsIntegral F α) :
    (F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K } :=
  (adjoin.powerBasis h).liftEquiv'.trans
    ((Equiv.refl _).subtypeEquiv fun x => by
      rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply])
Bijection between algebra homomorphisms \( F(\alpha) \to K \) and roots of the minimal polynomial of \( \alpha \) in \( K \)
Informal description
Given a field extension \( E \) of \( F \) and an element \( \alpha \in E \) that is integral over \( F \), there is a bijection between \( F \)-algebra homomorphisms from the field \( F(\alpha) \) to another field \( K \) and the roots in \( K \) of the minimal polynomial of \( \alpha \) over \( F \). More precisely, the equivalence maps: 1. Any \( F \)-algebra homomorphism \( \phi : F(\alpha) \to K \) to the element \( \phi(\alpha) \in K \), which is a root of the minimal polynomial of \( \alpha \) over \( F \). 2. Any root \( y \in K \) of the minimal polynomial of \( \alpha \) over \( F \) back to the unique \( F \)-algebra homomorphism \( F(\alpha) \to K \) sending \( \alpha \) to \( y \).
IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen theorem
(h : IsIntegral F α) (x : { x // x ∈ (minpoly F α).aroots K }) : (algHomAdjoinIntegralEquiv F h).symm x (AdjoinSimple.gen F α) = x
Full source 
lemma algHomAdjoinIntegralEquiv_symm_apply_gen (h : IsIntegral F α)
    (x : { x // x ∈ (minpoly F α).aroots K }) :
    (algHomAdjoinIntegralEquiv F h).symm x (AdjoinSimple.gen F α) = x :=
  (adjoin.powerBasis h).lift_gen x.val <| by
    rw [adjoin.powerBasis_gen, minpoly_gen]; exact (mem_aroots.mp x.2).2
Inverse of Algebra Homomorphism-Root Bijection Evaluates Generator to Root
Informal description
Let $F$ be a field and $E$ a field extension of $F$. Given an element $\alpha \in E$ that is integral over $F$, let $p \in F[X]$ be the minimal polynomial of $\alpha$ over $F$. For any root $x \in K$ of $p$ (where $K$ is another field extension of $F$), the inverse of the bijection between $F$-algebra homomorphisms $F(\alpha) \to K$ and roots of $p$ in $K$ maps $x$ to the unique $F$-algebra homomorphism $\phi : F(\alpha) \to K$ satisfying $\phi(\alpha) = x$. In other words, if $\phi$ is the unique $F$-algebra homomorphism extending $F \hookrightarrow K$ with $\phi(\alpha) = x$, then $\phi$ evaluated at the generator $\alpha$ of $F(\alpha)$ equals $x$, i.e., \[ \phi(\alpha) = x. \]
IntermediateField.fintypeOfAlgHomAdjoinIntegral definition
(h : IsIntegral F α) : Fintype (F⟮α⟯ →ₐ[F] K)
Full source 
/-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/
noncomputable def fintypeOfAlgHomAdjoinIntegral (h : IsIntegral F α) : Fintype (F⟮α⟯F⟮α⟯ →ₐ[F] K) :=
  PowerBasis.AlgHom.fintype (adjoin.powerBasis h)
Finiteness of algebra homomorphisms from \( F(\alpha) \) to \( K \) for integral \( \alpha \)
Informal description
Given a field extension \( E \) of \( F \) and an element \( \alpha \in E \) that is integral over \( F \), the set of \( F \)-algebra homomorphisms from the field \( F(\alpha) \) to another field \( K \) is finite.
IntermediateField.card_algHom_adjoin_integral theorem
(h : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : (minpoly F α).Splits (algebraMap F K)) : @Fintype.card (F⟮α⟯ →ₐ[F] K) (fintypeOfAlgHomAdjoinIntegral F h) = (minpoly F α).natDegree
Full source 
theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F K)) :
    @Fintype.card (F⟮α⟯F⟮α⟯ →ₐ[F] K) (fintypeOfAlgHomAdjoinIntegral F h) = (minpoly F α).natDegree := by
  rw [AlgHom.card_of_powerBasis] <;>
    simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]
  exact h_sep
Number of $F$-algebra homomorphisms $F(\alpha) \to K$ equals degree of minimal polynomial when $\alpha$ is integral and separable and $p$ splits in $K$
Informal description
Let $F$ be a field and $E$ a field extension of $F$. Given an element $\alpha \in E$ that is integral and separable over $F$, and another field extension $K$ of $F$ such that the minimal polynomial $p$ of $\alpha$ over $F$ splits completely in $K$, the number of $F$-algebra homomorphisms from $F(\alpha)$ to $K$ is equal to the degree of $p$.
Polynomial.irreducible_comp theorem
{f g : K[X]} (hfm : f.Monic) (hgm : g.Monic) (hf : Irreducible f) (hg : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = f), Irreducible (g.map (algebraMap _ _) - C (AdjoinSimple.gen K x))) : Irreducible (f.comp g)
Full source 
/-- Let `f, g` be monic polynomials over `K`. If `f` is irreducible, and `g(x) - α` is irreducible
in `K⟮α⟯` with `α` a root of `f`, then `f(g(x))` is irreducible. -/
theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g.Monic)
    (hf : Irreducible f)
    (hg : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = f),
      Irreducible (g.map (algebraMap _ _) - C (AdjoinSimple.gen K x))) :
    Irreducible (f.comp g) := by
  have hf' : natDegreenatDegree f ≠ 0 :=
    fun e ↦ not_irreducible_C (f.coeff 0) (eq_C_of_natDegree_eq_zero e ▸ hf)
  have hg' : natDegreenatDegree g ≠ 0 := by
    have := Fact.mk hf
    intro e
    apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
    -- Needed to specialize `map_sub` to avoid a timeout https://github.com/leanprover-community/mathlib4/pull/8386
    rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
    apply hg (AdjoinRoot f)
    rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
  have H₁ : f.comp g ≠ 0 := fun h ↦ by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h
  have H₂ : ¬ IsUnit (f.comp g) := fun h ↦
    by simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h
  have ⟨p, hp₁, hp₂⟩ := WfDvdMonoid.exists_irreducible_factor H₂ H₁
  suffices natDegree p = natDegree f * natDegree g from (associated_of_dvd_of_natDegree_le hp₂ H₁
    (this.trans natDegree_comp.symm).ge).irreducible hp₁
  have := Fact.mk hp₁
  let Kx := AdjoinRoot p
  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finite
  have key₁ : f = minpoly K (aeval (root p) g) := by
    refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
    rw [← aeval_comp]
    exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)
  have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f := by
    rw [adjoin.finrank, ← key₁]
    exact IsIntegral.of_finite _ _
  have key₂ : g.map (algebraMap _ _) - C (AdjoinSimple.gen K (aeval (root p) g)) =
      minpoly K⟮aeval (root p) g⟯ (root p) :=
    minpoly.eq_of_irreducible_of_monic (hg _ _ key₁.symm) (by simp [AdjoinSimple.gen])
      (Monic.sub_of_left (hgm.map _) (degree_lt_degree (by simpa [Nat.pos_iff_ne_zero] using hg')))
  have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g := by
    trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
    · have : K⟮aeval (root p) g⟯K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
      rw [← finrank_top', ← this, adjoin.finrank]
      exact IsIntegral.of_finite _ _
    · simp [← key₂]
  have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx
  rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Irreducibility of Composition of Monic Polynomials under Root Adjoin Condition
Informal description
Let $K$ be a field and $f, g \in K[X]$ be monic polynomials. If $f$ is irreducible and for every field extension $E$ of $K$ and every root $\alpha$ of $f$ in $E$ (with $\minpoly_K(\alpha) = f$), the polynomial $g(X) - \alpha$ is irreducible in $K(\alpha)[X]$, then the composition $f \circ g$ is irreducible in $K[X]$.
AdjoinRoot.algHomOfDvd definition
{p q : K[X]} (hpq : q ∣ p) : AdjoinRoot p →ₐ[K] AdjoinRoot q
Full source 
/-- The canonical algebraic homomorphism from `AdjoinRoot p` to `AdjoinRoot q`, where
  the polynomial `q : K[X]` divides `p`. -/
noncomputable def algHomOfDvd {p q : K[X]} (hpq : q ∣ p) :
    AdjoinRootAdjoinRoot p →ₐ[K] AdjoinRoot q :=
  (liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq]))
Canonical algebra homomorphism between adjoined roots of divisible polynomials
Informal description
Given polynomials $p, q \in K[X]$ where $q$ divides $p$, the function `algHomOfDvd` constructs the canonical $K$-algebra homomorphism from the ring `AdjoinRoot p` (which adjoins a root of $p$ to $K$) to the ring `AdjoinRoot q$ (which adjoins a root of $q$ to $K$). This homomorphism maps the adjoined root of $p$ to the adjoined root of $q$.
AdjoinRoot.coe_algHomOfDvd theorem
{p q : K[X]} (hpq : q ∣ p) : (algHomOfDvd hpq).toFun = liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq])
Full source 
theorem coe_algHomOfDvd {p q : K[X]} (hpq : q ∣ p) :
    (algHomOfDvd hpq).toFun = liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq]) :=
  rfl
Underlying Function of Algebra Homomorphism for Adjoined Roots of Divisible Polynomials
Informal description
For any polynomials $p, q \in K[X]$ such that $q$ divides $p$, the underlying function of the algebra homomorphism $\text{algHomOfDvd}\, hpq$ is equal to the lift of the homomorphism that maps the root of $p$ to the root of $q$. Specifically, if $q \mid p$, then \[ \text{algHomOfDvd}\, hpq = \text{liftHom}\, p\, (\text{root}\, q)\, \text{(proof)}. \]
AdjoinRoot.algHomOfDvd_apply_root theorem
{p q : K[X]} (hpq : q ∣ p) : algHomOfDvd hpq (root p) = root q
Full source 
/-- `algHomOfDvd` sends `AdjoinRoot.root p` to `AdjoinRoot.root q`. -/
theorem algHomOfDvd_apply_root {p q : K[X]} (hpq : q ∣ p) :
    algHomOfDvd hpq (root p) = root q := by
  rw [algHomOfDvd, liftHom_root]
Algebra homomorphism maps adjoined roots of divisible polynomials
Informal description
Given polynomials $p, q \in K[X]$ such that $q$ divides $p$, the algebra homomorphism $\text{algHomOfDvd}\, hpq$ maps the adjoined root of $p$ in $\text{AdjoinRoot}\, p$ to the adjoined root of $q$ in $\text{AdjoinRoot}\, q$. That is, \[ \text{algHomOfDvd}\, hpq (\text{root}\, p) = \text{root}\, q. \]
AdjoinRoot.algEquivOfEq definition
{p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : AdjoinRoot p ≃ₐ[K] AdjoinRoot q
Full source 
/-- The canonical algebraic equivalence between `AdjoinRoot p` and `AdjoinRoot q`, where
  the two polynomials `p q : K[X]` are equal. -/
noncomputable def algEquivOfEq {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    AdjoinRootAdjoinRoot p ≃ₐ[K] AdjoinRoot q :=
  ofAlgHom (algHomOfDvd (dvd_of_eq h_eq.symm)) (algHomOfDvd (dvd_of_eq h_eq))
    (PowerBasis.algHom_ext (powerBasis (h_eq ▸ hp))
      (by rw [algHomOfDvd, powerBasis_gen (h_eq ▸ hp), AlgHom.coe_comp, Function.comp_apply,
        algHomOfDvd, liftHom_root, liftHom_root, AlgHom.coe_id, id_eq]))
    (PowerBasis.algHom_ext (powerBasis hp)
      (by rw [algHomOfDvd, powerBasis_gen hp, AlgHom.coe_comp, Function.comp_apply, algHomOfDvd,
          liftHom_root, liftHom_root, AlgHom.coe_id, id_eq]))
Canonical algebra equivalence between adjoined roots of equal polynomials
Informal description
Given two nonzero polynomials $p, q \in K[X]$ that are equal ($p = q$), the function `algEquivOfEq` constructs a canonical $K$-algebra equivalence between the rings `AdjoinRoot p` and `AdjoinRoot q`, which adjoin roots of $p$ and $q$ to $K$ respectively. This equivalence maps the adjoined root of $p$ to the adjoined root of $q$.
AdjoinRoot.coe_algEquivOfEq theorem
{p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : (algEquivOfEq hp h_eq).toFun = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self])
Full source 
theorem coe_algEquivOfEq {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    (algEquivOfEq hp h_eq).toFun = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self]) :=
  rfl
Underlying function of algebra equivalence between adjoined roots of equal polynomials is the lifting homomorphism
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. Then the underlying function of the algebra equivalence $\text{algEquivOfEq}$ between $\text{AdjoinRoot}\, p$ and $\text{AdjoinRoot}\, q$ is equal to the algebra homomorphism $\text{liftHom}\, p\, (\text{root}\, q)$, where the proof that $\text{root}\, q$ is a root of $p$ follows from the equality $p = q$ and the properties of evaluation and quotient maps.
AdjoinRoot.algEquivOfEq_toAlgHom theorem
{p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : (algEquivOfEq hp h_eq).toAlgHom = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self])
Full source 
theorem algEquivOfEq_toAlgHom {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    (algEquivOfEq hp h_eq).toAlgHom = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self]) :=
  rfl
Underlying homomorphism of algebra equivalence between adjoined roots of equal polynomials is the lifting homomorphism
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. Then the algebra homomorphism underlying the algebra equivalence $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ is equal to the lifting homomorphism that maps the root of $p$ to the root of $q$.
AdjoinRoot.algEquivOfEq_apply_root theorem
{p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) : algEquivOfEq hp h_eq (root p) = root q
Full source 
/-- `algEquivOfEq` sends `AdjoinRoot.root p` to `AdjoinRoot.root q`. -/
theorem algEquivOfEq_apply_root {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    algEquivOfEq hp h_eq (root p) = root q := by
  rw [← coe_algHom, algEquivOfEq_toAlgHom, liftHom_root]
Algebra Equivalence Maps Adjoined Roots of Equal Polynomials
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p = q$. Then the algebra equivalence $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e., \[ \text{algEquivOfEq}(p, q, h_p, h_{eq})(\text{root}\, p) = \text{root}\, q. \]
AdjoinRoot.algEquivOfAssociated definition
{p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) : AdjoinRoot p ≃ₐ[K] AdjoinRoot q
Full source 
/-- The canonical algebraic equivalence between `AdjoinRoot p` and `AdjoinRoot q`,
where the two polynomials `p q : K[X]` are associated. -/
noncomputable def algEquivOfAssociated {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    AdjoinRootAdjoinRoot p ≃ₐ[K] AdjoinRoot q :=
  ofAlgHom (liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd] ))
    (liftHom q (root p) (by simp only [aeval_eq, mk_eq_zero, hpq.dvd]))
    ( PowerBasis.algHom_ext (powerBasis (hpq.ne_zero_iff.mp hp))
        (by rw [powerBasis_gen (hpq.ne_zero_iff.mp hp), AlgHom.coe_comp, Function.comp_apply,
          liftHom_root, liftHom_root, AlgHom.coe_id, id_eq]))
    (PowerBasis.algHom_ext (powerBasis hp)
      (by rw [powerBasis_gen hp, AlgHom.coe_comp, Function.comp_apply, liftHom_root, liftHom_root,
          AlgHom.coe_id, id_eq]))
Algebra equivalence of adjoined roots for associated polynomials
Informal description
Given a field $K$ and two nonzero associated polynomials $p, q \in K[X]$, there exists a canonical algebra equivalence between the rings obtained by adjoining a root of $p$ and $q$ to $K$, i.e., $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ as $K$-algebras.
AdjoinRoot.coe_algEquivOfAssociated theorem
{p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) : (algEquivOfAssociated hp hpq).toFun = liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd])
Full source 
theorem coe_algEquivOfAssociated {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    (algEquivOfAssociated hp hpq).toFun =
      liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]) :=
  rfl
Underlying Function of Algebra Equivalence for Adjoined Roots of Associated Polynomials
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero associated polynomials. Then the underlying function of the algebra equivalence $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ is equal to the algebra homomorphism obtained by lifting the evaluation map at $\text{root}(q)$ (which satisfies $p(\text{root}(q)) = 0$ since $p$ and $q$ are associated).
AdjoinRoot.algEquivOfAssociated_toAlgHom theorem
{p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) : (algEquivOfAssociated hp hpq).toAlgHom = liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd])
Full source 
theorem algEquivOfAssociated_toAlgHom {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    (algEquivOfAssociated hp hpq).toAlgHom =
      liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]) :=
  rfl
Underlying homomorphism of algebra equivalence for adjoined roots of associated polynomials
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero associated polynomials. Then the algebra homomorphism underlying the algebra equivalence $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ is equal to the lift of the algebra homomorphism that maps the root of $p$ to the root of $q$. More precisely, if $\varphi: \text{AdjoinRoot}\, p \to \text{AdjoinRoot}\, q$ is the algebra equivalence induced by the association of $p$ and $q$, then $\varphi$ as an algebra homomorphism equals the unique lift of the map sending $\text{root}(p)$ to $\text{root}(q)$.
AdjoinRoot.algEquivOfAssociated_apply_root theorem
{p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) : algEquivOfAssociated hp hpq (root p) = root q
Full source 
/-- `algEquivOfAssociated` sends `AdjoinRoot.root p` to `AdjoinRoot.root q`. -/
theorem algEquivOfAssociated_apply_root {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    algEquivOfAssociated hp hpq (root p) = root q := by
  rw [← coe_algHom, algEquivOfAssociated_toAlgHom, liftHom_root]
Algebra Equivalence Maps Adjoined Roots of Associated Polynomials
Informal description
Let $K$ be a field and let $p, q \in K[X]$ be nonzero associated polynomials. Then the algebra equivalence $\text{AdjoinRoot}\, p \simeq \text{AdjoinRoot}\, q$ maps the adjoined root of $p$ to the adjoined root of $q$, i.e., \[ \text{algEquivOfAssociated}(p, q)(\text{root}(p)) = \text{root}(q). \]
minpoly.algEquiv definition
{x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : K⟮x⟯ ≃ₐ[K] K⟮y⟯
Full source 
/-- The canonical `algEquiv` between `K⟮x⟯`and `K⟮y⟯`, sending `x` to `y`, where `x` and `y` have
  the same minimal polynomial over `K`. -/
noncomputable def algEquiv {x y : L} (hx : IsAlgebraic K x)
    (h_mp : minpoly K x = minpoly K y) : K⟮x⟯K⟮x⟯ ≃ₐ[K] K⟮y⟯ := by
  have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
  exact AlgEquiv.trans (adjoinRootEquivAdjoin K hx.isIntegral).symm
    (AlgEquiv.trans (AdjoinRoot.algEquivOfEq (ne_zero hx.isIntegral) h_mp)
      (adjoinRootEquivAdjoin K hy.isIntegral))
Isomorphism between field extensions generated by elements with the same minimal polynomial
Informal description
Given a field extension \( L \) of \( K \) and elements \( x, y \in L \) that are algebraic over \( K \) with the same minimal polynomial over \( K \), there exists a \( K \)-algebra isomorphism between the field extensions \( K(x) \) and \( K(y) \). This isomorphism maps the generator \( x \) of \( K(x) \) to the generator \( y \) of \( K(y) \).
minpoly.algEquiv_apply theorem
{x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y
Full source 
/-- `minpoly.algEquiv` sends the generator of `K⟮x⟯` to the generator of `K⟮y⟯`. -/
theorem algEquiv_apply {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
    algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y := by
  have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
  rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral,
    symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_apply_root,
    adjoinRootEquivAdjoin_apply_root K hy.isIntegral]
Isomorphism Maps Generator to Generator in Field Extensions with Same Minimal Polynomial
Informal description
Given a field extension \( L \) of \( K \) and elements \( x, y \in L \) that are algebraic over \( K \) with the same minimal polynomial over \( K \), the \( K \)-algebra isomorphism \( \varphi : K(x) \to K(y) \) maps the generator \( x \) of \( K(x) \) to the generator \( y \) of \( K(y) \), i.e., \[ \varphi(x) = y. \]
PowerBasis.equivAdjoinSimple definition
(pb : PowerBasis K L) : K⟮pb.gen⟯ ≃ₐ[K] L
Full source 
/-- `pb.equivAdjoinSimple` is the equivalence between `K⟮pb.gen⟯` and `L` itself. -/
noncomputable def equivAdjoinSimple (pb : PowerBasis K L) : K⟮pb.gen⟯K⟮pb.gen⟯ ≃ₐ[K] L :=
  (adjoin.powerBasis pb.isIntegral_gen).equivOfMinpoly pb <| by
    rw [adjoin.powerBasis_gen, minpoly_gen]
Algebra isomorphism between K(pb.gen) and L via power basis
Informal description
Given a power basis `pb` for the field extension `L` over `K`, the equivalence `pb.equivAdjoinSimple` is an algebra isomorphism between the simple field extension `K⟮pb.gen⟯` (the field obtained by adjoining the generator of the power basis to `K`) and `L` itself. This isomorphism preserves the `K`-algebra structure.
PowerBasis.equivAdjoinSimple_aeval theorem
(pb : PowerBasis K L) (f : K[X]) : pb.equivAdjoinSimple (aeval (AdjoinSimple.gen K pb.gen) f) = aeval pb.gen f
Full source 
@[simp]
theorem equivAdjoinSimple_aeval (pb : PowerBasis K L) (f : K[X]) :
    pb.equivAdjoinSimple (aeval (AdjoinSimple.gen K pb.gen) f) = aeval pb.gen f :=
  equivOfMinpoly_aeval _ pb _ f
Polynomial Evaluation under Power Basis Isomorphism: $\mathrm{pb.equivAdjoinSimple}(\mathrm{aeval}_{K(\mathrm{pb.gen})}(f)) = \mathrm{aeval}_{\mathrm{pb.gen}}(f)$
Informal description
Let $L$ be a field extension of $K$ with a power basis $\mathrm{pb}$ over $K$. For any polynomial $f \in K[X]$, the algebra isomorphism $\mathrm{pb.equivAdjoinSimple}$ between $K(\mathrm{pb.gen})$ and $L$ satisfies \[ \mathrm{pb.equivAdjoinSimple}\left(\mathrm{aeval}_{K(\mathrm{pb.gen})}(f)\right) = \mathrm{aeval}_{\mathrm{pb.gen}}(f), \] where $\mathrm{aeval}_{K(\mathrm{pb.gen})}(f)$ denotes the evaluation of $f$ at the generator of $K(\mathrm{pb.gen})$, and $\mathrm{aeval}_{\mathrm{pb.gen}}(f)$ denotes the evaluation of $f$ at $\mathrm{pb.gen}$ in $L$.
PowerBasis.equivAdjoinSimple_gen theorem
(pb : PowerBasis K L) : pb.equivAdjoinSimple (AdjoinSimple.gen K pb.gen) = pb.gen
Full source 
@[simp]
theorem equivAdjoinSimple_gen (pb : PowerBasis K L) :
    pb.equivAdjoinSimple (AdjoinSimple.gen K pb.gen) = pb.gen :=
  equivOfMinpoly_gen _ pb _
Generator Preservation in Power Basis Algebra Isomorphism
Informal description
Given a power basis `pb` for the field extension `L` over `K`, the algebra isomorphism `pb.equivAdjoinSimple` maps the generator of the simple field extension `K⟮pb.gen⟯` to the generator `pb.gen` of the power basis. In other words, if we denote the generator of `K⟮pb.gen⟯` by `α`, then the isomorphism satisfies: \[ \mathrm{pb.equivAdjoinSimple}(\alpha) = \mathrm{pb.gen}. \]
PowerBasis.equivAdjoinSimple_symm_aeval theorem
(pb : PowerBasis K L) (f : K[X]) : pb.equivAdjoinSimple.symm (aeval pb.gen f) = aeval (AdjoinSimple.gen K pb.gen) f
Full source 
@[simp]
theorem equivAdjoinSimple_symm_aeval (pb : PowerBasis K L) (f : K[X]) :
    pb.equivAdjoinSimple.symm (aeval pb.gen f) = aeval (AdjoinSimple.gen K pb.gen) f := by
  rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]
Polynomial Evaluation under Inverse of Power Basis Algebra Isomorphism
Informal description
Let $L$ be a field extension of $K$ with a power basis $\mathrm{pb}$, and let $f \in K[X]$ be a polynomial. Then the inverse of the algebra isomorphism $\mathrm{pb.equivAdjoinSimple}$ satisfies \[ \mathrm{pb.equivAdjoinSimple}^{-1}(\mathrm{aeval}_{\mathrm{pb.gen}}(f)) = \mathrm{aeval}_{\mathrm{AdjoinSimple.gen\,K\,pb.gen}}(f), \] where $\mathrm{AdjoinSimple.gen\,K\,pb.gen}$ is the generator of the field $K(\mathrm{pb.gen})$.
PowerBasis.equivAdjoinSimple_symm_gen theorem
(pb : PowerBasis K L) : pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen
Full source 
@[simp]
theorem equivAdjoinSimple_symm_gen (pb : PowerBasis K L) :
    pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen := by
  rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]
Inverse of Power Basis Isomorphism Maps Generator to Adjoined Generator
Informal description
Let $K$ be a field and $L$ a field extension of $K$ with a power basis $\mathrm{pb}$. The inverse of the algebra isomorphism $\mathrm{pb.equivAdjoinSimple}$ maps the generator $\mathrm{pb.gen}$ of $L$ to the generator $\mathrm{AdjoinSimple.gen}\, K\, \mathrm{pb.gen}$ of the simple extension field $K(\mathrm{pb.gen})$.
IntermediateField.lift_cardinalMk_adjoin_le theorem
{E : Type v} [Field E] [Algebra F E] (s : Set E) : Cardinal.lift.{u} #(adjoin F s) ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} #s ⊔ ℵ₀
Full source 
theorem lift_cardinalMk_adjoin_le {E : Type v} [Field E] [Algebra F E] (s : Set E) :
    Cardinal.lift.{u} #(adjoin F s) ≤ Cardinal.liftCardinal.lift.{v} #F ⊔ Cardinal.lift.{u} #sCardinal.lift.{v} #F ⊔ Cardinal.lift.{u} #s ⊔ ℵ₀ := by
  rw [show ↥(adjoin F s) = (adjoin F s).toSubfield from rfl, adjoin_toSubfield]
  apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans
  rw [lift_max, sup_le_iff, lift_aleph0]
  refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩
  simp_rw [lift_max, lift_aleph0, sup_assoc]
  exact sup_le_sup_right mk_range_le_lift _
Cardinality Bound for Field Adjoin: $\text{lift}_u(\#F(s)) \leq \text{lift}_v(\#F) \sqcup \text{lift}_u(\#s) \sqcup \aleph_0$
Informal description
For a field extension $E$ of $F$ and a subset $s \subseteq E$, the cardinality of the field $F(s)$ adjoined with $s$ satisfies the inequality: $$\text{lift}_u(\#F(s)) \leq \text{lift}_v(\#F) \sqcup \text{lift}_u(\#s) \sqcup \aleph_0$$ where $\text{lift}_u$ and $\text{lift}_v$ denote cardinal lifts to appropriate universes, and $\sqcup$ denotes the supremum operation on cardinals.
IntermediateField.cardinalMk_adjoin_le theorem
{E : Type u} [Field E] [Algebra F E] (s : Set E) : #(adjoin F s) ≤ #F ⊔ #s ⊔ ℵ₀
Full source 
theorem cardinalMk_adjoin_le {E : Type u} [Field E] [Algebra F E] (s : Set E) :
    #(adjoin F s) ≤ #F#F ⊔ #s#F ⊔ #s ⊔ ℵ₀ := by
  simpa using lift_cardinalMk_adjoin_le F s
Cardinality Bound for Field Adjoin: $\#F(s) \leq \max(\#F, \#s, \aleph_0)$
Informal description
For a field extension $E$ of $F$ and a subset $s \subseteq E$, the cardinality of the field $F(s)$ obtained by adjoining $s$ to $F$ satisfies the inequality: $$\#F(s) \leq \max(\#F, \#s, \aleph_0)$$ where $\#F(s)$ denotes the cardinality of $F(s)$, $\#F$ and $\#s$ denote the cardinalities of $F$ and $s$ respectively, and $\aleph_0$ is the first infinite cardinal.