English
There is a fullness property for the opposite of the subscheme functor: for every scheme Y, the functor sending a subscheme of Y to its opposite is full.
Русский
Существуют полнотности для противоположенного конструирования подсхем: для каждой схемы Y соответствующий противоположный-функтор полно представлен.
LaTeX
$$$(IdealSheafData.subschemeFunctor Y).Full$$$
Lean4
theorem toImage_app :
f.toImage.app (f.imageι ⁻¹ᵁ U) =
(f.ker.subschemeObjIso U).hom ≫
CommRingCat.ofHom (Ideal.Quotient.lift _ (f.app U.1).hom (IdealSheafData.ideal_ofIdeals_le _ _)) :=
by
have := ConcreteCategory.epi_of_surjective _ (f.ker.subschemeι_app_surjective U)
rw [← cancel_epi (f.ker.subschemeι.app U), ← Scheme.comp_app, Scheme.congr_app f.toImage_imageι, f.ker.subschemeι_app,
← IsIso.eq_comp_inv, ← Functor.map_inv]
simp only [comp_coeBase, Opens.map_comp_obj, Category.assoc, Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom]
rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom, eqToHom_refl,
CategoryTheory.Functor.map_id]
exact (Category.comp_id _).symm
