NYLL
Module

CompleteLocalResidueFieldHullArtinian.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalResidueFieldHullArtinian
2 declarations indexed from sourceView source ↗

Module documentation

Artinianness of a residue-field hull over a complete local ring

An endomorphism of the hull acts by a scalar on every maximal-ideal power-torsion layer. The scalar classes are compatible because their differences annihilate each smaller layer. Completeness lifts them to one scalar in the ring, and power torsion makes its action equal to the given endomorphism everywhere.

The scalar endomorphism theorem identifies submodules with their double annihilators. Noetherianity of the ring then gives the descending chain condition on submodules of the hull.

Imports11
Imported by3

Declarations

theorem

exists_smul_eq_of_completeLocal_residueFieldHull

L45 ↗
EtaleFundamentalGroups.Purity.exists_smul_eq_of_completeLocal_residueFieldHull
Documentation

Every endomorphism of an injective residue-field hull over a complete Noetherian local ring is multiplication by an element of the ring.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem exists_smul_eq_of_completeLocal_residueFieldHull
    [IsAdicComplete (maximalIdeal R) R]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i)) (f : E →ₗ[R] E) :
    ∃ a : R, ∀ z : E, f z = a • z
theorem

isArtinian_of_completeLocal_residueFieldHull

L84 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_completeLocal_residueFieldHull
Documentation

An injective hull of the residue field of a complete Noetherian local ring is Artinian as a module over that ring.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {E : Type u} [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem isArtinian_of_completeLocal_residueFieldHull
    [IsAdicComplete (maximalIdeal R) R]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i)) : IsArtinian R E

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