+ IsLocallyInjective
+ IsLocallySurjective
+ colimitPresheafOfModules
+ comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom
+ congr_map_apply
+ forgetToPresheafModuleCatObjMap
+ forgetToPresheafModuleCatObjMap_apply
+ forgetToPresheafModuleCatObjObj
+ forgetToPresheafModuleCatObjObj_coe
+ forgetToRingCat_map_apply
+ forgetToRingCat_obj
+ homMk
+ hom_ext
+ id_app
+ instance (M : PresheafOfModules R) (X : Cᵒᵖ) :
+ instance (X : Cᵒᵖ) : (evaluation.{v} R X).Additive
+ instance : Add (M₁ ⟶ M₂)
+ instance : AddCommGroup (M₁ ⟶ M₂)
+ instance : Category (PresheafOfModules.{v} R)
+ instance : IsLocallyInjective J (toSheafify α φ) := by
+ instance : IsLocallySurjective J (toSheafify α φ) := by
+ instance : Neg (M₁ ⟶ M₂)
+ instance : Sub (M₁ ⟶ M₂)
+ instance : Zero (M₁ ⟶ M₂)
+ instance {J : Type*} [Category J] (j : J) : ((evaluation J C).obj j).Additive
+ limitPresheafOfModules
+ map_smul
+ ofPresheaf
+ ofPresheaf_presheaf
+ presheaf_map_apply_coe
+ presheaf_obj_coe
+ restrictScalarsCompToPresheaf
+ restrictScalarsObj
+ sections.eval
+ toPresheaf_map_app_apply
+ toPresheaf_map_sheafificationAdjunction_unit_app
+ toPresheaf_map_sheafificationHomEquiv
+ toPresheaf_map_sheafificationHomEquiv_def
+ toPresheaf_map_toSheafify
+ toPresheaf_obj_coe
+ toSheafify_app_apply
+ zsmul_app
- BundledCorePresheafOfModules
- CorePresheafOfModules
- app
- colimitBundledCore
- colimitCoconeιApp
- colimitCoconeιApp_naturality
- comp
- comp_hom
- comp_sheafifyHomEquiv'_symm_hom
- ext
- id
- id_hom
- instance (X : Cᵒᵖ) : (evaluation R X).Additive
- instance (X : Cᵒᵖ) : Module (R.obj X) (M.presheaf.obj X) := M.module X
- instance (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X))
- instance : Add (P ⟶ Q) := ⟨fun f g => mk (f.hom + g.hom) (by
- instance : AddCommGroup (P ⟶ Q)
- instance : Category (PresheafOfModules R)
- instance : Neg (P ⟶ Q) := ⟨fun f => mk (-f.hom) (by
- instance : Presheaf.IsLocallyInjective J (toSheafify α φ).hom := by
- instance : Presheaf.IsLocallySurjective J (toSheafify α φ).hom := by
- instance : Sub (P ⟶ Q) := ⟨fun f g => mk (f.hom - g.hom) (by
- instance : Zero (P ⟶ Q) := ⟨mk 0 (by
- instance {R : Dᵒᵖ ⥤ RingCat.{u}} (P : PresheafOfModules.{v} R) (F : C ⥤ D) (X : Cᵒᵖ) :
- instance {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
- limitBundledCore
- limitConeπApp
- limitConeπApp_naturality
- map
- map_apply
- map_comp
- map_id
- mk'
- mk''
- mk'_app
- obj
- preTildeInAddCommGrp
- pushforward_obj_obj
- relativeDifferentials'BundledCore
- relativeDifferentials'_map_apply
- relativeDifferentials'_obj
- restrictScalarsBundledCore
- restrictionApp
- restrictionApp_apply
- restrictionApp_comp
- restrictionApp_id
- restrictionApp_naturality
- restrictionApp_toPresheafOfModules
- sheafificationAdjunction_unit_app_hom
- sheafificationHomEquiv_hom
- sheafificationHomEquiv_hom'
- tildeInAddCommGrp
- toCorePresheafOfModules
- toPresheaf_map_app
- unitCore
-- toPresheafOfModules
-- toPresheafOfModules_obj
-- toPresheafOfModules_presheaf_map_apply

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.