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.fst Y.fst) × (X.snd Y.snd))
@[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.

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) :
    (CategoryTheory.Iso.prod f 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) :
    (CategoryTheory.Iso.prod f 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.

    Instances For

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

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

      Instances For

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

        Instances For
          @[simp]
          theorem CategoryTheory.Prod.fst_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.fst C D).map f = f.fst

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

          Instances For
            @[simp]
            theorem CategoryTheory.Prod.snd_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.snd C D).map f = f.snd

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

            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.snd, f.fst)

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

              Instances For

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

                Instances For
                  @[simp]
                  theorem CategoryTheory.Prod.braiding_inverse_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
                  ∀ {X Y : D × C} (f : X Y), (CategoryTheory.Prod.braiding C D).inverse.map f = (f.snd, f.fst)
                  @[simp]
                  theorem CategoryTheory.Prod.braiding_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.Prod.braiding C D).functor.map f = (f.snd, f.fst)

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

                  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 Y : CategoryTheory.Functor C D} (α : X 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.

                    Instances For

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

                      Instances For

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

                        Instances For

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

                          Instances For

                            The diagonal functor.

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

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

                              Instances For