Mathlib.RingTheory.Adjoin.Field

AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly definition

{R : Type*} [CommRing R] [Algebra F R] (x : R) : Algebra.adjoin F ({ x } : Set R) ≃ₐ[F] AdjoinRoot (minpoly F x)

Full source

/-- If `p` is the minimal polynomial of `a` over `F` then `F[a] ≃ₐ[F] F[x]/(p)` -/
def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly {R : Type*} [CommRing R] [Algebra F R] (x : R) :
    Algebra.adjoinAlgebra.adjoin F ({x} : Set R) ≃ₐ[F] AdjoinRoot (minpoly F x) :=
  AlgEquiv.symm <| AlgEquiv.ofBijective (Minpoly.toAdjoin F x) <| by
    refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
    obtain ⟨P, rfl⟩ := mk_surjective P₁
    refine AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)
    rwa [Minpoly.toAdjoin_apply', liftHom_mk, ← Subalgebra.coe_eq_zero, aeval_subalgebra_coe] at hP₁

Isomorphism between generated subalgebra and adjoined root of minimal polynomial

Informal description

Given a commutative ring $R$ with an $F$-algebra structure and an element $x \in R$, there is an algebra isomorphism between the $F$-algebra generated by $\{x\}$ in $R$ and the quotient ring $F[X]/(\text{minpoly}_F x)$, where $\text{minpoly}_F x$ is the minimal polynomial of $x$ over $F$.

Algebra.adjoin.liftSingleton definition

 {S T : Type*} [CommRing S] [CommRing T] [Algebra F S] [Algebra F T] (x : S) (y : T) (h : aeval y (minpoly F x) = 0) :
  Algebra.adjoin F { x } →ₐ[F] T

Full source

/-- Produce an algebra homomorphism `Adjoin R {x} →ₐ[R] T` sending `x` to
a root of `x`'s minimal polynomial in `T`. -/
noncomputable def Algebra.adjoin.liftSingleton {S T : Type*}
    [CommRing S] [CommRing T] [Algebra F S] [Algebra F T]
    (x : S) (y : T) (h : aeval y (minpoly F x) = 0) :
    Algebra.adjoinAlgebra.adjoin F {x} →ₐ[F] T :=
  (AdjoinRoot.liftHom _ y h).comp (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x).toAlgHom

Lifting of algebra homomorphism from generated subalgebra to target algebra via minimal polynomial root

Informal description

Given a commutative ring $S$ with an $F$-algebra structure, a commutative ring $T$ with an $F$-algebra structure, an element $x \in S$, and an element $y \in T$ such that $y$ is a root of the minimal polynomial of $x$ over $F$ (i.e., $\text{aeval}_T y (\text{minpoly}_F x) = 0$), there exists an $F$-algebra homomorphism from the $F$-algebra generated by $\{x\}$ in $S$ to $T$ that maps $x$ to $y$.

Polynomial.lift_of_splits theorem

 {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (s : Finset K) :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (Algebra.adjoin F (s : Set K) →ₐ[F] L)

Full source

/-- If `K` and `L` are field extensions of `F` and we have `s : Finset K` such that
the minimal polynomial of each `x ∈ s` splits in `L` then `Algebra.adjoin F s` embeds in `L`. -/
theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K]
    [Algebra F L] (s : Finset K) : (∀ x ∈ s, IsIntegral F x ∧
      Splits (algebraMap F L) (minpoly F x)) → Nonempty (Algebra.adjoinAlgebra.adjoin F (s : Set K) →ₐ[F] L) := by
  classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : (minpoly Ks a).Splits (algebraMap Ks L) := by
      refine splits_of_splits_of_dvd _ ((minpoly.monic H1).map (algebraMap F Ks)).ne_zero
        ((splits_map_iff _ _).2 ?_) (minpoly.dvd _ _ ?_)
      · rw [← IsScalarTower.algebraMap_eq]
        exact H2
      · rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
    obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (minpoly.degree_pos H5).ne'
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩

Embedding of Adjoint Algebra into Field Extension via Split Minimal Polynomials

Informal description

Let $F$, $K$, and $L$ be fields with $K$ and $L$ being field extensions of $F$. Given a finite set $s \subseteq K$ such that for every $x \in s$, $x$ is integral over $F$ and the minimal polynomial of $x$ over $F$ splits in $L$ via the algebra map $F \to L$, then there exists an $F$-algebra homomorphism from the $F$-algebra generated by $s$ in $K$ to $L$.

IsIntegral.mem_range_algHom_of_minpoly_splits theorem

(int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x)) (f : K →ₐ[R] L) : x ∈ f.range

Full source

theorem IsIntegral.mem_range_algHom_of_minpoly_splits
    (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x)) (f : K →ₐ[R] L) :
    x ∈ f.range :=
  show x ∈ Set.range f from Set.image_subset_range _ ((minpoly R x).rootSet K) <| by
    rw [image_rootSet h f, mem_rootSet']
    exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

Integral elements with split minimal polynomial are in the range of algebra homomorphisms

Informal description

Let $R$ be a commutative ring and $K$, $L$ be $R$-algebras. For an element $x \in K$ that is integral over $R$, if the minimal polynomial of $x$ over $R$ splits in $K$ via the algebra map $\text{algebraMap}\ R\ K$, then for any $R$-algebra homomorphism $f: K \to L$, the element $x$ lies in the range of $f$.

IsIntegral.mem_range_algebraMap_of_minpoly_splits theorem

 [Algebra K L] [IsScalarTower R K L] (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x)) :
  x ∈ (algebraMap K L).range

Full source

theorem IsIntegral.mem_range_algebraMap_of_minpoly_splits [Algebra K L] [IsScalarTower R K L]
    (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x)) :
    x ∈ (algebraMap K L).range :=
  int.mem_range_algHom_of_minpoly_splits h (IsScalarTower.toAlgHom R K L)

Integral elements with split minimal polynomial are in the range of the algebra map between field extensions

Informal description

Let $R$ be a commutative ring and $K$, $L$ be field extensions of $R$ with $K \subseteq L$ (via an algebra map). For an element $x \in L$ that is integral over $R$, if the minimal polynomial of $x$ over $R$ splits in $K$ via the algebra map $\text{algebraMap}\ R\ K$, then $x$ lies in the range of the algebra map $\text{algebraMap}\ K\ L$.

minpoly_neg_splits theorem

[Algebra K L] {x : L} (g : (minpoly K x).Splits (algebraMap K L)) : (minpoly K (-x)).Splits (algebraMap K L)

Full source

theorem minpoly_neg_splits [Algebra K L] {x : L} (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (-x)).Splits (algebraMap K L) := by
  rw [minpoly.neg]
  apply splits_mul _ _ g.comp_neg_X
  simpa only [map_pow, map_neg, map_one] using
    splits_C (algebraMap K L) ((-1) ^ (minpoly K x).natDegree)

Splitting of Minimal Polynomial under Negation in Field Extension

Informal description

Let $K$ and $L$ be fields with $L$ an extension of $K$, and let $x \in L$. If the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra map $\text{algebraMap}\ K\ L$, then the minimal polynomial of $-x$ over $K$ also splits in $L$ via $\text{algebraMap}\ K\ L$.

minpoly_add_algebraMap_splits theorem

 [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
  (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L)

Full source

theorem minpoly_add_algebraMap_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L) := by
  simpa [minpoly.add_algebraMap] using g.comp_X_sub_C r

Splitting of Minimal Polynomial under Translation by Scalar in Field Extension

Informal description

Let $K$ and $L$ be field extensions of a field $R$ with $[K : R] < \infty$, and let $x \in L$ be integral over $R$. Suppose the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra map $\text{algebraMap}\ K\ L$. Then for any $r \in K$, the minimal polynomial of $x + \text{algebraMap}\ K\ L\ r$ over $K$ also splits in $L$ via $\text{algebraMap}\ K\ L$.

minpoly_sub_algebraMap_splits theorem

 [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
  (minpoly K (x - algebraMap K L r)).Splits (algebraMap K L)

Full source

theorem minpoly_sub_algebraMap_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (x - algebraMap K L r)).Splits (algebraMap K L) := by
  simpa only [sub_eq_add_neg, map_neg] using minpoly_add_algebraMap_splits (-r) g

Splitting of Minimal Polynomial under Translation by Scalar in Field Extension (Subtractive Form)

Informal description

Let $K$ and $L$ be field extensions of a base field with $[K : R] < \infty$, and let $x \in L$ be integral over $R$. Suppose the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra homomorphism $\text{algebraMap}\ K\ L$. Then for any $r \in K$, the minimal polynomial of $x - \text{algebraMap}\ K\ L\ r$ over $K$ also splits in $L$ via $\text{algebraMap}\ K\ L$.

minpoly_algebraMap_add_splits theorem

 [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
  (minpoly K (algebraMap K L r + x)).Splits (algebraMap K L)

Full source

theorem minpoly_algebraMap_add_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (algebraMap K L r + x)).Splits (algebraMap K L) := by
  simpa only [add_comm] using minpoly_add_algebraMap_splits r g

Splitting of Minimal Polynomial under Translation by Scalar in Field Extension (Additive Form)

Informal description

Let $K$ and $L$ be field extensions of a field $R$ with $[K : R] < \infty$, and let $x \in L$ be integral over $R$. Suppose the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra map $\text{algebraMap}\ K\ L$. Then for any $r \in K$, the minimal polynomial of $\text{algebraMap}\ K\ L\ r + x$ over $K$ also splits in $L$ via $\text{algebraMap}\ K\ L$.

minpoly_algebraMap_sub_splits theorem

 [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
  (minpoly K (algebraMap K L r - x)).Splits (algebraMap K L)

Full source

theorem minpoly_algebraMap_sub_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (algebraMap K L r - x)).Splits (algebraMap K L) := by
  simpa only [neg_sub] using minpoly_neg_splits (minpoly_sub_algebraMap_splits r g)

Splitting of Minimal Polynomial under Scalar Translation (Subtractive Form) in Field Extension

Informal description

Let $K$ and $L$ be fields with $L$ an extension of $K$, and let $x \in L$. If the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra homomorphism $\text{algebraMap}\ K\ L$, then for any $r \in K$, the minimal polynomial of $\text{algebraMap}\ K\ L\ r - x$ over $K$ also splits in $L$ via $\text{algebraMap}\ K\ L$.

IsIntegral.minpoly_splits_tower_top' theorem

(int : IsIntegral R x) {f : K →+* L} (h : Splits (f.comp <| algebraMap R K) (minpoly R x)) : Splits f (minpoly K x)

Full source

/-- The `RingHom` version of `IsIntegral.minpoly_splits_tower_top`. -/
theorem IsIntegral.minpoly_splits_tower_top' (int : IsIntegral R x) {f : K →+* L}
    (h : Splits (f.comp <| algebraMap R K) (minpoly R x)) :
    Splits f (minpoly K x) :=
  splits_of_splits_of_dvd _ ((minpoly.monic int).map _).ne_zero
    ((splits_map_iff _ _).mpr h) (minpoly.dvd_map_of_isScalarTower R _ x)

Splitting of Minimal Polynomial in Tower of Field Extensions via Ring Homomorphism

Informal description

Let $R$, $K$, and $L$ be commutative rings with $R \subseteq K \subseteq L$ forming a tower of algebras. Let $x \in L$ be integral over $R$. If the minimal polynomial of $x$ over $R$ splits in $L$ via the composition $f \circ \text{algebraMap}\ R\ K$, where $f : K \to L$ is a ring homomorphism, then the minimal polynomial of $x$ over $K$ splits in $L$ via $f$.

IsIntegral.minpoly_splits_tower_top theorem

 [Algebra K L] [Algebra R L] [IsScalarTower R K L] (int : IsIntegral R x) (h : Splits (algebraMap R L) (minpoly R x)) :
  Splits (algebraMap K L) (minpoly K x)

Full source

theorem IsIntegral.minpoly_splits_tower_top [Algebra K L] [Algebra R L] [IsScalarTower R K L]
    (int : IsIntegral R x) (h : Splits (algebraMap R L) (minpoly R x)) :
    Splits (algebraMap K L) (minpoly K x) := by
  rw [IsScalarTower.algebraMap_eq R K L] at h
  exact int.minpoly_splits_tower_top' h

Splitting of Minimal Polynomial in Tower of Field Extensions via Algebra Maps

Informal description

Let $R$, $K$, and $L$ be commutative rings with $R \subseteq K \subseteq L$ forming a tower of algebras, where the algebra structures are compatible via `IsScalarTower`. Let $x \in L$ be integral over $R$. If the minimal polynomial of $x$ over $R$ splits in $L$ via the algebra map $\text{algebraMap}\ R\ L$, then the minimal polynomial of $x$ over $K$ splits in $L$ via the algebra map $\text{algebraMap}\ K\ L$.

Subalgebra.adjoin_rank_le theorem

 {F : Type*} (E : Type*) {K : Type*} [CommSemiring F] [StrongRankCondition F] [CommSemiring E] [StrongRankCondition E]
  [Semiring K] [SMul F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K) [Module.Free F L] :
  Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L

Full source

/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `[E[L] : E] ≤ [L : F]`. -/
lemma Subalgebra.adjoin_rank_le {F : Type*} (E : Type*) {K : Type*}
    [CommSemiring F] [StrongRankCondition F] [CommSemiring E] [StrongRankCondition E] [Semiring K]
    [SMul F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K]
    (L : Subalgebra F K) [Module.Free F L] :
    Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L := by
  rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
  exact rank_span_le _ |>.trans Cardinal.mk_range_le

Rank Inequality for Adjoined Subalgebra: $\operatorname{rank}_E(E[L]) \leq \operatorname{rank}_F L$

Informal description

Let $F$, $E$, and $K$ be commutative semirings with $F$ and $E$ satisfying the strong rank condition. Suppose $K$ is a semiring equipped with compatible algebra structures over $F$ and $E$ (via `IsScalarTower F E K`). Let $L$ be a free $F$-subalgebra of $K$. Then the rank of the $E$-algebra generated by $L$ in $K$ is bounded by the rank of $L$ as an $F$-module, i.e., \[ \operatorname{rank}_E \big(\operatorname{adjoin}_E (L \subseteq K)\big) \leq \operatorname{rank}_F L. \]

Main statements