eq_presheaf_map_eqToHom — Mathlib

English

If two subopens V, W of U correspond under the inclusion U.ι, then the induced presheaf maps agree after applying the appropriate eqToHom.

Русский

Если два подпуста V и W открыты в U и соответствуют включению U.ι, то порождающие отображения расшитого пространства согласуются после применения соответствующего eqToHom.

LaTeX

$$$ X.presheaf.map (eqToHom e).op = U.toScheme.presheaf.map (eqToHom \\<| U.isOpenEmbedding.functor_obj_injective e).op $$$

Lean4

theorem eq_presheaf_map_eqToHom {V W : Opens U} (e : U.ι ''ᵁ V = U.ι ''ᵁ W) :
    X.presheaf.map (eqToHom e).op = U.toScheme.presheaf.map (eqToHom <| U.isOpenEmbedding.functor_obj_injective e).op :=
  rfl

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