germ_stalkIso_hom — Mathlib

English

Germs commute with the stalk isomorphism; the germ map on V followed by the stalk isomorphism equals the germ map on the ambient scheme.

Русский

Гермы коммутируют с изоморфизмом сталков; отображение germs на V далее через stalkIso равно отображению germs в X.

LaTeX

$$$ U. presheaf.germ(V,x,hx) \\; \\circ \\left(U.stalkIso(x)\\right)^{\\mathrm{hom}} = X.presheaf.germ((U.ι ''^ᵁ V) , x.1, \\langle x,hx,rfl \\rangle ) $$$

Lean4

@[reassoc (attr := simp)]
theorem germ_stalkIso_hom {X : Scheme.{u}} (U : X.Opens) {V : U.toScheme.Opens} (x : U) (hx : x ∈ V) :
    U.toScheme.presheaf.germ V x hx ≫ (U.stalkIso x).hom = X.presheaf.germ (U.ι ''ᵁ V) x.1 ⟨x, hx, rfl⟩ :=
  PresheafedSpace.restrictStalkIso_hom_eq_germ _ U.isOpenEmbedding _ _ _

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