English
If U is a compact open subset of an affine scheme, then basic opens corresponding to any section over U are compact.
Русский
Если U — компактное открытое подмножество аффинного схемы, то базовые открытые, соответствующие секциям над U, компактны.
LaTeX
$$$\forall X, \forall U: X.Opens, IsCompact(U) \Rightarrow \forall f \in Γ(X,U), IsCompact(X.basicOpen(f))$$$
Lean4
theorem isCompact_basicOpen (X : Scheme) {U : X.Opens} (hU : IsCompact (U : Set X)) (f : Γ(X, U)) :
IsCompact (X.basicOpen f : Set X) := by
classical
refine ((isCompactOpen_iff_eq_finset_affine_union _).mpr ?_).1
obtain ⟨s, hs, e⟩ := (isCompactOpen_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩
let g : s → X.affineOpens := by
intro V
use V.1 ⊓ X.basicOpen f
have : V.1.1 ⟶ U := by
apply homOfLE; change _ ⊆ (U : Set X); rw [e]
convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X)) V V.prop using 1
erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
exact IsAffineOpen.basicOpen V.1.prop _
haveI : Finite s := hs.to_subtype
refine ⟨Set.range g, Set.finite_range g, ?_⟩
refine (Set.inter_eq_right.mpr (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans ?_
rw [e, Set.iUnion₂_inter]
apply le_antisymm <;> apply Set.iUnion₂_subset
· intro i hi
exact
Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
(@Set.subset_iUnion₂ _ _ _ (fun (i : X.affineOpens) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace)) _
(Set.mem_range_self ⟨i, hi⟩))
· rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩
rw [← hj']
refine Set.Subset.trans ?_ (Set.subset_iUnion₂ j hj)
exact Set.Subset.rfl
