NYLL
Module

DerivedLocalCohomologyCoefficientsExact.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyCoefficientsExact
22 declarations indexed from sourceView source ↗

Module documentation

Exactness in the coefficients of derived local cohomology

For a short exact complex of coefficient modules, the covariant long exact sequence of derived Ext is natural in the first variable. Applying this to the quotients by all powers of an ideal gives an objectwise exact diagram. Exactness of filtered colimits then gives exactness of every adjacent three-term window after passing to derived local cohomology.

Imports2
Imported by7

Declarations

theorem

derivedExtContravariantMap_postcomp

L34 ↗
EtaleFundamentalGroups.derivedExtContravariantMap_postcomp
Documentation

Precomposition in the first variable of Ext commutes with postcomposition by a degree-zero morphism in the second variable.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantMap_postcomp
    {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') (n : ℕ) :
    AddCommGrpCat.ofHom
          ((CategoryTheory.Abelian.Ext.mk₀ g).postcomp X' (add_zero n)) ≫
        derivedExtContravariantMap f Y' n =
      derivedExtContravariantMap f Y n ≫
        AddCommGrpCat.ofHom
          ((CategoryTheory.Abelian.Ext.mk₀ g).postcomp X (add_zero n))
theorem

derivedExtContravariantMap_covariantConnecting

L56 ↗
EtaleFundamentalGroups.derivedExtContravariantMap_covariantConnecting
Documentation

Precomposition in the first variable of Ext commutes with the connecting morphism of a short exact complex in the second variable.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantMap_covariantConnecting
    {X X' : C} {S : ShortComplex C} (hS : S.ShortExact)
    (f : X ⟶ X') (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    AddCommGrpCat.ofHom (hS.extClass.postcomp X' h) ≫
        derivedExtContravariantMap f S.X₁ n₁ =
      derivedExtContravariantMap f S.X₃ n₀ ≫
        AddCommGrpCat.ofHom (hS.extClass.postcomp X h)
def

derivedExtCovariantSequenceMap

L77 ↗
EtaleFundamentalGroups.derivedExtCovariantSequenceMap
Documentation

A morphism in the first variable induces a contravariant morphism between the covariant six-term Ext sequences of a fixed short exact complex.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
def derivedExtCovariantSequenceMap
    {X X' : C} {S : ShortComplex C} (hS : S.ShortExact) (f : X ⟶ X')
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    CategoryTheory.Abelian.Ext.covariantSequence X' hS n₀ n₁ h ⟶
      CategoryTheory.Abelian.Ext.covariantSequence X hS n₀ n₁ h
theorem

derivedExtCovariantSequenceMap_id

L98 ↗
EtaleFundamentalGroups.derivedExtCovariantSequenceMap_id
Documentation

The map of covariant six-term sequences induced by an identity in the first variable is the identity.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtCovariantSequenceMap_id
    {X : C} {S : ShortComplex C} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    derivedExtCovariantSequenceMap hS (𝟙 X) n₀ n₁ h = 𝟙 _
theorem

derivedExtCovariantSequenceMap_comp

L119 ↗
EtaleFundamentalGroups.derivedExtCovariantSequenceMap_comp
Documentation

Composition law for the contravariant maps between covariant six-term Ext sequences.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtCovariantSequenceMap_comp
    {X₁ X₂ X₃ : C} {S : ShortComplex C} (hS : S.ShortExact)
    (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    derivedExtCovariantSequenceMap hS g n₀ n₁ h ≫
        derivedExtCovariantSequenceMap hS f n₀ n₁ h =
      derivedExtCovariantSequenceMap hS (f ≫ g) n₀ n₁ h
def

derivedExtCovariantSequenceDiagram

L156 ↗
EtaleFundamentalGroups.derivedExtCovariantSequenceDiagram
Documentation

A diagram in the first variable gives a contravariant diagram of the covariant six-term Ext sequences of a fixed short exact complex.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
variable {D : Type*} [Category D]
Lean source · full declaration
def derivedExtCovariantSequenceDiagram
    (F : D ⥤ C) {S : ShortComplex C} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Dᵒᵖ ⥤ ComposableArrows AddCommGrpCat.{w} 5 where
  obj d := CategoryTheory.Abelian.Ext.covariantSequence
    (F.obj (unop d)) hS n₀ n₁ h
  map {d e} f := derivedExtCovariantSequenceMap hS
    (F.map f.unop) n₀ n₁ h
  map_id d := by
    dsimp
    rw [F.map_id]
    apply derivedExtCovariantSequenceMap_id
  map_comp f g := by
    dsimp
    rw [F.map_comp]
    symm
    apply derivedExtCovariantSequenceMap_comp
theorem

derivedExtCovariantSequenceDiagram_obj_exact

L176 ↗
EtaleFundamentalGroups.derivedExtCovariantSequenceDiagram_obj_exact
Documentation

Every object of the diagram of covariant six-term Ext sequences is exact.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section CovariantSequenceNaturality
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
variable {D : Type*} [Category D]
Lean source · statement
theorem derivedExtCovariantSequenceDiagram_obj_exact
    (F : D ⥤ C) {S : ShortComplex C} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (d : Dᵒᵖ) :
    ((derivedExtCovariantSequenceDiagram F hS n₀ n₁ h).obj d).Exact
def

derivedLocalCohomologyCoefficientsPowersSequenceDiagram

L191 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsPowersSequenceDiagram
Documentation

The covariant six-term derived-Ext sequences of a short exact coefficient complex, assembled 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 w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsPowersSequenceDiagram
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (ℕᵒᵖ)ᵒᵖ ⥤ ComposableArrows AddCommGrpCat.{u} 5
theorem

derivedLocalCohomologyCoefficientsPowersSequenceDiagram_obj_exact

L202 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsPowersSequenceDiagram_obj_exact
Documentation

Every powers-indexed covariant six-term derived-Ext sequence is exact.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsPowersSequenceDiagram_obj_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) (d : (ℕᵒᵖ)ᵒᵖ) :
    ((derivedLocalCohomologyCoefficientsPowersSequenceDiagram
      I hS n₀ n₁ h).obj d).Exact
def

derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex

L214 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex
Documentation

An adjacent three-term window in the powers-indexed covariant six-term derived-Ext sequence.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    ShortComplex ((ℕᵒᵖ)ᵒᵖ ⥤ AddCommGrpCat.{u})
theorem

derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex_exact

L228 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex_exact
Documentation

Every adjacent three-term window is exact in the powers-diagram category.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    (derivedLocalCohomologyCoefficientsPowersAdjacentShortComplex
      I hS n₀ n₁ h k hk).Exact
def

derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex

L243 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex
Documentation

The filtered colimits of an adjacent three-term window of the powers-indexed coefficient sequence.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    ShortComplex AddCommGrpCat.{u}
theorem

derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex_exact

L254 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex_exact
Documentation

Filtered colimits preserve exactness of every adjacent three-term window in the coefficient long exact sequence for derived local cohomology.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    (derivedLocalCohomologyCoefficientsAdjacentColimitShortComplex
      I hS n₀ n₁ h k hk).Exact
def

derivedLocalCohomologyCoefficientsFirstMap

L268 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsFirstMap
Documentation

The map on derived local cohomology induced by the first morphism of a short exact coefficient complex.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsFirstMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomology I S.X₁ n ⟶
      derivedLocalCohomology I S.X₂ n
def

derivedLocalCohomologyCoefficientsSecondMap

L278 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap
Documentation

The map on derived local cohomology induced by the second morphism of a short exact coefficient complex.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsSecondMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomology I S.X₂ n ⟶
      derivedLocalCohomology I S.X₃ n
def

derivedLocalCohomologyCoefficientsConnectingMap

L288 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsConnectingMap
Documentation

The connecting map on derived local cohomology induced by a short exact coefficient complex.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyCoefficientsConnectingMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomology I S.X₃ n ⟶
      derivedLocalCohomology I S.X₁ (n + 1)
theorem

derivedLocalCohomologyCoefficientsFirstMap_comp_secondMap

L296 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsFirstMap_comp_secondMap
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsFirstMap_comp_secondMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomologyCoefficientsFirstMap I hS n ≫
        derivedLocalCohomologyCoefficientsSecondMap I hS n = 0
theorem

derivedLocalCohomologyCoefficientsSecondMap_comp_connectingMap

L305 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap_comp_connectingMap
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsSecondMap_comp_connectingMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomologyCoefficientsSecondMap I hS n ≫
        derivedLocalCohomologyCoefficientsConnectingMap I hS n = 0
theorem

derivedLocalCohomologyCoefficientsConnectingMap_comp_firstMap

L314 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsConnectingMap_comp_firstMap
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsConnectingMap_comp_firstMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    derivedLocalCohomologyCoefficientsConnectingMap I hS n ≫
        derivedLocalCohomologyCoefficientsFirstMap I hS (n + 1) = 0
theorem

derivedLocalCohomologyCoefficients_sameDegree_exact

L324 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficients_sameDegree_exact
Documentation

Exactness at the middle coefficient in a fixed degree.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficients_sameDegree_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk
      (derivedLocalCohomologyCoefficientsFirstMap I hS n)
      (derivedLocalCohomologyCoefficientsSecondMap I hS n)
      (derivedLocalCohomologyCoefficientsFirstMap_comp_secondMap
        I hS n)).Exact
theorem

derivedLocalCohomologyCoefficients_beforeConnecting_exact

L340 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficients_beforeConnecting_exact
Documentation

Exactness at the last coefficient in degree n, immediately before the connecting morphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficients_beforeConnecting_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk
      (derivedLocalCohomologyCoefficientsSecondMap I hS n)
      (derivedLocalCohomologyCoefficientsConnectingMap I hS n)
      (derivedLocalCohomologyCoefficientsSecondMap_comp_connectingMap
        I hS n)).Exact
theorem

derivedLocalCohomologyCoefficients_afterConnecting_exact

L355 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficients_afterConnecting_exact
Documentation

Exactness immediately after the connecting morphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficients_afterConnecting_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) :
    (ShortComplex.mk
      (derivedLocalCohomologyCoefficientsConnectingMap I hS n)
      (derivedLocalCohomologyCoefficientsFirstMap I hS (n + 1))
      (derivedLocalCohomologyCoefficientsConnectingMap_comp_firstMap
        I hS n)).Exact

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