morphismRestrictEq — Mathlib

English

Restrictions along two equal opens are canonically isomorphic; if U = V then f|_U ≅ f|_V.

Русский

Ограничения вдоль двух равных открытых множеств естественно изоморфны; если U = V, то f|_U ≅ f|_V.

LaTeX

$$def morphismRestrictEq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) : Arrow.mk (f|_U) ≅ Arrow.mk (f|_V) := eqToIso (by subst e; rfl)$$

Lean4

/-- The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when
unfolded, but it should not matter for now. Replace this definition if better defeqs are needed. -/
def morphismRestrictEq {X Y : Scheme.{u}} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) :
    Arrow.mk (f ∣_ U) ≅ Arrow.mk (f ∣_ V) :=
  eqToIso (by subst e; rfl)

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