Γ_map — Mathlib

English

On morphisms, the global sections map is given by the C-component of the opposite morphism evaluated at the top open.

Русский

На морфизмах отображение глобальных секций задаётся через компоненту C-части противоположного морфизма на верхнем открытом.

LaTeX

$$$\forall f:\, X^{op}\to Y^{op},\; Γ.map f = f.unop.c.app(\mathrm{op}\top)$$$

Lean4

@[simp]
theorem Γ_map {X Y : (SheafedSpace C)ᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.c.app (op ⊤) :=
  rfl

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