subsingleton_of_prod_injective — Mathlib

English

If M ⊕ N embeds into M, then N is a subsingleton.

Русский

Если M ⊕ N вкладывается в M, то N тривиально (is a singleton).

LaTeX

$$$\\forall f: M \\times N \\to M\\text{, if } f \\text{ is injective, then } N \\text{ is Subsingleton}$$$

Lean4

/-- If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial. -/
theorem subsingleton_of_prod_injective (f : M × N →ₗ[R] M) (i : Injective f) : Subsingleton N :=
  .intro fun x y ↦
    by
    have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective
    simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)

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