instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology

English

If A has colimits of shape J and has weak sheafify with coherent topology, then Condensed A has colimits of shape J.

Русский

Если у категории A есть колимиты по форме J и есть слабое касательноеSheafify в согласованной топологии, то Condensed A имеет колимиты по форме J.

LaTeX

$$$\operatorname{HasColimitsOfShape} J (\text{Condensed } A)$$$

Lean4

instance {A J : Type*} [Category A] [Category J] [HasColimitsOfShape J A]
    [HasWeakSheafify (coherentTopology CompHaus.{u}) A] : HasColimitsOfShape J (Condensed.{u} A) :=
  inferInstanceAs (HasColimitsOfShape J (Sheaf _ _))

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