isotypicComponents — Mathlib

English

If N : Submodule R M is simple, then IsIsotypic R (Subtype fun x => x ∈ N) S iff certain isomorphisms exist; equivalence with isotypic type of N.

Русский

Если N — простой подмодуль, тогда IsIsotypic R (Subtype ...) S эквивалентно существованию соответствующих изоморфизмов; эквивалентность с изотипическим типом N.

LaTeX

$$$IsIsotypic(R, N) \iff \forall m ≤ N, [IsSimpleModule(R, m)] → IsIsotypicOfType(R, N, m)$$$

Lean4

/-- The set of all (nontrivial) isotypic components of a module. -/
def isotypicComponents : Set (Submodule R M) :=
  {m | ∃ S : Submodule R M, IsSimpleModule R S ∧ m = isotypicComponent R M S}

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