hom_ext_uliftYoneda — Mathlib

English

Two morphisms in yonedaPairing are equal if they agree on every index Y; i.e., YonedaPairing Ext principle.

Русский

Два морфизма в yonedaPairing равны, если они совпадают на каждом индексе Y; принцип экстенциональности паринга Ёнеда.

LaTeX

$$$\forall Y, x.app Y = y.app Y \Rightarrow x = y$$$

Lean4

/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `uliftYoneda.obj X ⟶ P` agree. -/
theorem hom_ext_uliftYoneda {P Q : Cᵒᵖ ⥤ Type max w v₁} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : uliftYoneda.{w}.obj X ⟶ P), p ≫ f = p ≫ g) : f = g :=
  by
  ext X x
  simpa [uliftYonedaEquiv] using congr_arg uliftYonedaEquiv.{w} (h _ (uliftYonedaEquiv.symm x))

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