NYLL
Module

IdealQuotientMayerVietorisDerivedExtSupports.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisDerivedExtSupports
4 declarations indexed from sourceView source ↗

Module documentation

Support terms in the derived local-cohomology Mayer--Vietoris sequence

The third term in degree n₀ of the finite derived-Ext sequence is the simultaneous-intersection support, and the following term in degree n₁ is the simultaneous-supremum support. Cofinality identifies their filtered colimits with derived local cohomology at I ⊓ J and I ⊔ J.

Imports2
Imported by2

Declarations

def

idealQuotientMayerVietorisDerivedExtPowersInfTermIso

L31 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersInfTermIso
Documentation

The index-two term of the derived-Ext powers diagram is the derived local-cohomology diagram along simultaneous intersections.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersInfTermIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨2, by omega⟩) ≅
      derivedLocalCohomologyDiagram (idealInfPowersDiagram I J) M n₀ :=
  Iso.refl _
def

idealQuotientMayerVietorisDerivedExtPowersSupTermIso

L42 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersSupTermIso
Documentation

The index-three term of the derived-Ext powers diagram is the derived local-cohomology diagram along simultaneous suprema.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersSupTermIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨3, by omega⟩) ≅
      derivedLocalCohomologyDiagram (idealSupPowersDiagram I J) M n₁ :=
  Iso.refl _
def

idealQuotientMayerVietorisDerivedExtPowersInfColimitIso

L53 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersInfColimitIso
Documentation

The colimit of the index-two term is local cohomology supported on the intersection.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersInfColimitIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    colimit (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨2, by omega⟩) ≅
      derivedLocalCohomology (I ⊓ J) M n₀ :=
  HasColimit.isoOfNatIso
      (idealQuotientMayerVietorisDerivedExtPowersInfTermIso
        I J M n₀ n₁ h) ≪≫
    derivedLocalCohomologyOfInfPowersIso I J M n₀
def

idealQuotientMayerVietorisDerivedExtPowersSupColimitIso

L67 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersSupColimitIso
Documentation

The colimit of the index-three term is local cohomology supported on the supremum.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersSupColimitIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    colimit (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨3, by omega⟩) ≅
      derivedLocalCohomology (I ⊔ J) M n₁ :=
  HasColimit.isoOfNatIso
      (idealQuotientMayerVietorisDerivedExtPowersSupTermIso
        I J M n₀ n₁ h) ≪≫
    derivedLocalCohomologyOfSupPowersIso I J M n₁

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