English
There is a statement that profiniteSolid is a pointwise right Kan extension of finFree along FintypeCat.toProfinite, i.e., the right extension is determined objectwise.
Русский
Существует утверждение, что profiniteSolid является точечным правым Kan extension свободной конденсированной группы вдоль FintypeCat.toProfinite, то есть extension определяется по каждому объекту.
LaTeX
$$$\text{profiniteSolidIsPointwiseRightKanExtension} : (\mathrm{Functor.RightExtension.mk} _ (\mathrm{profiniteSolidCounit}(R))).IsPointwiseRightKanExtension$$$
Lean4
/-- The functor `Profinite.{u} ⥤ CondensedMod.{u} R` is a pointwise
right Kan extension of `finFree R : FintypeCat.{u} ⥤ CondensedMod.{u} R`
along `FintypeCat.toProfinite`. -/
def profiniteSolidIsPointwiseRightKanExtension :
(Functor.RightExtension.mk _ (profiniteSolidCounit R)).IsPointwiseRightKanExtension :=
Functor.isPointwiseRightKanExtensionOfIsRightKanExtension _ _
