hasGlobalSectionsFunctor_of_hasLimitsOfShape

English

If A has limits of shape C^op, then there is a global sections functor for J and A.

Русский

Если у A существуют пределы по shape C^op, то существует глобальная секционная функция Γ для J и A.

LaTeX

$$$[HasLimitsOfShape\ C^\mathrm{op}\ A] \Rightarrow [HasGlobalSectionsFunctor\ J\ A]$$$

Lean4

/-- Every site `C` admits a global sections functor for `A`-valued sheaves when `A` has limits of
shape `Cᵒᵖ`. -/
instance hasGlobalSectionsFunctor_of_hasLimitsOfShape [HasLimitsOfShape Cᵒᵖ A] : HasGlobalSectionsFunctor J A :=
  ⟨sheafToPresheaf J A ⋙ lim, ⟨constLimAdj.comp (sheafificationAdjunction J A)⟩⟩

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