instIsClosedImmersionLiftCoborder

English

If f is an immersion, then liftCoborder is a closed immersion.

Русский

Если f — вложение, то liftCoborder является замкнутым вложением.

LaTeX

$$$\\text{IsClosedImmersion}(\\text{liftCoborder}(f))$$$

Lean4

instance [IsImmersion f] : IsClosedImmersion f.liftCoborder :=
  by
  have : IsPreimmersion (f.liftCoborder ≫ f.coborderRange.ι) := by simp only [Scheme.Hom.liftCoborder_ι]; infer_instance
  have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι
  refine .of_isPreimmersion _ ?_
  convert isClosed_preimage_val_coborder
  apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.injective
  rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, f.liftCoborder_ι]
  exact (Set.image_preimage_eq_of_subset (by simpa using subset_coborder)).symm

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