nonempty_algHom_of_exist_roots — Mathlib

English

If for every x in E there exists y in K such that the evaluation of the minimal polynomial of x at y is zero, then there exists a K-algebra homomorphism from E to K.

Русский

Если для каждого x в E существует y в K такой, что eвалюация минимального многочлена x в y равна нулю, то существует гомоморф по K из E в K.

LaTeX

$$$\\Bigl(\\forall x\\in E,\\; \\exists y\\in K,\\; aeval\\,y\\bigl(minpoly\\ F\\ x\\bigr)=0\\Bigr) \\Rightarrow \\exists \\varphi: E \\to_F K$$$

Lean4

theorem nonempty_algHom_of_exist_roots (h : ∀ x : E, ∃ y : K, aeval y (minpoly F x) = 0) : Nonempty (E →ₐ[F] K) :=
  by
  refine Lifts.nonempty_algHom_of_exist_lifts_finset fun S ↦ ⟨⟨adjoin F S, ?_⟩, subset_adjoin _ _⟩
  let p := (S.prod <| minpoly F).map (algebraMap F K)
  let K' := SplittingField p
  have splits s (hs : s ∈ S) : (minpoly F s).Splits (algebraMap F K') := by
    apply
      splits_of_splits_of_dvd _ (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ minpoly.ne_zero <| (alg.isIntegral).1 _)
        ((splits_map_iff _ _).mp <| SplittingField.splits p) (Finset.dvd_prod_of_mem _ hs)
  let K₀ := (⊥ : IntermediateField K K').restrictScalars F
  let FS := adjoin F (S : Set E)
  let Ω := FS →ₐ[F] K'
  have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
  let M (ω : Ω) := Subalgebra.toSubmodule (K₀.comap ω).toSubalgebra
  have : ⋃ ω : Ω, (M ω : Set FS) = Set.univ :=
    Set.eq_univ_of_forall fun ⟨α, hα⟩ ↦
      Set.mem_iUnion.mpr <| by
        have ⟨β, hβ⟩ := h α
        let ϕ : F⟮α⟯ →ₐ[F] K' :=
          (IsScalarTower.toAlgHom _ _ _).comp
            ((AdjoinRoot.liftHom _ _ hβ).comp (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)
        have ⟨ω, hω⟩ :=
          exists_algHom_adjoin_of_splits (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ
            (adjoin_simple_le_iff.mpr hα)
        refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
        rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_algHom, adjoinRootEquivAdjoin_symm_apply_gen,
          AdjoinRoot.liftHom_root]
        rfl
  have ω : ∃ ω : Ω, ⊤ ≤ M ω := by
    cases finite_or_infinite F
    · have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
      have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
      exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩
    · simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]
  exact
    ((botEquiv K K').toAlgHom.restrictScalars F).comp
      (ω.choose.codRestrict K₀.toSubalgebra fun x ↦ ω.choose_spec trivial)

Похожие утверждения