quotientMap_surjective — Mathlib

English

If f is surjective, then the quotient map between quotients is surjective.

Русский

Если f сюръективен, то отображение частных между частными получаются сюръективны.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(\text{quotientMap } I f H)$$$

Lean4

theorem quotientMap_surjective {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S}
    {H : J ≤ I.comap f} (hf : Function.Surjective f) : Function.Surjective (quotientMap I f H) := fun x =>
  let ⟨x, hx⟩ := Quotient.mk_surjective x
  let ⟨y, hy⟩ := hf x
  ⟨(Quotient.mk J) y, by simp [hx, hy]⟩

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