Module

MaximalIdealPowerTorsionSocle.lean

Nyll.EtaleFundamentalGroups.Purity.MaximalIdealPowerTorsionSocle

2 declarations indexed from sourceView source ↗

Module documentation

Essential socles of ideal-power torsion modules

If every vector is killed by some power of an ideal, the submodule killed by the ideal itself is essential. On a submodule disjoint from it, induction on the annihilating exponent makes each vector zero. The successor step applies the induction hypothesis to every scalar multiple by an element of the ideal.

Taking the ideal to be the maximal ideal proves essentialness of the socle of a maximal-ideal-power torsion module. No finite generation hypothesis or auxiliary scalar structure is needed.

Imports5

Nyll.EtaleFundamentalGroups.Purity.EssentialModuleExtension
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs

Imported by3

theorem

isEssentialSubmodule_torsionBySet_of_idealPower_torsion

L36 ↗

EtaleFundamentalGroups.Purity.isEssentialSubmodule_torsionBySet_of_idealPower_torsion

Documentation

The vectors killed by an ideal form an essential submodule when each vector is killed by some power of that ideal.

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 isEssentialSubmodule_torsionBySet_of_idealPower_torsion
    (I : Ideal R)
    (hM : ∀ z : M, ∃ n : ℕ, ∀ a ∈ I ^ n, a • z = 0) :
    IsEssentialSubmodule (Submodule.torsionBySet R M I)

theorem

isEssentialSubmodule_torsionBySet_maximalIdeal_of_power_torsion

L69 ↗

EtaleFundamentalGroups.Purity.isEssentialSubmodule_torsionBySet_maximalIdeal_of_power_torsion