germ_stalkIso_inv — Mathlib

English

Inverse germ-stalk compatibility: the germ from the ambient equals the germ after applying stalkIso inverse.

Русский

Обратная совместимость герма и сталков: germ в X восстанавливается через inverse stalkIso.

LaTeX

$$$ X.presheaf.germ((U.ι ''^ᵁ V)) x \\langle x,hx,rfl \\rangle \\circ (U.stalkIso x)^{-1} = U.toScheme.presheaf.germ V x hx $$$

Lean4

@[reassoc]
theorem germ_stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (V : U.toScheme.Opens) (x : U) (hx : x ∈ V) :
    X.presheaf.germ (U.ι ''ᵁ V) x ⟨x, hx, rfl⟩ ≫ (U.stalkIso x).inv = U.toScheme.presheaf.germ V x hx :=
  PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace U.isOpenEmbedding V x hx

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