Definition df-lan 50082

Description: Definition of the (local) left Kan extension. Given a functor 𝐹:𝐶⟶𝐷 and a functor 𝑋:𝐶⟶𝐸, the set (𝐹(⟨𝐶, 𝐷⟩ Lan 𝐸)𝑋) consists of left Kan extensions of 𝑋 along 𝐹, which are universal pairs from 𝑋 to the pre-composition functor given by 𝐹 (lanval2 50102). See also § 3 of Chapter X in p. 240 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf 50102 (retrieved 3 Nov 2025).

A left Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (lanrcl4 50109) and the second component is a natural transformation 𝐴:𝑋⟶𝐿𝐹 (lanrcl5 50110) where 𝐿𝐹 is the composed functor. Intuitively, the first component 𝐿 can be regarded as the result of an "inverse" of pre-composition; the source category of 𝑋:𝐶⟶𝐸 is "extended" along 𝐹:𝐶⟶𝐷.

The left Kan extension is a generalization of many categorical concepts such as colimit. In § 7 of Chapter X of Categories for the Working Mathematician, it is concluded that "the notion of Kan extensions subsumes all the other fundamental concepts of category theory".

This definition was chosen over the other version in the commented out section due to its better reverse closure property.

See df-ran 50083 for the dual concept.

(Contributed by Zhi Wang, 3-Nov-2025.)

Assertion

Ref	Expression
df-lan	⊢ Lan = (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥)))

Distinct variable group:   𝑐,𝑑,𝑒,𝑓,𝑝,𝑥

Detailed syntax breakdown of Definition df-lan

Step	Hyp	Ref	Expression
1		clan 50080	. 2 class Lan
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3429	. . . 4 class V
5	4, 4	cxp 5629	. . 3 class (V × V)
6		vc	. . . 4 setvar 𝑐
7	2	cv 1541	. . . . 5 class 𝑝
8		c1st 7940	. . . . 5 class 1st
9	7, 8	cfv 6498	. . . 4 class (1st ‘𝑝)
10		vd	. . . . 5 setvar 𝑑
11		c2nd 7941	. . . . . 6 class 2nd
12	7, 11	cfv 6498	. . . . 5 class (2nd ‘𝑝)
13		vf	. . . . . 6 setvar 𝑓
14		vx	. . . . . 6 setvar 𝑥
15	6	cv 1541	. . . . . . 7 class 𝑐
16	10	cv 1541	. . . . . . 7 class 𝑑
17		cfunc 17821	. . . . . . 7 class Func
18	15, 16, 17	co 7367	. . . . . 6 class (𝑐 Func 𝑑)
19	3	cv 1541	. . . . . . 7 class 𝑒
20	15, 19, 17	co 7367	. . . . . 6 class (𝑐 Func 𝑒)
21	16, 19	cop 4573	. . . . . . . 8 class ⟨𝑑, 𝑒⟩
22	13	cv 1541	. . . . . . . 8 class 𝑓
23		cprcof 49848	. . . . . . . 8 class −∘F
24	21, 22, 23	co 7367	. . . . . . 7 class (⟨𝑑, 𝑒⟩ −∘F 𝑓)
25	14	cv 1541	. . . . . . 7 class 𝑥
26		cfuc 17912	. . . . . . . . 9 class FuncCat
27	16, 19, 26	co 7367	. . . . . . . 8 class (𝑑 FuncCat 𝑒)
28	15, 19, 26	co 7367	. . . . . . . 8 class (𝑐 FuncCat 𝑒)
29		cup 49648	. . . . . . . 8 class UP
30	27, 28, 29	co 7367	. . . . . . 7 class ((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))
31	24, 25, 30	co 7367	. . . . . 6 class ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥)
32	13, 14, 18, 20, 31	cmpo 7369	. . . . 5 class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥))
33	10, 12, 32	csb 3837	. . . 4 class ⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥))
34	6, 9, 33	csb 3837	. . 3 class ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥))
35	2, 3, 5, 4, 34	cmpo 7369	. 2 class (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥)))
36	1, 35	wceq 1542	1 wff Lan = (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ ((⟨𝑑, 𝑒⟩ −∘F 𝑓)((𝑑 FuncCat 𝑒) UP (𝑐 FuncCat 𝑒))𝑥)))

This definition is referenced by:  lanfn  50084  reldmlan  50086  lanfval  50088  rellan  50098