fst'_self_eq_snd — Mathlib

English

For representable presheaves with monomorphism base, the two projections fst' and snd coincide after applying the mono-preserving map.

Русский

Для представимого пресхрафа с мономорфным основанием сходятся проекции fst' и snd после применения мономорфной отображения.

LaTeX

$$$hf.rep.fst' f = hf.rep.snd f$$$

Lean4

theorem fst'_self_eq_snd (hP : P ≤ MorphismProperty.monomorphisms C) {X : C} {f : yoneda.obj X ⟶ G}
    (hf : P.presheaf f) : hf.rep.fst' f = hf.rep.snd f :=
  by
  have := P.presheaf_mono_of_le hP hf
  apply yoneda.map_injective
  rw [← cancel_mono f, (hf.rep.isPullback' f).w]

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