range_eq_top_of_cancel — Mathlib

English

If p is equal to the bottom submodule, then the quotient M/p is canonically isomorphic to M.

Русский

Если p равен нулю, то фактор‑модуль M/ p канонически изоморфен M.

LaTeX

$$$$ \\text{quotEquivOfEqBot}(p) : (M/ p) \\cong M \\quad (p = \\bot). $$$$

Lean4

/-- An epimorphism is surjective. -/
theorem range_eq_top_of_cancel {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ u v : M₂ →ₗ[R₂] M₂ ⧸ (range f), u.comp f = v.comp f → u = v) :
    range f = ⊤ := by
  have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
  rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
  exact ker_zero

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