preservesLimits_const — Mathlib

English

Let C and D be categories with appropriate structure. The constant functor Const_D: C ⟶ (D ⥤ C) preserves all limits (i.e., limits of every shape J in C are preserved by Const_D).

Русский

Пусть C и D — категории, имеющие необходимые структуры. Постоянный функтор Const_D: C ⟶ (D ⥤ C) сохраняет все пределы (то есть пределы любой формы J в C сохраняются постоянным функтором).

LaTeX

$$$\\text{Const}_D: \\; C \\to \\mathsf{Fun}(D, C) \\text{ preserves all limits}. $$$

Lean4

/-- The constant functor `C ⥤ (D ⥤ C)` preserves limits. -/
instance preservesLimits_const : PreservesLimitsOfSize.{w', w} (const D : C ⥤ _) :=
  preservesLimits_of_evaluation _ fun _ => preservesLimits_of_natIso <| Iso.symm <| constCompEvaluationObj _ _

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