English
Under qcqs, the unit of the Γ–Spec adjunction on basic opens is an isomorphism; i.e., the induced map at basicOpen is an isomorphism.
Русский
При qcqs единица adjunction между Γ и Spec на базовых открытых является изоморфизмом.
LaTeX
$$$\\mathrm{IsIso}(X\\to\\mathrm{Spec}\\Gamma(X,\\top)\\text{ on } \\mathrm{basicOpen})$$$
Lean4
/-- If `U` is qcqs, then `Γ(X, D(f)) ≃ Γ(X, U)_f` for every `f : Γ(X, U)`.
This is known as the **Qcqs lemma** in [R. Vakil, *The rising sea*][RisingSea]. -/
instance isIso_ΓSpec_adjunction_unit_app_basicOpen [CompactSpace X] [QuasiSeparatedSpace X] (f : Γ(X, ⊤)) :
IsIso (X.toSpecΓ.app (PrimeSpectrum.basicOpen f)) :=
by
refine
@IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _
?_
rw [ConcreteCategory.isIso_iff_bijective]
apply (config := { allowSynthFailures := true }) IsLocalization.bijective
· exact StructureSheaf.IsLocalization.to_basicOpen _ _
· refine isLocalization_basicOpen_of_qcqs ?_ ?_ _
· exact isCompact_univ
· exact isQuasiSeparated_univ
· simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra, ← Functor.map_comp]
