free — Mathlib

English

LightCondensed.free is the left adjoint to Forget, i.e., it assigns to a condensed set its free condensed R-module.

Русский

LightCondensed.free — левый смежный к Forget; он присваивает конденсированному множеству свободный конденсированный R-модуль.

LaTeX

$$$\text{free} : \text{LightCondSet} \to \text{LightCondMod}(R)$ is left adjoint to $\text{forget}(R)$.$$

Lean4

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

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