ext — Mathlib

English

If Y is a cover of a terminal-like structure, then two arrows into a limit object are equal provided they agree on all projections to Y_i.

Русский

Если Y образует покрытие и имеется столпоподобная конструкция, то два отображения в предел совпадают, если они согласованы на каждом Y_i.

LaTeX

$$$J.CoversTop Y \\Rightarrow\\ \\forall X,\\ f,g:\\, X\\to c.pt,\\ (\\forall i, f\\!\\cdot\\pi_{Y_i}=g\\!\\cdot\\pi_{Y_i})\\Rightarrow f=g$$$

Lean4

theorem ext (F : Sheaf J A) {c : Cone F.1} (hc : IsLimit c) {X : A} {f g : X ⟶ c.pt}
    (h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))) : f = g :=
  by
  refine hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)
  rintro ⟨W, a, ⟨i, ⟨b⟩⟩⟩
  simpa using h i =≫ F.1.map b.op

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