Module

GlobalSectionsComplex.lean

Nyll.EtaleCohomology.Classical.GlobalSectionsComplex

9 declarations indexed from sourceView source ↗

Module documentation

The constant-integer Hom complex and actual global sections

For a complex K of abelian sheaves on the small étale site, the Hom complex from the constant integer sheaf in degree zero identifies naturally with the complex obtained by taking actual global sections degreewise.

The raw Hom complex lives in the universe of sheaf morphisms, u + 1. The existing sections remain in AddCommGrpCat.{u}; the target uses the canonical AddCommGrpCat.uliftFunctor to express that universe boundary. No new sheaf-cohomology definition or derived comparison is assumed.

Imports14

Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Mathlib.Algebra.Category.Grp.Ulift
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Homology.HomologicalComplex
Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Adjunction.Additive
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.Sites.Abelian
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Sheaf

Imported by2

lemma

uliftIntegerHomEquiv_naturality

L45 ↗

EtaleCohomology.uliftIntegerHomEquiv_naturality

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology

Lean source · statement

lemma uliftIntegerHomEquiv_naturality
    {A B : AddCommGrpCat.{u}} (a : AddCommGrpCat.of (ULift.{u} ℤ) ⟶ A) (f : A ⟶ B) :
    AddCommGrpCat.uliftZMultiplesAddEquiv B (a ≫ f) =
      f (AddCommGrpCat.uliftZMultiplesAddEquiv A a)

def

integerHomSectionsEquiv

L56 ↗

EtaleCohomology.integerHomSectionsEquiv

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

def integerHomSectionsEquiv (F : (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})) :
    (((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (AddCommGrpCat.of (ULift.{u} ℤ))) ⟶ F) ≃+ F.obj.obj (op T)

lemma

integerHomSectionsEquiv_naturality

L62 ↗

EtaleCohomology.integerHomSectionsEquiv_naturality

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

lemma integerHomSectionsEquiv_naturality
    {F G : (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})}
    (a : ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (AddCommGrpCat.of (ULift.{u} ℤ))) ⟶ F) (φ : F ⟶ G) :
    integerHomSectionsEquiv X G (a ≫ φ) =
      φ.hom.app (op T) (integerHomSectionsEquiv X F a)

def

cochainSectionsEquiv

L80 ↗

EtaleCohomology.cochainSectionsEquiv

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

def cochainSectionsEquiv
    (K : CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℤ) (n : ℤ) :
    Cochain ((CochainComplex.singleFunctor (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) 0).obj
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)))) K n ≃+
      (K.X n).obj.obj (op T)

lemma

cochainSectionsEquiv_d

L88 ↗

EtaleCohomology.cochainSectionsEquiv_d

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

lemma cochainSectionsEquiv_d
    (K : CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℤ) (i j : ℤ)
    (z : Cochain
      ((CochainComplex.singleFunctor (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) 0).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ)))) K i) :
    cochainSectionsEquiv X K j (HomComplex.δ i j z) =
      (K.d i j).hom.app (op T) (cochainSectionsEquiv X K i z)

lemma

cochainSectionsEquiv_postcomp

L104 ↗

EtaleCohomology.cochainSectionsEquiv_postcomp

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

lemma cochainSectionsEquiv_postcomp
    {K L : CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℤ} (φ : K ⟶ L) (n : ℤ)
    (z : Cochain
      ((CochainComplex.singleFunctor (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) 0).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ)))) K n) :
    cochainSectionsEquiv X L n (z.comp (Cochain.ofHom φ) (add_zero n)) =
      (φ.f n).hom.app (op T) (cochainSectionsEquiv X K n z)

def

etaleHomFromIntegerFunctor

L119 ↗

EtaleCohomology.etaleHomFromIntegerFunctor

Documentation

The actual Hom complex from the constant integer sheaf in degree zero. Its maps are ordinary postcomposition of cochains by the given chain map.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · full declaration

def etaleHomFromIntegerFunctor :
    CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℤ ⥤
      CochainComplex AddCommGrpCat.{u + 1} ℤ where
  obj K := CochainComplex.HomComplex
    ((CochainComplex.singleFunctor (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) 0).obj
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)))) K
  map φ :=
    { f := fun n => AddCommGrpCat.ofHom
        { toFun := fun z => z.comp (Cochain.ofHom φ) (add_zero n)
          map_zero' := Cochain.zero_comp _ _
          map_add' := fun z w => Cochain.add_comp z w (Cochain.ofHom φ) (add_zero n) }
      comm' := fun i j _ => by
        apply AddCommGrpCat.hom_ext
        apply AddMonoidHom.ext
        intro z
        exact HomComplex.δ_comp_ofHom z φ j }
  map_id K := by
    apply HomologicalComplex.hom_ext
    intro n
    apply AddCommGrpCat.hom_ext
    apply AddMonoidHom.ext
    intro z
    exact Cochain.comp_id z
  map_comp φ ψ := by
    apply HomologicalComplex.hom_ext
    intro n
    apply AddCommGrpCat.hom_ext
    apply AddMonoidHom.ext
    intro z
    change z.comp (Cochain.ofHom (φ ≫ ψ)) (add_zero n) =
      (z.comp (Cochain.ofHom φ) (add_zero n)).comp (Cochain.ofHom ψ) (add_zero n)
    rw [Cochain.ofHom_comp]
    exact (Cochain.comp_assoc_of_second_is_zero_cochain z
      (Cochain.ofHom φ) (Cochain.ofHom ψ) (add_zero n)).symm

def

homFromIntegerSectionsIso

L155 ↗

EtaleCohomology.homFromIntegerSectionsIso

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

def homFromIntegerSectionsIso
    (K : CochainComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) ℤ) :
    (etaleHomFromIntegerFunctor X).obj K ≅
      ((((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj (op T)) ⋙
        AddCommGrpCat.uliftFunctor.{u + 1, u}).mapHomologicalComplex (ComplexShape.up ℤ)).obj K

def

etaleHomFromIntegerSectionsIso

L174 ↗

EtaleCohomology.etaleHomFromIntegerSectionsIso

Documentation

The natural cochain isomorphism from the raw constant-integer Hom complex to the canonical universe lift of the existing global-sections complex. The underlying coefficient sheaves and their section groups remain in universe u.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
open CochainComplex HomComplex
namespace EtaleCohomology
variable (X : Scheme.{u})
local notation "T" => (⊤_ X.Etale)

Lean source · statement

def etaleHomFromIntegerSectionsIso :
    etaleHomFromIntegerFunctor X ≅
      (((sheafSections X.smallEtaleTopology AddCommGrpCat.{u}).obj (op T)) ⋙
        AddCommGrpCat.uliftFunctor.{u + 1, u}).mapHomologicalComplex (ComplexShape.up ℤ)

Module documentation

The constant-integer Hom complex and actual global sections

Declarations