NYLL
Module

ResidueFieldHullFiniteTruncation.lean

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

Module documentation

Scalar endomorphisms on finite truncations of a residue-field hull

An endomorphism of an injective residue-field hull restricts to scalar multiplication on the elements annihilated by an ideal with finite-length quotient. Finite biduality supplies the scalar as a class in that quotient. Separation by the injective hull proves that its residue class is unique.

Imports5
Imported by2

Declarations

theorem

exists_smul_eq_on_torsionBySet_of_finiteLength_quotient

L34 ↗
EtaleFundamentalGroups.Purity.exists_smul_eq_on_torsionBySet_of_finiteLength_quotient
Documentation

On the submodule annihilated by an ideal with finite-length quotient, every endomorphism of an injective residue-field hull is scalar.

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 exists_smul_eq_on_torsionBySet_of_finiteLength_quotient
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (hess : IsEssentialSubmodule (LinearMap.range i))
    (J : Ideal R) (hJ : IsFiniteLength R (R ⧸ J)) (f : E →ₗ[R] E) :
    ∃ r : R, ∀ z : E, (∀ a : R, a ∈ J → a • z = 0) → f z = r • z
theorem

sub_mem_ideal_of_smul_eq_zero_on_torsionBySet

L58 ↗
EtaleFundamentalGroups.Purity.sub_mem_ideal_of_smul_eq_zero_on_torsionBySet
Documentation

If the difference of two scalars kills all elements annihilated by J, that difference belongs to J. This separation statement does not require the quotient by J to have finite length.

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 sub_mem_ideal_of_smul_eq_zero_on_torsionBySet
    (i : (R ⧸ maximalIdeal R) →ₗ[R] E) (hi : Function.Injective i)
    (J : Ideal R) (r s : R)
    (hrs : ∀ z : E, (∀ a : R, a ∈ J → a • z = 0) → (r - s) • z = 0) :
    r - s ∈ J

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