quotEquivQuotMap — Mathlib

English

The symmetric application of quotEquivQuotMap to a quotient of g corresponds to mk f mapped polynomially.

Русский

Симметрическая аппликация quotEquivQuotMap к квоте g соответствует mk f, отображённому полиномом.

LaTeX

$$quotEquivQuotMap_symm_apply_mk: = (quotEquivQuotMap f I).symm (Ideal.Quotient.mk _ (Polynomial.map (Ideal.Quotient.mk I) g)) = Ideal.Quotient.mk (I.map (of f)) (AdjoinRoot.mk f g)$$

Lean4

/-- Promote `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot` to an alg_equiv. -/
@[simps!]
noncomputable def quotEquivQuotMap (f : R[X]) (I : Ideal R) :
    (AdjoinRoot f ⧸ Ideal.map (of f) I) ≃ₐ[R]
      (R ⧸ I)[X] ⧸ Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X]) :=
  AlgEquiv.ofRingEquiv
    (show ∀ x, (quotAdjoinRootEquivQuotPolynomialQuot I f) (algebraMap R _ x) = algebraMap R _ x from fun x =>
      by
      have :
        algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I) x =
          Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I) ((mk f) (C x)) :=
        rfl
      rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C, Quotient.alg_map_eq]
      simp only [RingHom.comp_apply, Quotient.algebraMap_eq, Polynomial.algebraMap_apply])

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