isIsotypic_submodule_iff — Mathlib

English

IsIsotypic R N holds iff for all m ≤ N, [IsSimpleModule R m] implies IsIsotypicOfType R N m.

Русский

IsIsotypic R N эквивалентно тому, что для всех m ≤ N, если m прост, то IsIsotypicOfType R N m.

LaTeX

$$$IsIsotypic(R, N) \iff \forall m \le N, [IsSimpleModule(R, m)] \rightarrow IsIsotypicOfType(R, N, m)$$$

Lean4

theorem isIsotypic_submodule_iff {N : Submodule R M} :
    IsIsotypic R N ↔ ∀ m ≤ N, [IsSimpleModule R m] → IsIsotypicOfType R N m :=
  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, ←
    (e _).isIsotypicOfType_iff_type, IsIsotypic]

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