English
If X is a qcqs scheme, then the diagonal morphism Δ: X → X × X is quasi-compact (reiterated statement).
Русский
Если X—квазиразделимая схема, диагональ квазиуплотна.
LaTeX
$$$[\\mathrm{QuasiSeparatedSpace}(X)] \\Rightarrow \\mathrm{QuasiCompact}(\\Delta).$$$
Lean4
theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated (f ≫ g)] : QuasiSeparated f :=
by
let 𝒰 := (Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
apply HasAffineProperty.of_openCover ((Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _)
rintro ⟨i, j⟩; dsimp at i j
refine
@quasiSeparatedSpace_of_quasiSeparated _ _ ?_
(HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_
·
exact
pullback.map _ _ _ _ (𝟙 _) _ _ (by simp) (Category.comp_id _) ≫
(pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom
· exact inferInstance
