map_of_injective — Mathlib

English

If I is an associated prime of M and f: M → M' is injective, then I is also an associated prime of M'.

Русский

Если I ассоциирован в M и б f: M → M' инъективен, то I также ассоциирован в M'.

LaTeX

$$$$\IsAssociatedPrime I M \land \text{Injective}(f) \Rightarrow \IsAssociatedPrime I M'. $$$$

Lean4

theorem map_of_injective (h : IsAssociatedPrime I M) (hf : Function.Injective f) : IsAssociatedPrime I M' :=
  by
  obtain ⟨x, rfl⟩ := h.2
  refine ⟨h.1, ⟨f x, ?_⟩⟩
  ext r
  simp_rw [mem_ker, toSpanSingleton_apply, ← map_smul, ← f.map_zero, hf.eq_iff]

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