isoRestrict_hom_ofRestrict — Mathlib

English

For a LocallyRingedSpace open immersion f, the hom part of the stalk-level restriction is compatible with restriction maps; specifically, restricting f and then composing with the restricted Y-map equals the original f.

Русский

Для открытого вложения f между локально кольцевыми пространствами композиция ограничения гомоморфизмов совместима с ограничениями; то есть ограничение f и затем композиция с ограниченным отображением Y равны исходному f.

LaTeX

$$$(\text{isoRestrict}(f)).hom \; \circ \; Y.ofRestrict\_{} = f$$$

Lean4

@[reassoc (attr := simp)]
theorem isoRestrict_hom_ofRestrict : (isoRestrict f).hom ≫ Y.ofRestrict _ = f :=
  by
  ext1
  dsimp [isoRestrict, isoOfSheafedSpaceIso]
  apply SheafedSpace.forgetToPresheafedSpace.map_injective
  rw [Functor.map_comp, SheafedSpace.forgetToPresheafedSpace.map_preimage]
  exact SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.1

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