Module

SaturatedPowerDegreeZeroLocalCohomology.lean

Nyll.EtaleFundamentalGroups.Purity.SaturatedPowerDegreeZeroLocalCohomology

2 declarations indexed from sourceView source ↗

Module documentation

Degree-zero local cohomology of saturated-power quotients

The quotient by a saturated ideal is canonically the quotient of the original module by its maximal-ideal-primary component. The first isomorphism theorem identifies these actual quotients before the ideal is specialized to a power. The absence of power torsion then makes degree-zero maximal-ideal local cohomology vanish.

Imports10

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalSaturatedPowers
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomology
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDegreeZeroModule
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModule
Nyll.EtaleFundamentalGroups.Purity.MaximalIdealTorsionQuotient
Mathlib.Algebra.Category.Grp.Zero
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.Quotient.Basic

Imported by2

def

maximalIdealSaturationQuotientEquiv

L40 ↗

EtaleFundamentalGroups.Purity.maximalIdealSaturationQuotientEquiv

Documentation

Quotienting by the contracted primary component gives the actual quotient of the original module by that component.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

def maximalIdealSaturationQuotientEquiv (I : Ideal R) :
    (R ⧸ maximalIdealSaturation I) ≃ₗ[R]
      ((R ⧸ I) ⧸ Ideal.primaryComponent (R ⧸ I) (maximalIdeal R))

theorem

derivedLocalCohomology_maximalIdeal_saturatedPower_quotient_zero

L53 ↗

EtaleFundamentalGroups.Purity.derivedLocalCohomology_maximalIdeal_saturatedPower_quotient_zero