hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits

English

If D has finite limits and the functor F creates finite limits, then C has finite limits. The existence of limits in C follows from the existence in D and the fact that F creates those limits.

Русский

Если у D существуют конечные пределы и F создаёт конечные пределы, тогда у C существуют конечные пределы. Существование пределов в C следует из существования в D и того факта, что F создаёт эти пределы.

LaTeX

$$$HasFiniteLimits C$ given $HasFiniteLimits D$ and $CreatesFiniteLimits F$$$

Lean4

theorem hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (F : C ⥤ D) [HasFiniteLimits D]
    [CreatesFiniteLimits F] : HasFiniteLimits C where
  out _ _ _ := hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape F

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