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 : IType u₁) [(i : I) → ] :

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

Equations
@[reducible, inline]
instance CategoryTheory.pi' {I : Type v₁} (C : IType u₁) [(i : I) → ] :

This provides some assistance to typeclass search in a common situation, which otherwise fails. (Without this CategoryTheory.Pi.has_limit_of_has_limit_comp_eval fails.)

Equations
@[simp]
theorem CategoryTheory.Pi.id_apply {I : Type w₀} (C : IType u₁) [(i : I) → ] (X : (i : I) → C i) (i : I) :
@[simp]
theorem CategoryTheory.Pi.comp_apply {I : Type w₀} (C : IType u₁) [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} {Z : (i : I) → C i} (f : X Y) (g : Y Z) (i : I) :
theorem CategoryTheory.Pi.ext {I : Type w₀} (C : IType u₁) [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} {f : X Y} {g : X Y} (w : ∀ (i : I), f i = g i) :
f = g
@[simp]
theorem CategoryTheory.Pi.eval_map {I : Type w₀} (C : IType u₁) [(i : I) → ] (i : I) :
∀ {X Y : (i : I) → C i} (α : X Y), ().map α = α i
@[simp]
theorem CategoryTheory.Pi.eval_obj {I : Type w₀} (C : IType u₁) [(i : I) → ] (i : I) (f : (i : I) → C i) :
().obj f = f i
def CategoryTheory.Pi.eval {I : Type w₀} (C : IType u₁) [(i : I) → ] (i : I) :
CategoryTheory.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.

Equations
• = { obj := fun (f : (i : I) → C i) => f i, map := fun {X Y : (i : I) → C i} (α : X Y) => α i, map_id := , map_comp := }
Instances For
instance CategoryTheory.Pi.instCategoryComp {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (f : JI) (j : J) :
Equations
• = id inferInstance
@[simp]
theorem CategoryTheory.Pi.comap_map {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) :
∀ {X Y : (i : I) → C i} (α : X Y) (i : J), ().map α i = α (h i)
@[simp]
theorem CategoryTheory.Pi.comap_obj {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (f : (i : I) → C i) (i : J) :
().obj f i = f (h i)
def CategoryTheory.Pi.comap {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) :
CategoryTheory.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.

Equations
• = { obj := fun (f : (i : I) → C i) (i : J) => f (h i), map := fun {X Y : (i : I) → C i} (α : X Y) (i : J) => α (h i), map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Pi.comapId_inv_app (I : Type w₀) (C : IType u₁) [(i : I) → ] (X : (i : I) → C i) (i : I) :
.inv.app X i =
@[simp]
theorem CategoryTheory.Pi.comapId_hom_app (I : Type w₀) (C : IType u₁) [(i : I) → ] (X : (i : I) → C i) (i : I) :
.hom.app X i =
def CategoryTheory.Pi.comapId (I : Type w₀) (C : IType u₁) [(i : I) → ] :
CategoryTheory.Functor.id ((i : I) → C i)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pi.comapComp_hom_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (X : (i : I) → C i) (b : K) :
().hom.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
@[simp]
theorem CategoryTheory.Pi.comapComp_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (X : (i : I) → C i) (b : K) :
().inv.app X b = CategoryTheory.CategoryStruct.id (X (g (f b)))
def CategoryTheory.Pi.comapComp {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pi.comapEvalIsoEval_hom_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
.hom.app X = CategoryTheory.CategoryStruct.id (X (h j))
@[simp]
theorem CategoryTheory.Pi.comapEvalIsoEval_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
.inv.app X = CategoryTheory.CategoryStruct.id (X (h j))
def CategoryTheory.Pi.comapEvalIsoEval {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₁} (h : JI) (j : J) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Pi.sumElimCategory {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (s : I J) :
Equations
• = match x with | => id inferInstance | => id inferInstance
@[simp]
theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I J) :
(.obj X).obj Y s = match s with | => X i | => Y j
@[simp]
theorem CategoryTheory.Pi.sum_map_app {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] {X : (i : I) → C i} {X' : (i : I) → C i} (f : X X') (Y : (j : J) → D j) (s : I J) :
(.map f).app Y s = match s with | => f i | =>
@[simp]
theorem CategoryTheory.Pi.sum_obj_map {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] (X : (i : I) → C i) {Y : (j : J) → D j} {Y' : (j : J) → D j} (f : Y Y') (s : I J) :
(.obj X).map f s = match s with | => | => f j
def CategoryTheory.Pi.sum {I : Type w₀} (C : IType u₁) [(i : I) → ] {J : Type w₀} {D : JType u₁} [(j : J) → ] :
CategoryTheory.Functor ((i : I) → C i) (CategoryTheory.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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pi.isoApp_inv {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : I) :
().inv = f.inv i
@[simp]
theorem CategoryTheory.Pi.isoApp_hom {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : I) :
().hom = f.hom i
def CategoryTheory.Pi.isoApp {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {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.

Equations
• = { hom := f.hom i, inv := f.inv i, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Pi.isoApp_refl {I : Type w₀} {C : IType u₁} [(i : I) → ] (X : (i : I) → C i) (i : I) :
@[simp]
theorem CategoryTheory.Pi.isoApp_symm {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : I) :
CategoryTheory.Pi.isoApp f.symm i = ().symm
@[simp]
theorem CategoryTheory.Pi.isoApp_trans {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} {Z : (i : I) → C i} (f : X Y) (g : Y Z) (i : I) :
@[simp]
theorem CategoryTheory.Functor.pi_obj {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) (f : (i : I) → C i) (i : I) :
.obj f i = (F i).obj (f i)
@[simp]
theorem CategoryTheory.Functor.pi_map {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) :
∀ {X Y : (i : I) → C i} (α : X Y) (i : I), .map α i = (F i).map (α i)
def CategoryTheory.Functor.pi {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) :
CategoryTheory.Functor ((i : I) → C i) ((i : I) → D i)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.pi'_obj {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₃} [] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I) :
.obj a i = (f i).obj a
@[simp]
theorem CategoryTheory.Functor.pi'_map {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₃} [] (f : (i : I) → CategoryTheory.Functor A (C i)) :
∀ {X Y : A} (h : X Y) (i : I), .map h i = (f i).map h
def CategoryTheory.Functor.pi' {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₃} [] (f : (i : I) → CategoryTheory.Functor A (C i)) :
CategoryTheory.Functor A ((i : I) → C i)

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

Equations
• = { obj := fun (a : A) (i : I) => (f i).obj a, map := fun {X Y : A} (h : X Y) (i : I) => (f i).map h, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Functor.pi'CompEval_hom_app {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u_1} [] (F : (i : I) → CategoryTheory.Functor A (C i)) (i : I) (X : A) :
.hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
@[simp]
theorem CategoryTheory.Functor.pi'CompEval_inv_app {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u_1} [] (F : (i : I) → CategoryTheory.Functor A (C i)) (i : I) (X : A) :
.inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
def CategoryTheory.Functor.pi'CompEval {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u_1} [] (F : (i : I) → CategoryTheory.Functor A (C i)) (i : I) :
.comp () F i

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.eqToHom_proj {I : Type w₀} {C : IType u₁} [(i : I) → ] {x : (i : I) → C i} {x' : (i : I) → C i} (h : x = x') (i : I) :
@[simp]
theorem CategoryTheory.Functor.pi'_eval {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₃} [] (f : (i : I) → CategoryTheory.Functor A (C i)) (i : I) :
.comp () = f i
theorem CategoryTheory.Functor.pi_ext {I : Type w₀} {C : IType u₁} [(i : I) → ] {A : Type u₃} [] (f : CategoryTheory.Functor A ((i : I) → C i)) (f' : CategoryTheory.Functor A ((i : I) → C i)) (h : ∀ (i : I), f.comp () = f'.comp ()) :
f = f'

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

@[simp]
theorem CategoryTheory.NatTrans.pi_app {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (α : (i : I) → F i G i) (f : (i : I) → C i) (i : I) :
.app f i = (α i).app (f i)
def CategoryTheory.NatTrans.pi {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (α : (i : I) → F i G i) :

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

Equations
• = { app := fun (f : (i : I) → C i) (i : I) => (α i).app (f i), naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.pi'_app {I : Type w₀} {C : IType u₁} [(i : I) → ] {E : Type u_1} [] {F : CategoryTheory.Functor E ((i : I) → C i)} {G : CategoryTheory.Functor E ((i : I) → C i)} (τ : (i : I) → F.comp () G.comp ()) (X : E) (i : I) :
.app X i = (τ i).app X
def CategoryTheory.NatTrans.pi' {I : Type w₀} {C : IType u₁} [(i : I) → ] {E : Type u_1} [] {F : CategoryTheory.Functor E ((i : I) → C i)} {G : CategoryTheory.Functor E ((i : I) → C i)} (τ : (i : I) → F.comp () G.comp ()) :
F G

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

Equations
• = { app := fun (X : E) (i : I) => (τ i).app X, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatIso.pi_hom {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (e : (i : I) → F i G i) :
.hom = CategoryTheory.NatTrans.pi fun (i : I) => (e i).hom
@[simp]
theorem CategoryTheory.NatIso.pi_inv {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (e : (i : I) → F i G i) :
.inv = CategoryTheory.NatTrans.pi fun (i : I) => (e i).inv
def CategoryTheory.NatIso.pi {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (e : (i : I) → F i G i) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.NatIso.pi'_inv {I : Type w₀} {C : IType u₁} [(i : I) → ] {E : Type u_1} [] {F : CategoryTheory.Functor E ((i : I) → C i)} {G : CategoryTheory.Functor E ((i : I) → C i)} (e : (i : I) → F.comp () G.comp ()) :
.inv = CategoryTheory.NatTrans.pi' fun (i : I) => (e i).inv
@[simp]
theorem CategoryTheory.NatIso.pi'_hom {I : Type w₀} {C : IType u₁} [(i : I) → ] {E : Type u_1} [] {F : CategoryTheory.Functor E ((i : I) → C i)} {G : CategoryTheory.Functor E ((i : I) → C i)} (e : (i : I) → F.comp () G.comp ()) :
.hom = CategoryTheory.NatTrans.pi' fun (i : I) => (e i).hom
def CategoryTheory.NatIso.pi' {I : Type w₀} {C : IType u₁} [(i : I) → ] {E : Type u_1} [] {F : CategoryTheory.Functor E ((i : I) → C i)} {G : CategoryTheory.Functor E ((i : I) → C i)} (e : (i : I) → F.comp () G.comp ()) :
F G

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.isIso_pi_iff {I : Type w₀} {C : IType u₁} [(i : I) → ] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) :
∀ (i : I), CategoryTheory.IsIso (f i)
def CategoryTheory.Pi.eqToEquivalence {I : Type w₀} (C : IType u₁) [(i : I) → ] {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.

Equations
• = hCategoryTheory.Equivalence.refl
Instances For
@[simp]
theorem CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom {I : Type w₀} (C : IType u₁) [(i : I) → ] {i : I} {j : I} (h : i = j) :
@[simp]
theorem CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv {I : Type w₀} (C : IType u₁) [(i : I) → ] {i : I} {j : I} (h : i = j) :
def CategoryTheory.Pi.evalCompEqToEquivalenceFunctor {I : Type w₀} (C : IType u₁) [(i : I) → ] {i : I} {j : I} (h : i = j) :
().comp .functor

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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (f : JI) {i' : J} {j' : J} (h : i' = j') :
@[simp]
theorem CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (f : JI) {i' : J} {j' : J} (h : i' = j') :
def CategoryTheory.Pi.eqToEquivalenceFunctorIso {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (f : JI) {i' : J} {j' : J} (h : i' = j') :
.functor (CategoryTheory.Pi.eqToEquivalence (fun (i' : J) => C (f i')) h).functor

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Pi.equivalenceOfEquiv_counitIso {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (e : J I) :
.counitIso = CategoryTheory.NatIso.pi' fun (i : I) => ((CategoryTheory.Functor.pi' fun (i' : J) => CategoryTheory.Pi.eval (fun (i : I) => C i) (e i')).associator (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm i)) .functor).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.Functor.pi'CompEval (fun (i' : J) => CategoryTheory.Pi.eval (fun (i : I) => C i) (e i')) (e.symm i)) .functor ≪≫ ≪≫ ().leftUnitor.symm
@[simp]
theorem CategoryTheory.Pi.equivalenceOfEquiv_unitIso {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (e : J I) :
.unitIso = CategoryTheory.NatIso.pi' fun (i' : J) => (CategoryTheory.Pi.eval (fun (i : J) => C (e i)) i').leftUnitor ≪≫ (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor (fun (j : J) => C (e j)) ).symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm (e i'))) .symm ≪≫ (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp .functor).symm ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp) (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval fun (i : CategoryTheory.Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i')) .functor).symm ≪≫ ((CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp).associator (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval fun (i : CategoryTheory.Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i'))) (CategoryTheory.Pi.eval (fun (i : CategoryTheory.Functor (C (e (e.symm (e i')))) (C (e i'))) => C (e i')) .functor)).symm
@[simp]
theorem CategoryTheory.Pi.equivalenceOfEquiv_functor {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (e : J I) :
.functor = CategoryTheory.Functor.pi' fun (i : I) => (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm i)).comp .functor
@[simp]
theorem CategoryTheory.Pi.equivalenceOfEquiv_inverse {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (e : J I) :
.inverse = CategoryTheory.Functor.pi' fun (i' : J) => CategoryTheory.Pi.eval (fun (i : I) => C i) (e i')
noncomputable def CategoryTheory.Pi.equivalenceOfEquiv {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → ] (e : J I) :
((j : J) → C (e j)) (i : I) → C i

Reindexing a family of categories gives equivalent Pi categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pi.optionEquivalence_counitIso {J : Type w₁} (C' : Type u₁) [(i : ) → ] :
.counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.pi' fun (i : ) => match i with | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp (CategoryTheory.Pi.eval (fun (j : J) => C' (some j)) i)).comp ((CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun (i : J) => CategoryTheory.Pi.eval (fun (i : ) => C' i) (some i))))
@[simp]
theorem CategoryTheory.Pi.optionEquivalence_functor {J : Type w₁} (C' : Type u₁) [(i : ) → ] :
.functor = (CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun (i : J) => CategoryTheory.Pi.eval (fun (i : ) => C' i) (some i))
@[simp]
theorem CategoryTheory.Pi.optionEquivalence_unitIso {J : Type w₁} (C' : Type u₁) [(i : ) → ] :
.unitIso = CategoryTheory.NatIso.pi' fun (i : ) => match i with | none => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id ((i : ) → C' i)).comp (CategoryTheory.Pi.eval (fun (i : ) => C' i) none)) | some i => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id ((i : ) → C' i)).comp (CategoryTheory.Pi.eval (fun (i : ) => C' i) (some i)))
@[simp]
theorem CategoryTheory.Pi.optionEquivalence_inverse {J : Type w₁} (C' : Type u₁) [(i : ) → ] :
.inverse = CategoryTheory.Functor.pi' fun (i : ) => match i with | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j)) | some i => (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp (CategoryTheory.Pi.eval (fun (j : J) => C' (some j)) i)
def CategoryTheory.Pi.optionEquivalence {J : Type w₁} (C' : Type u₁) [(i : ) → ] :
((i : ) → C' i) C' none × ((j : J) → C' (some j))

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.pi_counitIso {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (E : (i : I) → C i D i) :
.counitIso = CategoryTheory.NatIso.pi fun (i : I) => (E i).counitIso
@[simp]
theorem CategoryTheory.Equivalence.pi_functor {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (E : (i : I) → C i D i) :
.functor = CategoryTheory.Functor.pi fun (i : I) => (E i).functor
@[simp]
theorem CategoryTheory.Equivalence.pi_inverse {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (E : (i : I) → C i D i) :
.inverse = CategoryTheory.Functor.pi fun (i : I) => (E i).inverse
@[simp]
theorem CategoryTheory.Equivalence.pi_unitIso {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (E : (i : I) → C i D i) :
.unitIso = CategoryTheory.NatIso.pi fun (i : I) => (E i).unitIso
def CategoryTheory.Equivalence.pi {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Equivalence.instIsEquivalenceForallPi {I : Type w₀} {C : IType u₁} [(i : I) → ] {D : IType u₂} [(i : I) → ] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) [∀ (i : I), (F i).IsEquivalence] :
.IsEquivalence
Equations
• =