Documentation

Mathlib.RingTheory.SimpleModule

Simple Modules #

Main Definitions #

Main Results #

TODO #

@[reducible, inline]
abbrev IsSimpleModule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] :

A module is simple when it has only two submodules, and .

Equations
Instances For
    @[reducible, inline]
    abbrev IsSemisimpleModule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] :

    A module is semisimple when every submodule has a complement, or equivalently, the module is a direct sum of simple modules.

    Equations
    Instances For
      @[reducible, inline]
      abbrev IsSemisimpleRing (R : Type u_2) [Ring R] :

      A ring is semisimple if it is semisimple as a module over itself.

      Equations
      Instances For
        theorem RingEquiv.isSemisimpleRing (R : Type u_2) (S : Type u_3) [Ring R] [Ring S] (e : R ≃+* S) [IsSemisimpleRing R] :
        theorem IsSimpleModule.nontrivial (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSimpleModule R M] :
        theorem LinearMap.isSimpleModule_iff_of_bijective {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) :
        theorem IsSimpleModule.congr {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (l : M ≃ₗ[R] N) [IsSimpleModule R N] :
        theorem isSimpleModule_iff_isAtom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} :
        theorem isSimpleModule_iff_isCoatom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} :
        theorem covBy_iff_quot_is_simple {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {A : Submodule R M} {B : Submodule R M} (hAB : A B) :
        A B IsSimpleModule R (B Submodule.comap B.subtype A)
        @[simp]
        theorem IsSimpleModule.isAtom {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} [IsSimpleModule R m] :
        theorem IsSimpleModule.span_singleton_eq_top (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] {m : M} (hm : m 0) :
        instance IsSimpleModule.instIsPrincipal (R : Type u_2) [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSimpleModule R M] (S : Submodule R M) :
        S.IsPrincipal
        Equations
        • =
        theorem isSimpleModule_iff_quot_maximal {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] :
        IsSimpleModule R M ∃ (I : Ideal R), I.IsMaximal Nonempty (M ≃ₗ[R] R I)

        A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal (not necessarily unique if the ring is not commutative).

        theorem IsSimpleModule.annihilator_isMaximal {M : Type u_4} [AddCommGroup M] {R : Type u_6} [CommRing R] [Module R M] [simple : IsSimpleModule R M] :
        (Module.annihilator R M).IsMaximal

        In general, the annihilator of a simple module is called a primitive ideal, and it is always a two-sided prime ideal, but mathlib's Ideal.IsPrime is not the correct definition for noncommutative rings.

        theorem isSimpleModule_self_iff_isUnit {R : Type u_2} [Ring R] :
        IsSimpleModule R R Nontrivial R ∀ (x : R), x 0IsUnit x

        A ring is a simple module over itself iff it is a division ring.

        @[deprecated IsSemisimpleModule.of_sSup_simples_eq_top]
        theorem is_semisimple_of_sSup_simples_eq_top {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (h : sSup {m : Submodule R M | IsSimpleModule R m} = ) :

        Alias of IsSemisimpleModule.of_sSup_simples_eq_top.

        theorem IsSemisimpleModule.eq_bot_or_exists_simple_le {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (N : Submodule R M) :
        N = mN, IsSimpleModule R m
        theorem IsSemisimpleModule.sSup_simples_le {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (N : Submodule R M) :
        sSup {m : Submodule R M | IsSimpleModule R m m N} = N

        The annihilator of a semisimple module over a commutative ring is a radical ideal.

        instance IsSemisimpleModule.submodule (R : Type u_2) [Ring R] (M : Type u_4) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} :
        Equations
        • =
        theorem IsSemisimpleModule.congr {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] (e : N ≃ₗ[R] M) :
        instance IsSemisimpleModule.quotient {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {m : Submodule R M} [IsSemisimpleModule R M] :
        Equations
        • =
        theorem IsSemisimpleModule.range {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] (f : M →ₗ[R] N) :
        theorem LinearMap.isSemisimpleModule_iff_of_bijective {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] {M' : Type u_6} [AddCommGroup M'] [Module R M'] {N' : Type u_7} [AddCommGroup N'] [Module S N'] {σ : R →+* S} (l : M' →ₛₗ[σ] N') [RingHomSurjective σ] (hl : Function.Bijective l) :

        A module is semisimple iff it is generated by its simple submodules.

        @[deprecated sSup_simples_eq_top_iff_isSemisimpleModule]

        Alias of sSup_simples_eq_top_iff_isSemisimpleModule.


        A module is semisimple iff it is generated by its simple submodules.

        theorem isSemisimpleModule_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {s : Set ι} {p : ιSubmodule R M} (hp : is, IsSemisimpleModule R (p i)) (hp' : is, p i = ) :

        A module generated by semisimple submodules is itself semisimple.

        theorem isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {s : Set ι} {p : ιSubmodule R M} (hp : is, IsSemisimpleModule R (p i)) :
        IsSemisimpleModule R (⨆ is, p i)
        theorem isSemisimpleModule_of_isSemisimpleModule_submodule' {ι : Type u_1} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {p : ιSubmodule R M} (hp : ∀ (i : ι), IsSemisimpleModule R (p i)) (hp' : ⨆ (i : ι), p i = ) :
        theorem IsSemisimpleModule.sup {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
        Equations
        • =
        Equations
        • =
        instance instIsSemisimpleRingForallOfFinite {ι : Type u_7} [Finite ι] (R : ιType u_6) [(i : ι) → Ring (R i)] [∀ (i : ι), IsSemisimpleRing (R i)] :
        IsSemisimpleRing ((i : ι) → R i)

        A finite product of semisimple rings is semisimple.

        Equations
        • =
        instance instIsSemisimpleRingProd {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] :

        A binary product of semisimple rings is semisimple.

        Equations
        • =
        theorem LinearMap.injective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] (f : M →ₗ[R] N) :
        theorem LinearMap.injective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] {f : M →ₗ[R] N} (h : f 0) :
        theorem LinearMap.surjective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] (f : M →ₗ[R] N) :
        theorem LinearMap.surjective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f 0) :
        theorem LinearMap.bijective_or_eq_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) :

        Schur's Lemma for linear maps between (possibly distinct) simple modules

        theorem LinearMap.bijective_of_ne_zero {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f 0) :
        theorem LinearMap.isCoatom_ker_of_surjective {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (hf : Function.Surjective f) :
        noncomputable instance Module.End.divisionRing {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] [DecidableEq (Module.End R M)] [IsSimpleModule R M] :

        Schur's Lemma makes the endomorphism ring of a simple module a division ring.

        Equations
        def JordanHolderModule.Iso {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (X : Submodule R M × Submodule R M) (Y : Submodule R M × Submodule R M) :

        An isomorphism X₂ / X₁ ∩ X₂ ≅ Y₂ / Y₁ ∩ Y₂ of modules for pairs (X₁,X₂) (Y₁,Y₂) : Submodule R M

        Equations
        Instances For
          theorem JordanHolderModule.second_iso {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {X : Submodule R M} {Y : Submodule R M} :
          X X YJordanHolderModule.Iso (X, X Y) (X Y, Y)
          Equations
          • One or more equations did not get rendered due to their size.