noncomputable def AffinePushforwardHigher.globalSectionsFunctor (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor X.Modules Ab

Global sections functor Γ(X, -) : X.Modules ⥤ Ab for a scheme X.

instance AffinePushforwardHigher.globalSectionsFunctor_additive (X : AlgebraicGeometry.Scheme) : (globalSectionsFunctor X).Additive

The global sections functor is additive.

noncomputable def AffinePushforwardHigher.rightDerivedFunctorIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.HasInjectiveResolutions C] (F G : CategoryTheory.Functor C D) [F.Additive] [G.Additive] (τ : F ≅ G) (n : ℕ) : F.rightDerived n ≅ G.rightDerived n

Naturally isomorphic additive functors have naturally isomorphic right derived functors.

theorem AffinePushforwardHigher.affinePushforwardExact {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] : (AlgebraicGeometry.Scheme.Modules.pushforward f).PreservesHomology

Pushforward along an affine morphism is exact on (quasi-coherent) modules.

noncomputable def AffinePushforwardHigher.globalSectionsCompPushforwardIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] : globalSectionsFunctor X ≅ (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (globalSectionsFunctor Y)

Natural isomorphism Γ(X, -) ≅ Γ(Y, f_*(-)).

noncomputable def AffinePushforwardHigher.rightDerivedCompExactIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [CategoryTheory.HasInjectiveResolutions X.Modules] [CategoryTheory.HasInjectiveResolutions Y.Modules] (F : X.Modules) [SheafOfModules.IsQuasicoherent F] (n : ℕ) : (((AlgebraicGeometry.Scheme.Modules.pushforward f).comp (globalSectionsFunctor Y)).rightDerived n).obj F ≅ ((globalSectionsFunctor Y).rightDerived n).obj ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

For f affine and F quasi-coherent, exactness of f_* gives Rⁿ(Γ_Y ∘ f_*)(F) ≅ Rⁿ Γ_Y (f_*F).

theorem AffinePushforwardHigher.higherDirectImageVanishing {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (F : X.Modules) [SheafOfModules.IsQuasicoherent F] [CategoryTheory.HasInjectiveResolutions X.Modules] (n : ℕ) (hn : 0 < n) : CategoryTheory.Limits.IsZero (((AlgebraicGeometry.Scheme.Modules.pushforward f).rightDerived n).obj F)

Higher direct images vanish along affine morphisms: Rⁿf_*F = 0 for n > 0 when f is affine and F is quasi-coherent (Prop 44, Lec 23).

noncomputable def AffinePushforwardHigher.affinePushforwardCohomologyIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (F : X.Modules) [SheafOfModules.IsQuasicoherent F] [CategoryTheory.HasInjectiveResolutions X.Modules] [CategoryTheory.HasInjectiveResolutions Y.Modules] (n : ℕ) : ((globalSectionsFunctor Y).rightDerived n).obj ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F) ≅ ((globalSectionsFunctor X).rightDerived n).obj F

Cohomology along an affine pushforward: Hⁿ(Y, f_*F) ≅ Hⁿ(X, F) (Prop 44, Lec 23).