Module

RegularArtinianParameterChoice.lean

Nyll.EtaleFundamentalGroups.Purity.RegularArtinianParameterChoice

1 declaration indexed from sourceView source ↗

Module documentation

A regular parameter with finite Artinian cokernel

For a finite module whose maximal ideal is not associated, its finitely many associated primes can be included in the primes avoided by an Artinian parameter. The resulting scalar is regular on the finite module and has finite-length cokernel on the Artinian module.

Imports4

Nyll.EtaleFundamentalGroups.Purity.ArtinianParameterChoice
Mathlib.Algebra.Module.Submodule.Pointwise
Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.Regular.IsSMulRegular

Imported by3

theorem

exists_regular_mem_maximalIdeal_finiteLength_quotient

L33 ↗

EtaleFundamentalGroups.Purity.exists_regular_mem_maximalIdeal_finiteLength_quotient

Documentation

A scalar in the maximal ideal can be chosen simultaneously regular on a finite module and with finite-length cokernel on an Artinian module, provided the maximal ideal is not associated to the finite module.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v w
open IsLocalRing
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem exists_regular_mem_maximalIdeal_finiteLength_quotient
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (A : Type w) [AddCommGroup A] [Module R A] [IsArtinian R A]
    (hm : maximalIdeal R ∉ associatedPrimes R M) :
    ∃ x : R, x ∈ maximalIdeal R ∧ IsSMulRegular M x ∧
      IsFiniteLength R (A ⧸ (x • (⊤ : Submodule R A)))

Module documentation

A regular parameter with finite Artinian cokernel

Declarations

exists_regular_mem_maximalIdeal_finiteLength_quotient