EtaleFundamentalGroups.Purity.finite_linearMap_to_completeLocal_residueFieldHull_of_artinian
The dual into a residue-field injective hull of an Artinian module whose elements are killed by maximal-ideal powers is finitely generated over the complete Noetherian local ring.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
open scoped BigOperators
variable {R E : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]Lean source · statement
theorem finite_linearMap_to_completeLocal_residueFieldHull_of_artinian
(i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
(hess : IsEssentialSubmodule (LinearMap.range i))
{A : Type v} [AddCommGroup A] [Module R A] [IsArtinian R A]
(hA : ∀ z : A, ∃ n : ℕ, ∀ a ∈ maximalIdeal R ^ n, a • z = 0) :
Module.Finite R (A →ₗ[R] E)