(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)
:
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 : α)
:
@[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 : α)
:
@[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)
:
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)
:
CategoryStruct.comp ((Sigma.ι f s).app d) (CategoryStruct.comp (sigmaObjIso f d).hom h) = CategoryStruct.comp (Sigma.ι (fun (s : α) => (f s).obj d) s) h
@[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)
:
CategoryStruct.comp (Sigma.ι (fun (s : α) => (f s).obj d) s) (CategoryStruct.comp (sigmaObjIso f d).inv h) = CategoryStruct.comp ((Sigma.ι f s).app d) h