fullyFaithfulFunctor

Mathlib.Condensed.Discrete.Module

URI: https://scilib.ai/kg/mathlib#CondensedMod.LocallyConstant.fullyFaithfulFunctor

← MathLib Explorer

English

The LocallyConstant functor is fully faithful.

Русский

Функтор LocallyConstant полностью верен.

LaTeX

$$$\operatorname{FullyFaithful}(\mathrm{LocallyConstant.functor})$$$

Lean4

/-- `CondensedMod.LocallyConstant.functor` is fully faithful.
-/
noncomputable def fullyFaithfulFunctor : (functor R).FullyFaithful :=
  (adjunction R).fullyFaithfulLOfCompIsoId (NatIso.ofComponents fun M ↦ (functorIsoDiscreteAux₁ R _).symm)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru