eq_bot_or_exists_simple_le — Mathlib

English

In a semisimple module, every submodule N is either zero or lies below some simple submodule.

Русский

В полупростом модуле каждый подмодуль N либо нулевой, либо лежит ниже некоторого простого подмодуля.

LaTeX

$$IsSemisimpleModule R N → (N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R m)$$

Lean4

theorem eq_bot_or_exists_simple_le (N : Submodule R M) [IsSemisimpleModule R N] : N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R m :=
  by
  rw [← N.subsingleton_iff_eq_bot, ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top]
  refine (eq_bot_or_exists_atom_le _).imp .symm fun ⟨m, h, _⟩ ↦ ⟨_, N.map_subtype_le m, ?_⟩
  rw [← isSimpleModule_iff_isAtom] at h
  exact .congr (m.equivMapOfInjective _ N.subtype_injective).symm

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