English
In the same setup as comapIso_inv_subschemeι, the composed map (I.comapIso f).hom followed by pullback.fst equals the subscheme embedding (I.comap f).subschemeι.
Русский
В той же конфигурации, как и comapIso_inv_subschemeι, композиция (I.comapIso f).hom затем pullback.fst совпадает с вложением subschemeι для comap f.
LaTeX
$$$(I.comapIso f).hom \cdot pullback.fst _ _ = (I.comap f).subschemeι$$$
Lean4
/-- The functor taking a morphism into `Y` to its kernel as an ideal sheaf on `Y`. -/
@[simps]
def kerFunctor (Y : Scheme.{u}) : (Over Y)ᵒᵖ ⥤ IdealSheafData Y
where
obj f := f.unop.hom.ker
map {f g}
hfg :=
homOfLE <| by
simpa only [Functor.id_obj, Functor.const_obj_obj, OrderDual.toDual_le_toDual, ← Over.w hfg.unop] using
hfg.unop.left.le_ker_comp f.unop.hom
map_id _ := Subsingleton.elim _ _
map_comp _ _ := Subsingleton.elim _ _
