NYLL
Module

InjectiveHullFiniteLengthDual.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveHullFiniteLengthDual
7 declarations indexed from sourceView source ↗

Module documentation

Finite-length duals into an injective residue-field hull

Restriction of maps into an injective module is surjective. Together with left exactness of Hom, this gives a short exact sequence dual to a submodule-quotient sequence. The dual of a simple module is identified with the residue field using the socle of its injective hull. Induction along a composition series then shows that duality preserves length. The evaluation map is injective because maps into the hull separate elements. Equality of finite lengths makes it an isomorphism.

Imports13
Imported by3

Declarations

theorem

injective_dualRestriction_surjective

L41 ↗
EtaleFundamentalGroups.Purity.injective_dualRestriction_surjective
Documentation

Every map from a submodule into an injective module extends to the ambient module, so the linear restriction map is surjective.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R E : Type u} [CommRing R] [AddCommGroup E] [Module R E]
Lean source · statement
theorem injective_dualRestriction_surjective [Module.Injective R E]
    {M : Type v} [AddCommGroup M] [Module R M] (N : Submodule R M) :
    Function.Surjective (LinearMap.lcomp R E N.subtype)
theorem

length_linearMap_to_residueFieldHull_of_simple

L51 ↗
EtaleFundamentalGroups.Purity.length_linearMap_to_residueFieldHull_of_simple
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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem length_linearMap_to_residueFieldHull_of_simple
    (i : (R ⧸ IsLocalRing.maximalIdeal R) →ₗ[R] E)
    (hi : Function.Injective i) (hess : IsEssentialSubmodule (LinearMap.range i))
    {M : Type v} [AddCommGroup M] [Module R M] [IsSimpleModule R M] :
    Module.length R (M →ₗ[R] E) = Module.length R M
theorem

length_linearMap_to_residueFieldHull_of_finiteLength

L72 ↗
EtaleFundamentalGroups.Purity.length_linearMap_to_residueFieldHull_of_finiteLength
Documentation

Duality into an injective hull of the residue field preserves the length of 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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem length_linearMap_to_residueFieldHull_of_finiteLength
    [Module.Injective 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] (hM : IsFiniteLength R M) :
    Module.length R (M →ₗ[R] E) = Module.length R M
theorem

isFiniteLength_linearMap_to_residueFieldHull

L104 ↗
EtaleFundamentalGroups.Purity.isFiniteLength_linearMap_to_residueFieldHull
Documentation

The dual of a finite-length module into an injective residue-field hull again has finite length.

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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem isFiniteLength_linearMap_to_residueFieldHull
    [Module.Injective 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] (hM : IsFiniteLength R M) :
    IsFiniteLength R (M →ₗ[R] E)
theorem

bijective_residueFieldHullEvaluation_of_finiteLength

L118 ↗
EtaleFundamentalGroups.Purity.bijective_residueFieldHullEvaluation_of_finiteLength
Documentation

Evaluation into the double dual is bijective on finite-length modules. Injectivity separates elements using the residue field; surjectivity follows because a proper submodule has strictly smaller length.

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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem bijective_residueFieldHullEvaluation_of_finiteLength
    [Module.Injective 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] (hM : IsFiniteLength R M) :
    Function.Bijective (residueFieldHullEvaluation R E M)
def

residueFieldHullBidualEquiv

L150 ↗
EtaleFundamentalGroups.Purity.residueFieldHullBidualEquiv
Documentation

The canonical evaluation isomorphism for finite-length modules.

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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
def residueFieldHullBidualEquiv
    [Module.Injective 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] (hM : IsFiniteLength R M) :
    M ≃ₗ[R] ((M →ₗ[R] E) →ₗ[R] E)
theorem

residueFieldHullBidualEquiv_apply

L159 ↗
EtaleFundamentalGroups.Purity.residueFieldHullBidualEquiv_apply
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] [AddCommGroup E] [Module R E]
variable [IsLocalRing R]
Lean source · statement
theorem residueFieldHullBidualEquiv_apply
    [Module.Injective 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]
    (hM : IsFiniteLength R M) (x : M) (f : M →ₗ[R] E) :
    residueFieldHullBidualEquiv i hi hess hM x f = f x

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