Metamath Proof Explorer

Theorem fucofunc

Description: The functor composition bifunctor is a functor.

However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let C and D be categories of one object and one morphism, for example, ( SetCat1o ) , and E be a category with two objects equipped with only two non-identity morphisms f and g , pointing in the same direction. It is possible to map the ordered pair of natural transformations <. a , i >. , where a sends to f and i is the identity natural transformation, to the other natural transformation b sending to g , i.e., define the morphism part P such that ( a ( U P V ) i ) = b such that ( bX ) = g given hypotheses of fuco23 . Such construction should be provable as a functor.

Given any P , it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of o.func , iff both of the following hold.

1. It has the same form as df-fuco up to fuco23 , but ( ( B ( U P V ) A )X ) might be mapped to a different morphism in category E . See fucofulem2 for some insights.

2. fuco22nat , fucoid , and fucoco are satisfied.

(Contributed by Zhi Wang, 3-Oct-2025)

Ref Expression
Hypotheses fucoco2.t ⊢ T = D FuncCat E × c C FuncCat D
fucoco2.q ⊢ Q = C FuncCat E
fucoco2.o No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
fucofunc.c ⊢ φ → C ∈ Cat
fucofunc.d ⊢ φ → D ∈ Cat
fucofunc.e ⊢ φ → E ∈ Cat
Assertion fucofunc ⊢ φ → O T Func Q P

Proof

Step Hyp Ref Expression
1 fucoco2.t ⊢ T = D FuncCat E × c C FuncCat D
2 fucoco2.q ⊢ Q = C FuncCat E
3 fucoco2.o Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
4 fucofunc.c ⊢ φ → C ∈ Cat
5 fucofunc.d ⊢ φ → D ∈ Cat
6 fucofunc.e ⊢ φ → E ∈ Cat
7 1 xpcfucbas ⊢ D Func E × C Func D = Base T
8 2 fucbas ⊢ C Func E = Base Q
9 eqid ⊢ Hom ⁡ T = Hom ⁡ T
10 eqid ⊢ C Nat E = C Nat E
11 2 10 fuchom ⊢ C Nat E = Hom ⁡ Q
12 eqid ⊢ Id ⁡ T = Id ⁡ T
13 eqid ⊢ Id ⁡ Q = Id ⁡ Q
14 eqid ⊢ comp ⁡ T = comp ⁡ T
15 eqid ⊢ comp ⁡ Q = comp ⁡ Q
16 eqid ⊢ D FuncCat E = D FuncCat E
17 16 5 6 fuccat ⊢ φ → D FuncCat E ∈ Cat
18 eqid ⊢ C FuncCat D = C FuncCat D
19 18 4 5 fuccat ⊢ φ → C FuncCat D ∈ Cat
20 1 17 19 xpccat ⊢ φ → T ∈ Cat
21 2 4 6 fuccat ⊢ φ → Q ∈ Cat
22 eqidd ⊢ φ → D Func E × C Func D = D Func E × C Func D
23 4 5 6 3 22 fucof1 ⊢ φ → O : D Func E × C Func D ⟶ C Func E
24 4 5 6 3 22 fucofn2 ⊢ φ → P Fn D Func E × C Func D × D Func E × C Func D
25 3 adantr Could not format ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
26 eqidd ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D → D Func E × C Func D = D Func E × C Func D
27 simprl ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D → x ∈ D Func E × C Func D
28 simprr ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D → y ∈ D Func E × C Func D
29 25 1 9 26 27 28 fucof21 ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D → x P y : x Hom ⁡ T y ⟶ O ⁡ x C Nat E O ⁡ y
30 3 adantr Could not format ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
31 eqidd ⊢ φ ∧ x ∈ D Func E × C Func D → D Func E × C Func D = D Func E × C Func D
32 simpr ⊢ φ ∧ x ∈ D Func E × C Func D → x ∈ D Func E × C Func D
33 30 1 12 2 13 31 32 fucoid2 ⊢ φ ∧ x ∈ D Func E × C Func D → x P x ⁡ Id ⁡ T ⁡ x = Id ⁡ Q ⁡ O ⁡ x
34 3 3ad2ant1 Could not format ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
35 eqidd ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → D Func E × C Func D = D Func E × C Func D
36 simp21 ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → x ∈ D Func E × C Func D
37 simp22 ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → y ∈ D Func E × C Func D
38 simp23 ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → z ∈ D Func E × C Func D
39 simp3l ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → m ∈ x Hom ⁡ T y
40 simp3r ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → n ∈ y Hom ⁡ T z
41 1 2 34 14 15 35 36 37 38 9 39 40 fucoco2 ⊢ φ ∧ x ∈ D Func E × C Func D ∧ y ∈ D Func E × C Func D ∧ z ∈ D Func E × C Func D ∧ m ∈ x Hom ⁡ T y ∧ n ∈ y Hom ⁡ T z → x P z ⁡ n x y comp ⁡ T z m = y P z ⁡ n O ⁡ x O ⁡ y comp ⁡ Q O ⁡ z x P y ⁡ m
42 7 8 9 11 12 13 14 15 20 21 23 24 29 33 41 isfuncd ⊢ φ → O T Func Q P