surjective_of_epi_of_finite — Mathlib

English

If a ring hom f is an epimorphism and finite (as a module), then f is surjective.

Русский

Если кольцевой гомоморфизм f является эпиморфизмом и конечным как модуль, то f сюрьективен.

LaTeX

$$Epi(f) ∧ RingHom.Finite f.hom ⇒ Function.Surjective f$$

Lean4

theorem surjective_of_epi_of_finite {R S : CommRingCat} (f : R ⟶ S) [Epi f] (h₂ : RingHom.Finite f.hom) :
    Function.Surjective f := by
  algebraize [f.hom]
  apply RingHom.surjective_of_tmul_eq_tmul_of_finite
  rwa [← CommRingCat.epi_iff_tmul_eq_tmul]

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