toStalk_stalkMap_toSpec — Mathlib

English

A variant refinement expresses how the IsLocalization data behaves with respect to different representations of the same localization at a prime; the equality is preserved under exchange of representations.

Русский

Вариант уточнения описывает согласованность данных IsLocalization при различных представлениях локализации по одному и тому же простому идеалу; равенство сохраняется при смене представления.

LaTeX

$$$$\text{Eq}\bigl( \text{IsLocalization.mk' S x_1 y_1}, \text{IsLocalization.mk' S x_2 y_2} \bigr)$$$$

Lean4

@[reassoc]
theorem toStalk_stalkMap_toSpec (f) (x) :
    StructureSheaf.toStalk _ _ ≫ (toSpec 𝒜 f).stalkMap x = awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x :=
  by
  rw [StructureSheaf.toStalk, Category.assoc]
  simp_rw [← «Spec».locallyRingedSpaceObj_presheaf']
  rw [LocallyRingedSpace.stalkMap_germ (toSpec 𝒜 f), toOpen_toSpec_val_c_app_assoc, Presheaf.germ_res]
  rfl

Похожие утверждения