of_comp — Mathlib

English

If f: X → Y and g: Y → Z with [IsImmersion g] and [IsImmersion (f ≫ g)], then IsImmersion f.

Русский

Если g — вложение и f ≫ g — вложение, то f — вложение.

LaTeX

$$$\\text{IsImmersion}(f) \\leftarrow \\text{IsImmersion}(f \\circ g)$$$

Lean4

theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion g] [IsImmersion (f ≫ g)] : IsImmersion f
    where
  __ := IsPreimmersion.of_comp f g
  isLocallyClosed_range := by
    rw [← Set.preimage_image_eq (Set.range _) g.isEmbedding.injective]
    have := (f ≫ g).isLocallyClosed_range.preimage g.base.hom.2
    simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] using this

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