Mathlib.FieldTheory.Extension

IntermediateField.Lifts structure

Full source

/-- Lifts `L → K` of `F → K` -/
structure Lifts where
  /-- The domain of a lift. -/
  carrier : IntermediateField F E
  /-- The lifted RingHom, expressed as an AlgHom. -/
  emb : carrier →ₐ[F] K

Field embedding extensions

Informal description

The structure `Lifts F E K` represents field embeddings from an intermediate field `E` to a field `K` that extend a given embedding from a subfield `F` to `K`. More precisely, it consists of pairs `(L, f)` where `L` is an intermediate field between `F` and `E`, and `f` is a field embedding from `L` to `K` that restricts to the given embedding on `F`.

IntermediateField.Lifts.instPartialOrder instance

: PartialOrder (Lifts F E K)

Full source

instance : PartialOrder (Lifts F E K) where
  le L₁ L₂ := ∃ h : L₁.carrier ≤ L₂.carrier, ∀ x, L₂.emb (inclusion h x) = L₁.emb x
  le_refl L := ⟨le_rfl, by simp⟩
  le_trans L₁ L₂ L₃ := by
    rintro ⟨h₁₂, h₁₂'⟩ ⟨h₂₃, h₂₃'⟩
    refine ⟨h₁₂.trans h₂₃, fun _ ↦ ?_⟩
    rw [← inclusion_inclusion h₁₂ h₂₃, h₂₃', h₁₂']
  le_antisymm := by
    rintro ⟨L₁, e₁⟩ ⟨L₂, e₂⟩ ⟨h₁₂, h₁₂'⟩ ⟨h₂₁, h₂₁'⟩
    obtain rfl : L₁ = L₂ := h₁₂.antisymm h₂₁
    congr
    exact AlgHom.ext h₂₁'

Partial Order on Field Embedding Extensions

Informal description

The set of field embedding extensions `Lifts F E K` forms a partial order, where the order is given by inclusion of intermediate fields and compatibility of the embeddings.

IntermediateField.Lifts.instOrderBot instance

: OrderBot (Lifts F E K)

Full source

noncomputable instance : OrderBot (Lifts F E K) where
  bot := ⟨⊥, (Algebra.ofId F K).comp (botEquiv F E)⟩
  bot_le L := ⟨bot_le, fun x ↦ by
    obtain ⟨x, rfl⟩ := (botEquiv F E).symm.surjective x
    simp_rw [AlgHom.comp_apply, AlgHom.coe_coe, AlgEquiv.apply_symm_apply]
    exact L.emb.commutes x⟩

Existence of Least Element in Field Embedding Extensions

Informal description

The set of field embedding extensions $\text{Lifts}(F, E, K)$ has a least element with respect to the partial order defined by inclusion of intermediate fields and compatibility of embeddings.

IntermediateField.Lifts.instInhabited instance

: Inhabited (Lifts F E K)

Full source

noncomputable instance : Inhabited (Lifts F E K) :=
  ⟨⊥⟩

Nonemptiness of Field Embedding Extensions

Informal description

The set of field embedding extensions $\text{Lifts}(F, E, K)$ is nonempty.

IntermediateField.Lifts.le_iff theorem

: L₁ ≤ L₂ ↔ ∃ h : L₁.carrier ≤ L₂.carrier, L₂.emb.comp (inclusion h) = L₁.emb

Full source

theorem le_iff : L₁ ≤ L₂ ↔
    ∃ h : L₁.carrier ≤ L₂.carrier, L₂.emb.comp (inclusion h) = L₁.emb := by
  simp_rw [AlgHom.ext_iff]; rfl

Characterization of Partial Order on Field Embedding Extensions

Informal description

For any two field embedding extensions $L_1$ and $L_2$ in $\text{Lifts}(F, E, K)$, the embedding $L_1$ is less than or equal to $L_2$ if and only if there exists an inclusion $h$ of the intermediate field $L_1.\text{carrier}$ into $L_2.\text{carrier}$ such that the composition of $L_2.\text{emb}$ with the inclusion map is equal to $L_1.\text{emb}$. In other words, $L_1 ≤ L_2$ holds precisely when: 1. The intermediate field of $L_1$ is contained in that of $L_2$, and 2. The embedding of $L_2$ restricts to the embedding of $L_1$ on their common subfield.

IntermediateField.Lifts.lt_iff_le_carrier_ne theorem

: L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

Full source

theorem lt_iff_le_carrier_ne : L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier := by
  rw [lt_iff_le_and_ne, and_congr_right]; intro h; simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]

Characterization of Strict Order in Field Embedding Extensions via Carrier Sets

Informal description

For any two field embedding extensions $ L_1 $ and $ L_2 $ in the partial order of `Lifts F E K`, the strict inequality $ L_1 < L_2 $ holds if and only if $ L_1 \leq L_2 $ and the underlying carrier sets of $ L_1 $ and $ L_2 $ are distinct.

IntermediateField.Lifts.lt_iff theorem

: L₁ < L₂ ↔ ∃ h : L₁.carrier < L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb

Full source

theorem lt_iff : L₁ < L₂ ↔
    ∃ h : L₁.carrier < L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb := by
  rw [lt_iff_le_carrier_ne, le_iff]
  exact ⟨fun h ↦ ⟨h.1.1.lt_of_ne h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1.ne⟩⟩

Characterization of Strict Order in Field Embedding Extensions via Strict Inclusion of Intermediate Fields

Informal description

For any two field embedding extensions $ L_1 $ and $ L_2 $ in the partial order of `Lifts(F, E, K)`, the strict inequality $ L_1 < L_2 $ holds if and only if there exists a strict inclusion $ h : L_1.\text{carrier} < L_2.\text{carrier} $ of intermediate fields such that the composition of $ L_2.\text{emb} $ with the inclusion map induced by $ h $ equals $ L_1.\text{emb} $. In other words, $ L_1 < L_2 $ if and only if: 1. The intermediate field of $ L_1 $ is strictly contained in that of $ L_2 $, and 2. The embedding of $ L_2 $ restricts to the embedding of $ L_1 $ on their common subfield.

IntermediateField.Lifts.le_of_carrier_le_iSup theorem

 {ι} {ρ : ι → Lifts F E K} {σ τ : Lifts F E K} (hσ : ∀ i, ρ i ≤ σ) (hτ : ∀ i, ρ i ≤ τ)
  (carrier_le : σ.carrier ≤ ⨆ i, (ρ i).carrier) : σ ≤ τ

Full source

theorem le_of_carrier_le_iSup {ι} {ρ : ι → Lifts F E K} {σ τ : Lifts F E K}
    (hσ : ∀ i, ρ i ≤ σ) (hτ : ∀ i, ρ i ≤ τ) (carrier_le : σ.carrier ≤ ⨆ i, (ρ i).carrier) :
    σ ≤ τ :=
  le_iff.mpr ⟨carrier_le.trans (iSup_le fun i ↦ (hτ i).1), algHom_ext_of_eq_adjoin _
      (carrier_le.antisymm (iSup_le fun i ↦ (hσ i).1)|>.trans <| iSup_eq_adjoin _ _) fun x hx ↦
    have ⟨i, hx⟩ := Set.mem_iUnion.mp hx
    ((hτ i).2 ⟨x, hx⟩).trans ((hσ i).2 ⟨x, hx⟩).symm⟩

Comparison of Field Embedding Extensions via Supremum of Intermediate Fields

Informal description

Let $F \subseteq E$ and $F \subseteq K$ be field extensions, and let $\{\rho_i : \iota \to \text{Lifts}(F, E, K)\}$ be a family of field embedding extensions. For any two extensions $\sigma, \tau \in \text{Lifts}(F, E, K)$, if: 1. $\rho_i \leq \sigma$ for all $i \in \iota$, 2. $\rho_i \leq \tau$ for all $i \in \iota$, and 3. The intermediate field of $\sigma$ is contained in the supremum of the intermediate fields of the $\rho_i$ (i.e., $\sigma.\text{carrier} \leq \bigsqcup_i \rho_i.\text{carrier}$), then $\sigma \leq \tau$.

IntermediateField.Lifts.IsExtendible definition

(σ : Lifts F E K) : Prop

Full source

/-- `σ : L →ₐ[F] K` is an extendible lift ("extendible pair" in [Isaacs1980]) if for every
intermediate field `M` that is finite-dimensional over `L`, `σ` extends to some `M →ₐ[F] K`.
In our definition we only require `M` to be finitely generated over `L`, which is equivalent
if the ambient field `E` is algebraic over `F` (which is the case in our main application).
We also allow the domain of the extension to be an intermediate field that properly contains `M`,
since one can always restrict the domain to `M`. -/
def IsExtendible (σ : Lifts F E K) : Prop :=
  ∀ S : Finset E, ∃ τ ≥ σ, (S : Set E) ⊆ τ.carrier

Extendible Field Embedding Extension

Informal description

A field embedding extension $\sigma \in \text{Lifts}(F, E, K)$ is called *extendible* if for every finite subset $S \subseteq E$, there exists an extension $\tau \geq \sigma$ in $\text{Lifts}(F, E, K)$ such that $S$ is contained in the intermediate field associated with $\tau$. In other words, $\sigma$ can be extended to a larger intermediate field that includes any given finite set of elements from $E$ while preserving the embedding structure.

IntermediateField.Lifts.union definition

: Lifts F E K

Full source

/-- The union of a chain of lifts. -/
noncomputable def union : Lifts F E K :=
  let t (i : ↑(insert ⊥ c)) := i.val.carrier
  have hc := hc.insert fun _ _ _ ↦ .inl bot_le
  have dir : Directed (· ≤ ·) t := hc.directedOn.directed_val.mono_comp _ fun _ _ h ↦ h.1
  ⟨iSup t, (Subalgebra.iSupLift (toSubalgebra <| t ·) dir (·.val.emb) (fun i j h ↦
    AlgHom.ext fun x ↦ (hc.total i.2 j.2).elim (fun hij ↦ (hij.snd x).symm) fun hji ↦ by
      rw [AlgHom.comp_apply, ← inclusion]
      dsimp only [coe_type_toSubalgebra]
      rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x])
    _ rfl).comp
      (Subalgebra.equivOfEq _ _ <| toSubalgebra_iSup_of_directed dir)⟩

Union of a chain of field embedding extensions

Informal description

The union of a chain of field embedding extensions in `Lifts F E K`, where each extension is a pair `(L, f)` with `L` an intermediate field between `F` and `E` and `f` an embedding of `L` into `K` extending the given embedding on `F`. The union is constructed by taking the supremum of the intermediate fields in the chain and lifting the embeddings compatibly.

IntermediateField.Lifts.le_union theorem

⦃σ : Lifts F E K⦄ (hσ : σ ∈ c) : σ ≤ union c hc

Full source

theorem le_union ⦃σ : Lifts F E K⦄ (hσ : σ ∈ c) : σ ≤ union c hc :=
  have hσ := Set.mem_insert_of_mem ⊥ hσ
  let t (i : ↑(insert ⊥ c)) := i.val.carrier
  ⟨le_iSup t ⟨σ, hσ⟩, fun x ↦ by
    dsimp only [union, AlgHom.comp_apply]
    exact Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)⟩

Field Embedding Extensions in a Chain are Bounded by Their Union

Informal description

For any field embedding extension $\sigma$ in a chain $c$ of extensions in $\text{Lifts}(F, E, K)$, $\sigma$ is less than or equal to the union of the chain $c$ with respect to the partial order on $\text{Lifts}(F, E, K)$.

IntermediateField.Lifts.carrier_union theorem

: (union c hc).carrier = ⨆ i : c, i.1.carrier

Full source

theorem carrier_union : (union c hc).carrier = ⨆ i : c, i.1.carrier :=
  le_antisymm (iSup_le <| by rintro ⟨i, rfl|hi⟩; exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]) <|
    iSup_le fun i ↦ le_iSup_of_le ⟨i, .inr i.2⟩ le_rfl

Union of Chain of Field Extensions Equals Supremum of Carriers

Informal description

For a chain $c$ of field embedding extensions in $\text{Lifts}(F, E, K)$, the carrier (intermediate field) of the union of the chain is equal to the supremum of the carriers of all elements in the chain. That is, if $\sigma = \text{union}\, c\, hc$ is the union of the chain, then $\sigma.\text{carrier} = \bigsqcup_{i \in c} i.1.\text{carrier}$.

IntermediateField.Lifts.exists_upper_bound theorem

(c : Set (Lifts F E K)) (hc : IsChain (· ≤ ·) c) : ∃ ub, ∀ a ∈ c, a ≤ ub

Full source

/-- A chain of lifts has an upper bound. -/
theorem exists_upper_bound (c : Set (Lifts F E K)) (hc : IsChain (· ≤ ·) c) :
    ∃ ub, ∀ a ∈ c, a ≤ ub := ⟨_, le_union c hc⟩

Existence of Upper Bound for Chain of Field Embedding Extensions

Informal description

For any chain $c$ of field embedding extensions in $\text{Lifts}(F, E, K)$, there exists an upper bound $ub$ such that every element $a \in c$ satisfies $a \leq ub$ with respect to the partial order on $\text{Lifts}(F, E, K)$.

IntermediateField.Lifts.union_isExtendible theorem

[alg : Algebra.IsAlgebraic F E] [Nonempty c] (hext : ∀ σ ∈ c, σ.IsExtendible) : (union c hc).IsExtendible

Full source

theorem union_isExtendible [alg : Algebra.IsAlgebraic F E]
    [Nonempty c] (hext : ∀ σ ∈ c, σ.IsExtendible) :
    (union c hc).IsExtendible := fun S ↦ by
  let Ω := adjoinadjoin F (S : Set E) →ₐ[F] K
  have ⟨ω, hω⟩ : ∃ ω : Ω, ∀ π : c, ∃ θ ≥ π.1, ⟨_, ω⟩ ≤ θ ∧ θ.carrier = π.1.1 ⊔ adjoin F S := by
    by_contra!; choose π hπ using this
    have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
    have ⟨π₀, hπ₀⟩ := hc.directed.finite_le π
    have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
    rw [← adjoin_le_iff] at hθ
    let θ₀ := θ.emb.comp (inclusion hθ)
    have := (hπ₀ θ₀).trans hθπ
    exact hπ θ₀ ⟨_, θ.emb.comp <| inclusion <| sup_le this.1 hθ⟩
      ⟨le_sup_left, this.2⟩ ⟨le_sup_right, fun _ ↦ rfl⟩ rfl
  choose θ ge hθ eq using hω
  have : IsChain (· ≤ ·) (Set.range θ) := by
    simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq
    rintro _ ⟨π₁, rfl⟩ _ ⟨π₂, rfl⟩ -
    wlog h : π₁ ≤ π₂ generalizing π₁ π₂
    · exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm
    refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
    · rw [eq, eq]; exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)
    rintro x (hx|hx)
    · change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
        (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
      rw [(ge π₁).2, (ge π₂).2, h.2]
    · change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
      rw [(hθ π₁).2, (hθ π₂).2]
  refine ⟨union _ this, le_of_carrier_le_iSup (fun π ↦ le_union c hc π.2)
    (fun π ↦ (ge π).trans <| le_union _ _ ⟨_, rfl⟩) (carrier_union _ _).le, ?_⟩
  simp_rw [carrier_union, iSup_range', eq]
  exact (subset_adjoin _ _).trans (SetLike.coe_subset_coe.mpr <|
    le_sup_right.trans <| le_iSup_of_le (Classical.arbitrary _) le_rfl)

Extendibility of Union of Chain of Field Embedding Extensions in Algebraic Field Extensions

Informal description

Let $F \subseteq E$ be an algebraic field extension, and let $c$ be a nonempty chain of field embedding extensions in $\text{Lifts}(F, E, K)$. If every embedding extension $\sigma \in c$ is extendible, then the union of the chain $c$ is also extendible.

IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset theorem

 [alg : Algebra.IsAlgebraic F E] (h : ∀ S : Finset E, ∃ σ : Lifts F E K, (S : Set E) ⊆ σ.carrier) : Nonempty (E →ₐ[F] K)

Full source

theorem nonempty_algHom_of_exist_lifts_finset [alg : Algebra.IsAlgebraic F E]
    (h : ∀ S : Finset E, ∃ σ : Lifts F E K, (S : Set E) ⊆ σ.carrier) :
    Nonempty (E →ₐ[F] K) := by
  have : (⊥ : Lifts F E K).IsExtendible := fun S ↦ have ⟨σ, hσ⟩ := h S; ⟨σ, bot_le, hσ⟩
  have ⟨ϕ, hϕ⟩ := zorn_le₀ {ϕ : Lifts F E K | ϕ.IsExtendible}
    fun c hext hc ↦ (isEmpty_or_nonempty c).elim
      (fun _ ↦ ⟨⊥, this, fun ϕ hϕ ↦ isEmptyElim (⟨ϕ, hϕ⟩ : c)⟩)
      fun _ ↦ ⟨_, union_isExtendible c hc hext, le_union c hc⟩
  suffices ϕ.carrier = ⊤ from ⟨ϕ.emb.comp <| ((equivOfEq this).trans topEquiv).symm⟩
  by_contra!
  obtain ⟨α, -, hα⟩ := SetLike.exists_of_lt this.lt_top
  let _ : Algebra ϕ.carrier K := ϕ.emb.toAlgebra
  let Λ := ϕ.carrier⟮α⟯ϕ.carrier⟮α⟯ →ₐ[ϕ.carrier] K
  have := finiteDimensional_adjoin (S := {α}) fun _ _ ↦ ((alg.tower_top ϕ.carrier).isIntegral).1 _
  let L (σ : Λ) : Lifts F E K := ⟨ϕ.carrier⟮α⟯.restrictScalars F, σ.restrictScalars F⟩
  have hL (σ : Λ) : ϕ < L σ := lt_iff.mpr
    ⟨by simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff],
      AlgHom.coe_ringHom_injective σ.comp_algebraMap⟩
  have ⟨(ϕ_ext : ϕ.IsExtendible), ϕ_max⟩ := maximal_iff_forall_gt.mp hϕ
  simp_rw [Set.mem_setOf, IsExtendible] at ϕ_max; push_neg at ϕ_max
  choose S hS using fun σ : Λ ↦ ϕ_max (hL σ)
  classical
  have ⟨θ, hθϕ, hθ⟩ := ϕ_ext ({α}{α} ∪ Finset.univ.biUnion S)
  simp_rw [Finset.coe_union, Set.union_subset_iff, Finset.coe_singleton, Set.singleton_subset_iff,
    Finset.coe_biUnion, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.iUnion_subset_iff] at hθ
  have : ϕ.carrier⟮α⟯.restrictScalars F ≤ θ.carrier := by
    rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]; exact ⟨hθϕ.1, hθ.1⟩
  exact hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)

Existence of Algebra Homomorphism for Algebraic Extensions with Finite Lifting Property

Informal description

Let $E/F$ be an algebraic field extension and $K$ another extension of $F$. Suppose that for every finite subset $S \subseteq E$, there exists a field embedding $\sigma \in \text{Lifts}(F,E,K)$ such that $S$ is contained in the intermediate field associated with $\sigma$. Then there exists at least one $F$-algebra homomorphism from $E$ to $K$.

IntermediateField.Lifts.exists_lift_of_splits' theorem

 (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carrier s) (h2 : (minpoly x.carrier s).Splits x.emb.toRingHom) :
  ∃ y, x ≤ y ∧ s ∈ y.carrier

Full source

/-- Given a lift `x` and an integral element `s : E` over `x.carrier` whose conjugates over
`x.carrier` are all in `K`, we can extend the lift to a lift whose carrier contains `s`. -/
theorem exists_lift_of_splits' (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carrier s)
    (h2 : (minpoly x.carrier s).Splits x.emb.toRingHom) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
  have I2 := (minpoly.degree_pos h1).ne'
  letI : Algebra x.carrier K := x.emb.toRingHom.toAlgebra
  let carrier := x.carrier⟮s⟯.restrictScalars F
  letI : Algebra x.carrier carrier := x.carrier⟮s⟯.toSubalgebra.algebra
  let φ : carrier →ₐ[x.carrier] K := ((algHomAdjoinIntegralEquiv x.carrier h1).symm
    ⟨rootOfSplits x.emb.toRingHom h2 I2, by
      rw [mem_aroots, and_iff_right (minpoly.ne_zero h1)]
      exact map_rootOfSplits x.emb.toRingHom h2 I2⟩)
  ⟨⟨carrier, (@algHomEquivSigma F x.carrier carrier K _ _ _ _ _ _ _ _
      (IsScalarTower.of_algebraMap_eq fun _ ↦ rfl)).symm ⟨x.emb, φ⟩⟩,
    ⟨fun z hz ↦ algebraMap_mem x.carrier⟮s⟯ ⟨z, hz⟩, φ.commutes⟩,
    mem_adjoin_simple_self x.carrier s⟩

Extension of Field Embeddings for Integral Elements with Split Minimal Polynomial

Informal description

Let $F \subseteq E$ be a field extension and $K$ another extension of $F$. Given a lift $x \in \text{Lifts}(F, E, K)$ (i.e., an intermediate field $x.\text{carrier}$ between $F$ and $E$ with an embedding $x.\text{emb} \colon x.\text{carrier} \to K$ over $F$) and an element $s \in E$ that is integral over $x.\text{carrier}$, if the minimal polynomial of $s$ over $x.\text{carrier}$ splits in $K$ via the embedding $x.\text{emb}$, then there exists a lift $y \in \text{Lifts}(F, E, K)$ extending $x$ (i.e., $x \leq y$) such that $s \in y.\text{carrier}$.

IntermediateField.Lifts.exists_lift_of_splits theorem

 (x : Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : (minpoly F s).Splits (algebraMap F K)) :
  ∃ y, x ≤ y ∧ s ∈ y.carrier

Full source

/-- Given an integral element `s : E` over `F` whose `F`-conjugates are all in `K`,
any lift can be extended to one whose carrier contains `s`. -/
theorem exists_lift_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s)
    (h2 : (minpoly F s).Splits (algebraMap F K)) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
  exists_lift_of_splits' x h1.tower_top <| h1.minpoly_splits_tower_top' <| by
    rwa [← x.emb.comp_algebraMap] at h2

Extension of Field Embeddings for Integral Elements with Split Minimal Polynomial over Base Field

Informal description

Let $F \subseteq E$ be a field extension and $K$ another extension of $F$. Given a field embedding $x \in \text{Lifts}(F, E, K)$ (where $x.\text{carrier}$ is an intermediate field between $F$ and $E$ with embedding $x.\text{emb} \colon x.\text{carrier} \to K$ over $F$) and an element $s \in E$ that is integral over $F$, if the minimal polynomial of $s$ over $F$ splits in $K$ via the canonical algebra map $\text{algebraMap} \colon F \to K$, then there exists an extension $y \in \text{Lifts}(F, E, K)$ such that $x \leq y$ (i.e., $y$ extends $x$) and $s \in y.\text{carrier}$.

IntermediateField.exists_algHom_adjoin_of_splits' theorem

: ∃ φ : adjoin L S →ₐ[F] K, φ.restrictDomain L = f

Full source

theorem exists_algHom_adjoin_of_splits' :
    ∃ φ : adjoin L S →ₐ[F] K, φ.restrictDomain L = f := by
  let L' := (IsScalarTower.toAlgHom F L E).fieldRange
  let f' : L' →ₐ[F] K := f.comp (AlgEquiv.ofInjectiveField _).symm.toAlgHom
  have := exists_algHom_adjoin_of_splits'' f' (S := S) fun s hs ↦ ?_
  · obtain ⟨φ, hφ⟩ := this; refine ⟨φ.comp <|
      inclusion (?_ : (adjoin L S).restrictScalars F ≤ (adjoin L' S).restrictScalars F), ?_⟩
    · simp_rw [← SetLike.coe_subset_coe, coe_restrictScalars, adjoin_subset_adjoin_iff]
      exact ⟨subset_adjoin_of_subset_left S (F := L'.toSubfield) le_rfl, subset_adjoin _ _⟩
    · ext x
      let y := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x
      refine Eq.trans congr($hφ y) ?_
      simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply, f']
      exact congr_arg f (AlgEquiv.symm_apply_apply _ _)
  letI : Algebra L L' := (AlgEquiv.ofInjectiveField _).toRingHom.toAlgebra
  have : IsScalarTower L L' E := IsScalarTower.of_algebraMap_eq' rfl
  refine ⟨(hK s hs).1.tower_top, (hK s hs).1.minpoly_splits_tower_top' ?_⟩
  convert (hK s hs).2
  ext
  simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply, f']
  exact congr_arg f (AlgEquiv.symm_apply_apply _ _)

Extension of Field Embeddings via Splitting Minimal Polynomials in Adjoined Fields

Informal description

Let $F$, $L$, $E$, and $K$ be fields with $L$ an intermediate field between $F$ and $E$, and $S$ a subset of $E$. Given an algebra homomorphism $f \colon L \to K$ over $F$ such that for every $s \in S$, the minimal polynomial of $s$ over $L$ splits in $K$ via $f$, there exists an algebra homomorphism $\varphi \colon F(S) \to K$ over $F$ extending $f$, where $F(S)$ denotes the field obtained by adjoining $S$ to $F$ in $E$.

IntermediateField.exists_algHom_of_adjoin_splits' theorem

(hS : adjoin L S = ⊤) : ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f

Full source

theorem exists_algHom_of_adjoin_splits' (hS : adjoin L S = ⊤) :
    ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits' f hK
  ⟨φ.comp (((equivOfEq hS).trans topEquiv).symm.toAlgHom.restrictScalars F), hφ⟩

Extension of Field Embeddings via Splitting Minimal Polynomials in Top Adjoined Field

Informal description

Let $F$, $L$, $E$, and $K$ be fields with $L$ an intermediate field between $F$ and $E$, and $S$ a subset of $E$ such that the adjunction of $S$ to $L$ equals $E$ (i.e., $L(S) = E$). Given an algebra homomorphism $f \colon L \to K$ over $F$ such that for every $s \in S$, the minimal polynomial of $s$ over $L$ splits in $K$ via $f$, there exists an algebra homomorphism $\varphi \colon E \to K$ over $F$ extending $f$.

IntermediateField.exists_algHom_of_splits' theorem

(hK : ∀ s : E, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) : ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f

Full source

theorem exists_algHom_of_splits' (hK : ∀ s : E, IsIntegralIsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) :
    ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f :=
  exists_algHom_of_adjoin_splits' f (fun x _ ↦ hK x) (adjoin_univ L E)

Extension of Field Embeddings via Splitting Minimal Polynomials

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given an $F$-algebra homomorphism $f \colon L \to K$ such that for every element $s \in E$, $s$ is integral over $L$ and the minimal polynomial of $s$ over $L$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism $\varphi \colon E \to K$ extending $f$.

IntermediateField.exists_algHom_adjoin_of_splits theorem

: ∃ φ : adjoin F S →ₐ[F] K, φ.comp (inclusion hL) = f

Full source

theorem exists_algHom_adjoin_of_splits : ∃ φ : adjoin F S →ₐ[F] K, φ.comp (inclusion hL) = f := by
  obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl
  refine ⟨φ.emb.comp (inclusion <| adjoin_le_iff.mpr fun s hs ↦ ?_), ?_⟩
  · rcases φ.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩
    exact (hφ h1).1 h2
  · ext; apply hfφ.2

Extension of Field Embeddings via Splitting Minimal Polynomials in Adjoined Field

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given a subset $S \subseteq E$ and an $F$-algebra homomorphism $f \colon L \to K$ such that for every $s \in S$, the minimal polynomial of $s$ over $F$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism $\varphi \colon F(S) \to K$ extending $f$, where $F(S)$ denotes the adjunction of $S$ to $F$ in $E$. Moreover, $\varphi$ satisfies $\varphi \circ \iota = f$, where $\iota \colon L \hookrightarrow F(S)$ is the inclusion map.

IntermediateField.nonempty_algHom_adjoin_of_splits theorem

: Nonempty (adjoin F S →ₐ[F] K)

Full source

theorem nonempty_algHom_adjoin_of_splits : Nonempty (adjoinadjoin F S →ₐ[F] K) :=
  have ⟨φ, _⟩ := exists_algHom_adjoin_of_splits hK (⊥ : Lifts F E K).emb bot_le; ⟨φ⟩

Existence of Field Embedding Extensions via Splitting Minimal Polynomials in Adjoined Field

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given a subset $S \subseteq E$ and an $F$-algebra homomorphism $f \colon L \to K$ such that for every $s \in S$, the minimal polynomial of $s$ over $F$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism from the adjunction $F(S)$ to $K$ extending $f$.

IntermediateField.exists_algHom_of_adjoin_splits theorem

: ∃ φ : E →ₐ[F] K, φ.comp L.val = f

Full source

theorem exists_algHom_of_adjoin_splits : ∃ φ : E →ₐ[F] K, φ.comp L.val = f :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK f (hS.symm ▸ le_top)
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

Extension of Field Embeddings via Splitting Minimal Polynomials in Adjoined Field

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given an $F$-algebra homomorphism $f \colon L \to K$ such that for every element $x$ in a generating set $S$ of $E$ over $L$, the minimal polynomial of $x$ over $L$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism $\varphi \colon E \to K$ extending $f$, i.e., satisfying $\varphi|_L = f$.

IntermediateField.nonempty_algHom_of_adjoin_splits theorem

: Nonempty (E →ₐ[F] K)

Full source

theorem nonempty_algHom_of_adjoin_splits : Nonempty (E →ₐ[F] K) :=
  have ⟨φ, _⟩ := exists_algHom_of_adjoin_splits hK (⊥ : Lifts F E K).emb hS; ⟨φ⟩

Existence of Field Embedding Extensions via Splitting Minimal Polynomials in Adjoined Field

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given an $F$-algebra homomorphism $f \colon L \to K$ such that for every element $x$ in a generating set $S$ of $E$ over $L$, the minimal polynomial of $x$ over $L$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism from $E$ to $K$ extending $f$.

IntermediateField.exists_algHom_adjoin_of_splits_of_aeval theorem

: ∃ φ : adjoin F S →ₐ[F] K, φ ⟨x, hx⟩ = y

Full source

theorem exists_algHom_adjoin_of_splits_of_aeval : ∃ φ : adjoin F S →ₐ[F] K, φ ⟨x, hx⟩ = y := by
  have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
  have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
  rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix
  obtain ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK ((algHomAdjoinIntegralEquiv F ix).symm
    ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)
  exact ⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <|
    algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩

Existence of Field Homomorphism Extending Adjoined Root Condition: $\varphi(x) = y$ for $\varphi : F(S) \to K$

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, $K$ another extension of $F$, and $S \subseteq E$ a subset. Given an element $x \in E$ with $x \in S$ (witnessed by $hx : x \in S$) and an element $y \in K$ such that $y$ is a root of the minimal polynomial of $x$ over $F$ when evaluated in $K$, there exists an $F$-algebra homomorphism $\varphi : F(S) \to K$ satisfying $\varphi(x) = y$. Here, $F(S)$ denotes the field obtained by adjoining $S$ to $F$ within $E$.

IntermediateField.exists_algHom_of_adjoin_splits_of_aeval theorem

: ∃ φ : E →ₐ[F] K, φ x = y

Full source

theorem exists_algHom_of_adjoin_splits_of_aeval : ∃ φ : E →ₐ[F] K, φ x = y :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits_of_aeval hK (hS ▸ mem_top) hy
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

Existence of Field Homomorphism Extending Root Condition: $\varphi(x) = y$ for $\varphi : E \to K$

Informal description

Let $F \subseteq E$ be a field extension, $K$ another extension of $F$, and $x \in E$ an element. If $y \in K$ is a root of the minimal polynomial of $x$ over $F$ (i.e., $\text{minpoly}_F(x)(y) = 0$), then there exists an $F$-algebra homomorphism $\varphi : E \to K$ such that $\varphi(x) = y$.

IntermediateField.exists_algHom_of_splits theorem

: ∃ φ : E →ₐ[F] K, φ.comp L.val = f

Full source

theorem exists_algHom_of_splits : ∃ φ : E →ₐ[F] K, φ.comp L.val = f :=
  exists_algHom_of_adjoin_splits (fun x _ ↦ hK' x) f (adjoin_univ F E)

Extension of Field Embeddings via Splitting Minimal Polynomials

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given an $F$-algebra homomorphism $f \colon L \to K$ such that for every element $x \in E$, the minimal polynomial of $x$ over $L$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism $\varphi \colon E \to K$ extending $f$, i.e., satisfying $\varphi|_L = f$.

IntermediateField.nonempty_algHom_of_splits theorem

: Nonempty (E →ₐ[F] K)

Full source

theorem nonempty_algHom_of_splits : Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_adjoin_splits (fun x _ ↦ hK' x) (adjoin_univ F E)

Existence of Field Embedding Extensions via Splitting Minimal Polynomials

Informal description

Let $F \subseteq L \subseteq E$ be a tower of field extensions, and let $K$ be another extension of $F$. Given an $F$-algebra homomorphism $f \colon L \to K$ such that for every element $x \in E$, the minimal polynomial of $x$ over $L$ splits in $K$ via $f$, there exists an $F$-algebra homomorphism from $E$ to $K$ extending $f$.

IntermediateField.exists_algHom_of_splits_of_aeval theorem

(hy : aeval y (minpoly F x) = 0) : ∃ φ : E →ₐ[F] K, φ x = y

Full source

theorem exists_algHom_of_splits_of_aeval (hy : aeval y (minpoly F x) = 0) :
    ∃ φ : E →ₐ[F] K, φ x = y :=
  exists_algHom_of_adjoin_splits_of_aeval (fun x _ ↦ hK' x) (adjoin_univ F E) hy

Existence of Field Homomorphism Extending Root Condition: $\varphi(x) = y$ for $\varphi : E \to K$

Informal description

Let $F \subseteq E$ be a field extension, $K$ another extension of $F$, and $x \in E$ an element. If $y \in K$ satisfies $\text{minpoly}_F(x)(y) = 0$ (i.e., $y$ is a root of the minimal polynomial of $x$ over $F$), then there exists an $F$-algebra homomorphism $\varphi \colon E \to K$ such that $\varphi(x) = y$.

Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits theorem

 {F K : Type*} (L : Type*) [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K]
  (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) [Algebra.IsAlgebraic F K] (x : K) :
  (Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L

Full source

/-- Let `K/F` be an algebraic extension of fields and `L` a field in which all the minimal
polynomial over `F` of elements of `K` splits. Then, for `x ∈ K`, the images of `x` by the
`F`-algebra morphisms from `K` to `L` are exactly the roots in `L` of the minimal polynomial
of `x` over `F`. -/
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (L : Type*)
    [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K]
    (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L))
    [Algebra.IsAlgebraic F K] (x : K) :
    (Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L := by
  ext a
  rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]
  refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
    (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩
  rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]

Image of Algebraic Elements under Field Homomorphisms Equals Root Set of Minimal Polynomial

Informal description

Let $F$, $K$, and $L$ be fields with $F$-algebra structures on $K$ and $L$. Suppose that for every $x \in K$, the minimal polynomial $\text{minpoly}_F(x)$ splits in $L$ via the algebra map $F \to L$, and that $K$ is algebraic over $F$. Then for any $x \in K$, the set of images $\{\psi(x) \mid \psi \colon K \to L \text{ is an } F\text{-algebra homomorphism}\}$ equals the set of roots in $L$ of $\text{minpoly}_F(x)$.

Reference