Module

InjectiveModuleLocalization.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveModuleLocalization

2 declarations indexed from sourceView source ↗

Module documentation

Localization of an injective module

Over a Noetherian ring the localization map of an injective module is surjective. Stabilization of the kernels of powers of a denominator makes an appropriate division map well-defined on a principal ideal; injectivity extends that map to the ring. For a principal localization the kernel is exactly the principal ideal-power torsion submodule.

Imports6

Mathlib.Algebra.Module.Injective
Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.Module.Torsion.PrimaryComponent
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Noetherian.Defs

Imported by3

theorem

localizedModule_mkLinearMap_surjective_of_injective

L35 ↗

EtaleFundamentalGroups.Purity.localizedModule_mkLinearMap_surjective_of_injective

Documentation

Localization of an injective module over a Noetherian ring is a quotient of the original module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (E : Type u) [AddCommGroup E] [Module R E]

Lean source · statement

theorem localizedModule_mkLinearMap_surjective_of_injective
    [IsNoetherianRing R] [Module.Injective R E] (S : Submonoid R) :
    Function.Surjective (LocalizedModule.mkLinearMap S E)

theorem

ker_localizedModule_mkLinearMap_powers

L97 ↗

EtaleFundamentalGroups.Purity.ker_localizedModule_mkLinearMap_powers