Module

DerivedLocalCohomologyScalarQuotient.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyScalarQuotient

2 declarations indexed from sourceView source ↗

Module documentation

Scalar quotients of local cohomology

For a regular scalar, the coefficient long exact sequence identifies local cohomology of the scalar quotient with the quotient of local cohomology by that scalar whenever the next cohomological degree vanishes.

Imports7

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModuleCoefficients
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyPrincipalAnnihilated
Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.Algebra.Exact.Basic
Mathlib.Algebra.Module.Submodule.Pointwise
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.RingTheory.Regular.Category

Imported by2

def

derivedLocalCohomologyModuleScalarQuotientEquiv

L34 ↗

EtaleFundamentalGroups.derivedLocalCohomologyModuleScalarQuotientEquiv

Documentation

If the next local-cohomology group vanishes, passing to the quotient by a regular scalar commutes with local cohomology in the current degree.

Source context 5 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits
open scoped Pointwise
variable {R : Type u} [CommRing R]

Lean source · statement

def derivedLocalCohomologyModuleScalarQuotientEquiv
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ)
    (x : R) (hx : IsSMulRegular M x)
    (hzero : IsZero (derivedLocalCohomology I M (n + 1))) :
    (derivedLocalCohomologyModule I M n ⧸
      x • (⊤ : Submodule R (derivedLocalCohomologyModule I M n))) ≃ₗ[R]
        derivedLocalCohomologyModule I (ModuleCat.smulShortComplex M x).X₃ n

theorem

derivedLocalCohomologyModuleScalarQuotientEquiv_apply_mk

L75 ↗

EtaleFundamentalGroups.derivedLocalCohomologyModuleScalarQuotientEquiv_apply_mk