primitive_element_iff_algHom_eq_of_eval

English

If there exists α with F⟮α⟯ = ⊤, then there exists a finite or infinite compatible structure such that E is generated by α.

Русский

Если существует α такой, что F⟮α⟯ = ⊤, тогда E порождается α.

LaTeX

$$$\exists \alpha\in E,\ F\langle \alpha\rangle = \top$$$

Lean4

theorem primitive_element_iff_algHom_eq_of_eval (α : E) (φ : E →ₐ[F] A) :
    F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ :=
  by
  refine
    ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ, fun h ↦
      eq_of_le_of_finrank_eq' le_top ?_⟩
  letI : Algebra F⟮α⟯ A := (φ.comp F⟮α⟯.val).toAlgebra
  haveI := Algebra.isSeparable_tower_top_of_isSeparable F F⟮α⟯ E
  rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
  ·
    exact
      ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦
        AlgHom.restrictScalars_injective F <| Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩
  · exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

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