toSchemeHom — Mathlib

English

A variant expressing the same identity via an eqToHom relation instead of a hom between opens.

Русский

Вариант выражения через eqToHom вместо гомоморфизма между открытыми множествами.

LaTeX

$$$$ (f.appIso U).inv ≫ f.app (f''ᵁ U) = Y.presheaf.map (eqToHom (preimage_image_eq f U).ge). $$$$

Lean4

/-- If `X ⟶ Y` is an open immersion of PresheafedSpaces, and `Y` is a Scheme, we can
upgrade it into a morphism of Schemes.
-/
def toSchemeHom : toScheme Y f ⟶ Y :=
  ⟨toLocallyRingedSpaceHom _ f⟩

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