Documentation

TauCeti.AlgebraicGeometry.Cohomology.ClosedImmersion.Basic

Cohomology and direct image along a closed immersion #

For a closed immersion f : X ⟶ Y and a sheaf of modules M on X, Hⁿ(Y, f_* M) ≅ Hⁿ(X, M), naturally in M. This allows cohomology computations on a closed subscheme to be performed on the ambient scheme. No quasi-coherence, Noetherianity or properness assumption is needed for this additive comparison.

References #

source
noncomputable def TauCeti.AlgebraicGeometry.cohomologyPushforwardNatIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] (n : ℕ) :
(AlgebraicGeometry.Scheme.Modules.pushforward f).comp (Scheme.Modules.cohomologyFunctor Y n) ≅ Scheme.Modules.cohomologyFunctor X n

Direct image along a closed immersion preserves cohomology, naturally in the coefficient sheaf of modules.

Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.cohomologyPushforwardIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] (M : X.Modules) (n : ℕ) :
    ↧(Scheme.Modules.Cohomology ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M) n) ≅ ↧(Scheme.Modules.Cohomology M n)

    The additive cohomology comparison for a sheaf of modules on a closed subscheme.

    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.cohomologyPushforwardNatIso_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] (M : X.Modules) (n : ℕ) :
      (cohomologyPushforwardNatIso f n).app M = cohomologyPushforwardIso f M n
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.cohomologyPushforwardNatIso_hom_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] (M : X.Modules) (n : ℕ) :
      (cohomologyPushforwardNatIso f n).hom.app M = (cohomologyPushforwardIso f M n).hom
      source
      theorem TauCeti.AlgebraicGeometry.cohomologyPushforwardIso_naturality {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] {M N : X.Modules} (α : M ⟶ N) (n : ℕ) :
      CategoryTheory.CategoryStruct.comp (((AlgebraicGeometry.Scheme.Modules.pushforward f).comp (Scheme.Modules.cohomologyFunctor Y n)).map α) (cohomologyPushforwardIso f N n).hom = CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIso f M n).hom ((Scheme.Modules.cohomologyFunctor X n).map α)

      The additive comparison commutes with maps of coefficient sheaves.

      source
      theorem TauCeti.AlgebraicGeometry.cohomologyPushforwardIso_naturality_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] {M N : X.Modules} (α : M ⟶ N) (n : ℕ) {Z : AddCommGrpCat} (h : ↧(Scheme.Modules.Cohomology N n) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((Scheme.Modules.cohomologyFunctor Y n).map ((AlgebraicGeometry.Scheme.Modules.pushforward f).map α)) (cohomologyPushforwardIso f N n).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIso f M n).hom ((Scheme.Modules.cohomologyFunctor X n).map α)) h

      The additive comparison commutes with maps of coefficient sheaves.