English
A restatement of the compatibility between germ maps and stalk-to-fiber homs in the Proj structure sheaf setting.
Русский
Переформулировка совместимости между отображениями зерна и гомоморфизмами стержня-до-фибра в настройке структуры Sheaf для Proj.
LaTeX
$$$$ \\text{germ} \\circ (\\text{stalkToFiberRingHom}) = (\\text{openToLocalization}) $$$$
Lean4
theorem awayToΓ_ΓToStalk (f) (x) :
awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x =
CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr x.2)) ≫
(«Proj».stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
((«Proj».toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.isOpenEmbedding _) x).inv :=
by
rw [awayToΓ, Category.assoc, ← Category.assoc _ (Iso.inv _), Iso.eq_comp_inv, Category.assoc, Category.assoc,
Presheaf.Γgerm]
rw [LocallyRingedSpace.restrictStalkIso_hom_eq_germ]
simp only [«Proj».toLocallyRingedSpace, «Proj».toSheafedSpace]
rw [Presheaf.germ_res, awayToSection_germ]
rfl
