subset_of_injective — Mathlib

English

If f is an injection, then the associated primes of M embed into those of M'.

Русский

Если f инъективно отображает M в M', то множества ассоциированных простых вложены: ассоциированные простые M ⊆ ассоциированные простые M'.

LaTeX

$$$$\operatorname{associatedPrimes}(R,M) \subseteq \operatorname{associatedPrimes}(R,M'). $$$$

Lean4

/-- If `M → M'` is injective, then the set of associated primes of `M` is
contained in that of `M'`. -/
@[stacks 02M3 "first part"]
theorem subset_of_injective (hf : Function.Injective f) : associatedPrimes R M ⊆ associatedPrimes R M' := fun _I h =>
  h.map_of_injective f hf

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