free — Mathlib

English

The left adjoint to forget: the free condensed R-module on a condensed set.

Русский

Левый сопряжённый к забыванию: свободный конденсированный R-модуль на конденсированном множестве.

LaTeX

$$$\text{Condensed.free}(R) : \text{CondensedSet} \to \text{CondensedMod } R$$$

Lean4

/-- The left adjoint to the forgetful functor. The *free condensed `R`-module* on a condensed set.
-/
noncomputable def free : CondensedSet ⥤ CondensedMod R :=
  Sheaf.composeAndSheafify _ (ModuleCat.free R)

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