SpecMap_ΓSpecIso_hom — Mathlib

English

The inverse of the ΓSpecIso composed with the appTop of homEquiv recovers φ.

Русский

Обратный ΓSpecIso, примененный через appTop гомэквививалентности восстанавливает φ.

LaTeX

$$(Scheme.ΓSpecIso B).inv ≫ ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = φ$$

Lean4

@[simp]
theorem SpecMap_ΓSpecIso_hom (R : CommRingCat.{u}) : Spec.map ((Scheme.ΓSpecIso R).hom) = (Spec R).toSpecΓ :=
  by
  have := ΓSpec.adjunction.right_triangle_components (op R)
  dsimp at this
  rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this

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