Module

ArtinianSecondaryDecomposition.lean

Nyll.EtaleFundamentalGroups.Purity.ArtinianSecondaryDecomposition

3 declarations indexed from sourceView source ↗

Module documentation

Secondary decompositions of Artinian modules

Multiplication on a secondary module is either surjective or nilpotent. If an Artinian module fails this condition, the stabilized kernel-range sum for the offending multiplication expresses it as the sum of two proper submodules. Well-founded induction on submodules therefore gives a finite secondary decomposition.

Imports10

Mathlib.Algebra.Module.LinearMap.End
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.Module.Submodule.LinearMap
Mathlib.Algebra.Module.Submodule.Map
Mathlib.Algebra.Module.Submodule.Range
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Finset.Empty
Mathlib.RingTheory.Artinian.Module
Mathlib.RingTheory.Nilpotent.Defs

Imported by2

def

IsSecondaryModule

L37 ↗

EtaleFundamentalGroups.Purity.IsSecondaryModule

Documentation

A nonzero module is secondary when every scalar acts surjectively or some power of that scalar annihilates the whole module.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

def IsSecondaryModule (R : Type u) (M : Type v)
    [CommRing R] [AddCommGroup M] [Module R M] : Prop

theorem

exists_ker_pow_lt_top_range_pow_lt_top

L47 ↗

EtaleFundamentalGroups.Purity.exists_ker_pow_lt_top_range_pow_lt_top

Documentation

If an endomorphism of an Artinian module is neither surjective nor nilpotent, a kernel and range of the same power are proper and sum to the whole module. No Noetherian hypothesis is needed for this sum.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem exists_ker_pow_lt_top_range_pow_lt_top
    [IsArtinian R M] (f : Module.End R M)
    (hsurj : ¬ Function.Surjective f) (hnil : ¬ IsNilpotent f) :
    ∃ n : ℕ,
      LinearMap.ker (f ^ n) < ⊤ ∧
        LinearMap.range (f ^ n) < ⊤ ∧
          LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤

theorem

exists_finset_secondarySubmodules_sup_eq_top

L72 ↗

EtaleFundamentalGroups.Purity.exists_finset_secondarySubmodules_sup_eq_top

Documentation

Every Artinian module is the sum of finitely many nonzero secondary submodules; the zero module has the empty decomposition.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem exists_finset_secondarySubmodules_sup_eq_top [IsArtinian R M] :
    ∃ s : Finset (Submodule R M),
      (∀ N ∈ s, IsSecondaryModule R N) ∧ s.sup id = ⊤

Module documentation

Secondary decompositions of Artinian modules

Declarations

IsSecondaryModule

exists_ker_pow_lt_top_range_pow_lt_top

exists_finset_secondarySubmodules_sup_eq_top