Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

(Co)products in functor categories #

Given f : α → D ⥤ C, we prove the isomorphisms (∏ᶜ f).obj d ≅ ∏ᶜ (fun s => (f s).obj d) and (∐ f).obj d ≅ ∐ (fun s => (f s).obj d).

noncomputable def CategoryTheory.Limits.piObjIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasLimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) :
(∏ᶜ f).obj d ∏ᶜ fun (s : α) => (f s).obj d

Evaluating a product of functors amounts to taking the product of the evaluations.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Limits.piObjIso_hom_comp_π {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasLimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) :
    CategoryStruct.comp (piObjIso f d).hom (Pi.π (fun (s : α) => (f s).obj d) s) = (Pi.π f s).app d
    @[simp]
    theorem CategoryTheory.Limits.piObjIso_hom_comp_π_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasLimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) {Z : C} (h : (f s).obj d Z) :
    CategoryStruct.comp (piObjIso f d).hom (CategoryStruct.comp (Pi.π (fun (s : α) => (f s).obj d) s) h) = CategoryStruct.comp ((Pi.π f s).app d) h
    @[simp]
    theorem CategoryTheory.Limits.piObjIso_inv_comp_pi {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasLimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) :
    CategoryStruct.comp (piObjIso f d).inv ((Pi.π f s).app d) = Pi.π (fun (s : α) => (f s).obj d) s
    @[simp]
    theorem CategoryTheory.Limits.piObjIso_inv_comp_pi_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasLimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) {Z : C} (h : (f s).obj d Z) :
    CategoryStruct.comp (piObjIso f d).inv (CategoryStruct.comp ((Pi.π f s).app d) h) = CategoryStruct.comp (Pi.π (fun (s : α) => (f s).obj d) s) h
    noncomputable def CategoryTheory.Limits.sigmaObjIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasColimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) :
    ( f).obj d fun (s : α) => (f s).obj d

    Evaluating a coproduct of functors amounts to taking the coproduct of the evaluations.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.Limits.ι_comp_sigmaObjIso_hom {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasColimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) :
      CategoryStruct.comp ((Sigma.ι f s).app d) (sigmaObjIso f d).hom = Sigma.ι (fun (s : α) => (f s).obj d) s
      @[simp]
      theorem CategoryTheory.Limits.ι_comp_sigmaObjIso_hom_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasColimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) {Z : C} (h : ( fun (s : α) => (f s).obj d) Z) :
      @[simp]
      theorem CategoryTheory.Limits.ι_comp_sigmaObjIso_inv {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasColimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) :
      CategoryStruct.comp (Sigma.ι (fun (s : α) => (f s).obj d) s) (sigmaObjIso f d).inv = (Sigma.ι f s).app d
      @[simp]
      theorem CategoryTheory.Limits.ι_comp_sigmaObjIso_inv_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {α : Type w} [HasColimitsOfShape (Discrete α) C] (f : αFunctor D C) (d : D) (s : α) {Z : C} (h : ( f).obj d Z) :