ker_quotientMap_mk — Mathlib

English

If f is surjective, the first isomorphism theorem yields an algebra isomorphism A/(ker f) ≃ₐ B.

Русский

Если f сюръективен, то теорема о первом изоморфизме даёт алгебраическое изоморфизм A/(ker f) ≃ₐ B.

LaTeX

$$$\text{quotientKerAlgEquivOfSurjective } f : (A \ocircle ker f) \simeq_A B$$$

Lean4

theorem ker_quotientMap_mk {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] :
    RingHom.ker (quotientMap (J.map _) (Quotient.mk I) le_comap_map) = I.map (Quotient.mk J) := by
  rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
    Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]

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