CategoryTheory.prod_comp
theorem CategoryTheory.prod_comp :
∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂)
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)),
CategoryTheory.CategoryStruct.comp f g =
(CategoryTheory.CategoryStruct.comp f.1 g.1, CategoryTheory.CategoryStruct.comp f.2 g.2)
This theorem, `CategoryTheory.prod_comp`, states that for any two categories `C` and `D` with any three objects `P, Q, R` from `C` and `S, T, U` from `D`, and any two morphisms `f` and `g` such that `f` is from `(P, S)` to `(Q, T)` and `g` is from `(Q, T)` to `(R, U)`, the composition of the morphisms `f` and `g` in the product category is equal to the pair of the compositions of the corresponding morphisms in the original categories `C` and `D`. In other words, composing morphisms in a product category is the same as composing the corresponding morphisms in the factors of the product, taken componentwise.
More concisely: In the product category of two categories C and D, the composition of morphisms (f : P → Q in C) and (g : Q → R in D), where P, Q, R are objects from C and S, T, U are objects from D, is equal to the pair of the compositions of f and g in C and D, respectively.
|
CategoryTheory.prod_id
theorem CategoryTheory.prod_id :
∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂)
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (X : C) (Y : D),
CategoryTheory.CategoryStruct.id (X, Y) =
(CategoryTheory.CategoryStruct.id X, CategoryTheory.CategoryStruct.id Y)
The theorem `CategoryTheory.prod_id` states that for any two categories `C` and `D` with arbitrary objects `X` and `Y` respectively, the identity morphism on the product of the objects `(X, Y)` is equal to the product of the identity morphisms on `X` and `Y`. This implies that each component of the product identity morphism is just the identity morphism of the corresponding component category.
More concisely: For any categories C and D with objects X from C and Y from D, the identity morphism of the product X × Y in the product category C × D is equal to the product of the identity morphisms of X and Y.
|