ker_eq_bot_of_cancel — Mathlib

English

φ.submoduleImage N equals map φ (comap O.subtype N).

Русский

φ.submoduleImage N равно map φ (comap O.subtype N).

LaTeX

$$$$ \varphi.\mathrm{submoduleImage }N = \operatorname{map} \varphi (\operatorname{comap} O.\mathrm{subtype} N). $$$$

Lean4

/-- A monomorphism is injective. -/
theorem ker_eq_bot_of_cancel {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ u v : ker f →ₗ[R] M, f.comp u = f.comp v → u = v) : ker f = ⊥ :=
  by
  have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _
  rw [← Submodule.range_subtype (ker f), ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]
  exact range_zero

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