quotientKerEquivRange — Mathlib

English

For a ring homomorphism f: A → B that is an algebra homomorphism over R, the quotient A/ker f is isomorphic to the range of f as an R-algebra.

Русский

Для гомоморфизма колец f: A → B, который является алгебра-гомоморфизмом над R, фактор-получение A/ker f изоморфно диапазону f как R-алгебра.

LaTeX

$$$(A/\\ker f) \\cong_{R} \\mathrm{range}(f)$$$

Lean4

/-- The **first isomorphism theorem** for commutative algebras (`AlgHom.range` version). -/
noncomputable def quotientKerEquivRange {R A B : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Semiring B]
    [Algebra R B] (f : A →ₐ[R] B) : (A ⧸ RingHom.ker f) ≃ₐ[R] f.range :=
  (Ideal.quotientEquivAlgOfEq R (AlgHom.ker_rangeRestrict f).symm).trans <|
    Ideal.quotientKerAlgEquivOfSurjective f.rangeRestrict_surjective

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