Documentation

Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

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.

source
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)
source
@[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.
Instances For
    source
    @[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
    source
    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⟩
    source
    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
    source
    @[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
    source
    @[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
    source
    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.
    Instances For
      source
      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)
      source
      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)
      source
      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 isomorphism sigmaConst.obj X ⋙ F ≅ sigmaConst.obj (F.obj X) when F preserves coproducts.

      Equations
      Instances For
        source
        @[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
        source
        @[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
        source
        @[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)
        source
        @[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