finFree — Mathlib

English

There is a functor finFree from finite sets to condensed modules, giving the free condensed abelian group on a finite set.

Русский

Существaвает функтор finFree от конечных множеств к конденсированным модулям, задающий свободную конденсированную абелеву группу на конечном множестве.

LaTeX

$$$\mathrm{finFree} : \mathrm{FintypeCat} \to \mathrm{CondensedMod}(R)$$$

Lean4

/-- The free condensed abelian group on a finite set. -/
abbrev finFree : FintypeCat.{u} ⥤ CondensedMod.{u} R :=
  FintypeCat.toProfinite ⋙ profiniteToCondensed ⋙ free R

Похожие утверждения