English
There is a natural adjunction between the opposite of the subscheme construction on Y and the kernel functor on Y.
Русский
Существует естественнаяAdjunction между противоположенным конструктором подсхем над Y и кер-функтором над Y.
LaTeX
$$$\\text{kerAdjunction}(Y) : (\\text{subschemeFunctor } Y)^{\\mathrm{rightOpp}} \\dashv Y.\\kerFunctor$$$
Lean4
/-- The adjunction between `Y.IdealSheafData` and `(Over Y)ᵒᵖ` given by taking kernels. -/
@[simps]
noncomputable def kerAdjunction (Y : Scheme.{u}) : (subschemeFunctor Y).rightOp ⊣ Y.kerFunctor
where
unit.app I := eqToHom (by simp)
counit.app f := (Over.homMk f.unop.hom.toImage f.unop.hom.toImage_imageι).op
counit.naturality _ _ _ := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
left_triangle_components I := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
