stalkIso_inv — Mathlib

English

The inverse stalk map is exactly the map induced by the inclusion.

Русский

Обратный каркас сталка равен отображению, индуцированному включением.

LaTeX

$$$ (U.stalkIso x)^{-1} = U.ι.stalkMap x $$$

Lean4

theorem stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (x : U) : (U.stalkIso x).inv = U.ι.stalkMap x :=
  by
  rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]
  apply TopCat.Presheaf.stalk_hom_ext
  intro W hxW
  simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]
  convert (Scheme.stalkMap_germ U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm
  refine (U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm
  exact (Set.preimage_image_eq _ Subtype.val_injective).le

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