profiniteFree — Mathlib

English

There is a functor profiniteFree from Profinite to condensed modules, giving the free condensed abelian group on a profinite space via profiniteToCondensed and free.

Русский

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

LaTeX

$$$\mathrm{profiniteFree} : \mathrm{Profinite} \to \mathrm{CondensedMod}(R)$$$

Lean4

/-- The free condensed abelian group on a profinite space. -/
abbrev profiniteFree : Profinite.{u} ⥤ CondensedMod.{u} R :=
  profiniteToCondensed ⋙ free R

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