ModuleDerivedLocalCohomology.lean
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomology
7 declarations indexed from sourceView source ↗ Module documentation
Local cohomology from derived-category Ext
Mathlib's existing localCohomology functor is defined using the legacy left-derived Ext functor. The long exact Ext sequence, on the other hand, is currently available for CategoryTheory.Abelian.Ext. This file names the corresponding ideal-power diagram and its colimit. It provides the common object used by the derived Mayer--Vietoris construction without asserting a comparison with the legacy implementation.
Declarations
EtaleFundamentalGroups.derivedExtContravariantFunctor
DocumentationDerived Ext in the first variable, regarded as a contravariant functor.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
section General
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
EtaleFundamentalGroups.derivedLocalCohomologyDiagram
DocumentationThe derived-category Ext diagram associated to a diagram of ideals.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
EtaleFundamentalGroups.derivedLocalCohomologyOfDiagram
DocumentationThe derived local-cohomology object computed from a diagram of ideals.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
EtaleFundamentalGroups.derivedLocalCohomologyPowersDiagram
DocumentationThe derived-category Ext diagram along all powers of an ideal.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
section Modules
variable {R : Type u} [CommRing R]
EtaleFundamentalGroups.derivedLocalCohomology
DocumentationLocal cohomology modeled as the colimit of derived-category Ext groups.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
section Modules
variable {R : Type u} [CommRing R]
EtaleFundamentalGroups.derivedLocalCohomologyPowersDiagram_obj
DocumentationThe object at exponent n is the expected derived Ext group against R / I^n.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
section Modules
variable {R : Type u} [CommRing R]
EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_subsingleton_ext_powers
DocumentationIf every derived Ext group in the powers diagram is trivial, then so is its colimit.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
section Modules
variable {R : Type u} [CommRing R]