sheafifyMap — Mathlib

English

The sheafification process assigns to P a functorial object representing its global sections through a double application of plus.

Русский

Процесс шеффизации присваивает P формальный объект глобальных секций через двойное применение plus.

LaTeX

$$toSheafify : (Cᵒᵖ ⥤ D) ⥤ (Cᵒᵖ ⥤ D)$$

Lean4

/-- The canonical map on sheafifications induced by a morphism. -/
noncomputable def sheafifyMap {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) : J.sheafify P ⟶ J.sheafify Q :=
  J.plusMap <| J.plusMap η

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