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)

@[implicit_reducible]

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)

noncomputable def CategoryTheory.Limits.sigmaConstObjCompIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasCoproducts C] [HasCoproducts D] (F : Functor C D) [∀ (T : Type w), PreservesColimitsOfShape (Discrete T) F] (X : C) : (sigmaConst.obj X).comp F ≅ sigmaConst.obj (F.obj X)

The isomophism sigmaConst.obj X ⋙ F ≅ sigmaConst.obj (F.obj X) when F preserves coproducts.

Equations

• CategoryTheory.Limits.sigmaConstObjCompIso F X = CategoryTheory.NatIso.ofComponents (fun (x : Type ?u.5) => CategoryTheory.Limits.PreservesCoproduct.iso F fun (x : x) => X) ⋯

@[simp]

theorem CategoryTheory.Limits.map_ι_sigmaConstObjCompIso_hom_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasCoproducts C] [HasCoproducts D] (F : Functor C D) [∀ (T : Type w), PreservesColimitsOfShape (Discrete T) F] (X : C) {T : Type w} (t : T) : CategoryStruct.comp (F.map (Sigma.ι (fun (x : T) => X) t)) ((sigmaConstObjCompIso F X).hom.app T) = Sigma.ι (fun (x : T) => F.obj X) t

@[simp]

theorem CategoryTheory.Limits.map_ι_sigmaConstObjCompIso_hom_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasCoproducts C] [HasCoproducts D] (F : Functor C D) [∀ (T : Type w), PreservesColimitsOfShape (Discrete T) F] (X : C) {T : Type w} (t : T) {Z : D} (h : (∐ fun (x : T) => F.obj X) ⟶ Z) : CategoryStruct.comp (F.map (Sigma.ι (fun (x : T) => X) t)) (CategoryStruct.comp ((sigmaConstObjCompIso F X).hom.app T) h) = CategoryStruct.comp (Sigma.ι (fun (x : T) => F.obj X) t) h

@[simp]

theorem CategoryTheory.Limits.ι_sigmaConstObjCompIso_inv_app {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasCoproducts C] [HasCoproducts D] (F : Functor C D) [∀ (T : Type w), PreservesColimitsOfShape (Discrete T) F] (X : C) {T : Type w} (t : T) : CategoryStruct.comp (Sigma.ι (fun (x : T) => F.obj X) t) ((sigmaConstObjCompIso F X).inv.app T) = F.map (Sigma.ι (fun (x : T) => X) t)

@[simp]

theorem CategoryTheory.Limits.ι_sigmaConstObjCompIso_inv_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasCoproducts C] [HasCoproducts D] (F : Functor C D) [∀ (T : Type w), PreservesColimitsOfShape (Discrete T) F] (X : C) {T : Type w} (t : T) {Z : D} (h : F.obj ((sigmaConst.obj X).obj T) ⟶ Z) : CategoryStruct.comp (Sigma.ι (fun (x : T) => F.obj X) t) (CategoryStruct.comp ((sigmaConstObjCompIso F X).inv.app T) h) = CategoryStruct.comp (F.map (Sigma.ι (fun (x : T) => X) t)) h