sSupIndep_isotypicComponents — Mathlib

English

The family of isotypic components is independent with respect to supremum; in particular, they form an independent set under taking suprema.

Русский

Семейство изотипических компонентов независимо относительно наибольшего (супремума); т.е. образуют независимую систему относительно объединения.

LaTeX

$$$$ \\operatorname{sSupIndep}(\\mathrm{isotypicComponents}(R,M)). $$$$

Lean4

theorem sSupIndep_isotypicComponents : sSupIndep (isotypicComponents R M) := fun c hc ↦
  disjoint_iff.mpr <|
    of_not_not fun ne ↦ by
      set s := isotypicComponents R M \ { c }
      have : IsSemisimpleModule R c := by obtain ⟨S, _, rfl⟩ := hc; infer_instance
      have := IsSemisimpleModule.of_injective _ (Submodule.inclusion_injective (inf_le_left : c ⊓ sSup s ≤ c))
      have (c : s) : IsSemisimpleModule R c := by obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c; infer_instance
      have ⟨S, le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le _).resolve_left ne
      have ⟨c', hc', S', le', ⟨e⟩⟩ := S.le_linearEquiv_of_le_sSup _ (le.trans inf_le_right)
      have := IsSimpleModule.congr e.symm
      refine hc'.2 ?_
      rw [eq_isotypicComponent_of_le hc (le.trans inf_le_left), eq_isotypicComponent_of_le hc'.1 le']
      exact e.symm.isotypicComponent_eq

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