hom_ext_yonedaULift — Mathlib

English

If two morphisms between sheaves yield equal compositions with all Yoneda-based arrows, then the morphisms are equal.

Русский

Если две стрелки между оболочками дают одинаковые композиции с любыми Yoneda-стрелами, то стрелки равны.

LaTeX

$$$\forall X\ p : J.yonedaULift.obj X ⟶ P, p \gg f = p \gg g \Rightarrow f = g$$$

Lean4

/-- Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree. -/
theorem hom_ext_yonedaULift {P Q : Sheaf J (Type (max v v'))} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : J.yonedaULift.obj X ⟶ P), p ≫ f = p ≫ g) : f = g :=
  by
  ext X x
  simpa only [yonedaULiftEquiv_comp, Equiv.apply_symm_apply] using
    congr_arg (J.yonedaULiftEquiv) (h _ (J.yonedaULiftEquiv.symm x))

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