English
Again, the diagonal range contains the diagonal of the pullback: Set.range (pullback.diagonal f).base ⊆ diagonalCoverDiagonalRange f 𝒰 𝒱.
Русский
Снова диагональный диапазон содержит диагональ вытяжки: множество образов pullback.diagonal f лежит в diagonalCoverDiagonalRange f 𝒰 𝒱.
LaTeX
$$$\mathrm{range}((\mathrm{pullback.diagonal}\ f).\mathrm{base}) \subseteq \operatorname{diagonalCoverDiagonalRange}(f, \mathcal{U}, \mathcal{V})$$$
Lean4
@[stacks 0DVA]
theorem isSeparated_of_injective (hf : Function.Injective f.base) : IsSeparated f :=
by
constructor
let 𝒰 := Y.affineCover
let 𝒱 (i) := (pullback f (𝒰.f i)).affineCover
refine IsZariskiLocalAtTarget.of_iSup_eq_top (fun i : PUnit.{0} ↦ ⊤) (by simp) fun _ ↦ ?_
rw [← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf]
exact isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱
