Documentation

Mathlib.RingTheory.SimpleModule

Simple Modules #

Main Definitions #

Main Results #

TODO #

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

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

Instances For
    @[inline, reducible]
    abbrev IsSemisimpleModule (R : Type u_1) [Ring R] (M : Type u_2) [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.

    Instances For
      theorem IsSimpleModule.nontrivial (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSimpleModule R M] :
      theorem IsSimpleModule.congr {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (l : M ≃ₗ[R] N) [IsSimpleModule R N] :
      theorem isSimpleModule_iff_isAtom {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {m : Submodule R M} :
      IsSimpleModule R { x // x m } IsAtom m
      theorem isSimpleModule_iff_isCoatom {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {m : Submodule R M} :
      theorem covby_iff_quot_is_simple {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {A : Submodule R M} {B : Submodule R M} (hAB : A B) :
      @[simp]
      theorem IsSimpleModule.isAtom {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {m : Submodule R M} [hm : IsSimpleModule R { x // x m }] :
      theorem is_semisimple_of_sSup_simples_eq_top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (h : sSup {m | IsSimpleModule R { x // x m }} = ) :
      theorem IsSemisimpleModule.sSup_simples_eq_top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :
      sSup {m | IsSimpleModule R { x // x m }} =
      instance IsSemisimpleModule.is_semisimple_submodule {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {m : Submodule R M} :
      IsSemisimpleModule R { x // x m }
      theorem is_semisimple_iff_top_eq_sSup_simples {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] :
      sSup {m | IsSimpleModule R { x // x m }} = IsSemisimpleModule R M
      theorem LinearMap.injective_or_eq_zero {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsSimpleModule R M] (f : M →ₗ[R] N) :
      theorem LinearMap.injective_of_ne_zero {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsSimpleModule R M] {f : M →ₗ[R] N} (h : f 0) :
      theorem LinearMap.surjective_or_eq_zero {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsSimpleModule R N] (f : M →ₗ[R] N) :
      theorem LinearMap.surjective_of_ne_zero {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f 0) :
      theorem LinearMap.bijective_or_eq_zero {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [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_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [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_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N} (hf : Function.Surjective f) :
      noncomputable instance Module.End.divisionRing {R : Type u_1} [Ring R] {M : Type u_2} [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.

      def JordanHolderModule.Iso {R : Type u_1} [Ring R] {M : Type u_2} [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

      Instances For
        theorem JordanHolderModule.second_iso {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {X : Submodule R M} {Y : Submodule R M} :
        X X YJordanHolderModule.Iso (X, X Y) (X Y, Y)