Documentation

Mathlib.CategoryTheory.Products.Basic

Cartesian products of categories #

We define the category instance on C × D when C and D are categories.

We define:

We further define evaluation : C ⥤ (C ⥤ D) ⥤ D and evaluationUncurried : C × (C ⥤ D) ⥤ D, and products of functors and natural transformations, written F.prod G and α.prod β.

@[simp]
theorem CategoryTheory.prod_Hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) (Y : C × D) :
(X Y) = ((X.1 Y.1) × (X.2 Y.2))
@[simp]

Two rfl lemmas that cannot be generated by @[simps].

@[simp]
theorem CategoryTheory.prod_comp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {R : C} {S : D} {T : D} {U : D} (f : (P, S) (Q, T)) (g : (Q, T) (R, U)) :

The isomorphism between (X.1, X.2) and X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Iso.prod_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
    (f.prod g).inv = (f.inv, g.inv)
    @[simp]
    theorem CategoryTheory.Iso.prod_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
    (f.prod g).hom = (f.hom, g.hom)
    def CategoryTheory.Iso.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {P : C} {Q : C} {S : D} {T : D} (f : P Q) (g : S T) :
    (P, S) (Q, T)

    Construct an isomorphism in C × D out of two isomorphisms in C and D.

    Equations
    • f.prod g = { hom := (f.hom, g.hom), inv := (f.inv, g.inv), hom_inv_id := , inv_hom_id := }
    Instances For

      Category.uniformProd C D is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.

      Equations

      sectl C Z is the functor C ⥤ C × D given by X ↦ (X, Z).

      Equations
      Instances For

        sectr Z D is the functor D ⥤ C × D given by Y ↦ (Z, Y) .

        Equations
        Instances For
          @[simp]

          fst is the functor (X, Y) ↦ X.

          Equations
          Instances For
            @[simp]

            snd is the functor (X, Y) ↦ Y.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Prod.swap_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
              ∀ {X Y : C × D} (f : X Y), (CategoryTheory.Prod.swap C D).map f = (f.2, f.1)

              The functor swapping the factors of a cartesian product of categories, C × D ⥤ D × C.

              Equations
              Instances For

                Swapping the factors of a cartesian product of categories twice is naturally isomorphic to the identity functor.

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

                  The equivalence, given by swapping factors, between C × D and D × C.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.evaluation_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) :
                    ∀ {X_1 Y : CategoryTheory.Functor C D} (α : X_1 Y), ((CategoryTheory.evaluation C D).obj X).map α = α.app X
                    @[simp]
                    theorem CategoryTheory.evaluation_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (f : X Y) (F : CategoryTheory.Functor C D) :
                    ((CategoryTheory.evaluation C D).map f).app F = F.map f

                    The "evaluation at X" functor, such that (evaluation.obj X).obj F = F.obj X, which is functorial in both X and F.

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

                      The "evaluation of F at X" functor, as a functor C × (C ⥤ D) ⥤ D.

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

                        The constant functor followed by the evaluation functor is just the identity.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Functor.prod_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D) :
                          ∀ {X Y : A × C} (f : X Y), (F.prod G).map f = (F.map f.1, G.map f.2)

                          The cartesian product of two functors.

                          Equations
                          • F.prod G = { obj := fun (X : A × C) => (F.obj X.1, G.obj X.2), map := fun {X Y : A × C} (f : X Y) => (F.map f.1, G.map f.2), map_id := , map_comp := }
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Functor.prod'_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) :
                            ∀ {X Y : A} (f : X Y), (F.prod' G).map f = (F.map f, G.map f)
                            @[simp]

                            Similar to prod, but both functors start from the same category A

                            Equations
                            • F.prod' G = { obj := fun (a : A) => (F.obj a, G.obj a), map := fun {X Y : A} (f : X Y) => (F.map f, G.map f), map_id := , map_comp := }
                            Instances For

                              The product F.prod' G followed by projection on the first component is isomorphic to F

                              Equations
                              Instances For

                                The product F.prod' G followed by projection on the second component is isomorphic to G

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Functor.diag_map (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X : C} {Y : C} (f : X Y) :

                                  The cartesian product of two natural transformations.

                                  Equations
                                  Instances For

                                    The cartesian product functor between functor categories

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

                                      The cartesian product of two natural isomorphisms.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.prod_functor {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A B) (E₂ : C D) :
                                        (E₁.prod E₂).functor = E₁.functor.prod E₂.functor
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.prod_unitIso {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A B) (E₂ : C D) :
                                        (E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.prod_inverse {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A B) (E₂ : C D) :
                                        (E₁.prod E₂).inverse = E₁.inverse.prod E₂.inverse
                                        @[simp]
                                        theorem CategoryTheory.Equivalence.prod_counitIso {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A B) (E₂ : C D) :
                                        (E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso

                                        The cartesian product of two equivalences of categories.

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

                                          F.flip composed with evaluation is the same as evaluating F.

                                          Equations
                                          Instances For

                                            The forward direction for functorProdFunctorEquiv

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.functorProdToProdFunctor_map (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] :
                                              ∀ {X Y : CategoryTheory.Functor A (B × C)} (α : X Y), (CategoryTheory.functorProdToProdFunctor A B C).map α = ({ app := fun (X_1 : A) => (α.app X_1).1, naturality := }, { app := fun (X_1 : A) => (α.app X_1).2, naturality := })

                                              The backward direction for functorProdFunctorEquiv

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

                                                The equivalence of categories between (A ⥤ B) × (A ⥤ C) and A ⥤ (B × C)

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.prodOpEquiv_counitIso (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] :
                                                  (CategoryTheory.prodOpEquiv C).counitIso = CategoryTheory.Iso.refl ({ obj := fun (x : Cᵒᵖ × Dᵒᵖ) => match x with | (X, Y) => Opposite.op (Opposite.unop X, Opposite.unop Y), map := fun {X Y : Cᵒᵖ × Dᵒᵖ} (x : X Y) => match x with | (f, g) => Opposite.op (f.unop, g.unop), map_id := , map_comp := }.comp { obj := fun (X : (C × D)ᵒᵖ) => (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2), map := fun {X Y : (C × D)ᵒᵖ} (f : X Y) => (f.unop.1.op, f.unop.2.op), map_id := , map_comp := })
                                                  @[simp]
                                                  theorem CategoryTheory.prodOpEquiv_inverse_map (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] :
                                                  ∀ {X Y : Cᵒᵖ × Dᵒᵖ} (x : X Y), (CategoryTheory.prodOpEquiv C).inverse.map x = match x with | (f, g) => Opposite.op (f.unop, g.unop)
                                                  @[simp]
                                                  theorem CategoryTheory.prodOpEquiv_functor_map (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] :
                                                  ∀ {X Y : (C × D)ᵒᵖ} (f : X Y), (CategoryTheory.prodOpEquiv C).functor.map f = (f.unop.1.op, f.unop.2.op)

                                                  The equivalence between the opposite of a product and the product of the opposites.

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