English
For any U ≤ V in the affine opens, the composition of glueDataObjMap with glueDataObjι V equals the composition of glueDataObjι U with the ambient map X.homOfLE h.
Русский
Для любых U ≤ V в афинных открытых подмножеств композиция glueDataObjMap с glueDataObjι V равна композиции glueDataObjι U с глобальной картой X.homOfLE h.
LaTeX
$$$ I.glueDataObjMap h \\; \\gg \\; I.glueDataObjι V = I.glueDataObjι U \\; \\gg \\; X.homOfLE h $$$
Lean4
@[reassoc (attr := simp)]
theorem glueDataObjMap_glueDataObjι {U V : X.affineOpens} (h : U ≤ V) :
I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h :=
by
rw [glueDataObjMap, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, Ideal.quotientMap_comp_mk,
CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι, Category.assoc]
congr 1
rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]
erw [Scheme.Opens.toSpecΓ_SpecMap_map_assoc U.1 V.1 h]
rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]
