adjunction_homEquiv_symm_apply — Mathlib

English

The inverse of the homEquiv in the Γ-Spec adjunction corresponds to the inverse of the locally ringed space homEquiv on the underlying morphism.

Русский

Обратная гомэквивательности Γ-Spec соответствует обратной гомэквивательности локально-кольцевого пространства на соответствующем отображении.

LaTeX

$$$(ΓSpec.adjunction.homEquiv X R).symm f = (locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R).symm (f.toLRSHom)$$$

Lean4

theorem adjunction_homEquiv_symm_apply {X : Scheme} {R : CommRingCatᵒᵖ} (f : X ⟶ Scheme.Spec.obj R) :
    (ΓSpec.adjunction.homEquiv X R).symm f = (locallyRingedSpaceAdjunction.homEquiv X.1 R).symm f.toLRSHom :=
  rfl

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