ModulePrimeQuotientCoefficients.lean
Nyll.EtaleFundamentalGroups.Purity.PrimeQuotientCoefficients
2 declarations indexed from sourceView source ↗ Module documentation
Scalars on modules isomorphic to prime quotients
The residue field is annihilated by the maximal ideal. For any other prime quotient of a local ring, an element of the maximal ideal outside the prime acts regularly. These properties transfer along a coefficient linear equivalence without constructing a map on local cohomology.
Imports4
- Mathlib.RingTheory.Ideal.Quotient.Basic
- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
- Mathlib.RingTheory.Regular.IsSMulRegular
- Mathlib.RingTheory.Spectrum.Prime.Basic
Imported by2
Declarations
EtaleFundamentalGroups.Purity.maximalIdeal_smul_eq_zero_of_equiv_residueField
DocumentationThe maximal ideal kills any module linearly equivalent to the residue field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]
variable {N : Type v} [AddCommGroup N] [Module R N]
EtaleFundamentalGroups.Purity.exists_regular_maximalIdeal_scalar_of_equiv_primeQuotient
DocumentationA prime quotient different from the residue field admits a regular scalar in the maximal ideal, also after transporting the coefficients along a linear equivalence.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]
variable {N : Type v} [AddCommGroup N] [Module R N]