morphismRestrict_base_coe — Mathlib

English

The underlying base map of the restricted morphism coincides with the restriction of the base map: (f|_U).base = U.1.restrictPreimage f.base.

Русский

Базовая карта ограниченного морфизма совпадает с ограничением базовой карты: (f|_U).base = U.1.restrictPreimage f.base.

LaTeX

$$$\text{base}((f|_U)) = U.1.restrictPreimage( f.\mathrm{base})$$$

Lean4

theorem morphismRestrict_base_coe {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (x) :
    @Coe.coe U Y (⟨fun x => x.1⟩) ((f ∣_ U).base x) = f.base x.1 :=
  congr_arg (fun f => (Scheme.Hom.toLRSHom f).base x) (morphismRestrict_ι f U)

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