hom_injective

Mathlib.CategoryTheory.Action.Basic

URI: https://scilib.ai/kg/mathlib#Action.hom_injective

English

The underlying map from morphisms to their action on objects is injective: Action.Hom.hom determines the morphism uniquely.

Русский

Растворение гомоморфизмов действия определяется однозначно по их действию на объекты.

LaTeX

$$∗ injectivity of Hom.hom$$

Lean4

theorem hom_injective {M N : Action V G} : Function.Injective (Hom.hom : (M ⟶ N) → (M.V ⟶ N.V)) := fun _ _ ↦ Hom.ext

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

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

Разделы

Аффилиация

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