adjoinSingletonEquivAdjoinRootMinpoly

English

For a field F and an algebra A over F, the F-subalgebra generated by a single element a ∈ A is canonically isomorphic to AdjoinRoot(minpoly F a), i.e., F[a] ≅_F F[x]/(minpoly F a).

Русский

При поле F и алгебре A над F, подалгебра над F, порождаемая одним элементом a ∈ A, канонически изоморфна AdjoinRoot(minpoly F a); то есть F[a] ≅_F F[x]/(minpoly F a).

LaTeX

$$$\\operatorname{adjoin}_F(\\{x\\}) \\cong_F \\operatorname{AdjoinRoot}(\\minpoly F x)$$$

Lean4

/-- If `p` is the minimal polynomial of `a` over `F` then `F[a] ≃ₐ[F] F[x]/(p)` -/
def adjoinSingletonEquivAdjoinRootMinpoly {R : Type*} [CommRing R] [Algebra F R] (x : R) :
    Algebra.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 ?_)
      simp_all [← Subalgebra.coe_eq_zero]

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