NYLL
Module

SymbolicPowerDegreeZeroLocalCohomology.lean

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

Module documentation

Degree-zero maximal-support cohomology of symbolic-power quotients

Multiplication by an element outside a prime is injective on every symbolic-power quotient. For a nonmaximal prime in a local ring, choose such an element in the maximal ideal. Its powers detect the vanishing of maximal-ideal-power torsion, hence of degree-zero local cohomology.

Imports8
Imported by1

Declarations

theorem

mul_mem_primeSymbolicPower_iff_of_notMem

L35 ↗
EtaleFundamentalGroups.Purity.mul_mem_primeSymbolicPower_iff_of_notMem
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open CategoryTheory Limits IsLocalRing
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem mul_mem_primeSymbolicPower_iff_of_notMem
    (P : Ideal R) [P.IsPrime] (n : ℕ) {s x : R} (hs : s ∉ P) :
    s * x ∈ primeSymbolicPower P n ↔ x ∈ primeSymbolicPower P n
theorem

smul_eq_zero_primeSymbolicPower_quotient

L46 ↗
EtaleFundamentalGroups.Purity.smul_eq_zero_primeSymbolicPower_quotient
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open CategoryTheory Limits IsLocalRing
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem smul_eq_zero_primeSymbolicPower_quotient
    (P : Ideal R) [P.IsPrime] (n : ℕ) {s : R} (hs : s ∉ P)
    (z : R ⧸ primeSymbolicPower P n) (hz : s • z = 0) : z = 0
theorem

derivedLocalCohomology_maximalIdeal_primeSymbolicPower_quotient_zero

L57 ↗
EtaleFundamentalGroups.Purity.derivedLocalCohomology_maximalIdeal_primeSymbolicPower_quotient_zero
Documentation

A quotient by a symbolic power of a nonmaximal prime has no maximal-support local cohomology in degree zero.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
open CategoryTheory Limits IsLocalRing
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_maximalIdeal_primeSymbolicPower_quotient_zero
    [IsLocalRing R] (P : Ideal R) [P.IsPrime]
    (hP : P ≠ maximalIdeal R) (n : ℕ) :
    IsZero (derivedLocalCohomology (maximalIdeal R)
      (ModuleCat.of R (R ⧸ primeSymbolicPower P n)) 0)

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