Module

AbelianUnderlying.lean

Nyll.EtaleCohomology.Classical.AbelianUnderlying

4 declarations indexed from sourceView source ↗

Module documentation

Underlying sets of actual abelian inverse images

Transport the proved module/set inverse-image comparison through the actual integer-module equivalence defining abelian inverse image. The comparison retains the original abelian sheaves and the existing set inverse image. This allows their extension fibers to be compared as sheaves of sets.

Imports4

Nyll.EtaleCohomology.Classical.AbelianSheafFunctors
Nyll.EtaleCohomology.Sites.ModuleSetComparison
Nyll.EtaleCohomology.Sites.SetSheafFunctors
Mathlib.CategoryTheory.Whiskering

Imported by1

Nyll.EtaleCohomology.Classical.All

def

etaleAbelianUnderlying

L31 ↗

EtaleCohomology.etaleAbelianUnderlying

Documentation

Forget the abelian group structure of an etale sheaf.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology

Lean source · statement

def etaleAbelianUnderlying (X : Scheme.{u}) :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{u} ⥤
      Sheaf X.smallEtaleTopology (Type u)

def

integerSheafEquivalenceUnderlyingIso

L36 ↗

EtaleCohomology.integerSheafEquivalenceUnderlyingIso

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology

Lean source · statement

def integerSheafEquivalenceUnderlyingIso (X : Scheme.{u}) :
    (Classical.integerSheafEquivalence X.smallEtaleTopology).functor ⋙
      etaleAbelianUnderlying X ≅ etaleModuleUnderlying X (ULift.{u} ℤ)

def

integerSheafInverseUnderlyingIso

L41 ↗

EtaleCohomology.integerSheafInverseUnderlyingIso

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology

Lean source · statement

def integerSheafInverseUnderlyingIso (X : Scheme.{u}) :
    (Classical.integerSheafEquivalence X.smallEtaleTopology).inverse ⋙
      etaleModuleUnderlying X (ULift.{u} ℤ) ≅ etaleAbelianUnderlying X

def

etaleAbelianPullbackUnderlyingIso

L51 ↗

EtaleCohomology.etaleAbelianPullbackUnderlyingIso

Documentation

The actual abelian inverse image commutes with forgetting to sheaves of sets.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology

Lean source · statement

def etaleAbelianPullbackUnderlyingIso {X Y : Scheme.{u}} (f : X ⟶ Y) :
    etaleAbelianPullback f ⋙ etaleAbelianUnderlying X ≅
      etaleAbelianUnderlying Y ⋙ etaleSetPullback f

Module documentation

Underlying sets of actual abelian inverse images

Declarations

etaleAbelianUnderlying

integerSheafEquivalenceUnderlyingIso

integerSheafInverseUnderlyingIso

etaleAbelianPullbackUnderlyingIso