isotypicComponent

Mathlib.RingTheory.SimpleModule.Isotypic

URI: https://scilib.ai/kg/mathlib#isotypicComponent

← MathLib Explorer

English

Same as above for submodule m with IsIsotypic R m; existence of n, x, S with m ≃ Fin n → S.

Русский

То же самое для подмодуля m: существует n и S с m ≃ Fin n → S.

LaTeX

$$$\text{(as in 184626)}$$$

Lean4

/-- If `S` is a simple `R`-module, the `S`-isotypic component in an `R`-module `M` is the sum of
all submodules of `M` isomorphic to `S`. -/
def isotypicComponent : Submodule R M :=
  sSup {m | Nonempty (m ≃ₗ[R] S)}

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru