NYLL
Module

IdealPowerTorsionInjective.lean

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

Module documentation

Injectivity of ideal-power torsion in an injective module

The primary component of an injective module embeds in an injective power-torsion module. Extending its inclusion into the original module gives a map back whose image remains in the primary component. This is a retraction, so lifting maps into the injective power-torsion module and composing with the retraction proves injectivity of the primary component.

Imports4
Imported by4

Declarations

theorem

moduleInjective_primaryComponent

L30 ↗
EtaleFundamentalGroups.Purity.moduleInjective_primaryComponent
Documentation

The ideal-primary component of an injective module over a Noetherian ring is injective.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem moduleInjective_primaryComponent (I : Ideal R)
    (E : Type u) [AddCommGroup E] [Module R E] [Module.Injective R E] :
    Module.Injective R (Ideal.primaryComponent E I)

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