Definition df-lan

Description: Definition of the (local) left Kan extension. Given a functor F : C --> D and a functor X : C --> E , the set ( F ( <. C , D >. Lan E ) X ) consists of left Kan extensions of X along F , which are universal pairs from X to the pre-composition functor given by F ( lanval2 ). 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 (retrieved 3 Nov 2025).

A left Kan extension is in the form of <. L , A >. where the first component is a functor L : D --> E ( lanrcl4 ) and the second component is a natural transformation A : X --> L F ( lanrcl5 ) where L F is the composed functor. Intuitively, the first component L can be regarded as the result of a "inverse" of pre-composition; the source category is "extended" along C --> D .

The left Kan extension is a generalization of many categorical concepts such as colimit. In § 7 of Chapter X ofCategories 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 for the dual concept.

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

	Ref	Expression
Assertion	df-lan	Could not format assertion : No typesetting found for |- Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clan	Could not format Lan : No typesetting found for class Lan with typecode class
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3	2 2	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
4		ve	$$setvare$$
5		c1st	$$class{1}^{st}$$
6	1	cv	$$setvarp$$
7	6 5	cfv	$$class{1}^{st}\left(p\right)$$
8		vc	$$setvarc$$
9		c2nd	$$class{2}^{nd}$$
10	6 9	cfv	$$class{2}^{nd}\left(p\right)$$
11		vd	$$setvard$$
12		vf	$$setvarf$$
13	8	cv	$$setvarc$$
14		cfunc	$$class\mathrm{Func}$$
15	11	cv	$$setvard$$
16	13 15 14	co	$$class\left(c\mathrm{Func}d\right)$$
17		vx	$$setvarx$$
18	4	cv	$$setvare$$
19	13 18 14	co	$$class\left(c\mathrm{Func}e\right)$$
20	15 18	cop	$$class⟨d,e⟩$$
21		cprcof	Could not format -o.F : No typesetting found for class -o.F with typecode class
22	12	cv	$$setvarf$$
23	20 22 21	co	Could not format ( <. d , e >. -o.F f ) : No typesetting found for class ( <. d , e >. -o.F f ) with typecode class
24		cfuc	$$class\mathrm{FuncCat}$$
25	15 18 24	co	$$class\left(d\mathrm{FuncCat}e\right)$$
26		cup	Could not format UP : No typesetting found for class UP with typecode class
27	13 18 24	co	$$class\left(c\mathrm{FuncCat}e\right)$$
28	25 27 26	co	Could not format ( ( d FuncCat e ) UP ( c FuncCat e ) ) : No typesetting found for class ( ( d FuncCat e ) UP ( c FuncCat e ) ) with typecode class
29	17	cv	$$setvarx$$
30	23 29 28	co	Could not format ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) : No typesetting found for class ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) with typecode class
31	12 17 16 19 30	cmpo	Could not format ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) : No typesetting found for class ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) with typecode class
32	11 10 31	csb	Could not format [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) : No typesetting found for class [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) with typecode class
33	8 7 32	csb	Could not format [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) : No typesetting found for class [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) with typecode class
34	1 4 3 2 33	cmpo	Could not format ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) : No typesetting found for class ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) with typecode class
35	0 34	wceq	Could not format Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) : No typesetting found for wff Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) with typecode wff