liftCoborder_ι — Mathlib

English

Any locally closed immersion can be factored as a closed immersion followed by a dominant open immersion: f = coborderRange.ι ∘ liftCoborder.

Русский

Любое локально замкнутое вложение может быть разложено как замкнутое вложение, за которым следует доминирующее открытое вложение: f = coborderRange.ι ∘ liftCoborder.

LaTeX

$$$\\text{liftCoborder}_{X,Y} \\; \\text{and} \\; \\text{coborderRange}.ι \\text{ give } f = \\text{liftCoborder} \\; \\text{then} \\; \\text{coborderRange}.ι$$$

Lean4

/-- Any (locally-closed) immersion can be factored into
a closed immersion followed by a (dominant) open immersion.
-/
@[reassoc (attr := simp)]
theorem liftCoborder_ι (f : X.Hom Y) [IsImmersion f] : f.liftCoborder ≫ f.coborderRange.ι = f :=
  IsOpenImmersion.lift_fac _ _ _

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