hasExactColimitsOfShape_discrete_finite

English

For any finite J, HasExactLimitsOfShape (Discrete J) C holds if C has finite biproducts and finite colimits.

Русский

Для любого конечного J верна точность пределов для дискретной категории Discrete J при наличии конечных бинопродуктов и конечных колимитов в C.

LaTeX

$$$\\forall J\\ (Finite J)\\;\\ HasExactLimitsOfShape(\\Discrete J) C$$$

Lean4

noncomputable instance hasExactColimitsOfShape_discrete_finite (J : Type*) [Finite J] :
    HasExactColimitsOfShape (Discrete J) C where
  preservesFiniteLimits := preservesFiniteLimits_of_natIso HasBiproductsOfShape.colimIsoLim.symm

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