NYLL
Module

ModuleInjectiveHull.lean

Nyll.EtaleFundamentalGroups.Purity.ModuleInjectiveHull
1 declaration indexed from sourceView source ↗

Module documentation

Existence of injective hulls for modules

Start with Mathlib's injective presentation of a module and replace the ambient injective module by an injective essential extension of the image. The resulting embedding has essential image and the same universe as the original module. The proof constructs the hull from the preceding maximal essential-extension argument; no hull existence is assumed.

Imports4
Imported by4

Declarations

theorem

exists_module_injective_hull

L34 ↗
EtaleFundamentalGroups.Purity.exists_module_injective_hull
Documentation

Every module admits an embedding with essential image into an injective module in the same universe.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [Ring R]
Lean source · statement
theorem exists_module_injective_hull (M : ModuleCat.{u} R) :
    ∃ (E : ModuleCat.{u} R) (i : M →ₗ[R] E),
      Function.Injective i ∧ IsEssentialSubmodule (LinearMap.range i) ∧
        Module.Injective R E

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