English
There is a natural transformation profiniteSolidification : profiniteFree R ⟶ profiniteSolid R, built from the right Kan extension data, expressing the canonical map from generators to the solidified construction.
Русский
Существует естественная трансформация profiniteSolidification: Free на конденсированную сторону, задаваемая данными правого Kan extension, отображающая генераторы в твердую (solid) конструкцию.
LaTeX
$$$\mathrm{profiniteSolidification} : \mathrm{profiniteFree}(R) \to \mathrm{profiniteSolid}(R)$$$
Lean4
/-- The natural transformation `R[S] ⟶ R[S]^\solid`. -/
def profiniteSolidification : profiniteFree R ⟶ profiniteSolid.{u} R :=
(profiniteSolid R).liftOfIsRightKanExtension (profiniteSolidCounit R) _ (𝟙 _)
