commuting — Mathlib

English

If D: J ⥤ Coalgebra T has a limit after forgetting, and T preserves limits of shape J, then D has a limit.

Русский

Если D: J ⥤ Coalgebra T имеет предел после забывания и T сохраняет пределы формы J, то D имеет предел.

LaTeX

$$$\\operatorname{HasLimit}(D \\circ \\operatorname{forget} T) \\Rightarrow \\operatorname{HasLimit} D$, assuming $\\operatorname{PreservesLimitsOfShape}(J, T)$.$$

Lean4

/-- (Impl) The key property defining the map `λ : L ⟶ TL`. -/
theorem commuting (j : J) : lambda c t ≫ (T : C ⥤ C).map (c.π.app j) = c.π.app j ≫ (D.obj j).a :=
  (isLimitOfPreserves _ t).fac (newCone c) j

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