hasExactColimitsOfShape — Mathlib

English

If A has finite limits and J is a Grothendieck topology with HasSheafify, then HasExactColimitsOfShape K (Sheaf J A) holds for all K.

Русский

Если A имеет конечные пределы и J — топология Гротениджа с HasSheafify, то у Sheaf J A есть точные колимиты формы K.

LaTeX

$$$\text{HasExactColimitsOfShape } K (\mathrm{Sheaf}\,J\,A)$$$

Lean4

instance hasExactColimitsOfShape [HasFiniteLimits A] [HasSheafify J A] [HasColimitsOfShape K A]
    [HasExactColimitsOfShape K A] : HasExactColimitsOfShape K (Sheaf J A) :=
  (sheafificationAdjunction J A).hasExactColimitsOfShape K

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