hom_ext_iff — Mathlib

English

In Karoubi(C), morphisms are determined by their underlying maps; two morphisms f,g: P → Q are equal iff their underlying maps f.f and g.f are equal.

Русский

В Karoubi(C) морфизмы определяются своими базовыми отображениями; два морфизма f,g: P → Q равны тогда и только тогда, когда их базовые отображения f.f и g.f равны.

LaTeX

$$$f = g \iff \underline{f} = \underline{g}$$$

Lean4

@[simp]
theorem hom_ext_iff {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f :=
  by
  constructor
  · intro h
    rw [h]
  · apply Hom.ext

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