algEquivQuotient — Mathlib

English

There is an algebra isomorphism between the polynomial quotient by f and the power-series quotient by g when g is a Weierstrass factorization of f by h with respect to I.

Русский

Существует алгебраическое изоморфизм между частными A[X]/(f) и A⟦X⟧/(g), когда g является факторизацией Вайершстраса f по h по I.

LaTeX

$$AlgEquiv A (HasQuotient.Quotient (Polynomial A) (Ideal.span { f })) ≃ₐ[A] HasQuotient.Quotient (PowerSeries A) (Ideal.span { g })$$

Lean4

/-- If `g = f * h` is a Weierstrass factorization, then there is a
natural isomorphism `A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g)`. -/
@[simps! apply]
noncomputable def algEquivQuotient [IsAdicComplete I A] : (A[X] ⧸ Ideal.span { f }) ≃ₐ[A] A⟦X⟧ ⧸ Ideal.span { g } :=
  H.isDistinguishedAt.algEquivQuotient.trans <|
    Ideal.quotientEquivAlgOfEq A <| by rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]

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