hom_ext

Mathlib.CategoryTheory.Action.Basic

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

English

Two Action morphisms are equal if their underlying maps are equal.

Русский

Два морфизма действия равны, если равны их базовые отображения.

LaTeX

$$$\forall \phi_1\phi_2:\ M \to N, \ (\phi_1.hom = \phi_2.hom) \Rightarrow \phi_1 = \phi_2$$$

Lean4

@[ext]
theorem hom_ext {M N : Action V G} (φ₁ φ₂ : M ⟶ N) (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂ :=
  Hom.ext h

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

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

Разделы

Аффилиация

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