English
There is a canonical natural transformation profiniteSolidCounit : FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R, given by the right Kan extension counit.
Русский
Существaет каноническая естественная трансформация profiniteSolidCounit: FintypeCat.toProfinite ⋙ profiniteSolid(R) ⟶ finFree(R), являющаяся каноническим пределом Кан extension.
LaTeX
$$$\mathrm{profiniteSolidCounit} : FintypeCat.toProfinite \circ \mathrm{profiniteSolid}(R) \Rightarrow \mathrm{finFree}(R)$$$
Lean4
/-- The natural transformation `FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R`
which is part of the assertion that `profiniteSolid R` is the (pointwise) right
Kan extension of `finFree R` along `FintypeCat.toProfinite`. -/
def profiniteSolidCounit : FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R :=
Functor.rightKanExtensionCounit FintypeCat.toProfinite (finFree R)
