Pulling back connected colimits

If c is a cocone over a functor J ⥤ C and f : X ⟶ c.pt, then for every j : J we can take the pullback of c.ι.app j and f. This gives a new cocone with cone point X. We show that if c is a colimit cocone, then this is again a colimit cocone as long as J is connected and C has exact colimits of shape J.

From this we deduce a hom_ext principle for morphisms factoring through a colimit. Usually, we only get hom_ext for morphisms from a colimit, so this is something a bit special.

The connectedness assumption on J is necessary: take C to be the category of abelian groups, let f : ℤ → ℤ ⊕ ℤ be the diagonal map, and let g := 𝟙 (ℤ ⊕ ℤ). Then the hypotheses of IsColimit.pullback_zero_ext are satisfied, but f ≫ g is not zero.

noncomputable def CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasPullbacks C] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] {F : Functor J C} {c : Cocone F} (hc : IsColimit c) {X : C} (f : X ⟶ c.pt) : IsColimit { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }

If c is a cocone over a functor J ⥤ C and f : X ⟶ c.pt, then for every j : J we can take the pullback of c.ι.app j and f. This gives a new cocone with cone point X, and this cocone is again a colimit cocone as long as J is connected and C has exact colimits of shape J.

Equations

• hc.pullbackOfHasExactColimitsOfShape f = { pt := X, ι := CategoryTheory.Limits.pullback.snd c.ι ((CategoryTheory.Functor.const J).map f) }.isColimitOfIsIsoColimMapι

theorem CategoryTheory.Limits.IsColimit.pullback_hom_ext {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasPullbacks C] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] {F : Functor J C} {c : Cocone F} (hc : IsColimit c) {X Y : C} {f : X ⟶ c.pt} {g h : c.pt ⟶ Y} (hf : ∀ (j : J), CategoryStruct.comp (pullback.snd (c.ι.app j) f) (CategoryStruct.comp f g) = CategoryStruct.comp (pullback.snd (c.ι.app j) f) (CategoryStruct.comp f h)) : CategoryStruct.comp f g = CategoryStruct.comp f h

Detecting equality of morphisms factoring through a connected colimit by pulling back along the inclusions of the colimit.

theorem CategoryTheory.Limits.IsColimit.pullback_zero_ext {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasPullbacks C] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] {F : Functor J C} {c : Cocone F} (hc : IsColimit c) {X Y : C} {f : X ⟶ c.pt} {g : c.pt ⟶ Y} (hf : ∀ (j : J), CategoryStruct.comp (pullback.snd (c.ι.app j) f) (CategoryStruct.comp f g) = 0) : CategoryStruct.comp f g = 0

Detecting vanishing of a morphism factoring through a connected colimit by pulling back along the inclusions of the colimit.

noncomputable def CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] {F : Functor J C} {c : Cone F} (hc : IsLimit c) {X : C} (f : c.pt ⟶ X) : IsLimit { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }

If c is a cone over a functor J ⥤ C and f : c.pt ⟶ X, then for every j : J we can take the pushout of c.π.app j and f. This gives a new cone with cone point X, and this cone is again a limit cone as long as J is connected and C has exact limits of shape J.

Equations

• hc.pushoutOfHasExactLimitsOfShape f = { pt := X, π := CategoryTheory.Limits.pushout.inr c.π ((CategoryTheory.Functor.const J).map f) }.isLimitOfIsIsoLimMapπ

theorem CategoryTheory.Limits.IsLimit.pushout_hom_ext {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] {F : Functor J C} {c : Cone F} (hc : IsLimit c) {X Y : C} {g h : Y ⟶ c.pt} {f : c.pt ⟶ X} (hf : ∀ (j : J), CategoryStruct.comp g (CategoryStruct.comp f (pushout.inr (c.π.app j) f)) = CategoryStruct.comp h (CategoryStruct.comp f (pushout.inr (c.π.app j) f))) : CategoryStruct.comp g f = CategoryStruct.comp h f

Detecting equality of morphisms factoring through a connected limit by pushing out along the projections of the limit.

theorem CategoryTheory.Limits.IsLimit.pushout_zero_ext {J : Type w} [Category.{w', w} J] [IsConnected J] {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] {F : Functor J C} {c : Cone F} (hc : IsLimit c) {X Y : C} {g : Y ⟶ c.pt} {f : c.pt ⟶ X} (hf : ∀ (j : J), CategoryStruct.comp g (CategoryStruct.comp f (pushout.inr (c.π.app j) f)) = 0) : CategoryStruct.comp g f = 0

Detecting vanishing of a morphism factoring though a connected limit by pushing out along the projections of the limit.