equivPUnitOfProdInjective — Mathlib

English

If M ⊕ N embeds into M and M is Noetherian, then there is a linear equivalence between N and the one-point module PUnit.

Русский

Если M ⊕ N встроено в M и M Нётеров, то существует линейное эквивалентность N и PUnit.

LaTeX

$$$\\text{equivPUnitOfProdInjective }(f,i): N \\simeq_R PUnit$$$

Lean4

/-- If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial. -/
@[simps!]
def equivPUnitOfProdInjective (f : M × N →ₗ[R] M) (i : Injective f) : N ≃ₗ[R] PUnit.{w + 1} :=
  haveI := IsNoetherian.subsingleton_of_prod_injective f i
  .ofSubsingleton _ _

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