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 ⊢ ( 𝜑 → 1 ∈ TermCat )
lmdran.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 1 ) )
lmdran.l ⊢ 𝐿 = ( 𝐶 Δfunc 1 )
lmdran.y ⊢ ( 𝜑 → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
Assertion cmdlan ( 𝜑 → ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) 𝑀 ) )

Proof

Step Hyp Ref Expression
1 lmdran.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
2 lmdran.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 1 ) )
3 lmdran.l ⊢ 𝐿 = ( 𝐶 Δfunc 1 )
4 lmdran.y ⊢ ( 𝜑 → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
5 cmdfval2 ⊢ ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
6 5 breqi ⊢ ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 )
8 7 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑋 ( ⟨ ( 1st ‘ ( 𝐶 Δfunc 𝐷 ) ) , ( 2nd ‘ ( 𝐶 Δfunc 𝐷 ) ) ⟩ ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 )
9 eqid ⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
10 9 fucbas ⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
11 8 10 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 8 12 uprcl4 ⊢ ( ( 𝜑 ∧ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
14 11 13 jca ⊢ ( ( 𝜑 ∧ 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 )
16 15 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑌 ( ⟨ ( 1st ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) , ( 2nd ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ⟩ ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 )
17 16 10 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
18 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
19 eqid ⊢ ( 1 FuncCat 𝐶 ) = ( 1 FuncCat 𝐶 )
20 19 fucbas ⊢ ( 1 Func 𝐶 ) = ( Base ‘ ( 1 FuncCat 𝐶 ) )
21 16 20 uprcl4 ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑌 ∈ ( 1 Func 𝐶 ) )
22 relfunc ⊢ Rel ( 1 Func 𝐶 )
23 21 22 oppfrcllem ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑌 ≠ ∅ )
24 18 23 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ )
25 fvfundmfvn0 ⊢ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom ( 1st ‘ 𝐿 ) ∧ Fun ( ( 1st ‘ 𝐿 ) ↾ { 𝑋 } ) ) )
26 25 simpld ⊢ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ dom ( 1st ‘ 𝐿 ) )
27 24 26 syl ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ dom ( 1st ‘ 𝐿 ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 1 ∈ TermCat )
29 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
30 29 func1st2nd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐹 ) )
31 30 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐶 ∈ Cat )
32 12 28 31 3 diag1f1o ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) )
33 f1of ⊢ ( ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( 1 Func 𝐶 ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( 1 Func 𝐶 ) )
35 34 fdmd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → dom ( 1st ‘ 𝐿 ) = ( Base ‘ 𝐶 ) )
36 17 35 syldan ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → dom ( 1st ‘ 𝐿 ) = ( Base ‘ 𝐶 ) )
37 27 36 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
38 17 37 jca ⊢ ( ( 𝜑 ∧ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
39 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
40 eqid ⊢ ( 𝐶 Δfunc 𝐷 ) = ( 𝐶 Δfunc 𝐷 )
41 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐷 Func 1 ) )
42 31 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
43 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) = ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) )
44 3 40 41 42 43 prcofdiag ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ∘func 𝐿 ) = ( 𝐶 Δfunc 𝐷 ) )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
46 19 42 9 41 prcoffunca ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ∈ ( ( 1 FuncCat 𝐶 ) Func ( 𝐷 FuncCat 𝐶 ) ) )
47 31 28 19 3 diagffth ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐿 ∈ ( ( 𝐶 Full ( 1 FuncCat 𝐶 ) ) ∩ ( 𝐶 Faith ( 1 FuncCat 𝐶 ) ) ) )
48 47 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐿 ∈ ( ( 𝐶 Full ( 1 FuncCat 𝐶 ) ) ∩ ( 𝐶 Faith ( 1 FuncCat 𝐶 ) ) ) )
49 f1ofo ⊢ ( ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –onto→ ( 1 Func 𝐶 ) )
50 32 49 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –onto→ ( 1 Func 𝐶 ) )
51 50 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –onto→ ( 1 Func 𝐶 ) )
52 12 20 39 44 45 46 48 51 uptr2a ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) )
53 14 38 52 bibiad ⊢ ( 𝜑 → ( 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) )
54 eqid ⊢ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) = ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 )
55 19 9 54 lanval2 ⊢ ( 𝐺 ∈ ( 𝐷 Func 1 ) → ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) = ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) )
56 2 55 syl ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) = ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) )
57 56 breqd ⊢ ( 𝜑 → ( 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ( ( 1 FuncCat 𝐶 ) UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ) )
58 53 57 bitr4d ⊢ ( 𝜑 → ( 𝑋 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) 𝑀 ) )
59 6 58 bitrid ⊢ ( 𝜑 → ( 𝑋 ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Lan 𝐶 ) 𝐹 ) 𝑀 ) )