instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet

Mathlib.Condensed.Light.Functors

URI: https://scilib.ai/kg/mathlib#instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet

English

The Yoneda embedding for LightProfinite is full, yielding a full functor from LightProfinite to LightCondSet.

Русский

Юнэда-карта для LightProfinite полнота: функтор от LightProfinite к LightCondSet полон.

LaTeX

$$$\text{LightProfinite} \to \text{LightCondSet}$ is full.$$

Lean4

instance : lightProfiniteToLightCondSet.Full :=
  inferInstanceAs ((coherentTopology LightProfinite).yoneda).Full

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

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

Разделы

Аффилиация

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