hom_ext — Mathlib

English

If two morphisms t1, t2: yoneda.obj X ⟶ P agree on the inclusion of S, then they are equal; this follows from unique_extend.

Русский

Если два морфизма t1, t2: yoneda.obj X → P совпадают на включении S, то они равны; это следует из уникального продолжения.

LaTeX

$$hom_ext (h : IsSheafFor P S.arrows) (t1 t2) (ht) : t1 = t2$$

Lean4

/-- If `P` is a sheaf for the sieve `S` on `X`, then if two natural transformations from `yoneda.obj X`
to `P` agree when restricted to the subfunctor given by `S`, they are equal.
-/
theorem hom_ext {P : Cᵒᵖ ⥤ Type v₁} (h : IsSheafFor P (S : Presieve X)) (t₁ t₂ : yoneda.obj X ⟶ P)
    (ht : S.functorInclusion ≫ t₁ = S.functorInclusion ≫ t₂) : t₁ = t₂ :=
  (h.unique_extend t₁ ht).trans (h.unique_extend t₂ rfl).symm

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