eq — Mathlib · SciLib

English

Let R be a commutative ring and M, M' be R-modules. If there exists an R-linear isomorphism l: M ≃_R M', then the sets of associated primes are equal: Ass_R(M) = Ass_R(M').

Русский

Пусть R — коммутативное кольцо, M и M' — R-модули. Если существует R-линейное изоморфное отображение l: M ≃_R M', то множества ассоциированных прайм-идеалов совпадают: Ass_R(M) = Ass_R(M').

LaTeX

$$$\\operatorname{Ass}_R(M) = \\operatorname{Ass}_R(M')$ при существовании изоморфизма $M \\cong_R M'.$$$

Lean4

theorem eq (l : M ≃ₗ[R] M') : associatedPrimes R M = associatedPrimes R M' :=
  le_antisymm (associatedPrimes.subset_of_injective l.injective) (associatedPrimes.subset_of_injective l.symm.injective)

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