English
If a category A has limits of shape J, has exact limits of shape J, and has finite limits, then the condensed category Condensed(A) has exact colimits of shape J. Equivalently, exact colimits are preserved under the condensation process for shape J.
Русский
Если у категории A существуют пределы формы J и они точны, и у A есть конечные пределы, тогда у Condensed(A) существуют точные пределы формы J. Иными словами, свойство точности пределов сохраняется при конденсации.
LaTeX
$$$\\mathrm{HasExactColimitsOfShape}\\,J\\; (\\mathrm{Condensed}\\; A)$$$
Lean4
theorem hasExactColimitsOfShape [HasColimitsOfShape J A] [HasExactColimitsOfShape J A] [HasFiniteLimits A] :
HasExactColimitsOfShape J (Condensed.{u} A) :=
by
let e : Condensed.{u} A ≌ Sheaf (extensiveTopology Stonean.{u}) A :=
(StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
exact HasExactColimitsOfShape.domain_of_functor _ e.functor
