Module

NatInjectiveResolution.lean

Nyll.EtaleCohomology.Classical.NatInjectiveResolution

7 declarations indexed from sourceView source ↗

Module documentation

Classical cohomology and nonnegative injective resolutions

Mapping a zero-extended complex by a zero-preserving functor commutes with extension: the comparison uses extendXIso in nonnegative degrees and actual zero-object witnesses in negative degrees. This is a constructed chain isomorphism, not an interchange premise.

The existing extension-homology comparison and exactness of the canonical abelian-group universe lift then remove the extension and lift from the classical cohomology calculation. Thus the original small Sheaf.H is computed by actual global sections of the original ℕ-indexed resolution. The existing InjectiveResolution.isoRightDerivedObj gives the corresponding objectwise comparison with Functor.rightDerived of actual global sections.

Imports13

Nyll.EtaleCohomology.Classical.InjectiveResolution
Mathlib.Algebra.Category.Grp.Ulift
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.Embedding.Extend
Mathlib.Algebra.Homology.Embedding.ExtendHomology
Mathlib.Algebra.Homology.HomologicalComplex
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Mathlib.CategoryTheory.Abelian.RightDerived
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Sites.Sheaf

Imported by2

theorem

isZero_extend_negSucc

L52 ↗

EtaleCohomology.Classical.isZero_extend_negSucc

Source context 6 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology.Classical
section Extension
variable {C : Type uC} [Category.{vC} C] [HasZeroMorphisms C] [HasZeroObject C]
  {D : Type uD} [Category.{vD} D] [HasZeroMorphisms D] [HasZeroObject D]
  (F : C ⥤ D) [F.PreservesZeroMorphisms]

Lean source · statement

theorem isZero_extend_negSucc (K : CochainComplex C ℕ) (n : ℕ) :
    IsZero ((K.extend ComplexShape.embeddingUpNat).X (Int.negSucc n))

def

mapExtendUpNatXIso

L58 ↗

EtaleCohomology.Classical.mapExtendUpNatXIso

Source context 6 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology.Classical
section Extension
variable {C : Type uC} [Category.{vC} C] [HasZeroMorphisms C] [HasZeroObject C]
  {D : Type uD} [Category.{vD} D] [HasZeroMorphisms D] [HasZeroObject D]
  (F : C ⥤ D) [F.PreservesZeroMorphisms]

Lean source · statement

def mapExtendUpNatXIso (K : CochainComplex C ℕ) (j : ℤ) :
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
      (K.extend ComplexShape.embeddingUpNat)).X j ≅
      (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).extend
        ComplexShape.embeddingUpNat).X j

def

mapExtendUpNatIso

L72 ↗

EtaleCohomology.Classical.mapExtendUpNatIso

Source context 6 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology.Classical
section Extension
variable {C : Type uC} [Category.{vC} C] [HasZeroMorphisms C] [HasZeroObject C]
  {D : Type uD} [Category.{vD} D] [HasZeroMorphisms D] [HasZeroObject D]
  (F : C ⥤ D) [F.PreservesZeroMorphisms]

Lean source · statement

def mapExtendUpNatIso (K : CochainComplex C ℕ) :
    (F.mapHomologicalComplex (ComplexShape.up ℤ)).obj (K.extend ComplexShape.embeddingUpNat) ≅
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K).extend
        ComplexShape.embeddingUpNat

def

etaleGlobalSectionsExtendIso

L117 ↗

EtaleCohomology.etaleGlobalSectionsExtendIso

Documentation

Actual global sections commute with zero extension of a nonnegative complex. The comparison is an explicit chain isomorphism in the original coefficient universe.

Source context 4 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def etaleGlobalSectionsExtendIso (X : Scheme.{u})
    (K : CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℕ) :
    (((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (op (⊤_ X.Etale))).mapHomologicalComplex
      (ComplexShape.up ℤ)).obj (K.extend ComplexShape.embeddingUpNat) ≅
      ((((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (op (⊤_ X.Etale))).mapHomologicalComplex (ComplexShape.up ℕ)).obj K).extend
          ComplexShape.embeddingUpNat

def

etaleAbelianCohomologyNatResolutionEquiv

L132 ↗

EtaleCohomology.etaleAbelianCohomologyNatResolutionEquiv

Documentation

The original small classical cohomology group is computed by actual global sections of the original nonnegative injective resolution. Both sides have carrier universe u; extension and universe lift have been explicitly compared and removed.

Source context 4 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def etaleAbelianCohomologyNatResolutionEquiv
    (X : Scheme.{u}) (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
    (I : InjectiveResolution F) (n : ℕ) :
    Sheaf.H.{u} F n ≃+
      ((((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (op (⊤_ X.Etale))).mapHomologicalComplex
          (ComplexShape.up ℕ)).obj I.cocomplex).homology n

instance

etaleAbelianGlobalSections_additive

L165 ↗

EtaleCohomology.etaleAbelianGlobalSections_additive

Documentation

Étale global sections are additive via the canonical sheaf-evaluation isomorphism and the existing additive inclusion and evaluation functors.

Source context 4 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

instance etaleAbelianGlobalSections_additive (X : Scheme.{u}) :
    ((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (op (⊤_ X.Etale))).Additive

def

etaleAbelianCohomologyRightDerivedEquiv

L175 ↗

EtaleCohomology.etaleAbelianCohomologyRightDerivedEquiv

Documentation

Objectwise identification of actual classical Sheaf.H with the existing right-derived functor of actual abelian global sections. This uses the canonical supplied injective resolution and its standard derived-functor computation.

Source context 4 commands

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

noncomputable section
universe uC vC uD vD u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def etaleAbelianCohomologyRightDerivedEquiv
    (X : Scheme.{u}) (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) (n : ℕ) :
    Sheaf.H.{u} F n ≃+
      ((((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (op (⊤_ X.Etale))).rightDerived n).obj F)

Module documentation

Classical cohomology and nonnegative injective resolutions

Declarations

isZero_extend_negSucc

mapExtendUpNatXIso

mapExtendUpNatIso

etaleGlobalSectionsExtendIso

etaleAbelianCohomologyNatResolutionEquiv

etaleAbelianGlobalSections_additive

etaleAbelianCohomologyRightDerivedEquiv