hom_ext — Mathlib

English

If two arrows f, f' : X ⟶ limit F agree after composing with every projection π j, then f = f'. This is the standard extensionality principle for limits.

Русский

Если две стрелки f, f' : X ⟶ limit F совпадают после композиции с каждой проекцией π_j, то f = f'. Это стандартный принцип экстенсивности пределов.

LaTeX

$$$\\forall j, f \\circ π F j = f' \\circ π F j \\;\\Rightarrow\\; f = f'$$$

Lean4

@[ext]
theorem hom_ext {F : J ⥤ C} [HasLimit F] {X : C} {f f' : X ⟶ limit F} (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) :
    f = f' :=
  (limit.isLimit F).hom_ext w

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