ModuleMaximalIdealTorsionQuotient.lean
Nyll.EtaleFundamentalGroups.Purity.MaximalIdealTorsionQuotient
2 declarations indexed from sourceView source ↗ Module documentation
Removing maximal-ideal-power torsion
The primary component of a finite module over a Noetherian ring has a uniform annihilating ideal power. If a quotient vector is killed by another power, the product of those two powers kills any lift. The lift therefore already lies in the primary component, and the quotient vector is zero.
For the maximal ideal of a local ring, this excludes the maximal ideal from the associated primes of the quotient.
Imports8
- Nyll.EtaleFundamentalGroups.Purity.FinitePowerTorsionLength
- Mathlib.Algebra.Module.Torsion.Basic
- Mathlib.Algebra.Module.Torsion.PrimaryComponent
- Mathlib.LinearAlgebra.Quotient.Basic
- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
- Mathlib.RingTheory.Ideal.Operations
- Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
- Mathlib.RingTheory.Noetherian.Basic
Imported by5
Declarations
EtaleFundamentalGroups.Purity.eq_zero_of_idealPower_torsion_quotient_primaryComponent
DocumentationQuotienting a finite module by its ideal-primary component removes all vectors annihilated by powers 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] [IsNoetherianRing R]
variable {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
EtaleFundamentalGroups.Purity.maximalIdeal_not_mem_associatedPrimes_quotient_primaryComponent
DocumentationThe maximal ideal is not associated to the quotient by the maximal-ideal-primary component of a finite 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] [IsNoetherianRing R]
variable {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]