English
The proof explains a specific natural isomorphism construction for the subscheme object iso.
Русский
Доказательство строит конкретное естественное изоморфление для подсхемного объекта-изоморфизма.
LaTeX
$$$\text{(proof sketch of an Iso between presheaf quotients and subscheme objects)}$$$
Lean4
theorem subschemeι_app (U : X.affineOpens) :
I.subschemeι.app U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv :=
by
have := I.subschemeCover_map_subschemeι U
simp only [glueDataObjι, Category.assoc, IsAffineOpen.isoSpec_inv_ι] at this
replace this := Scheme.congr_app this U
simp only [comp_coeBase, TopologicalSpace.Opens.map_comp_obj, comp_app, IsAffineOpen.fromSpec_app_self, eqToHom_op,
Category.assoc, Hom.naturality_assoc, TopologicalSpace.Opens.map_top, ← ΓSpecIso_inv_naturality_assoc] at this
simp_rw [← Category.assoc, ← IsIso.comp_inv_eq] at this
simp only [← this, ← Functor.map_inv, inv_eqToHom, Category.assoc, eqToHom_unop, ← Functor.map_comp,
IsIso.Iso.inv_inv, subschemeObjIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op,
Iso.hom_inv_id_assoc, Hom.appIso_inv_naturality_assoc, Functor.op_obj, Functor.op_map, unop_comp, unop_inv,
Quiver.Hom.unop_op, Hom.app_appIso_inv_assoc, TopologicalSpace.Opens.carrier_eq_coe, TopologicalSpace.Opens.map_coe,
homOfLE_leOfHom]
convert (Category.comp_id _).symm
exact CategoryTheory.Functor.map_id _ _
