instIsClosedImmersionFstScheme — Mathlib

English

A surjective closed immersion is an isomorphism when the target is reduced.

Русский

Замкнутое вложение, которое сюръективно, является изоморфизмом, если цель редуцирована.

LaTeX

$$IsIso(f) if IsClosedImmersion(f) and Surjective(f) and IsReduced(target)$$

Lean4

instance {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion g] : IsClosedImmersion (Limits.pullback.fst f g) :=
  MorphismProperty.pullback_fst _ _ ‹_›

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