toSpecΓ_appTop — Mathlib

English

The symmetrical of the homEquiv sends f to the inverse of the LocallyRingedSpace adjunction applied to f’s LRSHom.

Русский

Обратная гомэквивалентности отправляет f в обратную гомоморфизму локально-кольцевого пространства (LRSHom), применяемую к f.

LaTeX

$$$(ΓSpec.adjunction.homEquiv X R).symm f = (locallyRingedSpaceAdjunction.homEquiv X.1 R).symm f^{toLRSHom}$$$

Lean4

@[simp]
theorem toSpecΓ_appTop (X : Scheme.{u}) : X.toSpecΓ.appTop = (Scheme.ΓSpecIso Γ(X, ⊤)).hom :=
  by
  have := ΓSpec.adjunction.left_triangle_components X
  dsimp at this
  rw [← IsIso.eq_comp_inv] at this
  simp only [Category.id_comp] at this
  rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]

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