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

The global sections functor Γ(X, -) : X.Modules ⥤ Ab sending a sheaf of O_X-modules to its abelian group of global sections.

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

Γ(X, -) is an additive functor.

noncomputable def 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: if F ≅ G then RⁿF ≅ RⁿG for every n.

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

The pushforward f_* along an affine morphism preserves homology of complexes of quasi-coherent modules; equivalently it is exact on quasi-coherent sheaves.

theorem prop44_higher_direct_image_vanishing {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)

Vanishing of higher direct images along an affine morphism: for f affine and F quasi-coherent on X, Rⁿf_* F = 0 for all n > 0 (Prop 44, Lec 23).

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

Natural isomorphism Γ(X, -) ≅ Γ(Y, f_*(-)) from the definition of pushforward sections.

noncomputable def rightDerived_comp_exact_iso {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 (Scheme.Modules.globalSectionsFunctor Y)).rightDerived n).obj F ≅ ((Scheme.Modules.globalSectionsFunctor Y).rightDerived n).obj ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F)

For f affine and F quasi-coherent, the right derived functors of the composite Γ(Y, -) ∘ f_* agree with those of Γ(Y, -) applied to f_*F, since f_* is exact in this case (so the Grothendieck spectral sequence degenerates).

noncomputable def prop44_affine_pushforward_cohomology {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 : ℕ) : ((Scheme.Modules.globalSectionsFunctor Y).rightDerived n).obj ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj F) ≅ ((Scheme.Modules.globalSectionsFunctor X).rightDerived n).obj F

Proposition 44 (Lec 23): for f : X → Y affine and F quasi-coherent on X, the cohomology of f_*F on Y agrees with the cohomology of F on X: Hⁿ(Y, f_*F) ≅ Hⁿ(X, F).