functorHom_ext — Mathlib

English

Let C and D be categories and F, G: C ⥤ D be functors. For X in C, and x, y in (F.functorHom G).obj X, if x.app Y f = y.app Y f for every Y ∈ C and every morphism f: X ⟶ Y, then x = y.

Русский

Пусть C и D — категории, F и G: C ⥤ D — функторы. Пусть X ∈ Ob(C), и x, y ∈ (F.functorHom G).obj X. Если для каждого Y ∈ Ob(C) и каждого морфизма f: X ⟶ Y выполнено x.app Y f = y.app Y f, то x = y.

LaTeX

$$$\\forall \\{C\\} \\{D\\} [\\text{Category } C] [\\text{Category } D] \\{F G : C ⟩ D\\} \\{X \\} \\{x y : (F.functorHom G).obj X\\},\\ (\\forall (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f) \\Rightarrow x = y$$$

Lean4

@[ext]
theorem functorHom_ext {X : C} {x y : (F.functorHom G).obj X} (h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f) :
    x = y :=
  HomObj.ext (by ext; apply h)

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