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 | ⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) ) | |
| fucoco2.q | ⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 ) | ||
| fucoco2.o | ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ ) | ||
| fucofunc.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | ||
| fucofunc.d | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) | ||
| fucofunc.e | ⊢ ( 𝜑 → 𝐸 ∈ Cat ) | ||
| Assertion | fucofunc | ⊢ ( 𝜑 → 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fucoco2.t | ⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) ) | |
| 2 | fucoco2.q | ⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 ) | |
| 3 | fucoco2.o | ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ ) | |
| 4 | fucofunc.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | |
| 5 | fucofunc.d | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) | |
| 6 | fucofunc.e | ⊢ ( 𝜑 → 𝐸 ∈ Cat ) | |
| 7 | 1 | xpcfucbas | ⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ 𝑇 ) |
| 8 | 2 | fucbas | ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑄 ) |
| 9 | eqid | ⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 ) | |
| 10 | eqid | ⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 ) | |
| 11 | 2 10 | fuchom | ⊢ ( 𝐶 Nat 𝐸 ) = ( Hom ‘ 𝑄 ) |
| 12 | eqid | ⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 ) | |
| 13 | eqid | ⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 ) | |
| 14 | eqid | ⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 ) | |
| 15 | eqid | ⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 ) | |
| 16 | eqid | ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 ) | |
| 17 | 16 5 6 | fuccat | ⊢ ( 𝜑 → ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) |
| 18 | eqid | ⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 ) | |
| 19 | 18 4 5 | fuccat | ⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐷 ) ∈ Cat ) |
| 20 | 1 17 19 | xpccat | ⊢ ( 𝜑 → 𝑇 ∈ Cat ) |
| 21 | 2 4 6 | fuccat | ⊢ ( 𝜑 → 𝑄 ∈ Cat ) |
| 22 | eqidd | ⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 23 | 4 5 6 3 22 | fucof1 | ⊢ ( 𝜑 → 𝑂 : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 ) ) |
| 24 | 4 5 6 3 22 | fucofn2 | ⊢ ( 𝜑 → 𝑃 Fn ( ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) × ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) |
| 25 | 3 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ ) |
| 26 | eqidd | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 27 | simprl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) → 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 28 | simprr | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) → 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 29 | 25 1 9 26 27 28 | fucof21 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑦 ) ) ) |
| 30 | 3 | adantr | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ ) |
| 31 | eqidd | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 32 | simpr | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 33 | 30 1 12 2 13 31 32 | fucoid2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) → ( ( 𝑥 𝑃 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑄 ) ‘ ( 𝑂 ‘ 𝑥 ) ) ) |
| 34 | 3 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ ) |
| 35 | eqidd | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 36 | simp21 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 37 | simp22 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 38 | simp23 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) | |
| 39 | simp3l | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) | |
| 40 | simp3r | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) | |
| 41 | 1 2 34 14 15 35 36 37 38 9 39 40 | fucoco2 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑦 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∧ 𝑧 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑄 ) ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) |
| 42 | 7 8 9 11 12 13 14 15 20 21 23 24 29 33 41 | isfuncd | ⊢ ( 𝜑 → 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ) |