Metamath Proof Explorer

Theorem cmdlan

Description: To each colimit of a diagram there is a corresponding left Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent ( diag1f1o ). (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses lmdran.1 
|- ( ph -> .1. e. TermCat )
lmdran.g 
|- ( ph -> G e. ( D Func .1. ) )
lmdran.l 
|- L = ( C DiagFunc .1. )
lmdran.y 
|- ( ph -> Y = ( ( 1st ` L ) ` X ) )
Assertion cmdlan 
|- ( ph -> ( X ( ( C Colimit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) )

Proof

Step Hyp Ref Expression
1 lmdran.1 
 |-  ( ph -> .1. e. TermCat )
2 lmdran.g 
 |-  ( ph -> G e. ( D Func .1. ) )
3 lmdran.l 
 |-  L = ( C DiagFunc .1. )
4 lmdran.y 
 |-  ( ph -> Y = ( ( 1st ` L ) ` X ) )
5 cmdfval2 
 |-  ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
6 5 breqi 
 |-  ( X ( ( C Colimit D ) ` F ) M <-> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M )
7 simpr 
 |-  ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M )
8 7 up1st2nd 
 |-  ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) M )
9 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
10 9 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
11 8 10 uprcl3 
 |-  ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 8 12 uprcl4 
 |-  ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) )
14 11 13 jca 
 |-  ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) )
15 simpr 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M )
16 15 up1st2nd 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( <. ( 1st ` ( <. .1. , C >. -o.F G ) ) , ( 2nd ` ( <. .1. , C >. -o.F G ) ) >. ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M )
17 16 10 uprcl3 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) )
18 4 adantr 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) )
19 eqid 
 |-  ( .1. FuncCat C ) = ( .1. FuncCat C )
20 19 fucbas 
 |-  ( .1. Func C ) = ( Base ` ( .1. FuncCat C ) )
21 16 20 uprcl4 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y e. ( .1. Func C ) )
22 relfunc 
 |-  Rel ( .1. Func C )
23 21 22 oppfrcllem 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y =/= (/) )
24 18 23 eqnetrrd 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) )
25 fvfundmfvn0 
 |-  ( ( ( 1st ` L ) ` X ) =/= (/) -> ( X e. dom ( 1st ` L ) /\ Fun ( ( 1st ` L ) |` { X } ) ) )
26 25 simpld 
 |-  ( ( ( 1st ` L ) ` X ) =/= (/) -> X e. dom ( 1st ` L ) )
27 24 26 syl 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. dom ( 1st ` L ) )
28 1 adantr 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat )
29 simpr 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> F e. ( D Func C ) )
30 29 func1st2nd 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
31 30 funcrcl3 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> C e. Cat )
32 12 28 31 3 diag1f1o 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) )
33 f1of 
 |-  ( ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` L ) : ( Base ` C ) --> ( .1. Func C ) )
34 32 33 syl 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` L ) : ( Base ` C ) --> ( .1. Func C ) )
35 34 fdmd 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> dom ( 1st ` L ) = ( Base ` C ) )
36 17 35 syldan 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) )
37 27 36 eleqtrd 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) )
38 17 37 jca 
 |-  ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) )
39 4 adantr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> Y = ( ( 1st ` L ) ` X ) )
40 eqid 
 |-  ( C DiagFunc D ) = ( C DiagFunc D )
41 2 adantr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> G e. ( D Func .1. ) )
42 31 adantrr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> C e. Cat )
43 eqidd 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) )
44 3 40 41 42 43 prcofdiag 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) )
45 simprr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> X e. ( Base ` C ) )
46 19 42 9 41 prcoffunca 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) )
47 31 28 19 3 diagffth 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> L e. ( ( C Full ( .1. FuncCat C ) ) i^i ( C Faith ( .1. FuncCat C ) ) ) )
48 47 adantrr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> L e. ( ( C Full ( .1. FuncCat C ) ) i^i ( C Faith ( .1. FuncCat C ) ) ) )
49 f1ofo 
 |-  ( ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` L ) : ( Base ` C ) -onto-> ( .1. Func C ) )
50 32 49 syl 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` L ) : ( Base ` C ) -onto-> ( .1. Func C ) )
51 50 adantrr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` L ) : ( Base ` C ) -onto-> ( .1. Func C ) )
52 12 20 39 44 45 46 48 51 uptr2a 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) )
53 14 38 52 bibiad 
 |-  ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) )
54 eqid 
 |-  ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G )
55 19 9 54 lanval2 
 |-  ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) )
56 2 55 syl 
 |-  ( ph -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) )
57 56 breqd 
 |-  ( ph -> ( Y ( G ( <. D , .1. >. Lan C ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) )
58 53 57 bitr4d 
 |-  ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) )
59 6 58 bitrid 
 |-  ( ph -> ( X ( ( C Colimit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) )