English
A compatibility lemma for composition of ring homomorphisms with basic opens used to glue across X and Spec.
Русский
Лемма совместимости композиции кольцевых гомоморфизмов с ограничениями на базовые открытые множества.
LaTeX
$$comp_ring_hom_ext ...$$
Lean4
theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f : R ⟶ Γ.obj (op X)}
{β : X ⟶ Spec.locallyRingedSpaceObj R} (w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base)
(h :
∀ r : R,
f ≫ X.presheaf.map (homOfLE le_top : (Opens.map β.base).obj (basicOpen r) ⟶ _).op =
toOpen R (basicOpen r) ≫ β.c.app (op (basicOpen r))) :
X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β := by
ext1
refine Spec.basicOpen_hom_ext w ?_
intro r U
rw [LocallyRingedSpace.comp_c_app]
erw [toOpen_comp_comap_assoc]
rw [Category.assoc]
erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]
exact h r
