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) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Category.{max w₀ v₁, max u₁ w₀} ((i : I) → C i)

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

Equations

• CategoryTheory.pi C = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[reducible, inline]

instance CategoryTheory.pi' {I : Type v₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Category.{v₁, max u₁ v₁} ((i : I) → C 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

• CategoryTheory.pi' C = CategoryTheory.pi C

@[simp]

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

@[simp]

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

theorem CategoryTheory.Pi.ext {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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

def CategoryTheory.Pi.eval {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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

• CategoryTheory.Pi.eval C i = { obj := fun (f : (i : I) → C i) => f i, map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) => α i, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Pi.instCategoryComp C f = id inferInstance

def CategoryTheory.Pi.comap {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) : 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

• CategoryTheory.Pi.comap C h = { 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 := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.Pi.comapId (I : Type w₀) (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Pi.comap C id ≅ 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.

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Pi.sumElimCategory C (Sum.inl i) = id inferInstance
• CategoryTheory.Pi.sumElimCategory C (Sum.inr j) = id inferInstance

def CategoryTheory.Pi.sum {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D 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.

@[simp]

theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.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) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) : ∀ {x x_1 : (j : J) → D j} (f : x ⟶ x_1) (s : I ⊕ J), ((CategoryTheory.Pi.sum C).obj X).map f s = match s with | Sum.inl i => CategoryTheory.CategoryStruct.id (X i) | Sum.inr j => f j

@[simp]

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

def CategoryTheory.Pi.isoApp {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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

• CategoryTheory.Pi.isoApp f i = { hom := f.hom i, inv := f.inv i, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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

• CategoryTheory.Functor.pi F = { obj := fun (f : (i : I) → C i) (i : I) => (F i).obj (f i), map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : I) => (F i).map (α i), map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.pi' {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (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

• CategoryTheory.Functor.pi' f = { 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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Functor.pi'CompEval F i = CategoryTheory.Iso.refl ((CategoryTheory.Functor.pi' F).comp (CategoryTheory.Pi.eval C i))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Functor.pi_ext {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (f : CategoryTheory.Functor A ((i : I) → C i)) (f' : CategoryTheory.Functor A ((i : I) → C i)) (h : ∀ (i : I), f.comp (CategoryTheory.Pi.eval C i) = f'.comp (CategoryTheory.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) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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) : CategoryTheory.Functor.pi F ⟶ CategoryTheory.Functor.pi G

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

Equations

• CategoryTheory.NatTrans.pi α = { app := fun (f : (i : I) → C i) (i : I) => (α i).app (f i), naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.pi_app {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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) : (CategoryTheory.NatTrans.pi α).app f i = (α i).app (f i)

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

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

Equations

• CategoryTheory.NatTrans.pi' τ = { app := fun (X : E) (i : I) => (τ i).app X, naturality := ⋯ }

@[simp]

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

def CategoryTheory.NatIso.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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) : CategoryTheory.Functor.pi F ≅ CategoryTheory.Functor.pi G

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

Equations

• CategoryTheory.NatIso.pi e = { hom := CategoryTheory.NatTrans.pi fun (i : I) => (e i).hom, inv := CategoryTheory.NatTrans.pi fun (i : I) => (e i).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.NatIso.pi_hom {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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) : (CategoryTheory.NatIso.pi e).hom = CategoryTheory.NatTrans.pi fun (i : I) => (e i).hom

@[simp]

theorem CategoryTheory.NatIso.pi_inv {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D 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) : (CategoryTheory.NatIso.pi e).inv = CategoryTheory.NatTrans.pi fun (i : I) => (e i).inv

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

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

Equations

• CategoryTheory.NatIso.pi' e = { hom := CategoryTheory.NatTrans.pi' fun (i : I) => (e i).hom, inv := CategoryTheory.NatTrans.pi' fun (i : I) => (e i).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

def CategoryTheory.Pi.eqToEquivalence {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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

• CategoryTheory.Pi.eqToEquivalence C h = h ▸ CategoryTheory.Equivalence.refl

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

Equations

• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h = CategoryTheory.eqToIso ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h = CategoryTheory.eqToIso ⋯

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Pi.equivalenceOfEquiv {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pi.equivalenceOfEquiv_unitIso {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).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'))) (CategoryTheory.Pi.eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫ (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun (j : J) => C (e j)) (e.symm (e i'))).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).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')) (CategoryTheory.Pi.eqToEquivalence C ⋯).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')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor)).symm

def CategoryTheory.Pi.optionEquivalence {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_inverse {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)] : (CategoryTheory.Pi.optionEquivalence C').inverse = CategoryTheory.Functor.pi' fun (i : Option J) => 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)

@[simp]

theorem CategoryTheory.Pi.optionEquivalence_counitIso {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)] : (CategoryTheory.Pi.optionEquivalence C').counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.pi' fun (i : Option J) => 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 C' (some i))))

@[simp]

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

@[simp]

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

def CategoryTheory.Equivalence.pi {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯