instHasColimitsOfShapeWalkingParallelPairInd

English

If C has colimits for shape WalkingParallelPair, then Ind(C) has colimits of that shape.

Русский

Если в C существуют колимиты формы WalkingParallelPair, то и в Ind(C) есть колимиты такой формы.

LaTeX

$$$\operatorname{HasColimitsOfShape}(\mathrm{WalkingParallelPair}\, C) \Rightarrow \operatorname{HasColimitsOfShape}(\mathrm{WalkingParallelPair}\,(\mathrm{Ind}\,C))$$$

Lean4

instance [HasColimitsOfShape WalkingParallelPair C] : HasColimitsOfShape WalkingParallelPair (Ind C) :=
  by
  refine ⟨fun F => ?_⟩
  obtain ⟨P⟩ :=
    nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2 (F.obj WalkingParallelPair.one).2
      (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
      (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)
  exact hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

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