adjunction_homEquiv_apply — Mathlib

English

The Γ-Spec adjunction's homEquiv on a morphism f is exactly the locally ringed space homEquiv applied to f, packaged as a singleton element.

Русский

Гомэквивийность Γ-Spec на отображение f равна применению locallyRingedSpaceAdjunction.homEquiv к f и упаковке результата как одно элементарное отображение.

LaTeX

$$$ΓSpec.adjunction.homEquiv X R f = ⟨locallyRingedSpaceAdjunction.homEquiv X.1 R f⟩$$$

Lean4

theorem adjunction_homEquiv_apply {X : Scheme} {R : CommRingCatᵒᵖ} (f : (op <| Scheme.Γ.obj <| op X) ⟶ R) :
    ΓSpec.adjunction.homEquiv X R f = ⟨locallyRingedSpaceAdjunction.homEquiv X.1 R f⟩ :=
  rfl

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