Module

InjectiveResidueFieldCogenerator.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveResidueFieldCogenerator

4 declarations indexed from sourceView source ↗

Module documentation

Separation by an injective module containing the residue field

A nonzero element generates a cyclic module whose defining ideal is contained in the maximal ideal. Its quotient onto the residue field, followed by the given embedding, extends to the entire module by injectivity. Thus maps to the injective module separate elements, and the associated evaluation map into the double dual is injective.

Imports7

Mathlib.Algebra.Module.Injective
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.LinearAlgebra.BilinearMap
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.Span.Basic
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Imported by6

def

residueFieldHullEvaluation

L32 ↗

EtaleFundamentalGroups.Purity.residueFieldHullEvaluation

Documentation

Evaluation into the double dual with values in a fixed module.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v w
open IsLocalRing

Lean source · statement

def residueFieldHullEvaluation (R : Type u) (E : Type v) (M : Type w)
    [CommRing R] [AddCommGroup E] [Module R E]
    [AddCommGroup M] [Module R M] : M →ₗ[R] ((M →ₗ[R] E) →ₗ[R] E)

theorem

residueFieldHullEvaluation_apply

L37 ↗

EtaleFundamentalGroups.Purity.residueFieldHullEvaluation_apply

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v w
open IsLocalRing

Lean source · statement

theorem residueFieldHullEvaluation_apply
    (R : Type u) (E : Type v) (M : Type w)
    [CommRing R] [AddCommGroup E] [Module R E]
    [AddCommGroup M] [Module R M] (x : M) (f : M →ₗ[R] E) :
    residueFieldHullEvaluation R E M x f = f x

theorem

exists_linearMap_apply_ne_zero_of_injective_residueField

L48 ↗

EtaleFundamentalGroups.Purity.exists_linearMap_apply_ne_zero_of_injective_residueField

Documentation

Maps into an injective module containing the residue field detect every nonzero element. Essentiality of the residue-field image is not needed.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v w
open IsLocalRing
variable {R E : Type u} [CommRing R] [IsLocalRing R]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]

Lean source · statement

theorem exists_linearMap_apply_ne_zero_of_injective_residueField
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    {M : Type v} [AddCommGroup M] [Module R M] (x : M) (hx : x ≠ 0) :
    ∃ f : M →ₗ[R] E, f x ≠ 0

theorem

injective_eval_to_injective_residueField

L80 ↗

EtaleFundamentalGroups.Purity.injective_eval_to_injective_residueField

Documentation

Evaluation into the double dual is injective when the target is injective and contains the residue field.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v w
open IsLocalRing
variable {R E : Type u} [CommRing R] [IsLocalRing R]
variable [AddCommGroup E] [Module R E] [Module.Injective R E]

Lean source · statement

theorem injective_eval_to_injective_residueField
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (M : Type v) [AddCommGroup M] [Module R M] :
    Function.Injective (residueFieldHullEvaluation R E M)

Module documentation

Separation by an injective module containing the residue field

Declarations

residueFieldHullEvaluation

residueFieldHullEvaluation_apply

exists_linearMap_apply_ne_zero_of_injective_residueField

injective_eval_to_injective_residueField