ModuleIdealPowerTorsionInjectivePresentation.lean
Nyll.EtaleFundamentalGroups.Purity.IdealPowerTorsionInjectivePresentation
3 declarations indexed from sourceView source ↗ Module documentation
Injective presentations preserving ideal-power torsion
The injective hull of an ideal-power torsion module over a Noetherian ring is again ideal-power torsion because its embedded image is essential. The quotient inherits power torsion from the hull. The inclusion and the quotient map form a concrete short exact coefficient complex.
Declarations
EtaleFundamentalGroups.Purity.injectivePresentationShortComplex
DocumentationThe coefficient complex associated with a linear map into a module. Its objects are definitionally M, E, and E ⧸ LinearMap.range i.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
open CategoryTheory
universe u
variable {R : Type u} [CommRing R]
EtaleFundamentalGroups.Purity.injectivePresentationShortComplex_shortExact
DocumentationAn injective linear map and its range quotient form a short exact coefficient complex.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
open CategoryTheory
universe u
variable {R : Type u} [CommRing R]
EtaleFundamentalGroups.Purity.exists_idealPowerTorsion_injective_presentation
DocumentationEvery ideal-power torsion module over a Noetherian ring embeds into an injective ideal-power torsion module with ideal-power torsion quotient.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
open CategoryTheory
universe u
variable {R : Type u} [CommRing R]