refactor(ModuleCat): state pushforward coherence without identifying functor bracketings

[kim-em]

This PR makes the pushforward of (pre)sheaves of modules along the identity functor and along a composition of functors honestly typed. Currently pushforwardId takes 𝟙 S at the type S ⟶ (𝟭 C).op ⋙ S and pushforwardComp takes φ ≫ whiskerLeft F.op ψ at the type S ⟶ (F ⋙ G).op ⋙ T, which only elaborate because Functor.comp, Functor.id and Functor.op unfold. The new pushforwardIdHom and pushforwardCompHom are the unitor and associator composed with Functor.opId/Functor.opComp (see pushforwardIdHom_eq and pushforwardCompHom_eq), and the associativity and unitality isomorphisms of pushforward and pullback are transported along the functor associator and unitors through the new pushforwardCongr₂/pullbackCongr₂ (added at the presheaf level, together with pushforwardCongr, pushforwardNatTrans and pushforwardNatIso). The scheme-level pseudofunctor coherence lemmas in AlgebraicGeometry.Modules.Sheaf are reproved from these, and Adjunction.leftAdjointCompIso_trans is added for that purpose.

It is extracted from Paul Reichert's experiment making Functor.comp and Functor.id instance_reducible (master...leanprover-community:mathlib4-nightly-testing:datokrat/functorcomp, discussed at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency), and is the (pre)sheaf-of-modules half of #43566; it is independent of that PR.

🤖 Prepared with Claude Code

[github-actions]

PR summary ccab94e0d7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ conjugateIsoEquiv_symm_pushforwardCongr
+ leftAdjointCompIso_trans
+ map_id_apply
+ pullback_assoc
+ pullback_comp_id
+ pullback_id_comp
+ pushforwardCompHom_eq
+ pushforwardCompHom_hom
+ pushforwardCongr
+ pushforwardCongr_hom_app_app_apply
+ pushforwardCongr_inv_app_app_apply
+ pushforwardCongr_refl
+ pushforwardCongr_symm
+ pushforwardCongr₂
+ pushforwardCongr₂_hom_app_app_apply
+ pushforwardIdHom_eq
+ pushforwardIdHom_hom
+ pushforwardNatIso
+ pushforwardNatTrans
+ pushforwardNatTrans_app_app_apply
+ pushforward_assoc
++ instance : (pushforward.{v} (pushforwardCompHom φ ψ)).IsRightAdjoint
++ instance : (pushforward.{v} (pushforwardIdHom S)).IsRightAdjoint
++ pullbackCongr₂
++ pushforwardCompHom
++ pushforwardCompHom_assoc
++ pushforwardCompHom_pushforwardIdHom_left
++ pushforwardCompHom_pushforwardIdHom_right
++ pushforwardIdHom
++-- pushforwardId
- instance : (pushforward.{v} (F := F ⋙ G)
- instance : (pushforward.{v} (F := F ⋙ G) (φ ≫ whiskerLeft F.op ψ)).IsRightAdjoint
-++ pushforward_comp_id
-++ pushforward_id_comp
-- instance : (pushforward.{v} (F := 𝟭 C) (𝟙 S)).IsRightAdjoint
--++ pullbackId

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ccab94e).

• +44 new declarations
• −4 removed declarations

+AlgebraicGeometry.Scheme.Modules.conjugateIsoEquiv_symm_pushforwardCongr
+AlgebraicGeometry.Scheme.Modules.pullbackCongr.congr_simp
+AlgebraicGeometry.Scheme.Modules.pullback_assoc
+AlgebraicGeometry.Scheme.Modules.pullback_comp_id
+AlgebraicGeometry.Scheme.Modules.pullback_id_comp
+AlgebraicGeometry.Scheme.Modules.pushforwardCongr.congr_simp
+AlgebraicGeometry.Scheme.Modules.pushforwardCongr_refl
+AlgebraicGeometry.Scheme.Modules.pushforward_assoc
+AlgebraicGeometry.Scheme.Modules.pushforward_comp_id
+AlgebraicGeometry.Scheme.Modules.pushforward_id_comp
+CategoryTheory.Adjunction.leftAdjointCompIso_trans
-PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp
-PresheafOfModules.instIsRightAdjointPushforwardIdFunctorOppositeRingCat
+PresheafOfModules.instIsRightAdjointPushforwardPushforwardCompHom
+PresheafOfModules.instIsRightAdjointPushforwardPushforwardIdHom
+PresheafOfModules.map_id_apply
+PresheafOfModules.pullbackCongr₂
+PresheafOfModules.pushforwardCompHom
+PresheafOfModules.pushforwardCompHom_app
+PresheafOfModules.pushforwardCompHom_assoc
+PresheafOfModules.pushforwardCompHom_eq
+PresheafOfModules.pushforwardCompHom_pushforwardIdHom_left
+PresheafOfModules.pushforwardCompHom_pushforwardIdHom_right
+PresheafOfModules.pushforwardCongr
+PresheafOfModules.pushforwardCongr_hom_app_app_apply
+PresheafOfModules.pushforwardCongr_inv_app_app_apply
+PresheafOfModules.pushforwardCongr_symm
+PresheafOfModules.pushforwardCongr₂
+PresheafOfModules.pushforwardCongr₂_hom_app_app_apply
+PresheafOfModules.pushforwardIdHom
+PresheafOfModules.pushforwardIdHom_app
+PresheafOfModules.pushforwardIdHom_eq
+PresheafOfModules.pushforwardNatIso
+PresheafOfModules.pushforwardNatIso_hom
+PresheafOfModules.pushforwardNatTrans
+PresheafOfModules.pushforwardNatTrans_app_app_apply
-SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous
-SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat
+SheafOfModules.instIsRightAdjointPushforwardPushforwardCompHom
+SheafOfModules.instIsRightAdjointPushforwardPushforwardIdHom
+SheafOfModules.pullbackCongr₂
+SheafOfModules.pushforwardCompHom
+SheafOfModules.pushforwardCompHom_assoc
+SheafOfModules.pushforwardCompHom_hom
+SheafOfModules.pushforwardCompHom_pushforwardIdHom_left
+SheafOfModules.pushforwardCompHom_pushforwardIdHom_right
+SheafOfModules.pushforwardIdHom
+SheafOfModules.pushforwardIdHom_hom

---

Decrease in strong tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency	4684	-3

No changes to weak technical debt.

Current commit ccab94e0d7
Reference commit 572e4d091b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).