Categories of indexed families of objects.

We define the pointwise category structure on indexed families of objects in a category (and also the dependent generalization).

instance CategoryTheory.pi {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] : Category.{max w₀ v₁, max u₁ w₀} ((i : I) → C i)

pi C gives the cartesian product of an indexed family of categories.

@[simp]

theorem CategoryTheory.Pi.id_apply {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : CategoryStruct.id X i = CategoryStruct.id (X i)

@[simp]

theorem CategoryTheory.Pi.comp_apply {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {X Y Z : (i : I) → C i} (f : X ⟶ Y) (g : Y ⟶ Z) (i : I) : CategoryStruct.comp f g i = CategoryStruct.comp (f i) (g i)

theorem CategoryTheory.Pi.ext {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} {f g : X ⟶ Y} (w : ∀ (i : I), f i = g i) : f = g

theorem CategoryTheory.Pi.ext_iff {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} {f g : X ⟶ Y} : f = g ↔ ∀ (i : I), f i = g i

def CategoryTheory.Pi.eval {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (i : I) : Functor ((i : I) → C i) (C i)

The evaluation functor at i : I, sending an I-indexed family of objects to the object over i.

@[simp]

theorem CategoryTheory.Pi.eval_map {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (i : I) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) : (eval C i).map α = α i

@[simp]

theorem CategoryTheory.Pi.eval_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (i : I) (f : (i : I) → C i) : (eval C i).obj f = f i

instance CategoryTheory.Pi.instCategoryComp {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (f : J → I) (j : J) : Category.{v₁, u₁} ((C ∘ f) j)

def CategoryTheory.Pi.comap {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) : Functor ((i : I) → C i) ((j : J) → C (h j))

Pull back an I-indexed family of objects to a J-indexed family, along a function J → I.

@[simp]

theorem CategoryTheory.Pi.comap_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (f : (i : I) → C i) (i : J) : (comap C h).obj f i = f (h i)

@[simp]

theorem CategoryTheory.Pi.comap_map {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) (i : J) : (comap C h).map α i = α (h i)

def CategoryTheory.Pi.comapId (I : Type w₀) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] : comap C id ≅ Functor.id ((i : I) → C i)

The natural isomorphism between pulling back a grading along the identity function, and the identity functor.

@[simp]

theorem CategoryTheory.Pi.comapId_hom_app (I : Type w₀) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : (comapId I C).hom.app X i = CategoryStruct.id X i

@[simp]

theorem CategoryTheory.Pi.comapId_inv_app (I : Type w₀) (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : (comapId I C).inv.app X i = CategoryStruct.id X i

def CategoryTheory.Pi.comapComp {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) : (comap C g).comp (comap (C ∘ g) f) ≅ comap C (g ∘ f)

The natural isomorphism comparing between pulling back along two successive functions, and pulling back along their composition

@[simp]

theorem CategoryTheory.Pi.comapComp_hom_app {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K) : (comapComp C f g).hom.app X b = CategoryStruct.id (X (g (f b)))

@[simp]

theorem CategoryTheory.Pi.comapComp_inv_app {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) (X : (i : I) → C i) (b : K) : (comapComp C f g).inv.app X b = CategoryStruct.id (X (g (f b)))

def CategoryTheory.Pi.comapEvalIsoEval {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) : (comap C h).comp (eval (C ∘ h) j) ≅ eval C (h j)

The natural isomorphism between pulling back then evaluating, and just evaluating.

@[simp]

theorem CategoryTheory.Pi.comapEvalIsoEval_inv_app {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) (X : (i : I) → C i) : (comapEvalIsoEval C h j).inv.app X = CategoryStruct.id (X (h j))

@[simp]

theorem CategoryTheory.Pi.comapEvalIsoEval_hom_app {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) (X : (i : I) → C i) : (comapEvalIsoEval C h j).hom.app X = CategoryStruct.id (X (h j))

instance CategoryTheory.Pi.sumElimCategory {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → Category.{v₁, u₁} (D j)] (s : I ⊕ J) : Category.{v₁, u₁} (Sum.elim C D s)

def CategoryTheory.Pi.sum {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → Category.{v₁, u₁} (D j)] : Functor ((i : I) → C i) (Functor ((j : J) → D j) ((s : I ⊕ J) → Sum.elim C D s))

The bifunctor combining an I-indexed family of objects with a J-indexed family of objects to obtain an I ⊕ J-indexed family of objects.

@[simp]

theorem CategoryTheory.Pi.sum_map_app {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → Category.{v₁, u₁} (D j)] {X X' : (i : I) → C i} (f : X ⟶ X') (Y : (j : J) → D j) (s : I ⊕ J) : ((sum C).map f).app Y s = match s with | Sum.inl i => f i | Sum.inr j => CategoryStruct.id (Y j)

@[simp]

theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I ⊕ J) : ((sum C).obj X).obj Y s = match s with | Sum.inl i => X i | Sum.inr j => Y j

@[simp]

theorem CategoryTheory.Pi.sum_obj_map {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → Category.{v₁, u₁} (D j)] (X : (i : I) → C i) {x✝ x✝¹ : (j : J) → D j} (f : x✝ ⟶ x✝¹) (s : I ⊕ J) : ((sum C).obj X).map f s = match s with | Sum.inl i => CategoryStruct.id (X i) | Sum.inr j => f j

def CategoryTheory.Pi.isoApp {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} (f : X ≅ Y) (i : I) : X i ≅ Y i

An isomorphism between I-indexed objects gives an isomorphism between each pair of corresponding components.

@[simp]

theorem CategoryTheory.Pi.isoApp_hom {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} (f : X ≅ Y) (i : I) : (isoApp f i).hom = f.hom i

@[simp]

theorem CategoryTheory.Pi.isoApp_inv {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} (f : X ≅ Y) (i : I) : (isoApp f i).inv = f.inv i

@[simp]

theorem CategoryTheory.Pi.isoApp_refl {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) : isoApp (Iso.refl X) i = Iso.refl (X i)

@[simp]

theorem CategoryTheory.Pi.isoApp_symm {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} (f : X ≅ Y) (i : I) : isoApp f.symm i = (isoApp f i).symm

@[simp]

theorem CategoryTheory.Pi.isoApp_trans {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y Z : (i : I) → C i} (f : X ≅ Y) (g : Y ≅ Z) (i : I) : isoApp (f ≪≫ g) i = isoApp f i ≪≫ isoApp g i

def CategoryTheory.Functor.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (F : (i : I) → Functor (C i) (D i)) : Functor ((i : I) → C i) ((i : I) → D i)

Assemble an I-indexed family of functors into a functor between the pi types.

@[simp]

theorem CategoryTheory.Functor.pi_map {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (F : (i : I) → Functor (C i) (D i)) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) (i : I) : (pi F).map α i = (F i).map (α i)

@[simp]

theorem CategoryTheory.Functor.pi_obj {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (F : (i : I) → Functor (C i) (D i)) (f : (i : I) → C i) (i : I) : (pi F).obj f i = (F i).obj (f i)

def CategoryTheory.Functor.pi' {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u₃} [Category.{v₃, u₃} A] (f : (i : I) → Functor A (C i)) : Functor A ((i : I) → C i)

Similar to pi, but all functors come from the same category A

@[simp]

theorem CategoryTheory.Functor.pi'_obj {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u₃} [Category.{v₃, u₃} A] (f : (i : I) → Functor A (C i)) (a : A) (i : I) : (pi' f).obj a i = (f i).obj a

@[simp]

theorem CategoryTheory.Functor.pi'_map {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u₃} [Category.{v₃, u₃} A] (f : (i : I) → Functor A (C i)) {X✝ Y✝ : A} (h : X✝ ⟶ Y✝) (i : I) : (pi' f).map h i = (f i).map h

def CategoryTheory.Functor.pi'CompEval {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u_1} [Category.{u_2, u_1} A] (F : (i : I) → Functor A (C i)) (i : I) : (pi' F).comp (Pi.eval C i) ≅ F i

The projections of Functor.pi' F are isomorphic to the functors of the family F

@[simp]

theorem CategoryTheory.Functor.pi'CompEval_hom_app {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u_1} [Category.{u_2, u_1} A] (F : (i : I) → Functor A (C i)) (i : I) (X : A) : (pi'CompEval F i).hom.app X = CategoryStruct.id ((F i).obj X)

@[simp]

theorem CategoryTheory.Functor.pi'CompEval_inv_app {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u_1} [Category.{u_2, u_1} A] (F : (i : I) → Functor A (C i)) (i : I) (X : A) : (pi'CompEval F i).inv.app X = CategoryStruct.id ((F i).obj X)

@[simp]

theorem CategoryTheory.Functor.eqToHom_proj {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {x x' : (i : I) → C i} (h : x = x') (i : I) : eqToHom h i = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.pi'_eval {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u₃} [Category.{v₃, u₃} A] (f : (i : I) → Functor A (C i)) (i : I) : (pi' f).comp (Pi.eval C i) = f i

theorem CategoryTheory.Functor.pi_ext {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {A : Type u₃} [Category.{v₃, u₃} A] (f f' : Functor A ((i : I) → C i)) (h : ∀ (i : I), f.comp (Pi.eval C i) = f'.comp (Pi.eval C i)) : f = f'

Two functors to a product category are equal iff they agree on every coordinate.

def CategoryTheory.NatTrans.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] {F G : (i : I) → Functor (C i) (D i)} (α : (i : I) → F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G

Assemble an I-indexed family of natural transformations into a single natural transformation.

@[simp]

theorem CategoryTheory.NatTrans.pi_app {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] {F G : (i : I) → Functor (C i) (D i)} (α : (i : I) → F i ⟶ G i) (f : (i : I) → C i) (i : I) : (pi α).app f i = (α i).app (f i)

def CategoryTheory.NatTrans.pi' {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {E : Type u_1} [Category.{u_2, u_1} E] {F G : Functor E ((i : I) → C i)} (τ : (i : I) → F.comp (Pi.eval C i) ⟶ G.comp (Pi.eval C i)) : F ⟶ G

Assemble an I-indexed family of natural transformations into a single natural transformation.

@[simp]

theorem CategoryTheory.NatTrans.pi'_app {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {E : Type u_1} [Category.{u_2, u_1} E] {F G : Functor E ((i : I) → C i)} (τ : (i : I) → F.comp (Pi.eval C i) ⟶ G.comp (Pi.eval C i)) (X : E) (i : I) : (pi' τ).app X i = (τ i).app X

def CategoryTheory.NatIso.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] {F G : (i : I) → Functor (C i) (D i)} (e : (i : I) → F i ≅ G i) : Functor.pi F ≅ Functor.pi G

Assemble an I-indexed family of natural isomorphisms into a single natural isomorphism.

@[simp]

theorem CategoryTheory.NatIso.pi_inv {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] {F G : (i : I) → Functor (C i) (D i)} (e : (i : I) → F i ≅ G i) : (pi e).inv = NatTrans.pi fun (i : I) => (e i).inv

@[simp]

theorem CategoryTheory.NatIso.pi_hom {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] {F G : (i : I) → Functor (C i) (D i)} (e : (i : I) → F i ≅ G i) : (pi e).hom = NatTrans.pi fun (i : I) => (e i).hom

def CategoryTheory.NatIso.pi' {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {E : Type u_1} [Category.{u_2, u_1} E] {F G : Functor E ((i : I) → C i)} (e : (i : I) → F.comp (Pi.eval C i) ≅ G.comp (Pi.eval C i)) : F ≅ G

Assemble an I-indexed family of natural isomorphisms into a single natural isomorphism.

@[simp]

theorem CategoryTheory.NatIso.pi'_hom {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {E : Type u_1} [Category.{u_2, u_1} E] {F G : Functor E ((i : I) → C i)} (e : (i : I) → F.comp (Pi.eval C i) ≅ G.comp (Pi.eval C i)) : (pi' e).hom = NatTrans.pi' fun (i : I) => (e i).hom

@[simp]

theorem CategoryTheory.NatIso.pi'_inv {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {E : Type u_1} [Category.{u_2, u_1} E] {F G : Functor E ((i : I) → C i)} (e : (i : I) → F.comp (Pi.eval C i) ≅ G.comp (Pi.eval C i)) : (pi' e).inv = NatTrans.pi' fun (i : I) => (e i).inv

theorem CategoryTheory.isIso_pi_iff {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i} (f : X ⟶ Y) : IsIso f ↔ ∀ (i : I), IsIso (f i)

def CategoryTheory.Pi.eqToEquivalence {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : C i ≌ C j

For a family of categories C i indexed by I, an equality i = j in I induces an equivalence C i ≌ C j.

def CategoryTheory.Pi.evalCompEqToEquivalenceFunctor {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (eval C i).comp (eqToEquivalence C h).functor ≅ eval C j

When i = j, projections Pi.eval C i and Pi.eval C j are related by the equivalence Pi.eqToEquivalence C h : C i ≌ C j.

@[simp]

theorem CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (evalCompEqToEquivalenceFunctor C h).hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv {I : Type w₀} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (evalCompEqToEquivalenceFunctor C h).inv = eqToHom ⋯

def CategoryTheory.Pi.eqToEquivalenceFunctorIso {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (eqToEquivalence C ⋯).functor ≅ (eqToEquivalence (fun (i' : J) => C (f i')) h).functor

The equivalences given by Pi.eqToEquivalence are compatible with reindexing.

@[simp]

theorem CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (eqToEquivalenceFunctorIso C f h).inv = eqToHom ⋯

@[simp]

theorem CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (eqToEquivalenceFunctorIso C f h).hom = eqToHom ⋯

noncomputable def CategoryTheory.Pi.equivalenceOfEquiv {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (e : J ≃ I) : ((j : J) → C (e j)) ≌ (i : I) → C i

Reindexing a family of categories gives equivalent Pi categories.

@[simp]

theorem CategoryTheory.Pi.equivalenceOfEquiv_counitIso {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (e : J ≃ I) : (equivalenceOfEquiv C e).counitIso = NatIso.pi' fun (i : I) => ((Functor.pi' fun (i' : J) => eval C (e i')).associator (eval (fun (j : J) => C (e j)) (e.symm i)) (eqToEquivalence C ⋯).functor).symm ≪≫ Functor.isoWhiskerRight (Functor.pi'CompEval (fun (i' : J) => eval C (e i')) (e.symm i)) (eqToEquivalence C ⋯).functor ≪≫ evalCompEqToEquivalenceFunctor C ⋯ ≪≫ (eval C i).leftUnitor.symm

@[simp]

theorem CategoryTheory.Pi.equivalenceOfEquiv_inverse {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (e : J ≃ I) : (equivalenceOfEquiv C e).inverse = Functor.pi' fun (i' : J) => eval C (e i')

@[simp]

theorem CategoryTheory.Pi.equivalenceOfEquiv_unitIso {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (e : J ≃ I) : (equivalenceOfEquiv C e).unitIso = NatIso.pi' fun (i' : J) => (eval (fun (i : J) => C (e i)) i').leftUnitor ≪≫ (evalCompEqToEquivalenceFunctor (fun (j : J) => C (e j)) ⋯).symm ≪≫ (eval (fun (j : J) => C (e j)) (e.symm (e i'))).isoWhiskerLeft (eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫ (Functor.pi'CompEval (eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp (eqToEquivalence C ⋯).functor).symm ≪≫ (Functor.pi' (eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp).isoWhiskerLeft (Functor.pi'CompEval (eval fun (i : Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i')) (eqToEquivalence C ⋯).functor).symm ≪≫ ((Functor.pi' (eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp).associator (Functor.pi' (eval fun (i : Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i'))) (eval (fun (i : Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i')) (eqToEquivalence C ⋯).functor)).symm

@[simp]

theorem CategoryTheory.Pi.equivalenceOfEquiv_functor {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → Category.{v₁, u₁} (C i)] (e : J ≃ I) : (equivalenceOfEquiv C e).functor = Functor.pi' fun (i : I) => (eval (fun (j : J) => C (e j)) (e.symm i)).comp (eqToEquivalence C ⋯).functor

def CategoryTheory.Pi.optionEquivalence {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → Category.{v₁, u₁} (C' i)] : ((i : Option J) → C' i) ≌ C' none × ((j : J) → C' (some j))

A product of categories indexed by Option J identifies to a binary product.

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_functor {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → Category.{v₁, u₁} (C' i)] : (optionEquivalence C').functor = (eval C' none).prod' (Functor.pi' fun (i : J) => eval C' (some i))

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_inverse {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → Category.{v₁, u₁} (C' i)] : (optionEquivalence C').inverse = Functor.pi' fun (i : Option J) => match i with | none => Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (Prod.snd (C' none) ((j : J) → C' (some j))).comp (eval (fun (j : J) => C' (some j)) i)

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_unitIso {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → Category.{v₁, u₁} (C' i)] : (optionEquivalence C').unitIso = NatIso.pi' fun (i : Option J) => match i with | none => Iso.refl ((Functor.id ((i : Option J) → C' i)).comp (eval C' none)) | some val => Iso.refl ((Functor.id ((i : Option J) → C' i)).comp (eval C' (some val)))

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_counitIso {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → Category.{v₁, u₁} (C' i)] : (optionEquivalence C').counitIso = Iso.refl ((Functor.pi' fun (i : Option J) => match i with | none => Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (Prod.snd (C' none) ((j : J) → C' (some j))).comp (eval (fun (j : J) => C' (some j)) i)).comp ((eval C' none).prod' (Functor.pi' fun (i : J) => eval C' (some i))))

def CategoryTheory.Equivalence.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : ((i : I) → C i) ≌ (i : I) → D i

Assemble an I-indexed family of equivalences of categories into a single equivalence.

@[simp]

theorem CategoryTheory.Equivalence.pi_inverse {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (pi E).inverse = Functor.pi fun (i : I) => (E i).inverse

@[simp]

theorem CategoryTheory.Equivalence.pi_functor {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (pi E).functor = Functor.pi fun (i : I) => (E i).functor

@[simp]

theorem CategoryTheory.Equivalence.pi_counitIso {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (pi E).counitIso = NatIso.pi fun (i : I) => (E i).counitIso

@[simp]

theorem CategoryTheory.Equivalence.pi_unitIso {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (pi E).unitIso = NatIso.pi fun (i : I) => (E i).unitIso

instance CategoryTheory.Equivalence.instIsEquivalenceForallPi {I : Type w₀} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] (F : (i : I) → Functor (C i) (D i)) [∀ (i : I), (F i).IsEquivalence] : (Functor.pi F).IsEquivalence