English
There exists an affine-like property ensuring quasi-compactness of the carrier under the quasi-compact condition; formalizing that CompactSpace on the carrier is preserved under affine transformations.
Русский
Существование аффиноподобного свойства, обеспечивающего квази-компактность переносчика при квази-компактности; сохранение CompactSpace на носителе при аффинных преобразованиях.
LaTeX
$$$\exists$-style property asserting that quasi-compactness is reflected/preserved by affine structure on carriers.$$
Lean4
instance : HasAffineProperty @QuasiCompact (fun X _ _ _ ↦ CompactSpace X)
where
eq_targetAffineLocally' := by
ext X Y f
simp only [quasiCompact_iff_forall_affine, isCompact_iff_compactSpace, targetAffineLocally, Subtype.forall]
rfl
isLocal_affineProperty := by
constructor
· apply AffineTargetMorphismProperty.respectsIso_mk <;> rintro X Y Z e _ _ H
exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.base)), H]
· introv _ H
change CompactSpace ((Opens.map f.base).obj (Y.basicOpen r))
rw [Scheme.preimage_basicOpen f r]
erw [← isCompact_iff_compactSpace]
rw [← isCompact_univ_iff] at H
apply isCompact_basicOpen
exact H
· rintro X Y H f S hS hS'
rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS
· rw [← isCompact_univ_iff]
change IsCompact ((Opens.map f.base).obj ⊤).1
rw [← hS]
dsimp [Opens.map]
simp only [Opens.iSup_mk, Opens.coe_mk, Set.preimage_iUnion]
exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)
· exact isAffineOpen_top _
