instFaithfulModuleCatCondensedDiscrete

Mathlib.Condensed.Discrete.Module

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

English

The forgetful functor from discrete Condensed modules to Condensed modules is faithful.

Русский

Функтор забывания из дискретных Condensed модулей в Condensed модули верен.

LaTeX

$$$\operatorname{Faithful}((\text{Condensed.discrete}).\mathrm{Hom})$$$

Lean4

instance : (discrete (ModuleCat R)).Faithful :=
  Functor.Faithful.of_iso (functorIsoDiscrete R)

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

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

Разделы

Аффилиация

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