ΓSpecIso_inv_ΓSpec_adjunction_homEquiv

English

Given φ: B ⟶ Γ(X, ⊤), composing with ΓSpecIso’s inverse and taking appTop recovers φ.

Русский

Дано φ: B ⟶ Γ(X, ⊤); применение обратного ΓSpecIso и appTop восстанавливают φ.

LaTeX

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

Lean4

theorem ΓSpecIso_inv_ΓSpec_adjunction_homEquiv {X : Scheme.{u}} {B : CommRingCat} (φ : B ⟶ Γ(X, ⊤)) :
    (Scheme.ΓSpecIso B).inv ≫ ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = φ :=
  by
  simp only [Adjunction.homEquiv_apply, Scheme.Spec_map, Opens.map_top, Scheme.comp_app]
  simp

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