English
A scheme X is quasi-separated if and only if its diagonal morphism is qc and matches compact intersections of affine opens.
Русский
Схема X квазизадроблена тогда, когда её диагональная морфизма квази-компактна и совпадает по свойствам с компактными пересечениями аффинных открытых.
LaTeX
$$$QuasiSeparatedSpace X \\iff \\text{diagonal}(X) \\text{ is qc and intersections of affine opens are compact}$$$
Lean4
theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) :
AffineTargetMorphismProperty.diagonal (fun X _ _ _ ↦ CompactSpace X) f ↔ QuasiSeparatedSpace X :=
by
delta AffineTargetMorphismProperty.diagonal
rw [quasiSeparatedSpace_iff_affine]
constructor
· intro H U V
haveI : IsAffine _ := U.2
haveI : IsAffine _ := V.2
let g : pullback U.1.ι V.1.ι ⟶ X := pullback.fst _ _ ≫ U.1.ι
have : IsOpenImmersion g := inferInstance
have e := this.base_open.isEmbedding.toHomeomorph
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
erw [Subtype.range_coe, Subtype.range_coe] at e
rw [isCompact_iff_compactSpace]
exact @Homeomorph.compactSpace _ _ _ _ (H _ _) e
· introv H h₁ h₂
let g : pullback f₁ f₂ ⟶ X := pullback.fst _ _ ≫ f₁
have : IsOpenImmersion g := inferInstance
have e := this.base_open.isEmbedding.toHomeomorph
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
simp_rw [isCompact_iff_compactSpace] at H
exact
@Homeomorph.compactSpace _ _ _ _
(H ⟨⟨_, h₁.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩
⟨⟨_, h₂.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩)
e.symm
