isAssociatedPrime_iff_exists_injective_linearMap

English

I is an associated prime of M if and only if I is prime and there exists an injective linear map from R/I into M.

Русский

I — ассоциированный простой модуля M тогда и только тогда, когда I — прост и существует инъективное линейное отображение R/I в M.

LaTeX

$$$$\IsAssociatedPrime I M \iff I.IsPrime \land \exists f: (R/I) \to_L[R] M, \ \text{Injective}(f). $$$$

Lean4

theorem isAssociatedPrime_iff_exists_injective_linearMap :
    IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective f :=
  by
  rw [IsAssociatedPrime]
  congr! 1
  refine
    ⟨fun ⟨_, h⟩ ↦ ⟨Submodule.liftQ _ _ h.le, ker_eq_bot.1 (Submodule.ker_liftQ_eq_bot' _ _ h)⟩, fun ⟨f, h⟩ ↦
      ⟨(f ∘ₗ Submodule.mkQ I) 1, ?_⟩⟩
  have := I.ker_mkQ ▸ ker_comp_of_ker_eq_bot (Submodule.mkQ I) (ker_eq_bot_of_injective h)
  convert this.symm using 2
  ext; simp

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