quotAdjoinRootEquivQuotPolynomialQuot

English

The symmetry of the equiv' isomorphism preserves the canonical map on mk f p.

Русский

Симметрия изоморфизма equiv' сохраняет каноническое отображение mk f p.

LaTeX

$$equiv'_symm_toAlgHom_mk: = (equiv' g pb h1 h2).symm.toAlgHom = pb.lift (root g) h1$$

Lean4

/-- The natural isomorphism `R[α]/I[α] ≅ (R/I)[X]/(f mod I)` for `α` a root of `f : R[X]`
  and `I : Ideal R`. -/
def quotAdjoinRootEquivQuotPolynomialQuot :
    AdjoinRoot f ⧸ I.map (of f) ≃+* (R ⧸ I)[X] ⧸ span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]) :=
  (quotMapOfEquivQuotMapCMapSpanMk I f).trans
    ((quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f).trans
      ((Ideal.quotEquivOfEq (by rw [map_span, Set.image_singleton])).trans (Polynomial.quotQuotEquivComm I f).symm))

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