Description: Definition of the (local) right Kan extension. Given a functor F : C --> D and a functor X : C --> E , the set ( F ( <. C , D >. Ran E ) X ) consists of right Kan extensions of X along F , which are universal pairs from the pre-composition functor given by F to X ( ranval2 ). 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 (retrieved 3 Nov 2025).
A right Kan extension is in the form of <. L , A >. where the first component is a functor L : D --> E ( ranrcl4 ) and the second component is a natural transformation A : L F --> X ( ranrcl5 ) 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 right Kan extension is a generalization of many categorical concepts such as limit. 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-lan for the dual concept.
(Contributed by Zhi Wang, 4-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ran | ⊢ Ran = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cran | ⊢ Ran | |
| 1 | vp | ⊢ 𝑝 | |
| 2 | cvv | ⊢ V | |
| 3 | 2 2 | cxp | ⊢ ( V × V ) |
| 4 | ve | ⊢ 𝑒 | |
| 5 | c1st | ⊢ 1st | |
| 6 | 1 | cv | ⊢ 𝑝 |
| 7 | 6 5 | cfv | ⊢ ( 1st ‘ 𝑝 ) |
| 8 | vc | ⊢ 𝑐 | |
| 9 | c2nd | ⊢ 2nd | |
| 10 | 6 9 | cfv | ⊢ ( 2nd ‘ 𝑝 ) |
| 11 | vd | ⊢ 𝑑 | |
| 12 | vf | ⊢ 𝑓 | |
| 13 | 8 | cv | ⊢ 𝑐 |
| 14 | cfunc | ⊢ Func | |
| 15 | 11 | cv | ⊢ 𝑑 |
| 16 | 13 15 14 | co | ⊢ ( 𝑐 Func 𝑑 ) |
| 17 | vx | ⊢ 𝑥 | |
| 18 | 4 | cv | ⊢ 𝑒 |
| 19 | 13 18 14 | co | ⊢ ( 𝑐 Func 𝑒 ) |
| 20 | coppf | ⊢ oppFunc | |
| 21 | 15 18 | cop | ⊢ ⟨ 𝑑 , 𝑒 ⟩ |
| 22 | cprcof | ⊢ −∘F | |
| 23 | 12 | cv | ⊢ 𝑓 |
| 24 | 21 23 22 | co | ⊢ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) |
| 25 | 24 20 | cfv | ⊢ ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) |
| 26 | coppc | ⊢ oppCat | |
| 27 | cfuc | ⊢ FuncCat | |
| 28 | 15 18 27 | co | ⊢ ( 𝑑 FuncCat 𝑒 ) |
| 29 | 28 26 | cfv | ⊢ ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) |
| 30 | cup | ⊢ UP | |
| 31 | 13 18 27 | co | ⊢ ( 𝑐 FuncCat 𝑒 ) |
| 32 | 31 26 | cfv | ⊢ ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) |
| 33 | 29 32 30 | co | ⊢ ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) |
| 34 | 17 | cv | ⊢ 𝑥 |
| 35 | 25 34 33 | co | ⊢ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) |
| 36 | 12 17 16 19 35 | cmpo | ⊢ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) |
| 37 | 11 10 36 | csb | ⊢ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) |
| 38 | 8 7 37 | csb | ⊢ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) |
| 39 | 1 4 3 2 38 | cmpo | ⊢ ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ) |
| 40 | 0 39 | wceq | ⊢ Ran = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ) |