English
The diagonal of the pullback, restricted to the diagonal range, is a closed immersion.
Русский
Диагональ диагонального вытяжения, ограниченная диагональным диапазоном, является замкнутым вложением.
LaTeX
$$IsClosedImmersion\left(\mathrm{pullback.diagonal}\ f\big|_{\operatorname{diagonalCoverDiagonalRange}(f, \mathcal{U}, \mathcal{V})}\right)$$
Lean4
theorem isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange [∀ i, IsAffine (𝒰.X i)]
[∀ i j, IsAffine ((𝒱 i).X j)] : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱) :=
by
let U : (Σ i, (𝒱 i).I₀) → (diagonalCoverDiagonalRange f 𝒰 𝒱).toScheme.Opens := fun i ↦
(diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange
have hU (i) : (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange :=
by
rw [TopologicalSpace.Opens.functor_obj_map_obj, inf_eq_right, Hom.image_top_eq_opensRange, Opens.opensRange_ι]
exact le_iSup (fun i : Σ i, (𝒱 i).I₀ ↦ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange) i
have hf : iSup U = ⊤ :=
(TopologicalSpace.Opens.map_iSup _ _).symm.trans (diagonalCoverDiagonalRange f 𝒰 𝒱).ι_preimage_self
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsClosedImmersion) _ hf]
intro i
rw [MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictRestrict _ _ _),
MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictEq _ (hU i)),
MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (diagonalRestrictIsoDiagonal ..)]
infer_instance
