instance PresheafOfModules.pushforward₀_additive {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ RingCat) : (pushforward₀ F R).Additive

The "naked" pushforward pushforward₀ F R of presheaves of R-modules along F : C ⥤ D (without change of ring) is an additive functor.

instance PresheafOfModules.pushforward₀_preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ RingCat) : CategoryTheory.Limits.PreservesFiniteLimits (pushforward₀ F R)

The pushforward functor pushforward₀ F R preserves finite limits, computed section-wise via the evaluation functors.

instance PresheafOfModules.restrictScalars_preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') : CategoryTheory.Limits.PreservesFiniteLimits (restrictScalars α)

Restriction of scalars along a morphism of presheaves of rings preserves finite limits, evaluation-by-evaluation.

instance PresheafOfModules.pushforward_additive {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) : (pushforward φ).Additive

The full pushforward pushforward φ (which combines pushforward₀ and restriction of scalars via φ) is additive.

instance PresheafOfModules.pushforward_preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) : CategoryTheory.Limits.PreservesFiniteLimits (pushforward φ)

The full pushforward functor pushforward φ on presheaves of modules preserves finite limits, since both factors do.

noncomputable def PresheafOfModules.pushforward_kernel_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) {M N : PresheafOfModules R} (α : M ⟶ N) : (pushforward φ).obj (CategoryTheory.Limits.kernel α) ≅ CategoryTheory.Limits.kernel ((pushforward φ).map α)

Pushforward preserves kernels: the kernel of the pushforward of α is isomorphic to the pushforward of the kernel of α.

theorem PresheafOfModules.pushforward_kernel_iso_inv_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) {M N : PresheafOfModules R} (α : M ⟶ N) : CategoryTheory.CategoryStruct.comp (pushforward_kernel_iso φ α).inv ((pushforward φ).map (CategoryTheory.Limits.kernel.ι α)) = CategoryTheory.Limits.kernel.ι ((pushforward φ).map α)

Compatibility of the kernel isomorphism with the kernel inclusion ι.