ΓSpec_adjunction_homEquiv_eq — Mathlib

English

A variant of the previous compatibility showing the appTop component after applying the inverse iso and homEquiv.

Русский

Вариация совместимости, показывающая компоненту appTop после применения обратного изоморфизма и гомэквивалентности.

LaTeX

$$ΓSpecIso_inv_ΓSpec_adjunction_homEquiv$$

Lean4

theorem ΓSpec_adjunction_homEquiv_eq {X : Scheme.{u}} {B : CommRingCat} (φ : B ⟶ Γ(X, ⊤)) :
    ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = (Scheme.ΓSpecIso B).hom ≫ φ := by
  rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]

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