instance
L34 ↗(anonymous instance)
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)Lean source · statement
instance : (PresheafOfModules.pushforward.{u} (F := Opens.map f.base)
f.toRingCatSheafHom.hom).IsRightAdjoint