English
The right triangle identity holds in the Γ-Spec adjunction for any R.
Русский
Правый треугольник выполняется для любой кольцевой области R.
LaTeX
$$$identityToΓSpec.app (Spec.toLocallyRingedSpace.obj ⟨R⟩) ≫ Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R)= id$$$
Lean4
/-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
of `Γ(X, ⊤)` under `toΓSpec` agrees with the associated zero locus on `X`. -/
theorem toΓSpec_preimage_zeroLocus_eq {X : LocallyRingedSpace.{u}} (s : Set (X.presheaf.obj (op ⊤))) :
X.toΓSpec.base ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s :=
by
simp only [RingedSpace.zeroLocus]
have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
(SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ = X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ :=
by
symm
rw [Set.preimage_compl, Opens.carrier_eq_coe]
erw [X.toΓSpec_preimage_basicOpen_eq i]
erw [Set.iInter₂_congr this]
simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl]
rw [← PrimeSpectrum.zeroLocus_iUnion₂]
simp
