toΓSpecSheafedSpace — Mathlib

English

The triangle formed by the unit of the adjunction and the counit identities commutes, giving a triangular identity.

Русский

Треугольник единицы и counit в сопряжении не нарушается, образуя треугольную идентичность.

LaTeX

$$$toSpecΓ(Γ(X)) \to X \to Γ(X) = id$$$

Lean4

/-- The canonical morphism of sheafed spaces from `X` to the spectrum of its global sections. -/
@[simps]
def toΓSpecSheafedSpace : X.toSheafedSpace ⟶ Spec.toSheafedSpace.obj (op (Γ.obj (op X)))
    where
  base := X.toΓSpecBase
  c := TopCat.Sheaf.restrictHomEquivHom (structureSheaf (Γ.obj (op X))).1 _ isBasis_basic_opens X.toΓSpecCBasicOpens

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