functor_faithful

Mathlib.Topology.Category.TopCat.Opens

URI: https://scilib.ai/kg/mathlib#IsOpenMap.functor_faithful

English

The functor induced by an open embedding is faithful.

Русский

Функтор, индуцируемый открывающим вложением, верен (сохраняет различие гомоморфизмов).

LaTeX

$$$ hf.functor \text{ is faithful.}$$$

Lean4

instance functor_faithful {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : hf.functor.Faithful where

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

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

Разделы

Аффилиация

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