instance PushforwardExactness.pushforward_affine_preservesFiniteLimits {R S : Type v} [CommRing R] [CommRing S] (phi : R →+* S) : CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.restrictScalars phi)

Affine pushforward (restriction of scalars) preserves finite limits.

instance PushforwardExactness.pushforward_affine_preservesFiniteColimits {R S : Type v} [CommRing R] [CommRing S] (phi : R →+* S) : CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.restrictScalars phi)

Affine pushforward (restriction of scalars) preserves finite colimits.

theorem PushforwardExactness.pushforward_affine_exact {R S : Type v} [CommRing R] [CommRing S] (phi : R →+* S) : CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.restrictScalars phi) ∧ CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.restrictScalars phi)

Exactness of affine pushforward: it preserves both finite limits and finite colimits.

noncomputable def PushforwardExactness.schemePushforward {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Functor (TopCat.Sheaf AddCommGrpCat (AlgebraicGeometry.Scheme.forgetToTop.obj X)) (TopCat.Sheaf AddCommGrpCat (AlgebraicGeometry.Scheme.forgetToTop.obj Y))

The pushforward functor on sheaves of abelian groups along a morphism of schemes.

noncomputable def PushforwardExactness.schemePullbackPushforwardAdjunction {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : TopCat.Sheaf.pullback AddCommGrpCat (AlgebraicGeometry.Scheme.forgetToTop.map f) ⊣ schemePushforward f

The pullback–pushforward adjunction f⁻¹ ⊣ f_* for sheaves of abelian groups on the underlying topological spaces of schemes.

instance PushforwardExactness.pushforward_leftExact {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesFiniteLimits (schemePushforward f)

Sheaf-level pushforward is left exact: as a right adjoint, it preserves finite limits.