English
If R is commutative, M is a simple R-module, then the annihilator of M, Ann_R(M), is a maximal ideal of R.
Русский
Если R коммутативно, и M прост как R-модуль, то аннигилятор модуля Ann_R(M) является максимальной идеалой R.
LaTeX
$$Ideal.IsMaximal (Module.annihilator R M)$$
Lean4
/-- A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal
(not necessarily unique if the ring is not commutative). -/
theorem isSimpleModule_iff_quot_maximal : IsSimpleModule R M ↔ ∃ I : Ideal R, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I) :=
by
refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
· have := IsSimpleModule.nontrivial R M
have ⟨m, hm⟩ := exists_ne (0 : M)
exact
⟨_, ker_toSpanSingleton_isMaximal R hm,
⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
· convert congr equiv; rwa [isSimpleModule_iff_isCoatom]
