ModuleEssentialIdealPowerTorsion.lean
Nyll.EtaleFundamentalGroups.Purity.EssentialIdealPowerTorsion
2 declarations indexed from sourceView source ↗ Module documentation
Ideal-power torsion in essential extensions
Over a Noetherian ring, an essential extension of an ideal-power torsion module is again ideal-power torsion. First, any prime annihilator in the extension contains the ideal: otherwise an element of the ideal acts injectively on the associated cyclic module, contradicting essentialness and power torsion in the intersection.
Minimal primes over each element annihilator are themselves element annihilators. Their intersection contains the ideal, and finite generation converts this radical containment into an annihilating power.
Imports9
- Nyll.EtaleFundamentalGroups.Purity.EssentialModuleExtension
- Mathlib.Algebra.Module.Submodule.Lattice
- Mathlib.LinearAlgebra.Span.Defs
- Mathlib.RingTheory.Finiteness.Ideal
- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
- Mathlib.RingTheory.Ideal.MinimalPrime.Colon
- Mathlib.RingTheory.Ideal.Operations
- Mathlib.RingTheory.Ideal.Prime
- Mathlib.RingTheory.Noetherian.Defs
Imported by3
Declarations
EtaleFundamentalGroups.Purity.ideal_le_prime_colon_of_essential_power_torsion
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 {E : Type v} [AddCommGroup E] [Module R E]
EtaleFundamentalGroups.Purity.exists_ideal_pow_smul_eq_zero_of_essential_submodule
DocumentationOver a Noetherian ring, every vector in an essential extension of an ideal-power torsion module 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 {E : Type v} [AddCommGroup E] [Module R E]