NYLL
Module

InjectiveScalarEndomorphismArtinian.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveScalarEndomorphismArtinian
2 declarations indexed from sourceView source ↗

Module documentation

Double annihilators and the descending chain condition

For an injective module containing the residue field, maps to the module separate every quotient. If all its endomorphisms are scalar maps, this separation gives the double-annihilator equality for every submodule. Annihilators then embed its submodule lattice into the opposite ideal lattice. Over a Noetherian ring, the module is consequently Artinian.

Imports5
Imported by2

Declarations

theorem

torsionBySet_annihilator_eq_of_scalar_endomorphisms

L34 ↗
EtaleFundamentalGroups.Purity.torsionBySet_annihilator_eq_of_scalar_endomorphisms
Documentation

Scalar endomorphisms and injectivity recover each submodule from its annihilator.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
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 torsionBySet_annihilator_eq_of_scalar_endomorphisms
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hscalar : ∀ f : E →ₗ[R] E, ∃ r : R, ∀ z : E, f z = r • z)
    (N : Submodule R E) : Submodule.torsionBySet R E N.annihilator = N
theorem

isArtinian_of_injective_residueField_and_scalar_endomorphisms

L65 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_injective_residueField_and_scalar_endomorphisms
Documentation

If every endomorphism of an injective module containing the residue field is scalar, Noetherianity of the ring implies Artinianness of the module. The complete-local hull supplies the scalar property separately.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
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 isArtinian_of_injective_residueField_and_scalar_endomorphisms
    [IsNoetherianRing R]
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hscalar : ∀ f : E →ₗ[R] E, ∃ r : R, ∀ z : E, f z = r • z) :
    IsArtinian R E

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