instIsIsoSchemeMorphismRestrict — Mathlib

English

If f is an isomorphism, then its restriction f|_U is also an isomorphism.

Русский

Если морфизм f является изоморфизмом, то его ограничение f|_U также является изоморфизмом.

LaTeX

$$$\text{If } f \text{ is an isomorphism, then } f|_U \text{ is an isomorphism.}$$$

Lean4

instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] (U : Y.Opens) : IsIso (f ∣_ U) := by delta morphismRestrict;
  infer_instance

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