English
The pushforward functor along a continuous functor is right adjoint to a suitable pullback functor in the sheaf of modules context.
Русский
Функтор переноса вдоль непрерывного функторa является правым сопряженным к подходящему вытягиванию через тяжевающие пределы модулей.
LaTeX
$$$\mathrm{pushforward}(\varphi) \dashv \mathrm{pullback}(\varphi)$$$
Lean4
/-- Construction of a left adjoint to the functor `pushforward.{v} φ` by using the
pullback of presheaves of modules and the sheafification. -/
noncomputable def adjunction :
(forget S ⋙ PresheafOfModules.pullback.{v} φ.val ⋙ PresheafOfModules.sheafification (𝟙 R.val)) ⊣
pushforward.{v} φ :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun F G ↦
((PresheafOfModules.sheafificationAdjunction (𝟙 R.val)).homEquiv _ _).trans
(((PresheafOfModules.pullbackPushforwardAdjunction φ.val).homEquiv F.val G.val).trans
((fullyFaithfulForget S).homEquiv (Y := (pushforward φ).obj G)).symm)
homEquiv_naturality_left_symm := by
intros
dsimp [Functor.FullyFaithful.homEquiv]
-- these erw seem difficult to remove
erw [Adjunction.homEquiv_naturality_left_symm, Adjunction.homEquiv_naturality_left_symm]
dsimp
simp only [Functor.map_comp, Category.assoc]
homEquiv_naturality_right := by tauto }
