Definition df-ran 51122

Description: Definition of the (local) right Kan extension. Given a functor 𝐹:𝐶⟶𝐷 and a functor 𝑋:𝐶⟶𝐸, the set (𝐹(⟨𝐶, 𝐷⟩ Ran 𝐸)𝑋) consists of right Kan extensions of 𝑋 along 𝐹, which are universal pairs from the pre-composition functor given by 𝐹 to 𝑋 (ranval2 51144). The definition in § 3 of Chapter X in p. 236 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 51144 (retrieved 3 Nov 2025).

A right Kan extension is in the form of ⟨𝐿, 𝐴⟩ where the first component is a functor 𝐿:𝐷⟶𝐸 (ranrcl4 51153) and the second component is a natural transformation 𝐴:𝐿𝐹⟶𝑋 (ranrcl5 51154) 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 right Kan extension is a generalization of many categorical concepts such as limit. 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-lan 51121 for the dual concept.

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

Assertion

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

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

Detailed syntax breakdown of Definition df-ran

Step	Hyp	Ref	Expression
1		cran 51120	. 2 class Ran
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3454	. . . 4 class V
5	4, 4	cxp 5656	. . 3 class (V × V)
6		vc	. . . 4 setvar 𝑐
7	2	cv 1569	. . . . 5 class 𝑝
8		c1st 8033	. . . . 5 class 1st
9	7, 8	cfv 6566	. . . 4 class (1st ‘𝑝)
10		vd	. . . . 5 setvar 𝑑
11		c2nd 8034	. . . . . 6 class 2nd
12	7, 11	cfv 6566	. . . . 5 class (2nd ‘𝑝)
13		vf	. . . . . 6 setvar 𝑓
14		vx	. . . . . 6 setvar 𝑥
15	6	cv 1569	. . . . . . 7 class 𝑐
16	10	cv 1569	. . . . . . 7 class 𝑑
17		cfunc 18079	. . . . . . 7 class Func
18	15, 16, 17	co 7451	. . . . . 6 class (𝑐 Func 𝑑)
19	3	cv 1569	. . . . . . 7 class 𝑒
20	15, 19, 17	co 7451	. . . . . 6 class (𝑐 Func 𝑒)
21	16, 19	cop 4840	. . . . . . . . 9 class ⟨𝑑, 𝑒⟩
22	13	cv 1569	. . . . . . . . 9 class 𝑓
23		cprcof 50839	. . . . . . . . 9 class −∘F
24	21, 22, 23	co 7451	. . . . . . . 8 class (⟨𝑑, 𝑒⟩ −∘F 𝑓)
25		coppf 50569	. . . . . . . 8 class oppFunc
26	24, 25	cfv 6566	. . . . . . 7 class ( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))
27	14	cv 1569	. . . . . . 7 class 𝑥
28		cfuc 18170	. . . . . . . . . 10 class FuncCat
29	16, 19, 28	co 7451	. . . . . . . . 9 class (𝑑 FuncCat 𝑒)
30		coppc 17935	. . . . . . . . 9 class oppCat
31	29, 30	cfv 6566	. . . . . . . 8 class (oppCat‘(𝑑 FuncCat 𝑒))
32	15, 19, 28	co 7451	. . . . . . . . 9 class (𝑐 FuncCat 𝑒)
33	32, 30	cfv 6566	. . . . . . . 8 class (oppCat‘(𝑐 FuncCat 𝑒))
34		cup 50620	. . . . . . . 8 class UP
35	31, 33, 34	co 7451	. . . . . . 7 class ((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))
36	26, 27, 35	co 7451	. . . . . 6 class (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥)
37	13, 14, 18, 20, 36	cmpo 7453	. . . . 5 class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥))
38	10, 12, 37	csb 3851	. . . 4 class ⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥))
39	6, 9, 38	csb 3851	. . 3 class ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥))
40	2, 3, 5, 4, 39	cmpo 7453	. 2 class (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥)))
41	1, 40	wceq 1570	1 wff Ran = (𝑝 ∈ (V × V), 𝑒 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑐⦌⦋(2nd ‘𝑝) / 𝑑⦌(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (𝑐 Func 𝑒) ↦ (( oppFunc ‘(⟨𝑑, 𝑒⟩ −∘F 𝑓))((oppCat‘(𝑑 FuncCat 𝑒)) UP (oppCat‘(𝑐 FuncCat 𝑒)))𝑥)))

This definition is used by:  ranfn  51124  reldmran  51126  ranfval  51128  relran  51138