instance PushforwardExactAffine.restrictScalars_preservesFiniteLimits {R S : Type v} [CommRing R] [CommRing S] (φ : R →+* S) : CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.restrictScalars φ)

Restriction of scalars along a ring homomorphism preserves finite limits (it is a right adjoint to extension of scalars).

instance PushforwardExactAffine.restrictScalars_preservesFiniteColimits {R S : Type v} [CommRing R] [CommRing S] (φ : R →+* S) : CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.restrictScalars φ)

Restriction of scalars along a ring homomorphism preserves finite colimits (it is a left adjoint to coextension of scalars).

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

Restriction of scalars is exact: it preserves both finite limits and finite colimits.

instance PushforwardExactAffine.pushforward_preservesFiniteLimits {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesFiniteLimits (AlgebraicGeometry.Scheme.Modules.pushforward f)

The pushforward of modules along a morphism of schemes preserves finite limits (left-exactness of f_*).