English
There is an instance asserting that profiniteSolid R is the (pointwise) right Kan extension of finFree R along FintypeCat.toProfinite.
Русский
Существует инстанс, утверждающий, что profiniteSolid R является (точечным) правым Kan extension свободной конденсированной группы вдоль FintypeCat.toProfinite.
LaTeX
$$$\text{instance} : (\mathrm{profiniteSolid}(R)).IsRightKanExtension (\mathrm{profiniteSolidCounit}(R))$$$
Lean4
instance : (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R) :=
by
dsimp only [profiniteSolidCounit, profiniteSolid]
infer_instance
