quotientEquiv — Mathlib

English

There is a canonical algebra isomorphism between the quotient P.Quotient and S, compatible with the right R-ring structure.

Русский

Существует каноническое алгебраическое изоморфизм между квотами P.Quotient и S, согласованный с структурами над R.

LaTeX

$$$P.\\mathrm{Quotient} \\simeq_{\\!P.Ring} S$$$

Lean4

/-- `P.Quotient` is `P.Ring`-isomorphic to `S` and in particular `R`-isomorphic to `S`. -/
def quotientEquiv : P.Quotient ≃ₐ[P.Ring] S :=
  Ideal.quotientKerAlgEquivOfRightInverse (f := Algebra.ofId P.Ring S) (g := P.σ) <| fun x ↦ by
    rw [Algebra.ofId_apply, P.algebraMap_apply, P.aeval_val_σ]

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