NYLL
Module

ArtinianParameterChoice.lean

Nyll.EtaleFundamentalGroups.Purity.ArtinianParameterChoice
3 declarations indexed from sourceView source ↗

Module documentation

Choosing parameters on Artinian modules

A finite secondary decomposition has finitely many radical annihilators. Prime avoidance chooses a member of the maximal ideal outside all the nonmaximal ones, together with any prescribed finite set of nonmaximal prime ideals. Multiplication is surjective on those secondary summands. The remaining summands have maximal radical annihilator and finite length, so the scalar cokernel has finite length as well.

This is the Artinian parameter-choice step in the induction for top local cohomology. It uses secondary decomposition rather than Matlis duality.

Imports6
Imported by2

Declarations

theorem

finite_of_artinian_of_radical_annihilator_eq_maximalIdeal

L39 ↗
EtaleFundamentalGroups.Purity.finite_of_artinian_of_radical_annihilator_eq_maximalIdeal
Source context 6 commands

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

noncomputable section
open IsLocalRing
open scoped Pointwise
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem finite_of_artinian_of_radical_annihilator_eq_maximalIdeal
    [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [IsArtinian R M]
    (hAnn : (Module.annihilator R M).radical = maximalIdeal R) :
    Module.Finite R M
theorem

exists_mem_maximalIdeal_avoiding_finite_primes

L61 ↗
EtaleFundamentalGroups.Purity.exists_mem_maximalIdeal_avoiding_finite_primes
Source context 6 commands

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

noncomputable section
open IsLocalRing
open scoped Pointwise
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_mem_maximalIdeal_avoiding_finite_primes
    (s : Finset (Ideal R))
    (hs : ∀ P : Ideal R, P ∈ s → P.IsPrime ∧ P ≠ maximalIdeal R) :
    ∃ x : R, x ∈ maximalIdeal R ∧ ∀ P : Ideal R, P ∈ s → x ∉ P
theorem

exists_mem_maximalIdeal_avoiding_primes_finiteLength_quotient

L80 ↗
EtaleFundamentalGroups.Purity.exists_mem_maximalIdeal_avoiding_primes_finiteLength_quotient
Documentation

A parameter can avoid any fixed finite set of nonmaximal primes while having finite-length cokernel on an Artinian module.

Source context 6 commands

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

noncomputable section
open IsLocalRing
open scoped Pointwise
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem exists_mem_maximalIdeal_avoiding_primes_finiteLength_quotient
    [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [IsArtinian R M]
    (t : Finset (Ideal R))
    (ht : ∀ P : Ideal R, P ∈ t → P.IsPrime ∧ P ≠ maximalIdeal R) :
    ∃ x : R, x ∈ maximalIdeal R ∧
      (∀ P : Ideal R, P ∈ t → x ∉ P) ∧
      IsFiniteLength R (M ⧸ (x • (⊤ : Submodule R M)))

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