English
The diagonal of an affine morphism with qc-structure corresponds to quasi-separatedness of the source. In particular, qcAlong with affine implies quasi-separatedness.
Русский
Диагональ афинного морфизма с qc-структурой соответствует квазисепарабельности источника. В частности, qc + афинность ⇒ квазисепарабельность.
LaTeX
$$$\\text{quasiCompact\_affineProperty\_iff\_quasiSeparatedSpace} \\Big( f \\Big) : \\text{Affine} \\Rightarrow (\\QuasiCompact\\text{ diagonal} ) \\leftrightarrow (\\QuasiSeparatedSpace)$$$
Lean4
theorem quasiSeparatedSpace_iff_affine (X : Scheme) :
QuasiSeparatedSpace X ↔ ∀ U V : X.affineOpens, IsCompact (U ∩ V : Set X) :=
by
rw [quasiSeparatedSpace_iff]
constructor
· intro H U V; exact H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact
· intro H
suffices ∀ (U : X.Opens) (_ : IsCompact U.1) (V : X.Opens) (_ : IsCompact V.1), IsCompact (U ⊓ V).1 by
intro U V hU hU' hV hV'; exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'
intro U hU V hV
refine compact_open_induction_on V hV ?_ ?_
· simp
· intro S _ V hV
change IsCompact (U.1 ∩ (S.1 ∪ V.1))
rw [Set.inter_union_distrib_left]
apply hV.union
clear hV
refine compact_open_induction_on U hU ?_ ?_
· simp
· intro S _ W hW
change IsCompact ((S.1 ∪ W.1) ∩ V.1)
rw [Set.union_inter_distrib_right]
apply hW.union
apply H
