Module

CohomologyPullback.lean

Nyll.JacobianVarieties.Kummer.CohomologyPullback

6 declarations indexed from sourceView source ↗

Module documentation

Actual pullback of constant-coefficient etale cohomology

Use the exact inverse image of abelian sheaves and its actual comparison with constant sheaves. In degree one, the resulting map sends an extension class to the class of its inverse-image extension, with the original coefficient and integer sheaves. This construction does not define cohomology by characters.

Imports5

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

Imported by4

def

constantCohomologyPullback

L33 ↗

JacobianVarieties.Kummer.constantCohomologyPullback

Documentation

Pullback on actual derived cohomology, retaining constant coefficients.

Source context 5 commands

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

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

Lean source · statement

def constantCohomologyPullback (A : AddCommGrpCat.{u}) (n : ℕ) :
    Sheaf.H.{u} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A) n →+
      Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A) n

theorem

constantCohomologyPullback_apply

L49 ↗

JacobianVarieties.Kummer.constantCohomologyPullback_apply

Documentation

The map uses the actual exact-functor map on Ext.

Source context 5 commands

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

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

Lean source · statement

theorem constantCohomologyPullback_apply (A : AddCommGrpCat.{u}) (n : ℕ)
    (a : Sheaf.H.{u} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A) n) :
    constantCohomologyPullback f A n a =
      ((Ext.mk₀ ((etaleAbelianPullbackConstantIso f).inv.app
        (AddCommGrpCat.of (ULift.{u} ℤ)))).comp
          (a.mapExactFunctor (etaleAbelianPullback f)) (zero_add n)).comp
            (Ext.mk₀ ((etaleAbelianPullbackConstantIso f).hom.app A)) (add_zero n)

abbrev

pullbackExtension

L65 ↗

JacobianVarieties.Kummer.pullbackExtension

Documentation

The inverse-image extension, identifying both endpoints with the original constant sheaves through the actual inverse-image comparison.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Abelian EtaleCohomology
universe u
namespace JacobianVarieties.Kummer
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : AddCommGrpCat.{u})
  {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

abbrev pullbackExtension : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u})

def

pullbackExtensionIso

L73 ↗

JacobianVarieties.Kummer.pullbackExtensionIso

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Abelian EtaleCohomology
universe u
namespace JacobianVarieties.Kummer
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : AddCommGrpCat.{u})
  {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 pullbackExtensionIso :
    pullbackExtension f A i p h ≅ (ShortComplex.mk i p h).map (etaleAbelianPullback f)

theorem

pullbackExtension_shortExact

L89 ↗

JacobianVarieties.Kummer.pullbackExtension_shortExact

Documentation

Exactness is supplied by exact inverse image; no additional exactness condition is imposed on the pulled-back extension.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Abelian EtaleCohomology
universe u
namespace JacobianVarieties.Kummer
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : AddCommGrpCat.{u})
  {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 pullbackExtension_shortExact (hs : (ShortComplex.mk i p h).ShortExact) :
    (pullbackExtension f A i p h).ShortExact

theorem

constantCohomologyPullback_extClass

L96 ↗

JacobianVarieties.Kummer.constantCohomologyPullback_extClass

Documentation

Pullback of an actual degree-one cohomology class is represented by the actual inverse-image short exact sequence.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Abelian EtaleCohomology
universe u
namespace JacobianVarieties.Kummer
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
variable (A : AddCommGrpCat.{u})
  {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 =
      (pullbackExtension_shortExact f A i p h hs).extClass

Module documentation

Actual pullback of constant-coefficient etale cohomology

Declarations

constantCohomologyPullback

constantCohomologyPullback_apply

pullbackExtension

pullbackExtensionIso

pullbackExtension_shortExact

constantCohomologyPullback_extClass