instOfIsOpenImmersion — Mathlib

English

If f and g are preimmersion, then f ≫ g is preimmersion.

Русский

Если f и g — предварительно вложения, то композиция f ≫ g — также предварительное вложение.

LaTeX

$$$ IsPreimmersion f \land IsPreimmersion g \Rightarrow IsPreimmersion (f \circ g) $$$

Lean4

instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsPreimmersion f
    where
  base_embedding := f.isOpenEmbedding.isEmbedding
  surj_on_stalks _ := (ConcreteCategory.bijective_of_isIso _).2

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