Module

AbelianPullbackUnderlying.lean

Nyll.EtaleFundamentalGroups.Cohomology.AbelianPullbackUnderlying

1 declaration indexed from sourceView source ↗

Module documentation

Underlying sets of the actual abelian inverse image

The comparison is transported through the existing integer-module equivalence. It reuses the geometric-stalk proof for modules and its actual inverse-image functor. This is the comparison needed to pull back the sheaf of lifts of an extension representing a derived H¹ class.

Imports4

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

Imported by1

Nyll.EtaleFundamentalGroups.Cohomology.All

def

etaleAbelianPullbackUnderlyingIso

L32 ↗

EtaleFundamentalGroups.Cohomology.etaleAbelianPullbackUnderlyingIso

Documentation

Forgetting the abelian group structure commutes with actual étale inverse image.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def etaleAbelianPullbackUnderlyingIso :
    etaleAbelianPullback f ⋙
        sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u}) ≅
      sheafCompose Y.smallEtaleTopology (forget AddCommGrpCat.{u}) ⋙
        etaleSetPullback f

Module documentation

Underlying sets of the actual abelian inverse image

Declarations

etaleAbelianPullbackUnderlyingIso