ModuleFinitePowerTorsionLength.lean
Nyll.EtaleFundamentalGroups.Purity.FinitePowerTorsionLength
2 declarations indexed from sourceView source ↗ Module documentation
Finite length of finite maximal-ideal-power torsion modules
A finite generating set bounds the ideal-power exponents needed to kill individual elements. In the local Noetherian case the module is then finite over an Artinian maximal-ideal-power quotient, so it has finite length.
Imports9
- Nyll.EtaleFundamentalGroups.Purity.MaximalIdealPowerQuotientLength
- Mathlib.Algebra.Module.Submodule.Ker
- Mathlib.Algebra.Module.Torsion.Basic
- Mathlib.Data.Finset.Lattice.Fold
- Mathlib.RingTheory.Artinian.Module
- Mathlib.RingTheory.FiniteLength
- Mathlib.RingTheory.Finiteness.Basic
- Mathlib.RingTheory.Ideal.Operations
- Mathlib.RingTheory.Noetherian.Basic
Imported by5
Declarations
EtaleFundamentalGroups.Purity.exists_ideal_pow_le_annihilator_of_finite
DocumentationElementwise ideal-power torsion on a finite module has a uniform annihilating exponent.
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]
EtaleFundamentalGroups.Purity.isFiniteLength_of_finite_of_maximalIdealPower_torsion
DocumentationA finite module whose elements are killed by powers of the maximal ideal of a Noetherian local ring has finite length.
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]