Module

InjectiveResolution.lean

Nyll.EtaleCohomology.Classical.InjectiveResolution

4 declarations indexed from sourceView source ↗

Module documentation

Classical étale cohomology computed on an injective resolution

A given InjectiveResolution F is extended from nonnegative to integer degrees by the existing zero-extension functor. Its actual augmentation becomes a quasi-isomorphism from the single complex of F, and the extended resolution is K-injective by mathlib's bounded-below theorem.

The additive derived-Hom and homotopy-Hom comparisons therefore compute actual small-universe Sheaf.H by the Hom complex. The constructed natural cochain isomorphism then identifies this with the homology of actual global sections of the extended resolution, followed by the canonical universe lift. There is no comparison premise or replacement cohomology definition.

Imports19

Nyll.EtaleCohomology.Classical.GlobalSectionsComplex
Mathlib.Algebra.Category.Grp.Basic
Mathlib.Algebra.Homology.DerivedCategory.Basic
Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Mathlib.Algebra.Homology.DerivedCategory.KInjective
Mathlib.Algebra.Homology.Embedding.Extend
Mathlib.Algebra.Homology.Embedding.ExtendHomology
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Mathlib.CategoryTheory.Abelian.Injective.Resolution
Mathlib.CategoryTheory.HomCongr
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Basic
Mathlib.CategoryTheory.Shift.CommShift
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Imported by2

def

homCongrAddEquiv

L52 ↗

EtaleCohomology.Classical.homCongrAddEquiv

Source context 5 commands

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

noncomputable section
universe w v uC u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex
namespace EtaleCohomology.Classical

Lean source · full declaration

def homCongrAddEquiv {C : Type uC} [Category.{v} C] [Preadditive C]
    {A B A' B' : C} (e : A ≅ A') (f : B ≅ B') : (A ⟶ B) ≃+ (A' ⟶ B') where
  toEquiv := Iso.homCongr e f
  map_add' a b := by
    change e.inv ≫ (a + b) ≫ f.hom = (e.inv ≫ a ≫ f.hom) + (e.inv ≫ b ≫ f.hom)
    rw [Preadditive.add_comp, Preadditive.comp_add]

def

derivedHomComplexHomologyEquiv

L59 ↗

EtaleCohomology.Classical.derivedHomComplexHomologyEquiv

Source context 5 commands

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

noncomputable section
universe w v uC u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex
namespace EtaleCohomology.Classical

Lean source · statement

def derivedHomComplexHomologyEquiv
    {C : Type uC} [Category.{v} C] [Abelian C] [HasDerivedCategory C]
    (K L : CochainComplex C ℤ) [L.IsKInjective] (n : ℤ) :
    (DerivedCategory.Q.obj K ⟶ (DerivedCategory.Q.obj L)⟦n⟧) ≃+
      (CochainComplex.HomComplex K L).homology n

def

extResolutionHomologyEquiv

L82 ↗

EtaleCohomology.Classical.extResolutionHomologyEquiv

Source context 5 commands

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

noncomputable section
universe w v uC u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex
namespace EtaleCohomology.Classical

Lean source · statement

def extResolutionHomologyEquiv
    {C : Type uC} [Category.{v} C] [Abelian C] [HasDerivedCategory C] [HasExt.{w} C]
    (A : C) {F : C} (I : InjectiveResolution F) (n : ℕ) :
    Abelian.Ext.{w} A F n ≃+
      (CochainComplex.HomComplex ((CochainComplex.singleFunctor C 0).obj A)
        (I.cocomplex.extend ComplexShape.embeddingUpNat)).homology (n : ℤ)

def

etaleAbelianCohomologyInjectiveResolutionEquiv

L109 ↗

EtaleCohomology.etaleAbelianCohomologyInjectiveResolutionEquiv

Documentation

Classical Sheaf.H is computed by actual global sections of a given injective resolution, extended by zero to integer degrees. The left-hand cohomology remains in universe u; only the explicit target lift enters the raw Hom-complex universe.

Source context 5 commands

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

noncomputable section
universe w v uC u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex
namespace EtaleCohomology

Lean source · statement

def etaleAbelianCohomologyInjectiveResolutionEquiv
    (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))) ⋙
          AddCommGrpCat.uliftFunctor.{u + 1, u}).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (I.cocomplex.extend ComplexShape.embeddingUpNat)).homology (n : ℤ)

Module documentation

Classical étale cohomology computed on an injective resolution

Declarations

homCongrAddEquiv

derivedHomComplexHomologyEquiv

extResolutionHomologyEquiv

etaleAbelianCohomologyInjectiveResolutionEquiv