English
The left triangle identity in Γ-Spec adjunction holds, ensuring quasi-inverses.
Русский
Левая треугольная идентичность сохраняется для сопряжения Γ-спектра.
LaTeX
$$Same as 36845$$
Lean4
/-- The canonical morphism from `X` to the spectrum of its global sections. -/
@[simps! base]
def toΓSpec : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (op X))
where
__ := X.toΓSpecSheafedSpace
prop := by
intro x
let p : PrimeSpectrum (Γ.obj (op X)) := X.toΓSpecFun x
constructor
-- show stalk map is local hom ↓
let S := (structureSheaf _).presheaf.stalk p
rintro (t : S) ht
obtain ⟨⟨r, s⟩, he⟩ := IsLocalization.surj p.asIdeal.primeCompl t
dsimp at he
set t' := _
change t * t' = _ at he
apply isUnit_of_mul_isUnit_left (y := t')
rw [he]
refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)
apply (notMem_prime_iff_unit_in_stalk _ _ _).mpr
rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]
erw [← he]
rw [RingHom.map_mul]
exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _
