NYLL
Module

ClosedPushforward.lean

Nyll.EtaleCohomology.Classical.ClosedPushforward
5 declarations indexed from sourceView source ↗

Module documentation

Classical cohomology and closed direct image

For every closed immersion i : Z ⟶ X, actual direct image induces Hⁿ(X, i_*F) ≃ Hⁿ(Z, F) in all degrees. This follows from the exact inverse-image/direct-image adjunction and its action on the constant integer sheaf. The resulting comparison is natural and is linear for module coefficients. There are no finite-field, noetherian, or finiteness hypotheses.

Imports11
Imported by2

Declarations

def

etaleAbelianCohomologyClosedPushforwardEquiv

L41 ↗
EtaleCohomology.etaleAbelianCohomologyClosedPushforwardEquiv
Documentation

Closed direct image does not change classical abelian étale cohomology.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Abelian Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
Lean source · statement
def etaleAbelianCohomologyClosedPushforwardEquiv
    (F : Sheaf Z.smallEtaleTopology AddCommGrpCat.{u}) (n : ℕ) :
    Sheaf.H.{u} ((etaleAbelianPushforward i).obj F) n ≃+ Sheaf.H.{u} F n
lemma

etaleAbelianCohomologyClosedPushforwardEquiv_apply

L49 ↗
EtaleCohomology.etaleAbelianCohomologyClosedPushforwardEquiv_apply
Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Abelian Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
Lean source · statement
lemma etaleAbelianCohomologyClosedPushforwardEquiv_apply
    (F : Sheaf Z.smallEtaleTopology AddCommGrpCat.{u}) (n : ℕ)
    (x : ((etaleAbelianPushforward i).obj F).H n) :
    etaleAbelianCohomologyClosedPushforwardEquiv i F n x =
      (Ext.mk₀ ((etaleAbelianPullbackConstantIso i).app
        (AddCommGrpCat.of (ULift ℤ))).inv).comp
          ((etaleAbelianPullbackPushforwardAdjunction i).extEquiv.symm x) (zero_add n)
lemma

etaleAbelianCohomologyClosedPushforwardEquiv_naturality

L58 ↗
EtaleCohomology.etaleAbelianCohomologyClosedPushforwardEquiv_naturality
Documentation

The closed direct-image comparison respects all coefficient-sheaf morphisms.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Abelian Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
Lean source · statement
lemma etaleAbelianCohomologyClosedPushforwardEquiv_naturality
    {F G : Sheaf Z.smallEtaleTopology AddCommGrpCat.{u}} (φ : F ⟶ G) (n : ℕ)
    (x : ((etaleAbelianPushforward i).obj F).H n) :
    etaleAbelianCohomologyClosedPushforwardEquiv i G n
        (Sheaf.H.map ((etaleAbelianPushforward i).map φ) n x) =
      Sheaf.H.map φ n (etaleAbelianCohomologyClosedPushforwardEquiv i F n x)
def

etaleCohomologyClosedPushforwardEquiv

L73 ↗
EtaleCohomology.etaleCohomologyClosedPushforwardEquiv
Documentation

The closed direct-image comparison for classical module-valued étale cohomology, linear over the original coefficient ring.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Abelian Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
variable (R : Type u) [CommRing R]
Lean source · statement
def etaleCohomologyClosedPushforwardEquiv
    (F : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)) (n : ℕ) :
    etaleCohomology X R ((etalePushforward i R).obj F) n ≃ₗ[R]
      etaleCohomology Z R F n
lemma

etaleCohomologyClosedPushforwardEquiv_naturality

L87 ↗
EtaleCohomology.etaleCohomologyClosedPushforwardEquiv_naturality
Documentation

Naturality of the coefficient-linear comparison.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Abelian Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
variable (R : Type u) [CommRing R]
Lean source · statement
lemma etaleCohomologyClosedPushforwardEquiv_naturality
    {F G : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)} (φ : F ⟶ G) (n : ℕ)
    (x : etaleCohomology X R ((etalePushforward i R).obj F) n) :
    etaleCohomologyClosedPushforwardEquiv i R G n
        (Classical.cohomologyMap.{u + 1, u, u, u, u} ((etalePushforward i R).map φ) n x) =
      Classical.cohomologyMap.{u + 1, u, u, u, u} φ n
        (etaleCohomologyClosedPushforwardEquiv i R F n x)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.