isOpenImmersion_stableUnderBaseChange

English

Let f: X → Y be an open immersion. For any morphism Z → Y, the base-changed morphism X ×_Y Z → Z is again an open immersion.

Русский

Пусть f: X → Y является открытым вложением. Для любого Морфизма Z → Y базовое Base-изменение X ×_Y Z → Z снова является открытым вложением.

LaTeX

$$$\text{If } f: X \to Y \text{ is an open immersion and } g: Z \to Y, \text{ then } X \times_Y Z \to Z \text{ is an open immersion.}$$$

Lean4

instance isOpenImmersion_stableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsOpenImmersion :=
  MorphismProperty.IsStableUnderBaseChange.mk' <| by intro X Y Z f g _ H; infer_instance

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