sigmaConst.obj preserves colimits

Given an object R in a category C with coproducts of size w, the functor sigmaConst.obj R : Type w ⥤ C which sends a type T to the coproduct of copies of R indexed by T preserves all colimits.

instance CategoryTheory.Limits.instPreservesColimitsOfSizeObjFunctorTypeSigmaConst {C : Type u} [Category.{v, u} C] [HasCoproducts C] (R : C) : PreservesColimitsOfSize.{v', u', w, v, w + 1, u} (sigmaConst.obj R)

noncomputable def CategoryTheory.Limits.sigmaConstCokernelCofork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] : CokernelCofork (Sigma.map' f fun (x : α) => CategoryStruct.id R)

A colimit cokernel cofork for the map ∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R induced by a map f : α → β.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.sigmaConstCokernelCofork_pt {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] : (sigmaConstCokernelCofork R f).pt = ∐ fun (x : ↑(Set.range f)ᶜ) => R

theorem CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] (b : β) (hb : b ∉ Set.range f) : CategoryStruct.comp (Sigma.ι (fun (x : β) => R) b) (Cofork.π (sigmaConstCokernelCofork R f)) = Sigma.ι (fun (x : ↑(Set.range f)ᶜ) => R) ⟨b, hb⟩

theorem CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] (b : β) (hb : b ∉ Set.range f) {Z : C} (h : (∐ fun (x : ↑(Set.range f)ᶜ) => R) ⟶ Z) : CategoryStruct.comp (Sigma.ι (fun (x : β) => R) b) (CategoryStruct.comp (Cofork.π (sigmaConstCokernelCofork R f)) h) = CategoryStruct.comp (Sigma.ι (fun (x : ↑(Set.range f)ᶜ) => R) ⟨b, hb⟩) h

@[simp]

theorem CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] (a : α) : CategoryStruct.comp (Sigma.ι (fun (x : β) => R) (f a)) (Cofork.π (sigmaConstCokernelCofork R f)) = 0

@[simp]

theorem CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_eq_zero_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] (a : α) {Z : C} (h : (∐ fun (x : ↑(Set.range f)ᶜ) => R) ⟶ Z) : CategoryStruct.comp (Sigma.ι (fun (x : β) => R) (f a)) (CategoryStruct.comp (Cofork.π (sigmaConstCokernelCofork R f)) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Limits.isColimitSigmaConstCokernelCofork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] : IsColimit (sigmaConstCokernelCofork R f)

The cokernel of the map ∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R induced by a map f : α → β identifies to the coproduct of copies of R indexed by the complement of the range of f.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.instHasCokernelMap'Id {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [HasCoproduct fun (x : α) => R] [HasCoproduct fun (x : β) => R] [HasCoproduct fun (x : ↑(Set.range f)ᶜ) => R] : HasCokernel (Sigma.map' f fun (x : α) => CategoryStruct.id R)

instance CategoryTheory.Limits.instHasCokernelMapObjFunctorTypeSigmaConst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (R : C) [HasCoproducts C] {α β : Type w} (f : α ⟶ β) : HasCokernel ((sigmaConst.obj R).map f)