English
Equality of two composed morphisms involving glueDataObjMap and glueDataObjι holds, reflecting functorial coherence.
Русский
Сохранение равенства двух композиций морфизмов glueDataObjMap и glueDataObjι отражает когерентность склейки.
LaTeX
$$$ \\forall U V, \\; I.glueDataObjMap h \\circ I.glueDataObjι V = I.glueDataObjι U \\circ X.homOfLE h $$$
Lean4
theorem ideal_le_ker_glueDataObjι (U V : X.affineOpens) :
I.ideal V ≤ RingHom.ker (U.1.ι.app V.1 ≫ (I.glueDataObjι U).app _).hom :=
by
intro x hx
apply (I.glueDataObj U).IsSheaf.section_ext
intro p hp
obtain ⟨f, g, hfg, hf⟩ :=
exists_basicOpen_le_affine_inter U.2 V.2 ((I.glueDataObjι U).base p).1 ⟨((I.glueDataObjι U).base p).2, hp⟩
refine ⟨(I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f), fun x hx ↦ X.basicOpen_le g (hfg ▸ hx), hf, ?_⟩
have :=
Hom.isIso_app (I.glueDataObjMap (X.affineBasicOpen_le f)) (I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f)
(by rw [opensRange_glueDataObjMap])
apply ((ConcreteCategory.isIso_iff_bijective _).mp this).1
simp only [map_zero, ← RingHom.comp_apply, ← CommRingCat.hom_comp, Category.assoc]
simp only [Scheme.Hom.app_eq_appLE, homOfLE_leOfHom, Scheme.Hom.map_appLE, Scheme.appLE_comp_appLE, Category.assoc,
glueDataObjMap_glueDataObjι_assoc]
rw [Scheme.Hom.appLE]
have H : (X.homOfLE (X.basicOpen_le f) ≫ U.1.ι) ⁻¹ᵁ V.1 = ⊤ :=
by
simp only [Scheme.homOfLE_ι, ← top_le_iff]
exact fun x _ ↦ (hfg.trans_le (X.basicOpen_le g)) x.2
simp only [Scheme.comp_app, Scheme.Opens.ι_app, Scheme.homOfLE_app, ← Functor.map_comp, Scheme.app_eq _ H,
Scheme.Opens.toScheme_presheaf_map, ← Functor.map_comp_assoc, Category.assoc]
simp only [CommRingCat.hom_comp, RingHom.comp_apply]
convert RingHom.map_zero _ using 2
rw [← RingHom.mem_ker, ker_glueDataObjι_appTop, ← Ideal.mem_comap, Ideal.comap_comap, ← CommRingCat.hom_comp]
simp only [Scheme.affineBasicOpen_coe, homOfLE_leOfHom, Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj,
eqToHom_op, eqToHom_unop, ← Functor.map_comp, Scheme.Opens.topIso_hom, Category.assoc]
exact I.ideal_le_comap_ideal (U := X.affineBasicOpen f) (V := V) (hfg.trans_le (X.basicOpen_le g)) hx
