NYLL
Module

DerivedLocalCohomologyDimensionOne.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDimensionOne
8 declarations indexed from sourceView source ↗

Module documentation

Degree-one nonvanishing for derived local cohomology

For a nonzero nonunit x in a local domain, the extension class of 0 → R → R → R/(x^n) → 0 supplies a class in degree one which survives every transition in the principal ideal-powers diagram.

Imports5
Imported by1

Declarations

def

principalPowerShortComplex

L37 ↗
EtaleFundamentalGroups.principalPowerShortComplex
Documentation

The standard two-term short complex resolving the quotient by (x)^n, written with the exact quotient object used by the local-cohomology powers diagram.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
def principalPowerShortComplex (x : R) (n : ℕ) :
    ShortComplex (ModuleCat.{u} R)
theorem

principalPowerShortComplex_shortExact

L48 ↗
EtaleFundamentalGroups.principalPowerShortComplex_shortExact
Documentation

Regularity of x makes the principal power short complex short exact.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalPowerShortComplex_shortExact
    (x : R) (n : ℕ) (hx : IsSMulRegular R x) :
    (principalPowerShortComplex x n).ShortExact
def

principalPowerExtClass

L59 ↗
EtaleFundamentalGroups.principalPowerExtClass
Documentation

The degree-one extension class attached to the n-th principal power quotient.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
def principalPowerExtClass
    (x : R) (n : ℕ) (hx : IsSMulRegular R x) :
    Abelian.Ext
      (ModuleCat.of R (R ⧸ (Ideal.span {x}) ^ n))
      (ModuleCat.of R R) 1
def

principalPowerShortComplexTransition

L68 ↗
EtaleFundamentalGroups.principalPowerShortComplexTransition
Documentation

The compatible morphism from the m-th principal power short complex to the n-th one.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · full declaration
def principalPowerShortComplexTransition
    (x : R) {n m : ℕ} (h : n ≤ m) :
    principalPowerShortComplex x m ⟶
      principalPowerShortComplex x n where
  τ₁ := ModuleCat.ofHom (LinearMap.lsmul R R (x ^ (m - n)))
  τ₂ := 𝟙 _
  τ₃ := ModuleCat.ofHom (principalPowerQuotientTransition x h)
  comm₁₂ := by
    ext
    change x ^ n * (x ^ (m - n) * 1) = x ^ m * 1
    rw [← mul_assoc, mul_comm (x ^ n), pow_sub_mul_pow x h]
  comm₂₃ := by
    ext
    rfl
theorem

principalPowerExtClass_transition

L85 ↗
EtaleFundamentalGroups.principalPowerExtClass_transition
Documentation

The principal extension classes transform by the expected power of the parameter under a quotient transition.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalPowerExtClass_transition
    (x : R) (hx : IsSMulRegular R x) {n m : ℕ} (h : n ≤ m) :
    (Abelian.Ext.mk₀
        (ModuleCat.ofHom (principalPowerQuotientTransition x h))).comp
        (principalPowerExtClass x n hx) (zero_add 1) =
      x ^ (m - n) • principalPowerExtClass x m hx
theorem

principalPowerExtClass_one_transition_ne_zero

L99 ↗
EtaleFundamentalGroups.principalPowerExtClass_one_transition_ne_zero
Documentation

Starting from the first power, the transported principal extension class is nonzero at every later power.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalPowerExtClass_one_transition_ne_zero
    [IsDomain R] [IsLocalRing R]
    (x : R) (hxmem : x ∈ IsLocalRing.maximalIdeal R)
    (hx0 : x ≠ 0) (m : ℕ) (hm : 1 ≤ m) :
    x ^ (m - 1) • principalPowerExtClass x m
      (IsSMulRegular.of_ne_zero hx0) ≠ 0
theorem

derivedLocalCohomology_span_singleton_not_isZero_one

L153 ↗
EtaleFundamentalGroups.derivedLocalCohomology_span_singleton_not_isZero_one
Documentation

A nonzero element of the maximal ideal of a local domain gives nonvanishing degree-one derived local cohomology at its principal ideal.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section Principal
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_span_singleton_not_isZero_one
    [IsDomain R] [IsLocalRing R]
    (x : R) (hxmem : x ∈ IsLocalRing.maximalIdeal R) (hx0 : x ≠ 0) :
    ¬ IsZero
      (derivedLocalCohomology (Ideal.span {x})
        (ModuleCat.of R R) 1)
theorem

derivedLocalCohomology_maximalIdeal_not_isZero_one_of_ringKrullDim_eq_one

L174 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_not_isZero_one_of_ringKrullDim_eq_one
Documentation

Grothendieck top nonvanishing in dimension one for a Noetherian local domain.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem derivedLocalCohomology_maximalIdeal_not_isZero_one_of_ringKrullDim_eq_one
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hdim : ringKrullDim R = (1 : WithBot ℕ∞)) :
    ¬ IsZero
      (derivedLocalCohomology (IsLocalRing.maximalIdeal R)
        (ModuleCat.of R R) 1)

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