English
For a submodule N ⊆ M, IsIsotypicOfType R N S holds iff every sub-submodule m ≤ N which is simple is isomorphic to S.
Русский
Для подмодуля N ⊆ M, IsIsotypicOfType R N S эквивалентно тому, что любой подмодуль m ≤ N, являющийся простым, изоморфен S.
LaTeX
$$$IsIsotypicOfType(R, N, S) \iff \forall m \le N, [IsSimpleModule(R, m)] \rightarrow \exists e: m \simeq_{R} S.$$$
Lean4
theorem isIsotypicOfType_submodule_iff {N : Submodule R M} :
IsIsotypicOfType R N S ↔ ∀ m ≤ N, [IsSimpleModule R m] → Nonempty (m ≃ₗ[R] S) :=
by
rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]
have e := Submodule.equivMapOfInjective _ N.subtype_injective
simp_rw [Submodule.MapSubtype.orderIso, Equiv.coe_fn_mk, ← (e _).isSimpleModule_iff]
exact forall₂_congr fun m _ ↦ ⟨fun ⟨e'⟩ ↦ ⟨(e m).symm.trans e'⟩, fun ⟨e'⟩ ↦ ⟨(e m).trans e'⟩⟩
