surjective_iff_epi_and_finite — Mathlib

English

For rings R,S and f:R→S, f is surjective iff f is epi and f.hom is finite.

Русский

Для колец R,S и гомоморфизма f:R→S, f сюрьективно тогда и только тогда, когда f — эпиморфизм и f.hom конечен.

LaTeX

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

Lean4

theorem surjective_iff_epi_and_finite {R S : CommRingCat} {f : R ⟶ S} :
    Function.Surjective f ↔ Epi f ∧ RingHom.Finite f.hom
    where
  mp h := ⟨ConcreteCategory.epi_of_surjective f h, .of_surjective f.hom h⟩
  mpr := fun ⟨_, h⟩ ↦ surjective_of_epi_of_finite f h

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