Theorems · Definition · ring theory

iSupIndep.ringEquiv

{R : Type u_2} →
  {M : Type u} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {ι : Type u_5} →
            [DecidableEq ι] →
              {N : ι → Submodule R M} →
                iSupIndep N →
                  ⨆ i, N i = ⊤ →
                    (∀ (i : ι), (N i).IsFullyInvariant) → Module.End R M ≃+* ((i : ι) → Module.End R ↥(N i))

If an R-module M is the direct sum of fully invariant submodules Nᵢ, then End R M is isomorphic to Πᵢ End R Nᵢ as a ring.

Defined in

Mathlib.RingTheory.SimpleModule.Isotypic

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleDecidableEq