English
For qcqs X, there is an isomorphism given by the Γ-Spec adjunction unit on basic opens: the morphism X.toSpecΓ.app(PrimeSpectrum.basicOpen f) is an isomorphism.
Русский
Для qcqs X имеется изоморфизм, задаваемый единицей дуги между Γ и Spec на базовом открытом D(f).
LaTeX
$$$$\\text{IsIso} \\big( X.toSpecΓ.app (\\mathrm{PrimeSpectrum.basicOpen} f) \\big)$$$$
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]. -/
theorem isLocalization_basicOpen_of_qcqs {X : Scheme} {U : X.Opens} (hU : IsCompact U.1) (hU' : IsQuasiSeparated U.1)
(f : Γ(X, U)) : IsLocalization.Away f (Γ(X, X.basicOpen f)) :=
by
constructor
· rintro ⟨_, n, rfl⟩
simp only [map_pow, RingHom.algebraMap_toAlgebra]
exact IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)
· intro z
obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z
refine ⟨⟨y, _, n, rfl⟩, ?_⟩
simpa only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra, mul_comm z] using e.symm
· intro x y
rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]
simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]
generalize x - y = z
intro H
obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU _ _ H
refine ⟨⟨_, n, rfl⟩, ?_⟩
simpa [mul_comm z] using e
