Module

DerivedExtLegacyComparison.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedExtLegacyComparison

3 declarations indexed from sourceView source ↗

Module documentation

Comparison of the two Ext implementations used by local cohomology and depth

localCohomology is currently defined using the legacy derived-functor object _root_.Ext, whereas the depth API uses CategoryTheory.Abelian.Ext. This file records the vanishing comparison needed to pass from the latter to the former.

Imports4

Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Mathlib.CategoryTheory.Abelian.Ext
Mathlib.CategoryTheory.Abelian.Projective.Ext

Imported by4

theorem

legacyExt_isZero_of_subsingleton_derivedExt_zero

L30 ↗

EtaleFundamentalGroups.legacyExt_isZero_of_subsingleton_derivedExt_zero

Documentation

Vanishing of degree-zero derived-category Ext forces vanishing of the degree-zero legacy Ext object.

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

Lean source · statement

theorem legacyExt_isZero_of_subsingleton_derivedExt_zero
    {R : Type u} [CommRing R] [Small.{v} R]
    (X Y : ModuleCat.{v} R)
    (hExt : Subsingleton (CategoryTheory.Abelian.Ext.{v} X Y 0)) :
    IsZero (((_root_.Ext R (ModuleCat.{v} R) 0).obj (op X)).obj Y)

theorem

legacyExt_isZero_of_subsingleton_derivedExt_succ

L57 ↗

EtaleFundamentalGroups.legacyExt_isZero_of_subsingleton_derivedExt_succ

Documentation

Vanishing of positive-degree derived-category Ext forces vanishing of the corresponding legacy Ext object. Both sides are computed using the same projective resolution.

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

Lean source · statement

theorem legacyExt_isZero_of_subsingleton_derivedExt_succ
    {R : Type u} [CommRing R] [Small.{v} R]
    (X Y : ModuleCat.{v} R) (n : ℕ)
    (hExt : Subsingleton (CategoryTheory.Abelian.Ext.{v} X Y (n + 1))) :
    IsZero (((_root_.Ext R (ModuleCat.{v} R) (n + 1)).obj (op X)).obj Y)

theorem

legacyExt_isZero_of_subsingleton_derivedExt

L79 ↗

EtaleFundamentalGroups.legacyExt_isZero_of_subsingleton_derivedExt

Documentation

Vanishing of derived-category Ext in any degree forces vanishing of the corresponding legacy Ext object used by localCohomology.

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

Lean source · statement

theorem legacyExt_isZero_of_subsingleton_derivedExt
    {R : Type u} [CommRing R] [Small.{v} R]
    (X Y : ModuleCat.{v} R) (i : ℕ)
    (hExt : Subsingleton (CategoryTheory.Abelian.Ext.{v} X Y i)) :
    IsZero (((_root_.Ext R (ModuleCat.{v} R) i).obj (op X)).obj Y)

Module documentation

Comparison of the two Ext implementations used by local cohomology and depth

Declarations

legacyExt_isZero_of_subsingleton_derivedExt_zero

legacyExt_isZero_of_subsingleton_derivedExt_succ

legacyExt_isZero_of_subsingleton_derivedExt