Module

SchemePullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.SchemePullback

6 declarations indexed from sourceView source ↗

Module documentation

Scheme pullback of actual constant-coefficient cohomology

The map is induced on Ext by the exact inverse-image functor of abelian étale sheaves, with both constant objects identified by the actual constant-sheaf comparison. Its degree-one value is represented by the inverse image of the original extension with these identifications.

This constructs geometric pullback independently of the fundamental-group character comparison. Compatibility with monodromy is not assumed here.

Imports7

Nyll.EtaleCohomology.Classical.AbelianSheafFunctors
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Mathlib.Algebra.Category.Grp.AB
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt

Imported by6

def

constantCohomologyPullback

L39 ↗

EtaleFundamentalGroups.Cohomology.constantCohomologyPullback

Documentation

Pullback on actual derived cohomology, induced by exact inverse image.

Source context 6 commands

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

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

Lean source · full declaration

def constantCohomologyPullback (n : ℕ) :
    Sheaf.H.{u} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A) n →+
      Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A) n where
  toFun a :=
    ((Ext.mk₀ ((etaleAbelianPullbackConstantIso f).app
      (AddCommGrpCat.of (ULift.{u} ℤ))).inv).comp
        (a.mapExactFunctor (etaleAbelianPullback f)) (zero_add n)).comp
      (Ext.mk₀ ((etaleAbelianPullbackConstantIso f).app A).hom) (add_zero n)
  map_zero' := by
    rw [Ext.mapExactFunctor_zero, Ext.comp_zero, Ext.zero_comp]
  map_add' a b := by
    rw [Ext.mapExactFunctor_add, Ext.comp_add, Ext.add_comp]

theorem

constantCohomologyPullback_naturality

L53 ↗

EtaleFundamentalGroups.Cohomology.constantCohomologyPullback_naturality

Documentation

Exact inverse image commutes with maps of the original constant coefficients.

Source context 6 commands

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

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

Lean source · statement

theorem constantCohomologyPullback_naturality
    (B : AddCommGrpCat.{u}) (α : A ⟶ B) (n : ℕ)
    (a : Sheaf.H.{u} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A) n) :
    Sheaf.H.map ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).map α) n
        (constantCohomologyPullback f A n a) =
      constantCohomologyPullback f B n
        (Sheaf.H.map ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).map α) n a)

def

schemePullbackH1Extension

L85 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension

Documentation

The inverse-image extension with the original constant coefficient objects.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u})
variable {E : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ)))
  (h : i ≫ p = 0)

Lean source · statement

def schemePullbackH1Extension :
    ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})

def

schemePullbackH1ExtensionIso

L97 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1ExtensionIso

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u})
variable {E : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ)))
  (h : i ≫ p = 0)

Lean source · statement

def schemePullbackH1ExtensionIso :
    (ShortComplex.mk i p h).map (etaleAbelianPullback f) ≅
      schemePullbackH1Extension f A i p h

theorem

schemePullbackH1Extension_shortExact

L116 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension_shortExact

Documentation

Exactness is supplied by exact inverse image and the constant comparisons.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u})
variable {E : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ)))
  (h : i ≫ p = 0)

Lean source · statement

theorem schemePullbackH1Extension_shortExact
    (hs : (ShortComplex.mk i p h).ShortExact) :
    (schemePullbackH1Extension f A i p h).ShortExact

theorem

constantCohomologyPullback_extClass

L124 ↗

EtaleFundamentalGroups.Cohomology.constantCohomologyPullback_extClass

Documentation

The geometric inverse-image extension represents the pullback of its original derived H¹ class. No extension-class compatibility is postulated.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
open EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u})
variable {E : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ)))
  (h : i ≫ p = 0)

Lean source · statement

theorem constantCohomologyPullback_extClass
    (hs : (ShortComplex.mk i p h).ShortExact) :
    constantCohomologyPullback f A 1 hs.extClass =
      (schemePullbackH1Extension_shortExact f A i p h hs).extClass

Module documentation

Scheme pullback of actual constant-coefficient cohomology

Declarations

constantCohomologyPullback

constantCohomologyPullback_naturality

schemePullbackH1Extension

schemePullbackH1ExtensionIso

schemePullbackH1Extension_shortExact

constantCohomologyPullback_extClass