of_comp_of_isOpenImmersion — Mathlib

English

If the composition f ≫ g is dominant and g is an open immersion, then f is dominant.

Русский

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

LaTeX

$$$\\mathrm{IsDominant}(f \\circ g) \\land \\mathrm{IsOpenImmersion}(g) \\Rightarrow \\mathrm{IsDominant}(f)$$$

Lean4

theorem of_comp_of_isOpenImmersion (f : X ⟶ Y) (g : Y ⟶ Z) [H : IsDominant (f ≫ g)] [IsOpenImmersion g] :
    IsDominant f := by
  rw [isDominant_iff, DenseRange] at H ⊢
  simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] at H
  convert H.preimage g.isOpenEmbedding.isOpenMap using 1
  rw [Set.preimage_image_eq _ g.isOpenEmbedding.injective]

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