Functors out of sums of categories. #
This file records the universal property of sums of categories as an equivalence of
categories Sum.functorEquiv : A ⊕ A' ⥤ B ≌ (A ⥤ B) × (A' ⥤ B), and characterizes its
precompositions with the left and right inclusion as corresponding to the projections on
the product side.
def
CategoryTheory.Sum.functorEquiv
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
:
The equivalence between functors from a sum and the product of the functor categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_inverse_map
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
{X✝ Y✝ : Functor A B × Functor A' B}
(η : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_counitIso
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
:
(functorEquiv A A' B).counitIso = NatIso.ofComponents
(fun (F : Functor A B × Functor A' B) => (F.1.inlCompSum' F.2).prod (F.1.inrCompSum' F.2) ≪≫ prod.etaIso F) ⋯
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_functor_obj
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
(F : Functor (A ⊕ A') B)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_functor_map
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
{X✝ Y✝ : Functor (A ⊕ A') B}
(η : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_unitIso
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_inverse_obj
(A : Type u_1)
[Category.{u_3, u_1} A]
(A' : Type u_2)
[Category.{u_4, u_2} A']
(B : Type u)
[Category.{v, u} B]
(F : Functor A B × Functor A' B)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_unit_app_app_inl
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(a : A)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_unit_app_app_inr
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(a' : A')
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(a : A)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(a' : A')
:
def
CategoryTheory.Sum.functorEquivFunctorCompFstIso
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
:
Composing the forward direction of functorEquiv with the first projection is the same as
precomposition with inl_ A A'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.functorEquivFunctorCompFstIso_hom_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(X✝ : A)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquivFunctorCompFstIso_inv_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(X✝ : A)
:
def
CategoryTheory.Sum.functorEquivFunctorCompSndIso
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
:
Composing the forward direction of functorEquiv with the second projection is the same as
precomposition with inr_ A A'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.functorEquivFunctorCompSndIso_inv_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(X✝ : A')
:
@[simp]
theorem
CategoryTheory.Sum.functorEquivFunctorCompSndIso_hom_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
(X✝ : A')
:
def
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
:
Composing the backward direction of functorEquiv with precomposition with inl_ A A'.
is naturally isomorphic to the first projection.
Equations
- CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) => x.1.inlCompSum' x.2) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_inv_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor A B × Functor A' B)
(X✝ : A)
:
@[simp]
theorem
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_hom_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor A B × Functor A' B)
(X✝ : A)
:
def
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
:
Composing the backward direction of functorEquiv with the second projection is the same as
precomposition with inr_ A A'.
Equations
- CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) => x.1.inrCompSum' x.2) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_inv_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor A B × Functor A' B)
(X✝ : A')
:
@[simp]
theorem
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_hom_app_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor A B × Functor A' B)
(X✝ : A')
:
def
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G)
:
A consequence of functorEquiv: we can construct a natural transformation of functors
A ⊕ A' ⥤ B from the data of natural transformations of their whiskering with inl_ and inr_.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G)
(X : A ⊕ A')
:
(natTransOfWhiskerLeftInlInr η₁ η₂).app X = CategoryStruct.comp (((functorEquiv A A' B).unit.app F).app X)
(CategoryStruct.comp ((NatTrans.sum' η₁ η₂).app X) (((functorEquiv A A' B).unitInv.app G).app X))
@[simp]
theorem
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_id
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F : Functor (A ⊕ A') B}
:
natTransOfWhiskerLeftInlInr (CategoryStruct.id ((inl_ A A').comp F)) (CategoryStruct.id ((inr_ A A').comp F)) = CategoryStruct.id F
@[simp]
theorem
CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_comp
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G H : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G)
(ν₁ : (inl_ A A').comp G ⟶ (inl_ A A').comp H)
(ν₂ : (inr_ A A').comp G ⟶ (inr_ A A').comp H)
:
natTransOfWhiskerLeftInlInr (CategoryStruct.comp η₁ ν₁) (CategoryStruct.comp η₂ ν₂) = CategoryStruct.comp (natTransOfWhiskerLeftInlInr η₁ η₂) (natTransOfWhiskerLeftInlInr ν₁ ν₂)
def
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G)
:
A consequence of functorEquiv: we can construct a natural isomorphism of functors
A ⊕ A' ⥤ B from the data of natural isomorphisms of their whiskering with inl_ and inr_.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_hom
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G)
:
@[simp]
theorem
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_inv
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G)
:
theorem
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
{F G : Functor (A ⊕ A') B}
(η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G)
(η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G)
:
natIsoOfWhiskerLeftInlInr η₁ η₂ = (functorEquiv A A' B).unitIso.app F ≪≫ (functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫ (functorEquiv A A' B).unitIso.symm.app G
def
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
:
((equivalence A A').congrLeft.trans (functorEquiv A' A B)).functor ≅ ((functorEquiv A A' B).trans (Prod.braiding (Functor A B) (Functor A' B))).functor
functorEquiv A A' B transforms Swap.equivalence into Prod.braiding.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
:
(equivalenceFunctorEquivFunctorIso.hom.app X).2 = CategoryStruct.comp ((inr_ A' A).associator (swap A' A) X).inv (whiskerRight (swapCompInr A' A).hom X)
@[simp]
theorem
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
:
(equivalenceFunctorEquivFunctorIso.inv.app X).1 = CategoryStruct.comp (whiskerRight (swapCompInl A' A).inv X) ((inl_ A' A).associator (swap A' A) X).hom
@[simp]
theorem
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
:
(equivalenceFunctorEquivFunctorIso.hom.app X).1 = CategoryStruct.comp ((inl_ A' A).associator (swap A' A) X).inv (whiskerRight (swapCompInl A' A).hom X)
@[simp]
theorem
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd
{A : Type u_1}
[Category.{u_3, u_1} A]
{A' : Type u_2}
[Category.{u_4, u_2} A']
{B : Type u}
[Category.{v, u} B]
(X : Functor (A ⊕ A') B)
:
(equivalenceFunctorEquivFunctorIso.inv.app X).2 = CategoryStruct.comp (whiskerRight (swapCompInr A' A).inv X) ((inr_ A' A).associator (swap A' A) X).hom
def
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
:
((sum.associativity A A' T).congrLeft.trans
((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor ≅ (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
(prod.associativity (Functor A B) (Functor A' B) (Functor T B))).functor
The equivalence Sum.functorEquiv sends associativity of sums to associativity of products
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.2 = CategoryStruct.comp (whiskerLeft (inr_ A' T) ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv)
(CategoryStruct.comp ((inr_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).inv
(whiskerRight (sum.inrCompInrCompInverseAssociator A A' T).hom X))
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).1 = CategoryStruct.comp ((inl_ A A').associator (inl_ (A ⊕ A') T) X).inv
(CategoryStruct.comp (whiskerRight (sum.inlCompInverseAssociator A A' T).inv X)
((inl_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom)
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).1 = CategoryStruct.comp ((inl_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv
(CategoryStruct.comp (whiskerRight (sum.inlCompInverseAssociator A A' T).hom X)
((inl_ A A').associator (inl_ (A ⊕ A') T) X).hom)
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.1 = CategoryStruct.comp (whiskerLeft (inl_ A' T) ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv)
(CategoryStruct.comp ((inl_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).inv
(CategoryStruct.comp (whiskerRight (sum.inlCompInrCompInverseAssociator A A' T).hom X)
((inr_ A A').associator (inl_ (A ⊕ A') T) X).hom))
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.1 = CategoryStruct.comp ((inr_ A A').associator (inl_ (A ⊕ A') T) X).inv
(CategoryStruct.comp (whiskerRight (sum.inlCompInrCompInverseAssociator A A' T).inv X)
(CategoryStruct.comp ((inl_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).hom
(whiskerLeft (inl_ A' T) ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom)))
@[simp]
theorem
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd
{A : Type u_1}
[Category.{u_4, u_1} A]
{A' : Type u_2}
[Category.{u_5, u_2} A']
{B : Type u}
[Category.{v, u} B]
(T : Type u_3)
[Category.{u_6, u_3} T]
(X : Functor ((A ⊕ A') ⊕ T) B)
:
((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.2 = CategoryStruct.comp (whiskerRight (sum.inrCompInrCompInverseAssociator A A' T).inv X)
(CategoryStruct.comp ((inr_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).hom
(whiskerLeft (inr_ A' T) ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom))