morphismRestrict_appTop — Mathlib

English

A top-level variant expresses the same compatibility for appTop in the restricted morphism.

Русский

Вариант для верхнего уровня выражает ту же совместимость для appTop в ограниченном морфизме.

LaTeX

$$$(f \lvert_U).appTop = f.app (U.ι ''ᵁ ⊤) \;\circ\; X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U ⊤)).op$$$

Lean4

theorem morphismRestrict_appTop {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (f ∣_ U).appTop = f.app (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U ⊤)).op :=
  morphismRestrict_app ..

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