closedUnderLimitsOfShape_walkingParallelPair_isIndObject

English

Same as previous: finitary colimit of a diagram in Ind C remains an Ind object.

Русский

То же самое: конечный ко-лимит диаграммы в Ind C остаётся Ind-объектом.

LaTeX

$$$\\text{IsIndColimit}(I) \\Rightarrow \\text{IsIndObject}(\\operatorname{colimit} I)$$$

Lean4

/-- If `C` has equalizers. then ind-objects are closed under equalizers.

This is Proposition 6.1.17(i) in [Kashiwara2006].
-/
theorem closedUnderLimitsOfShape_walkingParallelPair_isIndObject [HasEqualizers C] :
    ClosedUnderLimitsOfShape WalkingParallelPair (IsIndObject (C := C)) :=
  by
  apply closedUnderLimitsOfShape_of_limit
  intro F hF h
  obtain ⟨P⟩ :=
    nonempty_indParallelPairPresentation (h WalkingParallelPair.zero) (h WalkingParallelPair.one)
      (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)
  exact
    IsIndObject.map
      (HasLimit.isoOfNatIso (P.parallelPairIsoParallelPairCompYoneda.symm ≪≫ (diagramIsoParallelPair _).symm)).hom
      (isIndObject_limit_comp_yoneda_comp_colim (parallelPair P.φ P.ψ) (fun i => isIndObject_limit_comp_yoneda _))

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