doc-next-gen

Mathlib.CategoryTheory.Pi.Basic

Module docstring

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

"}

CategoryTheory.pi instance
: Category.{max w₀ v₁} (∀ i, C i)
Full source 
/-- `pi C` gives the cartesian product of an indexed family of categories.
-/
instance pi : Category.{max w₀ v₁} (∀ i, C i) where
  Hom X Y := ∀ i, X i ⟶ Y i
  id X i := 𝟙 (X i)
  comp f g i := f i ≫ g i
Product Category of Indexed Family of Categories
Informal description
For any family of categories $\{C_i\}_{i \in I}$, the product category $\prod_{i \in I} C_i$ is a category where objects are tuples $(X_i)_{i \in I}$ with $X_i \in C_i$, and morphisms are tuples $(f_i)_{i \in I}$ with $f_i \colon X_i \to Y_i$ in $C_i$. Composition and identities are defined componentwise.
CategoryTheory.Pi.id_apply theorem
(X : ∀ i, C i) (i) : (𝟙 X : ∀ i, X i ⟶ X i) i = 𝟙 (X i)
Full source 
@[simp]
theorem id_apply (X : ∀ i, C i) (i) : (𝟙 X : ∀ i, X i ⟶ X i) i = 𝟙 (X i) :=
  rfl
Componentwise Identity in Product Category
Informal description
For any family of objects $\{X_i\}_{i \in I}$ in a product category $\prod_{i \in I} C_i$, the identity morphism $\mathbf{1}_X$ on the object $X = (X_i)_{i \in I}$ satisfies $(\mathbf{1}_X)_i = \mathbf{1}_{X_i}$ for each index $i \in I$.
CategoryTheory.Pi.comp_apply theorem
{X Y Z : ∀ i, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (i) : (f ≫ g : ∀ i, X i ⟶ Z i) i = f i ≫ g i
Full source 
@[simp]
theorem comp_apply {X Y Z : ∀ i, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (i) :
    (f ≫ g : ∀ i, X i ⟶ Z i) i = f i ≫ g i :=
  rfl
Componentwise Composition in Product Category
Informal description
For any objects $X, Y, Z$ in the product category $\prod_{i \in I} C_i$ and morphisms $f \colon X \to Y$, $g \colon Y \to Z$, the $i$-th component of the composition $f \circ g$ is equal to the composition of the $i$-th components of $f$ and $g$, i.e., $(f \circ g)_i = f_i \circ g_i$.
CategoryTheory.Pi.ext theorem
{X Y : ∀ i, C i} {f g : X ⟶ Y} (w : ∀ i, f i = g i) : f = g
Full source 
@[ext]
lemma ext {X Y : ∀ i, C i} {f g : X ⟶ Y} (w : ∀ i, f i = g i) : f = g :=
  funext (w ·)
Extensionality of Morphisms in Product Category
Informal description
For any two morphisms $f, g \colon X \to Y$ in the product category $\prod_{i \in I} C_i$, if $f_i = g_i$ for all $i \in I$, then $f = g$.
CategoryTheory.Pi.eval definition
(i : I) : (∀ i, C i) ⥤ C i
Full source 
/--
The evaluation functor at `i : I`, sending an `I`-indexed family of objects to the object over `i`.
-/
@[simps]
def eval (i : I) : (∀ i, C i) ⥤ C i where
  obj f := f i
  map α := α i
Evaluation functor for indexed families of categories
Informal description
The evaluation functor at index $i \in I$ maps an $I$-indexed family of objects $(X_j)_{j \in I}$ in categories $\{C_j\}_{j \in I}$ to the object $X_i$ in $C_i$, and similarly maps an $I$-indexed family of morphisms $(\alpha_j)_{j \in I}$ to the morphism $\alpha_i$ in $C_i$.
CategoryTheory.Pi.instCategoryComp instance
(f : J → I) : (j : J) → Category ((C ∘ f) j)
Full source 
instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by
  dsimp
  infer_instance
Category Structure on Composed Indexed Families
Informal description
For any function $f : J \to I$ and family of categories $C_i$ indexed by $i \in I$, the composition $C \circ f$ forms a category structure on the family of objects indexed by $J$, where for each $j \in J$, $(C \circ f)(j)$ is a category.
CategoryTheory.Pi.comap definition
(h : J → I) : (∀ i, C i) ⥤ (∀ j, C (h j))
Full source 
/-- Pull back an `I`-indexed family of objects to a `J`-indexed family, along a function `J → I`.
-/
@[simps]
def comap (h : J → I) : (∀ i, C i) ⥤ (∀ j, C (h j)) where
  obj f i := f (h i)
  map α i := α (h i)
Pullback of indexed family of categories along a function
Informal description
Given a function $h \colon J \to I$ and an $I$-indexed family of categories $\{C_i\}_{i \in I}$, the functor $\text{comap}_h$ pulls back the family to a $J$-indexed family $\{C_{h(j)}\}_{j \in J}$. On objects, it maps a family $(X_i)_{i \in I}$ to $(X_{h(j)})_{j \in J}$, and on morphisms, it maps a family $(f_i \colon X_i \to Y_i)_{i \in I}$ to $(f_{h(j)} \colon X_{h(j)} \to Y_{h(j)})_{j \in J}$.
CategoryTheory.Pi.comapId definition
: comap C (id : I → I) ≅ 𝟭 (∀ i, C i)
Full source 
/-- The natural isomorphism between
pulling back a grading along the identity function,
and the identity functor. -/
@[simps]
def comapId : comapcomap C (id : I → I) ≅ 𝟭 (∀ i, C i) where
  hom := { app := fun X => 𝟙 X }
  inv := { app := fun X => 𝟙 X }
Identity pullback isomorphism for indexed families of categories
Informal description
The natural isomorphism between the pullback functor along the identity function and the identity functor on the category of $I$-indexed families of objects in categories $\{C_i\}_{i \in I}$. Specifically, for any family $(X_i)_{i \in I}$, the isomorphism maps each $X_i$ to itself via the identity morphism.
CategoryTheory.Pi.comapComp definition
(f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f)
Full source 
/-- The natural isomorphism comparing between
pulling back along two successive functions, and
pulling back along their composition
-/
@[simps!]
def comapComp (f : K → J) (g : J → I) : comapcomap C g ⋙ comap (C ∘ g) fcomap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) where
  hom :=
  { app := fun X b => 𝟙 (X (g (f b)))
    naturality := fun X Y f' => by simp only [comap, Function.comp]; funext; simp }
  inv :=
  { app := fun X b => 𝟙 (X (g (f b)))
    naturality := fun X Y f' => by simp only [comap, Function.comp]; funext; simp }
Natural isomorphism for composition of pullback functors
Informal description
The natural isomorphism between the composition of pullback functors along functions $g \colon J \to I$ and $f \colon K \to J$, and the pullback functor along their composition $g \circ f \colon K \to I$. Specifically, for an $I$-indexed family of categories $\{C_i\}_{i \in I}$, the functors $\text{comap}_g \colon \prod_{i \in I} C_i \to \prod_{j \in J} C_{g(j)}$ and $\text{comap}_f \colon \prod_{j \in J} C_{g(j)} \to \prod_{k \in K} C_{g(f(k))}$ satisfy $\text{comap}_g \circ \text{comap}_f \cong \text{comap}_{g \circ f}$.
CategoryTheory.Pi.comapEvalIsoEval definition
(h : J → I) (j : J) : comap C h ⋙ eval (C ∘ h) j ≅ eval C (h j)
Full source 
/-- The natural isomorphism between pulling back then evaluating, and just evaluating. -/
@[simps!]
def comapEvalIsoEval (h : J → I) (j : J) : comapcomap C h ⋙ eval (C ∘ h) jcomap C h ⋙ eval (C ∘ h) j ≅ eval C (h j) :=
  NatIso.ofComponents (fun _ => Iso.refl _) (by simp only [Iso.refl]; simp)
Natural isomorphism between pullback-then-evaluate and evaluate-at-image
Informal description
For any function $h \colon J \to I$ and any index $j \in J$, there is a natural isomorphism between the composition of the pullback functor $\text{comap}_h$ followed by the evaluation functor at $j$, and the evaluation functor at $h(j)$. More precisely, the natural isomorphism relates the two functors: \[ \text{comap}_h \circ \text{eval}_j \cong \text{eval}_{h(j)} \] where $\text{comap}_h$ pulls back an $I$-indexed family of objects to a $J$-indexed family via $h$, and $\text{eval}_j$ evaluates at index $j$.
CategoryTheory.Pi.sumElimCategory instance
: ∀ s : I ⊕ J, Category.{v₁} (Sum.elim C D s)
Full source 
instance sumElimCategory : ∀ s : I ⊕ J, Category.{v₁} (Sum.elim C D s)
  | Sum.inl i => by
    dsimp
    infer_instance
  | Sum.inr j => by
    dsimp
    infer_instance
Pointwise Category Structure on Disjoint Union of Indexed Families
Informal description
For any disjoint union $I \oplus J$ and families of categories $C$ and $D$ indexed by $I$ and $J$ respectively, the pointwise category structure on the family $\text{Sum.elim}\, C\, D$ is defined for each $s \in I \oplus J$.
CategoryTheory.Pi.sum definition
: (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : I ⊕ J, Sum.elim C D s
Full source 
/-- 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.
-/
@[simps]
def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : I ⊕ J, Sum.elim C D s where
  obj X :=
    { obj := fun Y s =>
        match s with
        | .inl i => X i
        | .inr j => Y j
      map := fun {_} {_} f s =>
        match s with
        | .inl i => 𝟙 (X i)
        | .inr j => f j }
  map {X} {X'} f :=
    { app := fun Y s =>
        match s with
        | .inl i => f i
        | .inr j => 𝟙 (Y j) }
Disjoint union bifunctor for indexed families of objects
Informal description
The bifunctor that combines an $I$-indexed family of objects $(X_i)_{i \in I}$ with a $J$-indexed family of objects $(Y_j)_{j \in J}$ to obtain an $(I \oplus J)$-indexed family of objects, where $I \oplus J$ is the disjoint union of $I$ and $J$. For each $s \in I \oplus J$, the object is defined as: \[ \text{Sum.elim}\, X\, Y\, s = \begin{cases} X_i & \text{if } s = \text{inl}\, i, \\ Y_j & \text{if } s = \text{inr}\, j. \end{cases} \] The morphisms are defined componentwise, with identity morphisms on the $X_i$ components and the given morphisms on the $Y_j$ components.
CategoryTheory.Pi.isoApp definition
{X Y : ∀ i, C i} (f : X ≅ Y) (i : I) : X i ≅ Y i
Full source 
/-- An isomorphism between `I`-indexed objects gives an isomorphism between each
pair of corresponding components. -/
@[simps]
def isoApp {X Y : ∀ i, C i} (f : X ≅ Y) (i : I) : X i ≅ Y i :=
  ⟨f.hom i, f.inv i,
    by rw [← comp_apply, Iso.hom_inv_id, id_apply], by rw [← comp_apply, Iso.inv_hom_id, id_apply]⟩
Componentwise isomorphism of indexed families
Informal description
Given an isomorphism $f \colon X \cong Y$ between $I$-indexed families of objects in a category $\mathcal{C}$, the componentwise isomorphism at index $i \in I$ is the pair of morphisms $(f_i \colon X_i \to Y_i, f_i^{-1} \colon Y_i \to X_i)$ satisfying $f_i \circ f_i^{-1} = \text{id}_{Y_i}$ and $f_i^{-1} \circ f_i = \text{id}_{X_i}$.
CategoryTheory.Pi.isoApp_refl theorem
(X : ∀ i, C i) (i : I) : isoApp (Iso.refl X) i = Iso.refl (X i)
Full source 
@[simp]
theorem isoApp_refl (X : ∀ i, C i) (i : I) : isoApp (Iso.refl X) i = Iso.refl (X i) :=
  rfl
Componentwise Identity Isomorphism in Product Category
Informal description
For any $I$-indexed family of objects $X$ in a category $\mathcal{C}$ and any index $i \in I$, the componentwise application of the identity isomorphism on $X$ at $i$ is equal to the identity isomorphism on $X_i$. In other words, $(\text{id}_X)_i = \text{id}_{X_i}$.
CategoryTheory.Pi.isoApp_symm theorem
{X Y : ∀ i, C i} (f : X ≅ Y) (i : I) : isoApp f.symm i = (isoApp f i).symm
Full source 
@[simp]
theorem isoApp_symm {X Y : ∀ i, C i} (f : X ≅ Y) (i : I) : isoApp f.symm i = (isoApp f i).symm :=
  rfl
Inverse of Componentwise Isomorphism Equals Componentwise Inverse
Informal description
For any isomorphism $f \colon X \cong Y$ between $I$-indexed families of objects in a category $\mathcal{C}$, and for any index $i \in I$, the componentwise isomorphism of the inverse isomorphism $f^{-1}$ at $i$ is equal to the inverse of the componentwise isomorphism of $f$ at $i$. In symbols: $$(\text{isoApp}\, f^{-1})_i = (\text{isoApp}\, f)_i^{-1}.$$
CategoryTheory.Pi.isoApp_trans theorem
{X Y Z : ∀ i, C i} (f : X ≅ Y) (g : Y ≅ Z) (i : I) : isoApp (f ≪≫ g) i = isoApp f i ≪≫ isoApp g i
Full source 
@[simp]
theorem isoApp_trans {X Y Z : ∀ i, C i} (f : X ≅ Y) (g : Y ≅ Z) (i : I) :
    isoApp (f ≪≫ g) i = isoAppisoApp f i ≪≫ isoApp g i :=
  rfl
Componentwise Composition of Isomorphisms in Product Category
Informal description
For any isomorphisms $f \colon X \cong Y$ and $g \colon Y \cong Z$ between $I$-indexed families of objects in a category $\mathcal{C}$, and for any index $i \in I$, the componentwise isomorphism of the composition $f \ggg g$ at $i$ is equal to the composition of the componentwise isomorphisms of $f$ and $g$ at $i$. That is, $(f \ggg g)_i = f_i \ggg g_i$.
CategoryTheory.Functor.pi definition
(F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i
Full source 
/-- Assemble an `I`-indexed family of functors into a functor between the pi types.
-/
@[simps]
def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i where
  obj f i := (F i).obj (f i)
  map α i := (F i).map (α i)
Product functor of indexed family of functors
Informal description
Given an indexed family of functors $F_i \colon C_i \to D_i$ for each $i$ in some index set $I$, the functor $\prod_{i \in I} F_i \colon \prod_{i \in I} C_i \to \prod_{i \in I} D_i$ is defined by applying each $F_i$ componentwise. Specifically, it maps an object $(X_i)_{i \in I}$ to $(F_i(X_i))_{i \in I}$ and a morphism $(f_i)_{i \in I}$ to $(F_i(f_i))_{i \in I}$.
CategoryTheory.Functor.pi' definition
(f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i
Full source 
/-- Similar to `pi`, but all functors come from the same category `A`
-/
@[simps]
def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i where
  obj a i := (f i).obj a
  map h i := (f i).map h
Product functor from a family of functors with the same domain
Informal description
Given a category $A$ and a family of categories $\{C_i\}_{i \in I}$ with functors $F_i \colon A \to C_i$ for each $i \in I$, the functor $\prod_{i \in I} F_i \colon A \to \prod_{i \in I} C_i$ is defined by: - On objects: $(\prod_{i \in I} F_i)(a) = (F_i(a))_{i \in I}$ for any $a \in A$. - On morphisms: $(\prod_{i \in I} F_i)(h) = (F_i(h))_{i \in I}$ for any morphism $h$ in $A$. This functor maps an object $a$ in $A$ to the tuple of objects $(F_i(a))_{i \in I}$ in the product category, and a morphism $h$ in $A$ to the tuple of morphisms $(F_i(h))_{i \in I}$.
CategoryTheory.Functor.pi'CompEval definition
{A : Type*} [Category A] (F : ∀ i, A ⥤ C i) (i : I) : pi' F ⋙ Pi.eval C i ≅ F i
Full source 
/-- The projections of `Functor.pi' F` are isomorphic to the functors of the family `F` -/
@[simps!]
def pi'CompEval {A : Type*} [Category A] (F : ∀ i, A ⥤ C i) (i : I) :
    pi'pi' F ⋙ Pi.eval C ipi' F ⋙ Pi.eval C i ≅ F i :=
  Iso.refl _
Isomorphism between projection of product functor and component functor
Informal description
For any category \( A \) and a family of functors \( F_i \colon A \to C_i \) indexed by \( i \in I \), the composition of the product functor \( \prod_{i \in I} F_i \colon A \to \prod_{i \in I} C_i \) with the evaluation functor at index \( i \) is naturally isomorphic to \( F_i \). In other words, the projection of the product functor \( \prod_{i \in I} F_i \) onto the \( i \)-th component is isomorphic to \( F_i \) itself.
CategoryTheory.Functor.eqToHom_proj theorem
{x x' : ∀ i, C i} (h : x = x') (i : I) : (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i)
Full source 
@[simp]
theorem eqToHom_proj {x x' : ∀ i, C i} (h : x = x') (i : I) :
    (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i) := by
  subst h
  rfl
Componentwise Equality Morphism in Product Category
Informal description
For any family of objects $\{x_i\}_{i \in I}$ and $\{x'_i\}_{i \in I}$ in a category $\mathcal{C}$, and an equality $h : x = x'$ between them, the $i$-th component of the morphism $\text{eqToHom}(h) : x \to x'$ is equal to $\text{eqToHom}(h_i)$, where $h_i$ is the equality of the $i$-th components obtained from $h$ via function extensionality.
CategoryTheory.Functor.pi'_eval theorem
(f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙ Pi.eval C i = f i
Full source 
@[simp]
theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi'pi' f ⋙ Pi.eval C i = f i := by
  apply Functor.ext
  · intro _ _ _
    simp
  · intro _
    rfl
Evaluation of Product Functor Equals Component Functor
Informal description
For any family of functors $F_i \colon A \to C_i$ indexed by $i \in I$, the composition of the product functor $\prod_{i \in I} F_i \colon A \to \prod_{i \in I} C_i$ with the evaluation functor at index $i$ is equal to $F_i$. That is, $(\prod_{j \in I} F_j) \circ \text{eval}_i = F_i$ for each $i \in I$.
CategoryTheory.Functor.pi_ext theorem
(f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) : f = f'
Full source 
/-- Two functors to a product category are equal iff they agree on every coordinate. -/
theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) :
    f = f' := by
  apply Functor.ext; rotate_left
  · intro X
    ext i
    specialize h i
    have := congr_obj h X
    simpa
  · intro X Y g
    dsimp
    funext i
    specialize h i
    have := congr_hom h g
    simpa
Equality of Functors to Product Category via Componentwise Equality
Informal description
Let $A$ and $\{C_i\}_{i \in I}$ be categories, and let $f, f' \colon A \to \prod_{i \in I} C_i$ be functors. If for every $i \in I$, the composition of $f$ with the evaluation functor at $i$ equals the composition of $f'$ with the evaluation functor at $i$, i.e., $f \circ \text{eval}_i = f' \circ \text{eval}_i$, then $f = f'$.
CategoryTheory.NatTrans.pi definition
(α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G
Full source 
/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
-/
@[simps!]
def pi (α : ∀ i, F i ⟶ G i) : Functor.piFunctor.pi F ⟶ Functor.pi G where
  app f i := (α i).app (f i)
Product natural transformation of indexed family of natural transformations
Informal description
Given an indexed family of natural transformations $\alpha_i \colon F_i \to G_i$ for each $i$ in some index set $I$, the natural transformation $\prod_{i \in I} \alpha_i \colon \prod_{i \in I} F_i \to \prod_{i \in I} G_i$ is defined by applying each $\alpha_i$ componentwise. Specifically, it maps an object $(X_i)_{i \in I}$ to $(\alpha_i(X_i))_{i \in I}$.
CategoryTheory.NatTrans.pi' definition
{E : Type*} [Category E] {F G : E ⥤ ∀ i, C i} (τ : ∀ i, F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i) : F ⟶ G
Full source 
/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
-/
@[simps]
def pi' {E : Type*} [Category E] {F G : E ⥤ ∀ i, C i}
    (τ : ∀ i, F ⋙ Pi.eval C iF ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i) : F ⟶ G where
  app := fun X i => (τ i).app X
  naturality _ _ f := by
    ext i
    exact (τ i).naturality f
Natural transformation from an indexed family of natural transformations
Informal description
Given a category $E$ and two functors $F, G \colon E \to \prod_{i \in I} C_i$ into a product category, the function assembles an $I$-indexed family of natural transformations $\tau_i \colon F \circ \text{eval}_i \to G \circ \text{eval}_i$ (where $\text{eval}_i$ is the evaluation functor at index $i$) into a single natural transformation $\tau \colon F \to G$. For each object $X$ in $E$, the component $\tau_X$ is defined pointwise by $(\tau_X)_i = (\tau_i)_X$, and the naturality condition holds componentwise.
CategoryTheory.NatIso.pi definition
(e : ∀ i, F i ≅ G i) : Functor.pi F ≅ Functor.pi G
Full source 
/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
-/
@[simps]
def pi (e : ∀ i, F i ≅ G i) : Functor.piFunctor.pi F ≅ Functor.pi G where
  hom := NatTrans.pi (fun i => (e i).hom)
  inv := NatTrans.pi (fun i => (e i).inv)
Product natural isomorphism of indexed family of natural isomorphisms
Informal description
Given an indexed family of natural isomorphisms \( e_i \colon F_i \cong G_i \) for each \( i \) in some index set \( I \), the natural isomorphism \( \prod_{i \in I} e_i \colon \prod_{i \in I} F_i \cong \prod_{i \in I} G_i \) is defined by applying each \( e_i \) componentwise. Specifically, its forward component (hom) is the product natural transformation of the forward components \( (e_i)_\text{hom} \), and its backward component (inv) is the product natural transformation of the backward components \( (e_i)_\text{inv} \).
CategoryTheory.NatIso.pi' definition
{E : Type*} [Category E] {F G : E ⥤ ∀ i, C i} (e : ∀ i, F ⋙ Pi.eval C i ≅ G ⋙ Pi.eval C i) : F ≅ G
Full source 
/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
-/
@[simps]
def pi' {E : Type*} [Category E] {F G : E ⥤ ∀ i, C i}
    (e : ∀ i, F ⋙ Pi.eval C iF ⋙ Pi.eval C i ≅ G ⋙ Pi.eval C i) : F ≅ G where
  hom := NatTrans.pi' (fun i => (e i).hom)
  inv := NatTrans.pi' (fun i => (e i).inv)
Natural isomorphism from an indexed family of natural isomorphisms
Informal description
Given a category $E$ and two functors $F, G \colon E \to \prod_{i \in I} C_i$ into a product category, the function assembles an $I$-indexed family of natural isomorphisms $e_i \colon F \circ \text{eval}_i \to G \circ \text{eval}_i$ (where $\text{eval}_i$ is the evaluation functor at index $i$) into a single natural isomorphism $e \colon F \to G$. The components of the natural isomorphism are defined pointwise by the components of the family $e_i$.
CategoryTheory.isIso_pi_iff theorem
{X Y : ∀ i, C i} (f : X ⟶ Y) : IsIso f ↔ ∀ i, IsIso (f i)
Full source 
lemma isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) :
    IsIsoIsIso f ↔ ∀ i, IsIso (f i) := by
  constructor
  · intro _ i
    exact (Pi.isoApp (asIso f) i).isIso_hom
  · intro
    exact ⟨fun i => inv (f i), by aesop_cat, by aesop_cat⟩
Componentwise Isomorphism Criterion for Indexed Families
Informal description
For any morphism $f \colon X \to Y$ between $I$-indexed families of objects in a category $\mathcal{C}$, the morphism $f$ is an isomorphism if and only if for every index $i \in I$, the component $f_i \colon X_i \to Y_i$ is an isomorphism.
CategoryTheory.Pi.eqToEquivalence definition
{i j : I} (h : i = j) : C i ≌ C j
Full source 
/-- For a family of categories `C i` indexed by `I`, an equality `i = j` in `I` induces
an equivalence `C i ≌ C j`. -/
def Pi.eqToEquivalence {i j : I} (h : i = j) : C i ≌ C j := by subst h; rfl
Equivalence of categories induced by equality of indices
Informal description
Given an equality $h : i = j$ between indices $i$ and $j$ in an index type $I$, this definition constructs an equivalence of categories between the categories $C_i$ and $C_j$ associated with these indices. The equivalence is obtained by substituting $h$ to identify $i$ and $j$, and then using reflexivity to establish the equivalence.
CategoryTheory.Pi.evalCompEqToEquivalenceFunctor definition
{i j : I} (h : i = j) : Pi.eval C i ⋙ (Pi.eqToEquivalence C h).functor ≅ Pi.eval C j
Full source 
/-- 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`. -/
@[simps!]
def Pi.evalCompEqToEquivalenceFunctor {i j : I} (h : i = j) :
    Pi.evalPi.eval C i ⋙ (Pi.eqToEquivalence C h).functorPi.eval C i ⋙ (Pi.eqToEquivalence C h).functor ≅
      Pi.eval C j :=
  eqToIso (by subst h; rfl)
Isomorphism between evaluation functors via index equality
Informal description
For any equality \( h : i = j \) between indices \( i \) and \( j \) in an index type \( I \), the composition of the evaluation functor at \( i \) with the functor part of the equivalence induced by \( h \) is naturally isomorphic to the evaluation functor at \( j \).
CategoryTheory.Pi.eqToEquivalenceFunctorIso definition
(f : J → I) {i' j' : J} (h : i' = j') : (Pi.eqToEquivalence C (congr_arg f h)).functor ≅ (Pi.eqToEquivalence (fun i' => C (f i')) h).functor
Full source 
/-- The equivalences given by `Pi.eqToEquivalence` are compatible with reindexing. -/
@[simps!]
def Pi.eqToEquivalenceFunctorIso (f : J → I) {i' j' : J} (h : i' = j') :
    (Pi.eqToEquivalence C (congr_arg f h)).functor ≅
      (Pi.eqToEquivalence (fun i' => C (f i')) h).functor :=
  eqToIso (by subst h; rfl)
Isomorphism of functors induced by index equality under reindexing
Informal description
Given a function $f : J \to I$ between index types and an equality $h : i' = j'$ between indices $i', j' \in J$, the functors obtained from the equivalences of categories induced by $\text{congr\_arg}\, f\, h$ and by $h$ itself are isomorphic. Specifically, the functor from the equivalence induced by $\text{congr\_arg}\, f\, h$ (which maps $C(f\, i')$ to $C(f\, j')$) is isomorphic to the functor from the equivalence induced by $h$ (which maps $C(f\, i')$ to $C(f\, j')$ when $i' = j'$).
CategoryTheory.Pi.equivalenceOfEquiv definition
(e : J ≃ I) : (∀ j, C (e j)) ≌ (∀ i, C i)
Full source 
/-- Reindexing a family of categories gives equivalent `Pi` categories. -/
@[simps]
noncomputable def Pi.equivalenceOfEquiv (e : J ≃ I) :
    (∀ j, C (e j)) ≌ (∀ i, C i) where
  functor := Functor.pi' (fun i => Pi.eval _ (e.symm i) ⋙
    (Pi.eqToEquivalence C (by simp)).functor)
  inverse := Functor.pi' (fun i' => Pi.eval _ (e i'))
  unitIso := NatIso.pi' (fun i' => Functor.leftUnitor _ ≪≫
    (Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) (e.symm_apply_apply i')).symm ≪≫
    isoWhiskerLeft _ ((Pi.eqToEquivalenceFunctorIso C e (e.symm_apply_apply i')).symm) ≪≫
    (Functor.pi'CompEval _ _).symm ≪≫ isoWhiskerLeft _ (Functor.pi'CompEval _ _).symm ≪≫
    (Functor.associator _ _ _).symm)
  counitIso := NatIso.pi' (fun i => (Functor.associator _ _ _).symm ≪≫
    isoWhiskerRight (Functor.pi'CompEval _ _) _ ≪≫
    Pi.evalCompEqToEquivalenceFunctor C (e.apply_symm_apply i) ≪≫
    (Functor.leftUnitor _).symm)
Equivalence of product categories induced by index equivalence
Informal description
Given an equivalence $e : J \simeq I$ between index types $J$ and $I$, and a family of categories $\{C_i\}_{i \in I}$, there is an equivalence of categories between the product category $\prod_{j \in J} C_{e(j)}$ and the product category $\prod_{i \in I} C_i$. The equivalence is constructed via: - A functor that reindexes the product category $\prod_{j \in J} C_{e(j)}$ to $\prod_{i \in I} C_i$ using the inverse equivalence $e^{-1}$. - An inverse functor that reindexes back using $e$. - Natural isomorphisms witnessing that these functors form an equivalence.
CategoryTheory.Pi.optionEquivalence definition
(C' : Option J → Type u₁) [∀ i, Category.{v₁} (C' i)] : (∀ i, C' i) ≌ C' none × (∀ (j : J), C' (some j))
Full source 
/-- A product of categories indexed by `Option J` identifies to a binary product. -/
@[simps]
def Pi.optionEquivalence (C' : Option J → Type u₁) [∀ i, Category.{v₁} (C' i)] :
    (∀ i, C' i) ≌ C' none × (∀ (j : J), C' (some j)) where
  functor := Functor.prod' (Pi.eval C' none)
    (Functor.pi' (fun i => (Pi.eval _ (some i))))
  inverse := Functor.pi' (fun i => match i with
    | none => Prod.fst _ _
    | some i => Prod.snd _ _ ⋙ (Pi.eval _ i))
  unitIso := NatIso.pi' (fun i => match i with
    | none => Iso.refl _
    | some _ => Iso.refl _)
  counitIso := by exact Iso.refl _
Equivalence between product category over Option J and binary product with indexed product
Informal description
For any family of categories $\{C_i\}_{i \in \text{Option } J}$ indexed by $\text{Option } J$, there is an equivalence of categories between the product category $\prod_{i \in \text{Option } J} C_i$ and the product category $C_{\text{none}} \times \prod_{j \in J} C_{\text{some } j}$. The equivalence is given by: - A functor that evaluates at $\text{none}$ and maps the remaining components via a product functor. - An inverse functor that reconstructs the original family by projecting from the product. - Natural isomorphisms witnessing the equivalence, which are identity isomorphisms in each component.
CategoryTheory.Equivalence.pi definition
(E : ∀ i, C i ≌ D i) : (∀ i, C i) ≌ (∀ i, D i)
Full source 
/-- Assemble an `I`-indexed family of equivalences of categories
into a single equivalence. -/
@[simps]
def pi (E : ∀ i, C i ≌ D i) : (∀ i, C i) ≌ (∀ i, D i) where
  functor := Functor.pi (fun i => (E i).functor)
  inverse := Functor.pi (fun i => (E i).inverse)
  unitIso := NatIso.pi (fun i => (E i).unitIso)
  counitIso := NatIso.pi (fun i => (E i).counitIso)
Product Equivalence of Indexed Family of Equivalences
Informal description
Given an indexed family of equivalences of categories \( E_i \colon C_i \simeq D_i \) for each \( i \) in some index set \( I \), the equivalence \( \prod_{i \in I} E_i \colon \prod_{i \in I} C_i \simeq \prod_{i \in I} D_i \) is constructed as follows: - The forward functor is the product functor \( \prod_{i \in I} F_i \), where \( F_i \) is the forward functor of \( E_i \). - The inverse functor is the product functor \( \prod_{i \in I} G_i \), where \( G_i \) is the inverse functor of \( E_i \). - The unit isomorphism is the product natural isomorphism \( \prod_{i \in I} \eta_i \), where \( \eta_i \) is the unit isomorphism of \( E_i \). - The counit isomorphism is the product natural isomorphism \( \prod_{i \in I} \epsilon_i \), where \( \epsilon_i \) is the counit isomorphism of \( E_i \).
CategoryTheory.Equivalence.instIsEquivalenceForallPi instance
(F : ∀ i, C i ⥤ D i) [∀ i, (F i).IsEquivalence] : (Functor.pi F).IsEquivalence
Full source 
instance (F : ∀ i, C i ⥤ D i) [∀ i, (F i).IsEquivalence] :
    (Functor.pi F).IsEquivalence :=
  (pi (fun i => (F i).asEquivalence)).isEquivalence_functor
Product of Equivalences is an Equivalence
Informal description
For any family of functors $F_i \colon C_i \to D_i$ where each $F_i$ is an equivalence of categories, the product functor $\prod_{i} F_i \colon \prod_{i} C_i \to \prod_{i} D_i$ is also an equivalence of categories.