instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat

English

If X is a scheme with a subsingleton underlying space and f : Retract X Y is a retract to Y, then the component i of f is a closed immersion.

Русский

Если X — схема с одной точкой в качестве пространства, и f : Retract X Y является ретракцией к Y, то отображение f.i является замкнутым погружением.

LaTeX

$$$\mathrm{IsClosedImmersion}(f.i)$$$

Lean4

instance {X Y : Scheme.{u}} [Subsingleton X] (f : Retract X Y) : IsClosedImmersion f.i :=
  isClosedImmersion_of_comp_eq_id _ _ f.retract

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