NYLL
Module

ResidueFieldHullPowerTorsion.lean

Nyll.EtaleFundamentalGroups.Purity.ResidueFieldHullPowerTorsion
1 declaration indexed from sourceView source ↗

Module documentation

Power torsion in an essential extension of the residue field

The residue-field image is killed by the maximal ideal. The general preservation of ideal-power torsion under essential extensions therefore makes every vector in an essential extension of that image power torsion. No injectivity assumption on the ambient module is required.

Imports5
Imported by2

Declarations

theorem

exists_maximalIdeal_pow_smul_eq_zero_of_essential_residueField_range

L34 ↗
EtaleFundamentalGroups.Purity.exists_maximalIdeal_pow_smul_eq_zero_of_essential_residueField_range
Documentation

Every element of an essential extension of the residue field is annihilated by a power of the maximal ideal. The embedding furnished by an injective hull supplies i and hi; its injectivity is not needed here.

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 {E : Type v} [AddCommGroup E] [Module R E]
Lean source · statement
theorem exists_maximalIdeal_pow_smul_eq_zero_of_essential_residueField_range
    [IsNoetherianRing R]
    (i : R ⧸ maximalIdeal R →ₗ[R] E)
    (hi : IsEssentialSubmodule (LinearMap.range i)) (z : E) :
    ∃ n : ℕ, ∀ a : R, a ∈ maximalIdeal R ^ n → a • z = 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.