instHasLimitCompOfPreservesLimit — Mathlib

English

If K : J ⥤ C has a limit and F : C ⥤ D preserves that limit, then the composite K ⋙ F has a limit; i.e., the limit of K is transported along F.

Русский

Если у K: J ⥤ C есть предел, и F: C ⥤ D сохраняет этот предел, то композиция K ⋙ F имеет предел; то есть предел K переносится вдоль F.

LaTeX

$$$$\text{If } \mathrm{HasLimit}(K) \text{ and } \mathrm{PreservesLimit}(K,F), \ \mathrm{HasLimit}(K\cdot F).$$$$

Lean4

instance [HasLimit K] {F : C ⥤ D} [PreservesLimit K F] : HasLimit (K ⋙ F) where
  exists_limit := ⟨_, isLimitOfPreserves F (limit.isLimit K)⟩

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