isUnit_res_toΓSpecMapBasicOpen — Mathlib

English

There is a canonical morphism from the localization of the structure sheaf at the basic open to the presheaf on X, reflecting the adjunction.

Русский

Существует канонический морфизм между локализацией и прешейфом, отражающий сопряжение.

LaTeX

$$$X.toΓSpecCApp : (structureSheaf(Γ(X))).carrier \to X.presheaf(BasicOpen(r)).$$$

Lean4

/-- `r` is a unit as a section on the basic open defined by `r`. -/
theorem isUnit_res_toΓSpecMapBasicOpen : IsUnit (X.toToΓSpecMapBasicOpen r r) :=
  by
  convert
    (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)
  rw [← CommRingCat.comp_apply, ← Functor.map_comp]
  congr

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