NYLL
Module

FiniteLengthInjectiveEmbedding.lean

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

Module documentation

Embedding finite-length modules into finite products of a residue-field hull

A finite generating family of the dual gives finitely many maps that separate the original finite-length module. Their product is an embedding into a finite product of injective hulls. An embedding of an essential submodule extends injectively to the ambient module. If the hull is Artinian, the ambient module is Artinian as well.

Imports11
Imported by3

Declarations

theorem

exists_injective_linearMap_pi_of_finiteLength

L38 ↗
EtaleFundamentalGroups.Purity.exists_injective_linearMap_pi_of_finiteLength
Documentation

Finitely many maps into an injective residue-field hull jointly embed each finite-length module.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R E : Type u} [CommRing R] [IsLocalRing R]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem exists_injective_linearMap_pi_of_finiteLength
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hi : Function.Injective i) (hess : IsEssentialSubmodule (LinearMap.range i))
    {M : Type v} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) :
    ∃ n : ℕ, ∃ j : M →ₗ[R] (Fin n → E), Function.Injective j
theorem

isArtinian_of_finiteLength_essential_submodule

L69 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_finiteLength_essential_submodule
Documentation

Extending an embedding of an essential finite-length submodule into a finite product of Artinian injective hulls proves that the ambient module is Artinian.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R E : Type u} [CommRing R] [IsLocalRing R]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]
Lean source · statement
theorem isArtinian_of_finiteLength_essential_submodule
    [IsArtinian R E]
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hi : Function.Injective i) (hess : IsEssentialSubmodule (LinearMap.range i))
    {M : Type v} [AddCommGroup M] [Module R M]
    (N : Submodule R M) (hN : IsEssentialSubmodule N) (hlen : IsFiniteLength R N) :
    IsArtinian R M

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