English
An isomorphism interacts compatibly with pullbacks and refinements; the inverse composes with pullbackHom to give a transport along the refinement.
Русский
Изоморфизм совместим с тягодравлением и уточнением; обратная композиция с pullbackHom даёт перенос вдоль уточнения.
LaTeX
$$$$ (\mathcal{U}.pullbackCoverAffineRefinementObjIso f i)^{-1} \\circ (\mathcal{U}.affineRefinement.openCover.pullbackHom f i) = \\circ ((\mathcal{U}.X i.1).affineCover.pullbackHom (\mathcal{U}.pullbackHom f i.1)) i.2 $$$$
Lean4
theorem compactSpace {X : Scheme.{u}} (𝒰 : X.OpenCover) [Finite 𝒰.I₀] [H : ∀ i, CompactSpace (𝒰.X i)] :
CompactSpace X := by
cases nonempty_fintype 𝒰.I₀
rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]
apply isCompact_iUnion
intro i
rw [isCompact_iff_compactSpace]
exact
@Homeomorph.compactSpace _ _ _ _ (H i)
(TopCat.homeoOfIso
(asIso
(IsOpenImmersion.isoOfRangeEq (𝒰.f i)
(X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
Subtype.range_coe.symm).hom.base))
