isDominant_homOfLE — Mathlib

English

Let X be a scheme and U ⊆ V be open subschemes of X with U dense in X. Then the natural morphism X|U → X|V is dominant.

Русский

Пусть X — схема, U ⊆ V — открытые подсхемы X, причём U плотно входит в X. Тогда естественный морфизм X|U → X|V является доминирующим.

LaTeX

$$$\text{If } U \subseteq V \text{ are open subschemes of } X \text{ with } \overline{U}=X, \text{ then } X|U \to X|V \text{ is dominant.}$$$

Lean4

theorem isDominant_homOfLE {U V : X.Opens} (hU : Dense (X := X) U) (hU' : U ≤ V) : IsDominant (X.homOfLE hU') :=
  have : IsDominant (X.homOfLE hU' ≫ Opens.ι _) := by simpa using Opens.isDominant_ι hU
  IsDominant.of_comp_of_isOpenImmersion (g := Opens.ι _) _

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