Documentation

Mathlib.CategoryTheory.Pi.Basic

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) → CategoryTheory.Category.{v₁, u₁} (C 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) → CategoryTheory.Category.{v₁, u₁} (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
@[simp]
theorem CategoryTheory.Pi.id_apply {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) :
@[simp]
theorem CategoryTheory.Pi.comp_apply {I : Type w₀} (C : IType 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) :
theorem CategoryTheory.Pi.ext {I : Type w₀} (C : IType 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
@[simp]
theorem CategoryTheory.Pi.eval_map {I : Type w₀} (C : IType 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
@[simp]
theorem CategoryTheory.Pi.eval_obj {I : Type w₀} (C : IType 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
def CategoryTheory.Pi.eval {I : Type w₀} (C : IType 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 := }
Instances For
    instance CategoryTheory.Pi.instCategoryComp {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (f : JI) (j : J) :
    Equations
    @[simp]
    theorem CategoryTheory.Pi.comap_map {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : JI) :
    ∀ {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 : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : JI) (f : (i : I) → C i) (i : J) :
    (CategoryTheory.Pi.comap C h).obj f i = f (h i)
    def CategoryTheory.Pi.comap {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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
    • 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
      @[simp]
      theorem CategoryTheory.Pi.comapId_inv_app (I : Type w₀) (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) :
      @[simp]
      theorem CategoryTheory.Pi.comapId_hom_app (I : Type w₀) (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) :
      def CategoryTheory.Pi.comapId (I : Type w₀) (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (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) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (X : (i : I) → C i) (b : K) :
        @[simp]
        theorem CategoryTheory.Pi.comapComp_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : KJ) (g : JI) (X : (i : I) → C i) (b : K) :
        def CategoryTheory.Pi.comapComp {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
          @[simp]
          theorem CategoryTheory.Pi.comapEvalIsoEval_inv_app {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : JI) (j : J) (X : (i : I) → C i) :
          def CategoryTheory.Pi.comapEvalIsoEval {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : JType u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (s : I J) :
            Equations
            @[simp]
            theorem CategoryTheory.Pi.sum_obj_obj {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : JType 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_map_app {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : JType 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)
            @[simp]
            theorem CategoryTheory.Pi.sum_obj_map {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : JType u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) {Y : (j : J) → D j} {Y' : (j : J) → D j} (f : Y Y') (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
            def CategoryTheory.Pi.sum {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : JType 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.
            Instances For
              @[simp]
              theorem CategoryTheory.Pi.isoApp_inv {I : Type w₀} {C : IType 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 : IType 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
              def CategoryTheory.Pi.isoApp {I : Type w₀} {C : IType 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
              Instances For
                @[simp]
                theorem CategoryTheory.Pi.isoApp_refl {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I) :
                @[simp]
                theorem CategoryTheory.Pi.isoApp_symm {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) (i : I) :
                @[simp]
                theorem CategoryTheory.Pi.isoApp_trans {I : Type w₀} {C : IType 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) :
                @[simp]
                theorem CategoryTheory.Functor.pi_obj {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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
                • 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) → 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
                  @[simp]
                  theorem CategoryTheory.Functor.pi'_map {I : Type w₀} {C : IType 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
                  def CategoryTheory.Functor.pi' {I : Type w₀} {C : IType 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 := }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Functor.pi'CompEval_hom_app {I : Type w₀} {C : IType 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) :
                    @[simp]
                    theorem CategoryTheory.Functor.pi'CompEval_inv_app {I : Type w₀} {C : IType 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) :
                    def CategoryTheory.Functor.pi'CompEval {I : Type w₀} {C : IType 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) :

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

                      @[simp]
                      theorem CategoryTheory.NatTrans.pi_app {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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) :

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

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.NatTrans.pi'_app {I : Type w₀} {C : IType 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.NatTrans.pi' {I : Type w₀} {C : IType 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
                        Instances For
                          @[simp]
                          theorem CategoryTheory.NatIso.pi_hom {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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) :

                          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) → 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)) :
                            @[simp]
                            theorem CategoryTheory.NatIso.pi'_hom {I : Type w₀} {C : IType 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)) :
                            def CategoryTheory.NatIso.pi' {I : Type w₀} {C : IType 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
                            • 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) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) → C i} {Y : (i : I) → C i} (f : X Y) :
                              def CategoryTheory.Pi.eqToEquivalence {I : Type w₀} (C : IType 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
                              Instances For
                                def CategoryTheory.Pi.evalCompEqToEquivalenceFunctor {I : Type w₀} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i : I} {j : I} (h : i = 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
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv {I : Type w₀} {J : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C 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) → CategoryTheory.Category.{v₁, u₁} (C 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) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : JI) {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
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Pi.equivalenceOfEquiv_counitIso {I : Type w₀} {J : Type w₁} (C : IType 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 (fun (i : I) => C i) (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 (fun (i : I) => C i) (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 : IType 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
                                    @[simp]
                                    theorem CategoryTheory.Pi.equivalenceOfEquiv_functor {I : Type w₀} {J : Type w₁} (C : IType 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_inverse {I : Type w₀} {J : Type w₁} (C : IType 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 (fun (i : I) => C i) (e i')
                                    noncomputable def CategoryTheory.Pi.equivalenceOfEquiv {I : Type w₀} {J : Type w₁} (C : IType 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.
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Pi.optionEquivalence_counitIso {J : Type w₁} (C' : Option JType 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 (fun (i : Option J) => C' i) (some i))))
                                      @[simp]
                                      @[simp]
                                      theorem CategoryTheory.Pi.optionEquivalence_unitIso {J : Type w₁} (C' : Option JType 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 (fun (i : Option J) => C' i) none)) | some i => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id ((i : Option J) → C' i)).comp (CategoryTheory.Pi.eval (fun (i : Option J) => C' i) (some i)))
                                      @[simp]
                                      theorem CategoryTheory.Pi.optionEquivalence_inverse {J : Type w₁} (C' : Option JType 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)
                                      def CategoryTheory.Pi.optionEquivalence {J : Type w₁} (C' : Option JType 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.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.pi_counitIso {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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 : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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_inverse {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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_unitIso {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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
                                        def CategoryTheory.Equivalence.pi {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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.
                                        Instances For
                                          instance CategoryTheory.Equivalence.instIsEquivalenceForallPi {I : Type w₀} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType 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
                                          • =