functor — Mathlib

English

LocallyConstant functor is naturally isomorphic to discrete functor.

Русский

Функтор локально-константный естественным образом изоморфен дискретному функтору.

LaTeX

$$$\text{LocallyConstant.functor} \cong \text{Discrete.functor}$$$

Lean4

/-- `functorToPresheaves` as a functor to condensed modules. -/
abbrev functor : ModuleCat R ⥤ CondensedMod.{u} R :=
  CompHausLike.LocallyConstantModule.functor.{u + 1, u} R (fun _ _ _ ↦ ((CompHaus.effectiveEpi_tfae _).out 0 2).mp)

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