English
The right triangle identity is satisfied for Γ-Spec adjunction on LocallyRingedSpace with any R.
Русский
Правая треугольная идентичность выполняется для сопряжения Γ-Spec на LocallyRingedSpace для любого R.
LaTeX
$$ΓSpec.right_triangle(R) := ...$$
Lean4
/-- `SpecΓIdentity` is iso so these are mutually two-sided inverses. -/
theorem right_triangle (R : CommRingCat) :
identityToΓSpec.app (Spec.toLocallyRingedSpace.obj <| op R) ≫
Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op =
𝟙 _ :=
by
apply LocallyRingedSpace.comp_ring_hom_ext
· ext (p : PrimeSpectrum R)
dsimp
refine PrimeSpectrum.ext (Ideal.ext fun x => ?_)
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p) p.asIdeal x]
rfl
· intro r; apply toOpen_res