le_linearEquiv_of_sSup_eq_top — Mathlib

English

Under a linear equivalence e: N ≃ₗ[R] S, the isotypicComponent is preserved: isotypicComponent R M N = isotypicComponent R M S.

Русский

При линейном эквивеленте e: N ≃ₗ[R] S сохраняется isotypicComponent: isotypicComponent R M N = isotypicComponent R M S.

LaTeX

$$$isotypicComponent(R, M, N) = isotypicComponent(R, M, S)$$$

Lean4

theorem le_linearEquiv_of_sSup_eq_top [IsSemisimpleModule R M] (hs : sSup s = ⊤) :
    ∃ m ∈ s, ∃ S ≤ m, Nonempty (N ≃ₗ[R] S) :=
  by
  have := IsSimpleModule.nontrivial R N
  have ⟨_, compl⟩ := exists_isCompl N
  have ⟨m, hm, ne⟩ :=
    exists_ne_zero_of_sSup_eq_top (ne_zero_of_surjective (N.linearProjOfIsCompl_surjective compl)) _ hs
  have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne
  exact ⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩

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