# 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).

source
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.

Equations

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

source
@[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)
source
@[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)
source
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
source
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
source
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`.

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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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)
Equations

- CategoryTheory.Pi.instCategoryComp C f = inferInstanceAs ((j : J) → CategoryTheory.Category.{?u.39, ?u.38} (C (f j)))

source
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`.

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 := ⋯ }

Instances For

source
@[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)
source
@[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)
source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
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

Equations

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

Instances For

source
@[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)))
source
@[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)))
source
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.

Equations

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

Instances For

source
@[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))
source
@[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))
source
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)
Equations

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

source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
@[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)
source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
@[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)
source
@[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
source
@[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
source
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.

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 := ⋯ }

Instances For

source
@[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)
source
@[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)
source
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`

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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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`

Equations

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

Instances For

source
@[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)
source
@[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)
source
@[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 ⋯
source
@[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
source
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.

source
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.

Equations

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

Instances For

source
@[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)
source
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.

Equations

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

Instances For

source
@[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
source
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.

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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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.

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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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)
source
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`.

Equations

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

Instances For

source
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`.

Equations

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

Instances For

source
@[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 ⋯
source
@[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 ⋯
source
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.

Equations

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

Instances For

source
@[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 ⋯
source
@[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 ⋯
source
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.

Equations

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

Instances For

source
@[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')
source
@[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
source
@[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
source
@[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
source
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.

Equations

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

Instances For

source
@[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)))
source
@[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)
source
@[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))
source
@[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))))
source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
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