of_comp — Mathlib

English

If f and g are as above, and the composite f ≫ g is a closed immersion with some affine hypotheses, then the restricted diagonal is a closed immersion (Elaborated form of is ClosedImmersion).

Русский

Если композиция f ≫ g является замкнутым вложением и выполняются аффинные условия, то ограниченная диагональ — замкнутое вложение.

LaTeX

$$IsClosedImmersion\left(\mathrm{pullback.diagonal}\ f \restriction_{\operatorname{diagonalCoverDiagonalRange}(f, \mathcal{U}, \mathcal{V})}\right)$$

Lean4

theorem of_comp [IsClosedImmersion (f ≫ g)] [IsSeparated g] : IsClosedImmersion f :=
  by
  rw [← pullback.lift_snd (𝟙 _) f (Category.id_comp (f ≫ g))]
  infer_instance

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