right_triangle — Mathlib

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

Похожие утверждения